Adapt to tactic monad change.

src/checker/Pulse.Checker.Base.fst

@@ -1179,8 +1179,8 @@ let infer_post #g #ctxt (r:checker_result_t g ctxt NoHint)
   let bs0 = bindings g in
   let dom_g = dom g in
   let fvs_t = freevars t in
-  let fail_fv_typ #a (x:string) 
-  : T.Tac a =
+  let fail_fv_typ (x:string) 
+  : T.Tac unit =
     fail_doc g (Some (T.range_of_term t))
         [Pulse.PP.text "Could not infer a type for this block; the return type `";
           Pulse.PP.text (T.term_to_string t); 

src/checker/Pulse.Checker.Pure.fst

@@ -166,8 +166,8 @@ does not make sense, as that indicates a well-typed term with no particular
 expected type, which is fine. *)
 let ill_typed_term (t:term) (expected_typ got_typ : option term)
 : TacH (list document)
-       (requires fun _ -> None? expected_typ ==> None? got_typ)
-       (ensures fun _ _ -> True)
+       (requires None? expected_typ ==> None? got_typ)
+       (ensures fun _ -> True)
 =
   let open Pulse.PP in
   match expected_typ, got_typ with
@@ -192,7 +192,7 @@ let instantiate_term_implicits
   let rng = RU.range_of_term t0 in
   let f = RU.env_set_range f (Pulse.Typing.Env.get_range g (Some rng)) in
   let topt, issues = catch_all (fun _ -> rtb_instantiate_implicits g f t0 expected inst_extra) in
-  let fail #a issues : Tac a =
+  let fail issues : Tac _ = 
     fail_doc_with_subissues g (Some rng) issues []
   in
   match topt with

src/checker/Pulse.Checker.WithLocal.fst

