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/todo/vboyer/terms.sml
ViewVC logotype

Annotation of /sml/trunk/benchmarks/todo/vboyer/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 Vector.vector;
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 :     open VectorUtil
24 :    
25 :     datatype term
26 :     = Var of int
27 :     | Prop of head * term Vector.vector
28 :     withtype head = { name: string, props: (term * term) list ref }
29 :    
30 :     val lemmas = ref ([] : head list)
31 :    
32 :     (* replacement for property lists *)
33 :    
34 :     fun headname {name = n, props=p} = n
35 :    
36 :     fun get name =
37 :     let fun get_rec ((hd1 as {name=n,...})::hdl) =
38 :     if n = name then hd1 else get_rec hdl
39 :     | get_rec [] =
40 :     let val entry = {name = name, props = ref []} in
41 :     lemmas := entry :: !lemmas;
42 :     entry
43 :     end
44 :     in
45 :     get_rec (!lemmas)
46 :     end
47 :    
48 :     fun add_lemma (Prop(_, #[(left as Prop({props=r,...},_)), right])) =
49 :     r := (left, right) :: !r
50 :    
51 :     (* substitutions *)
52 :    
53 :     exception failure of string;
54 :    
55 :     datatype binding = Bind of int * term
56 :    
57 :     fun get_binding v =
58 :     let fun get_rec [] = raise (failure "unbound")
59 :     | get_rec (Bind(w,t)::rest) =
60 :     if v = w then t else get_rec rest
61 :     in
62 :     get_rec
63 :     end
64 :    
65 :     fun apply_subst alist =
66 :     let fun as_rec (term as Var v) =
67 :     ((get_binding v alist) handle failure _ => term)
68 :     | as_rec (Prop (head,argl)) =
69 :     Prop (head, mapv as_rec argl)
70 :     in
71 :     as_rec
72 :     end
73 :    
74 :     exception Unify;
75 :    
76 :     fun unify (term1, term2) = unify1 (term1, term2, [])
77 :     and unify1 (term1, term2, unify_subst) =
78 :     (case term2 of
79 :     Var v =>
80 :     ((if get_binding v unify_subst = term1
81 :     then unify_subst
82 :     else raise Unify)
83 :     handle failure _ =>
84 :     Bind(v,term1)::unify_subst)
85 :     | Prop (head2,argl2) => (case term1
86 :     of Var _ => raise Unify
87 :     | Prop (head1,argl1) => if head1=head2
88 :     then unify1_lst (listOfVector argl1, listOfVector argl2, unify_subst)
89 :     else raise Unify))
90 :    
91 :     and unify1_lst ([], [], unify_subst) = unify_subst
92 :     | unify1_lst (h1::r1, h2::r2, unify_subst) =
93 :     unify1_lst(r1, r2, unify1(h1, h2, unify_subst))
94 :     | unify1_lst _ = raise Unify
95 :    
96 :     fun rewrite (term as Var _) = term
97 :     | rewrite (Prop ((head as {props=p,...}), argl)) =
98 :     rewrite_with_lemmas (Prop (head, mapv rewrite argl), !p)
99 :     and rewrite_with_lemmas (term, []) = term
100 :     | rewrite_with_lemmas (term, (t1,t2)::rest) =
101 :     rewrite (apply_subst (unify (term, t1)) t2)
102 :     handle unify =>
103 :     rewrite_with_lemmas (term, rest)
104 :    
105 :     end; (* Terms *)

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