# HG changeset patch
# User haftmann
# Date 1464269270 -7200
# Node ID 72aaf69328fc627bf467bb9feacf07cfa0316386
# Parent  b561284a4214884e8a68024fa0046b2b66e988af
optional timing for code generator conversions

diff -r b561284a4214 -r 72aaf69328fc src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/Tools/Code/code_preproc.ML	Thu May 26 15:27:50 2016 +0200
@@ -21,7 +21,7 @@
   val sortargs: code_graph -> string -> sort list
   val all: code_graph -> string list
   val pretty: Proof.context -> code_graph -> Pretty.T
-  val obtain: bool -> Proof.context -> string list -> term list ->
+  val obtain: bool -> { ctxt: Proof.context, consts: string list, terms: term list } ->
     { algebra: code_algebra, eqngr: code_graph }
   val dynamic_conv: Proof.context
     -> (code_algebra -> code_graph -> term -> conv) -> conv
@@ -38,11 +38,41 @@
   val trace_all: Context.generic -> Context.generic
   val trace_only: string list -> Context.generic -> Context.generic
   val trace_only_ext: string list -> Context.generic -> Context.generic
+
+  val timing: bool Config.T
+  val timed: string -> ('a -> Proof.context) -> ('a -> 'b) -> 'a -> 'b
+  val timed_exec: string -> (unit -> 'a) -> Proof.context -> 'a
+  val timed_conv: string -> (Proof.context -> conv) -> Proof.context -> conv
+  val timed_value: string -> (Proof.context -> term -> 'a) -> Proof.context -> term -> 'a
 end
 
 structure Code_Preproc : CODE_PREPROC =
 struct
 
+(** timing **)
+
+val timing = Attrib.setup_config_bool @{binding code_timing} (K false);
+
+fun timed msg ctxt_of f x =
+  if Config.get (ctxt_of x) timing
+  then timeap_msg msg f x
+  else f x;
+
+fun timed_exec msg f ctxt =
+  if Config.get ctxt timing
+  then timeap_msg msg f ()
+  else f ();
+
+fun timed' msg f ctxt x =
+  if Config.get ctxt timing
+  then timeap_msg msg (f ctxt) x
+  else f ctxt x;
+
+val timed_conv = timed';
+val timed_value = timed';
+
+
+
 (** preprocessor administration **)
 
 (* theory data *)
@@ -212,7 +242,10 @@
     fun post_conv ctxt'' =
       Axclass.overload_conv ctxt''
       #> trans_conv_rule (Simplifier.rewrite (put_simpset post ctxt''))
-  in fn ctxt' => pre_conv ctxt' #> pair post_conv end;
+  in
+    fn ctxt' => timed_conv "preprocessing term" pre_conv ctxt'
+      #> pair (timed_conv "postprocessing term" post_conv)
+  end;
 
 fun simplifier_sandwich ctxt =
   Sandwich.lift (simplifier_conv_sandwich ctxt);
@@ -550,20 +583,22 @@
   * "evaluation" is a lifting of an evaluator
 *)
 
-fun obtain ignore_cache ctxt consts ts = apsnd snd
-  (Wellsorted.change_yield (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt))
-    (extend_arities_eqngr ctxt consts ts))
-  |> (fn (algebra, eqngr) => { algebra = algebra, eqngr = eqngr });
+fun obtain ignore_cache =
+  timed "preprocessing equations" #ctxt (fn { ctxt, consts, terms } =>
+    apsnd snd (Wellsorted.change_yield
+    (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt))
+    (extend_arities_eqngr ctxt consts terms)))
+  #> (fn (algebra, eqngr) => { algebra = algebra, eqngr = eqngr });
 
 fun dynamic_evaluation eval ctxt t =
   let
     val consts = fold_aterms
       (fn Const (c, _) => insert (op =) c | _ => I) t [];
-    val { algebra, eqngr } = obtain false ctxt consts [t];
+    val { algebra, eqngr } = obtain false { ctxt = ctxt, consts = consts, terms = [t] };
   in eval algebra eqngr t end;
 
 fun static_evaluation ctxt consts eval =
