# HG changeset patch
# User desharna
# Date 1413296254 -7200
# Node ID 69571f0a93df9468b5b4be972a7177307bcdaced
# Parent  eb98d1971d2a86bf6e48727d725f1a04ffaa134d
add 'kind' to 'cr_sugar'

diff -r eb98d1971d2a -r 69571f0a93df src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Oct 14 15:39:57 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Oct 14 16:17:34 2014 +0200
@@ -418,6 +418,9 @@
 val unflatt = fold_map unflat
 val unflattt = fold_map unflatt
 
+fun ctr_sugar_kind_of_fp_kind Least_FP = Datatype
+  | ctr_sugar_kind_of_fp_kind Greatest_FP = Codatatype
+
 fun uncurry_thm 0 thm = thm
   | uncurry_thm 1 thm = thm
   | uncurry_thm n thm = rotate_prems ~1 (uncurry_thm (n - 1) (rotate_prems 1 (conjI RS thm)));
@@ -2026,7 +2029,7 @@
     val ((xtor_co_recs, recs_args_types, corecs_args_types), lthy') =
       mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
 
-    fun define_ctrs_dtrs_for_type (((((((((((((((((((((((((((fp_bnf, fp_b), fpT), ctor), dtor),
+    fun define_ctrs_dtrs_for_type fp (((((((((((((((((((((((((((fp_bnf, fp_b), fpT), ctor), dtor),
               xtor_co_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
             pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), abs),
           abs_inject), abs_inverse), type_definition), ctr_bindings), ctr_mixfixes), ctr_Tss),
@@ -2113,8 +2116,8 @@
             val ctr_specs = @{map 3} ctr_spec_of disc_bindings ctrs0 sel_bindingss;
 
             val (ctr_sugar as {case_cong, ...}, lthy') =
-              free_constructors tacss ((((plugins, discs_sels), standard_binding), ctr_specs),
-                sel_default_eqs) lthy
+              free_constructors (ctr_sugar_kind_of_fp_kind fp) tacss
+                ((((plugins, discs_sels), standard_binding), ctr_specs), sel_default_eqs) lthy
 
             val anonymous_notes =
               [([case_cong], fundefcong_attrs)]
@@ -2366,7 +2369,7 @@
 
     val lthy'' = lthy'
       |> live > 0 ? fold2 (fn Type (s, _) => fn bnf => register_bnf_raw s bnf) fpTs fp_bnfs
-      |> fold_map define_ctrs_dtrs_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ ctors ~~ dtors ~~
+      |> fold_map (define_ctrs_dtrs_for_type fp) (fp_bnfs ~~ fp_bs ~~ fpTs ~~ ctors ~~ dtors ~~
         xtor_co_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ pre_set_defss ~~
         pre_rel_defs ~~ xtor_maps ~~ xtor_setss ~~ xtor_rels ~~ ns ~~ kss ~~ mss ~~
         abss ~~ abs_injects ~~ abs_inverses ~~ type_definitions ~~ ctr_bindingss ~~ ctr_mixfixess ~~
diff -r eb98d1971d2a -r 69571f0a93df src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Oct 14 15:39:57 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Oct 14 16:17:34 2014 +0200
@@ -7,8 +7,12 @@
 
 signature CTR_SUGAR =
 sig
+
+  datatype ctr_sugar_kind = Datatype | Codatatype | Record | Unknown
+
   type ctr_sugar =
-    {T: typ,
+    {kind: ctr_sugar_kind,
+     T: typ,
      ctrs: term list,
      casex: term,
      discs: term list,
@@ -73,7 +77,8 @@
   type ctr_options_cmd = (Proof.context -> string -> bool) * bool
 
   val fake_local_theory_for_sel_defaults: (binding * typ) list -> Proof.context -> Proof.context
-  val free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
+  val free_constructors: ctr_sugar_kind ->
+    ({prems: thm list, context: Proof.context} -> tactic) list list ->
     ((ctr_options * binding) * (term, binding) ctr_spec list) * term list -> local_theory ->
     ctr_sugar * local_theory
   val default_ctr_options: ctr_options
@@ -91,8 +96,11 @@
 open Ctr_Sugar_Tactics
 open Ctr_Sugar_Code
 
+datatype ctr_sugar_kind = Datatype | Codatatype | Record | Unknown;
+
 type ctr_sugar =
-  {T: typ,
+  {kind: ctr_sugar_kind,
+   T: typ,
    ctrs: term list,
    casex: term,
    discs: term list,
@@ -120,11 +128,12 @@
    split_sel_asms: thm list,
    case_eq_ifs: thm list};
 
-fun morph_ctr_sugar phi {T, ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
+fun morph_ctr_sugar phi {kind, T, ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
     case_thms, case_cong, case_cong_weak, split, split_asm, disc_defs, disc_thmss, discIs, sel_defs,
     sel_thmss, distinct_discsss, exhaust_discs, exhaust_sels, collapses, expands, split_sels,
     split_sel_asms, case_eq_ifs} =
-  {T = Morphism.typ phi T,
+  {kind = kind,
+   T = Morphism.typ phi T,
    ctrs = map (Morphism.term phi) ctrs,
    casex = Morphism.term phi casex,
    discs = map (Morphism.term phi) discs,
@@ -360,7 +369,7 @@
 
 val code_plugin = Plugin_Name.declare_setup @{binding code};
 
-fun prepare_free_constructors prep_plugins prep_term
+fun prepare_free_constructors kind prep_plugins prep_term
     ((((raw_plugins, discs_sels), raw_case_binding), ctr_specs),
       sel_default_eqs) no_defs_lthy =
   let
@@ -1037,15 +1046,15 @@
           |>> name_noted_thms fcT_name exhaustN;
 
         val ctr_sugar =
-          {T = fcT, ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
-           nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
-           case_thms = case_thms, case_cong = case_cong_thm, case_cong_weak = case_cong_weak_thm,
-           split = split_thm, split_asm = split_asm_thm, disc_defs = disc_defs,
-           disc_thmss = disc_thmss, discIs = discI_thms, sel_defs = sel_defs, sel_thmss = sel_thmss,
-           distinct_discsss = distinct_disc_thmsss, exhaust_discs = exhaust_disc_thms,
-           exhaust_sels = exhaust_sel_thms, collapses = all_collapse_thms, expands = expand_thms,
-           split_sels = split_sel_thms, split_sel_asms = split_sel_asm_thms,
-           case_eq_ifs = case_eq_if_thms}
+          {kind = kind, T = fcT, ctrs = ctrs, casex = casex, discs = discs, selss = selss,
+           exhaust = exhaust_thm, nchotomy = nchotomy_thm, injects = inject_thms,
+           distincts = distinct_thms, case_thms = case_thms, case_cong = case_cong_thm,
+           case_cong_weak = case_cong_weak_thm, split = split_thm, split_asm = split_asm_thm,
+           disc_defs = disc_defs, disc_thmss = disc_thmss, discIs = discI_thms, sel_defs = sel_defs,
+           sel_thmss = sel_thmss, distinct_discsss = distinct_disc_thmsss,
+           exhaust_discs = exhaust_disc_thms, exhaust_sels = exhaust_sel_thms,
+           collapses = all_collapse_thms, expands = expand_thms, split_sels = split_sel_thms,
+           split_sel_asms = split_sel_asm_thms, case_eq_ifs = case_eq_if_thms}
           |> morph_ctr_sugar (substitute_noted_thm noted);
       in
         (ctr_sugar, lthy' |> register_ctr_sugar plugins ctr_sugar)
@@ -1054,13 +1063,13 @@
     (goalss, after_qed, lthy')
   end;
 
-fun free_constructors tacss = (fn (goalss, after_qed, lthy) =>
+fun free_constructors kind tacss = (fn (goalss, after_qed, lthy) =>
   map2 (map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])) goalss tacss
-  |> (fn thms => after_qed thms lthy)) oo prepare_free_constructors (K I) (K I);
+  |> (fn thms => after_qed thms lthy)) oo prepare_free_constructors kind (K I) (K I);
 
-val free_constructors_cmd = (fn (goalss, after_qed, lthy) =>
+fun free_constructors_cmd kind = (fn (goalss, after_qed, lthy) =>
   Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
-  prepare_free_constructors Plugin_Name.make_filter Syntax.read_term;
+  prepare_free_constructors kind Plugin_Name.make_filter Syntax.read_term;
 
 val parse_bound_term = Parse.binding --| @{keyword ":"} -- Parse.term;
 
@@ -1089,6 +1098,6 @@
     "register an existing freely generated type's constructors"
     (parse_ctr_options -- Parse.binding --| @{keyword "for"} -- parse_ctr_specs
        -- parse_sel_default_eqs
-     >> free_constructors_cmd);
+     >> free_constructors_cmd Unknown);
 
 end;
diff -r eb98d1971d2a -r 69571f0a93df src/HOL/Tools/Old_Datatype/old_datatype_data.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Tue Oct 14 15:39:57 2014 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Tue Oct 14 16:17:34 2014 +0200
@@ -97,7 +97,8 @@
 fun ctr_sugar_of_info ({exhaust, nchotomy, inject, distinct, case_rewrites, case_cong,
     case_cong_weak, split, split_asm, ...} : Old_Datatype_Aux.info) =
   let val ctrs as ctr1 :: _ = ctrs_of_exhaust exhaust in
-    {T = body_type (fastype_of ctr1),
+    {kind = Ctr_Sugar.Datatype,
+     T = body_type (fastype_of ctr1),
      ctrs = ctrs,
      casex = case_of_case_rewrite (hd case_rewrites),
      discs = [],
diff -r eb98d1971d2a -r 69571f0a93df src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Tue Oct 14 15:39:57 2014 +0200
+++ b/src/HOL/Tools/record.ML	Tue Oct 14 16:17:34 2014 +0200
@@ -1783,9 +1783,9 @@
 
 fun add_ctr_sugar ctr exhaust inject sel_thms =
   Ctr_Sugar.default_register_ctr_sugar_global (K true)
-    {T = body_type (fastype_of ctr), ctrs = [ctr], casex = Term.dummy, discs = [], selss = [],
-     exhaust = exhaust, nchotomy = Drule.dummy_thm, injects = [inject], distincts = [],
-     case_thms = [], case_cong = Drule.dummy_thm, case_cong_weak = Drule.dummy_thm,
+    {kind = Ctr_Sugar.Record, T = body_type (fastype_of ctr), ctrs = [ctr], casex = Term.dummy,
+     discs = [], selss = [], exhaust = exhaust, nchotomy = Drule.dummy_thm, injects = [inject],
+     distincts = [], case_thms = [], case_cong = Drule.dummy_thm, case_cong_weak = Drule.dummy_thm,
      split = Drule.dummy_thm, split_asm = Drule.dummy_thm, disc_defs = [], disc_thmss = [],
      discIs = [], sel_defs = [], sel_thmss = [sel_thms], distinct_discsss = [], exhaust_discs = [],
      exhaust_sels = [], collapses = [], expands = [], split_sels = [], split_sel_asms = [],