src/Tools/nbe.ML

 
 signature NBE =
 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*)
     | DFree of string * int                  (*free (uninterpreted) dictionary parameters*)
     | BVar of int * Univ list

   val apps: Univ -> Univ list -> Univ        (*explicit applications*)
   val abss: int -> (Univ list -> Univ) -> Univ
                                              (*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
 end;
 

     #> apfst (fold (fn (name, deps) => fold (curry Code_Symbol.Graph.add_edge name) deps) names_deps
       #> compile
       #-> 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))
       else (nbe_program, (maxidx, idx_tab))
         |> compile_stmts ctxt (map (fn name => ((name, Code_Symbol.Graph.get_node program name),

         (Type.constraint (fastype_of t_original) t');
     fun check_tvars t' =
       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
     |> traced ctxt (fn t => "Types inferred:\n" ^ string_of_term t)
     |> check_tvars

 
 fun compile ignore_cache ctxt program =
   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;
 
 
 (* evaluation oracle *)
 

     normalize_term (compile false ctxt program) ctxt));
 
 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;