don't include unhelpful sequents

This commit is contained in:
Douglas Creager 2025-11-14 10:18:00 -05:00
parent cd87da208f
commit fec701e92d

View file

@ -1922,8 +1922,10 @@ impl<'db> SequentMap<'db> {
// if they're related to each other. // if they're related to each other.
let processed = std::mem::take(&mut self.processed); let processed = std::mem::take(&mut self.processed);
for other in &processed { for other in &processed {
if constraint != *other {
self.add_sequents_for_pair(db, constraint, *other); self.add_sequents_for_pair(db, constraint, *other);
} }
}
self.processed = processed; self.processed = processed;
// And see if we can create any sequents from the constraint on its own. // And see if we can create any sequents from the constraint on its own.
@ -1959,6 +1961,9 @@ impl<'db> SequentMap<'db> {
ante2: ConstrainedTypeVar<'db>, ante2: ConstrainedTypeVar<'db>,
post: ConstrainedTypeVar<'db>, post: ConstrainedTypeVar<'db>,
) { ) {
if ante1 == post || ante2 == post {
return;
}
self.pair_implications self.pair_implications
.entry(Self::pair_key(db, ante1, ante2)) .entry(Self::pair_key(db, ante1, ante2))
.or_default() .or_default()
@ -1970,6 +1975,9 @@ impl<'db> SequentMap<'db> {
ante: ConstrainedTypeVar<'db>, ante: ConstrainedTypeVar<'db>,
post: ConstrainedTypeVar<'db>, post: ConstrainedTypeVar<'db>,
) { ) {
if ante == post {
return;
}
self.single_implications.entry(ante).or_default().push(post); self.single_implications.entry(ante).or_default().push(post);
} }