lourenco/mgmt
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

lang: unification: Add equiv matching and resultant equalities

Browse Source 
The set of initial invariants that we see might include:

	?8 = func(inputs []int, function  ?4) ?3
	?8 = func(inputs []int, function ?10) ?9
	?8 = func arg0   []int, arg1      ?6) ?7

From this we can infer that since they are all equal, that we also know
that ?4, ?10 and ?6 must also be equal. The same is true of ?3, ?9 and
?10. Those new equalities are sometimes necessary in order to complete
the full unification.

The second interesting aspect is when we have dissimilar equalities:

	?2  = func(x  ?1) str
	?4  = func(a int) ?5
	?10 = func(a int) ?11

In this example we also have an additional equality:

	?6 = ?2

From this and the above we can determine that ?2, ?4, ?6 and ?10 are all
equal. We only know about ?4, ?6, and ?10 from the direct relationship,
and we add in ?2 from the indirect (graph) relationship. These
relationships let us determine new information that ?5 and ?11 are both
str and that ?1 is an int.

Two important reminders:

1) Arg names don't have to match. It would impossible to build such a
   system where this was both possible, but also let us name our
   functions sanely.

2) None of this guarantees we won't find an inconsistency in our
   solution. If this is found, it simply means that someone wrote code
   which does not type check.
This commit is contained in:
James Shubin
2023-08-22 15:05:34 -04:00
parent 0946e860f1
commit 6769786241
2 changed files with 154 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

90
lang/unification/simplesolver.go
View File

@@ -316,14 +316,37 @@ func SimpleInvariantSolver(invariants []interfaces.Invariant, expected []interfa
return unsolved, result
}
// list all the expr's connected to expr, use pairs as chains
listConnectedFn := func(expr interfaces.Expr, exprs []*interfaces.EqualityInvariant) []interfaces.Expr {
pairsType := pairs(exprs)
return pairsType.DFS(expr)
}
// does the equality invariant already exist in the set? order of expr1
// and expr2 doesn't matter
eqContains := func(eq *interfaces.EqualityInvariant, pairs []*interfaces.EqualityInvariant) bool {
for _, x := range pairs {
if eq.Expr1 == x.Expr1 && eq.Expr2 == x.Expr2 {
return true
}
if eq.Expr1 == x.Expr2 && eq.Expr2 == x.Expr1 { // reverse
return true
}
}
return false
}
// build a static list that won't get consumed
eqInvariants := []*interfaces.EqualityInvariant{}
fnInvariants := []*interfaces.EqualityWrapFuncInvariant{}
for _, x := range equalities {
eq, ok := x.(*interfaces.EqualityWrapFuncInvariant)
if !ok {
continue
if eq, ok := x.(*interfaces.EqualityInvariant); ok {
eqInvariants = append(eqInvariants, eq)
}
if eq, ok := x.(*interfaces.EqualityWrapFuncInvariant); ok {
fnInvariants = append(fnInvariants, eq)
}
fnInvariants = append(fnInvariants, eq)
}
logf("%s: starting loop with %d equalities", Name, len(equalities))
@@ -662,12 +685,39 @@ Loop:
}
}
equivs := listConnectedFn(eq.Expr1, eqInvariants) // or equivalent!
if debug && len(equivs) > 0 {
logf("%s: equiv %d: %p %+v", Name, len(equivs), eq.Expr1, eq.Expr1)
for i, x := range equivs {
logf("%s: equiv(%d): %p %+v", Name, i, x, x)
}
}
// This determines if a pointer is equivalent to
// a pointer we're interested to match against.
inEquiv := func(needle interfaces.Expr) bool {
for _, x := range equivs {
if x == needle {
return true
}
}
return false
}
// is there another EqualityWrapFuncInvariant with the same Expr1 pointer?
for _, fn := range fnInvariants {
if eq.Expr1 != fn.Expr1 {
// is this fn.Expr1 related by equivalency graph to eq.Expr1 ?
if (eq.Expr1 != fn.Expr1) && !inEquiv(fn.Expr1) {
if debug {
logf("%s: equiv skip: %p %+v", Name, fn.Expr1, fn.Expr1)
}
continue
}
// wow they match
if debug {
logf("%s: equiv used: %p %+v", Name, fn.Expr1, fn.Expr1)
}
//if eq.Expr1 != fn.Expr1 { // previously
// continue
//}
// wow they match or are equivalent
if len(eq.Expr2Ord) != len(fn.Expr2Ord) {
return nil, fmt.Errorf("func arg count differs")
@@ -681,6 +731,20 @@ Loop:
lhsTyp, lhsExists := solved[lhsExpr]
rhsTyp, rhsExists := solved[rhsExpr]
// add to eqInvariants if not already there!
// TODO: If this parent func invariant gets solved,
// will being unable to add this later be an issue?
newEq := &interfaces.EqualityInvariant{
Expr1: lhsExpr,
Expr2: rhsExpr,
}
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?
}
// both solved or both unsolved we skip
if lhsExists && !rhsExists { // teach rhs
typ, exists := funcPartials[eq.Expr1][rhsExpr]
@@ -730,6 +794,20 @@ Loop:
lhsTyp, lhsExists := solved[lhsExpr]
rhsTyp, rhsExists := solved[rhsExpr]
// add to eqInvariants if not already there!
// TODO: If this parent func invariant gets solved,
// will being unable to add this later be an issue?
newEq := &interfaces.EqualityInvariant{
Expr1: lhsExpr,
Expr2: rhsExpr,
}
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?
}
// both solved or both unsolved we skip
if lhsExists && !rhsExists { // teach rhs
typ, exists := funcPartials[eq.Expr1][rhsExpr]

70
lang/unification/util.go
View File

@@ -52,3 +52,73 @@ func UniqueExprList(exprList []interfaces.Expr) []interfaces.Expr {
exprMap := ExprListToExprMap(exprList)
return ExprMapToExprList(exprMap)
}
// ExprContains is an "in array" function to test for an expr in a slice of
// expressions.
func ExprContains(needle interfaces.Expr, haystack []interfaces.Expr) bool {
for _, v := range haystack {
if needle == v {
return true
}
}
return false
}
// pairs is a simple list of pairs of expressions which can be used as a simple
// undirected graph structure, or as a simple list of equalities.
type pairs []*interfaces.EqualityInvariant
// Vertices returns the list of vertices that the input expr is directly
// connected to.
func (obj pairs) Vertices(expr interfaces.Expr) []interfaces.Expr {
m := make(map[interfaces.Expr]struct{})
for _, x := range obj {
if x.Expr1 == x.Expr2 { // skip circular
continue
}
if x.Expr1 == expr {
m[x.Expr2] = struct{}{}
}
if x.Expr2 == expr {
m[x.Expr1] = struct{}{}
}
}
out := []interfaces.Expr{}
// FIXME: can we do this loop in a deterministic, sorted way?
for k := range m {
out = append(out, k)
}
return out
}
// DFS returns a depth first search for the graph, starting at the input vertex.
func (obj pairs) DFS(start interfaces.Expr) []interfaces.Expr {
var d []interfaces.Expr // discovered
var s []interfaces.Expr // stack
found := false
for _, x := range obj { // does the start exist?
if x.Expr1 == start || x.Expr2 == start {
found = true
break
}
}
if !found {
return nil // TODO: error
}
v := start
s = append(s, v)
for len(s) > 0 {
v, s = s[len(s)-1], s[:len(s)-1] // s.pop()
if !ExprContains(v, d) { // if not discovered
d = append(d, v) // label as discovered
for _, w := range obj.Vertices(v) {
s = append(s, w)
}
}
}
return d
}