1.1 --- a/src/HOL/Library/reflection.ML Fri Jul 17 21:33:00 2009 +0200
1.2 +++ b/src/HOL/Library/reflection.ML Fri Jul 17 21:33:00 2009 +0200
1.3 @@ -153,8 +153,8 @@
1.4 val certy = ctyp_of thy
1.5 val (tyenv, tmenv) =
1.6 Pattern.match thy
1.7 - ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
1.8 - (Envir.type_env (Envir.empty 0), Vartab.empty)
1.9 + ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
1.10 + (Vartab.empty, Vartab.empty)
1.11 val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv)
1.12 val (fts,its) =
1.13 (map (snd o snd) fnvs,
1.14 @@ -204,9 +204,7 @@
1.15 val xns_map = (fst (split_list nths)) ~~ xns
1.16 val subst = map (fn (nt, xn) => (nt, Var ((xn,0), fastype_of nt))) xns_map
1.17 val rhs_P = subst_free subst rhs
1.18 - val (tyenv, tmenv) = Pattern.match
1.19 - thy (rhs_P, t)
1.20 - (Envir.type_env (Envir.empty 0), Vartab.empty)
1.21 + val (tyenv, tmenv) = Pattern.match thy (rhs_P, t) (Vartab.empty, Vartab.empty)
1.22 val sbst = Envir.subst_vars (tyenv, tmenv)
1.23 val sbsT = Envir.typ_subst_TVars tyenv
1.24 val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t))
2.1 --- a/src/HOL/Tools/meson.ML Fri Jul 17 21:33:00 2009 +0200
2.2 +++ b/src/HOL/Tools/meson.ML Fri Jul 17 21:33:00 2009 +0200
2.3 @@ -87,14 +87,12 @@
2.4 fun typ_pair_of (ix, (sort,ty)) = (TVar (ix,sort), ty);
2.5 fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t);
2.6
2.7 -val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
2.8 -
2.9 (*FIXME: currently does not "rename variables apart"*)
2.10 fun first_order_resolve thA thB =
2.11 let val thy = theory_of_thm thA
2.12 val tmA = concl_of thA
2.13 val Const("==>",_) $ tmB $ _ = prop_of thB
2.14 - val (tyenv,tenv) = Pattern.first_order_match thy (tmB,tmA) (tyenv0,tenv0)
2.15 + val (tyenv, tenv) = Pattern.first_order_match thy (tmB, tmA) (Vartab.empty, Vartab.empty)
2.16 val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
2.17 in thA RS (cterm_instantiate ct_pairs thB) end
2.18 handle _ => raise THM ("first_order_resolve", 0, [thA,thB]); (* FIXME avoid handle _ *)
2.19 @@ -104,8 +102,8 @@
2.20 [] => th
2.21 | pairs =>
2.22 let val thy = theory_of_thm th
2.23 - val (tyenv,tenv) =
2.24 - List.foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs
2.25 + val (tyenv, tenv) =
2.26 + fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
2.27 val t_pairs = map term_pair_of (Vartab.dest tenv)
2.28 val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
2.29 in th' end
3.1 --- a/src/Pure/Isar/proof_context.ML Fri Jul 17 21:33:00 2009 +0200
3.2 +++ b/src/Pure/Isar/proof_context.ML Fri Jul 17 21:33:00 2009 +0200
3.3 @@ -779,7 +779,7 @@
3.4 fun simult_matches ctxt (t, pats) =
3.5 (case Seq.pull (Unify.matchers (theory_of ctxt) (map (rpair t) pats)) of
3.6 NONE => error "Pattern match failed!"
3.7 - | SOME (env, _) => map (apsnd snd) (Envir.alist_of env));
3.8 + | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []);
3.9
3.10
3.11 (* bind_terms *)
4.1 --- a/src/Pure/Proof/extraction.ML Fri Jul 17 21:33:00 2009 +0200
4.2 +++ b/src/Pure/Proof/extraction.ML Fri Jul 17 21:33:00 2009 +0200
4.3 @@ -105,9 +105,8 @@
4.4 val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty);
4.5 val prems' = map (pairself (Envir.subst_vars env o inc o ren)) prems;
4.6 val env' = Envir.Envir
4.7 - {maxidx = Library.foldl Int.max
4.8 - (~1, map (Int.max o pairself maxidx_of_term) prems'),
4.9 - iTs = Tenv, asol = tenv};
4.10 + {maxidx = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) prems' ~1,
4.11 + tenv = tenv, tyenv = Tenv};
4.12 val env'' = fold (Pattern.unify thy o pairself (lookup rew)) prems' env';
4.13 in SOME (Envir.norm_term env'' (inc (ren tm2)))
4.14 end handle Pattern.MATCH => NONE | Pattern.Unif => NONE)
5.1 --- a/src/Pure/Proof/reconstruct.ML Fri Jul 17 21:33:00 2009 +0200
5.2 +++ b/src/Pure/Proof/reconstruct.ML Fri Jul 17 21:33:00 2009 +0200
5.3 @@ -35,12 +35,6 @@
5.4 fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_prf
5.5 (vars_of prop @ frees_of prop) prf;
5.6
5.7 -fun merge_envs (Envir.Envir {asol=asol1, iTs=iTs1, maxidx=maxidx1})
5.8 - (Envir.Envir {asol=asol2, iTs=iTs2, maxidx=maxidx2}) =
5.9 - Envir.Envir {asol=Vartab.merge (op =) (asol1, asol2),
5.10 - iTs=Vartab.merge (op =) (iTs1, iTs2),
5.11 - maxidx=Int.max (maxidx1, maxidx2)};
5.12 -
5.13
5.14 (**** generate constraints for proof term ****)
5.15
5.16 @@ -48,31 +42,32 @@
5.17 let val (env', v) = Envir.genvar "a" (env, rev Ts ---> T)
5.18 in (env', list_comb (v, map Bound (length Ts - 1 downto 0))) end;
5.19
5.20 -fun mk_tvar (Envir.Envir {iTs, asol, maxidx}, s) =
5.21 - (Envir.Envir {iTs = iTs, asol = asol, maxidx = maxidx+1},
5.22 - TVar (("'t", maxidx+1), s));
5.23 +fun mk_tvar (Envir.Envir {maxidx, tenv, tyenv}, s) =
5.24 + (Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv},
5.25 + TVar (("'t", maxidx + 1), s));
5.26
5.27 val mk_abs = fold (fn T => fn u => Abs ("", T, u));
5.28
5.29 fun unifyT thy env T U =
5.30 let
5.31 - val Envir.Envir {asol, iTs, maxidx} = env;
5.32 - val (iTs', maxidx') = Sign.typ_unify thy (T, U) (iTs, maxidx)
5.33 - in Envir.Envir {asol=asol, iTs=iTs', maxidx=maxidx'} end
5.34 - handle Type.TUNIFY => error ("Non-unifiable types:\n" ^
5.35 - Syntax.string_of_typ_global thy T ^ "\n\n" ^ Syntax.string_of_typ_global thy U);
5.36 + val Envir.Envir {maxidx, tenv, tyenv} = env;
5.37 + val (tyenv', maxidx') = Sign.typ_unify thy (T, U) (tyenv, maxidx);
5.38 + in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end;
5.39
5.40 -fun chaseT (env as Envir.Envir {iTs, ...}) (T as TVar ixnS) =
5.41 - (case Type.lookup iTs ixnS of NONE => T | SOME T' => chaseT env T')
5.42 +fun chaseT env (T as TVar v) =
5.43 + (case Type.lookup (Envir.type_env env) v of
5.44 + NONE => T
5.45 + | SOME T' => chaseT env T')
5.46 | chaseT _ T = T;
5.47
5.48 -fun infer_type thy (env as Envir.Envir {maxidx, asol, iTs}) Ts vTs
5.49 - (t as Const (s, T)) = if T = dummyT then (case Sign.const_type thy s of
5.50 +fun infer_type thy (env as Envir.Envir {maxidx, tenv, tyenv}) Ts vTs
5.51 + (t as Const (s, T)) = if T = dummyT then
5.52 + (case Sign.const_type thy s of
5.53 NONE => error ("reconstruct_proof: No such constant: " ^ quote s)
5.54 | SOME T =>
5.55 let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T)
5.56 in (Const (s, T'), T', vTs,
5.57 - Envir.Envir {maxidx = maxidx + 1, asol = asol, iTs = iTs})
5.58 + Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv})
5.59 end)
5.60 else (t, T, vTs, env)
5.61 | infer_type thy env Ts vTs (t as Free (s, T)) =
5.62 @@ -236,21 +231,23 @@
5.63
5.64 fun upd_constrs env cs =
5.65 let
5.66 - val Envir.Envir {asol, iTs, ...} = env;
5.67 + val tenv = Envir.term_env env;
5.68 + val tyenv = Envir.type_env env;
5.69 val dom = []
5.70 - |> Vartab.fold (cons o #1) asol
5.71 - |> Vartab.fold (cons o #1) iTs;
5.72 + |> Vartab.fold (cons o #1) tenv
5.73 + |> Vartab.fold (cons o #1) tyenv;
5.74 val vran = []
5.75 - |> Vartab.fold (Term.add_var_names o #2 o #2) asol
5.76 - |> Vartab.fold (Term.add_tvar_namesT o #2 o #2) iTs;
5.77 + |> Vartab.fold (Term.add_var_names o #2 o #2) tenv
5.78 + |> Vartab.fold (Term.add_tvar_namesT o #2 o #2) tyenv;
5.79 fun check_cs [] = []
5.80 - | check_cs ((u, p, vs)::ps) =
5.81 - let val vs' = subtract (op =) dom vs;
5.82 - in if vs = vs' then (u, p, vs)::check_cs ps
5.83 - else (true, p, fold (insert (op =)) vs' vran)::check_cs ps
5.84 - end
5.85 + | check_cs ((u, p, vs) :: ps) =
5.86 + let val vs' = subtract (op =) dom vs in
5.87 + if vs = vs' then (u, p, vs) :: check_cs ps
5.88 + else (true, p, fold (insert op =) vs' vran) :: check_cs ps
5.89 + end;
5.90 in check_cs cs end;
5.91
5.92 +
5.93 (**** solution of constraints ****)
5.94
5.95 fun solve _ [] bigenv = bigenv
5.96 @@ -280,7 +277,7 @@
5.97 val Envir.Envir {maxidx, ...} = bigenv;
5.98 val (env, cs') = search (Envir.empty maxidx) cs;
5.99 in
5.100 - solve thy (upd_constrs env cs') (merge_envs bigenv env)
5.101 + solve thy (upd_constrs env cs') (Envir.merge (bigenv, env))
5.102 end;
5.103
5.104
6.1 --- a/src/Pure/pattern.ML Fri Jul 17 21:33:00 2009 +0200
6.2 +++ b/src/Pure/pattern.ML Fri Jul 17 21:33:00 2009 +0200
6.3 @@ -141,8 +141,10 @@
6.4 | split_type (Type ("fun",[T1,T2]),n,Ts) = split_type (T2,n-1,T1::Ts)
6.5 | split_type _ = error("split_type");
6.6
6.7 -fun type_of_G (env as Envir.Envir {iTs, ...}) (T,n,is) =
6.8 - let val (Ts, U) = split_type (Envir.norm_type iTs T, n, [])
6.9 +fun type_of_G env (T, n, is) =
6.10 + let
6.11 + val tyenv = Envir.type_env env;
6.12 + val (Ts, U) = split_type (Envir.norm_type tyenv T, n, []);
6.13 in map (nth Ts) is ---> U end;
6.14
6.15 fun mkhnf (binders,is,G,js) = mkabs (binders, is, app(G,js));
6.16 @@ -225,11 +227,12 @@
6.17 end;
6.18 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
6.19
6.20 -fun unify_types thy (T,U) (env as Envir.Envir{asol,iTs,maxidx}) =
6.21 - if T=U then env
6.22 - else let val (iTs',maxidx') = Sign.typ_unify thy (U, T) (iTs, maxidx)
6.23 - in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
6.24 - handle Type.TUNIFY => (typ_clash thy (iTs,T,U); raise Unif);
6.25 +fun unify_types thy (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) =
6.26 + if T = U then env
6.27 + else
6.28 + let val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx)
6.29 + in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end
6.30 + handle Type.TUNIFY => (typ_clash thy (tyenv, T, U); raise Unif);
6.31
6.32 fun unif thy binders (s,t) env = case (Envir.head_norm env s, Envir.head_norm env t) of
6.33 (Abs(ns,Ts,ts),Abs(nt,Tt,tt)) =>
7.1 --- a/src/Pure/proofterm.ML Fri Jul 17 21:33:00 2009 +0200
7.2 +++ b/src/Pure/proofterm.ML Fri Jul 17 21:33:00 2009 +0200
7.3 @@ -489,9 +489,8 @@
7.4 | remove_types (Const (s, _)) = Const (s, dummyT)
7.5 | remove_types t = t;
7.6
7.7 -fun remove_types_env (Envir.Envir {iTs, asol, maxidx}) =
7.8 - Envir.Envir {iTs = iTs, asol = Vartab.map (apsnd remove_types) asol,
7.9 - maxidx = maxidx};
7.10 +fun remove_types_env (Envir.Envir {maxidx, tenv, tyenv}) =
7.11 + Envir.Envir {maxidx = maxidx, tenv = Vartab.map (apsnd remove_types) tenv, tyenv = tyenv};
7.12
7.13 fun norm_proof' env prf = norm_proof (remove_types_env env) prf;
7.14
8.1 --- a/src/Pure/thm.ML Fri Jul 17 21:33:00 2009 +0200
8.2 +++ b/src/Pure/thm.ML Fri Jul 17 21:33:00 2009 +0200
8.3 @@ -1247,12 +1247,12 @@
8.4 val Thm (der, {thy_ref, maxidx, shyps, hyps, prop, ...}) = state;
8.5 val thy = Theory.deref thy_ref;
8.6 val (tpairs, Bs, Bi, C) = dest_state (state, i);
8.7 - fun newth n (env as Envir.Envir {maxidx, ...}, tpairs) =
8.8 + fun newth n (env, tpairs) =
8.9 Thm (deriv_rule1
8.10 ((if Envir.is_empty env then I else (Pt.norm_proof' env)) o
8.11 Pt.assumption_proof Bs Bi n) der,
8.12 {tags = [],
8.13 - maxidx = maxidx,
8.14 + maxidx = Envir.maxidx_of env,
8.15 shyps = Envir.insert_sorts env shyps,
8.16 hyps = hyps,
8.17 tpairs =
8.18 @@ -1465,15 +1465,15 @@
8.19
8.20 (*Faster normalization: skip assumptions that were lifted over*)
8.21 fun norm_term_skip env 0 t = Envir.norm_term env t
8.22 - | norm_term_skip env n (Const("all",_)$Abs(a,T,t)) =
8.23 - let val Envir.Envir{iTs, ...} = env
8.24 - val T' = Envir.typ_subst_TVars iTs T
8.25 - (*Must instantiate types of parameters because they are flattened;
8.26 - this could be a NEW parameter*)
8.27 - in Term.all T' $ Abs(a, T', norm_term_skip env n t) end
8.28 - | norm_term_skip env n (Const("==>", _) $ A $ B) =
8.29 - Logic.mk_implies (A, norm_term_skip env (n-1) B)
8.30 - | norm_term_skip env n t = error"norm_term_skip: too few assumptions??";
8.31 + | norm_term_skip env n (Const ("all", _) $ Abs (a, T, t)) =
8.32 + let
8.33 + val T' = Envir.typ_subst_TVars (Envir.type_env env) T
8.34 + (*Must instantiate types of parameters because they are flattened;
8.35 + this could be a NEW parameter*)
8.36 + in Term.all T' $ Abs (a, T', norm_term_skip env n t) end
8.37 + | norm_term_skip env n (Const ("==>", _) $ A $ B) =
8.38 + Logic.mk_implies (A, norm_term_skip env (n - 1) B)
8.39 + | norm_term_skip env n t = error "norm_term_skip: too few assumptions??";
8.40
8.41
8.42 (*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C)
8.43 @@ -1495,7 +1495,7 @@
8.44 and nlift = Logic.count_prems (strip_all_body Bi) + (if eres_flg then ~1 else 0)
8.45 val thy = Theory.deref (merge_thys2 state orule);
8.46 (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)
8.47 - fun addth A (As, oldAs, rder', n) ((env as Envir.Envir {maxidx, ...}, tpairs), thq) =
8.48 + fun addth A (As, oldAs, rder', n) ((env, tpairs), thq) =
8.49 let val normt = Envir.norm_term env;
8.50 (*perform minimal copying here by examining env*)
8.51 val (ntpairs, normp) =
8.52 @@ -1520,7 +1520,7 @@
8.53 curry op oo (Pt.norm_proof' env))
8.54 (Pt.bicompose_proof flatten Bs oldAs As A n (nlift+1))) rder' sder,
8.55 {tags = [],
8.56 - maxidx = maxidx,
8.57 + maxidx = Envir.maxidx_of env,
8.58 shyps = Envir.insert_sorts env (Sorts.union rshyps sshyps),
8.59 hyps = union_hyps rhyps shyps,
8.60 tpairs = ntpairs,
9.1 --- a/src/Pure/unify.ML Fri Jul 17 21:33:00 2009 +0200
9.2 +++ b/src/Pure/unify.ML Fri Jul 17 21:33:00 2009 +0200
9.3 @@ -52,36 +52,48 @@
9.4
9.5 type dpair = binderlist * term * term;
9.6
9.7 -fun body_type(Envir.Envir{iTs,...}) =
9.8 -let fun bT(Type("fun",[_,T])) = bT T
9.9 - | bT(T as TVar ixnS) = (case Type.lookup iTs ixnS of
9.10 - NONE => T | SOME(T') => bT T')
9.11 - | bT T = T
9.12 -in bT end;
9.13 +fun body_type env =
9.14 + let
9.15 + val tyenv = Envir.type_env env;
9.16 + fun bT (Type ("fun", [_, T])) = bT T
9.17 + | bT (T as TVar v) =
9.18 + (case Type.lookup tyenv v of
9.19 + NONE => T
9.20 + | SOME T' => bT T')
9.21 + | bT T = T;
9.22 + in bT end;
9.23
9.24 -fun binder_types(Envir.Envir{iTs,...}) =
9.25 -let fun bTs(Type("fun",[T,U])) = T :: bTs U
9.26 - | bTs(T as TVar ixnS) = (case Type.lookup iTs ixnS of
9.27 - NONE => [] | SOME(T') => bTs T')
9.28 - | bTs _ = []
9.29 -in bTs end;
9.30 +fun binder_types env =
9.31 + let
9.32 + val tyenv = Envir.type_env env;
9.33 + fun bTs (Type ("fun", [T, U])) = T :: bTs U
9.34 + | bTs (T as TVar v) =
9.35 + (case Type.lookup tyenv v of
9.36 + NONE => []
9.37 + | SOME T' => bTs T')
9.38 + | bTs _ = [];
9.39 + in bTs end;
9.40
9.41 fun strip_type env T = (binder_types env T, body_type env T);
9.42
9.43 fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t;
9.44
9.45
9.46 -(*Eta normal form*)
9.47 -fun eta_norm(env as Envir.Envir{iTs,...}) =
9.48 - let fun etif (Type("fun",[T,U]), t) =
9.49 - Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
9.50 - | etif (TVar ixnS, t) =
9.51 - (case Type.lookup iTs ixnS of
9.52 - NONE => t | SOME(T) => etif(T,t))
9.53 - | etif (_,t) = t;
9.54 - fun eta_nm (rbinder, Abs(a,T,body)) =
9.55 - Abs(a, T, eta_nm ((a,T)::rbinder, body))
9.56 - | eta_nm (rbinder, t) = etif(fastype env (rbinder,t), t)
9.57 +(* eta normal form *)
9.58 +
9.59 +fun eta_norm env =
9.60 + let
9.61 + val tyenv = Envir.type_env env;
9.62 + fun etif (Type ("fun", [T, U]), t) =
9.63 + Abs ("", T, etif (U, incr_boundvars 1 t $ Bound 0))
9.64 + | etif (TVar v, t) =
9.65 + (case Type.lookup tyenv v of
9.66 + NONE => t
9.67 + | SOME T => etif (T, t))
9.68 + | etif (_, t) = t;
9.69 + fun eta_nm (rbinder, Abs (a, T, body)) =
9.70 + Abs (a, T, eta_nm ((a, T) :: rbinder, body))
9.71 + | eta_nm (rbinder, t) = etif (fastype env (rbinder, t), t);
9.72 in eta_nm end;
9.73
9.74
9.75 @@ -186,11 +198,14 @@
9.76 exception ASSIGN; (*Raised if not an assignment*)
9.77
9.78
9.79 -fun unify_types thy (T,U, env as Envir.Envir{asol,iTs,maxidx}) =
9.80 - if T=U then env
9.81 - else let val (iTs',maxidx') = Sign.typ_unify thy (U, T) (iTs, maxidx)
9.82 - in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
9.83 - handle Type.TUNIFY => raise CANTUNIFY;
9.84 +fun unify_types thy (T, U, env) =
9.85 + if T = U then env
9.86 + else
9.87 + let
9.88 + val Envir.Envir {maxidx, tenv, tyenv} = env;
9.89 + val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx);
9.90 + in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end
9.91 + handle Type.TUNIFY => raise CANTUNIFY;
9.92
9.93 fun test_unify_types thy (args as (T,U,_)) =
9.94 let val str_of = Syntax.string_of_typ_global thy;
9.95 @@ -636,9 +651,9 @@
9.96
9.97
9.98 (*Pattern matching*)
9.99 -fun first_order_matchers thy pairs (Envir.Envir {asol = tenv, iTs = tyenv, maxidx}) =
9.100 +fun first_order_matchers thy pairs (Envir.Envir {maxidx, tenv, tyenv}) =
9.101 let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv)
9.102 - in Seq.single (Envir.Envir {asol = tenv', iTs = tyenv', maxidx = maxidx}) end
9.103 + in Seq.single (Envir.Envir {maxidx = maxidx, tenv = tenv', tyenv = tyenv'}) end
9.104 handle Pattern.MATCH => Seq.empty;
9.105
9.106 (*General matching -- keeps variables disjoint*)
9.107 @@ -661,10 +676,12 @@
9.108 Term.map_aterms (fn t as Var ((x, i), T) =>
9.109 if i > maxidx then Var ((x, i - offset), T) else t | t => t);
9.110
9.111 - fun norm_tvar (Envir.Envir {iTs = tyenv, ...}) ((x, i), S) =
9.112 - ((x, i - offset), (S, decr_indexesT (Envir.norm_type tyenv (TVar ((x, i), S)))));
9.113 - fun norm_var (env as Envir.Envir {iTs = tyenv, ...}) ((x, i), T) =
9.114 + fun norm_tvar env ((x, i), S) =
9.115 + ((x, i - offset),
9.116 + (S, decr_indexesT (Envir.norm_type (Envir.type_env env) (TVar ((x, i), S)))));
9.117 + fun norm_var env ((x, i), T) =
9.118 let
9.119 + val tyenv = Envir.type_env env;
9.120 val T' = Envir.norm_type tyenv T;
9.121 val t' = Envir.norm_term env (Var ((x, i), T'));
9.122 in ((x, i - offset), (decr_indexesT T', decr_indexes t')) end;
9.123 @@ -672,8 +689,8 @@
9.124 fun result env =
9.125 if Envir.above env maxidx then (* FIXME proper handling of generated vars!? *)
9.126 SOME (Envir.Envir {maxidx = maxidx,
9.127 - iTs = Vartab.make (map (norm_tvar env) pat_tvars),
9.128 - asol = Vartab.make (map (norm_var env) pat_vars)})
9.129 + tyenv = Vartab.make (map (norm_tvar env) pat_tvars),
9.130 + tenv = Vartab.make (map (norm_var env) pat_vars)})
9.131 else NONE;
9.132
9.133 val empty = Envir.empty maxidx';
10.1 --- a/src/Tools/eqsubst.ML Fri Jul 17 21:33:00 2009 +0200
10.2 +++ b/src/Tools/eqsubst.ML Fri Jul 17 21:33:00 2009 +0200
10.3 @@ -231,9 +231,9 @@
10.4 or should I be using them somehow? *)
10.5 fun mk_insts env =
10.6 (Vartab.dest (Envir.type_env env),
10.7 - Envir.alist_of env);
10.8 - val initenv = Envir.Envir {asol = Vartab.empty,
10.9 - iTs = typinsttab, maxidx = ix2};
10.10 + Vartab.dest (Envir.term_env env));
10.11 + val initenv =
10.12 + Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
10.13 val useq = Unify.smash_unifiers thry [a] initenv
10.14 handle UnequalLengths => Seq.empty
10.15 | Term.TERM _ => Seq.empty;
11.1 --- a/src/Tools/induct.ML Fri Jul 17 21:33:00 2009 +0200
11.2 +++ b/src/Tools/induct.ML Fri Jul 17 21:33:00 2009 +0200
11.3 @@ -423,14 +423,15 @@
11.4
11.5 local
11.6
11.7 -fun dest_env thy (env as Envir.Envir {iTs, ...}) =
11.8 +fun dest_env thy env =
11.9 let
11.10 val cert = Thm.cterm_of thy;
11.11 val certT = Thm.ctyp_of thy;
11.12 - val pairs = Envir.alist_of env;
11.13 + val pairs = Vartab.dest (Envir.term_env env);
11.14 + val types = Vartab.dest (Envir.type_env env);
11.15 val ts = map (cert o Envir.norm_term env o #2 o #2) pairs;
11.16 val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts);
11.17 - in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) (Vartab.dest iTs), xs ~~ ts) end;
11.18 + in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) types, xs ~~ ts) end;
11.19
11.20 in
11.21
11.22 @@ -450,8 +451,7 @@
11.23 val rule' = Thm.incr_indexes (maxidx + 1) rule;
11.24 val concl = Logic.strip_assums_concl goal;
11.25 in
11.26 - Unify.smash_unifiers thy [(Thm.concl_of rule', concl)]
11.27 - (Envir.empty (#maxidx (Thm.rep_thm rule')))
11.28 + Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
11.29 |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
11.30 end
11.31 end handle Subscript => Seq.empty;