feat(lean): add pattern-matching on constant literals

CHANGELOG.md

@@ -31,6 +31,7 @@ Changes to the Lean backend:
    not introduce extra `do` block (#1746)
  - Rename `Result` monad to `RustM` to avoid confusion with Rust `Result` type (#1768)
  - Add support for default methods of traits (#1777)
+ - Add support for pattern matching on constant literals (#1789)
 
 Miscellaneous:
 - Reserve extraction folder for auto-generated files in Lean examples (#1754)

rust-engine/src/backends/lean.rs

@@ -662,9 +662,12 @@ set_option linter.unusedVariables false
                     emit_error!(issue 1712, "Unsupported pattern-matching on arrays")
                 }
                 PatKind::Deref { .. } => unreachable_by_invariant!(Drop_references),
-                PatKind::Constant { .. } => {
-                    emit_error!(issue 1712, "Unsupported pattern-matching on constants")
+                PatKind::Constant {
+                    lit: Literal::Float { .. },
+                } => {
+                    emit_error!(issue 1788, "Unsupported pattern-matching on floats")
                 }
+                PatKind::Constant { lit } => docs![lit],
                 PatKind::Construct {
                     constructor,
                     is_record,

test-harness/src/snapshots/toolchain__lean-tests into-lean.snap

@@ -861,6 +861,21 @@ def Lean_tests.Reject_do_dsl.test
   (pure (Rust_primitives.Hax.Tuple2.mk
     Rust_primitives.Hax.Tuple0.mk Rust_primitives.Hax.Tuple0.mk))
 
+def Lean_tests.Matching.test_matching
+  (x : u32)
+  (c : Char)
+  (s : String)
+  (b : Bool)
+  : RustM u32
+  := do
+  let x : u32 ← match x with | 0 => (pure (42 : u32)) | _ => (pure (0 : u32));
+  let c : u32 ← match c with | 'a' => (pure (42 : u32)) | _ => (pure (0 : u32));
+  let s : u32 ←
+    match s with | "Hello" => (pure (42 : u32)) | _ => (pure (0 : u32));
+  let b : u32 ←
+    match b with | true => (pure (42 : u32)) | false => (pure (0 : u32));
+  ((← ((← (x +? c)) +? s)) +? b)
+
 def Lean_tests.Loops.loop1 (_ : Rust_primitives.Hax.Tuple0) : RustM u32 := do
   let x : u32 := (0 : u32);
   let x : u32 ←

tests/lean-tests/src/lib.rs

@@ -6,6 +6,7 @@ pub mod constants;
 pub mod enums;
 pub mod ite;
 pub mod loops;
+pub mod matching;
 pub mod monadic;
 pub mod reject_do_dsl;
 pub mod structs;

tests/lean-tests/src/matching.rs

@@ -0,0 +1,19 @@
+fn test_matching(x: u32, c: char, s: &str, b: bool) -> u32 {
+    let x = match x {
+        0 => 42,
+        _ => 0,
+    };
+    let c = match c {
+        'a' => 42,
+        _ => 0,
+    };
+    let s = match s {
+        "Hello" => 42,
+        _ => 0,
+    };
+    let b = match b {
+        true => 42,
+        false => 0,
+    };
+    return x + c + s + b;
+}