lang: unification: Add new eq to main list

We want to add the equality to the main list of equalities in case it is
needed somewhere else. This doesn't have any effect on any of our test
cases, but it doesn't seem to be harmful, and it could conceivably be
useful in the future. This is a separate commit in case we want to check
if this behaviour still holds true well into the future.
This commit is contained in:
James Shubin
2023-08-22 15:43:20 -04:00
parent 564c93ee21
commit 1f53fd85b4

View File

@@ -742,8 +742,8 @@ Loop:
if !eqContains(newEq, eqInvariants) { if !eqContains(newEq, eqInvariants) {
logf("%s: new equality: %p %+v <-> %p %+v", Name, newEq.Expr1, newEq.Expr1, newEq.Expr2, newEq.Expr2) logf("%s: new equality: %p %+v <-> %p %+v", Name, newEq.Expr1, newEq.Expr1, newEq.Expr2, newEq.Expr2)
eqInvariants = append(eqInvariants, newEq) eqInvariants = append(eqInvariants, newEq)
// TODO: add to main invariant list too? // TODO: add it as a generator instead?
// TODO: add it as a generator or to the equalities array directly? equalities = append(equalities, newEq)
} }
// both solved or both unsolved we skip // both solved or both unsolved we skip
@@ -805,8 +805,8 @@ Loop:
if !eqContains(newEq, eqInvariants) { if !eqContains(newEq, eqInvariants) {
logf("%s: new equality: %p %+v <-> %p %+v", Name, newEq.Expr1, newEq.Expr1, newEq.Expr2, newEq.Expr2) logf("%s: new equality: %p %+v <-> %p %+v", Name, newEq.Expr1, newEq.Expr1, newEq.Expr2, newEq.Expr2)
eqInvariants = append(eqInvariants, newEq) eqInvariants = append(eqInvariants, newEq)
// TODO: add to main invariant list too? // TODO: add it as a generator instead?
// TODO: add it as a generator or to the equalities array directly? equalities = append(equalities, newEq)
} }
// both solved or both unsolved we skip // both solved or both unsolved we skip