src/HOL/Eisbach/method_closure.ML
author wenzelm
Fri Oct 27 13:50:08 2017 +0200 (23 months ago)
changeset 66924 b4d4027f743b
parent 63527 59eff6e56d81
child 69593 3dda49e08b9d
permissions -rw-r--r--
more permissive;
     1 (*  Title:      HOL/Eisbach/method_closure.ML
     2     Author:     Daniel Matichuk, NICTA/UNSW
     3 
     4 Facilities for treating method syntax as a closure, with abstraction
     5 over terms, facts and other methods.
     6 
     7 The 'method' command allows to define new proof methods by combining
     8 existing ones with their usual syntax.
     9 *)
    10 
    11 signature METHOD_CLOSURE =
    12 sig
    13   val apply_method: Proof.context -> string -> term list -> thm list list ->
    14     (Proof.context -> Method.method) list -> Proof.context -> thm list -> context_tactic
    15   val method: binding -> (binding * typ option * mixfix) list -> binding list ->
    16     binding list -> binding list -> Token.src -> local_theory -> string * local_theory
    17   val method_cmd: binding -> (binding * string option * mixfix) list -> binding list ->
    18     binding list -> binding list -> Token.src -> local_theory -> string * local_theory
    19 end;
    20 
    21 structure Method_Closure: METHOD_CLOSURE =
    22 struct
    23 
    24 (* auxiliary data for method definition *)
    25 
    26 structure Method_Definition = Proof_Data
    27 (
    28   type T =
    29     (Proof.context -> Method.method) Symtab.table *  (*dynamic methods*)
    30     (term list -> Proof.context -> Method.method) Symtab.table  (*recursive methods*);
    31   fun init _ : T = (Symtab.empty, Symtab.empty);
    32 );
    33 
    34 fun lookup_dynamic_method ctxt full_name =
    35   (case Symtab.lookup (#1 (Method_Definition.get ctxt)) full_name of
    36     SOME m => m ctxt
    37   | NONE => error ("Illegal use of internal Eisbach method: " ^ quote full_name));
    38 
    39 val update_dynamic_method = Method_Definition.map o apfst o Symtab.update;
    40 
    41 fun get_recursive_method full_name ts ctxt =
    42   (case Symtab.lookup (#2 (Method_Definition.get ctxt)) full_name of
    43     SOME m => m ts ctxt
    44   | NONE => error ("Illegal use of internal Eisbach method: " ^ quote full_name));
    45 
    46 val put_recursive_method = Method_Definition.map o apsnd o Symtab.update;
    47 
    48 
    49 (* stored method closures *)
    50 
    51 type closure = {vars: term list, named_thms: string list, methods: string list, body: Method.text};
    52 
    53 structure Data = Generic_Data
    54 (
    55   type T = closure Symtab.table;
    56   val empty: T = Symtab.empty;
    57   val extend = I;
    58   fun merge data : T = Symtab.merge (K true) data;
    59 );
    60 
    61 fun get_closure ctxt name =
    62   (case Symtab.lookup (Data.get (Context.Proof ctxt)) name of
    63     SOME closure => closure
    64   | NONE => error ("Unknown Eisbach method: " ^ quote name));
    65 
    66 fun put_closure binding (closure: closure) lthy =
    67   let
    68     val name = Local_Theory.full_name lthy binding;
    69   in
    70     lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
    71       Data.map
    72         (Symtab.update (name,
    73           {vars = map (Morphism.term phi) (#vars closure),
    74            named_thms = #named_thms closure,
    75            methods = #methods closure,
    76            body = (Method.map_source o map) (Token.transform phi) (#body closure)})))
    77   end;
    78 
    79 
    80 (* instantiate and evaluate method text *)
    81 
    82 fun method_instantiate vars body ts ctxt =
    83   let
    84     val thy = Proof_Context.theory_of ctxt;
    85     val subst = fold (Pattern.match thy) (vars ~~ ts) (Vartab.empty, Vartab.empty);
    86     val morphism = Morphism.term_morphism "method_instantiate" (Envir.subst_term subst);
    87     val body' = (Method.map_source o map) (Token.transform morphism) body;
    88   in Method.evaluate_runtime body' ctxt end;
    89 
    90 
    91 
    92 (** apply method closure **)
    93 
    94 fun recursive_method full_name vars body ts =
    95   let val m = method_instantiate vars body
    96   in put_recursive_method (full_name, m) #> m ts end;
    97 
    98 fun apply_method ctxt method_name terms facts methods =
    99   let
   100     fun declare_facts (name :: names) (fact :: facts) =
   101           fold (Context.proof_map o Named_Theorems.add_thm name) fact
   102           #> declare_facts names facts
   103       | declare_facts _ [] = I
   104       | declare_facts [] (_ :: _) = error ("Excessive facts for method " ^ quote method_name);
   105     val {vars, named_thms, methods = method_args, body} = get_closure ctxt method_name;
   106   in
   107     declare_facts named_thms facts
   108     #> fold update_dynamic_method (method_args ~~ methods)
   109     #> recursive_method method_name vars body terms
   110   end;
   111 
   112 
   113 
   114 (** define method closure **)
   115 
   116 local
   117 
   118 fun setup_local_method binding lthy =
   119   let
   120     val full_name = Local_Theory.full_name lthy binding;
   121     fun dynamic_method ctxt = lookup_dynamic_method ctxt full_name;
   122   in
   123     lthy
   124     |> update_dynamic_method (full_name, K Method.fail)
   125     |> Method.local_setup binding (Scan.succeed dynamic_method) "(internal)"
   126   end;
   127 
   128 fun check_named_thm ctxt binding =
   129   let
   130     val bname = Binding.name_of binding;
   131     val pos = Binding.pos_of binding;
   132     val full_name = Named_Theorems.check ctxt (bname, pos);
   133     val parser: Method.modifier parser =
   134       Args.$$$ bname -- Args.colon
   135         >> K {init = I, attribute = Named_Theorems.add full_name, pos = pos};
   136   in (full_name, parser) end;
   137 
   138 fun parse_term_args args =
   139   Args.context :|-- (fn ctxt =>
   140     let
   141       val ctxt' = Proof_Context.set_mode (Proof_Context.mode_schematic) ctxt;
   142 
   143       fun parse T =
   144         (if T = propT then Syntax.parse_prop ctxt' else Syntax.parse_term ctxt')
   145         #> Type.constraint (Type_Infer.paramify_vars T);
   146 
   147       fun do_parse' T =
   148         Parse_Tools.name_term >> Parse_Tools.parse_val_cases (parse T);
   149 
   150       fun do_parse (Var (_, T)) = do_parse' T
   151         | do_parse (Free (_, T)) = do_parse' T
   152         | do_parse t = error ("Unexpected method parameter: " ^ Syntax.string_of_term ctxt' t);
   153 
   154        fun rep [] x = Scan.succeed [] x
   155          | rep (t :: ts) x  = (do_parse t ::: rep ts) x;
   156 
   157       fun check ts =
   158         let
   159           val (ts, fs) = split_list ts;
   160           val ts' = Syntax.check_terms ctxt' ts |> Variable.polymorphic ctxt';
   161           val _ = ListPair.app (fn (f, t) => f t) (fs, ts');
   162         in ts' end;
   163     in Scan.lift (rep args) >> check end);
   164 
   165 fun parse_method_args method_args =
   166   let
   167     fun bind_method (name, text) ctxt =
   168       let
   169         val method = Method.evaluate_runtime text;
   170         val inner_update = method o update_dynamic_method (name, K (method ctxt));
   171       in update_dynamic_method (name, inner_update) ctxt end;
   172 
   173     fun rep [] x = Scan.succeed [] x
   174       | rep (m :: ms) x = ((Method.text_closure >> pair m) ::: rep ms) x;
   175   in rep method_args >> fold bind_method end;
   176 
   177 fun gen_method add_fixes name vars uses declares methods source lthy =
   178   let
   179     val (uses_internal, lthy1) = lthy
   180       |> Proof_Context.concealed
   181       |> Local_Theory.open_target |-> Proof_Context.private_scope
   182       |> Local_Theory.map_background_naming (Name_Space.add_path (Binding.name_of name))
   183       |> Config.put Method.old_section_parser true
   184       |> fold setup_local_method methods
   185       |> fold_map (fn b => Named_Theorems.declare b "") uses;
   186 
   187     val (term_args, lthy2) = lthy1
   188       |> add_fixes vars |-> fold_map Proof_Context.inferred_param |>> map Free;
   189 
   190     val (named_thms, modifiers) = map (check_named_thm lthy2) (declares @ uses) |> split_list;
   191 
   192     val method_args = map (Local_Theory.full_name lthy2) methods;
   193 
   194     fun parser args meth =
   195       apfst (Config.put_generic Method.old_section_parser true) #>
   196       (parse_term_args args --
   197         parse_method_args method_args --|
   198         (Scan.depend (fn context =>
   199           Scan.succeed (fold Named_Theorems.clear uses_internal context, ())) --
   200          Method.sections modifiers)) >> (fn (ts, decl) => meth ts o decl);
   201 
   202     val full_name = Local_Theory.full_name lthy name;
   203 
   204     val lthy3 = lthy2
   205       |> Method.local_setup (Binding.make (Binding.name_of name, Position.none))
   206         (parser term_args (get_recursive_method full_name)) "(internal)"
   207       |> put_recursive_method (full_name, fn _ => fn _ => Method.fail);
   208 
   209     val (text, src) =
   210       Method.read_closure (Config.put Proof_Context.dynamic_facts_dummy true lthy3) source;
   211 
   212     val morphism =
   213       Variable.export_morphism lthy3
   214         (lthy
   215           |> Proof_Context.transfer (Proof_Context.theory_of lthy3)
   216           |> fold Token.declare_maxidx src
   217           |> Variable.declare_maxidx (Variable.maxidx_of lthy3));
   218 
   219     val text' = (Method.map_source o map) (Token.transform morphism) text;
   220     val term_args' = map (Morphism.term morphism) term_args;
   221   in
   222     lthy3
   223     |> Local_Theory.close_target
   224     |> Proof_Context.restore_naming lthy
   225     |> put_closure name
   226         {vars = term_args', named_thms = named_thms, methods = method_args, body = text'}
   227     |> Method.local_setup name
   228         (Args.context :|-- (fn ctxt =>
   229           let val {body, vars, ...} = get_closure ctxt full_name in
   230             parser vars (recursive_method full_name vars body) end)) ""
   231     |> pair full_name
   232   end;
   233 
   234 in
   235 
   236 val method = gen_method Proof_Context.add_fixes;
   237 val method_cmd = gen_method Proof_Context.add_fixes_cmd;
   238 
   239 end;
   240 
   241 val _ =
   242   Outer_Syntax.local_theory @{command_keyword method} "Eisbach method definition"
   243     (Parse.binding -- Parse.for_fixes --
   244       ((Scan.optional (@{keyword "methods"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) --
   245         (Scan.optional (@{keyword "uses"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) [])) --
   246       (Scan.optional (@{keyword "declares"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) --
   247       Parse.!!! (@{keyword "="} |-- Parse.args1 (K true)) >>
   248       (fn ((((name, vars), (methods, uses)), declares), src) =>
   249         #2 o method_cmd name vars uses declares methods src));
   250 
   251 end;