Fix question marks simplification with deref/borrow.

cryspen · Feb 10, 2025 · 8c1a0a7 · 8c1a0a7
1 parent e0ea99a
commit 8c1a0a7
Show file tree

Hide file tree

Showing 5 changed files with 719 additions and 10 deletions.
diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml
@@ -109,8 +109,8 @@ module Make (F : Features.T) = struct
 
     let deref_mut_app = concrete_app1 Core__ops__deref__DerefMut__deref_mut
 
-    let local_var (e : expr) : expr option =
-      match e.e with LocalVar _ -> Some e | _ -> None
+    let local_var (e : expr) : local_ident option =
+      match e.e with LocalVar v -> Some v | _ -> None
 
     let arrow (typ : ty) : (ty list * ty) option =
       match typ with

diff --git a/engine/lib/phases/phase_simplify_question_marks.ml b/engine/lib/phases/phase_simplify_question_marks.ml
@@ -175,14 +175,7 @@ module%inlined_contents Make (FA : Features.T) = struct
               arms =
                 [
                   { arm = { arm_pat = pat_break; body }; _ };
-                  {
-                    arm =
-                      {
-                        arm_pat = pat_continue;
-                        body = { e = LocalVar continue_var; _ };
-                      };
-                    _;
-                  };
+                  { arm = { arm_pat = pat_continue; body = continue_expr }; _ };
                 ];
             }
           when Global_ident.eq_name Core__ops__try_trait__Try__branch n ->
@@ -195,6 +188,13 @@ module%inlined_contents Make (FA : Features.T) = struct
             in
             let* f_break, residual_var' = extract_pat_app_bd pat_break in
             let* f_continue, continue_var' = extract_pat_app_bd pat_continue in
+            let continue_expr =
+              Option.value
+                (UA.Expect.borrow continue_expr)
+                ~default:continue_expr
+            in
+            let continue_expr = UA.unbox_underef_expr continue_expr in
+            let* continue_var = UA.Expect.local_var continue_expr in
             let*? _ = [%equal: local_ident] residual_var residual_var' in
             let*? _ = [%equal: local_ident] continue_var continue_var' in
             let*? _ =

diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
@@ -81,6 +81,38 @@ let test (x y: Core.Option.t_Option i32) : Core.Option.t_Option i32 =
   | Core.Option.Option_Some some -> some
   | Core.Option.Option_None  -> Core.Option.Option_None <: Core.Option.t_Option i32
 '''
+"Side_effects.Issue_1299_.fst" = '''
+module Side_effects.Issue_1299_
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+type t_Foo = { f_y:u8 }
+
+type t_S = { f_g:t_Foo }
+
+type t_OtherS = { f_g:Core.Option.t_Option t_Foo }
+
+let impl_Foo__from (i: t_Foo) : t_Foo =
+  { f_y = Core.Clone.f_clone #u8 #FStar.Tactics.Typeclasses.solve i.f_y } <: t_Foo
+
+type t_Error = | Error : t_Error
+
+let impl_S__from (i: t_OtherS) : Core.Result.t_Result t_S t_Error =
+  match
+    Core.Option.impl__ok_or #t_Foo
+      #t_Error
+      (Core.Option.impl__as_ref #t_Foo i.f_g <: Core.Option.t_Option t_Foo)
+      (Error <: t_Error)
+    <:
+    Core.Result.t_Result t_Foo t_Error
+  with
+  | Core.Result.Result_Ok hoist47 ->
+    Core.Result.Result_Ok ({ f_g = impl_Foo__from hoist47 } <: t_S)
+    <:
+    Core.Result.t_Result t_S t_Error
+  | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result t_S t_Error
+'''
 "Side_effects.Nested_return.fst" = '''
 module Side_effects.Nested_return
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"