distributed union/intersection

This commit is contained in:
Douglas Creager 2025-08-05 14:45:57 -04:00
parent 8235062718
commit 6f957475ef
1 changed files with 20 additions and 4 deletions

View File

@ -155,7 +155,7 @@ impl<'db> ConstraintSetSet<'db> {
result result
} }
/// union two sets of constraint sets. /// Union two sets of constraint sets.
/// ///
/// This is the ⊔ operator from [[POPL2015][]], Definition 3.5. /// This is the ⊔ operator from [[POPL2015][]], Definition 3.5.
/// ///
@ -165,6 +165,21 @@ impl<'db> ConstraintSetSet<'db> {
self.add(db, set); self.add(db, set);
} }
} }
/// Calculate the distributed intersection of an iterator of sets of constraint sets.
fn distributed_intersection(db: &'db dyn Db, sets: impl IntoIterator<Item = Self>) -> Self {
sets.into_iter()
.fold(Self::always(), |sets, element| element.intersect(db, &sets))
}
/// Calculate the distributed union of an iterator of sets of constraint sets.
fn distributed_union(db: &'db dyn Db, sets: impl IntoIterator<Item = Self>) -> Self {
let mut result = Self::never();
for set in sets {
result.union(db, set);
}
result
}
} }
impl<'db> From<Constraint<'db>> for ConstraintSetSet<'db> { impl<'db> From<Constraint<'db>> for ConstraintSetSet<'db> {
@ -225,9 +240,10 @@ fn normalized_constraints_from_type_inner<'db>(
Type::Union(union) => { Type::Union(union) => {
// Figure 3, step 6 // Figure 3, step 6
// A union is a subtype of Never only if every element is. // A union is a subtype of Never only if every element is.
(union.iter(db)).fold(ConstraintSetSet::always(), |sets, element| { ConstraintSetSet::distributed_union(
normalized_constraints_from_type(db, *element).intersect(db, &sets) db,
}) (union.iter(db)).map(|element| normalized_constraints_from_type(db, *element)),
)
} }
Type::Intersection(intersection) => { Type::Intersection(intersection) => {