From 33366469a3aff8aaf037371ccdbd2395e00b597c Mon Sep 17 00:00:00 2001 From: James Shubin Date: Sun, 20 Aug 2023 20:50:41 -0400 Subject: [PATCH] lang: unification: Add partial func knowledge to solved This performs the same task as the previous two commits, but it also adds partial information when solving a func. --- lang/unification/simplesolver.go | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/lang/unification/simplesolver.go b/lang/unification/simplesolver.go index a80827f4..79b31b5e 100644 --- a/lang/unification/simplesolver.go +++ b/lang/unification/simplesolver.go @@ -621,6 +621,16 @@ Loop: t, exists := funcPartials[eq.Expr1][y] if !exists { funcPartials[eq.Expr1][y] = typ // learn! + + // Even though this is only a partial learn, we should still add it to the solved information! + if newTyp, exists := solved[y]; !exists { + solved[y] = typ // yay, we learned something! + //used = append(used, i) // mark equality as used up when complete! + logf("%s: solved partial func arg equality", Name) + } else if err := newTyp.Cmp(typ); err != nil { + return nil, errwrap.Wrapf(err, "can't unify, invariant illogicality with partial func arg equality") + } + continue } if err := t.Cmp(typ); err != nil { @@ -635,6 +645,16 @@ Loop: t, exists := funcPartials[eq.Expr1][y] if !exists { funcPartials[eq.Expr1][y] = typ // learn! + + // Even though this is only a partial learn, we should still add it to the solved information! + if newTyp, exists := solved[y]; !exists { + solved[y] = typ // yay, we learned something! + //used = append(used, i) // mark equality as used up when complete! + logf("%s: solved partial func return equality", Name) + } else if err := newTyp.Cmp(typ); err != nil { + return nil, errwrap.Wrapf(err, "can't unify, invariant illogicality with partial func return equality") + } + continue } if err := t.Cmp(typ); err != nil {