# HG changeset patch # User wenzelm # Date 1431894814 -7200 # Node ID adde5ce1e0a735315b514d4bc846754aaaa20eb8 # Parent 410115884a92df9abda11173969addfbf84842c4 updated Eisbach, using version 134bc592909c of its Bitbucket repository; diff -r 410115884a92 -r adde5ce1e0a7 src/HOL/Eisbach/Tests.thy --- a/src/HOL/Eisbach/Tests.thy Sun May 17 21:44:34 2015 +0200 +++ b/src/HOL/Eisbach/Tests.thy Sun May 17 22:33:34 2015 +0200 @@ -458,9 +458,36 @@ done end +subsection \Proper context for method parameters\ + +method add_simp methods m uses f = (match f in H[simp]:_ \ \m\) + +method add_my_thms methods m uses f = (match f in H[my_thms_named]:_ \ \m\) + +method rule_my_thms = (rule my_thms_named) +method rule_my_thms' declares my_thms_named = (rule my_thms_named) + +lemma + assumes A: A and B: B + shows + "(A \ B) \ A \ A \ A" + apply (intro conjI) + apply (add_simp \add_simp \simp\ f: B\ f: A) + apply (add_my_thms \rule_my_thms\ f:A) + apply (add_my_thms \rule_my_thms'\ f:A) + 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) + +lemma True + by (all_args True False \-\ \fail\ f1: TrueI f2: TrueI my_thms_named: TrueI | rule TrueI) subsection \Method name internalization test\ + method test2 = (simp) method simp = fail diff -r 410115884a92 -r adde5ce1e0a7 src/HOL/Eisbach/match_method.ML --- a/src/HOL/Eisbach/match_method.ML Sun May 17 21:44:34 2015 +0200 +++ b/src/HOL/Eisbach/match_method.ML Sun May 17 22:33:34 2015 +0200 @@ -60,9 +60,9 @@ Parse_Tools.parse_term_val Parse.binding; val fixes = - Parse.and_list1 (Scan.repeat1 (Parse.position bound_term) -- + Parse.and_list1 (Scan.repeat1 (Parse.position bound_term) -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.typ) - >> (fn (xs, T) => map (fn (nm, pos) => ((nm, T), pos)) xs)) >> flat; + >> (fn (xs, T) => map (fn (x, pos) => ((x, T), pos)) xs)) >> flat; val for_fixes = Scan.optional (@{keyword "for"} |-- fixes) []; @@ -77,7 +77,7 @@ val parse_match_args = Scan.optional (Args.parens (Parse.enum1 "," - (Args.$$$ "multi" -- Scan.succeed ~1 || Args.$$$ "cut" -- Scan.optional Parse.int 1))) [] >> + (Args.$$$ "multi" -- Scan.succeed ~1 || Args.$$$ "cut" -- Scan.optional Parse.nat 1))) [] >> (fn ss => fold (fn s => fn {multi, cut} => (case s of @@ -87,14 +87,15 @@ fun parse_named_pats match_kind = Args.context :|-- (fn ctxt => - Scan.lift (Parse.and_list1 (Scan.option (dynamic_fact ctxt --| Args.colon) :-- - (fn opt_dyn => - if is_none opt_dyn orelse nameable_match match_kind - then Parse_Tools.name_term -- parse_match_args - else - let val b = #1 (the opt_dyn) - in error ("Cannot bind fact name in term match" ^ Position.here (pos_of b)) end)) - -- for_fixes -- (@{keyword "\"} |-- Parse.token Parse.cartouche)) + Scan.lift (Parse.and_list1 + (Scan.option (dynamic_fact ctxt --| Args.colon) :-- + (fn opt_dyn => + if is_none opt_dyn orelse nameable_match match_kind + then Parse_Tools.name_term -- parse_match_args + else + let val b = #1 (the opt_dyn) + in error ("Cannot bind fact name in term match" ^ Position.here (pos_of b)) end)) + -- for_fixes -- (@{keyword "\"} |-- Parse.token Parse.cartouche)) >> (fn ((ts, fixes), cartouche) => (case Token.get_value cartouche of SOME (Token.Source src) => @@ -249,10 +250,6 @@ end))); -fun parse_match_bodies match_kind = - Parse.enum1' "\" (parse_named_pats match_kind); - - fun dest_internal_fact t = (case try Logic.dest_conjunction t of SOME (params, head) => @@ -799,22 +796,19 @@ end; val match_parser = - parse_match_kind :-- (fn kind => Scan.lift @{keyword "in"} |-- parse_match_bodies kind) >> + parse_match_kind :-- (fn kind => + Scan.lift @{keyword "in"} |-- Parse.enum1' "\" (parse_named_pats kind)) >> (fn (matches, bodies) => fn ctxt => fn using => fn goal => if Method_Closure.is_dummy goal then Seq.empty else let fun exec (pats, fixes, text) goal = let - val ctxt' = fold Variable.declare_term fixes ctxt - |> fold (fn (_, t) => Variable.declare_term t) pats; (*Is this a good idea? We really only care about the maxidx*) - in - real_match using ctxt' fixes matches text pats goal - end; - in - Seq.FIRST (map exec bodies) goal - |> Seq.flat - end); + val ctxt' = + fold Variable.declare_term fixes ctxt + |> fold (fn (_, t) => Variable.declare_term t) pats; (*Is this a good idea? We really only care about the maxidx*) + in real_match using ctxt' fixes matches text pats goal end; + in Seq.flat (Seq.FIRST (map exec bodies) goal) end); val _ = Theory.setup diff -r 410115884a92 -r adde5ce1e0a7 src/HOL/Eisbach/method_closure.ML --- a/src/HOL/Eisbach/method_closure.ML Sun May 17 21:44:34 2015 +0200 +++ b/src/HOL/Eisbach/method_closure.ML Sun May 17 22:33:34 2015 +0200 @@ -25,7 +25,7 @@ val get_inner_method: Proof.context -> string * Position.T -> (term list * (string list * string list)) * Method.text val eval_inner_method: Proof.context -> (term list * string list) * Method.text -> - term list -> (string * thm list) list -> Method.method list -> + term list -> (string * thm list) list -> (Proof.context -> Method.method) list -> Proof.context -> Method.method val method_definition: binding -> (binding * typ option * mixfix) list -> binding list -> binding list -> binding list -> Token.src -> local_theory -> local_theory @@ -53,12 +53,12 @@ structure Local_Data = Proof_Data ( type T = - Method.method Symtab.table * (*dynamic methods*) + (Proof.context -> Method.method) Symtab.table * (*dynamic methods*) (term list -> Proof.context -> Method.method) (*recursive method*); fun init _ : T = (Symtab.empty, fn _ => fn _ => Method.fail); ); -fun lookup_dynamic_method full_name ctxt = +fun lookup_dynamic_method ctxt full_name = (case Symtab.lookup (#1 (Local_Data.get ctxt)) full_name of SOME m => m | NONE => error ("Illegal use of internal Eisbach method: " ^ quote full_name)); @@ -169,10 +169,6 @@ error ("Unexpected inner token value for method cartouche" ^ Position.here (Token.pos_of tok)))); -fun method_evaluate text ctxt : Method.method = fn facts => fn st => - if is_dummy st then Seq.empty - else Method.evaluate text (Config.put Method.closure false ctxt) facts st; - fun parse_term_args args = Args.context :|-- (fn ctxt => @@ -237,20 +233,28 @@ Token.Fact (SOME name, evaluate_dynamic_thm ctxt name) | x => x); +fun method_evaluate text ctxt : Method.method = fn facts => fn st => + let + val ctxt' = Config.put Method.closure false ctxt; + in + if is_dummy st then Seq.empty + else Method.evaluate (evaluate_named_theorems ctxt' text) ctxt' facts st + end; + fun evaluate_method_def fix_env raw_text ctxt = let val text = raw_text - |> instantiate_text fix_env - |> evaluate_named_theorems ctxt; + |> instantiate_text fix_env; in method_evaluate text ctxt end; fun setup_local_method binding lthy = let val full_name = Local_Theory.full_name lthy binding; + fun get_method ctxt = lookup_dynamic_method ctxt full_name ctxt; in lthy - |> update_dynamic_method (full_name, Method.fail) - |> Method.local_setup binding (Scan.succeed (lookup_dynamic_method full_name)) "(internal)" + |> update_dynamic_method (full_name, K Method.fail) + |> Method.local_setup binding (Scan.succeed get_method) "(internal)" end; fun setup_local_fact binding = Named_Theorems.declare binding ""; @@ -271,8 +275,11 @@ fun parse_method_args method_names = let - fun bind_method (name, text) ctxt = - update_dynamic_method (name, method_evaluate text ctxt) ctxt; + fun bind_method (name, text) ctxt = + let + val method = method_evaluate text; + val inner_update = method o update_dynamic_method (name,K (method ctxt)); + in update_dynamic_method (name,inner_update) ctxt end; fun do_parse t = parse_method >> pair t; fun rep [] x = Scan.succeed [] x @@ -341,11 +348,11 @@ fun parser args eval = apfst (Config.put_generic Method.old_section_parser true) #> - (parse_term_args args --| + (parse_term_args args -- + parse_method_args method_names --| (Scan.depend (fn context => Scan.succeed (Context.map_proof (fold empty_named_thm uses_nms) context,())) -- - Method.sections modifiers) -- - parse_method_args method_names >> eval); + Method.sections modifiers) >> eval); val lthy3 = lthy2 |> fold dummy_named_thm named_thms @@ -384,11 +391,11 @@ val _ = Outer_Syntax.local_theory @{command_keyword method} "Eisbach method definition" (Parse.binding -- Parse.for_fixes -- - ((Scan.optional (@{keyword "uses"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) -- - (Scan.optional (@{keyword "declares"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) [])) -- - (Scan.optional (@{keyword "methods"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) -- + ((Scan.optional (@{keyword "methods"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) -- + (Scan.optional (@{keyword "uses"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) [])) -- + (Scan.optional (@{keyword "declares"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) -- Parse.!!! (@{keyword "="} |-- (Parse.position (Parse.args1 (K true)) >> (fn (args, pos) => Token.src ("", pos) args))) - >> (fn ((((name, vars), (uses, attribs)), methods), source) => + >> (fn ((((name, vars), (methods, uses)), attribs), source) => method_definition_cmd name vars uses attribs methods source)); end;