Merge pull request #3974 from mtzguido/stats_record

Tactics: introduce stats_record

Author: mtzguido

src/tactics/FStarC.Tactics.V2.Basic.fst

@@ -3065,3 +3065,7 @@ let call_subtac_tm (g:env) (f_tm : term) (_u:universe) (goal_ty : typ) : tac (op
     return (Some w, [])
   | issues, _ ->
     return (None, issues)
+
+let stats_record (a:'a) (wp:'b) (s:string) (f : tac 'c) : tac 'c =
+  mk_tac (fun ps ->
+    Stats.record s (fun () -> run f ps))

src/tactics/FStarC.Tactics.V2.Basic.fsti

@@ -158,3 +158,5 @@ val log_issues                        : list Errors.issue -> tac unit
 
 val call_subtac                       : env -> tac unit -> universe -> typ -> refl_tac term
 val call_subtac_tm                    : env -> term     -> universe -> typ -> refl_tac term
+
+val stats_record (a:'a) (wp:'b) (s:string) (f : tac 'c) : tac 'c

src/tactics/FStarC.Tactics.V2.Primops.fst

@@ -271,4 +271,10 @@ let ops = [
 
   mk_tac_step_4 0 "call_subtac_tm"
     call_subtac_tm call_subtac_tm;
+
+  mk_tac_step_4 1 "stats_record"
+    #e_any      #e_any      #_ #(TI.e_tactic_thunk e_any)          #e_any
+    #NBET.e_any #NBET.e_any #_ #(TI.e_tactic_nbe_thunk NBET.e_any) #NBET.e_any
+    stats_record
+    stats_record;
 ]

ulib/FStar.Stubs.Tactics.V2.Builtins.fsti

@@ -644,3 +644,9 @@ val call_subtac_tm
     (g:env) (t : term) (u:universe)
     (goal_ty : term{typing_token g goal_ty (E_Total, pack_ln (Tv_Type u))})
   : Tac (ret_t (w:term{typing_token g w (E_Total, goal_ty)}))
+
+(* This will call the function [f] and log the time it takes under the stat key
+[s]. The stats can be printed by running F* with `--stats true`. Other than
+that, there is no observable difference from calling [f].  We could also expose
+a pure version of this function. *)
+val stats_record #a #wp (s : string) ($f : unit -> TAC a wp) : TAC a wp

ulib/ml/plugin/FStarC_Tactics_V2_Builtins.ml

@@ -180,3 +180,6 @@ let call_subtac g (t : unit -> unit __tac) u ty =
   from_tac_4 "B.call_subtac" B.call_subtac g t u ty
 
 let call_subtac_tm               = from_tac_4 "B.call_subtac_tm" B.call_subtac_tm
+
+let stats_record (s : string) (f : unit -> 'c __tac) : 'c __tac =
+  from_tac_2 "B.stats_record" (B.stats_record () ()) s (to_tac_0 (f ()))