# HG changeset patch # User wenzelm # Date 1450885411 -3600 # Node ID 0df21d79fe3230fdce8dbeefc330765f94cafe1e # Parent 7950ae6d326667c420489f0876ebc5b47ab2ea79# Parent b3d68dff610b9b4156a06bec183685f5aeee5785 merged diff -r 7950ae6d3266 -r 0df21d79fe32 src/HOL/Eisbach/Eisbach.thy --- a/src/HOL/Eisbach/Eisbach.thy Wed Dec 23 14:36:45 2015 +0100 +++ b/src/HOL/Eisbach/Eisbach.thy Wed Dec 23 16:43:31 2015 +0100 @@ -19,7 +19,6 @@ ML_file "method_closure.ML" ML_file "eisbach_rule_insts.ML" ML_file "match_method.ML" -ML_file "eisbach_antiquotations.ML" method solves methods m = (m; fail) diff -r 7950ae6d3266 -r 0df21d79fe32 src/HOL/Eisbach/eisbach_antiquotations.ML --- a/src/HOL/Eisbach/eisbach_antiquotations.ML Wed Dec 23 14:36:45 2015 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,54 +0,0 @@ -(* Title: HOL/Eisbach/eisbach_antiquotations.ML - Author: Daniel Matichuk, NICTA/UNSW - -ML antiquotations for Eisbach. -*) - -structure Eisbach_Antiquotations: sig end = -struct - -(** evaluate Eisbach method from ML **) - -val _ = - Theory.setup - (ML_Antiquotation.inline @{binding method} (* FIXME ML_Antiquotation.value (!?) *) - (Args.context -- Scan.lift (Args.mode "drop_cases") -- Scan.lift (Parse.position Parse.name) - >> (fn ((ctxt, drop_cases), nameref) => - let - val ((targs, (factargs, margs)), _) = Method_Closure.get_method ctxt nameref; - - val has_factargs = not (null factargs); - - val (targnms, ctxt') = - fold_map (fn (Var ((x, _), _)) => ML_Context.variant x) targs ctxt; - val (margnms, ctxt'') = fold_map ML_Context.variant margs ctxt'; - val (factsnm, _) = ML_Context.variant "facts" ctxt''; - - val fn_header = - margnms - |> has_factargs ? append [factsnm] - |> append targnms - |> map (fn nm => "fn " ^ nm ^ " => ") - |> implode; - - val ML_context = ML_Context.struct_name ctxt ^ ".ML_context"; - val ml_inner = - ML_Syntax.atomic - ("Method_Closure.get_method " ^ ML_context ^ - ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position nameref ^ - "|> (fn ((targs, (_, margs)), text) => Method_Closure.eval_method " ^ - ML_context ^ " ((targs, margs), text))"); - - val drop_cases_suffix = - if drop_cases then "#> (fn f => (fn ctxt => fn thms => f ctxt thms |> Seq.map snd))" - else ""; - - val factsnm = if has_factargs then factsnm else "[]"; - in - ML_Syntax.atomic - (fn_header ^ ml_inner ^ " " ^ ML_Syntax.print_list I targnms ^ " " ^ - factsnm ^ " " ^ - ML_Syntax.print_list I margnms ^ drop_cases_suffix) - end))); - -end; diff -r 7950ae6d3266 -r 0df21d79fe32 src/HOL/Eisbach/method_closure.ML --- a/src/HOL/Eisbach/method_closure.ML Wed Dec 23 14:36:45 2015 +0100 +++ b/src/HOL/Eisbach/method_closure.ML Wed Dec 23 16:43:31 2015 +0100 @@ -10,16 +10,16 @@ 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 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 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,7 +29,7 @@ structure Method_Closure: METHOD_CLOSURE = struct -(* context data *) +(* context data for ML antiquotation *) structure Data = Generic_Data ( @@ -39,9 +39,30 @@ fun merge data : T = Symtab.merge (K true) data; ); -val get_methods = Data.get o Context.Proof; -val map_methods = Data.map; +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 ( @@ -65,16 +86,12 @@ (* read method text *) fun read ctxt src = - let - val parser = - Parse.!!! (Method.parser 0 --| Scan.ahead Parse.eof) - >> apfst (Method.check_text ctxt); - in - (case Scan.read Token.stopper parser src of - SOME (text, range) => (Method.report (text, range); text) - | NONE => - error ("Failed to parse method" ^ Position.here (Position.set_range (Token.range_of src)))) - end; + (case Scan.read Token.stopper (Parse.!!! (Method.parser 0 --| Scan.ahead Parse.eof)) src of + SOME (text, range) => + if Method.checked_text text then text + else (Method.report (text, range); Method.check_text ctxt text) + | NONE => + error ("Failed to parse method" ^ Position.here (Position.set_range (Token.range_of src)))); fun read_closure ctxt src0 = let @@ -88,7 +105,6 @@ Token.read_no_commands (Thy_Header.get_keywords' ctxt) (Scan.one Token.not_eof) #> read_closure ctxt; - val method_text = Args.context -- Scan.lift (Parse.token Parse.text) >> (fn (ctxt, tok) => (case Token.get_value tok of @@ -100,6 +116,57 @@ in text end)); +(* evaluate method text *) + +fun method_evaluate text ctxt = + let + val text' = + text |> (Method.map_source o map o Token.map_facts) + (fn SOME name => + (case Proof_Context.lookup_fact ctxt name of + SOME (false, ths) => K ths + | _ => I) + | NONE => I); + 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 = + let + 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; + + + +(** Isar command **) + +local + +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, K Method.fail) + |> Method.local_setup binding (Scan.succeed get_method) "(internal)" + end; + +fun check_attrib ctxt attrib = + let + val name = Binding.name_of attrib; + val pos = Binding.pos_of attrib; + val named_thm = Named_Theorems.check ctxt (name, 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; + +fun dummy_named_thm named_thm = + Context.proof_map + (Named_Theorems.clear named_thm + #> Named_Theorems.add_thm named_thm Drule.free_dummy_thm); + fun parse_term_args args = Args.context :|-- (fn ctxt => let @@ -136,50 +203,6 @@ (map Term.dest_Var args ~~ ts) Vartab.empty; in Envir.Envir {maxidx = ~1, tenv = tenv, tyenv = tyenv} end; -fun check_attrib ctxt attrib = - let - val name = Binding.name_of attrib; - val pos = Binding.pos_of attrib; - val named_thm = Named_Theorems.check ctxt (name, 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; - - -fun method_evaluate text ctxt = - let - val text' = - text |> (Method.map_source o map o Token.map_facts) - (fn SOME name => - (case Proof_Context.lookup_fact ctxt name of - SOME (false, ths) => K ths - | _ => I) - | NONE => I); - 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 = - let - 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; - -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, K Method.fail) - |> Method.local_setup binding (Scan.succeed get_method) "(internal)" - end; - -fun dummy_named_thm named_thm = - Context.proof_map - (Named_Theorems.clear named_thm - #> Named_Theorems.add_thm named_thm Drule.free_dummy_thm); - fun parse_method_args method_names = let fun bind_method (name, text) ctxt = @@ -192,54 +215,6 @@ | rep (t :: ts) x = ((method_text >> pair t) ::: rep ts) x; in rep method_names >> fold bind_method 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 => - map_methods - (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)))); - -fun get_method ctxt (xname, pos) = - let - val name = Method.check_name ctxt (xname, pos); - in - (case Symtab.lookup (get_methods ctxt) name of - SOME entry => entry - | NONE => error ("Unknown Eisbach method: " ^ quote name ^ Position.here pos)) - end; - -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; - - - -(** Isar command **) - -local - fun gen_method add_fixes name vars uses declares methods source lthy = let val (uses_internal, lthy1) = lthy @@ -313,4 +288,69 @@ (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; + +val _ = + Theory.setup + (ML_Antiquotation.inline @{binding method} (* FIXME ML_Antiquotation.value (!?) *) + (Args.context -- Scan.lift (Args.mode "drop_cases") -- Scan.lift (Parse.position Parse.name) + >> (fn ((ctxt, drop_cases), nameref) => + let + val ((targs, (factargs, margs)), _) = get_method ctxt nameref; + + val has_factargs = not (null factargs); + + val (targnms, ctxt') = + fold_map (fn (Var ((x, _), _)) => ML_Context.variant x) targs ctxt; + val (margnms, ctxt'') = fold_map ML_Context.variant margs ctxt'; + val (factsnm, _) = ML_Context.variant "facts" ctxt''; + + val fn_header = + margnms + |> has_factargs ? append [factsnm] + |> append targnms + |> map (fn nm => "fn " ^ nm ^ " => ") + |> implode; + + val ML_context = ML_Context.struct_name ctxt ^ ".ML_context"; + val ml_inner = + ML_Syntax.atomic + ("Method_Closure.get_method " ^ ML_context ^ + ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position nameref ^ + "|> (fn ((targs, (_, margs)), text) => Method_Closure.eval_method " ^ + ML_context ^ " ((targs, margs), text))"); + + val drop_cases_suffix = + if drop_cases then "#> (fn f => (fn ctxt => fn thms => f ctxt thms |> Seq.map snd))" + else ""; + + val factsnm = if has_factargs then factsnm else "[]"; + in + ML_Syntax.atomic + (fn_header ^ ml_inner ^ " " ^ ML_Syntax.print_list I targnms ^ " " ^ + factsnm ^ " " ^ + ML_Syntax.print_list I margnms ^ drop_cases_suffix) + end))); + end; diff -r 7950ae6d3266 -r 0df21d79fe32 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Wed Dec 23 14:36:45 2015 +0100 +++ b/src/Pure/Isar/method.ML Wed Dec 23 16:43:31 2015 +0100 @@ -73,6 +73,7 @@ val check_name: Proof.context -> xstring * Position.T -> string val check_src: Proof.context -> Token.src -> Token.src val check_text: Proof.context -> text -> text + val checked_text: text -> bool val method_syntax: (Proof.context -> method) context_parser -> Token.src -> Proof.context -> method val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory @@ -439,6 +440,10 @@ | check_text _ (Basic m) = Basic m | check_text ctxt (Combinator (x, y, body)) = Combinator (x, y, map (check_text ctxt) body); +fun checked_text (Source src) = Token.checked_src src + | checked_text (Basic _) = true + | checked_text (Combinator (_, _, body)) = forall checked_text body; + (* method setup *)