Skip to content

Commit dcedba5

Browse files
clementblaudeauclementblaudeau
committed
Factor generics printing
1 parent 73cd86f commit dcedba5

File tree

3 files changed

+154
-43
lines changed

3 files changed

+154
-43
lines changed

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

Lines changed: 44 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -362,19 +362,13 @@ set_option linter.unusedVariables false
362362
// TODO : The lean backend should not ignore constraints on generic params, see
363363
// https://github.com/cryspen/hax/issues/1636
364364
docs![
365-
concat!(params.iter().map(|param| {
366-
match param.kind {
367-
GenericParamKind::Lifetime => unreachable!(),
368-
GenericParamKind::Type => docs![param, reflow!(" : Type")]
369-
.parens()
370-
.group()
371-
.append(line!()),
372-
GenericParamKind::Const { .. } => {
373-
todo!("-- Unsupported const param")
374-
}
375-
}
376-
})),
377-
zip_right!(constraints, line!()),
365+
zip_right!(params, line!()),
366+
zip_right!(
367+
constraints
368+
.iter()
369+
.map(|constraint| docs![constraint].brackets()),
370+
line!()
371+
),
378372
]
379373
.group()
380374
}
@@ -384,11 +378,23 @@ set_option linter.unusedVariables false
384378
generic_constraint: &'b GenericConstraint,
385379
) -> DocBuilder<'a, Self, A> {
386380
match generic_constraint {
387-
GenericConstraint::Type(impl_ident) => docs![impl_ident].brackets(),
381+
GenericConstraint::Type(impl_ident) => docs![impl_ident],
388382
_ => todo!("-- unsupported constraint"),
389383
}
390384
}
391385

386+
fn generic_param(&'a self, generic_param: &'b GenericParam) -> DocBuilder<'a, Self, A> {
387+
match generic_param.kind() {
388+
GenericParamKind::Type => docs![&generic_param.ident, reflow!(" : Type")]
389+
.parens()
390+
.group(),
391+
GenericParamKind::Lifetime => unreachable!(),
392+
GenericParamKind::Const { .. } => {
393+
todo!("-- Unsupported const param")
394+
}
395+
}
396+
}
397+
392398
fn pat(&'a self, pat: &'b Pat) -> DocBuilder<'a, Self, A> {
393399
docs![&*pat.kind, reflow!(" : "), &pat.ty].parens().group()
394400
}
@@ -790,10 +796,6 @@ set_option linter.unusedVariables false
790796
docs![&param.pat]
791797
}
792798

