--- 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)
--- 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
--- 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
--- 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 *)
--- 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;
--- 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;