--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/TFL/usyntax.sml Fri Oct 18 12:41:04 1996 +0200
@@ -0,0 +1,482 @@
+structure USyntax : USyntax_sig =
+struct
+
+structure Utils = Utils;
+open Utils;
+open Mask;
+
+infix 7 |->;
+infix 4 ##;
+
+fun ERR{func,mesg} = Utils.ERR{module = "USyntax", func = func, mesg = mesg};
+
+type Type = typ
+type Term = cterm
+type Preterm = term
+
+
+(*---------------------------------------------------------------------------
+ *
+ * Types
+ *
+ *---------------------------------------------------------------------------*)
+fun mk_type{Tyop, Args} = Type(Tyop,Args);
+val mk_prim_vartype = TVar;
+fun mk_vartype s = mk_prim_vartype((s,0),["term"]);
+
+fun dest_type(Type(ty,args)) = {Tyop = ty, Args = args}
+ | dest_type _ = raise ERR{func = "dest_type", mesg = "Not a compound type"};
+
+
+(* But internally, it's useful *)
+fun dest_vtype (TVar x) = x
+ | dest_vtype _ = raise ERR{func = "dest_vtype",
+ mesg = "not a flexible type variable"};
+
+val is_vartype = Utils.can dest_vtype;
+
+val type_vars = map mk_prim_vartype o typ_tvars
+fun type_varsl L = Utils.mk_set (Utils.curry op=)
+ (Utils.rev_itlist (Utils.curry op @ o type_vars) L []);
+
+val alpha = mk_vartype "'a"
+val beta = mk_vartype "'b"
+
+val bool = Type("bool",[]);
+
+fun match_type ty1 ty2 = raise ERR{func="match_type",mesg="not implemented"};
+
+
+(* What nonsense *)
+nonfix -->;
+val --> = -->;
+infixr 3 -->;
+
+(* hol_type -> hol_type list * hol_type *)
+fun strip_type ty =
+ let val {Tyop = "fun", Args = [ty1,ty2]} = dest_type ty
+ val (D,r) = strip_type ty2
+ in (ty1::D, r)
+ end
+ handle _ => ([],ty);
+
+(* hol_type -> hol_type list *)
+fun strip_prod_type ty =
+ let val {Tyop = "*", Args = [ty1,ty2]} = dest_type ty
+ in strip_prod_type ty1 @ strip_prod_type ty2
+ end handle _ => [ty];
+
+
+
+(*---------------------------------------------------------------------------
+ *
+ * Terms
+ *
+ *---------------------------------------------------------------------------*)
+nonfix aconv;
+val aconv = Utils.curry (op aconv);
+
+fun free_vars tm = add_term_frees(tm,[]);
+
+
+(* Free variables, in order of occurrence, from left to right in the
+ * syntax tree. *)
+fun free_vars_lr tm =
+ let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end
+ fun add (t, frees) = case t of
+ Free _ => if (memb t frees) then frees else t::frees
+ | Abs (_,_,body) => add(body,frees)
+ | f$t => add(t, add(f, frees))
+ | _ => frees
+ in rev(add(tm,[]))
+ end;
+
+
+
+fun free_varsl L = Utils.mk_set aconv
+ (Utils.rev_itlist (Utils.curry op @ o free_vars) L []);
+
+val type_of = type_of;
+val type_vars_in_term = map mk_prim_vartype o term_tvars;
+
+(* Can't really be very exact in Isabelle *)
+fun all_vars tm =
+ let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end
+ fun add (t, A) = case t of
+ Free _ => if (memb t A) then A else t::A
+ | Abs (s,ty,body) => add(body, add(Free(s,ty),A))
+ | f$t => add(t, add(f, A))
+ | _ => A
+ in rev(add(tm,[]))
+ end;
+fun all_varsl L = Utils.mk_set aconv
+ (Utils.rev_itlist (Utils.curry op @ o all_vars) L []);
+
+
+(* Prelogic *)
+val subst = subst_free o map (fn (a |-> b) => (a,b));
+
+fun dest_tybinding (v |-> ty) = (#1(dest_vtype v),ty)
+fun inst theta = subst_vars (map dest_tybinding theta,[])
+
+fun beta_conv((t1 as Abs _ ) $ t2) = betapply(t1,t2)
+ | beta_conv _ = raise ERR{func = "beta_conv", mesg = "Not a beta-redex"};
+
+
+(* Construction routines *)
+(* fun mk_var{Name,Ty} = Var((Name,0),Ty); *)
+fun mk_var{Name,Ty} = Free(Name,Ty);
+val mk_prim_var = Var;
+
+val string_variant = variant;
+
+local fun var_name(Var((Name,_),_)) = Name
+ | var_name(Free(s,_)) = s
+ | var_name _ = raise ERR{func = "variant",
+ mesg = "list elem. is not a variable"}
+in
+fun variant [] v = v
+ | variant vlist (Var((Name,i),ty)) =
+ Var((string_variant (map var_name vlist) Name,i),ty)
+ | variant vlist (Free(Name,ty)) =
+ Free(string_variant (map var_name vlist) Name,ty)
+ | variant _ _ = raise ERR{func = "variant",
+ mesg = "2nd arg. should be a variable"}
+end;
+
+fun mk_const{Name,Ty} = Const(Name,Ty)
+fun mk_comb{Rator,Rand} = Rator $ Rand;
+
+fun mk_abs{Bvar as Var((s,_),ty),Body} = Abs(s,ty,abstract_over(Bvar,Body))
+ | mk_abs{Bvar as Free(s,ty),Body} = Abs(s,ty,abstract_over(Bvar,Body))
+ | mk_abs _ = raise ERR{func = "mk_abs", mesg = "Bvar is not a variable"};
+
+fun list_mk_comb (h,[]) = h
+ | list_mk_comb (h,L) =
+ rev_itlist (fn t1 => fn t2 => mk_comb{Rator = t2, Rand = t1}) L h;
+
+
+fun mk_eq{lhs,rhs} =
+ let val ty = type_of lhs
+ val c = mk_const{Name = "op =", Ty = ty --> ty --> bool}
+ in list_mk_comb(c,[lhs,rhs])
+ end
+
+fun mk_imp{ant,conseq} =
+ let val c = mk_const{Name = "op -->", Ty = bool --> bool --> bool}
+ in list_mk_comb(c,[ant,conseq])
+ end;
+
+fun mk_select (r as {Bvar,Body}) =
+ let val ty = type_of Bvar
+ val c = mk_const{Name = "Eps", Ty = (ty --> bool) --> ty}
+ in list_mk_comb(c,[mk_abs r])
+ end;
+
+fun mk_forall (r as {Bvar,Body}) =
+ let val ty = type_of Bvar
+ val c = mk_const{Name = "All", Ty = (ty --> bool) --> bool}
+ in list_mk_comb(c,[mk_abs r])
+ end;
+
+fun mk_exists (r as {Bvar,Body}) =
+ let val ty = type_of Bvar
+ val c = mk_const{Name = "Ex", Ty = (ty --> bool) --> bool}
+ in list_mk_comb(c,[mk_abs r])
+ end;
+
+
+fun mk_conj{conj1,conj2} =
+ let val c = mk_const{Name = "op &", Ty = bool --> bool --> bool}
+ in list_mk_comb(c,[conj1,conj2])
+ end;
+
+fun mk_disj{disj1,disj2} =
+ let val c = mk_const{Name = "op |", Ty = bool --> bool --> bool}
+ in list_mk_comb(c,[disj1,disj2])
+ end;
+
+fun prod_ty ty1 ty2 = mk_type{Tyop = "*", Args = [ty1,ty2]};
+
+local
+fun mk_uncurry(xt,yt,zt) =
+ mk_const{Name = "split", Ty = (xt --> yt --> zt) --> prod_ty xt yt --> zt}
+fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
+ | dest_pair _ = raise ERR{func = "dest_pair", mesg = "not a pair"}
+fun is_var(Var(_)) = true | is_var (Free _) = true | is_var _ = false
+in
+fun mk_pabs{varstruct,body} =
+ let fun mpa(varstruct,body) =
+ if (is_var varstruct)
+ then mk_abs{Bvar = varstruct, Body = body}
+ else let val {fst,snd} = dest_pair varstruct
+ in mk_comb{Rator= mk_uncurry(type_of fst,type_of snd,type_of body),
+ Rand = mpa(fst,mpa(snd,body))}
+ end
+ in mpa(varstruct,body)
+ end
+ handle _ => raise ERR{func = "mk_pabs", mesg = ""};
+end;
+
+(* Destruction routines *)
+
+datatype lambda = VAR of {Name : string, Ty : Type}
+ | CONST of {Name : string, Ty : Type}
+ | COMB of {Rator: Preterm, Rand : Preterm}
+ | LAMB of {Bvar : Preterm, Body : Preterm};
+
+
+fun dest_term(Var((s,i),ty)) = VAR{Name = s, Ty = ty}
+ | dest_term(Free(s,ty)) = VAR{Name = s, Ty = ty}
+ | dest_term(Const(s,ty)) = CONST{Name = s, Ty = ty}
+ | dest_term(M$N) = COMB{Rator=M,Rand=N}
+ | dest_term(Abs(s,ty,M)) = let val v = mk_var{Name = s, Ty = ty}
+ in LAMB{Bvar = v, Body = betapply (M,v)}
+ end
+ | dest_term(Bound _) = raise ERR{func = "dest_term",mesg = "Bound"};
+
+fun dest_var(Var((s,i),ty)) = {Name = s, Ty = ty}
+ | dest_var(Free(s,ty)) = {Name = s, Ty = ty}
+ | dest_var _ = raise ERR{func = "dest_var", mesg = "not a variable"};
+
+fun dest_const(Const(s,ty)) = {Name = s, Ty = ty}
+ | dest_const _ = raise ERR{func = "dest_const", mesg = "not a constant"};
+
+fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2}
+ | dest_comb _ = raise ERR{func = "dest_comb", mesg = "not a comb"};
+
+fun dest_abs(a as Abs(s,ty,M)) =
+ let val v = mk_var{Name = s, Ty = ty}
+ in {Bvar = v, Body = betapply (a,v)}
+ end
+ | dest_abs _ = raise ERR{func = "dest_abs", mesg = "not an abstraction"};
+
+fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N}
+ | dest_eq _ = raise ERR{func = "dest_eq", mesg = "not an equality"};
+
+fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N}
+ | dest_imp _ = raise ERR{func = "dest_imp", mesg = "not an implication"};
+
+fun dest_select(Const("Eps",_) $ (a as Abs _)) = dest_abs a
+ | dest_select _ = raise ERR{func = "dest_select", mesg = "not a select"};
+
+fun dest_forall(Const("All",_) $ (a as Abs _)) = dest_abs a
+ | dest_forall _ = raise ERR{func = "dest_forall", mesg = "not a forall"};
+
+fun dest_exists(Const("Ex",_) $ (a as Abs _)) = dest_abs a
+ | dest_exists _ = raise ERR{func = "dest_exists", mesg="not an existential"};
+
+fun dest_neg(Const("not",_) $ M) = M
+ | dest_neg _ = raise ERR{func = "dest_neg", mesg = "not a negation"};
+
+fun dest_conj(Const("op &",_) $ M $ N) = {conj1=M, conj2=N}
+ | dest_conj _ = raise ERR{func = "dest_conj", mesg = "not a conjunction"};
+
+fun dest_disj(Const("op |",_) $ M $ N) = {disj1=M, disj2=N}
+ | dest_disj _ = raise ERR{func = "dest_disj", mesg = "not a disjunction"};
+
+fun mk_pair{fst,snd} =
+ let val ty1 = type_of fst
+ val ty2 = type_of snd
+ val c = mk_const{Name = "Pair", Ty = ty1 --> ty2 --> prod_ty ty1 ty2}
+ in list_mk_comb(c,[fst,snd])
+ end;
+
+fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
+ | dest_pair _ = raise ERR{func = "dest_pair", mesg = "not a pair"};
+
+
+local val ucheck = Utils.assert (curry (op =) "split" o #Name o dest_const)
+in
+fun dest_pabs tm =
+ let val {Bvar,Body} = dest_abs tm
+ in {varstruct = Bvar, body = Body}
+ end handle _
+ => let val {Rator,Rand} = dest_comb tm
+ val _ = ucheck Rator
+ val {varstruct = lv,body} = dest_pabs Rand
+ val {varstruct = rv,body} = dest_pabs body
+ in {varstruct = mk_pair{fst = lv, snd = rv}, body = body}
+ end
+end;
+
+
+(* Garbage - ought to be dropped *)
+val lhs = #lhs o dest_eq
+val rhs = #rhs o dest_eq
+val rator = #Rator o dest_comb
+val rand = #Rand o dest_comb
+val bvar = #Bvar o dest_abs
+val body = #Body o dest_abs
+
+
+(* Query routines *)
+val is_var = can dest_var
+val is_const = can dest_const
+val is_comb = can dest_comb
+val is_abs = can dest_abs
+val is_eq = can dest_eq
+val is_imp = can dest_imp
+val is_forall = can dest_forall
+val is_exists = can dest_exists
+val is_neg = can dest_neg
+val is_conj = can dest_conj
+val is_disj = can dest_disj
+val is_pair = can dest_pair
+val is_pabs = can dest_pabs
+
+
+(* Construction of a Term from a list of Terms *)
+
+fun list_mk_abs(L,tm) = itlist (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm;
+
+(* These others are almost never used *)
+fun list_mk_imp(A,c) = itlist(fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;
+fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists{Bvar=v, Body=b})V t;
+fun list_mk_forall(V,t) = itlist(fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
+val list_mk_conj = end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm})
+val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj{disj1=d1, disj2=tm})
+
+
+(* Need to reverse? *)
+fun gen_all tm = list_mk_forall(free_vars tm, tm);
+
+(* Destructing a Term to a list of Terms *)
+fun strip_comb tm =
+ let fun dest(M$N, A) = dest(M, N::A)
+ | dest x = x
+ in dest(tm,[])
+ end;
+
+fun strip_abs(tm as Abs _) =
+ let val {Bvar,Body} = dest_abs tm
+ val (bvs, core) = strip_abs Body
+ in (Bvar::bvs, core)
+ end
+ | strip_abs M = ([],M);
+
+
+fun strip_imp fm =
+ if (is_imp fm)
+ then let val {ant,conseq} = dest_imp fm
+ val (was,wb) = strip_imp conseq
+ in ((ant::was), wb)
+ end
+ else ([],fm);
+
+fun strip_forall fm =
+ if (is_forall fm)
+ then let val {Bvar,Body} = dest_forall fm
+ val (bvs,core) = strip_forall Body
+ in ((Bvar::bvs), core)
+ end
+ else ([],fm);
+
+
+fun strip_exists fm =
+ if (is_exists fm)
+ then let val {Bvar, Body} = dest_exists fm
+ val (bvs,core) = strip_exists Body
+ in (Bvar::bvs, core)
+ end
+ else ([],fm);
+
+fun strip_conj w =
+ if (is_conj w)
+ then let val {conj1,conj2} = dest_conj w
+ in (strip_conj conj1@strip_conj conj2)
+ end
+ else [w];
+
+fun strip_disj w =
+ if (is_disj w)
+ then let val {disj1,disj2} = dest_disj w
+ in (strip_disj disj1@strip_disj disj2)
+ end
+ else [w];
+
+fun strip_pair tm =
+ if (is_pair tm)
+ then let val {fst,snd} = dest_pair tm
+ fun dtuple t =
+ if (is_pair t)
+ then let val{fst,snd} = dest_pair t
+ in (fst :: dtuple snd)
+ end
+ else [t]
+ in fst::dtuple snd
+ end
+ else [tm];
+
+
+fun mk_preterm tm = #t(rep_cterm tm);
+
+fun mk_prop (tm as Const("Trueprop",_) $ _) = tm
+ | mk_prop tm = mk_comb{Rator=mk_const{Name = "Trueprop",
+ Ty = bool --> mk_type{Tyop = "prop",Args=[]}},
+ Rand = tm};
+
+fun drop_Trueprop (Const("Trueprop",_) $ X) = X
+ | drop_Trueprop X = X;
+
+(* Miscellaneous *)
+
+fun mk_vstruct ty V =
+ let fun follow_prod_type ty vs =
+ let val {Tyop = "*", Args = [ty1,ty2]} = dest_type ty
+ val (ltm,vs1) = follow_prod_type ty1 vs
+ val (rtm,vs2) = follow_prod_type ty2 vs1
+ in (mk_pair{fst=ltm, snd=rtm}, vs2)
+ end handle _ => (hd vs, tl vs)
+ in fst(follow_prod_type ty V)
+ end;
+
+
+(* Search a term for a sub-term satisfying the predicate p. *)
+fun find_term p =
+ let fun find tm =
+ if (p tm)
+ then tm
+ else if (is_abs tm)
+ then find (#Body(dest_abs tm))
+ else let val {Rator,Rand} = dest_comb tm
+ in find Rator handle _ => find Rand
+ end handle _ => raise ERR{func = "find_term",mesg = ""}
+ in find
+ end;
+
+(*******************************************************************
+ * find_terms: (term -> bool) -> term -> term list
+ *
+ * Find all subterms in a term that satisfy a given predicate p.
+ *
+ *******************************************************************)
+fun find_terms p =
+ let fun accum tl tm =
+ let val tl' = if (p tm) then (tm::tl) else tl
+ in if (is_abs tm)
+ then accum tl' (#Body(dest_abs tm))
+ else let val {Rator,Rand} = dest_comb tm
+ in accum (accum tl' Rator) Rand
+ end handle _ => tl'
+ end
+ in accum []
+ end;
+
+
+val Term_to_string = string_of_cterm;
+
+fun dest_relation tm =
+ if (type_of tm = bool)
+ then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm
+ in (R,y,x)
+ end handle _ => raise ERR{func="dest_relation",
+ mesg="unexpected term structure"}
+ else raise ERR{func="dest_relation",mesg="not a boolean term"};
+
+fun is_WFR tm = (#Name(dest_const(rator tm)) = "wf") handle _ => false;
+
+fun ARB ty = mk_select{Bvar=mk_var{Name="v",Ty=ty},
+ Body=mk_const{Name="True",Ty=bool}};
+
+end; (* Syntax *)