Add test for let-else.

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)
+    })
+}