Type.unify and Type.typ_match now use Vartab instead of association lists.
--- 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])
--- 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?*)
--- 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;
--- 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)) =