# HG changeset patch # User berghofe # Date 952696705 -3600 # Node ID d522ad1809e91b0c609fc7fd2eca0e9b352a25a2 # Parent a217b0cd304d6d37e764cbd572f141d30a16b06b Envir now uses Vartab instead of association lists. diff -r a217b0cd304d -r d522ad1809e9 src/Pure/envir.ML --- 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; diff -r a217b0cd304d -r d522ad1809e9 src/Pure/thm.ML --- 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