--- a/src/HOL/Library/reflection.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/HOL/Library/reflection.ML Fri Jul 17 23:13:50 2009 +0200
@@ -153,8 +153,8 @@
val certy = ctyp_of thy
val (tyenv, tmenv) =
Pattern.match thy
- ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
- (Envir.type_env (Envir.empty 0), Vartab.empty)
+ ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
+ (Vartab.empty, Vartab.empty)
val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv)
val (fts,its) =
(map (snd o snd) fnvs,
@@ -204,11 +204,9 @@
val xns_map = (fst (split_list nths)) ~~ xns
val subst = map (fn (nt, xn) => (nt, Var ((xn,0), fastype_of nt))) xns_map
val rhs_P = subst_free subst rhs
- val (tyenv, tmenv) = Pattern.match
- thy (rhs_P, t)
- (Envir.type_env (Envir.empty 0), Vartab.empty)
- val sbst = Envir.subst_vars (tyenv, tmenv)
- val sbsT = Envir.typ_subst_TVars tyenv
+ val (tyenv, tmenv) = Pattern.match thy (rhs_P, t) (Vartab.empty, Vartab.empty)
+ val sbst = Envir.subst_term (tyenv, tmenv)
+ val sbsT = Envir.subst_type tyenv
val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t))
(Vartab.dest tyenv)
val tml = Vartab.dest tmenv
--- a/src/HOL/Nominal/nominal_inductive.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Fri Jul 17 23:13:50 2009 +0200
@@ -342,7 +342,7 @@
val env = Pattern.first_order_match thy (ihypt, prop_of ihyp)
(Vartab.empty, Vartab.empty);
val ihyp' = Thm.instantiate ([], map (pairself (cterm_of thy))
- (map (Envir.subst_vars env) vs ~~
+ (map (Envir.subst_term env) vs ~~
map (fold_rev (NominalDatatype.mk_perm [])
(rev pis' @ pis)) params' @ [z])) ihyp;
fun mk_pi th =
--- a/src/HOL/Nominal/nominal_inductive2.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Jul 17 23:13:50 2009 +0200
@@ -147,7 +147,7 @@
let val env = Pattern.first_order_match thy (p, prop_of th)
(Vartab.empty, Vartab.empty)
in Thm.instantiate ([],
- map (Envir.subst_vars env #> cterm_of thy) vs ~~ cts) th
+ map (Envir.subst_term env #> cterm_of thy) vs ~~ cts) th
end;
fun prove_strong_ind s avoids ctxt =
--- a/src/HOL/Tools/Datatype/datatype_case.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Fri Jul 17 23:13:50 2009 +0200
@@ -293,7 +293,7 @@
end;
fun make_case tab ctxt = gen_make_case
- (match_type (ProofContext.theory_of ctxt)) Envir.subst_TVars fastype_of tab ctxt;
+ (match_type (ProofContext.theory_of ctxt)) Envir.subst_term_types fastype_of tab ctxt;
val make_case_untyped = gen_make_case (K (K Vartab.empty))
(K (Term.map_types (K dummyT))) (K dummyT);
--- a/src/HOL/Tools/Function/context_tree.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/HOL/Tools/Function/context_tree.ML Fri Jul 17 23:13:50 2009 +0200
@@ -116,8 +116,9 @@
val (c, subs) = (concl_of r, prems_of r)
val subst = Pattern.match (ProofContext.theory_of ctx) (c, tt') (Vartab.empty, Vartab.empty)
- val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_vars subst) subs
- val inst = map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_vars subst (Var v)))) (Term.add_vars c [])
+ val branches = map (mk_branch ctx o Envir.beta_norm o Envir.subst_term subst) subs
+ val inst = map (fn v =>
+ (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v)))) (Term.add_vars c [])
in
(cterm_instantiate inst r, dep, branches)
end
--- a/src/HOL/Tools/Function/fundef_datatype.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_datatype.ML Fri Jul 17 23:13:50 2009 +0200
@@ -102,7 +102,8 @@
fun inst_constrs_of thy (T as Type (name, _)) =
- map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
+ map (fn (Cn,CT) =>
+ Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
(the (Datatype.get_constrs thy name))
| inst_constrs_of thy _ = raise Match
--- a/src/HOL/Tools/Function/mutual.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/HOL/Tools/Function/mutual.ML Fri Jul 17 23:13:50 2009 +0200
@@ -100,7 +100,7 @@
val (caTss, resultTs) = split_list (map curried_types fs)
val argTs = map (foldr1 HOLogic.mk_prodT) caTss
- val dresultTs = distinct (Type.eq_type Vartab.empty) resultTs
+ val dresultTs = distinct (op =) resultTs
val n' = length dresultTs
val RST = BalancedTree.make (uncurry SumTree.mk_sumT) dresultTs
@@ -114,7 +114,7 @@
fun define (fvar as (n, T)) caTs resultT i =
let
val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *)
- val i' = find_index (fn Ta => Type.eq_type Vartab.empty (Ta, resultT)) dresultTs + 1
+ val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1
val f_exp = SumTree.mk_proj RST n' i' (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars))
val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp)
--- a/src/HOL/Tools/Function/pattern_split.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/HOL/Tools/Function/pattern_split.ML Fri Jul 17 23:13:50 2009 +0200
@@ -39,7 +39,8 @@
(* This is copied from "fundef_datatype.ML" *)
fun inst_constrs_of thy (T as Type (name, _)) =
- map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
+ map (fn (Cn,CT) =>
+ Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
(the (Datatype.get_constrs thy name))
| inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], [])
--- a/src/HOL/Tools/TFL/casesplit.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML Fri Jul 17 23:13:50 2009 +0200
@@ -129,8 +129,8 @@
| _ => error "not a valid case thm";
val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T))
(Vartab.dest type_insts);
- val cPv = ctermify (Envir.subst_TVars type_insts Pv);
- val cDv = ctermify (Envir.subst_TVars type_insts Dv);
+ val cPv = ctermify (Envir.subst_term_types type_insts Pv);
+ val cDv = ctermify (Envir.subst_term_types type_insts Dv);
in
(beta_eta_contract
(case_thm
--- a/src/HOL/Tools/TFL/thry.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/HOL/Tools/TFL/thry.ML Fri Jul 17 23:13:50 2009 +0200
@@ -35,7 +35,7 @@
fun match_term thry pat ob =
let
val (ty_theta, tm_theta) = Pattern.match thry (pat,ob) (Vartab.empty, Vartab.empty);
- fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t)
+ fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.subst_type ty_theta T), t)
in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta))
end;
--- a/src/HOL/Tools/inductive.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/HOL/Tools/inductive.ML Fri Jul 17 23:13:50 2009 +0200
@@ -922,7 +922,7 @@
val tab = fold (Pattern.first_order_match thy) (ts ~~ us)
(Vartab.empty, Vartab.empty);
in
- map (Envir.subst_vars tab) vars
+ map (Envir.subst_term tab) vars
end
in
map (mtch o apsnd prop_of) (cases ~~ intros)
--- a/src/HOL/Tools/inductive_set.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/HOL/Tools/inductive_set.ML Fri Jul 17 23:13:50 2009 +0200
@@ -324,7 +324,7 @@
fun to_pred_proc thy rules t = case lookup_rule thy I rules t of
NONE => NONE
| SOME (lhs, rhs) =>
- SOME (Envir.subst_vars
+ SOME (Envir.subst_term
(Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) rhs);
fun to_pred thms ctxt thm =
--- a/src/HOL/Tools/meson.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/HOL/Tools/meson.ML Fri Jul 17 23:13:50 2009 +0200
@@ -87,14 +87,12 @@
fun typ_pair_of (ix, (sort,ty)) = (TVar (ix,sort), ty);
fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
-val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
-
(*FIXME: currently does not "rename variables apart"*)
fun first_order_resolve thA thB =
let val thy = theory_of_thm thA
val tmA = concl_of thA
val Const("==>",_) $ tmB $ _ = prop_of thB
- val (tyenv,tenv) = Pattern.first_order_match thy (tmB,tmA) (tyenv0,tenv0)
+ val (tyenv, tenv) = Pattern.first_order_match thy (tmB, tmA) (Vartab.empty, Vartab.empty)
val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
in thA RS (cterm_instantiate ct_pairs thB) end
handle _ => raise THM ("first_order_resolve", 0, [thA,thB]); (* FIXME avoid handle _ *)
@@ -104,8 +102,8 @@
[] => th
| pairs =>
let val thy = theory_of_thm th
- val (tyenv,tenv) =
- List.foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs
+ val (tyenv, tenv) =
+ fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
val t_pairs = map term_pair_of (Vartab.dest tenv)
val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
in th' end
--- a/src/HOLCF/Tools/adm_tac.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/HOLCF/Tools/adm_tac.ML Fri Jul 17 23:13:50 2009 +0200
@@ -117,8 +117,8 @@
val tye' = Sign.typ_match thy (PT, #T (rep_cterm Pt)) tye;
val ctye = map (fn (ixn, (S, T)) =>
(ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)) (Vartab.dest tye');
- val tv = cterm_of thy (Var (("t", j), Envir.typ_subst_TVars tye' tT));
- val Pv = cterm_of thy (Var (("P", j), Envir.typ_subst_TVars tye' PT));
+ val tv = cterm_of thy (Var (("t", j), Envir.subst_type tye' tT));
+ val Pv = cterm_of thy (Var (("P", j), Envir.subst_type tye' PT));
val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule
in rule' end;
--- a/src/Pure/Isar/overloading.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/Pure/Isar/overloading.ML Fri Jul 17 23:13:50 2009 +0200
@@ -76,7 +76,7 @@
| _ => I)
| accumulate_improvements _ = I;
val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty;
- val ts' = (map o map_types) (Envir.typ_subst_TVars improvements) ts;
+ val ts' = (map o map_types) (Envir.subst_type improvements) ts;
fun apply_subst t = Envir.expand_term (fn Const (c, ty) => (case subst (c, ty)
of SOME (ty', t') =>
if Type.typ_instance tsig (ty, ty')
--- a/src/Pure/Isar/proof_context.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/Pure/Isar/proof_context.ML Fri Jul 17 23:13:50 2009 +0200
@@ -779,7 +779,7 @@
fun simult_matches ctxt (t, pats) =
(case Seq.pull (Unify.matchers (theory_of ctxt) (map (rpair t) pats)) of
NONE => error "Pattern match failed!"
- | SOME (env, _) => map (apsnd snd) (Envir.alist_of env));
+ | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []);
(* bind_terms *)
--- a/src/Pure/Proof/extraction.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/Pure/Proof/extraction.ML Fri Jul 17 23:13:50 2009 +0200
@@ -103,11 +103,10 @@
fun ren t = the_default t (Term.rename_abs tm1 tm t);
val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1);
val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty);
- val prems' = map (pairself (Envir.subst_vars env o inc o ren)) prems;
+ val prems' = map (pairself (Envir.subst_term env o inc o ren)) prems;
val env' = Envir.Envir
- {maxidx = Library.foldl Int.max
- (~1, map (Int.max o pairself maxidx_of_term) prems'),
- iTs = Tenv, asol = tenv};
+ {maxidx = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) prems' ~1,
+ tenv = tenv, tyenv = Tenv};
val env'' = fold (Pattern.unify thy o pairself (lookup rew)) prems' env';
in SOME (Envir.norm_term env'' (inc (ren tm2)))
end handle Pattern.MATCH => NONE | Pattern.Unif => NONE)
--- a/src/Pure/Proof/reconstruct.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/Pure/Proof/reconstruct.ML Fri Jul 17 23:13:50 2009 +0200
@@ -35,12 +35,6 @@
fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_prf
(vars_of prop @ frees_of prop) prf;
-fun merge_envs (Envir.Envir {asol=asol1, iTs=iTs1, maxidx=maxidx1})
- (Envir.Envir {asol=asol2, iTs=iTs2, maxidx=maxidx2}) =
- Envir.Envir {asol=Vartab.merge (op =) (asol1, asol2),
- iTs=Vartab.merge (op =) (iTs1, iTs2),
- maxidx=Int.max (maxidx1, maxidx2)};
-
(**** generate constraints for proof term ****)
@@ -48,31 +42,32 @@
let val (env', v) = Envir.genvar "a" (env, rev Ts ---> T)
in (env', list_comb (v, map Bound (length Ts - 1 downto 0))) end;
-fun mk_tvar (Envir.Envir {iTs, asol, maxidx}, s) =
- (Envir.Envir {iTs = iTs, asol = asol, maxidx = maxidx+1},
- TVar (("'t", maxidx+1), s));
+fun mk_tvar (Envir.Envir {maxidx, tenv, tyenv}, s) =
+ (Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv},
+ TVar (("'t", maxidx + 1), s));
val mk_abs = fold (fn T => fn u => Abs ("", T, u));
fun unifyT thy env T U =
let
- val Envir.Envir {asol, iTs, maxidx} = env;
- val (iTs', maxidx') = Sign.typ_unify thy (T, U) (iTs, maxidx)
- in Envir.Envir {asol=asol, iTs=iTs', maxidx=maxidx'} end
- handle Type.TUNIFY => error ("Non-unifiable types:\n" ^
- Syntax.string_of_typ_global thy T ^ "\n\n" ^ Syntax.string_of_typ_global thy U);
+ val Envir.Envir {maxidx, tenv, tyenv} = env;
+ val (tyenv', maxidx') = Sign.typ_unify thy (T, U) (tyenv, maxidx);
+ in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end;
-fun chaseT (env as Envir.Envir {iTs, ...}) (T as TVar ixnS) =
- (case Type.lookup iTs ixnS of NONE => T | SOME T' => chaseT env T')
+fun chaseT env (T as TVar v) =
+ (case Type.lookup (Envir.type_env env) v of
+ NONE => T
+ | SOME T' => chaseT env T')
| chaseT _ T = T;
-fun infer_type thy (env as Envir.Envir {maxidx, asol, iTs}) Ts vTs
- (t as Const (s, T)) = if T = dummyT then (case Sign.const_type thy s of
+fun infer_type thy (env as Envir.Envir {maxidx, tenv, tyenv}) Ts vTs
+ (t as Const (s, T)) = if T = dummyT then
+ (case Sign.const_type thy s of
NONE => error ("reconstruct_proof: No such constant: " ^ quote s)
| SOME T =>
let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T)
in (Const (s, T'), T', vTs,
- Envir.Envir {maxidx = maxidx + 1, asol = asol, iTs = iTs})
+ Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv})
end)
else (t, T, vTs, env)
| infer_type thy env Ts vTs (t as Free (s, T)) =
@@ -236,21 +231,23 @@
fun upd_constrs env cs =
let
- val Envir.Envir {asol, iTs, ...} = env;
+ val tenv = Envir.term_env env;
+ val tyenv = Envir.type_env env;
val dom = []
- |> Vartab.fold (cons o #1) asol
- |> Vartab.fold (cons o #1) iTs;
+ |> Vartab.fold (cons o #1) tenv
+ |> Vartab.fold (cons o #1) tyenv;
val vran = []
- |> Vartab.fold (Term.add_var_names o #2 o #2) asol
- |> Vartab.fold (Term.add_tvar_namesT o #2 o #2) iTs;
+ |> Vartab.fold (Term.add_var_names o #2 o #2) tenv
+ |> Vartab.fold (Term.add_tvar_namesT o #2 o #2) tyenv;
fun check_cs [] = []
- | check_cs ((u, p, vs)::ps) =
- let val vs' = subtract (op =) dom vs;
- in if vs = vs' then (u, p, vs)::check_cs ps
- else (true, p, fold (insert (op =)) vs' vran)::check_cs ps
- end
+ | check_cs ((u, p, vs) :: ps) =
+ let val vs' = subtract (op =) dom vs in
+ if vs = vs' then (u, p, vs) :: check_cs ps
+ else (true, p, fold (insert op =) vs' vran) :: check_cs ps
+ end;
in check_cs cs end;
+
(**** solution of constraints ****)
fun solve _ [] bigenv = bigenv
@@ -280,7 +277,7 @@
val Envir.Envir {maxidx, ...} = bigenv;
val (env, cs') = search (Envir.empty maxidx) cs;
in
- solve thy (upd_constrs env cs') (merge_envs bigenv env)
+ solve thy (upd_constrs env cs') (Envir.merge (bigenv, env))
end;
--- a/src/Pure/defs.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/Pure/defs.ML Fri Jul 17 23:13:50 2009 +0200
@@ -46,7 +46,7 @@
handle Type.TUNIFY => true);
fun match_args (Ts, Us) =
- Option.map Envir.typ_subst_TVars
+ Option.map Envir.subst_type
(SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE);
--- a/src/Pure/envir.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/Pure/envir.ML Fri Jul 17 23:13:50 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
@@ -32,124 +34,144 @@
val eta_contract: term -> term
val beta_eta_contract: term -> term
val fastype: env -> typ list -> term -> typ
- val typ_subst_TVars: Type.tyenv -> typ -> typ
- val subst_TVars: Type.tyenv -> term -> term
- val subst_Vars: tenv -> term -> term
- val subst_vars: Type.tyenv * tenv -> term -> term
+ val subst_type_same: Type.tyenv -> typ Same.operation
+ val subst_term_types_same: Type.tyenv -> term Same.operation
+ val subst_term_same: Type.tyenv * tenv -> term Same.operation
+ val subst_type: Type.tyenv -> typ -> typ
+ val subst_term_types: Type.tyenv -> term -> term
+ val subst_term: Type.tyenv * tenv -> term -> term
val expand_atom: typ -> typ * term -> term
val expand_term: (term -> (typ * term) option) -> term -> term
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 +181,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 +204,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 +278,89 @@
(*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;
+(** plain substitution -- without variable chasing **)
+
+local
-(*Substitute for type Vars in a term*)
-val subst_TVars = map_types o typ_subst_TVars;
+fun subst_type0 tyenv = Term_Subst.map_atypsT_same
+ (fn TVar v =>
+ (case Type.lookup tyenv v of
+ SOME U => U
+ | NONE => raise Same.SAME)
+ | _ => raise Same.SAME);
-(*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))
- | subst (Abs (a, T, t)) = Abs (a, T, subst t)
- | subst (f $ t) = subst f $ subst t
- | subst t = t
- in subst t end;
+fun subst_term1 tenv = Term_Subst.map_aterms_same
+ (fn Var v =>
+ (case lookup' (tenv, v) of
+ SOME u => u
+ | NONE => raise Same.SAME)
+ | _ => raise Same.SAME);
-(*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
+fun subst_term2 tenv tyenv : term Same.operation =
+ let
+ val substT = subst_type0 tyenv;
+ fun subst (Const (a, T)) = Const (a, substT T)
+ | subst (Free (a, T)) = Free (a, substT T)
+ | subst (Var (xi, T)) =
+ (case lookup' (tenv, (xi, T)) of
+ SOME u => u
+ | NONE => Var (xi, substT T))
+ | subst (Bound _) = raise Same.SAME
+ | subst (Abs (a, T, t)) =
+ (Abs (a, substT T, Same.commit subst t)
+ handle Same.SAME => Abs (a, T, subst t))
+ | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
in subst end;
+in
-(* expand defined atoms -- with local beta reduction *)
+fun subst_type_same tyenv T =
+ if Vartab.is_empty tyenv then raise Same.SAME
+ else subst_type0 tyenv T;
+
+fun subst_term_types_same tyenv t =
+ if Vartab.is_empty tyenv then raise Same.SAME
+ else Term_Subst.map_types_same (subst_type0 tyenv) t;
+
+fun subst_term_same (tyenv, tenv) =
+ if Vartab.is_empty tenv then subst_term_types_same tyenv
+ else if Vartab.is_empty tyenv then subst_term1 tenv
+ else subst_term2 tenv tyenv;
+
+fun subst_type tyenv T = subst_type_same tyenv T handle Same.SAME => T;
+fun subst_term_types tyenv t = subst_term_types_same tyenv t handle Same.SAME => t;
+fun subst_term envs t = subst_term_same envs t handle Same.SAME => t;
+
+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]);
+ subst_term_types (Type.raw_match (U, T) Vartab.empty) u
+ handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]);
fun expand_term get =
let
@@ -326,10 +373,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;
--- a/src/Pure/pattern.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/Pure/pattern.ML Fri Jul 17 23:13:50 2009 +0200
@@ -141,8 +141,10 @@
| split_type (Type ("fun",[T1,T2]),n,Ts) = split_type (T2,n-1,T1::Ts)
| split_type _ = error("split_type");
-fun type_of_G (env as Envir.Envir {iTs, ...}) (T,n,is) =
- let val (Ts, U) = split_type (Envir.norm_type iTs T, n, [])
+fun type_of_G env (T, n, is) =
+ let
+ val tyenv = Envir.type_env env;
+ val (Ts, U) = split_type (Envir.norm_type tyenv T, n, []);
in map (nth Ts) is ---> U end;
fun mkhnf (binders,is,G,js) = mkabs (binders, is, app(G,js));
@@ -225,11 +227,12 @@
end;
in if TermOrd.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
-fun unify_types thy (T,U) (env as Envir.Envir{asol,iTs,maxidx}) =
- if T=U then env
- else let val (iTs',maxidx') = Sign.typ_unify thy (U, T) (iTs, maxidx)
- in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
- handle Type.TUNIFY => (typ_clash thy (iTs,T,U); raise Unif);
+fun unify_types thy (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) =
+ if T = U then env
+ else
+ let val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx)
+ in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end
+ handle Type.TUNIFY => (typ_clash thy (tyenv, T, U); raise Unif);
fun unif thy binders (s,t) env = case (Envir.head_norm env s, Envir.head_norm env t) of
(Abs(ns,Ts,ts),Abs(nt,Tt,tt)) =>
@@ -351,7 +354,7 @@
Abs(ns,Ts,ts) =>
(case obj of
Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (ts,tt) env
- | _ => let val Tt = Envir.typ_subst_TVars iTs Ts
+ | _ => let val Tt = Envir.subst_type iTs Ts
in mtch((ns,Tt)::binders) (ts,(incr obj)$Bound(0)) env end)
| _ => (case obj of
Abs(nt,Tt,tt) =>
@@ -425,7 +428,7 @@
fun match_rew thy tm (tm1, tm2) =
let val rtm = the_default tm2 (Term.rename_abs tm1 tm tm2) in
- SOME (Envir.subst_vars (match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm)
+ SOME (Envir.subst_term (match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm)
handle MATCH => NONE
end;
--- a/src/Pure/proofterm.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/Pure/proofterm.ML Fri Jul 17 23:13:50 2009 +0200
@@ -489,9 +489,8 @@
| remove_types (Const (s, _)) = Const (s, dummyT)
| remove_types t = t;
-fun remove_types_env (Envir.Envir {iTs, asol, maxidx}) =
- Envir.Envir {iTs = iTs, asol = Vartab.map (apsnd remove_types) asol,
- maxidx = maxidx};
+fun remove_types_env (Envir.Envir {maxidx, tenv, tyenv}) =
+ Envir.Envir {maxidx = maxidx, tenv = Vartab.map (apsnd remove_types) tenv, tyenv = tyenv};
fun norm_proof' env prf = norm_proof (remove_types_env env) prf;
@@ -1088,7 +1087,7 @@
fun prf_subst (pinst, (tyinsts, insts)) =
let
- val substT = Envir.typ_subst_TVars tyinsts;
+ val substT = Envir.subst_type tyinsts;
fun subst' lev (t as Var (ixn, _)) = (case AList.lookup (op =) insts ixn of
NONE => t
--- a/src/Pure/thm.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/Pure/thm.ML Fri Jul 17 23:13:50 2009 +0200
@@ -317,7 +317,7 @@
(Ctyp {T = TVar ((a, i), S), thy_ref = Theory.check_thy thy, maxidx = i, sorts = sorts},
Ctyp {T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts});
fun mk_ctinst ((x, i), (T, t)) =
- let val T = Envir.typ_subst_TVars Tinsts T in
+ let val T = Envir.subst_type Tinsts T in
(Cterm {t = Var ((x, i), T), T = T, thy_ref = Theory.check_thy thy,
maxidx = i, sorts = sorts},
Cterm {t = t, T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts})
@@ -1247,12 +1247,12 @@
val Thm (der, {thy_ref, maxidx, shyps, hyps, prop, ...}) = state;
val thy = Theory.deref thy_ref;
val (tpairs, Bs, Bi, C) = dest_state (state, i);
- fun newth n (env as Envir.Envir {maxidx, ...}, tpairs) =
+ fun newth n (env, tpairs) =
Thm (deriv_rule1
((if Envir.is_empty env then I else (Pt.norm_proof' env)) o
Pt.assumption_proof Bs Bi n) der,
{tags = [],
- maxidx = maxidx,
+ maxidx = Envir.maxidx_of env,
shyps = Envir.insert_sorts env shyps,
hyps = hyps,
tpairs =
@@ -1465,15 +1465,15 @@
(*Faster normalization: skip assumptions that were lifted over*)
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' = Envir.typ_subst_TVars iTs T
- (*Must instantiate types of parameters because they are flattened;
- this could be a NEW parameter*)
- in Term.all T' $ Abs(a, T', norm_term_skip env n t) end
- | norm_term_skip env n (Const("==>", _) $ A $ B) =
- Logic.mk_implies (A, norm_term_skip env (n-1) B)
- | norm_term_skip env n t = error"norm_term_skip: too few assumptions??";
+ | norm_term_skip env n (Const ("all", _) $ Abs (a, T, t)) =
+ let
+ val T' = Envir.subst_type (Envir.type_env env) T
+ (*Must instantiate types of parameters because they are flattened;
+ this could be a NEW parameter*)
+ in Term.all T' $ Abs (a, T', norm_term_skip env n t) end
+ | norm_term_skip env n (Const ("==>", _) $ A $ B) =
+ Logic.mk_implies (A, norm_term_skip env (n - 1) B)
+ | norm_term_skip env n t = error "norm_term_skip: too few assumptions??";
(*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C)
@@ -1495,7 +1495,7 @@
and nlift = Logic.count_prems (strip_all_body Bi) + (if eres_flg then ~1 else 0)
val thy = Theory.deref (merge_thys2 state orule);
(** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)
- fun addth A (As, oldAs, rder', n) ((env as Envir.Envir {maxidx, ...}, tpairs), thq) =
+ fun addth A (As, oldAs, rder', n) ((env, tpairs), thq) =
let val normt = Envir.norm_term env;
(*perform minimal copying here by examining env*)
val (ntpairs, normp) =
@@ -1520,7 +1520,7 @@
curry op oo (Pt.norm_proof' env))
(Pt.bicompose_proof flatten Bs oldAs As A n (nlift+1))) rder' sder,
{tags = [],
- maxidx = maxidx,
+ maxidx = Envir.maxidx_of env,
shyps = Envir.insert_sorts env (Sorts.union rshyps sshyps),
hyps = union_hyps rhyps shyps,
tpairs = ntpairs,
--- a/src/Pure/type.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/Pure/type.ML Fri Jul 17 23:13:50 2009 +0200
@@ -494,12 +494,15 @@
(*equality with respect to a type environment*)
-fun eq_type tye (T, T') =
+fun equal_type tye (T, T') =
(case (devar tye T, devar tye T') of
(Type (s, Ts), Type (s', Ts')) =>
- s = s' andalso ListPair.all (eq_type tye) (Ts, Ts')
+ s = s' andalso ListPair.all (equal_type tye) (Ts, Ts')
| (U, U') => U = U');
+fun eq_type tye =
+ if Vartab.is_empty tye then op = else equal_type tye;
+
(** extend and merge type signatures **)
--- a/src/Pure/type_infer.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/Pure/type_infer.ML Fri Jul 17 23:13:50 2009 +0200
@@ -402,7 +402,7 @@
(*convert to preterms*)
val ts = burrow_types check_typs raw_ts;
- val (ts', (vps, ps)) =
+ val (ts', _) =
fold_map (preterm_of const_type is_param o constrain_vars) ts (Vartab.empty, Vartab.empty);
(*do type inference*)
--- a/src/Pure/unify.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/Pure/unify.ML Fri Jul 17 23:13:50 2009 +0200
@@ -52,36 +52,48 @@
type dpair = binderlist * term * term;
-fun body_type(Envir.Envir{iTs,...}) =
-let fun bT(Type("fun",[_,T])) = bT T
- | bT(T as TVar ixnS) = (case Type.lookup iTs ixnS of
- NONE => T | SOME(T') => bT T')
- | bT T = T
-in bT end;
+fun body_type env =
+ let
+ val tyenv = Envir.type_env env;
+ fun bT (Type ("fun", [_, T])) = bT T
+ | bT (T as TVar v) =
+ (case Type.lookup tyenv v of
+ NONE => T
+ | SOME T' => bT T')
+ | bT T = T;
+ in bT end;
-fun binder_types(Envir.Envir{iTs,...}) =
-let fun bTs(Type("fun",[T,U])) = T :: bTs U
- | bTs(T as TVar ixnS) = (case Type.lookup iTs ixnS of
- NONE => [] | SOME(T') => bTs T')
- | bTs _ = []
-in bTs end;
+fun binder_types env =
+ let
+ val tyenv = Envir.type_env env;
+ fun bTs (Type ("fun", [T, U])) = T :: bTs U
+ | bTs (T as TVar v) =
+ (case Type.lookup tyenv v of
+ NONE => []
+ | SOME T' => bTs T')
+ | bTs _ = [];
+ in bTs end;
fun strip_type env T = (binder_types env T, body_type env T);
fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t;
-(*Eta normal form*)
-fun eta_norm(env as Envir.Envir{iTs,...}) =
- let fun etif (Type("fun",[T,U]), t) =
- Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
- | etif (TVar ixnS, t) =
- (case Type.lookup iTs ixnS of
- NONE => t | SOME(T) => etif(T,t))
- | etif (_,t) = t;
- fun eta_nm (rbinder, Abs(a,T,body)) =
- Abs(a, T, eta_nm ((a,T)::rbinder, body))
- | eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t)
+(* eta normal form *)
+
+fun eta_norm env =
+ let
+ val tyenv = Envir.type_env env;
+ fun etif (Type ("fun", [T, U]), t) =
+ Abs ("", T, etif (U, incr_boundvars 1 t $ Bound 0))
+ | etif (TVar v, t) =
+ (case Type.lookup tyenv v of
+ NONE => t
+ | SOME T => etif (T, t))
+ | etif (_, t) = t;
+ fun eta_nm (rbinder, Abs (a, T, body)) =
+ Abs (a, T, eta_nm ((a, T) :: rbinder, body))
+ | eta_nm (rbinder, t) = etif (fastype env (rbinder, t), t);
in eta_nm end;
@@ -186,11 +198,14 @@
exception ASSIGN; (*Raised if not an assignment*)
-fun unify_types thy (T,U, env as Envir.Envir{asol,iTs,maxidx}) =
- if T=U then env
- else let val (iTs',maxidx') = Sign.typ_unify thy (U, T) (iTs, maxidx)
- in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
- handle Type.TUNIFY => raise CANTUNIFY;
+fun unify_types thy (T, U, env) =
+ if T = U then env
+ else
+ let
+ val Envir.Envir {maxidx, tenv, tyenv} = env;
+ val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx);
+ in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end
+ handle Type.TUNIFY => raise CANTUNIFY;
fun test_unify_types thy (args as (T,U,_)) =
let val str_of = Syntax.string_of_typ_global thy;
@@ -636,9 +651,9 @@
(*Pattern matching*)
-fun first_order_matchers thy pairs (Envir.Envir {asol = tenv, iTs = tyenv, maxidx}) =
+fun first_order_matchers thy pairs (Envir.Envir {maxidx, tenv, tyenv}) =
let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv)
- in Seq.single (Envir.Envir {asol = tenv', iTs = tyenv', maxidx = maxidx}) end
+ in Seq.single (Envir.Envir {maxidx = maxidx, tenv = tenv', tyenv = tyenv'}) end
handle Pattern.MATCH => Seq.empty;
(*General matching -- keeps variables disjoint*)
@@ -661,10 +676,12 @@
Term.map_aterms (fn t as Var ((x, i), T) =>
if i > maxidx then Var ((x, i - offset), T) else t | t => t);
- fun norm_tvar (Envir.Envir {iTs = tyenv, ...}) ((x, i), S) =
- ((x, i - offset), (S, decr_indexesT (Envir.norm_type tyenv (TVar ((x, i), S)))));
- fun norm_var (env as Envir.Envir {iTs = tyenv, ...}) ((x, i), T) =
+ fun norm_tvar env ((x, i), S) =
+ ((x, i - offset),
+ (S, decr_indexesT (Envir.norm_type (Envir.type_env env) (TVar ((x, i), S)))));
+ fun norm_var env ((x, i), T) =
let
+ val tyenv = Envir.type_env env;
val T' = Envir.norm_type tyenv T;
val t' = Envir.norm_term env (Var ((x, i), T'));
in ((x, i - offset), (decr_indexesT T', decr_indexes t')) end;
@@ -672,8 +689,8 @@
fun result env =
if Envir.above env maxidx then (* FIXME proper handling of generated vars!? *)
SOME (Envir.Envir {maxidx = maxidx,
- iTs = Vartab.make (map (norm_tvar env) pat_tvars),
- asol = Vartab.make (map (norm_var env) pat_vars)})
+ tyenv = Vartab.make (map (norm_tvar env) pat_tvars),
+ tenv = Vartab.make (map (norm_var env) pat_vars)})
else NONE;
val empty = Envir.empty maxidx';
--- a/src/Tools/Compute_Oracle/linker.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/Tools/Compute_Oracle/linker.ML Fri Jul 17 23:13:50 2009 +0200
@@ -341,7 +341,7 @@
let
val (newsubsts, instances) = Linker.add_instances thy instances monocs
val _ = if not (null newsubsts) then changed := true else ()
- val newpats = map (fn subst => Envir.subst_TVars subst p) newsubsts
+ val newpats = map (fn subst => Envir.subst_term_types subst p) newsubsts
in
PolyPattern (p, instances, instancepats@newpats)
end
--- a/src/Tools/coherent.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/Tools/coherent.ML Fri Jul 17 23:13:50 2009 +0200
@@ -131,7 +131,7 @@
let val seq = Seq.of_list rules |> Seq.maps (fn (th, ps, cs) =>
valid_conj ctxt facts empty_env ps |> Seq.maps (fn (env as (tye, _), is) =>
let val cs' = map (fn (Ts, ts) =>
- (map (Envir.typ_subst_TVars tye) Ts, map (Envir.subst_vars env) ts)) cs
+ (map (Envir.subst_type tye) Ts, map (Envir.subst_term env) ts)) cs
in
inst_extra_vars ctxt dom cs' |>
Seq.map_filter (fn (inst, cs'') =>
@@ -184,7 +184,7 @@
(Thm.ctyp_of thy (TVar ((ixn, S))), Thm.ctyp_of thy T))
(Vartab.dest tye),
map (fn (ixn, (T, t)) =>
- (Thm.cterm_of thy (Var (ixn, Envir.typ_subst_TVars tye T)),
+ (Thm.cterm_of thy (Var (ixn, Envir.subst_type tye T)),
Thm.cterm_of thy t)) (Vartab.dest env) @
map (fn (ixnT, t) =>
(Thm.cterm_of thy (Var ixnT), Thm.cterm_of thy t)) insts) th)
--- a/src/Tools/eqsubst.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/Tools/eqsubst.ML Fri Jul 17 23:13:50 2009 +0200
@@ -231,9 +231,9 @@
or should I be using them somehow? *)
fun mk_insts env =
(Vartab.dest (Envir.type_env env),
- Envir.alist_of env);
- val initenv = Envir.Envir {asol = Vartab.empty,
- iTs = typinsttab, maxidx = ix2};
+ Vartab.dest (Envir.term_env env));
+ val initenv =
+ Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
val useq = Unify.smash_unifiers thry [a] initenv
handle UnequalLengths => Seq.empty
| Term.TERM _ => Seq.empty;
--- a/src/Tools/induct.ML Fri Jul 17 10:07:15 2009 +0200
+++ b/src/Tools/induct.ML Fri Jul 17 23:13:50 2009 +0200
@@ -423,14 +423,15 @@
local
-fun dest_env thy (env as Envir.Envir {iTs, ...}) =
+fun dest_env thy env =
let
val cert = Thm.cterm_of thy;
val certT = Thm.ctyp_of thy;
- val pairs = Envir.alist_of env;
+ val pairs = Vartab.dest (Envir.term_env env);
+ val types = Vartab.dest (Envir.type_env env);
val ts = map (cert o Envir.norm_term env o #2 o #2) pairs;
val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts);
- in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) (Vartab.dest iTs), xs ~~ ts) end;
+ in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) types, xs ~~ ts) end;
in
@@ -450,8 +451,7 @@
val rule' = Thm.incr_indexes (maxidx + 1) rule;
val concl = Logic.strip_assums_concl goal;
in
- Unify.smash_unifiers thy [(Thm.concl_of rule', concl)]
- (Envir.empty (#maxidx (Thm.rep_thm rule')))
+ Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
|> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
end
end handle Subscript => Seq.empty;