# HG changeset patch # User wenzelm # Date 1247859180 -7200 # Node ID e2e6b0691264f56be1e0d93f92f891eabea2d5f3 # Parent 49d7d0bb90c60130f082eb5bcac2b94eaff5caa8 major cleanup, simplification, modernization; diff -r 49d7d0bb90c6 -r e2e6b0691264 src/Pure/envir.ML --- 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;