tactics: make refl_typing_builting_wrapper take a tac argument

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

@@ -2088,26 +2088,40 @@ let dbg_refl (g:env) (msg:unit -> string) =
   then BU.print_string (msg ())
 
 let issues = list Errors.issue
-let refl_typing_builtin_wrapper (f:unit -> 'a) : tac (option 'a & issues) =
-  let tx = UF.new_transaction () in
-  let errs, r =
-    try Errors.catch_errors_and_ignore_rest f
-    with exn -> //catch everything
+
+let catch_tac_errs (f : unit -> tac 'a) : tac (option 'a & issues) =
+  mk_tac (fun ps ->
+    let tx = UF.new_transaction () in
+    Env.promote_id_info ps.main_context (FStar.TypeChecker.Tc.compress_and_norm ps.main_context);
+    try
+      match (Errors.catch_errors_and_ignore_rest (fun () -> Tactics.Monad.run (f ()) ps)) with
+      (* Success without errors, return Some and advance proofstate *)
+      | [], Some (Success (r, ps')) ->
+        UF.commit tx;
+        Success ((Some r, []), ps')
+
+      (* Some errors logged, or Failure, return None and leave state unchanged. *)
+      | errs, _ ->
+        UF.rollback tx;
+        Success ((None, errs), ps)
+    with
+    | exn ->
+      (* Can this really occur? *)
       let issue = FStar.Errors.({
         issue_msg = BU.print_exn exn;
         issue_level = EError;
         issue_range = None;
         issue_number = (Some 17);
         issue_ctx = get_ctx ()
       }) in
-      [issue], None
-  in
+      UF.rollback tx;
+      (* Same as last case *)
+      Success ((None, [issue]), ps))
+
+let refl_typing_builtin_wrapper (f : unit -> tac 'a) : tac (option 'a & issues) =
+  let! r = catch_tac_errs f in
   let! ps = get in
-  Env.promote_id_info ps.main_context (FStar.TypeChecker.Tc.compress_and_norm ps.main_context);
-  UF.rollback tx;
-  if List.length errs > 0
-  then ret (None, errs)
-  else ret (r, errs)
+  ret r
 
 let no_uvars_in_term (t:term) : bool =
   t |> Free.uvars |> BU.set_is_empty &&
@@ -2152,10 +2166,11 @@ let refl_check_relation (g:env) (t0 t1:typ) (rel:relation)
          match f g t0 t1 with
          | Inl None ->
            dbg_refl g (fun _ -> "refl_check_relation: succeeded (no guard)");
-           ()
+           ret ()
          | Inl (Some guard_f) ->
            Rel.force_trivial_guard g {Env.trivial_guard with guard_f=NonTrivial guard_f};
-           dbg_refl g (fun _ -> "refl_check_relation: succeeded")
+           dbg_refl g (fun _ -> "refl_check_relation: succeeded");
+           ret ()
          | Inr err ->
            dbg_refl g (fun _ -> BU.format1 "refl_check_relation failed: %s\n" (Core.print_error err));
            Errors.raise_error (Errors.Fatal_IllTyped, "check_relation failed: " ^ (Core.print_error err)) Range.dummyRange)
@@ -2195,7 +2210,7 @@ let refl_core_compute_term_type (g:env) (e:term) (eff:tot_or_ghost) : tac (optio
              BU.format2 "refl_core_compute_term_type for %s computed type %s\n"
                (Print.term_to_string e)
                (Print.term_to_string t));
-           t
+           ret t
          | Inr err ->
            dbg_refl g (fun _ -> BU.format1 "refl_core_compute_term_type: %s\n" (Core.print_error err));
            Errors.raise_error (Errors.Fatal_IllTyped, "core_compute_term_type failed: " ^ (Core.print_error err)) Range.dummyRange)
@@ -2268,7 +2283,7 @@ let refl_tc_term (g:env) (e:term) (eff:tot_or_ghost) : tac (option (term & typ)
           BU.format2 "refl_tc_term for %s computed type %s\n"
             (Print.term_to_string e)
             (Print.term_to_string t));
-        e, t
+        ret (e, t)
      | Inr err ->
         dbg_refl g (fun _ -> BU.format1 "refl_tc_term failed: %s\n" (Core.print_error err));
         Errors.raise_error (Errors.Fatal_IllTyped, "tc_term callback failed: " ^ Core.print_error err) e.pos
@@ -2291,11 +2306,12 @@ let refl_universe_of (g:env) (e:term) : tac (option universe & issues) =
          let t, u = U.type_u () in
          let must_tot = false in
          match Core.check_term g e t must_tot with
-         | Inl None -> check_univ_var_resolved u
+         | Inl None ->
+           ret (check_univ_var_resolved u)
          | Inl (Some guard) ->
            Rel.force_trivial_guard g
              {Env.trivial_guard with guard_f=NonTrivial guard};
-           check_univ_var_resolved u
+           ret (check_univ_var_resolved u)
          | Inr err ->
            let msg = BU.format1 "refl_universe_of failed: %s\n" (Core.print_error err) in
            dbg_refl g (fun _ -> msg);
@@ -2321,8 +2337,8 @@ let refl_check_prop_validity (g:env) (e:term) : tac (option unit & issues) =
              dbg_refl g (fun _ -> msg);
              Errors.raise_error (Errors.Fatal_IllTyped, msg) Range.dummyRange
          in
-         Rel.force_trivial_guard g
-           {Env.trivial_guard with guard_f=NonTrivial e})
+         ret (Rel.force_trivial_guard g
+           {Env.trivial_guard with guard_f=NonTrivial e}))
   else ret (None, [unexpected_uvars_issue (Env.get_range g)])
 
 let refl_check_match_complete (g:env) (sc:term) (scty:typ) (pats : list RD.pattern)
@@ -2374,7 +2390,7 @@ let refl_instantiate_implicits (g:env) (e:term) : tac (option (term & typ) & iss
       BU.format2 "} finished tc with e = %s and t = %s\n"
         (Print.term_to_string e)
         (Print.term_to_string t));
-    (e, t))
+    ret (e, t))
   else ret (None, [unexpected_uvars_issue (Env.get_range g)])
 
 let refl_maybe_relate_after_unfolding (g:env) (t0 t1:typ)
@@ -2392,7 +2408,7 @@ let refl_maybe_relate_after_unfolding (g:env) (t0 t1:typ)
          dbg_refl g (fun _ ->
            BU.format1 "} returning side: %s\n"
              (Core.side_to_string s));
-         s)
+         ret s)
   else ret (None, [unexpected_uvars_issue (Env.get_range g)])
 
 let refl_maybe_unfold_head (g:env) (e:term) : tac (option term & issues) =
@@ -2412,7 +2428,7 @@ let refl_maybe_unfold_head (g:env) (e:term) : tac (option term & issues) =
                              BU.format1
                                "Could not unfold head: %s\n"
                                (Print.term_to_string e)) e.pos
-    else eopt |> must)
+    else eopt |> must |> ret)
   else ret (None, [unexpected_uvars_issue (Env.get_range g)])
 
 let push_open_namespace (e:env) (ns:list string) =