src/Pure/Tools/plugin.ML
author blanchet
Wed Dec 17 16:51:29 2014 +0100 (2014-12-17)
changeset 59145 0e304b1568a5
parent 59058 a78612c67ec0
child 59880 30687c3f2b10
permissions -rw-r--r--
tuning
wenzelm@58657
     1
(*  Title:      Pure/Tools/plugin.ML
wenzelm@58657
     2
    Author:     Makarius
wenzelm@58657
     3
    Author:     Jasmin Blanchette
wenzelm@58657
     4
wenzelm@58657
     5
Named plugins for definitional packages.
wenzelm@58657
     6
*)
wenzelm@58657
     7
wenzelm@58657
     8
(** plugin name **)
wenzelm@58657
     9
wenzelm@58657
    10
signature PLUGIN_NAME =
wenzelm@58657
    11
sig
wenzelm@58657
    12
  val check: Proof.context -> xstring * Position.T -> string
wenzelm@58658
    13
  val define: binding -> string list -> theory -> string * theory
wenzelm@58658
    14
  val define_setup: binding -> string list -> string
wenzelm@58657
    15
  val declare: binding -> theory -> string * theory
wenzelm@58658
    16
  val declare_setup: binding -> string
wenzelm@58657
    17
  type filter = string -> bool
wenzelm@58660
    18
  val default_filter: filter
wenzelm@58660
    19
  val make_filter: Proof.context -> (Proof.context -> filter) -> filter
wenzelm@58657
    20
  val parse_filter: (Proof.context -> filter) parser
wenzelm@58657
    21
end;
wenzelm@58657
    22
wenzelm@58657
    23
structure Plugin_Name: PLUGIN_NAME =
wenzelm@58657
    24
struct
wenzelm@58657
    25
wenzelm@58657
    26
(* theory data *)
wenzelm@58657
    27
wenzelm@58657
    28
structure Data = Theory_Data
wenzelm@58657
    29
(
wenzelm@58658
    30
  type T = string list Name_Space.table;
wenzelm@58657
    31
  val empty: T = Name_Space.empty_table "plugin";
wenzelm@58657
    32
  val extend = I;
wenzelm@58657
    33
  val merge = Name_Space.merge_tables;
wenzelm@58657
    34
);
wenzelm@58657
    35
wenzelm@58657
    36
wenzelm@58657
    37
(* check *)
wenzelm@58657
    38
wenzelm@58657
    39
fun check ctxt =
wenzelm@58657
    40
  #1 o Name_Space.check (Context.Proof ctxt) (Data.get (Proof_Context.theory_of ctxt));
wenzelm@58657
    41
wenzelm@58657
    42
val _ = Theory.setup
wenzelm@58657
    43
  (ML_Antiquotation.inline @{binding plugin}
wenzelm@58657
    44
    (Args.context -- Scan.lift (Parse.position Args.name)
wenzelm@58657
    45
      >> (ML_Syntax.print_string o uncurry check)));
wenzelm@58657
    46
wenzelm@58657
    47
wenzelm@58658
    48
(* indirections *)
wenzelm@58657
    49
wenzelm@58658
    50
fun resolve thy = maps (fn name =>
wenzelm@58658
    51
  (case Name_Space.get (Data.get thy) name of
wenzelm@58658
    52
    [] => [name]
wenzelm@58658
    53
  | names => resolve thy names));
wenzelm@58658
    54
wenzelm@58658
    55
fun define binding rhs thy =
wenzelm@58657
    56
  let
wenzelm@58668
    57
    val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.global_naming);
