--- a/src/Pure/envir.ML Fri Jul 17 21:32:59 2009 +0200
+++ b/src/Pure/envir.ML Fri Jul 17 21:33:00 2009 +0200
@@ -1,27 +1,29 @@
(* Title: Pure/envir.ML
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
-Environments. The type of a term variable / sort of a type variable is
-part of its name. The lookup function must apply type substitutions,
+Free-form environments. The type of a term variable / sort of a type variable is
+part of its name. The lookup function must apply type substitutions,
since they may change the identity of a variable.
*)
signature ENVIR =
sig
type tenv = (typ * term) Vartab.table
- datatype env = Envir of {asol: tenv, iTs: Type.tyenv, maxidx: int}
+ datatype env = Envir of {maxidx: int, tenv: tenv, tyenv: Type.tyenv}
+ val maxidx_of: env -> int
+ val term_env: env -> tenv
val type_env: env -> Type.tyenv
+ val is_empty: env -> bool
+ val empty: int -> env
+ val merge: env * env -> env
val insert_sorts: env -> sort list -> sort list
val genvars: string -> env * typ list -> env * term list
val genvar: string -> env * typ -> env * term
val lookup: env * (indexname * typ) -> term option
val lookup': tenv * (indexname * typ) -> term option
val update: ((indexname * typ) * term) * env -> env
- val empty: int -> env
- val is_empty: env -> bool
val above: env -> int -> bool
val vupdate: ((indexname * typ) * term) * env -> env
- val alist_of: env -> (indexname * (typ * term)) list
val norm_type_same: Type.tyenv -> typ Same.operation
val norm_types_same: Type.tyenv -> typ list Same.operation
val norm_type: Type.tyenv -> typ -> typ
@@ -41,115 +43,133 @@
val expand_term_frees: ((string * typ) * term) list -> term -> term
end;
-structure Envir : ENVIR =
+structure Envir: ENVIR =
struct
-(*updating can destroy environment in 2 ways!!
- (1) variables out of range (2) circular assignments
+(** datatype env **)
+
+(*Updating can destroy environment in 2 ways!
+ (1) variables out of range
+ (2) circular assignments
*)
+
type tenv = (typ * term) Vartab.table;
datatype env = Envir of
- {maxidx: int, (*maximum index of vars*)
- asol: tenv, (*assignments to Vars*)
- iTs: Type.tyenv}; (*assignments to TVars*)
+ {maxidx: int, (*upper bound of maximum index of vars*)
+ tenv: tenv, (*assignments to Vars*)
+ tyenv: Type.tyenv}; (*assignments to TVars*)
+
+fun make_env (maxidx, tenv, tyenv) = Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv};
+fun map_env f (Envir {maxidx, tenv, tyenv}) = make_env (f (maxidx, tenv, tyenv));
+
+fun maxidx_of (Envir {maxidx, ...}) = maxidx;
+fun term_env (Envir {tenv, ...}) = tenv;
+fun type_env (Envir {tyenv, ...}) = tyenv;
+
+fun is_empty env =
+ Vartab.is_empty (term_env env) andalso
+ Vartab.is_empty (type_env env);
-fun type_env (Envir {iTs, ...}) = iTs;
+
+(* build env *)
+
+fun empty maxidx = make_env (maxidx, Vartab.empty, Vartab.empty);
-(*NB: type unification may invent new sorts*)
+fun merge
+ (Envir {maxidx = maxidx1, tenv = tenv1, tyenv = tyenv1},
+ Envir {maxidx = maxidx2, tenv = tenv2, tyenv = tyenv2}) =
+ make_env (Int.max (maxidx1, maxidx2),
+ Vartab.merge (op =) (tenv1, tenv2),
+ Vartab.merge (op =) (tyenv1, tyenv2));
+
+
+(*NB: type unification may invent new sorts*) (* FIXME tenv!? *)
val insert_sorts = Vartab.fold (fn (_, (_, T)) => Sorts.insert_typ T) o type_env;
(*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 =
+fun genvars name (Envir {maxidx, tenv, tyenv}, 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;
+ in (Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}, 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 var_clash ixn T T' = raise TYPE ("Variable " ^
- quote (Term.string_of_vname ixn) ^ " has two distinct types",
+fun var_clash xi T T' =
+ raise TYPE ("Variable " ^ quote (Term.string_of_vname xi) ^ " has two distinct types",
[T', T], []);
-fun gen_lookup f asol (xname, T) =
- (case Vartab.lookup asol xname of
+fun lookup_check check tenv (xi, T) =
+ (case Vartab.lookup tenv xi of
NONE => NONE
- | SOME (U, t) => if f (T, U) then SOME t else var_clash xname T U);
+ | SOME (U, t) => if check (T, U) then SOME t else var_clash xi T U);
(* When dealing with environments produced by matching instead *)
(* of unification, there is no need to chase assigned TVars. *)
(* In this case, we can simply ignore the type substitution *)
(* and use = instead of eq_type. *)
-fun lookup' (asol, p) = gen_lookup op = asol p;
+fun lookup' (tenv, p) = lookup_check (op =) tenv p;
-fun lookup2 (iTs, asol) p =
- if Vartab.is_empty iTs then lookup' (asol, p)
- else gen_lookup (Type.eq_type iTs) asol p;
-
-fun lookup (Envir {asol, iTs, ...}, p) = lookup2 (iTs, asol) p;
+fun lookup2 (tyenv, tenv) =
+ lookup_check (Type.eq_type tyenv) tenv;
-fun update (((xname, T), t), Envir {maxidx, asol, iTs}) =
- Envir {maxidx = maxidx, asol = Vartab.update_new (xname, (T, t)) asol, iTs = iTs};
+fun lookup (Envir {tenv, tyenv, ...}, p) = lookup2 (tyenv, tenv) p;
-(*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;
+fun update (((xi, T), t), Envir {maxidx, tenv, tyenv}) =
+ Envir {maxidx = maxidx, tenv = Vartab.update_new (xi, (T, t)) tenv, tyenv = tyenv};
(*Determine if the least index updated exceeds lim*)
-fun above (Envir {asol, iTs, ...}) lim =
- (case Vartab.min_key asol of SOME (_, i) => i > lim | NONE => true) andalso
- (case Vartab.min_key iTs of SOME (_, i) => i > lim | NONE => true);
+fun above (Envir {tenv, tyenv, ...}) lim =
+ (case Vartab.min_key tenv of SOME (_, i) => i > lim | NONE => true) andalso
+ (case Vartab.min_key tyenv of SOME (_, i) => i > lim | NONE => true);
(*Update, checking Var-Var assignments: try to suppress higher indexes*)
-fun vupdate ((aU as (a, U), t), env as Envir {iTs, ...}) = case t of
- Var (nT as (name', T)) =>
- if a = name' then env (*cycle!*)
- else if TermOrd.indexname_ord (a, name') = LESS then
- (case lookup (env, nT) of (*if already assigned, chase*)
- NONE => update ((nT, Var (a, T)), env)
- | SOME u => vupdate ((aU, u), env))
- else update ((aU, t), env)
- | _ => update ((aU, t), env);
+fun vupdate ((aU as (a, U), t), env as Envir {tyenv, ...}) =
+ (case t of
+ Var (nT as (name', T)) =>
+ if a = name' then env (*cycle!*)
+ else if TermOrd.indexname_ord (a, name') = LESS then
+ (case lookup (env, nT) of (*if already assigned, chase*)
+ NONE => update ((nT, Var (a, T)), env)
+ | SOME u => vupdate ((aU, u), env))
+ else update ((aU, t), env)
+ | _ => update ((aU, t), env));
-(*Convert environment to alist*)
-fun alist_of (Envir{asol,...}) = Vartab.dest asol;
+(** beta normalization wrt. environment **)
-(*** 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. ***)
+(*Chases variables in env. Does not exploit sharing of variable bindings
+ Does not check types, so could loop.*)
local
-fun norm_type0 iTs : typ Same.operation =
+fun norm_type0 tyenv : typ Same.operation =
let
fun norm (Type (a, Ts)) = Type (a, Same.map norm Ts)
| norm (TFree _) = raise Same.SAME
| norm (TVar v) =
- (case Type.lookup iTs v of
+ (case Type.lookup tyenv v of
SOME U => Same.commit norm U
| NONE => raise Same.SAME);
in norm end;
-fun norm_term1 asol : term Same.operation =
+fun norm_term1 tenv : term Same.operation =
let
fun norm (Var v) =
- (case lookup' (asol, v) of
+ (case lookup' (tenv, v) of
SOME u => Same.commit norm u
| NONE => raise Same.SAME)
- | norm (Abs (a, T, body)) = Abs (a, T, norm body)
+ | norm (Abs (a, T, body)) = Abs (a, T, norm body)
| norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body))
| norm (f $ t) =
((case norm f of
@@ -159,13 +179,13 @@
| norm _ = raise Same.SAME;
in norm end;
-fun norm_term2 asol iTs : term Same.operation =
+fun norm_term2 tenv tyenv : term Same.operation =
let
- val normT = norm_type0 iTs;
+ val normT = norm_type0 tyenv;
fun norm (Const (a, T)) = Const (a, normT T)
| norm (Free (a, T)) = Free (a, normT T)
| norm (Var (xi, T)) =
- (case lookup2 (iTs, asol) (xi, T) of
+ (case lookup2 (tyenv, tenv) (xi, T) of
SOME u => Same.commit norm u
| NONE => Var (xi, normT T))
| norm (Abs (a, T, body)) =
@@ -182,19 +202,19 @@
in
-fun norm_type_same iTs T =
- if Vartab.is_empty iTs then raise Same.SAME
- else norm_type0 iTs T;
+fun norm_type_same tyenv T =
+ if Vartab.is_empty tyenv then raise Same.SAME
+ else norm_type0 tyenv T;
-fun norm_types_same iTs Ts =
- if Vartab.is_empty iTs then raise Same.SAME
- else Same.map (norm_type0 iTs) Ts;
+fun norm_types_same tyenv Ts =
+ if Vartab.is_empty tyenv then raise Same.SAME
+ else Same.map (norm_type0 tyenv) Ts;
-fun norm_type iTs T = norm_type_same iTs T handle Same.SAME => T;
+fun norm_type tyenv T = norm_type_same tyenv T handle Same.SAME => T;
-fun norm_term_same (Envir {asol, iTs, ...}) =
- if Vartab.is_empty iTs then norm_term1 asol
- else norm_term2 asol iTs;
+fun norm_term_same (Envir {tenv, tyenv, ...}) =
+ if Vartab.is_empty tyenv then norm_term1 tenv
+ else norm_term2 tenv tyenv;
fun norm_term envir t = norm_term_same envir t handle Same.SAME => t;
fun beta_norm t = if Term.has_abs t then norm_term (empty 0) t else t;
@@ -256,64 +276,72 @@
(*finds type of term without checking that combinations are consistent
Ts holds types of bound variables*)
-fun fastype (Envir {iTs, ...}) =
-let val funerr = "fastype: expected function type";
+fun fastype (Envir {tyenv, ...}) =
+ let
+ val funerr = "fastype: expected function type";
fun fast Ts (f $ u) =
- (case fast Ts f of
- Type ("fun", [_, T]) => T
- | TVar ixnS =>
- (case Type.lookup iTs ixnS of
- SOME (Type ("fun", [_, T])) => T
- | _ => raise TERM (funerr, [f $ u]))
- | _ => raise TERM (funerr, [f $ u]))
+ (case fast Ts f of
+ Type ("fun", [_, T]) => T
+ | TVar v =>
+ (case Type.lookup tyenv v of
+ SOME (Type ("fun", [_, T])) => T
+ | _ => raise TERM (funerr, [f $ u]))
+ | _ => raise TERM (funerr, [f $ u]))
| fast Ts (Const (_, T)) = T
| fast Ts (Free (_, T)) = T
| fast Ts (Bound i) =
- (nth Ts i
- handle Subscript => raise TERM ("fastype: Bound", [Bound i]))
+ (nth Ts i handle Subscript => raise TERM ("fastype: Bound", [Bound i]))
| fast Ts (Var (_, T)) = T
- | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u
-in fast end;
+ | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u;
+ in fast end;
(*Substitute for type Vars in a type*)
-fun typ_subst_TVars iTs T = if Vartab.is_empty iTs then T else
- let fun subst(Type(a, Ts)) = Type(a, map subst Ts)
- | subst(T as TFree _) = T
- | subst(T as TVar ixnS) =
- (case Type.lookup iTs ixnS of NONE => T | SOME(U) => U)
- in subst T end;
+fun typ_subst_TVars tyenv T =
+ if Vartab.is_empty tyenv then T
+ else
+ let
+ fun subst (Type (a, Ts)) = Type (a, map subst Ts)
+ | subst (T as TFree _) = T
+ | subst (T as TVar v) = (case Type.lookup tyenv v of NONE => T | SOME U => U);
+ in subst T end;
(*Substitute for type Vars in a term*)
val subst_TVars = map_types o typ_subst_TVars;
(*Substitute for Vars in a term *)
-fun subst_Vars itms t = if Vartab.is_empty itms then t else
- let fun subst (v as Var ixnT) = the_default v (lookup' (itms, ixnT))
+fun subst_Vars tenv tm =
+ if Vartab.is_empty tenv then tm
+ else
+ let
+ fun subst (t as Var v) = the_default t (lookup' (tenv, v))
| subst (Abs (a, T, t)) = Abs (a, T, subst t)
- | subst (f $ t) = subst f $ subst t
- | subst t = t
- in subst t end;
+ | subst (t $ u) = subst t $ subst u
+ | subst t = t;
+ in subst tm end;
(*Substitute for type/term Vars in a term *)
-fun subst_vars (iTs, itms) =
- if Vartab.is_empty iTs then subst_Vars itms else
- let fun subst (Const (a, T)) = Const(a, typ_subst_TVars iTs T)
- | subst (Free (a, T)) = Free (a, typ_subst_TVars iTs T)
- | subst (Var (ixn, T)) = (case lookup' (itms, (ixn, T)) of
- NONE => Var (ixn, typ_subst_TVars iTs T)
- | SOME t => t)
- | subst (b as Bound _) = b
- | subst (Abs (a, T, t)) = Abs(a, typ_subst_TVars iTs T, subst t)
- | subst (f $ t) = subst f $ subst t
- in subst end;
+fun subst_vars (tyenv, tenv) =
+ if Vartab.is_empty tyenv then subst_Vars tenv
+ else
+ let
+ fun subst (Const (a, T)) = Const (a, typ_subst_TVars tyenv T)
+ | subst (Free (a, T)) = Free (a, typ_subst_TVars tyenv T)
+ | subst (Var (xi, T)) =
+ (case lookup' (tenv, (xi, T)) of
+ NONE => Var (xi, typ_subst_TVars tyenv T)
+ | SOME t => t)
+ | subst (t as Bound _) = t
+ | subst (Abs (a, T, t)) = Abs (a, typ_subst_TVars tyenv T, subst t)
+ | subst (t $ u) = subst t $ subst u;
+ in subst end;
(* expand defined atoms -- with local beta reduction *)
fun expand_atom T (U, u) =
subst_TVars (Type.raw_match (U, T) Vartab.empty) u
- handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
+ handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
fun expand_term get =
let
@@ -326,10 +354,9 @@
(case head of
Abs (x, T, t) => comb (Abs (x, T, expand t))
| _ =>
- (case get head of
- SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args')
- | NONE => comb head)
- | _ => comb head)
+ (case get head of
+ SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args')
+ | NONE => comb head))
end;
in expand end;