# HG changeset patch # User wenzelm # Date 1450884795 -3600 # Node ID 0f9e0106c3786605405096b52e0649e91972e11c # Parent 35ec3757d3c16230744d81b0d9707331a9fffcc6 tuned module arrangement; diff -r 35ec3757d3c1 -r 0f9e0106c378 src/HOL/Eisbach/Eisbach.thy --- a/src/HOL/Eisbach/Eisbach.thy Wed Dec 23 14:40:18 2015 +0100 +++ b/src/HOL/Eisbach/Eisbach.thy Wed Dec 23 16:33:15 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 35ec3757d3c1 -r 0f9e0106c378 src/HOL/Eisbach/eisbach_antiquotations.ML --- a/src/HOL/Eisbach/eisbach_antiquotations.ML Wed Dec 23 14:40:18 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 35ec3757d3c1 -r 0f9e0106c378 src/HOL/Eisbach/method_closure.ML --- a/src/HOL/Eisbach/method_closure.ML Wed Dec 23 14:40:18 2015 +0100 +++ b/src/HOL/Eisbach/method_closure.ML Wed Dec 23 16:33:15 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 -> @@ -39,8 +39,27 @@ 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)))); structure Local_Data = Proof_Data @@ -84,7 +103,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 @@ -96,42 +114,6 @@ in text end)); -fun parse_term_args args = - Args.context :|-- (fn ctxt => - let - val ctxt' = Proof_Context.set_mode (Proof_Context.mode_schematic) ctxt; - - fun parse T = - (if T = propT then Syntax.parse_prop ctxt' else Syntax.parse_term ctxt') - #> Type.constraint (Type_Infer.paramify_vars T); - - fun do_parse' T = - Parse_Tools.name_term >> Parse_Tools.parse_val_cases (parse T); - - fun do_parse (Var (_, T)) = do_parse' T - | do_parse (Free (_, T)) = do_parse' T - | do_parse t = error ("Unexpected method parameter: " ^ Syntax.string_of_term ctxt' t); - - fun rep [] x = Scan.succeed [] x - | rep (t :: ts) x = (do_parse t ::: rep ts) x; - - fun check ts = - let - val (ts, fs) = split_list ts; - val ts' = Syntax.check_terms ctxt' ts |> Variable.polymorphic ctxt'; - val _ = ListPair.app (fn (f, t) => f t) (fs, ts'); - 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 check_attrib ctxt attrib = let val name = Binding.name_of attrib; @@ -189,53 +171,47 @@ 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 parse_term_args args = + Args.context :|-- (fn ctxt => + let + val ctxt' = Proof_Context.set_mode (Proof_Context.mode_schematic) ctxt; + + fun parse T = + (if T = propT then Syntax.parse_prop ctxt' else Syntax.parse_term ctxt') + #> Type.constraint (Type_Infer.paramify_vars T); + + fun do_parse' T = + Parse_Tools.name_term >> Parse_Tools.parse_val_cases (parse T); + + fun do_parse (Var (_, T)) = do_parse' T + | do_parse (Free (_, T)) = do_parse' T + | do_parse t = error ("Unexpected method parameter: " ^ Syntax.string_of_term ctxt' t); + + fun rep [] x = Scan.succeed [] x + | rep (t :: ts) x = (do_parse t ::: rep ts) x; + + fun check ts = + let + val (ts, fs) = split_list ts; + val ts' = Syntax.check_terms ctxt' ts |> Variable.polymorphic ctxt'; + val _ = ListPair.app (fn (f, t) => f t) (fs, ts'); + 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 gen_method add_fixes name vars uses declares methods source lthy = let val (uses_internal, lthy1) = lthy @@ -309,4 +285,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;