Type.unify and Type.typ_match now use Vartab instead of association lists.
authorberghofe
Fri Mar 10 14:57:06 2000 +0100 (2000-03-10)
changeset 8406a217b0cd304d
parent 8405 0255394a05da
child 8407 d522ad1809e9
Type.unify and Type.typ_match now use Vartab instead of association lists.
src/Pure/drule.ML
src/Pure/pattern.ML
src/Pure/type.ML
src/Pure/unify.ML
     1.1 --- a/src/Pure/drule.ML	Fri Mar 10 01:16:19 2000 +0100
     1.2 +++ b/src/Pure/drule.ML	Fri Mar 10 14:57:06 2000 +0100
     1.3 @@ -560,12 +560,12 @@
     1.4      in  (sign', tye', maxi')  end;
     1.5  in
     1.6  fun cterm_instantiate ctpairs0 th =
     1.7 -  let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th),[],0))
     1.8 +  let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th), Vartab.empty, 0))
     1.9        val tsig = #tsig(Sign.rep_sg sign);
    1.10 -      fun instT(ct,cu) = let val inst = subst_TVars tye
    1.11 +      fun instT(ct,cu) = let val inst = subst_TVars_Vartab tye
    1.12                           in (cterm_fun inst ct, cterm_fun inst cu) end
    1.13        fun ctyp2 (ix,T) = (ix, ctyp_of sign T)
    1.14 -  in  instantiate (map ctyp2 tye, map instT ctpairs0) th  end
    1.15 +  in  instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th  end
    1.16    handle TERM _ =>
    1.17             raise THM("cterm_instantiate: incompatible signatures",0,[th])
    1.18         | TYPE (msg, _, _) => raise THM(msg, 0, [th])
     2.1 --- a/src/Pure/pattern.ML	Fri Mar 10 01:16:19 2000 +0100
     2.2 +++ b/src/Pure/pattern.ML	Fri Mar 10 14:57:06 2000 +0100
     2.3 @@ -332,8 +332,8 @@
     2.4        | _ => raise MATCH
     2.5    in mtch end;
     2.6  
     2.7 -fun first_order_match tsig = fomatch tsig ([],[]);
     2.8 - 
     2.9 +fun first_order_match tsig = apfst Vartab.dest o fomatch tsig (Vartab.empty, []);
    2.10 +
    2.11  (* Matching of higher-order patterns *)
    2.12  
    2.13  fun match_bind(itms,binders,ixn,is,t) =
    2.14 @@ -355,7 +355,7 @@
    2.15        Abs(ns,Ts,ts) =>
    2.16          (case obj of
    2.17             Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (env,(ts,tt))
    2.18 -         | _ => let val Tt = typ_subst_TVars iTs Ts
    2.19 +         | _ => let val Tt = typ_subst_TVars_Vartab iTs Ts
    2.20                  in mtch((ns,Tt)::binders)(env,(ts,(incr obj)$Bound(0))) end)
    2.21      | _ => (case obj of
    2.22                Abs(nt,Tt,tt) =>
    2.23 @@ -392,11 +392,11 @@
    2.24  
    2.25    val pT = fastype_of pat
    2.26    and oT = fastype_of obj
    2.27 -  val iTs = typ_match tsg ([],(pT,oT))
    2.28 +  val iTs = typ_match tsg (Vartab.empty, (pT,oT))
    2.29    val insts2 = (iTs,[])
    2.30  
    2.31 -in mtch [] (insts2, po)
    2.32 -   handle Pattern => fomatch tsg insts2 po
    2.33 +in apfst Vartab.dest (mtch [] (insts2, po)
    2.34 +   handle Pattern => fomatch tsg insts2 po)
    2.35  end;
    2.36  
    2.37  (*Predicate: does the pattern match the object?*)
     3.1 --- a/src/Pure/type.ML	Fri Mar 10 01:16:19 2000 +0100
     3.2 +++ b/src/Pure/type.ML	Fri Mar 10 14:57:06 2000 +0100
     3.3 @@ -47,18 +47,19 @@
     3.4    val norm_typ: type_sig -> typ -> typ
     3.5    val norm_term: type_sig -> term -> term
     3.6    val inst_term_tvars: type_sig * (indexname * typ) list -> term -> term
     3.7 +  val inst_typ_tvars: type_sig * (indexname * typ) list -> typ -> typ
     3.8  
     3.9    (*type matching*)
    3.10    exception TYPE_MATCH
    3.11 -  val typ_match: type_sig -> (indexname * typ) list * (typ * typ)
    3.12 -    -> (indexname * typ) list
    3.13 +  val typ_match: type_sig -> typ Vartab.table * (typ * typ)
    3.14 +    -> typ Vartab.table
    3.15    val typ_instance: type_sig * typ * typ -> bool
    3.16    val of_sort: type_sig -> typ * sort -> bool
    3.17  
    3.18    (*type unification*)
    3.19    exception TUNIFY
    3.20 -  val unify: type_sig -> int -> (indexname * typ) list -> (typ * typ)
    3.21 -    -> (indexname * typ) list * int
    3.22 +  val unify: type_sig -> int -> typ Vartab.table -> (typ * typ)
    3.23 +    -> typ Vartab.table * int
    3.24    val raw_unify: typ * typ -> bool
    3.25  
    3.26    (*type inference*)
    3.27 @@ -691,8 +692,8 @@
    3.28  fun typ_match tsig =
    3.29    let
    3.30      fun match (subs, (TVar (v, S), T)) =
    3.31 -          (case assoc (subs, v) of
    3.32 -            None => ((v, (check_has_sort (tsig, T, S); T)) :: subs
    3.33 +          (case Vartab.lookup (subs, v) of
    3.34 +            None => (Vartab.update_new ((v, (check_has_sort (tsig, T, S); T)), subs)
    3.35                handle TYPE _ => raise TYPE_MATCH)
    3.36            | Some U => if U = T then subs else raise TYPE_MATCH)
    3.37        | match (subs, (Type (a, Ts), Type (b, Us))) =
    3.38 @@ -704,7 +705,7 @@
    3.39    in match end;
    3.40  
    3.41  fun typ_instance (tsig, T, U) =
    3.42 -  (typ_match tsig ([], (U, T)); true) handle TYPE_MATCH => false;
    3.43 +  (typ_match tsig (Vartab.empty, (U, T)); true) handle TYPE_MATCH => false;
    3.44  
    3.45  
    3.46  
    3.47 @@ -721,7 +722,7 @@
    3.48        | occ (TFree _) = false
    3.49        | occ (TVar (w, _)) =
    3.50            eq_ix (v, w) orelse
    3.51 -            (case assoc (tye, w) of
    3.52 +            (case Vartab.lookup (tye, w) of
    3.53                None => false
    3.54              | Some U => occ U);
    3.55    in occ end;
    3.56 @@ -731,7 +732,7 @@
    3.57  
    3.58  (*if devar returns a type var then it must be unassigned*)
    3.59  fun devar (T as TVar (v, _), tye) =
    3.60 -      (case  assoc (tye, v) of
    3.61 +      (case  Vartab.lookup (tye, v) of
    3.62          Some U => devar (U, tye)
    3.63        | None => T)
    3.64    | devar (T, tye) = T;
    3.65 @@ -740,11 +741,8 @@
    3.66  (* add_env *)
    3.67  
    3.68  (*avoids chains 'a |-> 'b |-> 'c ...*)
    3.69 -fun add_env (p, []) = [p]
    3.70 -  | add_env (vT as (v, T), (xU as (x, TVar (w, S))) :: ps) =
    3.71 -      (if eq_ix (v, w) then (x, T) else xU) :: add_env (vT, ps)
    3.72 -  | add_env (v, x :: xs) = x :: add_env (v, xs);
    3.73 -
    3.74 +fun add_env (vT as (v, T), tab) = Vartab.update_new (vT, Vartab.map
    3.75 +  (fn (U as (TVar (w, S))) => if eq_ix (v, w) then T else U | U => U) tab);
    3.76  
    3.77  (* unify *)
    3.78  
    3.79 @@ -798,7 +796,7 @@
    3.80  
    3.81  (*purely structural unification -- ignores sorts*)
    3.82  fun raw_unify (ty1, ty2) =
    3.83 -  (unify tsig0 0 [] (rem_sorts ty1, rem_sorts ty2); true)
    3.84 +  (unify tsig0 0 Vartab.empty (rem_sorts ty1, rem_sorts ty2); true)
    3.85      handle TUNIFY => false;
    3.86  
    3.87  
     4.1 --- a/src/Pure/unify.ML	Fri Mar 10 01:16:19 2000 +0100
     4.2 +++ b/src/Pure/unify.ML	Fri Mar 10 14:57:06 2000 +0100
     4.3 @@ -49,14 +49,14 @@
     4.4  
     4.5  fun body_type(Envir.Envir{iTs,...}) = 
     4.6  let fun bT(Type("fun",[_,T])) = bT T
     4.7 -      | bT(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of
     4.8 +      | bT(T as TVar(ixn,_)) = (case Vartab.lookup (iTs,ixn) of
     4.9  		None => T | Some(T') => bT T')
    4.10        | bT T = T
    4.11  in bT end;
    4.12  
    4.13  fun binder_types(Envir.Envir{iTs,...}) = 
    4.14  let fun bTs(Type("fun",[T,U])) = T :: bTs U
    4.15 -      | bTs(T as TVar(ixn,_)) = (case assoc(iTs,ixn) of
    4.16 +      | bTs(T as TVar(ixn,_)) = (case Vartab.lookup (iTs,ixn) of
    4.17  		None => [] | Some(T') => bTs T')
    4.18        | bTs _ = []
    4.19  in bTs end;
    4.20 @@ -104,7 +104,7 @@
    4.21  	(case (fast (rbinder, f)) of
    4.22  	   Type("fun",[_,T]) => T
    4.23  	 | TVar(ixn,_) =>
    4.24 -		(case assoc(iTs,ixn) of
    4.25 +		(case Vartab.lookup (iTs,ixn) of
    4.26  		   Some(Type("fun",[_,T])) => T
    4.27  		 | _ => raise TERM(funerr, [f$u]))
    4.28  	 | _ => raise TERM(funerr, [f$u]))
    4.29 @@ -123,7 +123,7 @@
    4.30    let fun etif (Type("fun",[T,U]), t) =
    4.31  	    Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
    4.32  	| etif (TVar(ixn,_),t) = 
    4.33 -	    (case assoc(iTs,ixn) of
    4.34 +	    (case Vartab.lookup (iTs,ixn) of
    4.35  		  None => t | Some(T) => etif(T,t))
    4.36  	| etif (_,t) = t;
    4.37        fun eta_nm (rbinder, Abs(a,T,body)) =