Merge pull request #779 from hacspec/fix-155

Support let-else pattern.

engine/lib/import_thir.ml

@@ -370,6 +370,84 @@ end) : EXPR = struct
     let v = Global_ident.of_name Value Rust_primitives__hax__dropped_body in
     { span; typ; e = GlobalVar v }
 
+  and c_block ~expr ~span ~stmts ~ty : expr =
+    let full_span = Span.of_thir span in
+    let typ = c_ty span ty in
+    (* if there is no expression & the last expression is ⊥, just use that *)
+    let lift_last_statement_as_expr_if_possible expr stmts (ty : Thir.ty) =
+      match (ty, expr, List.drop_last stmts, List.last stmts) with
+      | ( Thir.Never,
+          None,
+          Some stmts,
+          Some ({ kind = Thir.Expr { expr; _ }; _ } : Thir.stmt) ) ->
+          (stmts, Some expr)
+      | _ -> (stmts, expr)
+    in
+    let o_stmts, o_expr =
+      lift_last_statement_as_expr_if_possible expr stmts ty
+    in
+    let init =
+      Option.map
+        ~f:(fun e ->
+          let e = c_expr e in
+          { e with e = Block (e, W.block) })
+        o_expr
+      |> Option.value ~default:(unit_expr full_span)
+    in
+    List.fold_right o_stmts ~init ~f:(fun { kind; _ } body ->
+        match kind with
+        | Expr { expr = rhs; _ } ->
+            let rhs = c_expr rhs in
+            let e =
+              Let { monadic = None; lhs = wild_pat rhs.span rhs.typ; rhs; body }
+            in
+            { e; typ; span = Span.union rhs.span body.span }
+        | Let
+            {
+              else_block = Some { expr; span; stmts; _ };
+              pattern = lhs;
+              initializer' = Some rhs;
+              _;
+            } ->
+            let lhs = c_pat lhs in
+            let rhs = c_expr rhs in
+            let else_block = c_block ~expr ~span ~stmts ~ty in
+            let lhs_body_span = Span.union lhs.span body.span in
+            let e =
+              Match
+                {
+                  arms =
+                    [
+                      { arm = { arm_pat = lhs; body }; span = lhs_body_span };
+                      {
+                        arm =
+                          {
+                            arm_pat =
+                              {
+                                p = PWild;
+                                span = else_block.span;
+                                typ = lhs.typ;
+                              };
+                            body = { else_block with typ = body.typ };
+                          };
+                        span = else_block.span;
+                      };
+                    ];
+                  scrutinee = rhs;
+                }
+            in
+            { e; typ; span = full_span }
+        | Let { initializer' = None; _ } ->
+            unimplemented ~issue_id:156 [ span ]
+              "Sorry, Hax does not support declare-first let bindings (see \
+               https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) \
+               for now."
+        | Let { pattern = lhs; initializer' = Some rhs; _ } ->
+            let lhs = c_pat lhs in
+            let rhs = c_expr rhs in
+            let e = Let { monadic = None; lhs; rhs; body } in
+            { e; typ; span = Span.union rhs.span body.span })
+
   and c_expr_unwrapped (e : Thir.decorated_for__expr_kind) : expr =
     (* TODO: eliminate that `call`, use the one from `ast_utils` *)
     let call f args =
@@ -516,61 +594,8 @@ end) : EXPR = struct
       | Let _ -> unimplemented [ e.span ] "Let"
       | Block { safety_mode = BuiltinUnsafe | ExplicitUnsafe; _ } ->
           unsafe_block [ e.span ]
-      | Block o ->
-          (* if there is no expression & the last expression is ⊥, just use that *)
-          let lift_last_statement_as_expr_if_possible expr stmts (ty : Thir.ty)
-              =
-            match (ty, expr, List.drop_last stmts, List.last stmts) with
-            | ( Thir.Never,
-                None,
-                Some stmts,
-                Some ({ kind = Thir.Expr { expr; _ }; _ } : Thir.stmt) ) ->
-                (stmts, Some expr)
-            | _ -> (stmts, expr)
-          in
-          let o_stmts, o_expr =
-            lift_last_statement_as_expr_if_possible o.expr o.stmts e.ty
-          in
-          let init =
-            Option.map
-              ~f:(fun e ->
-                let e = c_expr e in
-                { e with e = Block (e, W.block) })
-              o_expr
-            |> Option.value ~default:(unit_expr span)
-          in
-          let { e; _ } =
-            List.fold_right o_stmts ~init ~f:(fun { kind; _ } body ->
-                match kind with
-                | Expr { expr = rhs; _ } ->
-                    let rhs = c_expr rhs in
-                    let e =
-                      Let
-                        {
-                          monadic = None;
-                          lhs = wild_pat rhs.span rhs.typ;
-                          rhs;
-                          body;
-                        }
-                    in
-                    { e; typ; span = Span.union rhs.span body.span }
-                | Let { else_block = Some _; _ } ->
-                    unimplemented ~issue_id:155 [ e.span ]
-                      "Sorry, Hax does not support [let-else] (see \
-                       https://doc.rust-lang.org/rust-by-example/flow_control/let_else.html) \
-                       for now."
-                | Let { initializer' = None; _ } ->
-                    unimplemented ~issue_id:156 [ e.span ]
-                      "Sorry, Hax does not support declare-first let bindings \
-                       (see \
-                       https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) \
-                       for now."
-                | Let { pattern = lhs; initializer' = Some rhs; _ } ->
-                    let lhs = c_pat lhs in
-                    let rhs = c_expr rhs in
-                    let e = Let { monadic = None; lhs; rhs; body } in
-                    { e; typ; span = Span.union rhs.span body.span })
-          in
+      | Block { expr; span; stmts; _ } ->
+          let { e; _ } = c_block ~expr ~span ~stmts ~ty:e.ty in
           e
       | Assign { lhs; rhs } ->
           let lhs = c_expr lhs in

test-harness/src/snapshots/toolchain__let-else into-coq.snap

@@ -0,0 +1,55 @@
+---
+source: test-harness/src/harness.rs
+expression: snapshot
+info:
+  kind:
+    Translate:
+      backend: coq
+  info:
+    name: let-else
+    manifest: let-else/Cargo.toml
+    description: ~
+  spec:
+    optional: false
+    broken: false
+    issue_id: ~
+    positive: true
+    snapshot:
+      stderr: false
+      stdout: true
+    include_flag: ~
+    backend_options: ~
+---
+exit = 0
+
+[stdout]
+diagnostics = []
+
+[stdout.files]
+"Let_else.v" = '''
+(* File automatically generated by Hacspec *)
+From Hacspec Require Import Hacspec_Lib MachineIntegers.
+From Coq Require Import ZArith.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+
+(*Not implemented yet? todo(item)*)
+
+Definition let_else (opt : t_Option_t int32) : bool :=
+  run match opt with
+  | Option_Some x =>
+    ControlFlow_Continue true
+  | _ =>
+    ControlFlow_Break false
+  end.
+
+Definition let_else_different_type (opt : t_Option_t int32) : bool :=
+  run (let hoist1 := match opt with
+    | Option_Some x =>
+      ControlFlow_Continue (Option_Some (x.+(@repr WORDSIZE32 1)))
+    | _ =>
+      ControlFlow_Break false
+    end : t_Option_t int32 in
+  ControlFlow_Continue (let_else hoist1)).
+'''

test-harness/src/snapshots/toolchain__let-else into-fstar.snap

@@ -0,0 +1,45 @@
+---
+source: test-harness/src/harness.rs
+expression: snapshot
+info:
+  kind:
+    Translate:
+      backend: fstar
+  info:
+    name: let-else
+    manifest: let-else/Cargo.toml
+    description: ~
+  spec:
+    optional: false
+    broken: false
+    issue_id: ~
+    positive: true
+    snapshot:
+      stderr: false
+      stdout: true
+    include_flag: ~
+    backend_options: ~
+---
+exit = 0
+
+[stdout]
+diagnostics = []
+
+[stdout.files]
+"Let_else.fst" = '''
+module Let_else
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let let_else (opt: Core.Option.t_Option u32) : bool =
+  match opt with
+  | Core.Option.Option_Some x -> true
+  | _ -> false
+
+let let_else_different_type (opt: Core.Option.t_Option u32) : bool =
+  match opt with
+  | Core.Option.Option_Some x ->
+    let_else (Core.Option.Option_Some (x +! 1ul <: u32) <: Core.Option.t_Option u32)
+  | _ -> false
+'''

test-harness/src/snapshots/toolchain__let-else into-ssprove.snap

@@ -0,0 +1,80 @@
+---
+source: test-harness/src/harness.rs
+expression: snapshot
+info:
+  kind:
+    Translate:
+      backend: ssprove
+  info:
+    name: let-else
+    manifest: let-else/Cargo.toml
+    description: ~
+  spec:
+    optional: false
+    broken: false
+    issue_id: ~
+    positive: true
+    snapshot:
+      stderr: false
+      stdout: true
+    include_flag: ~
+    backend_options: ~
+---
+exit = 0
+
+[stdout]
+diagnostics = []
+
+[stdout.files]
+"Let_else.v" = '''
+(* File automatically generated by Hacspec *)
+Set Warnings "-notation-overridden,-ambiguous-paths".
+From Crypt Require Import choice_type Package Prelude.
+Import PackageNotation.
+From extructures Require Import ord fset.
+From mathcomp Require Import word_ssrZ word.
+From Jasmin Require Import word.
+
+From Coq Require Import ZArith.
+From Coq Require Import Strings.String.
+Import List.ListNotations.
+Open Scope list_scope.
+Open Scope Z_scope.
+Open Scope bool_scope.
+
+From Hacspec Require Import ChoiceEquality.
+From Hacspec Require Import LocationUtility.
+From Hacspec Require Import Hacspec_Lib_Comparable.
+From Hacspec Require Import Hacspec_Lib_Pre.
+From Hacspec Require Import Hacspec_Lib.
+
+Open Scope hacspec_scope.
+Import choice.Choice.Exports.
+
+Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
+
+(*Not implemented yet? todo(item)*)
+
+Equations let_else {L1 : {fset Location}} {I1 : Interface} (opt : both L1 I1 (t_Option int32)) : both L1 I1 'bool :=
+  let_else opt  :=
+    solve_lift (run (matchb opt with
+    | Option_Some_case x =>
+      letb x := ret_both ((x) : (int32)) in
+      ControlFlow_Continue (solve_lift (ret_both (true : 'bool)))
+    | _ =>
+      ControlFlow_Break (solve_lift (ret_both (false : 'bool)))
+    end)) : both L1 I1 'bool.
+Fail Next Obligation.
+
+Equations let_else_different_type {L1 : {fset Location}} {I1 : Interface} (opt : both L1 I1 (t_Option int32)) : both L1 I1 'bool :=
+  let_else_different_type opt  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code 'bool] hoist1 := matchb opt with
+    | Option_Some_case x =>
+      letb x := ret_both ((x) : (int32)) in
+      ControlFlow_Continue (Option_Some (solve_lift (x .+ (ret_both (1 : int32)))))
+    | _ =>
+      ControlFlow_Break (solve_lift (ret_both (false : 'bool)))
+    end in
+    ControlFlow_Continue (let_else hoist1))) : both L1 I1 'bool.
+Fail Next Obligation.
+'''

tests/Cargo.toml

@@ -5,6 +5,7 @@ members = [
         "slices",
         "naming",
         "if-let",
+        "let-else",
         "enum-repr",
         "pattern-or",
         "side-effects",

tests/let-else/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "let-else"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+
+[package.metadata.hax-tests]
+into."fstar+coq+ssprove" = { broken = false, snapshot = "stdout", issue_id = "155" }

tests/let-else/src/lib.rs

@@ -0,0 +1,13 @@
+#![allow(dead_code)]
+
+pub fn let_else(opt: Option<u32>) -> bool {
+    let Some(x) = opt else { return false };
+    true
+}
+
+pub fn let_else_different_type(opt: Option<u32>) -> bool {
+    let_else({
+        let Some(x) = opt else { return false };
+        Some(x + 1)
+    })
+}