print timing information
authorblanchet
Wed Sep 05 16:17:53 2012 +0200 (2012-09-05)
changeset 4916768623861e0f2
parent 49166 e075733fa8c2
child 49168 766a09b84562
print timing information
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 05 16:07:39 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 05 16:17:53 2012 +0200
     1.3 @@ -66,7 +66,6 @@
     1.4      val _ = (case duplicates (op =) As of [] => ()
     1.5        | A :: _ => error ("Duplicate type parameter " ^ quote (Syntax.string_of_typ lthy A)));
     1.6  
     1.7 -    (* TODO: print timing information for sugar *)
     1.8      (* TODO: use sort constraints on type args *)
     1.9      (* TODO: use mixfix *)
    1.10  
    1.11 @@ -94,14 +93,12 @@
    1.12      val sel_bindersss = map (map (map fst)) ctr_argsss;
    1.13      val ctr_Tsss = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss;
    1.14  
    1.15 -    val rhs_As = (case subtract (op =) As' (fold (fold (fold Term.add_tfreesT)) ctr_Tsss []) of
    1.16 +    val rhs_As' = fold (fold (fold Term.add_tfreesT)) ctr_Tsss [];
    1.17 +    val _ = (case subtract (op =) As' rhs_As' of
    1.18          [] => ()
    1.19        | A' :: _ => error ("Extra type variables on rhs: " ^
    1.20            quote (Syntax.string_of_typ lthy (TFree A'))));
    1.21  
    1.22 -    (* TODO: check that no type variables occur in the rhss that's not in the lhss *)
    1.23 -
    1.24 -
    1.25      val (Bs, C) =
    1.26        lthy
    1.27        |> fold (fold (fn s => Variable.declare_typ (TFree (s, dummyS))) o type_args_of) specs
    1.28 @@ -127,6 +124,8 @@
    1.29      val ((raw_unfs, raw_flds, unf_flds, fld_unfs, fld_injects), lthy') =
    1.30        fp_bnf (if gfp then bnf_gfp else bnf_lfp) bs As' eqs lthy;
    1.31  
    1.32 +    val timer = time (Timer.startRealTimer ());
    1.33 +
    1.34      fun mk_unf_or_fld get_foldedT Ts t =
    1.35        let val Type (_, Ts0) = get_foldedT (fastype_of t) in
    1.36          Term.subst_atomic_types (Ts0 ~~ Ts) t
    1.37 @@ -248,10 +247,15 @@
    1.38          wrap_data tacss ((ctrs, casex), (disc_binders, sel_binderss)) lthy'
    1.39          |> (if gfp then sugar_gfp else sugar_lfp)
    1.40        end;
    1.41 +
    1.42 +    val lthy'' =
    1.43 +      fold pour_sugar_on_type (bs ~~ Ts ~~ flds ~~ unfs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~
    1.44 +        ctr_binderss ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss) lthy'
    1.45 +
    1.46 +    val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
    1.47 +      (if gfp then "co" else "") ^ "datatype"));
    1.48    in
    1.49 -    lthy'
    1.50 -    |> fold pour_sugar_on_type (bs ~~ Ts ~~ flds ~~ unfs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~
    1.51 -      ctr_binderss ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss)
    1.52 +    (timer; lthy'')
    1.53    end;
    1.54  
    1.55  fun data_cmd info specs lthy =