Skip to content

Commit 024f6a1

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

File tree

2 files changed

+122
-148
lines changed

2 files changed

+122
-148
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: 105 additions & 148 deletions
Original file line numberDiff line numberDiff line change
@@ -456,65 +456,46 @@ set_option linter.unusedVariables false
456456
}
457457

458458
/// Render generics, adding a space after each parameter
459-
fn generics(
460-
&self,
461-
Generics {
462-
params,
463-
constraints,
464-
}: &Generics,
465-
) -> DocBuilder<A> {
459+
fn generics(&self, generics: &Generics) -> DocBuilder<A> {
466460
docs![
467-
zip_right!(params, line!()),
461+
zip_right!(&generics.params, line!()),
468462
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),
463+
generics.type_constraints().map(|impl_ident| {
464+
let projections = generics.projection_constraints()
465+
.map(|p|
466+
if let ImplExprKind::LocalBound { id } = &*p.impl_.kind && *id == impl_ident.name {
467+
docs![p]
468+
} else {
469+
emit_error!(issue 1710, "Unsupported variant of associated type projection")
470+
}
471+
)
472+
.collect::<Vec<_>>();
473+
docs![
474+
docs![
475+
impl_ident.goal.trait_,
476+
".AssociatedTypes",
477+
concat!(
478+
impl_ident.goal.args.iter().map(|arg| docs![line!(), arg])
479+
)
480+
]
481+
.brackets()
482+
.group()
483+
.nest(INDENT),
484+
line!(),
485+
docs![
486+
impl_ident.goal.trait_,
487+
concat!(
488+
impl_ident.goal.args.iter().map(|arg| docs![line!(), arg])
489+
),
499490
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()
491+
self.associated_type_projections(impl_ident, projections)
511492
]
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-
}),
493+
.brackets()
494+
.nest(INDENT)
495+
.group()
496+
]
497+
.group()
498+
}),
518499
line!()
519500
),
520501
]
@@ -1097,17 +1078,10 @@ set_option linter.unusedVariables false
10971078
generics,
10981079
items,
10991080
} => {
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<_>>();
1081+
let generic_types = generics.type_constraints().collect::<Vec<_>>();
1082+
if generic_types.len() < generics.constraints.len() {
1083+
emit_error!(issue 1710, "Unsupported equality constraints on associated types")
1084+
}
11111085
docs![
11121086
// A trait is encoded as two Lean type classes: one holding the associated types,
11131087
// and one holding all other fields.
@@ -1121,75 +1095,66 @@ set_option linter.unusedVariables false
11211095
]),
11221096
softline!(),
11231097
"where"
1124-
].group(),
1098+
]
1099+
.group(),
11251100
zip_left!(
11261101
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-
)
1142-
)
1102+
generic_types.iter().map(|impl_ident| docs![
1103+
self.fresh_constraint_name(&self.render_last(name), impl_ident),
1104+
" :",
1105+
line!(),
1106+
&impl_ident.goal.trait_,
1107+
".AssociatedTypes",
1108+
line!(),
1109+
intersperse!(&impl_ident.goal.args, line!())
1110+
]
1111+
.group()
1112+
.brackets())
11431113
),
11441114
zip_left!(
11451115
hardline!(),
1146-
items.iter().filter(|item| {
1147-
matches!(item.kind, TraitItemKind::Type(_))
1148-
})
1116+
items
1117+
.iter()
1118+
.filter(|item| { matches!(item.kind, TraitItemKind::Type(_)) })
11491119
),
11501120
]
11511121
.nest(INDENT),
11521122
// We add the `[instance]` attribute to the contained constraints to make
11531123
// them available for type inference:
11541124
zip_left!(
11551125
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-
)
1169-
)
1126+
generic_types.iter().map(|impl_ident| docs![
1127+
"attribute [instance]",
1128+
line!(),
1129+
name,
1130+
".AssociatedTypes.",
1131+
self.fresh_constraint_name(&self.render_last(name), impl_ident),
1132+
]
1133+
.group()
1134+
.nest(INDENT))
11701135
),
11711136
// When referencing associated types, we would like to refer to them as
11721137
// `TraitName.TypeName` instead of `TraitName.AssociatedTypes.TypeName`:
11731138
zip_left!(
11741139
docs![hardline!(), hardline!()],
1175-
items.iter()
1176-
.filter(|item| {
1177-
matches!(item.kind, TraitItemKind::Type(_))
1178-
})
1179-
.map(|item| {
1180-
docs![
1181-
"abbrev ",
1182-
name,
1183-
".",
1184-
self.render_last(&item.ident),
1185-
" :=",
1186-
line!(),
1187-
name, ".AssociatedTypes",
1188-
".",
1189-
self.render_last(&item.ident),
1190-
]
1191-
.nest(INDENT)
1192-
})
1140+
items
1141+
.iter()
1142+
.filter(|item| { matches!(item.kind, TraitItemKind::Type(_)) })
1143+
.map(|item| {
1144+
docs![
1145+
"abbrev ",
1146+
name,
1147+
".",
1148+
self.render_last(&item.ident),
1149+
" :=",
1150+
line!(),
1151+
name,
1152+
".AssociatedTypes",
1153+
".",
1154+
self.render_last(&item.ident),
1155+
]
1156+
.nest(INDENT)
1157+
})
11931158
),
11941159
hardline!(),
11951160
hardline!(),
@@ -1210,7 +1175,8 @@ set_option linter.unusedVariables false
12101175
"outParam",
12111176
softline!(),
12121177
docs![
1213-
name, ".AssociatedTypes",
1178+
name,
1179+
".AssociatedTypes",
12141180
softline!(),
12151181
intersperse!(&generics.params, softline!()),
12161182
]
@@ -1225,25 +1191,22 @@ set_option linter.unusedVariables false
12251191
"where"
12261192
]
12271193
.group(),
1228-
// Lean's `extends` does not work for us because one cannot implement
1194+
// Lean's `extends` does not work for us because one cannot implement
12291195
// different functions of the same name on the super- and on the
12301196
// subclass. So we treat supertraits like any other constraint:
12311197
zip_left!(
12321198
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()
1199+
generic_types.iter().map(|impl_ident| docs![
1200+
self.fresh_constraint_name(&self.render_last(name), impl_ident),
1201+
" :",
1202+
line!(),
1203+
impl_ident.goal.trait_,
1204+
concat!(
1205+
impl_ident.goal.args.iter().map(|arg| docs![line!(), arg])
12451206
)
1246-
)
1207+
]
1208+
.group()
1209+
.brackets())
12471210
),
12481211
zip_left!(
12491212
hardline!(),
@@ -1261,21 +1224,15 @@ set_option linter.unusedVariables false
12611224
// them available for type inference:
12621225
zip_left!(
12631226
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-
)
1278-
)
1227+
generic_types.iter().map(|impl_ident| docs![
1228+
"attribute [instance]",
1229+
line!(),
1230+
name,
1231+
".",
1232+
self.fresh_constraint_name(&self.render_last(name), impl_ident),
1233+
]
1234+
.group()
1235+
.nest(INDENT))
12791236
),
12801237
]
12811238
}

0 commit comments

Comments
 (0)