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