Skip to content

Commit aa83c98

Browse files
abentkampabentkamp
authored
Merge branch 'main' into alex/shift-left
2 parents 08712e7 + cc85bb6 commit aa83c98

File tree

8 files changed

+204
-60
lines changed

8 files changed

+204
-60
lines changed

‎CHANGELOG.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@ Changes to the Lean backend:
3131
not introduce extra `do` block (#1746)
3232
- Rename `Result` monad to `RustM` to avoid confusion with Rust `Result` type (#1768)
3333
- Add support for shift-left (#1785)
34+
- Add support for default methods of traits (#1777)
3435

3536
Miscellaneous:
3637
- Reserve extraction folder for auto-generated files in Lean examples (#1754)

‎engine/backends/lean/lean_backend.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ include
1414
include On.Quote
1515
include On.Dyn
1616
include On.Unsafe
17+
include On.Trait_item_default
1718
end)
1819
(struct
1920
let backend = Diagnostics.Backend.FStar
@@ -45,7 +46,7 @@ module SubtypeToInputLanguage
4546
and type state_passing_loop = Features.Off.state_passing_loop
4647
and type fold_like_loop = Features.Off.fold_like_loop
4748
and type match_guard = Features.Off.match_guard
48-
and type trait_item_default = Features.Off.trait_item_default) =
49+
and type trait_item_default = Features.On.trait_item_default) =
4950
struct
5051
module FB = InputLanguage
5152

@@ -120,7 +121,6 @@ module TransformToInputLanguage =
120121
|> Phases.Traits_specs
121122
|> Phases.Simplify_hoisting
122123
|> Phases.Newtype_as_refinement
123-
|> Phases.Reject.Trait_item_default
124124
|> Phases.Bundle_cycles
125125
|> Phases.Reorder_fields
126126
|> Phases.Sort_items

‎rust-engine/src/backends/lean.rs‎

Lines changed: 28 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -325,6 +325,16 @@ const _: () = {
325325
fn do_block<A: 'static + Clone, D: ToDocument<Self, A>>(&self, body: D) -> DocBuilder<A> {
326326
docs!["do", line!(), body].group()
327327
}
328+
329+
/// Produces a fresh name for a constraint on an associated type. It needs a fresh name to
330+
/// be added as an extra field
331+
fn fresh_constraint_name(
332+
&self,
333+
associated_type_name: &String,
334+
constraint: &ImplIdent,
335+
) -> String {
336+
format!("_constr_{}_{}", associated_type_name, constraint.name)
337+
}
328338
}
329339

330340
impl<A: 'static + Clone> PrettyAst<A> for LeanPrinter {
@@ -963,7 +973,7 @@ set_option linter.unusedVariables false
963973
.map(|constraint: &GenericConstraint| {
964974
match constraint {
965975
GenericConstraint::Type(tc_constraint) => docs![
966-
format!("_constr_{}", tc_constraint.name),
976+
self.fresh_constraint_name(&self.render_last(name), tc_constraint),
967977
" :",
968978
line!(),
969979
constraint
@@ -1079,7 +1089,7 @@ set_option linter.unusedVariables false
10791089
concat!(constraints.iter().map(|c| docs![
10801090
hardline!(),
10811091
docs![
1082-
format!("_constr_{}", c.name),
1092+
self.fresh_constraint_name(&name, c),
10831093
reflow!(" :"),
10841094
line!(),
10851095
&c.goal
@@ -1090,8 +1100,22 @@ set_option linter.unusedVariables false
10901100
]))
10911101
]
10921102
}
1093-
TraitItemKind::Default { .. } =>
1094-
emit_error!(issue 1707, "Unsupported default implementation for trait items"),
1103+
TraitItemKind::Default { params, body } => docs![
1104+
docs![
1105+
name,
1106+
softline!(),
1107+
generics,
1108+
zip_right!(params, line!()).group(),
1109+
docs![": RustM ", body.ty].group(),
1110+
line!(),
1111+
":= do",
1112+
]
1113+
.group(),
1114+
line!(),
1115+
body,
1116+
]
1117+
.group()
1118+
.nest(INDENT),
10951119
TraitItemKind::Resugared(_) => {
10961120
unreachable!("This backend has no resugaring for trait items")
10971121
}

‎test-harness/src/snapshots/toolchain__lean-core-models into-lean.snap‎

Lines changed: 43 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -42,8 +42,8 @@ set_option mvcgen.warning false
4242
set_option linter.unusedVariables false
4343

4444
inductive Lean_core_models.Result.E1 : Type
45-
| C1 : Lean_core_models.Result.E1
46-
| C2 : u32 -> Lean_core_models.Result.E1
45+
| C1 : Lean_core_models.Result.E1
46+
| C2 : u32 -> Lean_core_models.Result.E1
4747

4848

4949
instance Lean_core_models.Result.Impl :
@@ -52,64 +52,64 @@ instance Lean_core_models.Result.Impl :
5252

5353

5454
inductive Lean_core_models.Result.E2 : Type
55-
| C1 : Lean_core_models.Result.E2
56-
| C2 : u32 -> Lean_core_models.Result.E2
55+
| C1 : Lean_core_models.Result.E2
56+
| C2 : u32 -> Lean_core_models.Result.E2
5757

5858

5959
def Lean_core_models.Result.tests
6060
(_ : Rust_primitives.Hax.Tuple0)
61-
: Result (Core.Result.Result u32 Lean_core_models.Result.E1)
61+
: RustM (Core.Result.Result u32 Lean_core_models.Result.E1)
6262
:= do
6363
let v1 : (Core.Result.Result u32 Lean_core_models.Result.E1) :=
6464
(Core.Result.Result.Ok (1 : u32));
6565
let v2 : (Core.Result.Result u32 Lean_core_models.Result.E1) :=
6666
(Core.Result.Result.Err Lean_core_models.Result.E1.C1);
67-
let f : (u32 -> Result u32) := (fun x => (do (x +? (1 : u32)) : Result u32));
67+
let f : (u32 -> RustM u32) := (fun x => (do (x +? (1 : u32)) : RustM u32));
6868
let v5 : (Core.Result.Result i32 Lean_core_models.Result.E1) ←
69-
(Core.Result.Impl.map i32 Lean_core_models.Result.E1 i32 (i32 -> Result i32)
69+
(Core.Result.Impl.map i32 Lean_core_models.Result.E1 i32 (i32 -> RustM i32)
7070
(Core.Result.Result.Ok (1 : i32))
71-
(fun v => (do (v +? (1 : i32)) : Result i32)));
71+
(fun v => (do (v +? (1 : i32)) : RustM i32)));
7272
let v6 : u32 ←
7373
(Core.Result.Impl.map_or
7474
u32
7575
Lean_core_models.Result.E1
7676
u32
77-
(u32 -> Result u32) (Core.Result.Result.Ok (1 : u32)) (9 : u32) f);
77+
(u32 -> RustM u32) (Core.Result.Result.Ok (1 : u32)) (9 : u32) f);
7878
let v7 : u32 ←
7979
(Core.Result.Impl.map_or_else
8080
u32
8181
Lean_core_models.Result.E1
8282
u32
83-
(Lean_core_models.Result.E1 -> Result u32)
84-
(u32 -> Result u32)
83+
(Lean_core_models.Result.E1 -> RustM u32)
84+
(u32 -> RustM u32)
8585
(Core.Result.Result.Ok (1 : u32))
86-
(fun _ => (do (pure (10 : u32)) : Result u32))
86+
(fun _ => (do (pure (10 : u32)) : RustM u32))
8787
f);
8888
let v8 : (Core.Result.Result i32 Lean_core_models.Result.E2) ←
8989
(Core.Result.Impl.map_err
9090
i32
9191
Lean_core_models.Result.E1
9292
Lean_core_models.Result.E2
93-
(Lean_core_models.Result.E1 -> Result Lean_core_models.Result.E2)
93+
(Lean_core_models.Result.E1 -> RustM Lean_core_models.Result.E2)
9494
(Core.Result.Result.Ok (0 : i32))
9595
(fun e => (do
9696
match e with
9797
| (Lean_core_models.Result.E1.C1 )
9898
=> (pure Lean_core_models.Result.E2.C1)
9999
| (Lean_core_models.Result.E1.C2 x)
100100
=> (pure (Lean_core_models.Result.E2.C2 (← (x +? (1 : u32))))) :
101-
Result Lean_core_models.Result.E2)));
101+
RustM Lean_core_models.Result.E2)));
102102
let v9 : Bool ← (Core.Result.Impl.is_ok u32 Lean_core_models.Result.E1 v1);
103103
let v10 : Bool ← (Core.Result.Impl.is_err u32 Lean_core_models.Result.E1 v1);
104104
let v11 : (Core.Result.Result u32 Lean_core_models.Result.E1) ←
105105
(Core.Result.Impl.and_then
106106
u32
107107
Lean_core_models.Result.E1
108108
u32
109-
(u32 -> Result (Core.Result.Result u32 Lean_core_models.Result.E1))
109+
(u32 -> RustM (Core.Result.Result u32 Lean_core_models.Result.E1))
110110
(← (Core.Clone.Clone.clone v1))
111111
(fun x => (do
112-
(pure (Core.Result.Result.Ok (← (x +? (1 : u32))))) : Result
112+
(pure (Core.Result.Result.Ok (← (x +? (1 : u32))))) : RustM
113113
(Core.Result.Result u32 Lean_core_models.Result.E1))));
114114
let v12 : u32 ←
115115
(Core.Result.Impl.unwrap u32 u32
@@ -123,7 +123,7 @@ def Lean_core_models.Result.tests
123123
u32
124124
Lean_core_models.Result.E1
125125
u32
126-
(u32 -> Result u32) v1 f))
126+
(u32 -> RustM u32) v1 f))
127127
with
128128
| (Core.Result.Result.Ok hoist2)
129129
=>
@@ -139,7 +139,7 @@ structure Lean_core_models.Option.S where
139139
f1 : u32
140140

