--- a/src/Pure/Tools/rule_insts.ML Thu Mar 19 17:25:57 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML Thu Mar 19 22:30:57 2015 +0100
@@ -6,11 +6,16 @@
signature BASIC_RULE_INSTS =
sig
- val res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
- val eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
- val cut_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
- val forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
- val dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
+ val res_inst_tac: Proof.context ->
+ ((indexname * Position.T) * string) list -> thm -> int -> tactic
+ val eres_inst_tac: Proof.context ->
+ ((indexname * Position.T) * string) list -> thm -> int -> tactic
+ val cut_inst_tac: Proof.context ->
+ ((indexname * Position.T) * string) list -> thm -> int -> tactic
+ val forw_inst_tac: Proof.context ->
+ ((indexname * Position.T) * string) list -> thm -> int -> tactic
+ val dres_inst_tac: Proof.context ->
+ ((indexname * Position.T) * string) list -> thm -> int -> tactic
val thin_tac: Proof.context -> string -> int -> tactic
val subgoal_tac: Proof.context -> string -> int -> tactic
end;
@@ -18,14 +23,18 @@
signature RULE_INSTS =
sig
include BASIC_RULE_INSTS
- val where_rule: Proof.context -> (indexname * string) list ->
+ val where_rule: Proof.context ->
+ ((indexname * Position.T) * string) list ->
(binding * string option * mixfix) list -> thm -> thm
val of_rule: Proof.context -> string option list * string option list ->
(binding * string option * mixfix) list -> thm -> thm
- val read_instantiate: Proof.context -> (indexname * string) list -> string list -> thm -> thm
- val instantiate_tac: Proof.context -> (indexname * string) list -> string list -> tactic
+ val read_instantiate: Proof.context ->
+ ((indexname * Position.T) * string) list -> string list -> thm -> thm
+ val instantiate_tac: Proof.context ->
+ ((indexname * Position.T) * string) list -> string list -> tactic
val make_elim_preserve: Proof.context -> thm -> thm
- val method: (Proof.context -> (indexname * string) list -> thm -> int -> tactic) ->
+ val method:
+ (Proof.context -> ((indexname * Position.T) * string) list -> thm -> int -> tactic) ->
(Proof.context -> thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
end;
@@ -34,21 +43,22 @@
(** reading instantiations **)
-val partition_insts = List.partition (fn ((x, _), _) => String.isPrefix "'" x);
+val partition_insts = List.partition (fn (((x, _), _), _) => String.isPrefix "'" x);
+
+fun error_var msg (xi, pos) =
+ error (msg ^ quote (Term.string_of_vname xi) ^ Position.here pos);
local
-fun error_var msg xi = error (msg ^ quote (Term.string_of_vname xi));
-
-fun the_sort tvars (xi: indexname) =
+fun the_sort tvars (xi, pos) : sort =
(case AList.lookup (op =) tvars xi of
SOME S => S
- | NONE => error_var "No such type variable in theorem: " xi);
+ | NONE => error_var "No such type variable in theorem: " (xi, pos));
-fun the_type vars (xi: indexname) =
+fun the_type vars (xi, pos) : typ =
(case AList.lookup (op =) vars xi of
SOME T => T
- | NONE => error_var "No such variable in theorem: " xi);
+ | NONE => error_var "No such variable in theorem: " (xi, pos));
fun instantiate inst =
Term_Subst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
@@ -89,13 +99,13 @@
(* type instantiations *)
- fun readT (xi, s) =
+ fun readT ((xi, pos), s) =
let
- val S = the_sort tvars xi;
+ val S = the_sort tvars (xi, pos);
val T = Syntax.read_typ ctxt s;
in
if Sign.of_sort thy (T, S) then ((xi, S), T)
- else error_var "Incompatible sort for typ instantiation of " xi
+ else error_var "Incompatible sort for typ instantiation of " (xi, pos)
end;
val instT1 = Term_Subst.instantiateT (map readT type_insts);
@@ -110,7 +120,7 @@
val instT2 = Term.typ_subst_TVars inferred;
val vars2 = map (apsnd instT2) vars1;
- val inst2 = instantiate (xs ~~ ts);
+ val inst2 = instantiate (map #1 xs ~~ ts);
(* result *)
@@ -140,7 +150,7 @@
let
fun zip_vars _ [] = []
| zip_vars (_ :: xs) (NONE :: rest) = zip_vars xs rest
- | zip_vars ((x, _) :: xs) (SOME t :: rest) = (x, t) :: zip_vars xs rest
+ | zip_vars ((x, _) :: xs) (SOME t :: rest) = ((x, Position.none), t) :: zip_vars xs rest
| zip_vars [] _ = error "More instantiations than variables in theorem";
val insts =
zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @
@@ -167,9 +177,9 @@
val _ = Theory.setup
(Attrib.setup @{binding "where"}
(Scan.lift
- (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_inner_syntax)) -- Parse.for_fixes) >>
- (fn (insts, fixes) =>
- Thm.rule_attribute (fn context => where_rule (Context.proof_of context) insts fixes)))
+ (Parse.and_list (Parse.position Args.var -- (Args.$$$ "=" |-- Args.name_inner_syntax))
+ -- Parse.for_fixes) >> (fn (insts, fixes) =>
+ Thm.rule_attribute (fn context => where_rule (Context.proof_of context) insts fixes)))
"named instantiation of theorem");
@@ -220,29 +230,29 @@
(* process type insts: Tinsts_env *)
- fun absent xi =
- error ("No such variable in theorem: " ^ Term.string_of_vname xi);
-
val (rtypes, rsorts) = Drule.types_sorts thm;
- fun readT (xi, s) =
+ fun readT ((xi, pos), s) =
let
- val S = (case rsorts xi of SOME S => S | NONE => absent xi);
+ val S =
+ (case rsorts xi of
+ SOME S => S
+ | NONE => error_var "No such type variable in theorem: " (xi, pos));
val T = Syntax.read_typ ctxt' s;
val U = TVar (xi, S);
in
if Sign.typ_instance thy (T, U) then (U, T)
- else error ("Instantiation of " ^ Term.string_of_vname xi ^ " fails")
+ else error_var "Cannot instantiate: " (xi, pos)
end;
val Tinsts_env = map readT Tinsts;
(* preprocess rule: extract vars and their types, apply Tinsts *)
- fun get_typ xi =
+ fun get_typ (xi, pos) =
(case rtypes xi of
SOME T => typ_subst_atomic Tinsts_env T
- | NONE => absent xi);
- val (xis, ss) = Library.split_list tinsts;
+ | NONE => error_var "No such variable in theorem: " (xi, pos) xi);
+ val (xis, ss) = split_list tinsts;
val Ts = map get_typ xis;
val (ts, envT) =
@@ -250,7 +260,7 @@
val envT' =
map (fn (xi, T) => (TVar (xi, the (rsorts xi)), T)) envT @ Tinsts_env;
val cenv =
- map (fn (xi, t) => apply2 (Thm.cterm_of ctxt') (Var (xi, fastype_of t), t))
+ map (fn ((xi, _), t) => apply2 (Thm.cterm_of ctxt') (Var (xi, fastype_of t), t))
(distinct
(fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
(xis ~~ ts));
@@ -312,10 +322,12 @@
(* derived tactics *)
(*deletion of an assumption*)
-fun thin_tac ctxt s = eres_inst_tac ctxt [(("V", 0), s)] Drule.thin_rl;
+fun thin_tac ctxt s =
+ eres_inst_tac ctxt [((("V", 0), Position.none), s)] Drule.thin_rl;
(*Introduce the given proposition as lemma and subgoal*)
-fun subgoal_tac ctxt A = DETERM o res_inst_tac ctxt [(("psi", 0), A)] cut_rl;
+fun subgoal_tac ctxt A =
+ DETERM o res_inst_tac ctxt [((("psi", 0), Position.none), A)] cut_rl;
@@ -324,8 +336,8 @@
fun method inst_tac tac =
Args.goal_spec --
Scan.optional (Scan.lift
- (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_inner_syntax)) --|
- Args.$$$ "in")) [] --
+ (Parse.and_list1 (Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_inner_syntax))
+ --| Args.$$$ "in")) [] --
Attrib.thms >>
(fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts =>
if null insts then quant (Method.insert_tac facts THEN' tac ctxt thms)