# HG changeset patch
# User blanchet
# Date 1346854673 -7200
# Node ID 68623861e0f27d908ad47cfe7415a9b80cd62a15
# Parent  e075733fa8c2f895194bf2a70f07a6ada39e6db1
print timing information

diff -r e075733fa8c2 -r 68623861e0f2 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 05 16:07:39 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 05 16:17:53 2012 +0200
@@ -66,7 +66,6 @@
     val _ = (case duplicates (op =) As of [] => ()
       | A :: _ => error ("Duplicate type parameter " ^ quote (Syntax.string_of_typ lthy A)));
 
-    (* TODO: print timing information for sugar *)
     (* TODO: use sort constraints on type args *)
     (* TODO: use mixfix *)
 
@@ -94,14 +93,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 = (case subtract (op =) As' (fold (fold (fold Term.add_tfreesT)) ctr_Tsss []) of
+    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'))));
 
-    (* TODO: check that no type variables occur in the rhss that's not in the lhss *)
-
-
     val (Bs, C) =
       lthy
       |> fold (fold (fn s => Variable.declare_typ (TFree (s, dummyS))) o type_args_of) specs
@@ -127,6 +124,8 @@
     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;
 
+    val timer = time (Timer.startRealTimer ());
+
     fun mk_unf_or_fld get_foldedT Ts t =
       let val Type (_, Ts0) = get_foldedT (fastype_of t) in
         Term.subst_atomic_types (Ts0 ~~ Ts) t
@@ -248,10 +247,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_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 =