141141
inductive Lean_core_models.Option.E : Type
142-
| C : u32 -> Lean_core_models.Option.E
142+
| C : u32 -> Lean_core_models.Option.E
143143

144144

145145
instance Lean_core_models.Option.Impl :
@@ -150,20 +150,20 @@ instance Lean_core_models.Option.Impl :
150150

151151
def Lean_core_models.Option.test
152152
(_ : Rust_primitives.Hax.Tuple0)
153-
: Result Rust_primitives.Hax.Tuple0
153+
: RustM Rust_primitives.Hax.Tuple0
154154
:= do
155155
let o1 : (Core.Option.Option i32) := (Core.Option.Option.Some (4 : i32));
156156
let o2 : (Core.Option.Option i32) := Core.Option.Option.None;
157157
let o3 : Bool ←
158-
(Core.Option.Impl.is_some_and i32 (i32 -> Result Bool)
158+
(Core.Option.Impl.is_some_and i32 (i32 -> RustM Bool)
159159
(← (Core.Clone.Clone.clone o1))
160160
(fun x => (do
161-
(Rust_primitives.Hax.Machine_int.eq x (0 : i32)) : Result Bool)));
161+
(Rust_primitives.Hax.Machine_int.eq x (0 : i32)) : RustM Bool)));
162162
let o3 : Bool ←
163-
(Core.Option.Impl.is_none_or i32 (i32 -> Result Bool)
163+
(Core.Option.Impl.is_none_or i32 (i32 -> RustM Bool)
164164
(← (Core.Clone.Clone.clone o1))
165165
(fun x => (do
166-
(Rust_primitives.Hax.Machine_int.eq x (0 : i32)) : Result Bool)));
166+
(Rust_primitives.Hax.Machine_int.eq x (0 : i32)) : RustM Bool)));
167167
let o4 : i32 ←
168168
(Core.Option.Impl.unwrap i32 (Core.Option.Option.Some (0 : i32)));
169169
let o5 : i32 ←
@@ -173,30 +173,30 @@ def Lean_core_models.Option.test
173173
let o6 : i32 ←
174174
(Core.Option.Impl.unwrap_or_else
175175
i32
176-
(Rust_primitives.Hax.Tuple0 -> Result i32)
176+
(Rust_primitives.Hax.Tuple0 -> RustM i32)
177177
(Core.Option.Option.Some (0 : i32))
178-
(fun _ => (do (pure (9 : i32)) : Result i32)));
178+
(fun _ => (do (pure (9 : i32)) : RustM i32)));
179179
let o7 : Lean_core_models.Option.S ←
180180
(Core.Option.Impl.unwrap_or_default Lean_core_models.Option.S
181181
Core.Option.Option.None);
182182
let o8 : (Core.Option.Option i32) ←
183-
(Core.Option.Impl.map i32 i32 (i32 -> Result i32)
183+
(Core.Option.Impl.map i32 i32 (i32 -> RustM i32)
184184
(Core.Option.Option.Some (0 : i32))
185-
(fun x => (do (x +? (1 : i32)) : Result i32)));
185+
(fun x => (do (x +? (1 : i32)) : RustM i32)));
186186
let o9 : i32 ←
187-
(Core.Option.Impl.map_or i32 i32 (i32 -> Result i32)
187+
(Core.Option.Impl.map_or i32 i32 (i32 -> RustM i32)
188188
(Core.Option.Option.Some (1 : i32))
189189
(9 : i32)
190-
(fun x => (do (x +? (1 : i32)) : Result i32)));
190+
(fun x => (do (x +? (1 : i32)) : RustM i32)));
191191
let o10 : i32 ←
192192
(Core.Option.Impl.map_or_else
193193
i32
194194
i32
195-
(Rust_primitives.Hax.Tuple0 -> Result i32)
196-
(i32 -> Result i32)
195+
(Rust_primitives.Hax.Tuple0 -> RustM i32)
196+
(i32 -> RustM i32)
197197
(Core.Option.Option.Some (2 : i32))
198-
(fun _ => (do (pure (9 : i32)) : Result i32))
199-
(fun x => (do (x +? (1 : i32)) : Result i32)));
198+
(fun _ => (do (pure (9 : i32)) : RustM i32))
199+
(fun x => (do (x +? (1 : i32)) : RustM i32)));
200200
let o11 : (Core.Result.Result i32 Lean_core_models.Option.E) ←
201201
(Core.Option.Impl.ok_or i32 Lean_core_models.Option.E
202202
(Core.Option.Option.Some (3 : i32))
@@ -205,16 +205,16 @@ def Lean_core_models.Option.test
205205
(Core.Option.Impl.ok_or_else
206206
i32
207207
Lean_core_models.Option.E
208-
(Rust_primitives.Hax.Tuple0 -> Result Lean_core_models.Option.E)
208+
(Rust_primitives.Hax.Tuple0 -> RustM Lean_core_models.Option.E)
209209
(Core.Option.Option.Some (1 : i32))
210210
(fun _ => (do
211-
(pure (Lean_core_models.Option.E.C (1 : u32))) : Result
211+
(pure (Lean_core_models.Option.E.C (1 : u32))) : RustM
212212
Lean_core_models.Option.E)));
213213
let o13 : (Core.Option.Option u32) ←
214-
(Core.Option.Impl.and_then u32 u32 (u32 -> Result (Core.Option.Option u32))
214+
(Core.Option.Impl.and_then u32 u32 (u32 -> RustM (Core.Option.Option u32))
215215
Core.Option.Option.None
216216
(fun x => (do
217-
(pure (Core.Option.Option.Some x)) : Result (Core.Option.Option u32))));
217+
(pure (Core.Option.Option.Some x)) : RustM (Core.Option.Option u32))));
218218
let ⟨_, out⟩ ←
219219
(Core.Option.Impl.take Lean_core_models.Option.S
220220
(Core.Option.Option.Some
@@ -243,7 +243,7 @@ instance Lean_core_models.Default.Structs.Impl :
243243

244244
def Lean_core_models.Default.Structs.test
245245
(_ : Rust_primitives.Hax.Tuple0)
246-
: Result Lean_core_models.Default.Structs.S
246+
: RustM Lean_core_models.Default.Structs.S
247247
:= do
248248
(Core.Default.Default.default Rust_primitives.Hax.Tuple0.mk)
249249

@@ -262,14 +262,12 @@ instance Lean_core_models.Default.Enums.Impl
262262

263263
def Lean_core_models.Function.test
264264
(_ : Rust_primitives.Hax.Tuple0)
265-
: Result u32
265+
: RustM u32
266266
:= do
267-
let f_1 : (u32 -> Result u32) :=
268-
(fun _ => (do (pure (9 : u32)) : Result u32));
269-
let f_2 : (u32 -> u32 -> Result u32) :=
270-
(fun x y => (do (x +? y) : Result u32));
271-
let f_2_tuple : ((Rust_primitives.Hax.Tuple2 u32 u32) -> Result u32) :=
272-
(fun ⟨x, y⟩ => (do (x +? y) : Result u32));
267+
let f_1 : (u32 -> RustM u32) := (fun _ => (do (pure (9 : u32)) : RustM u32));
268+
let f_2 : (u32 -> u32 -> RustM u32) := (fun x y => (do (x +? y) : RustM u32));
269+
let f_2_tuple : ((Rust_primitives.Hax.Tuple2 u32 u32) -> RustM u32) :=
270+
(fun ⟨x, y⟩ => (do (x +? y) : RustM u32));
273271
((← ((← (Core.Ops.Function.Fn.call
274272
f_1
275273
(Rust_primitives.Hax.Tuple1.mk (0 : u32))))

0 commit comments

Comments
 (0)