@@ -46,7 +46,7 @@ let with_local_pre_typing (#g:env) (#pre:term) (pre_typing:tot_typing g pre tm_s
                tm_slprop
   = admit()
 
-#push-options "--z3rlimit_factor 8 --fuel 0 --ifuel 1 --split_queries no"
+#push-options "--z3rlimit_factor 10 --fuel 0 --ifuel 1 --split_queries no"
 let head_range (t:st_term {Tm_WithLocal? t.term}) : range =
   let Tm_WithLocal { initializer } = t.term in
   (RU.range_of_term initializer)

src/checker/Pulse.JoinComp.fst

@@ -285,7 +285,7 @@ let rec join_comps
   (c_else:comp_st)
   (e_else_typing:st_typing g_else e_else c_else)
   (post:post_hint_t)
-  : TacS (c:comp_st &
+  : T.TacH (c:comp_st &
           st_typing g_then e_then c &
           st_typing g_else e_else c)
          (requires

src/checker/Pulse.JoinComp.fsti

@@ -19,12 +19,6 @@ module Pulse.JoinComp
 open Pulse.Syntax
 open Pulse.Typing
 module T = FStar.Tactics.V2
-effect TacS (a:Type) (pre : Type0) (post : (_:a{pre}) -> Type0) =
-  Tactics.TacH a (requires (fun _ -> pre))
-                 (ensures (fun _ r -> pre /\ (
-                                      match r with
-                                      | Tactics.Result.Success r _ -> post r
-                                      | _ -> True))) // does not guarantee anything on failure
 
 val join_post #g #hyp #b
     (p1:post_hint_for_env (g_with_eq g hyp b tm_true))
@@ -41,7 +35,7 @@ val join_comps
   (c_else:comp_st)
   (e_else_typing:st_typing g_else e_else c_else)
   (post:post_hint_t)
-: TacS (c:comp_st &
+: T.TacH (c:comp_st &
         st_typing g_then e_then c &
         st_typing g_else e_else c)
     (requires

src/checker/Pulse.Typing.Combinators.fst

@@ -169,7 +169,6 @@ let rec slprop_equiv_typing (#g:_) (#t0 #t1:term) (v:slprop_equiv g t0 t1)
         let t0_typing = d1 t1_typing in
         construct_forall_typing #g #u #b #t0 x b_typing t0_typing)
 
-#push-options "--z3rlimit_factor 8 --ifuel 1 --fuel 2"
 let bind_t (case_c1 case_c2:comp_st -> bool) =
       (g:env) ->
       (pre:term) ->
@@ -190,15 +189,14 @@ let bind_t (case_c1 case_c2:comp_st -> bool) =
             c:comp_st { st_comp_of_comp c == st_comp_with_pre (st_comp_of_comp c2) pre  /\
                         comp_post_matches_hint c post_hint } &
             st_typing g t c)
-           (requires fun _ ->
-              let _, x = px in
+           (requires
+              (let _, x = px in
               comp_pre c1 == pre /\
               None? (lookup g x) /\
               (~(x `Set.mem` freevars_st e2)) /\
               open_term (comp_post c1) x == comp_pre c2 /\
-              (~ (x `Set.mem` freevars (comp_post c2))))
-           (ensures fun _ _ -> True)
-#pop-options
+              (~ (x `Set.mem` freevars (comp_post c2)))))
+           (ensures fun _ -> True)
 
 let mk_bind_st_st
   : bind_t C_ST? C_ST?
@@ -359,18 +357,18 @@ let rec mk_bind (g:env)
               st_comp_of_comp c == st_comp_with_pre (st_comp_of_comp c2) pre /\
               comp_post_matches_hint c post_hint } &
             st_typing g t c)
-           (requires fun _ ->
-              let _, x = px in
+           (requires
+              (let _, x = px in
               comp_pre c1 == pre /\
               None? (lookup g x) /\
               (~(x `Set.mem` freevars_st e2)) /\
               open_term (comp_post c1) x == comp_pre c2 /\
-              (~ (x `Set.mem` freevars (comp_post c2))))
-           (ensures fun _ _ -> True) =
+              (~ (x `Set.mem` freevars (comp_post c2)))))
+           (ensures fun _ -> True) =
   let _, x = px in
   let b = nvar_as_binder px (comp_res c1) in
-  let fail_bias (#a:Type) tag
-  : T.TacH a (requires fun _ -> True) (ensures fun _ r -> FStar.Tactics.Result.Failed? r)
+  let fail_bias tag
+  : T.TacH _ (requires True) (ensures fun _ -> False)
   = let open Pulse.PP in
     fail_doc g (Some e1.range)
       [text "Cannot compose computations in this " ^/^ text tag ^/^ text " block:";

src/checker/Pulse.Typing.Combinators.fsti

@@ -58,14 +58,14 @@ val mk_bind (g:env)
             c:comp_st { st_comp_of_comp c == st_comp_with_pre (st_comp_of_comp c2) pre /\
                         comp_post_matches_hint c post_hint } &
             st_typing g t c)
-           (requires fun _ ->
-              let _, x = px in
+           (requires
+              (let _, x = px in
               comp_pre c1 == pre /\
               None? (lookup g x) /\
               (~(x `Set.mem` freevars_st e2)) /\
               open_term (comp_post c1) x == comp_pre c2 /\
-              (~ (x `Set.mem` freevars (comp_post c2))))
-           (ensures fun _ _ -> True)
+              (~ (x `Set.mem` freevars (comp_post c2)))))
+           (ensures fun _ -> True)
 
 
 val bind_res_and_post_typing (g:env) (s2:comp_st) (x:var { fresh_wrt x g (freevars (comp_post s2)) })

src/checker/Pulse.Typing.Env.fst

@@ -459,7 +459,6 @@ let info (g:env) (r:option range) (msg:string) =
 let fail_doc_with_subissues #a (g:env) (ro : option range)
   (sub : list Issue.issue)
   (msg : list document)
-  : T.TacH a (requires fun _ -> True) (ensures fun _ r -> FStar.Tactics.Result.Failed? r)
 =
   (* If for whatever reason `sub` is empty, F* will handle it well
   and a generic error message will be displayed *)

src/checker/Pulse.Typing.Env.fsti

@@ -225,10 +225,10 @@ val get_range (g:env) (r:option range) : T.Tac range
 
 val fail_doc_env (#a:Type) (with_env:bool)
                  (g:env) (r:option range) (msg:list Pprint.document)
-  : T.TacH a (requires fun _ -> True) (ensures fun _ r -> FStar.Tactics.Result.Failed? r)
+  : T.TacH a (requires True) (ensures fun _ -> False)
 
 let fail_doc (#a:Type) (g:env) (r:option range) (msg:list Pprint.document)
-  : T.TacH a (requires fun _ -> True) (ensures fun _ r -> FStar.Tactics.Result.Failed? r)
+  : T.TacH a (requires True) (ensures fun _ -> False)
   = fail_doc_env false g r msg
 
 val warn_doc (g:env) (r:option range) (msg:list Pprint.document)
@@ -241,7 +241,7 @@ val info_doc_env (g:env) (r:option range) (msg:list Pprint.document)
   : T.Tac unit
 
 val fail (#a:Type) (g:env) (r:option range) (msg:string) 
-  : T.TAC a (fun _ post -> forall ex ps. post FStar.Tactics.Result.(Failed ex ps))
+  : T.TacH a (requires True) (ensures fun _ -> False)
 
 val warn (g:env) (r:option range) (msg:string)
   : T.Tac unit
@@ -252,7 +252,7 @@ val info (g:env) (r:option range) (msg:string)
 val fail_doc_with_subissues #a (g:env) (ro : option range)
   (sub : list Issue.issue)
   (msg : list Pprint.document)
-  : T.TacH a (requires fun _ -> True) (ensures fun _ r -> FStar.Tactics.Result.Failed? r)
+  : T.TacH a (requires True) (ensures fun _ -> False)
 
 val info_doc_with_subissues (g:env) (r:option range)
   (sub : list Issue.issue)

src/ml/PulseSyntaxExtension_SyntaxWrapper.ml

@@ -238,9 +238,7 @@ let tac_to_string (env:Env.env) f =
                 []
                 []
     in
-    match f ps with
-    | FStarC_Tactics_Result.Success (x, _) -> x
-    | FStarC_Tactics_Result.Failed (exn, _) -> failwith (print_exn exn)
+    f (ref ps)
 
 let binder_to_string (env:Env.env) (b:binder)
   : string

src/ml/Pulse_RuntimeUtils.ml

@@ -3,8 +3,7 @@ type context = ((string * FStarC_Range.range option) list) (* FStar_Sealed.seale
 let extend_context (s:string) (r:FStarC_Range.range option) (c:context) = (s,r)::c
 module TR = FStarC_Tactics_Result
 
-type ('a,'wp) tac_repr = FStarC_Tactics_Types.proofstate -> 'a TR.__result
-type 'a utac = ('a, unit) tac_repr 
+type 'a utac = 'a FStarC_Tactics_Monad.tac
 
 let ctxt_elt_as_string (s, r) =
     match r with
@@ -13,10 +12,7 @@ let ctxt_elt_as_string (s, r) =
       "@" ^ FStarC_Range.string_of_range r ^ ": " ^ s
 let rec print_context (c:context) : string utac =
   fun ps ->
-    TR.Success (
-      String.concat "\n>" (List.map ctxt_elt_as_string c),
-      ps
-    )
+    String.concat "\n>" (List.map ctxt_elt_as_string c)
 let rec with_context (c:context) (f: unit -> 'a utac) : 'a utac =
   fun ps ->
     match c with
@@ -206,31 +202,25 @@ let whnf_lax (g:TcEnv.env) (t:S.term) : S.term =
 let hnf_lax (g:TcEnv.env) (t:S.term) : S.term =
   FStarC_TypeChecker_Normalize.normalize [TcEnv.Unascribe; TcEnv.Primops; TcEnv.HNF; TcEnv.UnfoldUntil S.delta_constant; TcEnv.Beta] g t
 
-let norm_well_typed_term_aux
-      (g:TcEnv.env)
-      (t:S.term)
-      (steps:FStarC_NormSteps.norm_step list)
-  = let steps = FStarC_TypeChecker_Cfg.translate_norm_steps steps in
-    let t' = FStarC_TypeChecker_Normalize.normalize (TcEnv.Unascribe::steps) g t in
-    FStar_Pervasives.Mkdtuple3 (t', (), ())
-
 let norm_well_typed_term      
       (g:TcEnv.env)
       (t:S.term)
       (eff:_)
       (k:_)
       (typing:_)
       (steps:FStarC_NormSteps.norm_step list)
-      (ps:_)
-  = let t' = norm_well_typed_term_aux g t steps in
-    FStarC_Tactics_Result.Success (t', ps)
+  : ((S.term, unit, unit) Fstar_pluginlib.FStar_Pervasives.dtuple3) utac
+  = fun ps ->
+    let steps = FStarC_TypeChecker_Cfg.translate_norm_steps steps in
+    let t' = FStarC_TypeChecker_Normalize.normalize (TcEnv.Unascribe::steps) g t in
+    Fstar_pluginlib.FStar_Pervasives.Mkdtuple3 (t', (), ())
 
 let add_attribute (s:S.sigelt) (x:S.attribute) =
   { s with sigattrs = x::s.sigattrs }
 let add_noextract_qual (s:S.sigelt) =
   { s with sigquals = S.NoExtract::s.sigquals }
-let get_attributes (s:S.sigelt) (ps:_) =
-  FStarC_Tactics_Result.Success (s.sigattrs, ps)
+let get_attributes (s:S.sigelt) : _ utac = fun ps ->
+  s.sigattrs
 
 let must_erase_for_extraction (g:FStarC_Reflection_Types.env) (ty:FStarC_Syntax_Syntax.term) =
   FStarC_TypeChecker_Util.must_erase_for_extraction g ty

test/bug-reports/Bug.SpinLock.fst.output.expected

@@ -1,5 +1,6 @@
 * Info at Bug.SpinLock.fst(45,2-45,4):
   - Expected failure:
+  - Tactic failed
   - Cannot prove:
       Pulse.Lib.Reference.pts_to __ ?__
   - In the context:

test/bug-reports/Bug107.fst.output.expected

@@ -1,8 +1,10 @@
 * Info at Bug107.fst(45,9-45,16):
   - Expected failure:
+  - Tactic failed
   - Could not resolve implicit uu___#87 of type Prims.int in term Bug107.foo 1 _
 
 * Info at Bug107.fst(56,9-56,16):
   - Expected failure:
+  - Tactic failed
   - Could not resolve implicit uu___#87 of type Prims.int in term Bug107.foo _ 2
 

test/bug-reports/Bug267.fst.output.expected

@@ -1,5 +1,6 @@
 * Info at Bug267.fst(14,4-14,6):
   - Expected failure:
+  - Tactic failed
   - Expected a total term, but this term has Ghost effect
 
 * Info at Bug267.fst(62,4-62,5):

test/bug-reports/Bug274.fst.output.expected

@@ -1,5 +1,6 @@
 * Info at Bug274.fst(29,4-29,15):
   - Expected failure:
+  - Tactic failed
   - Cannot prove any of:
       Pulse.Lib.Trade.trade _ _ ** Pulse.Lib.Trade.trade _ _
   - In the context:
@@ -36,6 +37,7 @@
 
 * Info at Bug274.fst(41,4-41,15):
   - Expected failure:
+  - Tactic failed
   - Cannot prove any of:
       Pulse.Lib.Trade.trade _ _ ** Pulse.Lib.Trade.trade _ _
   - In the context:
@@ -72,6 +74,7 @@
 
 * Info at Bug274.fst(73,4-73,12):
   - Expected failure:
+  - Tactic failed
   - Cannot prove any of:
       _ ** Pulse.Lib.Trade.trade _ _
   - In the context:

test/bug-reports/Bug29.fst.output.expected

@@ -1,5 +1,6 @@
 * Info at Bug29.fst(57,4-57,45):
   - Expected failure:
+  - Tactic failed
   - Cannot prove:
       Pulse.Lib.Reference.pts_to r v
   - In the context:

test/bug-reports/ExistsErasedAndPureEqualities.fst.output.expected

@@ -1,10 +1,12 @@
 * Info at ExistsErasedAndPureEqualities.fst(32,4-33,21):
   - Expected failure:
+  - Tactic failed
   - Could not resolve all free variables in the proposition: v == v_
   - See also ExistsErasedAndPureEqualities.fst(32,4-34,12)
 
 * Info at ExistsErasedAndPureEqualities.fst(50,4-51,21):
   - Expected failure:
+  - Tactic failed
   - Could not resolve all free variables in the proposition: v == v_
   - See also ExistsErasedAndPureEqualities.fst(50,4-52,12)
 
@@ -21,6 +23,7 @@
 
 * Info at ExistsErasedAndPureEqualities.fst(79,4-80,21):
   - Expected failure:
+  - Tactic failed
   - Could not resolve all free variables in the proposition: v == v_
   - See also ExistsErasedAndPureEqualities.fst(79,4-81,12)
 

test/bug-reports/IntroGhost.fst.output.expected

@@ -1,12 +1,14 @@
 * Info at IntroGhost.fst(44,18-44,20):
   - Expected failure:
+  - Tactic failed
   - Cannot prove:
       Pulse.Lib.Reference.pts_to r __
   - In the context:
       IntroGhost.my_inv b r
 
 * Info at IntroGhost.fst(71,2-71,4):
   - Expected failure:
+  - Tactic failed
   - Cannot prove:
       Pulse.Lib.Reference.pts_to r 0
   - In the context:

test/bug-reports/PartialApp.fst.output.expected

@@ -1,10 +1,12 @@
 * Info at PartialApp.fst(26,2-26,3):
   - Expected failure:
+  - Tactic failed
   - This statement returns a value of type: Prims.int
   - Did you forget to assign it or ignore it?
 
 * Info at PartialApp.fst(60,2-60,9):
   - Expected failure:
+  - Tactic failed
   - This function is partially applied. Remaining type:
       y: t
         -> Pulse.Lib.Core.stt Prims.unit

test/nolib/Test.Matcher.fst.output.expected

@@ -1,5 +1,6 @@
 * Info at Test.Matcher.fst(69,2-69,4):
   - Expected failure:
+  - Tactic failed
   - Cannot prove:
       Test.Matcher.fpts_to #Prims.int
         r

test/nolib/Test.RewriteBy.fst.output.expected

@@ -12,5 +12,5 @@
   - Reduction stopped at:
       reify (let _ = FStar.Stubs.Tactics.V2.Builtins.dump "a" in
           Test.RewriteBy.tac ())
-        "(((proofstate)))"
+        "(((ref proofstate)))"