# HG changeset patch
# User blanchet
# Date 1420448982 -3600
# Node ID 1b4dc8a9f7d99eb606a874daae041b085acb7e33
# Parent  2949ace404c3808b3ce557282a0dc62f2954bf3f
added plugins syntax to prim(co)rec

diff -r 2949ace404c3 -r 1b4dc8a9f7d9 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Jan 05 09:54:41 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Jan 05 10:09:42 2015 +0100
@@ -829,7 +829,7 @@
 
     val bnf_T = Morphism.typ phi T_rhs;
     val bad_args = Term.add_tfreesT bnf_T [];
-    val _ = if null bad_args then () else error ("Locally fixed type arguments " ^
+    val _ = null bad_args orelse error ("Locally fixed type arguments " ^
       commas_quote (map (Syntax.string_of_typ no_defs_lthy o TFree) bad_args));
 
     val bnf_sets =
diff -r 2949ace404c3 -r 1b4dc8a9f7d9 src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Mon Jan 05 09:54:41 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML	Mon Jan 05 10:09:42 2015 +0100
@@ -7,9 +7,9 @@
 
 signature BNF_FP_REC_SUGAR_TRANSFER =
 sig
-  val primrec_transfer_interpretation: BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> Proof.context ->
+  val lfp_rec_sugar_transfer_interpretation: BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> Proof.context ->
     Proof.context
-  val primcorec_transfer_interpretation: BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> Proof.context ->
+  val gfp_rec_sugar_transfer_interpretation: BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> Proof.context ->
     Proof.context
 end;
 
@@ -22,14 +22,15 @@
 open BNF_FP_Util
 open BNF_FP_Def_Sugar
 open BNF_FP_Rec_Sugar_Util
+open BNF_LFP_Rec_Sugar
 
 val transferN = "transfer";
 
-fun mk_primrec_transfer_tac ctxt def =
+fun mk_lfp_rec_sugar_transfer_tac ctxt def =
   Ctr_Sugar_Tactics.unfold_thms_tac ctxt [def] THEN
   HEADGOAL (Transfer.transfer_prover_tac ctxt);
 
-fun mk_primcorec_transfer_tac apply_transfer ctxt f_def corec_def type_definitions
+fun mk_gfp_rec_sugar_transfer_tac apply_transfer ctxt f_def corec_def type_definitions
     dtor_corec_transfers rel_pre_defs disc_eq_cases cases case_distribs case_congs =
   let
     fun instantiate_with_lambda thm =
@@ -113,7 +114,7 @@
           (fn () => error "Function is not parametric" (*FIXME: wording*)) ())
     (transfers ~~ fun_names ~~ funs ~~ fun_defs) lthy;
 
-fun prim_co_rec_transfer_interpretation prove =
+fun fp_rec_sugar_transfer_interpretation prove =
   prove_parametricity_if_bnf (fn n => fn bnfs => fn f_name => fn f => fn def => fn lthy =>
     (case try (prove n bnfs f def) lthy of
       NONE => error "Failed to prove parametricity"
@@ -125,16 +126,16 @@
         snd (Local_Theory.notes notes lthy)
       end));
 
-val primrec_transfer_interpretation = prim_co_rec_transfer_interpretation
+val lfp_rec_sugar_transfer_interpretation = fp_rec_sugar_transfer_interpretation
   (fn _ => fn _ => fn f => fn def => fn lthy =>
      let val (goal, names_lthy) = mk_goal lthy f in
        Goal.prove lthy [] [] goal (fn {context = ctxt, prems = _} =>
-         mk_primrec_transfer_tac ctxt def)
+         mk_lfp_rec_sugar_transfer_tac ctxt def)
        |> singleton (Proof_Context.export names_lthy lthy)
        |> Thm.close_derivation
      end);
 
