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