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