support for named plugins for definitional packages;
authorwenzelm
Mon Oct 13 15:45:23 2014 +0200 (2014-10-13 ago)
changeset 58657c917dc025184
parent 58654 3e1cad27fc2f
child 58658 9002fe021e2f
support for named plugins for definitional packages;
src/Pure/Pure.thy
src/Pure/Tools/plugin.ML
     1.1 --- a/src/Pure/Pure.thy	Sun Oct 12 21:52:45 2014 +0200
     1.2 +++ b/src/Pure/Pure.thy	Mon Oct 13 15:45:23 2014 +0200
     1.3 @@ -120,6 +120,7 @@
     1.4  ML_file "Tools/proof_general_pure.ML"
     1.5  ML_file "Tools/simplifier_trace.ML"
     1.6  ML_file "Tools/named_theorems.ML"
     1.7 +ML_file "Tools/plugin.ML"
     1.8  
     1.9  
    1.10  section \<open>Basic attributes\<close>
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Tools/plugin.ML	Mon Oct 13 15:45:23 2014 +0200
     2.3 @@ -0,0 +1,171 @@
     2.4 +(*  Title:      Pure/Tools/plugin.ML
     2.5 +    Author:     Makarius
     2.6 +    Author:     Jasmin Blanchette
     2.7 +
     2.8 +Named plugins for definitional packages.
     2.9 +*)
    2.10 +
    2.11 +(** plugin name **)
    2.12 +
    2.13 +signature PLUGIN_NAME =
    2.14 +sig
    2.15 +  val check: Proof.context -> xstring * Position.T -> string
    2.16 +  val declare: binding -> theory -> string * theory
    2.17 +  val setup: binding -> string
    2.18 +  type filter = string -> bool
    2.19 +  val parse_filter: (Proof.context -> filter) parser
    2.20 +  val make_filter: Proof.context -> (Proof.context -> filter) -> filter
    2.21 +end;
    2.22 +
    2.23 +structure Plugin_Name: PLUGIN_NAME =
    2.24 +struct
    2.25 +
    2.26 +(* theory data *)
    2.27 +
    2.28 +structure Data = Theory_Data
    2.29 +(
    2.30 +  type T = unit Name_Space.table;
    2.31 +  val empty: T = Name_Space.empty_table "plugin";
    2.32 +  val extend = I;
    2.33 +  val merge = Name_Space.merge_tables;
    2.34 +);
    2.35 +
    2.36 +
    2.37 +(* check *)
    2.38 +
    2.39 +fun check ctxt =
    2.40 +  #1 o Name_Space.check (Context.Proof ctxt) (Data.get (Proof_Context.theory_of ctxt));
    2.41 +
    2.42 +val _ = Theory.setup
    2.43 +  (ML_Antiquotation.inline @{binding plugin}
    2.44 +    (Args.context -- Scan.lift (Parse.position Args.name)
    2.45 +      >> (ML_Syntax.print_string o uncurry check)));
    2.46 +
    2.47 +
    2.48 +(* declare *)
    2.49 +
    2.50 +fun declare binding thy =
    2.51 +  let
    2.52 +    val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.default_naming);
    2.53 +    val (name, data') = Name_Space.define context true (binding, ()) (Data.get thy);
    2.54 +    val thy' = Data.put data' thy;
    2.55 +  in (name, thy') end;
    2.56 +
    2.57 +fun setup binding = Context.>>> (Context.map_theory_result (declare binding));
    2.58 +
    2.59 +
    2.60 +(* filter *)
    2.61 +
    2.62 +type filter = string -> bool;
    2.63 +
    2.64 +fun make_filter (ctxt: Proof.context) f : filter = f ctxt;
    2.65 +
    2.66 +val parse_filter =
    2.67 +  Parse.position (Parse.reserved "plugins") --
    2.68 +    Parse.position (Parse.reserved "only" >> K I || Parse.reserved "del" >> K not) --
    2.69 +    (@{keyword ":"} |-- Scan.repeat (Parse.position Parse.name)) >>
    2.70 +      (fn (((_, pos1), (modif, pos2)), args) => fn ctxt =>
    2.71 +        let
    2.72 +          val _ = Context_Position.reports ctxt (map (rpair Markup.quasi_keyword) [pos1, pos2]);
    2.73 +          val names = map (check ctxt) args;
    2.74 +        in modif o member (op =) names end);
    2.75 +
    2.76 +end;
    2.77 +
    2.78 +
    2.79 +
    2.80 +(** plugin content **)
    2.81 +
    2.82 +signature PLUGIN =
    2.83 +sig
    2.84 +  type T
    2.85 +  val data: Plugin_Name.filter -> T -> local_theory -> local_theory
    2.86 +  val interpretation: string -> (T -> local_theory -> local_theory) -> theory -> theory
    2.87 +end;
    2.88 +
    2.89 +functor Plugin(type T): PLUGIN =
    2.90 +struct
    2.91 +
    2.92 +type T = T;
    2.93 +
    2.94 +
    2.95 +(* data with interpretation *)
    2.96 +
    2.97 +type data = {filter: Plugin_Name.filter, naming: Name_Space.naming, value: T, id: serial};
    2.98 +type interp = {name: string, apply: T -> local_theory -> local_theory, id: serial};
    2.99 +
   2.100 +val eq_data: data * data -> bool = op = o pairself #id;
   2.101 +val eq_interp: interp * interp -> bool = op = o pairself #id;
   2.102 +
   2.103 +fun mk_data filter naming x : data = {filter = filter, naming = naming, value = x, id = serial ()};
   2.104 +fun mk_interp name f : interp = {name = name, apply = f, id = serial ()};
   2.105 +
   2.106 +
   2.107 +(* theory data *)
   2.108 +
   2.109 +structure Plugin_Data = Theory_Data
   2.110 +(
   2.111 +  type T = data list * (interp * data list) list;
   2.112 +  val empty : T = ([], []);
   2.113 +  val extend = I;
   2.114 +  val merge_data = merge eq_data;
   2.115 +  fun merge ((data1, interps1), (data2, interps2)) : T =
   2.116 +    (merge_data (data1, data2), AList.join eq_interp (K merge_data) (interps1, interps2));
   2.117 +);
   2.118 +
   2.119 +
   2.120 +(* consolidate data wrt. interpretations *)
   2.121 +
   2.122 +local
   2.123 +
   2.124 +fun apply change_naming (interp: interp) (data: data) lthy =
   2.125 +  lthy
   2.126 +  |> change_naming ? Local_Theory.map_naming (K (#naming data))
   2.127 +  |> #apply interp (#value data)
   2.128 +  |> Local_Theory.restore_naming lthy;
   2.129 +
   2.130 +fun unfinished data (interp: interp, data') =
   2.131 +  (interp,
   2.132 +    if eq_list eq_data (data, data') then []
   2.133 +    else data |> filter (fn d => #filter d (#name interp) andalso not (member eq_data data' d)));
   2.134 +
   2.135 +fun unfinished_data thy =
   2.136 +  let
   2.137 +    val (data, interps) = Plugin_Data.get thy;
   2.138 +    val finished = map (apsnd (K data)) interps;
   2.139 +    val thy' = Plugin_Data.put (data, finished) thy;
   2.140 +  in (map (unfinished data) interps, thy') end;
   2.141 +
   2.142 +in
   2.143 +
   2.144 +val consolidate =
   2.145 +  Local_Theory.raw_theory_result unfinished_data
   2.146 +  #-> fold_rev (fn (interp, data) => fold_rev (apply false interp) data);
   2.147 +
   2.148 +val consolidate' =
   2.149 +  unfinished_data #> (fn (unfinished, thy) =>
   2.150 +    if forall (null o #2) unfinished then NONE
   2.151 +    else
   2.152 +      Named_Target.theory_init thy
   2.153 +      |> fold_rev (fn (interp, data) => fold_rev (apply true interp) data) unfinished
   2.154 +      |> Local_Theory.exit_global
   2.155 +      |> SOME);
   2.156 +
   2.157 +end;
   2.158 +
   2.159 +val _ = Theory.setup (Theory.at_begin consolidate');
   2.160 +
   2.161 +
   2.162 +(* add content *)
   2.163 +
   2.164 +fun data filter x =
   2.165 +  Local_Theory.background_theory (fn thy =>
   2.166 +    Plugin_Data.map (apfst (cons (mk_data filter (Sign.naming_of thy) x))) thy)
   2.167 +  #> consolidate;
   2.168 +
   2.169 +fun interpretation name f =
   2.170 +  Plugin_Data.map (apsnd (cons (mk_interp name f, [])))
   2.171 +  #> perhaps consolidate';
   2.172 +
   2.173 +end;
   2.174 +