Adapted to new interface of instantiation and unification / matching functions.
--- a/TFL/casesplit.ML Thu Apr 21 19:12:03 2005 +0200
+++ b/TFL/casesplit.ML Thu Apr 21 19:13:03 2005 +0200
@@ -162,11 +162,12 @@
case (Thm.concl_of case_thm) of
(_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) =>
(Pv, Dv,
- Vartab.dest (Type.typ_match tsig (Vartab.empty, (Dty, ty))))
+ Type.typ_match tsig (Vartab.empty, (Dty, ty)))
| _ => raise ERROR_MESSAGE ("not a valid case thm");
- val type_cinsts = map (apsnd ctypify) type_insts;
- val cPv = ctermify (Sign.inst_term_tvars sgn type_insts Pv);
- val cDv = ctermify (Sign.inst_term_tvars sgn type_insts Dv);
+ 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);
in
(beta_eta_contract
(case_thm
--- a/TFL/rules.ML Thu Apr 21 19:12:03 2005 +0200
+++ b/TFL/rules.ML Thu Apr 21 19:13:03 2005 +0200
@@ -276,12 +276,12 @@
local (* this is fragile *)
val {prop,sign,...} = rep_thm spec
val x = hd (tl (term_vars prop))
- val (TVar (indx,_)) = type_of x
+ val cTV = ctyp_of sign (type_of x)
val gspec = forall_intr (cterm_of sign x) spec
in
fun SPEC tm thm =
let val {sign,T,...} = rep_cterm tm
- val gspec' = instantiate([(indx,ctyp_of sign T)],[]) gspec
+ val gspec' = instantiate ([(cTV, ctyp_of sign T)], []) gspec
in
thm RS (forall_elim tm gspec')
end
@@ -295,13 +295,14 @@
(* Not optimized! Too complicated. *)
local val {prop,sign,...} = rep_thm allI
val [P] = add_term_vars (prop, [])
- fun cty_theta s = map (fn (i,ty) => (i, ctyp_of s ty))
- fun ctm_theta s = map (fn (i,tm2) =>
+ fun cty_theta s = map (fn (i, (S, ty)) => (ctyp_of s (TVar (i, S)), ctyp_of s ty))
+ fun ctm_theta s = map (fn (i, (_, tm2)) =>
let val ctm2 = cterm_of s tm2
in (cterm_of s (Var(i,#T(rep_cterm ctm2))), ctm2)
end)
- fun certify s (ty_theta,tm_theta) = (cty_theta s ty_theta,
- ctm_theta s tm_theta)
+ fun certify s (ty_theta,tm_theta) =
+ (cty_theta s (Vartab.dest ty_theta),
+ ctm_theta s (Vartab.dest tm_theta))
in
fun GEN v th =
let val gth = forall_intr v th
--- a/TFL/thry.ML Thu Apr 21 19:12:03 2005 +0200
+++ b/TFL/thry.ML Thu Apr 21 19:13:03 2005 +0200
@@ -26,17 +26,23 @@
* Matching
*---------------------------------------------------------------------------*)
-local fun tybind (x,y) = (TVar (x, HOLogic.typeS) , y)
- fun tmbind (x,y) = (Var (x, Term.type_of y), y)
+local
+
+fun tybind (ixn, (S, T)) = (TVar (ixn, S), T);
+
in
- fun match_term thry pat ob =
- let val tsig = Sign.tsig_of (Theory.sign_of thry)
- val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob)
- in (map tmbind tm_theta, map tybind ty_theta)
- end
- fun match_type thry pat ob = map tybind (Vartab.dest
- (Type.typ_match (Sign.tsig_of (Theory.sign_of thry)) (Vartab.empty, (pat,ob))))
+fun match_term thry pat ob =
+ let
+ val tsig = Sign.tsig_of (Theory.sign_of thry)
+ val (ty_theta, tm_theta) = Pattern.match tsig (pat,ob)
+ fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t)
+ in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta))
+ end;
+
+fun match_type thry pat ob = map tybind (Vartab.dest
+ (Type.typ_match (Sign.tsig_of (Theory.sign_of thry)) (Vartab.empty, (pat, ob))));
+
end;
--- a/src/Pure/IsaPlanner/rw_inst.ML Thu Apr 21 19:12:03 2005 +0200
+++ b/src/Pure/IsaPlanner/rw_inst.ML Thu Apr 21 19:13:03 2005 +0200
@@ -33,7 +33,7 @@
(string * Term.typ) list -> Thm.thm -> Thm.cterm list * Thm.thm
val mk_fixtvar_tyinsts :
Term.indexname list ->
- Term.term list -> ((string * int) * Term.typ) list * string list
+ Term.term list -> ((string * int) * Term.typ) list * (string * sort) list
val mk_renamings :
Term.term -> Thm.thm -> (((string * int) * Term.typ) * Term.term) list
val new_tfree :
@@ -151,14 +151,14 @@
(* make instantiations to fix type variables that are not
already instantiated (in ignore_ixs) from the list of terms. *)
fun mk_fixtvar_tyinsts ignore_ixs ts =
- let val (tvars, tfreenames) =
- foldr (fn (t, (varixs, tfreenames)) =>
+ let val (tvars, tfrees) =
+ foldr (fn (t, (varixs, tfrees)) =>
(Term.add_term_tvars (t,varixs),
- Term.add_term_tfree_names (t,tfreenames)))
+ Term.add_term_tfrees (t,tfrees)))
([],[]) ts;
val unfixed_tvars = List.filter (fn (ix,s) => not (ix mem ignore_ixs)) tvars;
- val (fixtyinsts, _) = foldr new_tfree ([], tfreenames) unfixed_tvars
- in (fixtyinsts, tfreenames) end;
+ val (fixtyinsts, _) = foldr new_tfree ([], map fst tfrees) unfixed_tvars
+ in (fixtyinsts, tfrees) end;
(* cross-instantiate the instantiations - ie for each instantiation
@@ -212,10 +212,13 @@
val ctyp_insts = map (apsnd ctypeify) typinsts;
(* type instantiated versions *)
- val tgt_th_tyinst =
- Thm.instantiate (ctyp_insts, []) target_thm;
- val rule_tyinst =
- Thm.instantiate (ctyp_insts, []) rule;
+ fun tyinst insts rule =
+ let val (_, rsorts) = types_sorts rule
+ in Thm.instantiate (List.mapPartial (fn (ixn, cT) => Option.map
+ (fn S => (ctypeify (TVar (ixn, S)), cT)) (rsorts ixn)) insts, []) rule
+ end;
+ val tgt_th_tyinst = tyinst ctyp_insts target_thm;
+ val rule_tyinst = tyinst ctyp_insts rule;
(* type instanitated outer term *)
val outerterm_tyinst =
--- a/src/Pure/IsaPlanner/term_lib.ML Thu Apr 21 19:12:03 2005 +0200
+++ b/src/Pure/IsaPlanner/term_lib.ML Thu Apr 21 19:13:03 2005 +0200
@@ -143,7 +143,10 @@
(* Higher order matching with exception handled *)
(* returns optional instantiation *)
fun clean_match tsig (a as (pat, t)) =
- SOME (Pattern.match tsig a) handle Pattern.MATCH => NONE;
+ let val (tyenv, tenv) = Pattern.match tsig a
+ in SOME (map (apsnd snd) (Vartab.dest tyenv),
+ map (apsnd snd) (Vartab.dest tenv))
+ end handle Pattern.MATCH => NONE;
(* Higher order unification with exception handled, return the instantiations *)
(* given Signature, max var index, pat, tgt *)
(* returns Seq of instantiations *)
@@ -166,7 +169,8 @@
(* is it right to throw away the flexes?
or should I be using them somehow? *)
fun mk_insts (env,flexflexes) =
- (Vartab.dest (Envir.type_env env), Envir.alist_of env);
+ (map (apsnd snd) (Vartab.dest (Envir.type_env env)),
+ map (apsnd snd) (Envir.alist_of env));
val initenv = Envir.Envir {asol = Vartab.empty,
iTs = typinsttab, maxidx = ix2};
val useq = (Unify.unifiers (sgn,initenv,[a]))
--- a/src/Pure/Isar/attrib.ML Thu Apr 21 19:12:03 2005 +0200
+++ b/src/Pure/Isar/attrib.ML Thu Apr 21 19:13:03 2005 +0200
@@ -260,13 +260,14 @@
fun typ_subst env = apsnd (Term.typ_subst_TVars env);
fun subst env = apsnd (Term.subst_TVars env);
-fun instantiate sign envT env =
+fun instantiate sign envT env thm =
let
- fun prepT (a, T) = (a, Thm.ctyp_of sign T);
+ val (_, sorts) = Drule.types_sorts thm;
+ fun prepT (a, T) = (Thm.ctyp_of sign (TVar (a, the_sort sorts a)), Thm.ctyp_of sign T);
fun prep (xi, t) = pairself (Thm.cterm_of sign) (Var (xi, Term.fastype_of t), t);
in
Drule.instantiate (map prepT (distinct envT),
- map prep (gen_distinct (fn ((xi, t), (yj, u)) => xi = yj andalso t aconv u) env))
+ map prep (gen_distinct (fn ((xi, t), (yj, u)) => xi = yj andalso t aconv u) env)) thm
end;
in
@@ -309,8 +310,8 @@
(* internal term instantiations *)
val types' = #1 (Drule.types_sorts thm');
- val unifier = Vartab.dest (#1
- (Library.foldl (unify_types sign types') ((Vartab.empty, 0), internal_insts)));
+ val unifier = map (apsnd snd) (Vartab.dest (#1
+ (Library.foldl (unify_types sign types') ((Vartab.empty, 0), internal_insts))));
val type_insts'' = map (typ_subst unifier) type_insts';
val internal_insts'' = map (subst unifier) internal_insts;
--- a/src/Pure/Isar/locale.ML Thu Apr 21 19:12:03 2005 +0200
+++ b/src/Pure/Isar/locale.ML Thu Apr 21 19:13:03 2005 +0200
@@ -499,7 +499,8 @@
|> Drule.implies_intr_list (map cert hyps)
|> Drule.tvars_intr_list (map (#1 o #1) env')
|> (fn (th', al) => th' |>
- Thm.instantiate ((map (fn ((a, _), T) => (valOf (assoc (al, a)), certT T)) env'), []))
+ Thm.instantiate ((map (fn ((a, _), T) =>
+ (certT (TVar (valOf (assoc (al, a)))), certT T)) env'), []))
|> (fn th'' => Drule.implies_elim_list th''
(map (Thm.assume o cert o inst_term env') hyps))
end;
@@ -535,7 +536,7 @@
else thm |> Drule.implies_intr_list (map cert hyps)
|> Drule.tvars_intr_list (map #1 tinst')
|> (fn (th, al) => th |> Thm.instantiate
- ((map (fn (a, T) => (valOf (assoc (al, a)), certT T)) tinst'),
+ ((map (fn (a, T) => (certT (TVar (valOf (assoc (al, a)))), certT T)) tinst'),
[]))
|> (fn th => Drule.implies_elim_list th
(map (Thm.assume o cert o tinst_tab_term tinst) hyps))
@@ -584,7 +585,7 @@
else thm |> Drule.implies_intr_list (map cert hyps)
|> Drule.tvars_intr_list (map #1 tinst')
|> (fn (th, al) => th |> Thm.instantiate
- ((map (fn (a, T) => (valOf (assoc (al, a)), certT T)) tinst'),
+ ((map (fn (a, T) => (certT (TVar (valOf (assoc (al, a)))), certT T)) tinst'),
[]))
|> Drule.forall_intr_list (map (cert o #1) inst')
|> Drule.forall_elim_list (map (cert o #2) inst')
@@ -604,14 +605,14 @@
(* parameter types *)
(* CB: frozen_tvars has the following type:
- ProofContext.context -> Term.typ list -> (Term.indexname * Term.typ) list *)
+ ProofContext.context -> Term.typ list -> (Term.indexname * (sort * Term.typ)) list *)
fun frozen_tvars ctxt Ts =
let
val tvars = rev (Library.foldl Term.add_tvarsT ([], Ts));
val tfrees = map TFree
(Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars);
- in map #1 tvars ~~ tfrees end;
+ in map (fn ((x, S), y) => (x, (S, y))) (tvars ~~ tfrees) end;
fun unify_frozen ctxt maxidx Ts Us =
let
@@ -1382,7 +1383,7 @@
(* get their sorts *)
val tfrees = foldr Term.add_typ_tfrees [] param_types
val Tenv' = map
- (fn ((a, i), T) => ((a, valOf (assoc_string (tfrees, a))), T))
+ (fn ((a, i), (S, T)) => ((a, S), T))
(Vartab.dest Tenv);
(* process (internal) elements *)
@@ -1417,7 +1418,7 @@
|> Drule.tvars_intr_list (map (#1 o #1) Tenv')
|> (fn (th', al) => th' |>
Thm.instantiate ((map (fn ((a, _), T) =>
- (valOf (assoc (al, a)), certT T)) Tenv'), []))
+ (certT (TVar (valOf (assoc (al, a)))), certT T)) Tenv'), []))
|> (fn th'' => Drule.implies_elim_list th''
(map (Thm.assume o cert o inst_term Tenv') hyps))
end;
@@ -1623,7 +1624,7 @@
(* type instantiation *)
val vtinst = Library.foldl (Type.typ_match (Sign.tsig_of sign))
(Vartab.empty, (parmvTs ~~ map Term.fastype_of ts));
- val tinst = Vartab.dest vtinst |> map (fn ((x, 0), T) => (x, T))
+ val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
|> Symtab.make;
(* replace parameter names in ids by instantiations *)
val vinst = Symtab.make (parms ~~ vts);
--- a/src/Pure/Isar/method.ML Thu Apr 21 19:12:03 2005 +0200
+++ b/src/Pure/Isar/method.ML Thu Apr 21 19:13:03 2005 +0200
@@ -354,7 +354,8 @@
fun readT (xi, s) =
let val S = case rsorts xi of SOME S => S | NONE => absent xi;
val T = Sign.read_typ (sign, sorts) s;
- in if Sign.typ_instance sign (T, TVar (xi, S)) then (xi, T)
+ val U = TVar (xi, S);
+ in if Sign.typ_instance sign (T, U) then (U, T)
else error
("Instantiation of " ^ Syntax.string_of_vname xi ^ " fails")
end;
@@ -362,7 +363,7 @@
(* Preprocess rule: extract vars and their types, apply Tinsts *)
fun get_typ xi =
(case rtypes xi of
- SOME T => typ_subst_TVars Tinsts_env T
+ SOME T => typ_subst_atomic Tinsts_env T
| NONE => absent xi);
val (xis, ss) = Library.split_list tinsts;
val Ts = map get_typ xis;
@@ -380,7 +381,8 @@
val used = Drule.add_used thm (Drule.add_used st []);
val (ts, envT) =
ProofContext.read_termTs_schematic ctxt internal types' sorts used (ss ~~ Ts);
- val cenvT = map (apsnd (Thm.ctyp_of sign)) (envT @ Tinsts_env);
+ val envT' = map (fn (ixn, T) =>
+ (TVar (ixn, valOf (rsorts ixn)), T)) envT @ Tinsts_env;
val cenv =
map
(fn (xi, t) =>
@@ -399,11 +401,9 @@
(params, Logic.incr_indexes(paramTs,inc) t)
fun liftpair (cv,ct) =
(cterm_fun liftvar cv, cterm_fun liftterm ct)
- fun lifttvar((a,i),ctyp) =
- let val {T,sign} = rep_ctyp ctyp
- in ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
+ val lifttvar = pairself (ctyp_of sign o incr_tvar inc);
val rule = Drule.instantiate
- (map lifttvar cenvT, map liftpair cenv)
+ (map lifttvar envT', map liftpair cenv)
(lift_rule (st, i) thm)
in
if i > nprems_of st then no_tac st
--- a/src/Pure/Isar/proof_context.ML Thu Apr 21 19:12:03 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML Thu Apr 21 19:13:03 2005 +0200
@@ -562,7 +562,7 @@
let
val env = unifyT ctxt (T, U) handle Type.TUNIFY =>
raise TYPE ("norm_term: ill-typed variable assignment", [T, U], [t, u]);
- val u' = Term.subst_TVars_Vartab env u;
+ val u' = Envir.subst_TVars env u;
in norm u' handle SAME => u' end
| NONE =>
if schematic then raise SAME
@@ -877,7 +877,7 @@
val _ = (*may not assign variables from text*)
if null (map #1 (Envir.alist_of env) inter (map #1 (Drule.vars_of_terms (map #2 pairs))))
then () else fail ();
- fun norm_bind (xi, t) = if xi mem domain then SOME (xi, Envir.norm_term env t) else NONE;
+ fun norm_bind (xi, (_, t)) = if xi mem domain then SOME (xi, Envir.norm_term env t) else NONE;
in List.mapPartial norm_bind (Envir.alist_of env) end;
--- a/src/Pure/Proof/extraction.ML Thu Apr 21 19:12:03 2005 +0200
+++ b/src/Pure/Proof/extraction.ML Thu Apr 21 19:13:03 2005 +0200
@@ -108,11 +108,11 @@
fun ren t = getOpt (Term.rename_abs tm1 tm t, t);
val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1);
val env as (Tenv, tenv) = Pattern.match tsig (inc tm1, tm);
- val prems' = map (pairself (subst_vars env o inc o ren)) prems;
+ val prems' = map (pairself (Envir.subst_vars 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 = Vartab.make Tenv, asol = Vartab.make tenv};
+ iTs = Tenv, asol = tenv};
val env'' = Library.foldl (fn (env, p) =>
Pattern.unify (sign, env, [pairself (lookup rew) p])) (env', prems')
in SOME (Envir.norm_term env'' (inc (ren tm2)))
--- a/src/Pure/Proof/proofchecker.ML Thu Apr 21 19:12:03 2005 +0200
+++ b/src/Pure/Proof/proofchecker.ML Thu Apr 21 19:13:03 2005 +0200
@@ -40,7 +40,8 @@
let
val tvars = term_tvars (prop_of thm);
val (thm', fmap) = Thm.varifyT' [] thm;
- val ctye = map fst tvars @ map snd fmap ~~ map (Thm.ctyp_of sg) Ts
+ val ctye = map (pairself (Thm.ctyp_of sg))
+ (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
in
Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm'))
end;
--- a/src/Pure/Proof/reconstruct.ML Thu Apr 21 19:12:03 2005 +0200
+++ b/src/Pure/Proof/reconstruct.ML Thu Apr 21 19:13:03 2005 +0200
@@ -42,7 +42,7 @@
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 aconv) (asol1, asol2),
+ Envir.Envir {asol=Vartab.merge (op =) (asol1, asol2),
iTs=Vartab.merge (op =) (iTs1, iTs2),
maxidx=Int.max (maxidx1, maxidx2)};
@@ -67,8 +67,8 @@
handle Type.TUNIFY => error ("Non-unifiable types:\n" ^
Sign.string_of_typ sg T ^ "\n\n" ^ Sign.string_of_typ sg U);
-fun chaseT (env as Envir.Envir {iTs, ...}) (T as TVar (ixn, _)) =
- (case Vartab.lookup (iTs, ixn) of NONE => T | SOME T' => chaseT env T')
+fun chaseT (env as Envir.Envir {iTs, ...}) (T as TVar ixnS) =
+ (case Type.lookup (iTs, ixnS) of NONE => T | SOME T' => chaseT env T')
| chaseT _ T = T;
fun infer_type sg (env as Envir.Envir {maxidx, asol, iTs}) Ts vTs
@@ -247,8 +247,8 @@
val Envir.Envir {asol, iTs, ...} = env;
val dom = Vartab.foldl (uncurry (cons o fst) o Library.swap)
(Vartab.foldl (uncurry (cons o fst) o Library.swap) ([], asol), iTs);
- val vran = Vartab.foldl (add_typ_ixns o apsnd snd)
- (Vartab.foldl (add_term_ixns o apsnd snd) ([], asol), iTs);
+ val vran = Vartab.foldl (add_typ_ixns o apsnd (snd o snd))
+ (Vartab.foldl (add_term_ixns o apsnd (snd o snd)) ([], asol), iTs);
fun check_cs [] = []
| check_cs ((u, p, vs)::ps) =
let val vs' = vs \\ dom;