Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] Annotation of /sml/trunk/benchmarks/programs/boyer/terms.sml
ViewVC logotype

Annotation of /sml/trunk/benchmarks/programs/boyer/terms.sml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 193 - (view) (download)

1 : monnier 193 (* terms.sml:
2 :     *
3 :     * Manipulations over terms
4 :     *)
5 :    
6 :     signature TERMS =
7 :     sig
8 :     type head;
9 :     datatype term =
10 :     Var of int
11 :     | Prop of head * term list;
12 :     datatype binding = Bind of int * term;
13 :     val get: string -> head
14 :     and headname: head -> string
15 :     and add_lemma: term -> unit
16 :     and apply_subst: binding list -> term -> term
17 :     and rewrite: term -> term
18 :     end;
19 :    
20 :     structure Terms:TERMS =
21 :     struct
22 :    
23 :     datatype term
24 :     = Var of int
25 :     | Prop of { name: string, props: (term * term) list ref } * term list
26 :    
27 :     type head = { name: string, props: (term * term) list ref }
28 :    
29 :     val lemmas = ref ([] : head list)
30 :    
31 :     (* replacement for property lists *)
32 :    
33 :     fun headname {name = n, props=p} = n;
34 :    
35 :     fun get name =
36 :     let fun get_rec ((hd1 as {name=n,...})::hdl) =
37 :     if n = name then hd1 else get_rec hdl
38 :     | get_rec [] =
39 :     let val entry = {name = name, props = ref []} in
40 :     lemmas := entry :: !lemmas;
41 :     entry
42 :     end
43 :     in
44 :     get_rec (!lemmas)
45 :     end
46 :     ;
47 :    
48 :     fun add_lemma (Prop(_, [(left as Prop({props=r,...},_)), right])) =
49 :     r := (left, right) :: !r
50 :     ;
51 :    
52 :     (* substitutions *)
53 :    
54 :     exception failure of string;
55 :    
56 :     datatype binding = Bind of int * term
57 :     ;
58 :    
59 :     fun get_binding v =
60 :     let fun get_rec [] = raise (failure "unbound")
61 :     | get_rec (Bind(w,t)::rest) =
62 :     if v = w then t else get_rec rest
63 :     in
64 :     get_rec
65 :     end
66 :     ;
67 :    
68 :     fun apply_subst alist =
69 :     let fun as_rec (term as Var v) =
70 :     ((get_binding v alist) handle failure _ => term)
71 :     | as_rec (Prop (head,argl)) =
72 :     Prop (head, map as_rec argl)
73 :     in
74 :     as_rec
75 :     end
76 :     ;
77 :    
78 :     exception Unify;
79 :    
80 :     fun unify (term1, term2) = unify1 (term1, term2, [])
81 :     and unify1 (term1, term2, unify_subst) =
82 :     (case term2 of
83 :     Var v =>
84 :     ((if get_binding v unify_subst = term1
85 :     then unify_subst
86 :     else raise Unify)
87 :     handle failure _ =>
88 :     Bind(v,term1)::unify_subst)
89 :     | Prop (head2,argl2) =>
90 :     case term1 of
91 :     Var _ => raise Unify
92 :     | Prop (head1,argl1) =>
93 :     if head1=head2 then unify1_lst (argl1, argl2, unify_subst)
94 :     else raise Unify)
95 :     and unify1_lst ([], [], unify_subst) = unify_subst
96 :     | unify1_lst (h1::r1, h2::r2, unify_subst) =
97 :     unify1_lst(r1, r2, unify1(h1, h2, unify_subst))
98 :     | unify1_lst _ = raise Unify
99 :     ;
100 :    
101 :     fun rewrite (term as Var _) = term
102 :     | rewrite (Prop ((head as {props=p,...}), argl)) =
103 :     rewrite_with_lemmas (Prop (head, map rewrite argl), !p)
104 :     and rewrite_with_lemmas (term, []) = term
105 :     | rewrite_with_lemmas (term, (t1,t2)::rest) =
106 :     rewrite (apply_subst (unify (term, t1)) t2)
107 :     handle unify =>
108 :     rewrite_with_lemmas (term, rest)
109 :     ;
110 :     end;

root@smlnj-gforge.cs.uchicago.edu
ViewVC Help
Powered by ViewVC 1.0.0