added Induct/Binary_Trees.thy, Induct/Tree_Forest (converted from
former ex/TF.ML ex/TF.thy ex/Term.ML ex/Term.thy);
(* Title: Pure/envir.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1988 University of Cambridge
Environments. They don't take account that typ is part of variable
name. Therefore we check elsewhere that two variables with same names
and different types cannot occur.
*)
signature ENVIR =
sig
datatype env = Envir of {asol: term Vartab.table, iTs: typ Vartab.table, maxidx: int}
exception SAME
val genvars: string -> env * typ list -> env * term list
val genvar: string -> env * typ -> env * term
val lookup: env * indexname -> term option
val update: (indexname * term) * env -> env
val empty: int -> env
val is_empty: env -> bool
val above: int * env -> bool
val vupdate: (indexname * term) * env -> env
val alist_of: env -> (indexname * term) list
val norm_term: env -> term -> term
val norm_term_same: env -> term -> term
val norm_type: env -> typ -> typ
val norm_type_same: env -> typ -> typ
val norm_types_same: env -> typ list -> typ list
val beta_norm: term -> term
end;
structure Envir : ENVIR =
struct
(*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 Vartab.table, (*table of assignments to Vars*)
iTs: typ Vartab.table} (*table of assignments to TVars*)
(*Generate a list of distinct variables.
Increments index to make them distinct from ALL present variables. *)
fun genvars name (Envir{maxidx, asol, iTs}, Ts) : env * term list =
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)
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])
in (env',v) end;
fun lookup (Envir{asol,...}, xname) : term option = Vartab.lookup (asol, xname);
fun update ((xname, t), Envir{maxidx, asol, 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=Vartab.empty, iTs=Vartab.empty};
(*Test for empty environment*)
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, ...}) =
(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
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)
| _ => update((a,t), env);
(*Convert environment to alist*)
fun alist_of (Envir{asol,...}) = Vartab.dest asol;
(*** 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. ***)
(*raised when norm has no effect on a term, to do sharing instead of copying*)
exception SAME;
fun norm_term1 same (asol,t) : term =
let fun norm (Var (w,T)) =
(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)
| norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body))
| norm (f $ t) =
((case norm f of
Abs(_,_,body) => normh(subst_bound (t, body))
| nf => nf $ (norm t handle SAME => t))
handle SAME => f $ norm t)
| norm _ = raise SAME
and normh t = norm t handle SAME => t
in (if same then norm else normh) t end
fun normT iTs (Type (a, Ts)) = Type (a, normTs iTs Ts)
| normT iTs (TFree _) = raise SAME
| normT iTs (TVar(v, _)) = (case Vartab.lookup (iTs, v) of
Some U => normTh iTs U
| None => raise SAME)
and normTh iTs T = ((normT iTs T) handle SAME => T)
and normTs iTs [] = raise SAME
| normTs iTs (T :: Ts) =
((normT iTs T :: (normTs iTs Ts handle SAME => Ts))
handle SAME => T :: normTs iTs Ts);
fun norm_term2 same (asol, iTs, t) : term =
let fun norm (Const (a, T)) = Const(a, normT iTs T)
| norm (Free (a, T)) = Free(a, normT iTs T)
| norm (Var (w, T)) =
(case Vartab.lookup (asol, w) of
Some u => normh u
| None => Var(w, normT iTs T))
| norm (Abs (a, T, body)) =
(Abs (a, normT iTs T, normh body) handle SAME => Abs (a, T, norm body))
| norm (Abs(_, _, body) $ t) = normh (subst_bound (t, body))
| norm (f $ t) =
((case norm f of
Abs(_, _, body) => normh (subst_bound (t, body))
| nf => nf $ normh t)
handle SAME => f $ norm t)
| norm _ = raise SAME
and normh t = (norm t) handle SAME => t
in (if same then norm else normh) t end;
fun gen_norm_term same (env as Envir{asol,iTs,...}) t : term =
if Vartab.is_empty iTs then norm_term1 same (asol, t)
else norm_term2 same (asol, iTs, t);
val norm_term = gen_norm_term false;
val norm_term_same = gen_norm_term true;
val beta_norm = norm_term (empty 0);
fun norm_type (Envir {iTs, ...}) = normTh iTs;
fun norm_type_same (Envir {iTs, ...}) =
if Vartab.is_empty iTs then raise SAME else normT iTs;
fun norm_types_same (Envir {iTs, ...}) =
if Vartab.is_empty iTs then raise SAME else normTs iTs;
end;