Envir now uses Vartab instead of association lists.
authorberghofe
Fri Mar 10 14:58:25 2000 +0100 (2000-03-10)
changeset 8407d522ad1809e9
parent 8406 a217b0cd304d
child 8408 4d981311dab7
Envir now uses Vartab instead of association lists.
src/Pure/envir.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/envir.ML	Fri Mar 10 14:57:06 2000 +0100
     1.2 +++ b/src/Pure/envir.ML	Fri Mar 10 14:58:25 2000 +0100
     1.3 @@ -12,11 +12,8 @@
     1.4  
     1.5  signature ENVIR =
     1.6  sig
     1.7 -  type 'a xolist
     1.8 -  exception ENVIR of string * indexname;
     1.9 -  datatype env = Envir of {asol: term xolist, iTs: typ xolist, maxidx: int}
    1.10 +  datatype env = Envir of {asol: term Vartab.table, iTs: typ Vartab.table, maxidx: int}
    1.11    val alist_of		: env -> (indexname * term) list
    1.12 -  val alist_of_olist	: 'a xolist -> (indexname * 'a) list
    1.13    val empty		: int->env
    1.14    val is_empty		: env -> bool
    1.15    val above		: int * env -> bool
    1.16 @@ -24,8 +21,6 @@
    1.17    val genvars		: string -> env * typ list -> env * term list
    1.18    val lookup		: env * indexname -> term option
    1.19    val norm_term		: env -> term -> term
    1.20 -  val null_olist	: 'a xolist
    1.21 -  val olist_of_alist	: (indexname * 'a) list -> 'a xolist
    1.22    val update		: (indexname * term) * env -> env
    1.23    val vupdate		: (indexname * term) * env -> env
    1.24  end;
    1.25 @@ -33,71 +28,13 @@
    1.26  structure Envir : ENVIR =
    1.27  struct
    1.28  
    1.29 -(*association lists with keys in ascending order, no repeated keys*)
    1.30 -type 'a xolist = (indexname * 'a) list;
    1.31 -
    1.32 -
    1.33 -exception ENVIR of string * indexname;
    1.34 -
    1.35 -(*look up key in ordered list*)
    1.36 -fun xsearch ([], key) = None
    1.37 -  | xsearch (((keyi,xi)::pairs), key) =
    1.38 -      if xless(keyi,key) then xsearch (pairs, key)
    1.39 -      else if key=keyi then Some xi
    1.40 -      else None;
    1.41 -
    1.42 -(*insert pair in ordered list, reject if key already present*)
    1.43 -fun xinsert_new (newpr as (key, x), al) =
    1.44 -  let fun insert [] = [newpr]
    1.45 -        | insert ((pair as (keyi,xi)) :: pairs) =
    1.46 -            if xless(keyi,key) then pair :: insert pairs
    1.47 -            else if key=keyi then
    1.48 -                raise ENVIR("xinsert_new: already present",key)
    1.49 -            else newpr::pair::pairs
    1.50 -  in  (insert al)  end;
    1.51 -
    1.52 -(*insert pair in ordered list, overwrite if key already present*)
    1.53 -fun xinsert (newpr as (key, x), al) =
    1.54 -  let fun insert [] = [newpr]
    1.55 -        | insert ((pair as (keyi,xi)) :: pairs) =
    1.56 -            if xless(keyi,key) then pair :: insert pairs
    1.57 -            else if key=keyi then newpr::pairs
    1.58 -            else newpr::pair::pairs
    1.59 -  in  (insert al)  end;
    1.60 -
    1.61 -(*apply function to the contents part of each pair*)
    1.62 -fun xmap f (pairs) =
    1.63 -  let fun xmp [] = []
    1.64 -        | xmp ((key,x)::pairs) = (key, f x) :: xmp pairs
    1.65 -  in (xmp pairs)  end;
    1.66 -
    1.67 -(*allows redefinition of a key by "join"ing the contents parts*)
    1.68 -fun xmerge_olists join (pairsa, pairsb) =
    1.69 -  let fun xmrg ([],pairsb) = pairsb
    1.70 -        | xmrg (pairsa,[]) = pairsa
    1.71 -        | xmrg ((keya,x)::pairsa, (keyb,y)::pairsb) =
    1.72 -            if xless(keya,keyb) then
    1.73 -                (keya,x) :: xmrg (pairsa, (keyb,y)::pairsb)
    1.74 -            else if xless(keyb,keya) then
    1.75 -                (keyb,y) :: xmrg ((keya,x)::pairsa, pairsb)
    1.76 -            else (*equal*)  (keya, join(x,y)) :: xmrg (pairsa, pairsb)
    1.77 -  in  (xmrg (pairsa,pairsb))  end;
    1.78 -
    1.79 -val null_olist = [];
    1.80 -
    1.81 -fun alist_of_olist (pairs) = pairs;
    1.82 -
    1.83 -fun olist_of_alist pairs = foldr xinsert (pairs, []);
    1.84 -
    1.85 -
    1.86 -
    1.87  (*updating can destroy environment in 2 ways!!
    1.88     (1) variables out of range   (2) circular assignments
    1.89  *)
    1.90  datatype env = Envir of
    1.91      {maxidx: int,               (*maximum index of vars*)
    1.92 -     asol: term xolist,         (*table of assignments to Vars*)
    1.93 -     iTs:  typ  xolist}         (*table of assignments to TVars*)
    1.94 +     asol: term Vartab.table,   (*table of assignments to Vars*)
    1.95 +     iTs: typ Vartab.table}     (*table of assignments to TVars*)
    1.96  
    1.97  
    1.98  (*Generate a list of distinct variables.
    1.99 @@ -115,24 +52,24 @@
   1.100    let val (env',[v]) = genvars name (env,[T])
   1.101    in  (env',v)  end;
   1.102  
   1.103 -fun lookup (Envir{asol,...}, xname) : term option = xsearch (asol,xname);
   1.104 +fun lookup (Envir{asol,...}, xname) : term option = Vartab.lookup (asol, xname);
   1.105  
   1.106  fun update ((xname, t), Envir{maxidx, asol, iTs}) =
   1.107 -  Envir{maxidx=maxidx, asol=xinsert_new ((xname,t), asol), iTs=iTs};
   1.108 +  Envir{maxidx=maxidx, asol=Vartab.update_new ((xname,t), asol), iTs=iTs};
   1.109  
   1.110  (*The empty environment.  New variables will start with the given index+1.*)
   1.111 -fun empty m = Envir{maxidx=m, asol=null_olist, iTs=[]};
   1.112 +fun empty m = Envir{maxidx=m, asol=Vartab.empty, iTs=Vartab.empty};
   1.113  
   1.114  (*Test for empty environment*)
   1.115 -fun is_empty (Envir {asol = [], iTs = [], ...}) = true
   1.116 -  | is_empty _ = false;
   1.117 +fun is_empty (Envir {asol, iTs, ...}) = Vartab.is_empty asol andalso Vartab.is_empty iTs;
   1.118  
   1.119  (*Determine if the least index updated exceeds lim*)
   1.120 -fun above (lim, Envir {asol, iTs, ...}) = 
   1.121 -    let fun upd [] = true
   1.122 -	  | upd (i::is) = i>lim andalso upd is
   1.123 -    in  upd (map (#2 o #1) asol @ (map (#2 o #1) iTs))
   1.124 -    end;
   1.125 +fun above (lim, Envir {asol, iTs, ...}) =
   1.126 +  (case (Vartab.min_key asol, Vartab.min_key iTs) of
   1.127 +     (None, None) => true
   1.128 +   | (Some (_, i), None) => i > lim
   1.129 +   | (None, Some (_, i')) => i' > lim
   1.130 +   | (Some (_, i), Some (_, i')) => i > lim andalso i' > lim);
   1.131  
   1.132  (*Update, checking Var-Var assignments: try to suppress higher indexes*)
   1.133  fun vupdate((a,t), env) = case t of
   1.134 @@ -147,7 +84,7 @@
   1.135  
   1.136  
   1.137  (*Convert environment to alist*)
   1.138 -fun alist_of (Envir{maxidx,asol,...}) = alist_of_olist asol;
   1.139 +fun alist_of (Envir{asol,...}) = Vartab.dest asol;
   1.140  
   1.141  
   1.142  (*** Beta normal form for terms (not eta normal form).
   1.143 @@ -159,7 +96,7 @@
   1.144  
   1.145  fun norm_term1 (asol,t) : term =
   1.146    let fun norm (Var (w,T)) =
   1.147 -	    (case xsearch(asol,w) of
   1.148 +	    (case Vartab.lookup (asol, w) of
   1.149  		Some u => (norm u handle SAME => u)
   1.150  	      | None   => raise SAME)
   1.151  	| norm (Abs(a,T,body)) =  Abs(a, T, norm body)
   1.152 @@ -176,7 +113,7 @@
   1.153  and norm_term2(asol,iTs,t) : term =
   1.154    let fun normT(Type(a,Ts)) = Type(a, normTs Ts)
   1.155  	| normT(TFree _) = raise SAME
   1.156 -	| normT(TVar(v,_)) = (case assoc(iTs,v) of
   1.157 +	| normT(TVar(v,_)) = (case Vartab.lookup (iTs, v) of
   1.158  		Some(U) => normTh U
   1.159  	      | None => raise SAME)
   1.160        and normTh T = ((normT T) handle SAME => T)
   1.161 @@ -186,7 +123,7 @@
   1.162        and norm(Const(a,T)) = Const(a, normT T)
   1.163  	| norm(Free(a,T)) = Free(a, normT T)
   1.164  	| norm(Var (w,T)) =
   1.165 -	    (case xsearch(asol,w) of
   1.166 +	    (case Vartab.lookup (asol, w) of
   1.167  		Some u => normh u
   1.168  	      | None   => Var(w,normT T))
   1.169  	| norm(Abs(a,T,body)) =
   1.170 @@ -203,7 +140,7 @@
   1.171  
   1.172  (*curried version might be slower in recursive calls*)
   1.173  fun norm_term (env as Envir{asol,iTs,...}) t : term =
   1.174 -        if null iTs then norm_term1(asol, t) else norm_term2(asol,iTs, t)
   1.175 +        if Vartab.is_empty iTs then norm_term1(asol, t) else norm_term2(asol,iTs, t)
   1.176  
   1.177  end;
   1.178  
     2.1 --- a/src/Pure/thm.ML	Fri Mar 10 14:57:06 2000 +0100
     2.2 +++ b/src/Pure/thm.ML	Fri Mar 10 14:58:25 2000 +0100
     2.3 @@ -517,11 +517,11 @@
     2.4  fun add_terms_sorts ([], Ss) = Ss
     2.5    | add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss));
     2.6  
     2.7 -fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs;
     2.8 +fun env_codT (Envir.Envir {iTs, ...}) = map snd (Vartab.dest iTs);
     2.9  
    2.10 -fun add_env_sorts (env, Ss) =
    2.11 -  add_terms_sorts (map snd (Envir.alist_of env),
    2.12 -    add_typs_sorts (env_codT env, Ss));
    2.13 +fun add_env_sorts (Envir.Envir {iTs, asol, ...}, Ss) =
    2.14 +  Vartab.foldl (add_term_sorts o swap o apsnd snd)
    2.15 +    (Vartab.foldl (add_typ_sorts o swap o apsnd snd) (Ss, iTs), asol);
    2.16  
    2.17  fun add_thm_sorts (Thm {hyps, prop, ...}, Ss) =
    2.18    add_terms_sorts (hyps, add_term_sorts (prop, Ss));
    2.19 @@ -1389,7 +1389,7 @@
    2.20  fun norm_term_skip env 0 t = Envir.norm_term env t
    2.21    | norm_term_skip env n (Const("all",_)$Abs(a,T,t)) =
    2.22          let val Envir.Envir{iTs, ...} = env
    2.23 -            val T' = typ_subst_TVars iTs T
    2.24 +            val T' = typ_subst_TVars_Vartab iTs T
    2.25              (*Must instantiate types of parameters because they are flattened;
    2.26                this could be a NEW parameter*)
    2.27          in  all T' $ Abs(a, T', norm_term_skip env n t)  end