more realistic Eisbach method invocation from ML;
misc tuning and clarification;

--- a/src/HOL/Eisbach/Tests.thy	Tue Jan 05 17:20:56 2016 +0100
+++ b/src/HOL/Eisbach/Tests.thy	Tue Jan 05 21:55:34 2016 +0100
@@ -478,6 +478,7 @@
   apply (add_my_thms \<open>rule my_thms_named\<close> f:A)
   done
 
+
 subsection \<open>Shallow parser tests\<close>
 
 method all_args for A B methods m1 m2 uses f1 f2 declares my_thms_named = fail
@@ -485,6 +486,7 @@
 lemma True
   by (all_args True False - fail f1: TrueI f2: TrueI my_thms_named: TrueI | rule TrueI)
 
+
 subsection \<open>Method name internalization test\<close>
 
 
@@ -494,4 +496,25 @@
 
 lemma "A \<Longrightarrow> A" by test2
 
+
+subsection \<open>Eisbach method invocation from ML\<close>
+
+method test_method for x y uses r = (print_term x, print_term y, rule r)
+
+method_setup test_method' = \<open>
+  Args.term -- Args.term --
+  (Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms) >>
+    (fn ((x, y), r) => fn ctxt =>
+      Method_Closure.apply_method ctxt "Tests.test_method" [x, y] [r] [] ctxt);
+\<close>
+
+lemma
+  fixes a b :: nat
+  assumes "a = b"
+  shows "b = a"
+  apply (test_method a b)?
+  apply (test_method' a b rule: refl)?
+  apply (test_method' a b rule: assms [symmetric])?
+  done
+
 end

--- a/src/HOL/Eisbach/method_closure.ML	Tue Jan 05 17:20:56 2016 +0100
+++ b/src/HOL/Eisbach/method_closure.ML	Tue Jan 05 21:55:34 2016 +0100
@@ -10,16 +10,13 @@
 
 signature METHOD_CLOSURE =
 sig
-  val get_method: Proof.context -> string * Position.T ->
-    (term list * (string list * string list)) * Method.text
-  val eval_method: Proof.context -> (term list * string list) * Method.text ->
-    term list -> (string * thm list) list -> (Proof.context -> Method.method) list ->
-    Proof.context -> Method.method
   val read: Proof.context -> Token.src -> Method.text
   val read_closure: Proof.context -> Token.src -> Method.text * Token.src
   val read_closure_input: Proof.context -> Input.source -> Method.text * Token.src
   val method_text: Method.text context_parser
   val method_evaluate: Method.text -> Proof.context -> Method.method
+  val apply_method: Proof.context -> string -> term list -> thm list list ->
+    (Proof.context -> Method.method) list -> Proof.context -> thm list -> context_tactic
   val method: binding -> (binding * typ option * mixfix) list -> binding list ->
     binding list -> binding list -> Token.src -> local_theory -> string * local_theory
   val method_cmd: binding -> (binding * string option * mixfix) list -> binding list ->
@@ -29,42 +26,9 @@
 structure Method_Closure: METHOD_CLOSURE =
 struct
 
-(* context data for ML antiquotation *)
-
-structure Data = Generic_Data
-(
-  type T = ((term list * (string list * string list)) * Method.text) Symtab.table;
-  val empty: T = Symtab.empty;
-  val extend = I;
-  fun merge data : T = Symtab.merge (K true) data;
-);
+(* auxiliary data for method definition *)
 
-fun get_method ctxt (xname, pos) =
-  let
-    val name = Method.check_name ctxt (xname, pos);
-  in
-    (case Symtab.lookup (Data.get (Context.Proof ctxt)) name of
-      SOME entry => entry
-    | NONE => error ("Unknown Eisbach method: " ^ quote name ^ Position.here pos))
-  end;
-
-(* FIXME redundant!? -- base name of binding is not changed by usual morphisms*)
-fun Morphism_name phi name =
-  Morphism.binding phi (Binding.make (name, Position.none)) |> Binding.name_of;
-
-fun add_method binding ((fixes, declares, methods), text) lthy =
-  lthy |>
-  Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
-    Data.map
-      (Symtab.update (Local_Theory.full_name lthy binding,
-        (((map (Morphism.term phi) fixes),
-          (map (Morphism_name phi) declares, map (Morphism_name phi) methods)),
-          (Method.map_source o map) (Token.transform phi) text))));
-
-
-(* context data for method definition *)
-
-structure Local_Data = Proof_Data
+structure Method_Definition = Proof_Data
 (
   type T =
     (Proof.context -> Method.method) Symtab.table *  (*dynamic methods*)
@@ -73,14 +37,45 @@
 );
 
 fun lookup_dynamic_method ctxt full_name =
-  (case Symtab.lookup (#1 (Local_Data.get ctxt)) full_name of
+  (case Symtab.lookup (#1 (Method_Definition.get ctxt)) full_name of
     SOME m => m
   | NONE => error ("Illegal use of internal Eisbach method: " ^ quote full_name));
 
-val update_dynamic_method = Local_Data.map o apfst o Symtab.update;
+val update_dynamic_method = Method_Definition.map o apfst o Symtab.update;
+
+val get_recursive_method = #2 o Method_Definition.get;
+val put_recursive_method = Method_Definition.map o apsnd o K;
+
+
+(* stored method closures *)
+
+type closure = {vars: term list, named_thms: string list, methods: string list, body: Method.text};
+
+structure Data = Generic_Data
+(
+  type T = closure Symtab.table;
+  val empty: T = Symtab.empty;
+  val extend = I;
+  fun merge data : T = Symtab.merge (K true) data;
+);
 
-val get_recursive_method = #2 o Local_Data.get;
-val put_recursive_method = Local_Data.map o apsnd o K;
+fun get_closure ctxt name =
+  (case Symtab.lookup (Data.get (Context.Proof ctxt)) name of
+    SOME closure => closure
+  | NONE => error ("Unknown Eisbach method: " ^ quote name));
+
+fun put_closure binding (closure: closure) lthy =
+  let
+    val name = Local_Theory.full_name lthy binding;
+  in
+    lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
+      Data.map
+        (Symtab.update (name,
+          {vars = map (Morphism.term phi) (#vars closure),
+           named_thms = #named_thms closure,
+           methods = #methods closure,
+           body = (Method.map_source o map) (Token.transform phi) (#body closure)})))
+  end;
 
 
 (* read method text *)
@@ -130,15 +125,50 @@
     val ctxt' = Config.put Method.closure false ctxt;
   in fn facts => Method.RUNTIME (fn st => Method.evaluate text' ctxt' facts st) end;
 
-fun method_instantiate env text =
+
+
+(** apply method closure **)
+
+local
+
+fun method_instantiate vars body ts ctxt =
   let
+    val match_types = Sign.typ_match (Proof_Context.theory_of ctxt) o apply2 Term.type_of;
+    val tyenv = fold match_types (vars ~~ ts) Vartab.empty;
+    val tenv =
+      fold (fn ((xi, T), t) => Vartab.update_new (xi, (T, t)))
+        (map Term.dest_Var vars ~~ ts) Vartab.empty;
+    val env = Envir.Envir {maxidx = ~1, tenv = tenv, tyenv = tyenv};
+
     val morphism = Morphism.term_morphism "method_instantiate" (Envir.norm_term env);
-    val text' = (Method.map_source o map) (Token.transform morphism) text;
-  in method_evaluate text' end;
+    val body' = (Method.map_source o map) (Token.transform morphism) body;
+  in method_evaluate body' ctxt end;
+
+in
+
+fun recursive_method vars body ts =
+  let val m = method_instantiate vars body
+  in put_recursive_method m #> m ts end;
+
+fun apply_method ctxt method_name terms facts methods =
+  let
+    fun declare_facts (name :: names) (fact :: facts) =
+          fold (Context.proof_map o Named_Theorems.add_thm name) fact
+          #> declare_facts names facts
+      | declare_facts _ [] = I
+      | declare_facts [] (_ :: _) = error ("Excessive facts for method " ^ quote method_name);
+    val {vars, named_thms, methods = method_args, body} = get_closure ctxt method_name;
+  in
+    declare_facts named_thms facts
+    #> fold update_dynamic_method (method_args ~~ methods)
+    #> recursive_method vars body terms
+  end;
+
+end;
 
 
 
-(** Isar command **)
+(** define method closure **)
 
 local
 
@@ -152,15 +182,15 @@
     |> Method.local_setup binding (Scan.succeed get_method) "(internal)"
   end;
 
-fun check_attrib ctxt attrib =
+fun check_named_thm ctxt binding =
   let
-    val name = Binding.name_of attrib;
-    val pos = Binding.pos_of attrib;
-    val named_thm = Named_Theorems.check ctxt (name, pos);
+    val bname = Binding.name_of binding;
+    val pos = Binding.pos_of binding;
+    val full_name = Named_Theorems.check ctxt (bname, pos);
     val parser: Method.modifier parser =
-      Args.$$$ name -- Args.colon >>
-        K {init = I, attribute = Named_Theorems.add named_thm, pos = pos};
-  in (named_thm, parser) end;
+      Args.$$$ bname -- Args.colon
+        >> K {init = I, attribute = Named_Theorems.add full_name, pos = pos};
+  in (full_name, parser) end;
 
 fun dummy_named_thm named_thm =
   Context.proof_map
@@ -194,16 +224,7 @@
         in ts' end;
     in Scan.lift (rep args) >> check end);
 
-fun match_term_args ctxt args ts =
-  let
-    val match_types = Sign.typ_match (Proof_Context.theory_of ctxt) o apply2 Term.fastype_of;
-    val tyenv = fold match_types (args ~~ ts) Vartab.empty;
-    val tenv =
-      fold (fn ((xi, T), t) => Vartab.update_new (xi, (T, t)))
-        (map Term.dest_Var args ~~ ts) Vartab.empty;
-  in Envir.Envir {maxidx = ~1, tenv = tenv, tyenv = tyenv} end;
-
-fun parse_method_args method_names =
+fun parse_method_args method_args =
   let
     fun bind_method (name, text) ctxt =
       let
@@ -212,8 +233,8 @@
       in update_dynamic_method (name, inner_update) ctxt end;
 
     fun rep [] x = Scan.succeed [] x
-      | rep (t :: ts) x = ((method_text >> pair t) ::: rep ts) x;
-  in rep method_names >> fold bind_method end;
+      | rep (m :: ms) x = ((method_text >> pair m) ::: rep ms) x;
+  in rep method_args >> fold bind_method end;
 
 fun gen_method add_fixes name vars uses declares methods source lthy =
   let
@@ -228,13 +249,14 @@
     val (term_args, lthy2) = lthy1
       |> add_fixes vars |-> fold_map Proof_Context.inferred_param |>> map Free;
 
-    val (named_thms, modifiers) = map (check_attrib lthy2) (declares @ uses) |> split_list;
-    val method_names = map (Local_Theory.full_name lthy2) methods;
+    val (named_thms, modifiers) = map (check_named_thm lthy2) (declares @ uses) |> split_list;
+
+    val method_args = map (Local_Theory.full_name lthy2) methods;
 
     fun parser args =
       apfst (Config.put_generic Method.old_section_parser true) #>
       (parse_term_args args --
-        parse_method_args method_names --|
+        parse_method_args method_args --|
         (Scan.depend (fn context =>
           Scan.succeed (fold Named_Theorems.clear uses_internal context, ())) --
          Method.sections modifiers));
@@ -256,18 +278,15 @@
 
     val text' = (Method.map_source o map) (Token.transform morphism) text;
     val term_args' = map (Morphism.term morphism) term_args;
-
-    fun real_exec ts ctxt =
-      method_instantiate (match_term_args ctxt term_args' ts) text' ctxt;
-    val real_parser =
-      parser term_args' >> (fn (fixes, decl) => fn ctxt =>
-        real_exec fixes (put_recursive_method real_exec (decl ctxt)));
   in
     lthy3
     |> Local_Theory.close_target
     |> Proof_Context.restore_naming lthy
-    |> Method.local_setup name real_parser "(defined in Eisbach)"
-    |> add_method name ((term_args', named_thms, method_names), text')
+    |> put_closure name
+        {vars = term_args', named_thms = named_thms, methods = method_args, body = text'}
+    |> Method.local_setup name
+        (parser term_args' >> (fn (ts, decl) => decl #> recursive_method term_args' text' ts))
+        "(defined in Eisbach)"
     |> pair (Local_Theory.full_name lthy name)
   end;
 
@@ -288,27 +307,4 @@
       (fn ((((name, vars), (methods, uses)), declares), src) =>
         #2 o method_cmd name vars uses declares methods src));
 
-
-
-(** ML antiquotation **)
-
-fun eval_method ctxt0 header fixes attribs methods =
-  let
-    val ((term_args, hmethods), text) = header;
-
-    fun match fixes = (* FIXME proper context!? *)
-      (case Seq.pull (Unify.matchers (Context.Proof ctxt0) (term_args ~~ fixes)) of
-        SOME (env, _) => env
-      | NONE => error "Couldn't match term arguments");
-
-    fun add_thms (name, thms) =
-      fold (Context.proof_map o Named_Theorems.add_thm name) thms;
-
-    val setup_ctxt = fold add_thms attribs
-      #> fold update_dynamic_method (hmethods ~~ methods)
-      #> put_recursive_method (fn xs => method_instantiate (match xs) text);
-  in
-    fn ctxt => method_instantiate (match fixes) text (setup_ctxt ctxt)
-  end;
-
 end;