From 1f53fd85b41bcea043bf28739db781695b3f32a5 Mon Sep 17 00:00:00 2001 From: James Shubin Date: Tue, 22 Aug 2023 15:43:20 -0400 Subject: [PATCH] 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. --- lang/unification/simplesolver.go | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/lang/unification/simplesolver.go b/lang/unification/simplesolver.go index 5893a54d..ad18c71b 100644 --- a/lang/unification/simplesolver.go +++ b/lang/unification/simplesolver.go @@ -742,8 +742,8 @@ Loop: if !eqContains(newEq, eqInvariants) { logf("%s: new equality: %p %+v <-> %p %+v", Name, newEq.Expr1, newEq.Expr1, newEq.Expr2, newEq.Expr2) eqInvariants = append(eqInvariants, newEq) - // TODO: add to main invariant list too? - // TODO: add it as a generator or to the equalities array directly? + // TODO: add it as a generator instead? + equalities = append(equalities, newEq) } // both solved or both unsolved we skip @@ -805,8 +805,8 @@ Loop: if !eqContains(newEq, eqInvariants) { logf("%s: new equality: %p %+v <-> %p %+v", Name, newEq.Expr1, newEq.Expr1, newEq.Expr2, newEq.Expr2) eqInvariants = append(eqInvariants, newEq) - // TODO: add to main invariant list too? - // TODO: add it as a generator or to the equalities array directly? + // TODO: add it as a generator instead? + equalities = append(equalities, newEq) } // both solved or both unsolved we skip