-  eval (obtain true ctxt consts []);
+  eval (obtain true { ctxt = ctxt, consts = consts, terms = [] });
 
 fun dynamic_conv ctxt conv =
   Sandwich.conversion (value_sandwich ctxt)
diff -r b561284a4214 -r 72aaf69328fc src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/Tools/Code/code_runtime.ML	Thu May 26 15:27:50 2016 +0200
@@ -80,9 +80,10 @@
 
 fun compile_ML verbose code context =
  (if Config.get_generic context trace then tracing code else ();
-  ML_Context.exec (fn () => ML_Compiler0.ML ML_Env.context
+  Code_Preproc.timed "compiling ML" Context.proof_of
+    (ML_Context.exec (fn () => ML_Compiler0.ML ML_Env.context
     {line = 0, file = "generated code", verbose = verbose,
-       debug = false} code) context);
+       debug = false} code)) context);
 
 fun value ctxt (get, put, put_ml) (prelude, value) =
   let
@@ -92,7 +93,8 @@
     val ctxt' = ctxt
       |> put (fn () => error ("Bad computation for " ^ quote put_ml))
       |> Context.proof_map (compile_ML false code);
-  in get ctxt' () end;
+    val computator = get ctxt';
+  in Code_Preproc.timed_exec "running ML" computator ctxt' end;
 
 
 (* computation as evaluation into ML language values *)
@@ -300,7 +302,10 @@
     val ml_name_for_const = the o AList.lookup (op =) const_map;
     val (ml_names, of_term_code) = print_of_term ctxt ml_name_for_const T cTs
     val of_term = value ctxt cookie (context_code ^ "\n" ^ of_term_code, List.last ml_names);
-  in fn ctxt' => fn t => fn _ => fn _ => Exn.interruptible_capture (of_term ctxt') t end;
+  in
+    Code_Preproc.timed_value "computing" 
+      (fn ctxt' => fn t => fn _ => fn _ => Exn.interruptible_capture (of_term ctxt') t)
+  end;
 
 fun fully_static_value_exn cookie { ctxt, lift_postproc, consts, T } =
   let
diff -r b561284a4214 -r 72aaf69328fc src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/Tools/Code/code_simp.ML	Thu May 26 15:27:50 2016 +0200
@@ -30,9 +30,11 @@
   val merge = merge_ss;
 );
 
-fun map_ss f thy = Simpset.map (simpset_map (Proof_Context.init_global thy) f) thy;
+fun map_ss f thy =
+  Simpset.map (simpset_map (Proof_Context.init_global thy) f) thy;
 
-fun simpset_default ctxt some_ss = the_default (Simpset.get (Proof_Context.theory_of ctxt)) some_ss;
+fun simpset_default ctxt some_ss =
+  the_default (Simpset.get (Proof_Context.theory_of ctxt)) some_ss;
 
 
 (* diagnostic *)
@@ -60,13 +62,18 @@
 
 val add_program = Code_Symbol.Graph.fold (add_stmt o fst o snd);
 
-fun simpset_program ctxt some_ss program =
-  simpset_map ctxt (add_program program) (simpset_default ctxt some_ss);
+val simpset_program =
+  Code_Preproc.timed "building simpset" #ctxt
+  (fn { ctxt, some_ss, program } => simpset_map ctxt (add_program program) (simpset_default ctxt some_ss));
 
 fun rewrite_modulo ctxt some_ss program =
   let
-    val ss = simpset_program ctxt some_ss program;
-  in fn ctxt => Simplifier.full_rewrite (ctxt |> put_simpset ss |> set_trace) end;
+    val ss = simpset_program
+      { ctxt = ctxt, some_ss = some_ss, program = program };
+  in fn ctxt => 
+    Code_Preproc.timed_conv "simplifying"
+      Simplifier.full_rewrite (ctxt |> put_simpset ss |> set_trace)
+  end;
 
 fun conclude_tac ctxt some_ss =
   let
