src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML

--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jan 05 09:54:41 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jan 05 10:09:42 2015 +0100
@@ -8,7 +8,11 @@
 
 signature BNF_GFP_REC_SUGAR =
 sig
-  datatype primcorec_option = Sequential_Option | Exhaustive_Option | Transfer_Option
+  datatype corec_option =
+    Plugins_Option of Proof.context -> Plugin_Name.filter |
+    Sequential_Option |
+    Exhaustive_Option |
+    Transfer_Option
 
   datatype corec_call =
     Dummy_No_Corec of int |
@@ -45,14 +49,13 @@
     corec_spec list * typ list * thm * thm * thm list * thm list * (Token.src list * Token.src list)
     * bool * local_theory
 
-  val primcorec_interpretation:
-    string -> (BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> local_theory -> local_theory) ->
-    theory -> theory
+  val gfp_rec_sugar_interpretation: string ->
+    (BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> local_theory -> local_theory) -> theory -> theory
 
-  val add_primcorecursive_cmd: primcorec_option list ->
+  val add_primcorecursive_cmd: corec_option list ->
     (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
     Proof.context -> Proof.state
-  val add_primcorec_cmd: primcorec_option list ->
+  val add_primcorec_cmd: corec_option list ->
     (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
     local_theory -> local_theory
 end;
@@ -88,7 +91,11 @@
 fun primcorec_error_eqn str eqn = raise PRIMCOREC (str, [eqn]);
 fun primcorec_error_eqns str eqns = raise PRIMCOREC (str, eqns);
 
-datatype primcorec_option = Sequential_Option | Exhaustive_Option | Transfer_Option;
+datatype corec_option =
+  Plugins_Option of Proof.context -> Plugin_Name.filter |
+  Sequential_Option |
+  Exhaustive_Option |
+  Transfer_Option;
 
 datatype corec_call =
   Dummy_No_Corec of int |
@@ -411,15 +418,13 @@
     (case fp_sugar_of ctxt s of SOME {fp_bnf_sugar = {map_thms, ...}, ...} => map_thms | NONE => [])
   | map_thms_of_typ _ _ = [];
 
-val transfer_primcorec = morph_fp_rec_sugar o Morphism.transfer_morphism;
-
-structure Primcorec_Plugin = Plugin(type T = fp_rec_sugar);
+structure GFP_Rec_Sugar_Plugin = Plugin(type T = fp_rec_sugar);
 
-fun primcorec_interpretation name f =
-  Primcorec_Plugin.interpretation name (fn fp_rec_sugar => fn lthy =>
-    f (transfer_primcorec (Proof_Context.theory_of lthy) fp_rec_sugar) lthy);
+fun gfp_rec_sugar_interpretation name f =
+  GFP_Rec_Sugar_Plugin.interpretation name (fn fp_rec_sugar => fn lthy =>
+    f (transfer_fp_rec_sugar (Proof_Context.theory_of lthy) fp_rec_sugar) lthy);
 
-val interpret_primcorec = Primcorec_Plugin.data_default;
+val interpret_gfp_rec_sugar = GFP_Rec_Sugar_Plugin.data;
 
 fun corec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 =
   let
@@ -992,9 +997,11 @@
 
     val actual_nn = length bs;
 
-    val sequentials = replicate actual_nn (member (op =) opts Sequential_Option);
-    val exhaustives = replicate actual_nn (member (op =) opts Exhaustive_Option);
-    val transfers = replicate actual_nn (member (op =) opts Transfer_Option);
+    val plugins = get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts)
+      |> the_default Plugin_Name.default_filter;
+    val sequentials = replicate actual_nn (exists (can (fn Sequential_Option => ())) opts);
+    val exhaustives = replicate actual_nn (exists (can (fn Exhaustive_Option => ())) opts);
+    val transfers = replicate actual_nn (exists (can (fn Transfer_Option => ())) opts);
 
     val fun_names = map Binding.name_of bs;
     val basic_ctr_specss = map (basic_corec_specs_of lthy) res_Ts;
@@ -1445,12 +1452,14 @@
           let
             val phi = Local_Theory.target_morphism lthy;
             val Ts = take actual_nn (map #T corec_specs);
+            val fp_rec_sugar =
+              {transfers = transfers, fun_names = fun_names, funs = map (Morphism.term phi) ts,
+               fun_defs = Morphism.fact phi def_thms, fpTs = Ts};
           in
-            interpret_primcorec {transfers = transfers, fun_names = fun_names,
-              funs = map (Morphism.term phi) ts, fun_defs = Morphism.fact phi def_thms, fpTs = Ts}
-              lthy
+            interpret_gfp_rec_sugar plugins fp_rec_sugar lthy
           end)
       end;
+
     fun after_qed thmss' = fold_map Local_Theory.define defs #-> prove thmss';
   in
     (goalss, after_qed, lthy')
@@ -1484,8 +1493,9 @@
       | _ => error "\"auto\" failed -- use \"primcorecursive\" instead of \"primcorec\"")
     goalss)) ooo add_primcorec_ursive_cmd true;
 
-val primcorec_option_parser = Parse.group (K "option")
-  (Parse.reserved "sequential" >> K Sequential_Option
+val corec_option_parser = Parse.group (K "option")
+  (Plugin_Name.parse_filter >> Plugins_Option
+   || Parse.reserved "sequential" >> K Sequential_Option
    || Parse.reserved "exhaustive" >> K Exhaustive_Option
    || Parse.reserved "transfer" >> K Transfer_Option);
 
@@ -1496,16 +1506,16 @@
 val _ = Outer_Syntax.local_theory_to_proof @{command_spec "primcorecursive"}
   "define primitive corecursive functions"
   ((Scan.optional (@{keyword "("} |--
-      Parse.!!! (Parse.list1 primcorec_option_parser) --| @{keyword ")"}) []) --
+      Parse.!!! (Parse.list1 corec_option_parser) --| @{keyword ")"}) []) --
     (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorecursive_cmd);
 
 val _ = Outer_Syntax.local_theory @{command_spec "primcorec"}
   "define primitive corecursive functions"
-  ((Scan.optional (@{keyword "("} |--
-      Parse.!!! (Parse.list1 primcorec_option_parser) --| @{keyword ")"}) []) --
+  ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
+      --| @{keyword ")"}) []) --
     (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorec_cmd);
 
-val _ = Theory.setup (primcorec_interpretation Transfer_BNF.transfer_plugin
-  primcorec_transfer_interpretation);
+val _ = Theory.setup (gfp_rec_sugar_interpretation Transfer_BNF.transfer_plugin
+  gfp_rec_sugar_transfer_interpretation);
 
 end;