wenzelm@58658
    58
    val (name, data') = Name_Space.define context true (binding, resolve thy rhs) (Data.get thy);
wenzelm@58657
    59
    val thy' = Data.put data' thy;
wenzelm@58657
    60
  in (name, thy') end;
wenzelm@58657
    61
wenzelm@58658
    62
fun define_setup binding rhs = Context.>>> (Context.map_theory_result (define binding rhs));
wenzelm@58658
    63
wenzelm@58658
    64
wenzelm@58658
    65
(* immediate entries *)
wenzelm@58658
    66
wenzelm@58658
    67
fun declare binding thy = define binding [] thy;
wenzelm@58658
    68
fun declare_setup binding = Context.>>> (Context.map_theory_result (declare binding));
wenzelm@58657
    69
wenzelm@58657
    70
wenzelm@58657
    71
(* filter *)
wenzelm@58657
    72
wenzelm@58657
    73
type filter = string -> bool;
wenzelm@58657
    74
wenzelm@58660
    75
val default_filter: filter = K true;
wenzelm@58660
    76
wenzelm@58657
    77
fun make_filter (ctxt: Proof.context) f : filter = f ctxt;
wenzelm@58657
    78
wenzelm@58657
    79
val parse_filter =
wenzelm@58657
    80
  Parse.position (Parse.reserved "plugins") --
wenzelm@58657
    81
    Parse.position (Parse.reserved "only" >> K I || Parse.reserved "del" >> K not) --
wenzelm@58660
    82
    (Parse.$$$ ":" |-- Scan.repeat (Parse.position Parse.name)) >>
wenzelm@58657
    83
      (fn (((_, pos1), (modif, pos2)), args) => fn ctxt =>
wenzelm@58657
    84
        let
wenzelm@58658
    85
          val thy = Proof_Context.theory_of ctxt;
wenzelm@58657
    86
          val _ = Context_Position.reports ctxt (map (rpair Markup.quasi_keyword) [pos1, pos2]);
wenzelm@58658
    87
          val basic_names = resolve thy (map (check ctxt) args);
wenzelm@58658
    88
        in modif o member (op =) basic_names end);
wenzelm@58657
    89
wenzelm@58657
    90
end;
wenzelm@58657
    91
wenzelm@58657
    92
wenzelm@58657
    93
wenzelm@58657
    94
(** plugin content **)
wenzelm@58657
    95
wenzelm@58657
    96
signature PLUGIN =
wenzelm@58657
    97
sig
wenzelm@58657
    98
  type T
wenzelm@58657
    99
  val data: Plugin_Name.filter -> T -> local_theory -> local_theory
wenzelm@58666
   100
  val data_default: T -> local_theory -> local_theory
wenzelm@58657
   101
  val interpretation: string -> (T -> local_theory -> local_theory) -> theory -> theory
wenzelm@58657
   102
end;
wenzelm@58657
   103
wenzelm@58657
   104
functor Plugin(type T): PLUGIN =
wenzelm@58657
   105
struct
wenzelm@58657
   106
wenzelm@58657
   107
type T = T;
wenzelm@58657
   108
wenzelm@58657
   109
wenzelm@58657
   110
(* data with interpretation *)
wenzelm@58657
   111
wenzelm@58657
   112
type data = {filter: Plugin_Name.filter, naming: Name_Space.naming, value: T, id: serial};
wenzelm@58657
   113
type interp = {name: string, apply: T -> local_theory -> local_theory, id: serial};
wenzelm@58657
   114
wenzelm@59058
   115
val eq_data: data * data -> bool = op = o apply2 #id;
wenzelm@59058
   116
val eq_interp: interp * interp -> bool = op = o apply2 #id;
wenzelm@58657
   117
wenzelm@58657
   118
fun mk_data filter naming x : data = {filter = filter, naming = naming, value = x, id = serial ()};
wenzelm@58657
   119
fun mk_interp name f : interp = {name = name, apply = f, id = serial ()};
wenzelm@58657
   120
wenzelm@58657
   121
wenzelm@58657
   122
(* theory data *)
wenzelm@58657
   123
wenzelm@58657
   124
structure Plugin_Data = Theory_Data
wenzelm@58657
   125
(
wenzelm@58657
   126
  type T = data list * (interp * data list) list;
wenzelm@58657
   127
  val empty : T = ([], []);
wenzelm@58657
   128
  val extend = I;
wenzelm@58657
   129
  val merge_data = merge eq_data;
wenzelm@58657
   130
  fun merge ((data1, interps1), (data2, interps2)) : T =
wenzelm@58657
   131
    (merge_data (data1, data2), AList.join eq_interp (K merge_data) (interps1, interps2));
wenzelm@58657
   132
);
wenzelm@58657
   133
wenzelm@58657
   134
wenzelm@58657
   135
(* consolidate data wrt. interpretations *)
wenzelm@58657
   136
wenzelm@58657
   137
local
wenzelm@58657
   138
wenzelm@58657
   139
fun apply change_naming (interp: interp) (data: data) lthy =
wenzelm@58657
   140
  lthy
wenzelm@58657
   141
  |> change_naming ? Local_Theory.map_naming (K (#naming data))
wenzelm@58657
   142
  |> #apply interp (#value data)
wenzelm@58657
   143
  |> Local_Theory.restore_naming lthy;
wenzelm@58657
   144
wenzelm@58657
   145
fun unfinished data (interp: interp, data') =
wenzelm@58657
   146
  (interp,
wenzelm@58657
   147
    if eq_list eq_data (data, data') then []
wenzelm@58657
   148
    else data |> filter (fn d => #filter d (#name interp) andalso not (member eq_data data' d)));
wenzelm@58657
   149
wenzelm@58657
   150
fun unfinished_data thy =
wenzelm@58657
   151
  let
wenzelm@58657
   152
    val (data, interps) = Plugin_Data.get thy;
wenzelm@58657
   153
    val finished = map (apsnd (K data)) interps;
wenzelm@58657
   154
    val thy' = Plugin_Data.put (data, finished) thy;
wenzelm@58657
   155
  in (map (unfinished data) interps, thy') end;
wenzelm@58657
   156
wenzelm@58657
   157
in
wenzelm@58657
   158
wenzelm@58657
   159
val consolidate =
wenzelm@58657
   160
  Local_Theory.raw_theory_result unfinished_data
wenzelm@58657
   161
  #-> fold_rev (fn (interp, data) => fold_rev (apply false interp) data);
wenzelm@58657
   162
wenzelm@58657
   163
val consolidate' =
wenzelm@58657
   164
  unfinished_data #> (fn (unfinished, thy) =>
wenzelm@58657
   165
    if forall (null o #2) unfinished then NONE
wenzelm@58657
   166
    else
wenzelm@58665
   167
      SOME (Named_Target.theory_map
wenzelm@58665
   168
        (fold_rev (fn (interp, data) => fold_rev (apply true interp) data) unfinished) thy));
wenzelm@58657
   169
wenzelm@58657
   170
end;
wenzelm@58657
   171
wenzelm@58657
   172
val _ = Theory.setup (Theory.at_begin consolidate');
wenzelm@58657
   173
wenzelm@58657
   174
wenzelm@58657
   175
(* add content *)
wenzelm@58657
   176
wenzelm@58657
   177
fun data filter x =
wenzelm@58657
   178
  Local_Theory.background_theory (fn thy =>
wenzelm@58657
   179
    Plugin_Data.map (apfst (cons (mk_data filter (Sign.naming_of thy) x))) thy)
wenzelm@58657
   180
  #> consolidate;
wenzelm@58657
   181
wenzelm@58666
   182
val data_default = data Plugin_Name.default_filter;
wenzelm@58666
   183
wenzelm@58657
   184
fun interpretation name f =
wenzelm@58657
   185
  Plugin_Data.map (apsnd (cons (mk_interp name f, [])))
wenzelm@58657
   186
  #> perhaps consolidate';
wenzelm@58657
   187
wenzelm@58657
   188
end;