--- a/src/Pure/envir.ML Fri Mar 10 14:57:06 2000 +0100
+++ b/src/Pure/envir.ML Fri Mar 10 14:58:25 2000 +0100
@@ -12,11 +12,8 @@
signature ENVIR =
sig
- type 'a xolist
- exception ENVIR of string * indexname;
- datatype env = Envir of {asol: term xolist, iTs: typ xolist, maxidx: int}
+ datatype env = Envir of {asol: term Vartab.table, iTs: typ Vartab.table, maxidx: int}
val alist_of : env -> (indexname * term) list
- val alist_of_olist : 'a xolist -> (indexname * 'a) list
val empty : int->env
val is_empty : env -> bool
val above : int * env -> bool
@@ -24,8 +21,6 @@
val genvars : string -> env * typ list -> env * term list
val lookup : env * indexname -> term option
val norm_term : env -> term -> term
- val null_olist : 'a xolist
- val olist_of_alist : (indexname * 'a) list -> 'a xolist
val update : (indexname * term) * env -> env
val vupdate : (indexname * term) * env -> env
end;
@@ -33,71 +28,13 @@
structure Envir : ENVIR =
struct
-(*association lists with keys in ascending order, no repeated keys*)
-type 'a xolist = (indexname * 'a) list;
-
-
-exception ENVIR of string * indexname;
-
-(*look up key in ordered list*)
-fun xsearch ([], key) = None
- | xsearch (((keyi,xi)::pairs), key) =
- if xless(keyi,key) then xsearch (pairs, key)
- else if key=keyi then Some xi
- else None;
-
-(*insert pair in ordered list, reject if key already present*)
-fun xinsert_new (newpr as (key, x), al) =
- let fun insert [] = [newpr]
- | insert ((pair as (keyi,xi)) :: pairs) =
- if xless(keyi,key) then pair :: insert pairs
- else if key=keyi then
- raise ENVIR("xinsert_new: already present",key)
- else newpr::pair::pairs
- in (insert al) end;
-
-(*insert pair in ordered list, overwrite if key already present*)
-fun xinsert (newpr as (key, x), al) =
- let fun insert [] = [newpr]
- | insert ((pair as (keyi,xi)) :: pairs) =
- if xless(keyi,key) then pair :: insert pairs
- else if key=keyi then newpr::pairs
- else newpr::pair::pairs
- in (insert al) end;
-
-(*apply function to the contents part of each pair*)
-fun xmap f (pairs) =
- let fun xmp [] = []
- | xmp ((key,x)::pairs) = (key, f x) :: xmp pairs
- in (xmp pairs) end;
-
-(*allows redefinition of a key by "join"ing the contents parts*)
-fun xmerge_olists join (pairsa, pairsb) =
- let fun xmrg ([],pairsb) = pairsb
- | xmrg (pairsa,[]) = pairsa
- | xmrg ((keya,x)::pairsa, (keyb,y)::pairsb) =
- if xless(keya,keyb) then
- (keya,x) :: xmrg (pairsa, (keyb,y)::pairsb)
- else if xless(keyb,keya) then
- (keyb,y) :: xmrg ((keya,x)::pairsa, pairsb)
- else (*equal*) (keya, join(x,y)) :: xmrg (pairsa, pairsb)
- in (xmrg (pairsa,pairsb)) end;
-
-val null_olist = [];
-
-fun alist_of_olist (pairs) = pairs;
-
-fun olist_of_alist pairs = foldr xinsert (pairs, []);
-
-
-
(*updating can destroy environment in 2 ways!!
(1) variables out of range (2) circular assignments
*)
datatype env = Envir of
{maxidx: int, (*maximum index of vars*)
- asol: term xolist, (*table of assignments to Vars*)
- iTs: typ xolist} (*table of assignments to TVars*)
+ asol: term Vartab.table, (*table of assignments to Vars*)
+ iTs: typ Vartab.table} (*table of assignments to TVars*)
(*Generate a list of distinct variables.
@@ -115,24 +52,24 @@
let val (env',[v]) = genvars name (env,[T])
in (env',v) end;
-fun lookup (Envir{asol,...}, xname) : term option = xsearch (asol,xname);
+fun lookup (Envir{asol,...}, xname) : term option = Vartab.lookup (asol, xname);
fun update ((xname, t), Envir{maxidx, asol, iTs}) =
- Envir{maxidx=maxidx, asol=xinsert_new ((xname,t), asol), iTs=iTs};
+ Envir{maxidx=maxidx, asol=Vartab.update_new ((xname,t), asol), iTs=iTs};
(*The empty environment. New variables will start with the given index+1.*)
-fun empty m = Envir{maxidx=m, asol=null_olist, iTs=[]};
+fun empty m = Envir{maxidx=m, asol=Vartab.empty, iTs=Vartab.empty};
(*Test for empty environment*)
-fun is_empty (Envir {asol = [], iTs = [], ...}) = true
- | is_empty _ = false;
+fun is_empty (Envir {asol, iTs, ...}) = Vartab.is_empty asol andalso Vartab.is_empty iTs;
(*Determine if the least index updated exceeds lim*)
-fun above (lim, Envir {asol, iTs, ...}) =
- let fun upd [] = true
- | upd (i::is) = i>lim andalso upd is
- in upd (map (#2 o #1) asol @ (map (#2 o #1) iTs))
- end;
+fun above (lim, Envir {asol, iTs, ...}) =
+ (case (Vartab.min_key asol, Vartab.min_key iTs) of
+ (None, None) => true
+ | (Some (_, i), None) => i > lim
+ | (None, Some (_, i')) => i' > lim
+ | (Some (_, i), Some (_, i')) => i > lim andalso i' > lim);
(*Update, checking Var-Var assignments: try to suppress higher indexes*)
fun vupdate((a,t), env) = case t of
@@ -147,7 +84,7 @@
(*Convert environment to alist*)
-fun alist_of (Envir{maxidx,asol,...}) = alist_of_olist asol;
+fun alist_of (Envir{asol,...}) = Vartab.dest asol;
(*** Beta normal form for terms (not eta normal form).
@@ -159,7 +96,7 @@
fun norm_term1 (asol,t) : term =
let fun norm (Var (w,T)) =
- (case xsearch(asol,w) of
+ (case Vartab.lookup (asol, w) of
Some u => (norm u handle SAME => u)
| None => raise SAME)
| norm (Abs(a,T,body)) = Abs(a, T, norm body)
@@ -176,7 +113,7 @@
and norm_term2(asol,iTs,t) : term =
let fun normT(Type(a,Ts)) = Type(a, normTs Ts)
| normT(TFree _) = raise SAME
- | normT(TVar(v,_)) = (case assoc(iTs,v) of
+ | normT(TVar(v,_)) = (case Vartab.lookup (iTs, v) of
Some(U) => normTh U
| None => raise SAME)
and normTh T = ((normT T) handle SAME => T)
@@ -186,7 +123,7 @@
and norm(Const(a,T)) = Const(a, normT T)
| norm(Free(a,T)) = Free(a, normT T)
| norm(Var (w,T)) =
- (case xsearch(asol,w) of
+ (case Vartab.lookup (asol, w) of
Some u => normh u
| None => Var(w,normT T))
| norm(Abs(a,T,body)) =
@@ -203,7 +140,7 @@
(*curried version might be slower in recursive calls*)
fun norm_term (env as Envir{asol,iTs,...}) t : term =
- if null iTs then norm_term1(asol, t) else norm_term2(asol,iTs, t)
+ if Vartab.is_empty iTs then norm_term1(asol, t) else norm_term2(asol,iTs, t)
end;
--- a/src/Pure/thm.ML Fri Mar 10 14:57:06 2000 +0100
+++ b/src/Pure/thm.ML Fri Mar 10 14:58:25 2000 +0100
@@ -517,11 +517,11 @@
fun add_terms_sorts ([], Ss) = Ss
| add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss));
-fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs;
+fun env_codT (Envir.Envir {iTs, ...}) = map snd (Vartab.dest iTs);
-fun add_env_sorts (env, Ss) =
- add_terms_sorts (map snd (Envir.alist_of env),
- add_typs_sorts (env_codT env, Ss));
+fun add_env_sorts (Envir.Envir {iTs, asol, ...}, Ss) =
+ Vartab.foldl (add_term_sorts o swap o apsnd snd)
+ (Vartab.foldl (add_typ_sorts o swap o apsnd snd) (Ss, iTs), asol);
fun add_thm_sorts (Thm {hyps, prop, ...}, Ss) =
add_terms_sorts (hyps, add_term_sorts (prop, Ss));
@@ -1389,7 +1389,7 @@
fun norm_term_skip env 0 t = Envir.norm_term env t
| norm_term_skip env n (Const("all",_)$Abs(a,T,t)) =
let val Envir.Envir{iTs, ...} = env
- val T' = typ_subst_TVars iTs T
+ val T' = typ_subst_TVars_Vartab iTs T
(*Must instantiate types of parameters because they are flattened;
this could be a NEW parameter*)
in all T' $ Abs(a, T', norm_term_skip env n t) end