@@ -95,7 +102,9 @@
 
 fun static_conv { ctxt, simpset, consts } =
   Code_Thingol.static_conv_isa { ctxt = ctxt, consts = consts }
-    (fn program => K o rewrite_modulo ctxt simpset program);
+    (fn program => let
+       val conv = rewrite_modulo ctxt simpset program
+     in fn ctxt => fn _ => conv ctxt end);
 
 fun static_tac { ctxt, simpset, consts } =
   let
diff -r b561284a4214 -r 72aaf69328fc src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/Tools/Code/code_target.ML	Thu May 26 15:27:50 2016 +0200
@@ -343,7 +343,10 @@
       else (check_name true raw_module_name; raw_module_name)
     val (mounted_serializer, (prepared_syms, prepared_program)) =
       mount_serializer ctxt target_name some_width module_name args program syms;
-  in mounted_serializer prepared_program (if all_public then [] else prepared_syms) end;
+  in
+    Code_Preproc.timed_exec "serializing"
+      (fn () => mounted_serializer prepared_program (if all_public then [] else prepared_syms)) ctxt
+  end;
 
 fun assert_module_name "" = error "Empty module name not allowed here"
   | assert_module_name module_name = module_name;
@@ -417,7 +420,10 @@
   let
     val (mounted_serializer, (_, prepared_program)) =
       mount_serializer ctxt target_name NONE generatedN [] program syms;
-  in dynamic_computation_text mounted_serializer prepared_program syms end;
+  in
+    Code_Preproc.timed_exec "serializing"
+    (fn () => dynamic_computation_text mounted_serializer prepared_program syms) ctxt
+  end;
 
 end; (* local *)
 
diff -r b561284a4214 -r 72aaf69328fc src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/Tools/Code/code_thingol.ML	Thu May 26 15:27:50 2016 +0200
@@ -786,15 +786,17 @@
 
 (* program generation *)
 
-fun invoke_generation_for_consts ctxt { ignore_cache, permissive }
-  { algebra, eqngr } consts =
-  invoke_generation ignore_cache ctxt
-    (fold_map (ensure_const ctxt algebra eqngr permissive)) consts;
+fun invoke_generation_for_consts ctxt { ignore_cache, permissive } { algebra, eqngr } consts =
+  Code_Preproc.timed "translating program" #ctxt
+  (fn { ctxt, algebra, eqngr, consts } => invoke_generation ignore_cache ctxt
+    (fold_map (ensure_const ctxt algebra eqngr permissive)) consts)
+    { ctxt = ctxt, algebra = algebra, eqngr = eqngr, consts = consts };
 
 fun invoke_generation_for_consts' ctxt ignore_cache_and_permissive consts =
   invoke_generation_for_consts ctxt
     { ignore_cache = ignore_cache_and_permissive, permissive = ignore_cache_and_permissive }
-    (Code_Preproc.obtain ignore_cache_and_permissive ctxt consts []) consts
+    (Code_Preproc.obtain ignore_cache_and_permissive
+      { ctxt = ctxt, consts = consts, terms = []}) consts
   |> snd;
 
 fun invoke_generation_for_consts'' ctxt algebra_eqngr =