-val primcorec_transfer_interpretation = prim_co_rec_transfer_interpretation
+val gfp_rec_sugar_transfer_interpretation = fp_rec_sugar_transfer_interpretation
   (fn n => fn bnfs => fn f => fn def => fn lthy =>
      let
        val fp_sugars = map (the o fp_sugar_of_bnf lthy) bnfs;
@@ -155,7 +156,7 @@
            end) (fastype_of f) ([], [], [], []);
      in
        Goal.prove lthy [] [] goal (fn {context = ctxt, prems = _} =>
-         mk_primcorec_transfer_tac true ctxt def
+         mk_gfp_rec_sugar_transfer_tac true ctxt def
          (#co_rec_def (#fp_co_induct_sugar (nth fp_sugars n)))
          (map (#type_definition o #absT_info) fp_sugars)
          (maps (#xtor_co_rec_transfers o #fp_res) fp_sugars)
@@ -165,7 +166,7 @@
        |> Thm.close_derivation
      end);
 
-val _ = Theory.setup (BNF_LFP_Rec_Sugar.primrec_interpretation Transfer_BNF.transfer_plugin
-  primrec_transfer_interpretation);
+val _ = Theory.setup (lfp_rec_sugar_interpretation Transfer_BNF.transfer_plugin
+  lfp_rec_sugar_transfer_interpretation);
 
 end;
diff -r 2949ace404c3 -r 1b4dc8a9f7d9 src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Mon Jan 05 09:54:41 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Mon Jan 05 10:09:42 2015 +0100
@@ -21,6 +21,7 @@
      fpTs: typ list}
 
   val morph_fp_rec_sugar: morphism -> fp_rec_sugar -> fp_rec_sugar
+  val transfer_fp_rec_sugar: theory -> fp_rec_sugar -> fp_rec_sugar
 
   val flat_rec_arg_args: 'a list list -> 'a list
 
@@ -66,7 +67,7 @@
    fun_names: string list,
    funs: term list,
    fun_defs: thm list,
-   fpTs: typ list}
+   fpTs: typ list};
 
 fun morph_fp_rec_sugar phi {transfers, fun_names, funs, fun_defs, fpTs} =
   {transfers = transfers,
@@ -75,9 +76,11 @@
    fun_defs = map (Morphism.thm phi) fun_defs,
    fpTs = map (Morphism.typ phi) fpTs};
 
+val transfer_fp_rec_sugar = morph_fp_rec_sugar o Morphism.transfer_morphism;
+
 fun flat_rec_arg_args xss =
-  (* FIXME (once the old datatype package is phased out): The first line below gives the preferred
-     order. The second line is for compatibility with the old datatype package. *)
+  (* FIXME (once the old datatype package is completely phased out): The first line below gives the
+     preferred order. The second line is for compatibility with the old datatype package. *)
   (* flat xss *)
   map hd xss @ maps tl xss;
 
diff -r 2949ace404c3 -r 1b4dc8a9f7d9 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;
diff -r 2949ace404c3 -r 1b4dc8a9f7d9 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Jan 05 09:54:41 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Jan 05 10:09:42 2015 +0100
@@ -8,7 +8,10 @@
 
 signature BNF_LFP_REC_SUGAR =
 sig
-  datatype primrec_option = Nonexhaustive_Option | Transfer_Option;
+  datatype rec_option =
+    Plugins_Option of Proof.context -> Plugin_Name.filter |
+    Nonexhaustive_Option |
+    Transfer_Option
 
   datatype rec_call =
     No_Rec of int * typ |
@@ -57,13 +60,12 @@
     (term * term list list) list list -> local_theory ->
     (bool * rec_spec list * typ list * thm * thm list * Token.src list * typ list) * local_theory
 
-  val primrec_interpretation:
-    string -> (BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> local_theory -> local_theory) ->
-    theory -> theory
+  val lfp_rec_sugar_interpretation: string ->
+    (BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> local_theory -> local_theory) -> theory -> theory
 
   val add_primrec: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> local_theory -> (term list * thm list list) * local_theory
-  val add_primrec_cmd: primrec_option list -> (binding * string option * mixfix) list ->
+  val add_primrec_cmd: rec_option list -> (binding * string option * mixfix) list ->
     (Attrib.binding * string) list -> local_theory -> (term list * thm list list) * local_theory
   val add_primrec_global: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> theory -> (term list * thm list list) * theory
@@ -92,7 +94,10 @@
 exception OLD_PRIMREC of unit;
 exception PRIMREC of string * term list;
 
-datatype primrec_option = Nonexhaustive_Option | Transfer_Option;
+datatype rec_option =
+  Plugins_Option of Proof.context -> Plugin_Name.filter |
+  Nonexhaustive_Option |
+  Transfer_Option;
 
 datatype rec_call =
   No_Rec of int * typ |
@@ -178,15 +183,13 @@
     SOME {rewrite_nested_rec_call = SOME f, ...} => f ctxt
   | _ => error "Unsupported nested recursion");
 
-val transfer_primrec = morph_fp_rec_sugar o Morphism.transfer_morphism;
-
-structure Primrec_Plugin = Plugin(type T = fp_rec_sugar);
+structure LFP_Rec_Sugar_Plugin = Plugin(type T = fp_rec_sugar);
 
-fun primrec_interpretation name f =
-  Primrec_Plugin.interpretation name (fn fp_rec_sugar => fn lthy =>
-    f (transfer_primrec (Proof_Context.theory_of lthy) fp_rec_sugar) lthy);
+fun lfp_rec_sugar_interpretation name f =
+  LFP_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_primrec = Primrec_Plugin.data_default;
+val interpret_lfp_rec_sugar = LFP_Rec_Sugar_Plugin.data;
 
 fun rec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 =
   let
@@ -491,7 +494,7 @@
   unfold_thms_tac ctxt (nested_simps ctxt @ map_ident0s @ map_comps) THEN
   HEADGOAL (rtac refl);
 
-fun prepare_primrec nonexhaustives transfers fixes specs lthy0 =
+fun prepare_primrec plugins nonexhaustives transfers fixes specs lthy0 =
   let
     val thy = Proof_Context.theory_of lthy0;
 
@@ -578,11 +581,11 @@
           val def_thms = map (snd o snd) defs;
           val ts = map fst defs;
           val phi = Local_Theory.target_morphism lthy;
+          val fp_rec_sugar =
+            {transfers = transfers, fun_names = fun_names, funs = map (Morphism.term phi) ts,
+             fun_defs = Morphism.fact phi def_thms, fpTs = take actual_nn Ts};
         in
-          map_prod split_list
-            (interpret_primrec {transfers = transfers, fun_names = fun_names,
-               funs = (map (Morphism.term phi) ts), fun_defs = (Morphism.fact phi def_thms),
-               fpTs = (take actual_nn Ts)})
+          map_prod split_list (interpret_lfp_rec_sugar plugins fp_rec_sugar)
             (@{fold_map 2} (prove defs) (take actual_nn rec_specs) funs_data lthy)
         end),
       lthy |> Local_Theory.notes (notes @ common_notes) |> snd)
