src/Pure/Tools/plugin.ML
changeset 58657 c917dc025184
child 58658 9002fe021e2f
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Tools/plugin.ML	Mon Oct 13 15:45:23 2014 +0200
     1.3 @@ -0,0 +1,171 @@
     1.4 +(*  Title:      Pure/Tools/plugin.ML
     1.5 +    Author:     Makarius
     1.6 +    Author:     Jasmin Blanchette
     1.7 +
     1.8 +Named plugins for definitional packages.
     1.9 +*)
    1.10 +
    1.11 +(** plugin name **)
    1.12 +
    1.13 +signature PLUGIN_NAME =
    1.14 +sig
    1.15 +  val check: Proof.context -> xstring * Position.T -> string
    1.16 +  val declare: binding -> theory -> string * theory
    1.17 +  val setup: binding -> string
    1.18 +  type filter = string -> bool
    1.19 +  val parse_filter: (Proof.context -> filter) parser
    1.20 +  val make_filter: Proof.context -> (Proof.context -> filter) -> filter
    1.21 +end;
    1.22 +
    1.23 +structure Plugin_Name: PLUGIN_NAME =
    1.24 +struct
    1.25 +
    1.26 +(* theory data *)
    1.27 +
    1.28 +structure Data = Theory_Data
    1.29 +(
    1.30 +  type T = unit Name_Space.table;
    1.31 +  val empty: T = Name_Space.empty_table "plugin";
    1.32 +  val extend = I;
    1.33 +  val merge = Name_Space.merge_tables;
    1.34 +);
    1.35 +
    1.36 +
    1.37 +(* check *)
    1.38 +
    1.39 +fun check ctxt =
    1.40 +  #1 o Name_Space.check (Context.Proof ctxt) (Data.get (Proof_Context.theory_of ctxt));
    1.41 +
    1.42 +val _ = Theory.setup
    1.43 +  (ML_Antiquotation.inline @{binding plugin}
    1.44 +    (Args.context -- Scan.lift (Parse.position Args.name)
    1.45 +      >> (ML_Syntax.print_string o uncurry check)));
    1.46 +
    1.47 +
    1.48 +(* declare *)
    1.49 +
    1.50 +fun declare binding thy =
    1.51 +  let
    1.52 +    val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.default_naming);
    1.53 +    val (name, data') = Name_Space.define context true (binding, ()) (Data.get thy);
    1.54 +    val thy' = Data.put data' thy;
    1.55 +  in (name, thy') end;
    1.56 +
    1.57 +fun setup binding = Context.>>> (Context.map_theory_result (declare binding));
    1.58 +
    1.59 +
    1.60 +(* filter *)
    1.61 +
    1.62 +type filter = string -> bool;
    1.63 +
    1.64 +fun make_filter (ctxt: Proof.context) f : filter = f ctxt;
    1.65 +
    1.66 +val parse_filter =
    1.67 +  Parse.position (Parse.reserved "plugins") --
    1.68 +    Parse.position (Parse.reserved "only" >> K I || Parse.reserved "del" >> K not) --
    1.69 +    (@{keyword ":"} |-- Scan.repeat (Parse.position Parse.name)) >>
    1.70 +      (fn (((_, pos1), (modif, pos2)), args) => fn ctxt =>
    1.71 +        let
    1.72 +          val _ = Context_Position.reports ctxt (map (rpair Markup.quasi_keyword) [pos1, pos2]);
    1.73 +          val names = map (check ctxt) args;
    1.74 +        in modif o member (op =) names end);
    1.75 +
    1.76 +end;
    1.77 +
    1.78 +
    1.79 +
    1.80 +(** plugin content **)
    1.81 +
    1.82 +signature PLUGIN =
    1.83 +sig
    1.84 +  type T
    1.85 +  val data: Plugin_Name.filter -> T -> local_theory -> local_theory
    1.86 +  val interpretation: string -> (T -> local_theory -> local_theory) -> theory -> theory
    1.87 +end;
    1.88 +
    1.89 +functor Plugin(type T): PLUGIN =
    1.90 +struct
    1.91 +
    1.92 +type T = T;
    1.93 +
    1.94 +
    1.95 +(* data with interpretation *)
    1.96 +
    1.97 +type data = {filter: Plugin_Name.filter, naming: Name_Space.naming, value: T, id: serial};
    1.98 +type interp = {name: string, apply: T -> local_theory -> local_theory, id: serial};
    1.99 +
   1.100 +val eq_data: data * data -> bool = op = o pairself #id;
   1.101 +val eq_interp: interp * interp -> bool = op = o pairself #id;
   1.102 +
   1.103 +fun mk_data filter naming x : data = {filter = filter, naming = naming, value = x, id = serial ()};
   1.104 +fun mk_interp name f : interp = {name = name, apply = f, id = serial ()};
   1.105 +
   1.106 +
   1.107 +(* theory data *)
   1.108 +
   1.109 +structure Plugin_Data = Theory_Data
   1.110 +(
   1.111 +  type T = data list * (interp * data list) list;
   1.112 +  val empty : T = ([], []);
   1.113 +  val extend = I;
   1.114 +  val merge_data = merge eq_data;
   1.115 +  fun merge ((data1, interps1), (data2, interps2)) : T =
   1.116 +    (merge_data (data1, data2), AList.join eq_interp (K merge_data) (interps1, interps2));
   1.117 +);
   1.118 +
   1.119 +
   1.120 +(* consolidate data wrt. interpretations *)
   1.121 +
   1.122 +local
   1.123 +
   1.124 +fun apply change_naming (interp: interp) (data: data) lthy =
   1.125 +  lthy
   1.126 +  |> change_naming ? Local_Theory.map_naming (K (#naming data))
   1.127 +  |> #apply interp (#value data)
   1.128 +  |> Local_Theory.restore_naming lthy;
   1.129 +
   1.130 +fun unfinished data (interp: interp, data') =
   1.131 +  (interp,
   1.132 +    if eq_list eq_data (data, data') then []
   1.133 +    else data |> filter (fn d => #filter d (#name interp) andalso not (member eq_data data' d)));
   1.134 +
   1.135 +fun unfinished_data thy =
   1.136 +  let
   1.137 +    val (data, interps) = Plugin_Data.get thy;
   1.138 +    val finished = map (apsnd (K data)) interps;
   1.139 +    val thy' = Plugin_Data.put (data, finished) thy;
   1.140 +  in (map (unfinished data) interps, thy') end;
   1.141 +
   1.142 +in
   1.143 +
   1.144 +val consolidate =
   1.145 +  Local_Theory.raw_theory_result unfinished_data
   1.146 +  #-> fold_rev (fn (interp, data) => fold_rev (apply false interp) data);
   1.147 +
   1.148 +val consolidate' =
   1.149 +  unfinished_data #> (fn (unfinished, thy) =>
   1.150 +    if forall (null o #2) unfinished then NONE
   1.151 +    else
   1.152 +      Named_Target.theory_init thy
   1.153 +      |> fold_rev (fn (interp, data) => fold_rev (apply true interp) data) unfinished
   1.154 +      |> Local_Theory.exit_global
   1.155 +      |> SOME);
   1.156 +
   1.157 +end;
   1.158 +
   1.159 +val _ = Theory.setup (Theory.at_begin consolidate');
   1.160 +
   1.161 +
   1.162 +(* add content *)
   1.163 +
   1.164 +fun data filter x =
   1.165 +  Local_Theory.background_theory (fn thy =>
   1.166 +    Plugin_Data.map (apfst (cons (mk_data filter (Sign.naming_of thy) x))) thy)
   1.167 +  #> consolidate;
   1.168 +
   1.169 +fun interpretation name f =
   1.170 +  Plugin_Data.map (apsnd (cons (mk_interp name f, [])))
   1.171 +  #> perhaps consolidate';
   1.172 +
   1.173 +end;
   1.174 +