feat(lean): add support for base expression of structs

CHANGELOG.md

@@ -16,6 +16,7 @@ Change to cargo-hax:
 Changes to hax-lib:
 
 Changes to the Lean backend:
+ - Add support for base-expressions of structs (#1736)
 
 Miscellaneous:
 

rust-engine/src/backends/lean.rs

@@ -258,6 +258,22 @@ const _: () = {
             }
         }
 
+        /// Prints fields of structures (when in braced notation)
+        fn struct_fields<'a, 'b, A: 'a + Clone, D>(
+            &'a self,
+            fields: &'b [(GlobalId, D)],
+        ) -> DocBuilder<'a, Self, A>
+        where
+            &'b D: Pretty<'a, Self, A>,
+        {
+            docs![intersperse!(
+                fields
+                    .iter()
+                    .map(|(id, e)| { docs![self.render_last(id), reflow!(" := "), e].group() }),
+                docs![",", line!()]
+            )]
+            .group()
+        }
         /// Prints named arguments (record) of a variant or constructor of struct
         fn named_arguments<'a, 'b, A: 'a + Clone, D>(
             &'a self,
@@ -266,7 +282,6 @@ const _: () = {
         where
             &'b D: Pretty<'a, Self, A>,
         {
-            macro_rules! line {($($tt:tt)*) => {disambiguated_line!($($tt)*)};}
             docs![intersperse!(
                 fields.iter().map(|(id, e)| {
                     docs![self.render_last(id), reflow!(" := "), e]
@@ -286,7 +301,6 @@ const _: () = {
         where
             &'b D: Pretty<'a, Self, A>,
         {
-            macro_rules! line {($($tt:tt)*) => {disambiguated_line!($($tt)*)};}
             docs![intersperse!(fields.iter().map(|(_, e)| e), line!())].group()
         }
 
@@ -487,14 +501,21 @@ set_option linter.unusedVariables false
                 ExprKind::Construct {
                     constructor,
                     is_record,
-                    is_struct: _,
+                    is_struct,
                     fields,
                     base,
                 } => {
                     if fields.is_empty() && base.is_none() {
                         docs![constructor]
-                    } else if base.is_some() {
-                        emit_error!(issue 1637, "Unsupported base expressions for structs.")
+                    } else if let Some(base) = base {
+                        if !(*is_record && *is_struct) {
+                            unreachable!(
+                                "Constructors with base expressions are necessarily structs with record-like arguments"
+                            )
+                        }
+                        docs![base, line!(), reflow!("with "), self.struct_fields(fields)]
+                            .braces()
+                            .group()
                     } else {
                         docs![constructor, line!(), self.arguments(fields, is_record)]
                             .nest(INDENT)

rustc-coverage-tests/test_config.yaml

@@ -176,6 +176,7 @@ tests:
     - fstar
   inner_items:
     - json
+    - lean
   issue_83601:
     - json
     - coq

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

@@ -273,6 +273,27 @@ def Lean_tests.Structs.Miscellaneous.test_tuples
       (Rust_primitives.Hax.Tuple2.mk z z)));
   (Rust_primitives.Hax.Tuple2.mk (1 : i32) (2 : i32))
 
+structure Lean_tests.Structs.Base_expressions.S where
+  f1 : u32
+  f2 : u32
+  f3 : u32
+
+def Lean_tests.Structs.Base_expressions.test
+  (_ : Rust_primitives.Hax.Tuple0)
+  : Result Rust_primitives.Hax.Tuple0
+  := do
+  let s1 : Lean_tests.Structs.Base_expressions.S ← (pure
+    (Lean_tests.Structs.Base_expressions.S.mk
+      (f1 := (1 : u32)) (f2 := (2 : u32)) (f3 := (3 : u32))));
+  let _ ← (pure {s1 with f1 := (0 : u32)});
+  let _ ← (pure {s1 with f2 := (0 : u32)});
+  let _ ← (pure {s1 with f3 := (0 : u32)});
+  let _ ← (pure {s1 with f1 := (0 : u32), f2 := (1 : u32)});
+  let _ ← (pure {s1 with f2 := (0 : u32), f3 := (1 : u32)});
+  let _ ← (pure {s1 with f3 := (0 : u32), f1 := (2 : u32)});
+  let _ ← (pure {s1 with f1 := (0 : u32), f2 := (1 : u32), f3 := (0 : u32)});
+  Rust_primitives.Hax.Tuple0.mk
+
 structure Lean_tests.Structs.T0 where
 
 

tests/lean-tests/src/structs.rs

@@ -162,3 +162,32 @@ mod miscellaneous {
         (1, 2)
     }
 }
+
+mod base_expressions {
+
+    struct S {
+        f1: u32,
+        f2: u32,
+        f3: u32,
+    }
+
+    fn test() {
+        let s1 = S {
+            f1: 1,
+            f2: 2,
+            f3: 3,
+        };
+        let _ = S { f1: 0, ..s1 };
+        let _ = S { f2: 0, ..s1 };
+        let _ = S { f3: 0, ..s1 };
+        let _ = S { f1: 0, f2: 1, ..s1 };
+        let _ = S { f2: 0, f3: 1, ..s1 };
+        let _ = S { f3: 0, f1: 2, ..s1 };
+        let _ = S {
+            f1: 0,
+            f2: 1,
+            f3: 0,
+            ..s1
+        };
+    }
+}