Skip to content

Commit a195845

Browse files
abentkampabentkamp
committed
refactor(lean): helper functions on AST element Generic 
1 parent f9b6cfd commit a195845

File tree

2 files changed

+99
-118
lines changed

2 files changed

+99
-118
lines changed

‎rust-engine/src/ast.rs‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1452,6 +1452,23 @@ pub struct Module {
14521452
pub meta: Metadata,
14531453
}
14541454

1455+
impl Generics {
1456+
/// Returns Iterator over all type constraints (`GenericConstraint::Type`)
1457+
pub fn type_constraints(&self) -> impl Iterator<Item = &ImplIdent> {
1458+
self.constraints.iter().filter_map(|c| match c {
1459+
GenericConstraint::Type(impl_id) => Some(impl_id),
1460+
_ => None,
1461+
})
1462+
}
1463+
/// Returns Iterator over all projection constraints (`GenericConstraint::Projection`)
1464+
pub fn projection_constraints(&self) -> impl Iterator<Item = &ProjectionPredicate> {
1465+
self.constraints.iter().filter_map(|c| match c {
1466+
GenericConstraint::Projection(pp) => Some(pp),
1467+
_ => None,
1468+
})
1469+
}
1470+
}
1471+
14551472
/// Traits for utilities on AST data types
14561473
pub mod traits {
14571474
use super::*;

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

Lines changed: 82 additions & 118 deletions
Original file line numberDiff line numberDiff line change
@@ -458,63 +458,47 @@ set_option linter.unusedVariables false
458458
/// Render generics, adding a space after each parameter
459459
fn generics(
460460
&self,
461-
Generics {
462-
params,
463-
constraints,
464-
}: &Generics,
461+
generics: &Generics
465462
) -> DocBuilder<A> {
466463
docs![
467-
zip_right!(params, line!()),
464+
zip_right!(&generics.params, line!()),
468465
zip_right!(
469-
constraints
470-
.iter()
471-
.map(|generic_constraint|
472-
match generic_constraint {
473-
GenericConstraint::Type(impl_ident) => {
474-
let projections = constraints
475-
.iter()
476-
.filter_map(|c|
477-
if let GenericConstraint::Projection(p) = c {
478-
if let ImplExprKind::LocalBound { id } = &*p.impl_.kind && *id == impl_ident.name {
479-
Some(docs![p])
480-
} else {
481-
Some((|| emit_error!(issue 1710, "Unsupported variant of associated type projection"))())
482-
}
483-
} else {
484-
None
485-
}
486-
)
487-
.collect::<Vec<_>>();
488-
docs![
489-
docs![
490-
impl_ident.goal.trait_,
491-
".AssociatedTypes",
492-
concat!(
493-
impl_ident.goal.args.iter().map(|arg| docs![line!(), arg])
494-
)
495-
]
496-
.brackets()
497-
.group()
498-
.nest(INDENT),
466+
generics.type_constraints().map(|impl_ident| {
467+
let projections = generics.projection_constraints()
468+
.map(|p|
469+
if let ImplExprKind::LocalBound { id } = &*p.impl_.kind && *id == impl_ident.name {
470+
docs![p]
471+
} else {
472+
emit_error!(issue 1710, "Unsupported variant of associated type projection")
473+
}
474+
)
475+
.collect::<Vec<_>>();
476+
docs![
477+
docs![
478+
impl_ident.goal.trait_,
479+
".AssociatedTypes",
480+
concat!(
481+
impl_ident.goal.args.iter().map(|arg| docs![line!(), arg])
482+
)
483+
]
484+
.brackets()
485+
.group()
486+
.nest(INDENT),
487+
line!(),
488+
docs![
489+
impl_ident.goal.trait_,
490+
concat!(
491+
impl_ident.goal.args.iter().map(|arg| docs![line!(), arg])
492+
),
499493
line!(),
500-
docs![
501-
impl_ident.goal.trait_,
502-
concat!(
503-
impl_ident.goal.args.iter().map(|arg| docs![line!(), arg])
504-
),
505-
line!(),
506-
self.associated_type_projections(impl_ident, projections)
507-
]
508-
.brackets()
509-
.nest(INDENT)
510-
.group()
494+
self.associated_type_projections(impl_ident, projections)
511495
]
512-
.group()}
513-
// Projections are rendered via `self.associated_type_projections` above.
514-
GenericConstraint::Projection(_) => docs![None],
515-
GenericConstraint::Lifetime(_) =>
516-
unreachable_by_invariant!(Drop_references),
517-
}),
496+
.brackets()
497+
.nest(INDENT)
498+
.group()
499+
]
500+
.group()
501+
}),
518502
line!()
519503
),
520504
]
@@ -1097,17 +1081,10 @@ set_option linter.unusedVariables false
10971081
generics,
10981082
items,
10991083
} => {
1100-
let generic_types = generics
1101-
.constraints
1102-
.iter()
1103-
.map(|constraint| match constraint {
1104-
GenericConstraint::Type(tc_constraint) => Some(tc_constraint),
1105-
GenericConstraint::Lifetime(_) => {
1106-
unreachable_by_invariant!(Drop_references)
1107-
}
1108-
GenericConstraint::Projection(_) => None,
1109-
})
1110-
.collect::<Vec<_>>();
1084+
let generic_types = generics.type_constraints().collect::<Vec<_>>();
1085+
if generic_types.len() < generics.constraints.len() {
1086+
emit_error!(issue 1710, "Unsupported equality constraints on associated types")
1087+
}
11111088
docs![
11121089
// A trait is encoded as two Lean type classes: one holding the associated types,
11131090
// and one holding all other fields.
@@ -1124,21 +1101,18 @@ set_option linter.unusedVariables false
11241101
].group(),
11251102
zip_left!(
11261103
hardline!(),
1127-
generic_types.iter().map(|maybe_impl_ident|
1128-
maybe_impl_ident.map_or_else(
1129-
|| emit_error!(issue 1710, "Unsupported equality constraints on associated types"),
1130-
|impl_ident| docs![
1131-
self.fresh_constraint_name(&self.render_last(name), impl_ident),
1132-
" :",
1133-
line!(),
1134-
&impl_ident.goal.trait_,
1135-
".AssociatedTypes",
1136-
line!(),
1137-
intersperse!(&impl_ident.goal.args, line!())
1138-
]
1139-
.group()
1140-
.brackets()
1141-
)
1104+
generic_types.iter().map(|impl_ident|
1105+
docs![
1106+
self.fresh_constraint_name(&self.render_last(name), impl_ident),
1107+
" :",
1108+
line!(),
1109+
&impl_ident.goal.trait_,
1110+
".AssociatedTypes",
1111+
line!(),
1112+
intersperse!(&impl_ident.goal.args, line!())
1113+
]
1114+
.group()
1115+
.brackets()
11421116
)
11431117
),
11441118
zip_left!(
@@ -1153,19 +1127,16 @@ set_option linter.unusedVariables false
11531127
// them available for type inference:
11541128
zip_left!(
11551129
docs![hardline!(), hardline!()],
1156-
generic_types.iter().map(|maybe_impl_ident|
1157-
maybe_impl_ident.map_or_else(
1158-
|| emit_error!(issue 1710, "Unsupported equality constraints on associated types"),
1159-
|impl_ident| docs![
1160-
"attribute [instance]",
1161-
line!(),
1162-
name,
1163-
".AssociatedTypes.",
1164-
self.fresh_constraint_name(&self.render_last(name), impl_ident),
1165-
]
1166-
.group()
1167-
.nest(INDENT)
1168-
)
1130+
generic_types.iter().map(|impl_ident|
1131+
docs![
1132+
"attribute [instance]",
1133+
line!(),
1134+
name,
1135+
".AssociatedTypes.",
1136+
self.fresh_constraint_name(&self.render_last(name), impl_ident),
1137+
]
1138+
.group()
1139+
.nest(INDENT)
11691140
)
11701141
),
11711142
// When referencing associated types, we would like to refer to them as
@@ -1230,19 +1201,16 @@ set_option linter.unusedVariables false
12301201
// subclass. So we treat supertraits like any other constraint:
12311202
zip_left!(
12321203
hardline!(),
1233-
generic_types.iter().map(|maybe_impl_ident|
1234-
maybe_impl_ident.map_or_else(
1235-
|| emit_error!(issue 1710, "Unsupported equality constraints on associated types"),
1236-
|impl_ident| docs![
1237-
self.fresh_constraint_name(&self.render_last(name), impl_ident),
1238-
" :",
1239-
line!(),
1240-
impl_ident.goal.trait_,
1241-
concat!(impl_ident.goal.args.iter().map(|arg| docs![line!(), arg]))
1242-
]
1243-
.group()
1244-
.brackets()
1245-
)
1204+
generic_types.iter().map(
1205+
|impl_ident| docs![
1206+
self.fresh_constraint_name(&self.render_last(name), impl_ident),
1207+
" :",
1208+
line!(),
1209+
impl_ident.goal.trait_,
1210+
concat!(impl_ident.goal.args.iter().map(|arg| docs![line!(), arg]))
1211+
]
1212+
.group()
1213+
.brackets()
12461214
)
12471215
),
12481216
zip_left!(
@@ -1261,20 +1229,16 @@ set_option linter.unusedVariables false
12611229
// them available for type inference:
12621230
zip_left!(
12631231
docs![hardline!(), hardline!()],
1264-
generic_types.iter().map(|maybe_impl_ident|
1265-
maybe_impl_ident.map_or_else(
1266-
|| emit_error!(issue 1710, "Unsupported equality constraints on associated types"),
1267-
|impl_ident|
1268-
docs![
1269-
"attribute [instance]",
1270-
line!(),
1271-
name,
1272-
".",
1273-
self.fresh_constraint_name(&self.render_last(name), impl_ident),
1274-
]
1275-
.group()
1276-
.nest(INDENT)
1277-
)
1232+
generic_types.iter().map(|impl_ident|
1233+
docs![
1234+
"attribute [instance]",
1235+
line!(),
1236+
name,
1237+
".",
1238+
self.fresh_constraint_name(&self.render_last(name), impl_ident),
1239+
]
1240+
.group()
1241+
.nest(INDENT)
12781242
)
12791243
),
12801244
]

0 commit comments

Comments
 (0)