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