# HG changeset patch # User berghofe # Date 952696626 -3600 # Node ID a217b0cd304d6d37e764cbd572f141d30a16b06b # Parent 0255394a05dac3f1fd1a72a0a485bb9e15ebd1c7 Type.unify and Type.typ_match now use Vartab instead of association lists. diff -r 0255394a05da -r a217b0cd304d src/Pure/drule.ML --- a/src/Pure/drule.ML Fri Mar 10 01:16:19 2000 +0100 +++ b/src/Pure/drule.ML Fri Mar 10 14:57:06 2000 +0100 @@ -560,12 +560,12 @@ in (sign', tye', maxi') end; in fun cterm_instantiate ctpairs0 th = - let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th),[],0)) + let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th), Vartab.empty, 0)) val tsig = #tsig(Sign.rep_sg sign); - fun instT(ct,cu) = let val inst = subst_TVars tye + fun instT(ct,cu) = let val inst = subst_TVars_Vartab tye in (cterm_fun inst ct, cterm_fun inst cu) end fun ctyp2 (ix,T) = (ix, ctyp_of sign T) - in instantiate (map ctyp2 tye, map instT ctpairs0) th end + in instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th end handle TERM _ => raise THM("cterm_instantiate: incompatible signatures",0,[th]) | TYPE (msg, _, _) => raise THM(msg, 0, [th]) diff -r 0255394a05da -r a217b0cd304d src/Pure/pattern.ML --- a/src/Pure/pattern.ML Fri Mar 10 01:16:19 2000 +0100 +++ b/src/Pure/pattern.ML Fri Mar 10 14:57:06 2000 +0100 @@ -332,8 +332,8 @@ | _ => raise MATCH in mtch end; -fun first_order_match tsig = fomatch tsig ([],[]); - +fun first_order_match tsig = apfst Vartab.dest o fomatch tsig (Vartab.empty, []); + (* Matching of higher-order patterns *) fun match_bind(itms,binders,ixn,is,t) = @@ -355,7 +355,7 @@ Abs(ns,Ts,ts) => (case obj of Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (env,(ts,tt)) - | _ => let val Tt = typ_subst_TVars iTs Ts + | _ => let val Tt = typ_subst_TVars_Vartab iTs Ts in mtch((ns,Tt)::binders)(env,(ts,(incr obj)$Bound(0))) end) | _ => (case obj of Abs(nt,Tt,tt) => @@ -392,11 +392,11 @@ val pT = fastype_of pat and oT = fastype_of obj - val iTs = typ_match tsg ([],(pT,oT)) + val iTs = typ_match tsg (Vartab.empty, (pT,oT)) val insts2 = (iTs,[]) -in mtch [] (insts2, po) - handle Pattern => fomatch tsg insts2 po +in apfst Vartab.dest (mtch [] (insts2, po) + handle Pattern => fomatch tsg insts2 po) end; (*Predicate: does the pattern match the object?*) diff -r 0255394a05da -r a217b0cd304d src/Pure/type.ML --- a/src/Pure/type.ML Fri Mar 10 01:16:19 2000 +0100 +++ b/src/Pure/type.ML Fri Mar 10 14:57:06 2000 +0100 @@ -47,18 +47,19 @@ val norm_typ: type_sig -> typ -> typ val norm_term: type_sig -> term -> term val inst_term_tvars: type_sig * (indexname * typ) list -> term -> term + val inst_typ_tvars: type_sig * (indexname * typ) list -> typ -> typ (*type matching*) exception TYPE_MATCH - val typ_match: type_sig -> (indexname * typ) list * (typ * typ) - -> (indexname * typ) list + val typ_match: type_sig -> typ Vartab.table * (typ * typ) + -> typ Vartab.table val typ_instance: type_sig * typ * typ -> bool val of_sort: type_sig -> typ * sort -> bool (*type unification*) exception TUNIFY - val unify: type_sig -> int -> (indexname * typ) list -> (typ * typ) - -> (indexname * typ) list * int + val unify: type_sig -> int -> typ Vartab.table -> (typ * typ) + -> typ Vartab.table * int val raw_unify: typ * typ -> bool (*type inference*) @@ -691,8 +692,8 @@ fun typ_match tsig = let fun match (subs, (TVar (v, S), T)) = - (case assoc (subs, v) of - None => ((v, (check_has_sort (tsig, T, S); T)) :: subs + (case Vartab.lookup (subs, v) of + None => (Vartab.update_new ((v, (check_has_sort (tsig, T, S); T)), subs) handle TYPE _ => raise TYPE_MATCH) | Some U => if U = T then subs else raise TYPE_MATCH) | match (subs, (Type (a, Ts), Type (b, Us))) = @@ -704,7 +705,7 @@ in match end; fun typ_instance (tsig, T, U) = - (typ_match tsig ([], (U, T)); true) handle TYPE_MATCH => false; + (typ_match tsig (Vartab.empty, (U, T)); true) handle TYPE_MATCH => false; @@ -721,7 +722,7 @@ | occ (TFree _) = false | occ (TVar (w, _)) = eq_ix (v, w) orelse - (case assoc (tye, w) of + (case Vartab.lookup (tye, w) of None => false | Some U => occ U); in occ end; @@ -731,7 +732,7 @@ (*if devar returns a type var then it must be unassigned*) fun devar (T as TVar (v, _), tye) = - (case assoc (tye, v) of + (case Vartab.lookup (tye, v) of Some U => devar (U, tye) | None => T) | devar (T, tye) = T; @@ -740,11 +741,8 @@ (* add_env *) (*avoids chains 'a |-> 'b |-> 'c ...*) -fun add_env (p, []) = [p] - | add_env (vT as (v, T), (xU as (x, TVar (w, S))) :: ps) = - (if eq_ix (v, w) then (x, T) else xU) :: add_env (vT, ps) - | add_env (v, x :: xs) = x :: add_env (v, xs); - +fun add_env (vT as (v, T), tab) = Vartab.update_new (vT, Vartab.map + (fn (U as (TVar (w, S))) => if eq_ix (v, w) then T else U | U => U) tab); (* unify *) @@ -798,7 +796,7 @@ (*purely structural unification -- ignores sorts*) fun raw_unify (ty1, ty2) = - (unify tsig0 0 [] (rem_sorts ty1, rem_sorts ty2); true) + (unify tsig0 0 Vartab.empty (rem_sorts ty1, rem_sorts ty2); true) handle TUNIFY => false; diff -r 0255394a05da -r a217b0cd304d src/Pure/unify.ML --- a/src/Pure/unify.ML Fri Mar 10 01:16:19 2000 +0100 +++ b/src/Pure/unify.ML Fri Mar 10 14:57:06 2000 +0100 @@ -49,14 +49,14 @@ fun body_type(Envir.Envir{iTs,...}) = let fun bT(Type("fun",[_,T])) = bT T - | bT(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of + | bT(T as TVar(ixn,_)) = (case Vartab.lookup (iTs,ixn) of None => T | Some(T') => bT T') | bT T = T in bT end; fun binder_types(Envir.Envir{iTs,...}) = let fun bTs(Type("fun",[T,U])) = T :: bTs U - | bTs(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of + | bTs(T as TVar(ixn,_)) = (case Vartab.lookup (iTs,ixn) of None => [] | Some(T') => bTs T') | bTs _ = [] in bTs end; @@ -104,7 +104,7 @@ (case (fast (rbinder, f)) of Type("fun",[_,T]) => T | TVar(ixn,_) => - (case assoc(iTs,ixn) of + (case Vartab.lookup (iTs,ixn) of Some(Type("fun",[_,T])) => T | _ => raise TERM(funerr, [f$u])) | _ => raise TERM(funerr, [f$u])) @@ -123,7 +123,7 @@ let fun etif (Type("fun",[T,U]), t) = Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0)) | etif (TVar(ixn,_),t) = - (case assoc(iTs,ixn) of + (case Vartab.lookup (iTs,ixn) of None => t | Some(T) => etif(T,t)) | etif (_,t) = t; fun eta_nm (rbinder, Abs(a,T,body)) =