@@ -850,7 +852,10 @@
 fun dynamic_evaluation eval ctxt algebra eqngr t =
   let
     val ((program, (vs_ty_t', deps)), _) =
-      invoke_generation false ctxt (ensure_value ctxt algebra eqngr) t;
+      Code_Preproc.timed "translating term" #ctxt
+      (fn { ctxt, algebra, eqngr, t } =>
+        invoke_generation false ctxt (ensure_value ctxt algebra eqngr) t)
+        { ctxt = ctxt, algebra = algebra, eqngr = eqngr, t = t };
   in eval program t vs_ty_t' deps end;
 
 fun dynamic_conv ctxt conv =
@@ -869,7 +874,10 @@
     fun evaluation program dynamic_eval ctxt t =
       let
         val ((_, ((vs_ty', t'), deps)), _) =
-          ensure_value ctxt algebra eqngr t ([], program);
+          Code_Preproc.timed "translating term" #ctxt
+          (fn { ctxt, t } =>
+            ensure_value ctxt algebra eqngr t ([], program))
+            { ctxt = ctxt, t = t };
       in dynamic_eval ctxt t (vs_ty', t') deps end;
   in
     static_evaluation ctxt consts algebra_eqngr (fn program_deps =>
@@ -935,7 +943,8 @@
 
 fun code_depgr ctxt consts =
   let
-    val { eqngr, ... } = Code_Preproc.obtain true ctxt consts [];
+    val { eqngr, ... } = Code_Preproc.obtain true
+      { ctxt = ctxt, consts = consts, terms = [] };
     val all_consts = Graph.all_succs eqngr consts;
   in Graph.restrict (member (op =) all_consts) eqngr end;
 
diff -r b561284a4214 -r 72aaf69328fc src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/Tools/nbe.ML	Thu May 26 15:27:50 2016 +0200
@@ -8,8 +8,10 @@
 sig
   val dynamic_conv: Proof.context -> conv
   val dynamic_value: Proof.context -> term -> term
-  val static_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv
-  val static_value: { ctxt: Proof.context, consts: string list } -> Proof.context -> term -> term
+  val static_conv: { ctxt: Proof.context, consts: string list }
+    -> Proof.context -> conv
+  val static_value: { ctxt: Proof.context, consts: string list }
+    -> Proof.context -> term -> term
 
   datatype Univ =
       Const of int * Univ list               (*named (uninterpreted) constants*)
@@ -21,7 +23,8 @@
                                              (*abstractions as closures*)
   val same: Univ * Univ -> bool
 
-  val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context
+  val put_result: (unit -> Univ list -> Univ list)
+    -> Proof.context -> Proof.context
   val trace: bool Config.T
 
   val add_const_alias: thm -> theory -> theory
@@ -477,7 +480,7 @@
       #-> fold (fn (name, univ) => (Code_Symbol.Graph.map_node name o apfst) (K (SOME univ))))
   end;
 
-fun compile_program ctxt program =
+fun compile_program { ctxt, program } =
   let
     fun add_stmts names (nbe_program, (maxidx, idx_tab)) = if exists ((can o Code_Symbol.Graph.get_node) nbe_program) names
       then (nbe_program, (maxidx, idx_tab))
@@ -554,7 +557,7 @@
       if null (Term.add_tvars t' []) then t'
       else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t');
   in
-    compile_and_reconstruct_term
+    Code_Preproc.timed "computing NBE expression" #ctxt compile_and_reconstruct_term
       { ctxt = ctxt, nbe_program = nbe_program, idx_tab = idx_tab, deps = deps, term = (vs, t) }
     |> traced ctxt (fn t => "Normalized:\n" ^ string_of_term t)
     |> type_infer
@@ -576,7 +579,8 @@
   let
     val (nbe_program, (_, idx_tab)) =
       Nbe_Functions.change (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt))
-        (compile_program ctxt program);
+        (Code_Preproc.timed "compiling NBE program" #ctxt
+          compile_program { ctxt = ctxt, program = program });
   in (nbe_program, idx_tab) end;
 
 
@@ -608,13 +612,13 @@
 fun static_conv (ctxt_consts as { ctxt, ... }) =
   let
     val conv = Code_Thingol.static_conv_thingol ctxt_consts
-      (fn { program, ... } => oracle (compile true ctxt program));
+      (fn { program, deps = _ } => oracle (compile true ctxt program));
   in fn ctxt' => lift_triv_classes_conv ctxt' conv end;
 
 fun static_value { ctxt, consts } =
   let
     val comp = Code_Thingol.static_value { ctxt = ctxt, lift_postproc = I, consts = consts }
-      (fn { program, ... } => normalize_term (compile false ctxt program));
+      (fn { program, deps = _ } => normalize_term (compile false ctxt program));
   in fn ctxt' => lift_triv_classes_rew ctxt' (comp ctxt') end;
 
 end;