optional timing for code generator conversions
authorhaftmann
Thu May 26 15:27:50 2016 +0200 (2016-05-26)
changeset 6316472aaf69328fc
parent 63163 b561284a4214
child 63165 c12845e8e80a
optional timing for code generator conversions
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_simp.ML
src/Tools/Code/code_target.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/Tools/Code/code_preproc.ML	Thu May 26 15:27:50 2016 +0200
     1.2 +++ b/src/Tools/Code/code_preproc.ML	Thu May 26 15:27:50 2016 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4    val sortargs: code_graph -> string -> sort list
     1.5    val all: code_graph -> string list
     1.6    val pretty: Proof.context -> code_graph -> Pretty.T
     1.7 -  val obtain: bool -> Proof.context -> string list -> term list ->
     1.8 +  val obtain: bool -> { ctxt: Proof.context, consts: string list, terms: term list } ->
     1.9      { algebra: code_algebra, eqngr: code_graph }
    1.10    val dynamic_conv: Proof.context
    1.11      -> (code_algebra -> code_graph -> term -> conv) -> conv
    1.12 @@ -38,11 +38,41 @@
    1.13    val trace_all: Context.generic -> Context.generic
    1.14    val trace_only: string list -> Context.generic -> Context.generic
    1.15    val trace_only_ext: string list -> Context.generic -> Context.generic
    1.16 +
    1.17 +  val timing: bool Config.T
    1.18 +  val timed: string -> ('a -> Proof.context) -> ('a -> 'b) -> 'a -> 'b
    1.19 +  val timed_exec: string -> (unit -> 'a) -> Proof.context -> 'a
    1.20 +  val timed_conv: string -> (Proof.context -> conv) -> Proof.context -> conv
    1.21 +  val timed_value: string -> (Proof.context -> term -> 'a) -> Proof.context -> term -> 'a
    1.22  end
    1.23  
    1.24  structure Code_Preproc : CODE_PREPROC =
    1.25  struct
    1.26  
    1.27 +(** timing **)
    1.28 +
    1.29 +val timing = Attrib.setup_config_bool @{binding code_timing} (K false);
    1.30 +
    1.31 +fun timed msg ctxt_of f x =
    1.32 +  if Config.get (ctxt_of x) timing
    1.33 +  then timeap_msg msg f x
    1.34 +  else f x;
    1.35 +
    1.36 +fun timed_exec msg f ctxt =
    1.37 +  if Config.get ctxt timing
    1.38 +  then timeap_msg msg f ()
    1.39 +  else f ();
    1.40 +
    1.41 +fun timed' msg f ctxt x =
    1.42 +  if Config.get ctxt timing
    1.43 +  then timeap_msg msg (f ctxt) x
    1.44 +  else f ctxt x;
    1.45 +
    1.46 +val timed_conv = timed';
    1.47 +val timed_value = timed';
    1.48 +
    1.49 +
    1.50 +
    1.51  (** preprocessor administration **)
    1.52  
    1.53  (* theory data *)
    1.54 @@ -212,7 +242,10 @@
    1.55      fun post_conv ctxt'' =
    1.56        Axclass.overload_conv ctxt''
    1.57        #> trans_conv_rule (Simplifier.rewrite (put_simpset post ctxt''))
    1.58 -  in fn ctxt' => pre_conv ctxt' #> pair post_conv end;
    1.59 +  in
    1.60 +    fn ctxt' => timed_conv "preprocessing term" pre_conv ctxt'
    1.61 +      #> pair (timed_conv "postprocessing term" post_conv)
    1.62 +  end;
    1.63  
    1.64  fun simplifier_sandwich ctxt =
    1.65    Sandwich.lift (simplifier_conv_sandwich ctxt);
    1.66 @@ -550,20 +583,22 @@
    1.67    * "evaluation" is a lifting of an evaluator
    1.68  *)
    1.69  
    1.70 -fun obtain ignore_cache ctxt consts ts = apsnd snd
    1.71 -  (Wellsorted.change_yield (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt))
    1.72 -    (extend_arities_eqngr ctxt consts ts))
    1.73 -  |> (fn (algebra, eqngr) => { algebra = algebra, eqngr = eqngr });
    1.74 +fun obtain ignore_cache =
    1.75 +  timed "preprocessing equations" #ctxt (fn { ctxt, consts, terms } =>
    1.76 +    apsnd snd (Wellsorted.change_yield
    1.77 +    (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt))
    1.78 +    (extend_arities_eqngr ctxt consts terms)))
    1.79 +  #> (fn (algebra, eqngr) => { algebra = algebra, eqngr = eqngr });
    1.80  
    1.81  fun dynamic_evaluation eval ctxt t =
    1.82    let
    1.83      val consts = fold_aterms
    1.84        (fn Const (c, _) => insert (op =) c | _ => I) t [];
    1.85 -    val { algebra, eqngr } = obtain false ctxt consts [t];
    1.86 +    val { algebra, eqngr } = obtain false { ctxt = ctxt, consts = consts, terms = [t] };
    1.87    in eval algebra eqngr t end;
    1.88  
    1.89  fun static_evaluation ctxt consts eval =
    1.90 -  eval (obtain true ctxt consts []);
    1.91 +  eval (obtain true { ctxt = ctxt, consts = consts, terms = [] });
    1.92  
    1.93  fun dynamic_conv ctxt conv =
    1.94    Sandwich.conversion (value_sandwich ctxt)
     2.1 --- a/src/Tools/Code/code_runtime.ML	Thu May 26 15:27:50 2016 +0200
     2.2 +++ b/src/Tools/Code/code_runtime.ML	Thu May 26 15:27:50 2016 +0200
     2.3 @@ -80,9 +80,10 @@
     2.4  
     2.5  fun compile_ML verbose code context =
     2.6   (if Config.get_generic context trace then tracing code else ();
     2.7 -  ML_Context.exec (fn () => ML_Compiler0.ML ML_Env.context
     2.8 +  Code_Preproc.timed "compiling ML" Context.proof_of
     2.9 +    (ML_Context.exec (fn () => ML_Compiler0.ML ML_Env.context
    2.10      {line = 0, file = "generated code", verbose = verbose,
    2.11 -       debug = false} code) context);
    2.12 +       debug = false} code)) context);
    2.13  
    2.14  fun value ctxt (get, put, put_ml) (prelude, value) =
    2.15    let
    2.16 @@ -92,7 +93,8 @@
    2.17      val ctxt' = ctxt
    2.18        |> put (fn () => error ("Bad computation for " ^ quote put_ml))
    2.19        |> Context.proof_map (compile_ML false code);
    2.20 -  in get ctxt' () end;
    2.21 +    val computator = get ctxt';
    2.22 +  in Code_Preproc.timed_exec "running ML" computator ctxt' end;
    2.23  
    2.24  
    2.25  (* computation as evaluation into ML language values *)
    2.26 @@ -300,7 +302,10 @@
    2.27      val ml_name_for_const = the o AList.lookup (op =) const_map;
    2.28      val (ml_names, of_term_code) = print_of_term ctxt ml_name_for_const T cTs
    2.29      val of_term = value ctxt cookie (context_code ^ "\n" ^ of_term_code, List.last ml_names);
    2.30 -  in fn ctxt' => fn t => fn _ => fn _ => Exn.interruptible_capture (of_term ctxt') t end;
    2.31 +  in
    2.32 +    Code_Preproc.timed_value "computing" 
    2.33 +      (fn ctxt' => fn t => fn _ => fn _ => Exn.interruptible_capture (of_term ctxt') t)
    2.34 +  end;
    2.35  
    2.36  fun fully_static_value_exn cookie { ctxt, lift_postproc, consts, T } =
    2.37    let
     3.1 --- a/src/Tools/Code/code_simp.ML	Thu May 26 15:27:50 2016 +0200
     3.2 +++ b/src/Tools/Code/code_simp.ML	Thu May 26 15:27:50 2016 +0200
     3.3 @@ -30,9 +30,11 @@
     3.4    val merge = merge_ss;
     3.5  );
     3.6  
     3.7 -fun map_ss f thy = Simpset.map (simpset_map (Proof_Context.init_global thy) f) thy;
     3.8 +fun map_ss f thy =
     3.9 +  Simpset.map (simpset_map (Proof_Context.init_global thy) f) thy;
    3.10  
    3.11 -fun simpset_default ctxt some_ss = the_default (Simpset.get (Proof_Context.theory_of ctxt)) some_ss;
    3.12 +fun simpset_default ctxt some_ss =
    3.13 +  the_default (Simpset.get (Proof_Context.theory_of ctxt)) some_ss;
    3.14  
    3.15  
    3.16  (* diagnostic *)
    3.17 @@ -60,13 +62,18 @@
    3.18  
    3.19  val add_program = Code_Symbol.Graph.fold (add_stmt o fst o snd);
    3.20  
    3.21 -fun simpset_program ctxt some_ss program =
    3.22 -  simpset_map ctxt (add_program program) (simpset_default ctxt some_ss);
    3.23 +val simpset_program =
    3.24 +  Code_Preproc.timed "building simpset" #ctxt
    3.25 +  (fn { ctxt, some_ss, program } => simpset_map ctxt (add_program program) (simpset_default ctxt some_ss));
    3.26  
    3.27  fun rewrite_modulo ctxt some_ss program =
    3.28    let
    3.29 -    val ss = simpset_program ctxt some_ss program;
    3.30 -  in fn ctxt => Simplifier.full_rewrite (ctxt |> put_simpset ss |> set_trace) end;
    3.31 +    val ss = simpset_program
    3.32 +      { ctxt = ctxt, some_ss = some_ss, program = program };
    3.33 +  in fn ctxt => 
    3.34 +    Code_Preproc.timed_conv "simplifying"
    3.35 +      Simplifier.full_rewrite (ctxt |> put_simpset ss |> set_trace)
    3.36 +  end;
    3.37  
    3.38  fun conclude_tac ctxt some_ss =
    3.39    let
    3.40 @@ -95,7 +102,9 @@
    3.41  
    3.42  fun static_conv { ctxt, simpset, consts } =
    3.43    Code_Thingol.static_conv_isa { ctxt = ctxt, consts = consts }
    3.44 -    (fn program => K o rewrite_modulo ctxt simpset program);
    3.45 +    (fn program => let
    3.46 +       val conv = rewrite_modulo ctxt simpset program
    3.47 +     in fn ctxt => fn _ => conv ctxt end);
    3.48  
    3.49  fun static_tac { ctxt, simpset, consts } =
    3.50    let
     4.1 --- a/src/Tools/Code/code_target.ML	Thu May 26 15:27:50 2016 +0200
     4.2 +++ b/src/Tools/Code/code_target.ML	Thu May 26 15:27:50 2016 +0200
     4.3 @@ -343,7 +343,10 @@
     4.4        else (check_name true raw_module_name; raw_module_name)
     4.5      val (mounted_serializer, (prepared_syms, prepared_program)) =
     4.6        mount_serializer ctxt target_name some_width module_name args program syms;
     4.7 -  in mounted_serializer prepared_program (if all_public then [] else prepared_syms) end;
     4.8 +  in
     4.9 +    Code_Preproc.timed_exec "serializing"
    4.10 +      (fn () => mounted_serializer prepared_program (if all_public then [] else prepared_syms)) ctxt
    4.11 +  end;
    4.12  
    4.13  fun assert_module_name "" = error "Empty module name not allowed here"
    4.14    | assert_module_name module_name = module_name;
    4.15 @@ -417,7 +420,10 @@
    4.16    let
    4.17      val (mounted_serializer, (_, prepared_program)) =
    4.18        mount_serializer ctxt target_name NONE generatedN [] program syms;
    4.19 -  in dynamic_computation_text mounted_serializer prepared_program syms end;
    4.20 +  in
    4.21 +    Code_Preproc.timed_exec "serializing"
    4.22 +    (fn () => dynamic_computation_text mounted_serializer prepared_program syms) ctxt
    4.23 +  end;
    4.24  
    4.25  end; (* local *)
    4.26  
     5.1 --- a/src/Tools/Code/code_thingol.ML	Thu May 26 15:27:50 2016 +0200
     5.2 +++ b/src/Tools/Code/code_thingol.ML	Thu May 26 15:27:50 2016 +0200
     5.3 @@ -786,15 +786,17 @@
     5.4  
     5.5  (* program generation *)
     5.6  
     5.7 -fun invoke_generation_for_consts ctxt { ignore_cache, permissive }
     5.8 -  { algebra, eqngr } consts =
     5.9 -  invoke_generation ignore_cache ctxt
    5.10 -    (fold_map (ensure_const ctxt algebra eqngr permissive)) consts;
    5.11 +fun invoke_generation_for_consts ctxt { ignore_cache, permissive } { algebra, eqngr } consts =
    5.12 +  Code_Preproc.timed "translating program" #ctxt
    5.13 +  (fn { ctxt, algebra, eqngr, consts } => invoke_generation ignore_cache ctxt
    5.14 +    (fold_map (ensure_const ctxt algebra eqngr permissive)) consts)
    5.15 +    { ctxt = ctxt, algebra = algebra, eqngr = eqngr, consts = consts };
    5.16  
    5.17  fun invoke_generation_for_consts' ctxt ignore_cache_and_permissive consts =
    5.18    invoke_generation_for_consts ctxt
    5.19      { ignore_cache = ignore_cache_and_permissive, permissive = ignore_cache_and_permissive }
    5.20 -    (Code_Preproc.obtain ignore_cache_and_permissive ctxt consts []) consts
    5.21 +    (Code_Preproc.obtain ignore_cache_and_permissive
    5.22 +      { ctxt = ctxt, consts = consts, terms = []}) consts
    5.23    |> snd;
    5.24  
    5.25  fun invoke_generation_for_consts'' ctxt algebra_eqngr =
    5.26 @@ -850,7 +852,10 @@
    5.27  fun dynamic_evaluation eval ctxt algebra eqngr t =
    5.28    let
    5.29      val ((program, (vs_ty_t', deps)), _) =
    5.30 -      invoke_generation false ctxt (ensure_value ctxt algebra eqngr) t;
    5.31 +      Code_Preproc.timed "translating term" #ctxt
    5.32 +      (fn { ctxt, algebra, eqngr, t } =>
    5.33 +        invoke_generation false ctxt (ensure_value ctxt algebra eqngr) t)
    5.34 +        { ctxt = ctxt, algebra = algebra, eqngr = eqngr, t = t };
    5.35    in eval program t vs_ty_t' deps end;
    5.36  
    5.37  fun dynamic_conv ctxt conv =
    5.38 @@ -869,7 +874,10 @@
    5.39      fun evaluation program dynamic_eval ctxt t =
    5.40        let
    5.41          val ((_, ((vs_ty', t'), deps)), _) =
    5.42 -          ensure_value ctxt algebra eqngr t ([], program);
    5.43 +          Code_Preproc.timed "translating term" #ctxt
    5.44 +          (fn { ctxt, t } =>
    5.45 +            ensure_value ctxt algebra eqngr t ([], program))
    5.46 +            { ctxt = ctxt, t = t };
    5.47        in dynamic_eval ctxt t (vs_ty', t') deps end;
    5.48    in
    5.49      static_evaluation ctxt consts algebra_eqngr (fn program_deps =>
    5.50 @@ -935,7 +943,8 @@
    5.51  
    5.52  fun code_depgr ctxt consts =
    5.53    let
    5.54 -    val { eqngr, ... } = Code_Preproc.obtain true ctxt consts [];
    5.55 +    val { eqngr, ... } = Code_Preproc.obtain true
    5.56 +      { ctxt = ctxt, consts = consts, terms = [] };
    5.57      val all_consts = Graph.all_succs eqngr consts;
    5.58    in Graph.restrict (member (op =) all_consts) eqngr end;
    5.59  
     6.1 --- a/src/Tools/nbe.ML	Thu May 26 15:27:50 2016 +0200
     6.2 +++ b/src/Tools/nbe.ML	Thu May 26 15:27:50 2016 +0200
     6.3 @@ -8,8 +8,10 @@
     6.4  sig
     6.5    val dynamic_conv: Proof.context -> conv
     6.6    val dynamic_value: Proof.context -> term -> term
     6.7 -  val static_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv
     6.8 -  val static_value: { ctxt: Proof.context, consts: string list } -> Proof.context -> term -> term
     6.9 +  val static_conv: { ctxt: Proof.context, consts: string list }
    6.10 +    -> Proof.context -> conv
    6.11 +  val static_value: { ctxt: Proof.context, consts: string list }
    6.12 +    -> Proof.context -> term -> term
    6.13  
    6.14    datatype Univ =
    6.15        Const of int * Univ list               (*named (uninterpreted) constants*)
    6.16 @@ -21,7 +23,8 @@
    6.17                                               (*abstractions as closures*)
    6.18    val same: Univ * Univ -> bool
    6.19  
    6.20 -  val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context
    6.21 +  val put_result: (unit -> Univ list -> Univ list)
    6.22 +    -> Proof.context -> Proof.context
    6.23    val trace: bool Config.T
    6.24  
    6.25    val add_const_alias: thm -> theory -> theory
    6.26 @@ -477,7 +480,7 @@
    6.27        #-> fold (fn (name, univ) => (Code_Symbol.Graph.map_node name o apfst) (K (SOME univ))))
    6.28    end;
    6.29  
    6.30 -fun compile_program ctxt program =
    6.31 +fun compile_program { ctxt, program } =
    6.32    let
    6.33      fun add_stmts names (nbe_program, (maxidx, idx_tab)) = if exists ((can o Code_Symbol.Graph.get_node) nbe_program) names
    6.34        then (nbe_program, (maxidx, idx_tab))
    6.35 @@ -554,7 +557,7 @@
    6.36        if null (Term.add_tvars t' []) then t'
    6.37        else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t');
    6.38    in
    6.39 -    compile_and_reconstruct_term
    6.40 +    Code_Preproc.timed "computing NBE expression" #ctxt compile_and_reconstruct_term
    6.41        { ctxt = ctxt, nbe_program = nbe_program, idx_tab = idx_tab, deps = deps, term = (vs, t) }
    6.42      |> traced ctxt (fn t => "Normalized:\n" ^ string_of_term t)
    6.43      |> type_infer
    6.44 @@ -576,7 +579,8 @@
    6.45    let
    6.46      val (nbe_program, (_, idx_tab)) =
    6.47        Nbe_Functions.change (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt))
    6.48 -        (compile_program ctxt program);
    6.49 +        (Code_Preproc.timed "compiling NBE program" #ctxt
    6.50 +          compile_program { ctxt = ctxt, program = program });
    6.51    in (nbe_program, idx_tab) end;
    6.52  
    6.53  
    6.54 @@ -608,13 +612,13 @@
    6.55  fun static_conv (ctxt_consts as { ctxt, ... }) =
    6.56    let
    6.57      val conv = Code_Thingol.static_conv_thingol ctxt_consts
    6.58 -      (fn { program, ... } => oracle (compile true ctxt program));
    6.59 +      (fn { program, deps = _ } => oracle (compile true ctxt program));
    6.60    in fn ctxt' => lift_triv_classes_conv ctxt' conv end;
    6.61  
    6.62  fun static_value { ctxt, consts } =
    6.63    let
    6.64      val comp = Code_Thingol.static_value { ctxt = ctxt, lift_postproc = I, consts = consts }
    6.65 -      (fn { program, ... } => normalize_term (compile false ctxt program));
    6.66 +      (fn { program, deps = _ } => normalize_term (compile false ctxt program));
    6.67    in fn ctxt' => lift_triv_classes_rew ctxt' (comp ctxt') end;
    6.68  
    6.69  end;