# HG changeset patch
# User wenzelm
# Date 1346870173 -7200
# Node ID bf6f727cb3627b0f29e79c556260173869771115
# Parent  937a0fadddfb13c9a9c2b26ad259d9b02a9992c5# Parent  3d7a695385f1e4bf908829e6a650aa794a7e691b
merged

diff -r 3d7a695385f1 -r bf6f727cb362 src/HOL/Codatatype/Examples/Misc_Data.thy
--- a/src/HOL/Codatatype/Examples/Misc_Data.thy	Wed Sep 05 20:19:37 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Misc_Data.thy	Wed Sep 05 20:36:13 2012 +0200
@@ -61,8 +61,7 @@
   IH1 'b 'a | IH2 'c
 *)
 
-(* FIXME data 'b nofail1 = NF11 "'a \<times> 'b" | NF12 'b *)
-data_raw nofail1: 'a = "'a \<times> 'b + 'b"
+data 'b nofail1 = NF11 "'b nofail1 \<times> 'b" | NF12 'b
 data 'b nofail2 = NF2 "('b nofail2 \<times> 'b \<times> 'b nofail2 \<times> 'b) list"
 data 'b nofail3 = NF3 "'b \<times> ('b nofail3 \<times> 'b \<times> 'b nofail3 \<times> 'b) fset"
 data 'b nofail4 = NF4 "('b nofail3 \<times> ('b nofail3 \<times> 'b \<times> 'b nofail3 \<times> 'b) fset) list"
diff -r 3d7a695385f1 -r bf6f727cb362 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 05 20:19:37 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 05 20:36:13 2012 +0200
@@ -64,12 +64,9 @@
     val As' = map dest_TFree As;
 
     val _ = (case duplicates (op =) As of [] => ()
-      | T :: _ => error ("Duplicate type parameter " ^ quote (Syntax.string_of_typ lthy T)));
+      | A :: _ => error ("Duplicate type parameter " ^ quote (Syntax.string_of_typ lthy A)));
 
