File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -70,7 +70,10 @@ let check_fndefn
7070 let rng = body . range in
7171 debug_main g ( fun _ -> Printf. sprintf " \n body after mk_abs:\n %s\n " ( P. st_term_to_string body ));
7272
73- let (| body , c , t_typing |) = Pulse.Checker.Abs. check_abs g body Pulse.Checker. check in
73+ let (| body , c , t_typing |) =
74+ stats_record " top_level check_abs" fun () ->
75+ Pulse.Checker.Abs. check_abs g body Pulse.Checker. check
76+ in
7477
7578 Pulse.Checker.Prover.Util. debug_prover g
7679 ( fun _ -> Printf. sprintf " \n check call returned in main with:\n %s\n at type %s\n "
@@ -89,6 +92,7 @@ let check_fndefn
8992 let cur_module = T. cur_module () in
9093
9194 let maybe_add_impl t ( se : RT. sigelt_for ( fstar_env g ) t ) : Tac ( RT. sigelt_for ( fstar_env g ) t ) =
95+ stats_record " pulse_extraction" fun () ->
9296 let open Pulse.Extract.Main in begin
9397 if T. ext_enabled " pulse.noextract" then (
9498 T. print " >>>>>Skipping extraction\n " ;
You can’t perform that action at this time.
0 commit comments