--- a/src/Pure/envir.ML Thu Jan 20 13:35:40 1994 +0100
+++ b/src/Pure/envir.ML Mon Jan 24 12:03:53 1994 +0100
@@ -1,6 +1,6 @@
-(* Title: envir
+(* Title: Pure/envir.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1988 University of Cambridge
*)
@@ -11,16 +11,18 @@
*)
-signature ENVIR =
+signature ENVIR =
sig
type 'a xolist
exception ENVIR of string * indexname;
datatype env = Envir of {asol: term xolist,
- iTs: (indexname * typ) list,
- maxidx: int}
+ iTs: (indexname * typ) list,
+ 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 minidx : env -> int option
val genvar : string -> env * typ -> env * term
val genvars : string -> env * typ list -> env * term list
val lookup : env * indexname -> term option
@@ -31,7 +33,7 @@
val vupdate : (indexname * term) * env -> env
end;
-functor EnvirFun () : ENVIR =
+functor EnvirFun () : ENVIR =
struct
@@ -40,49 +42,49 @@
exception ENVIR of string * indexname;
-
-(*look up key in ordered list*)
+
+(*look up key in ordered list*)
fun xsearch (Olist[], key) = None
| xsearch (Olist ((keyi,xi)::pairs), key) =
if xless(keyi,key) then xsearch (Olist pairs, key)
- else if key=keyi then Some xi
+ 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), Olist 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
+ | 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 Olist (insert al) end;
(*insert pair in ordered list, overwrite if key already present*)
fun xinsert (newpr as (key, x), Olist 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
+ | 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 Olist (insert al) end;
-(*apply function to the contents part of each pair*)
+(*apply function to the contents part of each pair*)
fun xmap f (Olist pairs) =
let fun xmp [] = []
- | xmp ((key,x)::pairs) = (key, f x) :: xmp pairs
+ | xmp ((key,x)::pairs) = (key, f x) :: xmp pairs
in Olist (xmp pairs) end;
(*allows redefinition of a key by "join"ing the contents parts*)
fun xmerge_olists join (Olist pairsa, Olist 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)
+ | 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 Olist (xmrg (pairsa,pairsb)) end;
val null_olist = Olist[];
@@ -97,9 +99,9 @@
(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: (indexname*typ)list} (*table of assignments to TVars*)
+ {maxidx: int, (*maximum index of vars*)
+ asol: term xolist, (*table of assignments to Vars*)
+ iTs: (indexname*typ)list} (*table of assignments to TVars*)
(*Generate a list of distinct variables.
@@ -108,13 +110,13 @@
let fun genvs (_, [] : typ list) : term list = []
| genvs (n, [T]) = [ Var((name, maxidx+1), T) ]
| genvs (n, T::Ts) =
- Var((name ^ radixstring(26,"a",n), maxidx+1), T)
- :: genvs(n+1,Ts)
+ Var((name ^ radixstring(26,"a",n), maxidx+1), T)
+ :: genvs(n+1,Ts)
in (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts)) end;
(*Generate a variable.*)
fun genvar name (env,T) : env * term =
- let val (env',[v]) = genvars name (env,[T])
+ let val (env',[v]) = genvars name (env,[T])
in (env',v) end;
fun lookup (Envir{asol,...}, xname) : term option = xsearch (asol,xname);
@@ -125,15 +127,26 @@
(*The empty environment. New variables will start with the given index.*)
fun empty m = Envir{maxidx=m, asol=null_olist, iTs=[]};
+(*is_empty*)
+fun is_empty (Envir {asol = Olist [], iTs = [], ...}) = true
+ | is_empty _ = false;
+
+(*minidx*)
+fun minidx (Envir {asol = Olist asns, iTs, ...}) =
+ (case (asns, iTs) of
+ ([], []) => None
+ | (((_, i), _) :: _, _) => Some (min (i :: map (snd o fst) iTs))
+ | _ => Some (min (map (snd o fst) iTs)));
+
(*Update, checking Var-Var assignments: try to suppress higher indexes*)
fun vupdate((a,t), env) = case t of
Var(name',T) =>
- if a=name' then env (*cycle!*)
- else if xless(a, name') then
- (case lookup(env,name') of (*if already assigned, chase*)
- None => update((name', Var(a,T)), env)
- | Some u => vupdate((a,u), env))
- else update((a,t), env)
+ if a=name' then env (*cycle!*)
+ else if xless(a, name') then
+ (case lookup(env,name') of (*if already assigned, chase*)
+ None => update((name', Var(a,T)), env)
+ | Some u => vupdate((a,u), env))
+ else update((a,t), env)
| _ => update((a,t), env);
@@ -141,67 +154,66 @@
fun alist_of (Envir{maxidx,asol,...}) = alist_of_olist asol;
-(*Beta normal form for terms (not eta normal form).
+(*Beta normal form for terms (not eta normal form).
Chases variables in env; Does not exploit sharing of variable bindings
Does not check types, so could loop. *)
-local
- (*raised when norm has no effect on a term,
+local
+ (*raised when norm has no effect on a term,
to encourage sharing instead of copying*)
exception SAME;
fun norm_term1 (asol,t) : term =
- let fun norm (Var (w,T)) =
- (case xsearch(asol,w) of
- Some u => normh u
- | None => raise SAME)
- | norm (Abs(a,T,body)) = Abs(a, T, norm body)
- | norm (Abs(_,_,body) $ t) = normh(subst_bounds([t], body))
- | norm (f $ t) =
- ((case norm f of
- Abs(_,_,body) => normh(subst_bounds([t], body))
- | nf => nf $ normh t)
- handle SAME => f $ norm t)
- | norm _ = raise SAME
- and normh t = (norm t) handle SAME => t
+ let fun norm (Var (w,T)) =
+ (case xsearch(asol,w) of
+ Some u => normh u
+ | None => raise SAME)
+ | norm (Abs(a,T,body)) = Abs(a, T, norm body)
+ | norm (Abs(_,_,body) $ t) = normh(subst_bounds([t], body))
+ | norm (f $ t) =
+ ((case norm f of
+ Abs(_,_,body) => normh(subst_bounds([t], body))
+ | nf => nf $ normh t)
+ handle SAME => f $ norm t)
+ | norm _ = raise SAME
+ and normh t = (norm t) handle SAME => t
in normh t end
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
- Some(U) => normTh U
- | None => raise SAME)
- and normTh T = ((normT T) handle SAME => T)
- and normTs([]) = raise SAME
- | normTs(T::Ts) = ((normT T :: normTsh Ts)
- handle SAME => T :: normTs Ts)
- and normTsh Ts = ((normTs Ts) handle SAME => Ts)
- 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
- Some u => normh u
- | None => Var(w,normT T))
- | norm(Abs(a,T,body)) =
- (Abs(a,normT T,normh body) handle SAME => Abs(a, T, norm body))
- | norm(Abs(_,_,body) $ t) = normh(subst_bounds([t], body))
- | norm(f $ t) =
- ((case norm f of
- Abs(_,_,body) => normh(subst_bounds([t], body))
- | nf => nf $ normh t)
- handle SAME => f $ norm t)
- | norm _ = raise SAME
- and normh t = (norm t) handle SAME => t
+ | normT(TFree _) = raise SAME
+ | normT(TVar(v,_)) = (case assoc(iTs,v) of
+ Some(U) => normTh U
+ | None => raise SAME)
+ and normTh T = ((normT T) handle SAME => T)
+ and normTs([]) = raise SAME
+ | normTs(T::Ts) = ((normT T :: normTsh Ts)
+ handle SAME => T :: normTs Ts)
+ and normTsh Ts = ((normTs Ts) handle SAME => Ts)
+ 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
+ Some u => normh u
+ | None => Var(w,normT T))
+ | norm(Abs(a,T,body)) =
+ (Abs(a,normT T,normh body) handle SAME => Abs(a, T, norm body))
+ | norm(Abs(_,_,body) $ t) = normh(subst_bounds([t], body))
+ | norm(f $ t) =
+ ((case norm f of
+ Abs(_,_,body) => normh(subst_bounds([t], body))
+ | nf => nf $ normh t)
+ handle SAME => f $ norm t)
+ | norm _ = raise SAME
+ and normh t = (norm t) handle SAME => t
in normh t end;
in
(*curried version might be slower in recursive calls*)
fun norm_term (env as Envir{asol,iTs,...}) t : term =
- if iTs=[] then norm_term1(asol, t) else norm_term2(asol,iTs, t)
+ if iTs=[] then norm_term1(asol, t) else norm_term2(asol,iTs, t)
end;
end;
-