-    (* TODO: print timing information for sugar *)
-    (* TODO: check that no type variables occur in the rhss that's not in the lhss *)
     (* TODO: use sort constraints on type args *)
-    (* TODO: use mixfix *)
 
     val N = length specs;
 
@@ -95,6 +92,12 @@
     val sel_bindersss = map (map (map fst)) ctr_argsss;
     val ctr_Tsss = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss;
 
+    val rhs_As' = fold (fold (fold Term.add_tfreesT)) ctr_Tsss [];
+    val _ = (case subtract (op =) As' rhs_As' of
+        [] => ()
+      | A' :: _ => error ("Extra type variables on rhs: " ^
+          quote (Syntax.string_of_typ lthy (TFree A'))));
+
     val (Bs, C) =
       lthy
       |> fold (fold (fn s => Variable.declare_typ (TFree (s, dummyS))) o type_args_of) specs
@@ -118,7 +121,9 @@
     val eqs = map dest_TFree Bs ~~ sum_prod_TsBs;
 
     val ((raw_unfs, raw_flds, unf_flds, fld_unfs, fld_injects), lthy') =
-      fp_bnf (if gfp then bnf_gfp else bnf_lfp) bs As' eqs lthy;
+      fp_bnf (if gfp then bnf_gfp else bnf_lfp) bs mixfixes As' eqs lthy;
+
+    val timer = time (Timer.startRealTimer ());
 
     fun mk_unf_or_fld get_foldedT Ts t =
       let val Type (_, Ts0) = get_foldedT (fastype_of t) in
@@ -131,8 +136,8 @@
     val unfs = map (mk_unf As) raw_unfs;
     val flds = map (mk_fld As) raw_flds;
 
-    fun pour_sugar_on_type ((((((((((b, T), fld), unf), fld_unf), unf_fld), fld_inject),
-        ctr_binders), ctr_Tss), disc_binders), sel_binderss) no_defs_lthy =
+    fun pour_sugar_on_type (((((((((((b, T), fld), unf), fld_unf), unf_fld), fld_inject),
+        ctr_binders), ctr_mixfixes), ctr_Tss), disc_binders), sel_binderss) no_defs_lthy =
       let
         val n = length ctr_binders;
         val ks = 1 upto n;
@@ -159,9 +164,9 @@
           fold_rev Term.lambda (fs @ [v]) (mk_sum_caseN (uncurry_fs fs xss) $ (unf $ v));
 
         val (((raw_ctrs, raw_ctr_defs), (raw_case, raw_case_def)), (lthy', lthy)) = no_defs_lthy
-          |> apfst split_list o fold_map2 (fn b => fn rhs =>
-               Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), rhs)) #>> apsnd snd)
-             ctr_binders ctr_rhss
+          |> apfst split_list o fold_map3 (fn b => fn mx => fn rhs =>
+               Local_Theory.define ((b, mx), ((Thm.def_binding b, []), rhs)) #>> apsnd snd)
+             ctr_binders ctr_mixfixes ctr_rhss
           ||>> (Local_Theory.define ((case_binder, NoSyn), ((Thm.def_binding case_binder, []),
              case_rhs)) #>> apsnd snd)
           ||> `Local_Theory.restore;
@@ -241,10 +246,15 @@
         wrap_data tacss ((ctrs, casex), (disc_binders, sel_binderss)) lthy'
         |> (if gfp then sugar_gfp else sugar_lfp)
       end;
+
+    val lthy'' =
+      fold pour_sugar_on_type (bs ~~ Ts ~~ flds ~~ unfs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~
+        ctr_binderss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss) lthy';
+
+    val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
+      (if gfp then "co" else "") ^ "datatype"));
   in
-    lthy'
-    |> fold pour_sugar_on_type (bs ~~ Ts ~~ flds ~~ unfs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~
-      ctr_binderss ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss)
+    (timer; lthy'')
   end;
 
 fun data_cmd info specs lthy =
diff -r 3d7a695385f1 -r bf6f727cb362 src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 05 20:19:37 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 05 20:36:13 2012 +0200
@@ -98,11 +98,12 @@
 
   val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
 
-  val fp_bnf: (binding list -> (string * sort) list -> typ list list -> BNF_Def.BNF list ->
-    local_theory -> 'a) ->
-    binding list -> (string * sort) list -> ((string * sort) * typ) list -> local_theory -> 'a
-  val fp_bnf_cmd: (binding list -> (string * sort) list -> typ list list -> BNF_Def.BNF list ->
-    local_theory -> 'a) ->
+  val fp_bnf: (binding list -> mixfix list -> (string * sort) list -> typ list list ->
+    BNF_Def.BNF list -> local_theory -> 'a) ->
+    binding list -> mixfix list -> (string * sort) list -> ((string * sort) * typ) list ->
+    local_theory -> 'a
+  val fp_bnf_cmd: (binding list -> mixfix list -> (string * sort) list -> typ list list ->
+    BNF_Def.BNF list -> local_theory -> 'a) ->
     binding list * (string list * string list) -> local_theory -> 'a
 end;
 
@@ -259,7 +260,7 @@
 fun fp_sort lhss Ass = Library.sort (Term_Ord.typ_ord o pairself TFree)
   (subtract (op =) lhss (fold (fold (insert (op =))) Ass [])) @ lhss;
 
-fun mk_fp_bnf timer construct bs resBs sort lhss bnfs deadss livess unfold lthy =
+fun mk_fp_bnf timer construct bs mixfixes resBs sort lhss bnfs deadss livess unfold lthy =
   let
     val name = fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "";
     fun qualify i bind =
@@ -289,14 +290,14 @@
 
     val timer = time (timer "Normalization & sealing of BNFs");
 
-    val res = construct bs resDs Dss bnfs'' lthy'';
+    val res = construct bs mixfixes resDs Dss bnfs'' lthy'';
 
     val timer = time (timer "FP construction in total");
   in
     res
   end;
 
-fun fp_bnf construct bs resBs eqs lthy =
+fun fp_bnf construct bs mixfixes resBs eqs lthy =
   let
     val timer = time (Timer.startRealTimer ());
     val (lhss, rhss) = split_list eqs;
@@ -305,7 +306,7 @@
       (fold_map2 (fn b => bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort) bs rhss
         (empty_unfold, lthy));
   in
-    mk_fp_bnf timer construct bs resBs sort lhss bnfs Dss Ass unfold lthy'
+    mk_fp_bnf timer construct bs mixfixes resBs sort lhss bnfs Dss Ass unfold lthy'
   end;
 
 fun fp_bnf_cmd construct (bs, (raw_lhss, raw_bnfs)) lthy =
@@ -318,7 +319,7 @@
         (bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort (Syntax.read_typ lthy rawT)))
         bs raw_bnfs (empty_unfold, lthy));
   in
-    mk_fp_bnf timer construct bs [] sort lhss bnfs Dss Ass unfold lthy'
+    mk_fp_bnf timer construct bs (map (K NoSyn) bs) [] sort lhss bnfs Dss Ass unfold lthy'
   end;
 
 end;
diff -r 3d7a695385f1 -r bf6f727cb362 src/HOL/Codatatype/Tools/bnf_gfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Wed Sep 05 20:19:37 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Wed Sep 05 20:36:13 2012 +0200
@@ -9,8 +9,9 @@
 
 signature BNF_GFP =
 sig
-  val bnf_gfp: binding list -> (string * sort) list -> typ list list -> BNF_Def.BNF list ->
-    local_theory -> (term list * term list * thm list * thm list * thm list) * local_theory
+  val bnf_gfp: binding list -> mixfix list -> (string * sort) list -> typ list list ->
+    BNF_Def.BNF list -> local_theory ->
+    (term list * term list * thm list * thm list * thm list) * local_theory
 end;
 
 structure BNF_GFP : BNF_GFP =
@@ -52,7 +53,7 @@
      ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;
 
 (*all bnfs have the same lives*)
-fun bnf_gfp bs resDs Dss_insts bnfs lthy =
+fun bnf_gfp bs mixfixes resDs Dss_insts bnfs lthy =
   let
     val timer = time (Timer.startRealTimer ());
 
@@ -1830,9 +1831,9 @@
 
     val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
       lthy
-      |> fold_map3 (fn b => fn car_final => fn in_car_final =>
-        typedef false NONE (b, params, NoSyn) car_final NONE
-          (EVERY' [rtac exI, rtac in_car_final] 1)) bs car_finals in_car_final_thms
+      |> fold_map4 (fn b => fn mx => fn car_final => fn in_car_final =>
+        typedef false NONE (b, params, mx) car_final NONE
+          (EVERY' [rtac exI, rtac in_car_final] 1)) bs mixfixes car_finals in_car_final_thms
       |>> apsnd split_list o split_list;
 
     val Ts = map (fn name => Type (name, params')) T_names;
diff -r 3d7a695385f1 -r bf6f727cb362 src/HOL/Codatatype/Tools/bnf_lfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 05 20:19:37 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 05 20:36:13 2012 +0200
@@ -8,8 +8,9 @@
 
 signature BNF_LFP =
 sig
-  val bnf_lfp: binding list -> (string * sort) list -> typ list list -> BNF_Def.BNF list ->
-    local_theory -> (term list * term list * thm list * thm list * thm list) * local_theory
+  val bnf_lfp: binding list -> mixfix list -> (string * sort) list -> typ list list ->
+    BNF_Def.BNF list -> local_theory ->
+    (term list * term list * thm list * thm list * thm list) * local_theory
 end;
 
 structure BNF_LFP : BNF_LFP =
@@ -23,7 +24,7 @@
 open BNF_LFP_Tactics
 
 (*all bnfs have the same lives*)
-fun bnf_lfp bs resDs Dss_insts bnfs lthy =
+fun bnf_lfp bs mixfixes resDs Dss_insts bnfs lthy =
   let
     val timer = time (Timer.startRealTimer ());
     val live = live_of_bnf (hd bnfs);
@@ -927,9 +928,9 @@
 
     val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
       lthy
-      |> fold_map2 (fn b => fn car_init => typedef true NONE (b, params, NoSyn) car_init NONE
+      |> fold_map3 (fn b => fn mx => fn car_init => typedef true NONE (b, params, mx) car_init NONE
           (EVERY' [rtac ssubst, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms,
-            rtac alg_init_thm] 1)) bs car_inits
+            rtac alg_init_thm] 1)) bs mixfixes car_inits
       |>> apsnd split_list o split_list;
 
     val Ts = map (fn name => Type (name, params')) T_names;
diff -r 3d7a695385f1 -r bf6f727cb362 src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Wed Sep 05 20:19:37 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Wed Sep 05 20:36:13 2012 +0200
@@ -97,8 +97,6 @@
 val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
 
 fun mk_split_asm_tac ctxt split =
-  rtac (split RS trans) 1 THEN
-  Local_Defs.unfold_tac ctxt split_asm_thms THEN
-  rtac refl 1;
+  rtac (split RS trans) 1 THEN Local_Defs.unfold_tac ctxt split_asm_thms THEN rtac refl 1;
 
 end;