@@ -591,9 +594,14 @@
 fun add_primrec_simple' opts fixes ts lthy =
   let
     val actual_nn = length fixes;
-    val nonexhaustives = replicate actual_nn (member (op =) opts Nonexhaustive_Option);
-    val transfers = replicate actual_nn (member (op =) opts Transfer_Option);
-    val (((names, defs), prove), lthy') = prepare_primrec nonexhaustives transfers fixes ts lthy
+
+    val plugins = get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts)
+      |> the_default Plugin_Name.default_filter;
+    val nonexhaustives = replicate actual_nn (exists (can (fn Nonexhaustive_Option => ())) opts);
+    val transfers = replicate actual_nn (exists (can (fn Transfer_Option => ())) opts);
+
+    val (((names, defs), prove), lthy') =
+      prepare_primrec plugins nonexhaustives transfers fixes ts lthy
       handle ERROR str => raise PRIMREC (str, []);
   in
     lthy'
@@ -658,14 +666,15 @@
   #> add_primrec fixes specs
   ##> Local_Theory.exit_global;
 
-val primrec_option_parser = Parse.group (K "option")
-  (Parse.reserved "nonexhaustive" >> K Nonexhaustive_Option
+val rec_option_parser = Parse.group (K "option")
+  (Plugin_Name.parse_filter >> Plugins_Option
+   || Parse.reserved "nonexhaustive" >> K Nonexhaustive_Option
    || Parse.reserved "transfer" >> K Transfer_Option);
 
 val _ = Outer_Syntax.local_theory @{command_spec "primrec"}
   "define primitive recursive functions"
-  ((Scan.optional (@{keyword "("} |--
-      Parse.!!! (Parse.list1 primrec_option_parser) --| @{keyword ")"}) []) --
+  ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 rec_option_parser)
+      --| @{keyword ")"}) []) --
     (Parse.fixes -- Parse_Spec.where_alt_specs)
     >> (fn (opts, (fixes, specs)) => snd o add_primrec_cmd opts fixes specs));
 
diff -r 2949ace404c3 -r 1b4dc8a9f7d9 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Jan 05 09:54:41 2015 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Jan 05 10:09:42 2015 +0100
@@ -378,12 +378,10 @@
 val code_plugin = Plugin_Name.declare_setup @{binding code};
 
 fun prepare_free_constructors kind prep_plugins prep_term
-    ((((raw_plugins, discs_sels), raw_case_binding), ctr_specs),
-      sel_default_eqs) no_defs_lthy =
+    ((((raw_plugins, discs_sels), raw_case_binding), ctr_specs), sel_default_eqs) no_defs_lthy =
   let
     val plugins = prep_plugins no_defs_lthy raw_plugins;
 
-
     (* TODO: sanity checks on arguments *)
 
     val raw_ctrs = map ctr_of_ctr_spec ctr_specs;
@@ -393,7 +391,7 @@
     val n = length raw_ctrs;
     val ks = 1 upto n;
 
-    val _ = if n > 0 then () else error "No constructors specified";
+    val _ = n > 0 orelse error "No constructors specified";
 
     val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs;
 
@@ -1127,8 +1125,8 @@
 
 val parse_ctr_options =
   Scan.optional (@{keyword "("} |-- Parse.list1
-        (Plugin_Name.parse_filter >> (apfst o K) ||
-         Parse.reserved "discs_sels" >> (apsnd o K o K true)) --|
+        (Plugin_Name.parse_filter >> (apfst o K)
+         || Parse.reserved "discs_sels" >> (apsnd o K o K true)) --|
       @{keyword ")"}
       >> (fn fs => fold I fs default_ctr_options_cmd))
     default_ctr_options_cmd;