793-
fn generic_param(&'a self, generic_param: &'b GenericParam) -> DocBuilder<'a, Self, A> {
794-
docs![&generic_param.ident]
795-
}
796-
797799
fn item(
798800
&'a self,
799801
item @ Item {
@@ -911,37 +913,36 @@ set_option linter.unusedVariables false
911913
docs![
912914
docs![
913915
docs![reflow!("class "), name],
916+
(!generics.params.is_empty()).then_some(docs![
917+
line!(),
918+
intersperse!(&generics.params, line!()).group()
919+
]),
914920
line!(),
915-
zip_right!(
916-
generics
917-
.params
918-
.iter()
919-
.map(|p| docs![p, reflow!(" : Type")].parens().group()),
920-
line!()
921-
)
922-
.group(),
923921
"where"
924922
]
925923
.group(),
926924
hardline!(),
927-
zip_right!(
928-
generics.constraints.iter().map(|c| {
929-
match c {
930-
GenericConstraint::Type(tc_constraint) => docs![
931-
format!("_constr_{}", tc_constraint.name),
932-
reflow!(" :"),
933-
line!(),
934-
&tc_constraint.goal
935-
]
936-
.nest(INDENT)
937-
.group()
938-
.brackets(),
939-
GenericConstraint::Lifetime(_) => unreachable!(),
940-
GenericConstraint::Projection(_projection_predicate) => todo!(),
941-
}
942-
}),
925+
(!generics.constraints.is_empty()).then_some(docs![zip_right!(
926+
generics
927+
.constraints
928+
.iter()
929+
.map(|constraint: &GenericConstraint| {
930+
match constraint {
931+
GenericConstraint::Type(tc_constraint) => docs![
932+
format!("_constr_{}", tc_constraint.name),
933+
" :",
934+
line!(),
935+
constraint
936+
]
937+
.group()
938+
.brackets(),
939+
_ => {
940+
todo!("unsupported type constraint in trait definition")
941+
}
942+
}
943+
}),
943944
hardline!()
944-
),
945+
)]),
945946
intersperse!(
946947
items.iter().filter(|item| {
947948
// TODO: should be treated directly by name rendering, see :

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

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,65 @@ def Lean_tests.Traits.Overlapping_methods.test
7474
+? (← Lean_tests.Traits.Overlapping_methods.T2.f x))
7575
+? (← Lean_tests.Traits.Overlapping_methods.T3.f x))
7676

77+
class Lean_tests.Traits.Inheritance.T1 (Self : Type) where
78+
f1 : Self -> Result usize
79+
80+
class Lean_tests.Traits.Inheritance.T2 (Self : Type) where
81+
f2 : Self -> Result usize
82+
83+
class Lean_tests.Traits.Inheritance.T3 (Self : Type) where
84+
[_constr_5860918688139008796 : (Lean_tests.Traits.Inheritance.T2 Self)]
85+
[_constr_2614080591691505761 : (Lean_tests.Traits.Inheritance.T1 Self)]
86+
f3 : Self -> Result usize
87+
88+
class Lean_tests.Traits.Inheritance.Tp1 (Self : Type) where
89+
f1 : Self -> Result usize
90+
91+
class Lean_tests.Traits.Inheritance.Tp2 (Self : Type) where
92+
[_constr_9900012313089209274 : (Lean_tests.Traits.Inheritance.Tp1 Self)]
93+
[_constr_3518312647081482353 : (Lean_tests.Traits.Inheritance.T3 Self)]
94+
fp2 : Self -> Result usize
95+
96+
structure Lean_tests.Traits.Inheritance.S where
97+
98+
99+
instance Lean_tests.Traits.Inheritance.Impl :
100+
Lean_tests.Traits.Inheritance.T1 Lean_tests.Traits.Inheritance.S
101+
where
102+
f1 (self : Lean_tests.Traits.Inheritance.S) := do (1 : usize)
103+
104+
instance Lean_tests.Traits.Inheritance.Impl_1 :
105+
Lean_tests.Traits.Inheritance.T2 Lean_tests.Traits.Inheritance.S
106+
where
107+
f2 (self : Lean_tests.Traits.Inheritance.S) := do (2 : usize)
108+
109+
instance Lean_tests.Traits.Inheritance.Impl_2 :
110+
Lean_tests.Traits.Inheritance.T3 Lean_tests.Traits.Inheritance.S
111+
where
112+
f3 (self : Lean_tests.Traits.Inheritance.S) := do (3 : usize)
113+
114+
instance Lean_tests.Traits.Inheritance.Impl_3 :
115+
Lean_tests.Traits.Inheritance.Tp1 Lean_tests.Traits.Inheritance.S
116+
where
117+
f1 (self : Lean_tests.Traits.Inheritance.S) := do (10 : usize)
118+
119+
instance Lean_tests.Traits.Inheritance.Impl_4 :
120+
Lean_tests.Traits.Inheritance.Tp2 Lean_tests.Traits.Inheritance.S
121+
where
122+
fp2 (self : Lean_tests.Traits.Inheritance.S) := do
123+
(← (← (← (← Lean_tests.Traits.Inheritance.Tp1.f1 self)
124+
+? (← Lean_tests.Traits.Inheritance.T1.f1 self))
125+
+? (← Lean_tests.Traits.Inheritance.T2.f2 self))
126+
+? (← Lean_tests.Traits.Inheritance.T3.f3 self))
127+
128+
def Lean_tests.Traits.Inheritance.test
129+
(_ : Rust_primitives.Hax.Tuple0)
130+
: Result usize
131+
:= do
132+
let s : Lean_tests.Traits.Inheritance.S ← (pure
133+
Lean_tests.Traits.Inheritance.S.mk);
134+
(← (← Lean_tests.Traits.Inheritance.T3.f3 s) +? (1 : usize))
135+
77136
class Lean_tests.Traits.Bounds.T1 (Self : Type) where
78137
f1 : Self -> Result usize
79138

‎tests/lean-tests/src/traits.rs‎

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -118,3 +118,54 @@ mod overlapping_methods {
118118
T1::f(&x) + T2::f(&x) + T3::f(&x)
119119
}
120120
}
121+
122+
mod inheritance {
123+
trait T1 {
124+
fn f1(&self) -> usize;
125+
}
126+
trait T2 {
127+
fn f2(&self) -> usize;
128+
}
129+
trait T3: T2 + T1 {
130+
fn f3(&self) -> usize;
131+
}
132+
trait Tp1 {
133+
fn f1(&self) -> usize;
134+
}
135+
trait Tp2: Tp1 + T3 {
136+
fn fp2(&self) -> usize;
137+
}
138+
139+
struct S {}
140+
impl T1 for S {
141+
fn f1(&self) -> usize {
142+
1
143+
}
144+
}
145+
impl T2 for S {
146+
fn f2(&self) -> usize {
147+
2
148+
}
149+
}
150+
impl T3 for S {
151+
fn f3(&self) -> usize {
152+
3
153+
}
154+
}
155+
156+
impl Tp1 for S {
157+
fn f1(&self) -> usize {
158+
10
159+
}
160+
}
161+
162+
impl Tp2 for S {
163+
fn fp2(&self) -> usize {
164+
Tp1::f1(self) + T1::f1(self) + T2::f2(self) + T3::f3(self)
165+
}
166+
}
167+
fn test() -> usize {
168+
let s = S {};
169+
s.f3() + 1
170+
}
171+
}

0 commit comments

Comments
 (0)