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