From 9ecf552d2b7e2d1a0159cd49faa6ff3315a2e0f7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Wed, 8 Oct 2025 12:25:44 +0200 Subject: [PATCH 1/4] feat(lean): add support for base expression of structs --- rust-engine/src/backends/lean.rs | 30 +++++++++++++++++-- .../toolchain__lean-tests into-lean.snap | 21 +++++++++++++ tests/lean-tests/src/structs.rs | 29 ++++++++++++++++++ 3 files changed, 77 insertions(+), 3 deletions(-) diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index da5a31db9..99521db03 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -258,6 +258,23 @@ 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>, + { + macro_rules! line {($($tt:tt)*) => {disambiguated_line!($($tt)*)};} + 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, @@ -487,14 +504,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) diff --git a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap index b32ed21b8..826745dfe 100644 --- a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap +++ b/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 diff --git a/tests/lean-tests/src/structs.rs b/tests/lean-tests/src/structs.rs index 1ec171dd0..1dd582ca5 100644 --- a/tests/lean-tests/src/structs.rs +++ b/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 + }; + } +} From 7ed75a16e0f0404ac538a630a31a7d964b2f4be2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Wed, 8 Oct 2025 12:31:50 +0200 Subject: [PATCH 2/4] Changelog --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4c0f44476..691d71030 100644 --- a/CHANGELOG.md +++ b/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: From ca5432adde9414bad4e580d432d7ae1f7f00c53a Mon Sep 17 00:00:00 2001 From: maximebuyse <45398004+maximebuyse@users.noreply.github.com> Date: Wed, 8 Oct 2025 13:50:52 +0200 Subject: [PATCH 3/4] Update test_config.yaml. --- rustc-coverage-tests/test_config.yaml | 1 + 1 file changed, 1 insertion(+) diff --git a/rustc-coverage-tests/test_config.yaml b/rustc-coverage-tests/test_config.yaml index 007e80ee8..a4f720421 100644 --- a/rustc-coverage-tests/test_config.yaml +++ b/rustc-coverage-tests/test_config.yaml @@ -176,6 +176,7 @@ tests: - fstar inner_items: - json + - lean issue_83601: - json - coq From ab394caeba8d0bd1b8c65771003ca28c2a8f10ef Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Wed, 8 Oct 2025 14:37:45 +0200 Subject: [PATCH 4/4] refactor(lean): Remove duplicated macro definition --- rust-engine/src/backends/lean.rs | 3 --- 1 file changed, 3 deletions(-) diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 99521db03..dcc980633 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -266,7 +266,6 @@ const _: () = { where &'b D: Pretty<'a, Self, A>, { - macro_rules! line {($($tt:tt)*) => {disambiguated_line!($($tt)*)};} docs![intersperse!( fields .iter() @@ -283,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] @@ -303,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() }