# HG changeset patch # User wenzelm # Date 1452027334 -3600 # Node ID b13b98a4d5f86cd58df1044f84fee714404c63a3 # Parent 28acb93a745f8dc27fd536d527d838746d5dc353 more realistic Eisbach method invocation from ML; misc tuning and clarification; diff -r 28acb93a745f -r b13b98a4d5f8 src/HOL/Eisbach/Tests.thy --- 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 \rule my_thms_named\ f:A) done + subsection \Shallow parser tests\ 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 \Method name internalization test\ @@ -494,4 +496,25 @@ lemma "A \ A" by test2 + +subsection \Eisbach method invocation from ML\ + +method test_method for x y uses r = (print_term x, print_term y, rule r) + +method_setup test_method' = \ + 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); +\ + +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 diff -r 28acb93a745f -r b13b98a4d5f8 src/HOL/Eisbach/method_closure.ML --- 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;