lang: funcs: core: world: Add unification to schedule return expr

This adds a sneaky unification between the expression of the function
return value in the unification. I am not entirely sure how often this
will get used, but it could be valuable in the right instance if this
isn't already learned through other sources. I'm fairly confident that
it isn't incorrect, so in the worst case scenario it's redundant
information for the unification solver.

This is being added as a separate commit so that it's obvious how this
type of unification invariant can be applied.
This commit is contained in:
James Shubin
2021-05-23 19:31:11 -04:00
parent 6b2ad8ebc8
commit 0f30f47249

View File

@@ -142,7 +142,7 @@ func (obj *SchedulePolyFunc) Unify(expr interfaces.Expr) ([]interfaces.Invariant
if cfavInvar.Func != expr {
continue
}
// cfavInvar.Expr is the ExprCall!
// cfavInvar.Expr is the ExprCall! (the return pointer)
// cfavInvar.Args are the args that ExprCall uses!
if len(cfavInvar.Args) == 0 {
return nil, fmt.Errorf("unable to build function with no args")
@@ -155,6 +155,13 @@ func (obj *SchedulePolyFunc) Unify(expr interfaces.Expr) ([]interfaces.Invariant
var invariants []interfaces.Invariant
var invar interfaces.Invariant
// add the relationship to the returned value
invar = &interfaces.EqualityInvariant{
Expr1: cfavInvar.Expr,
Expr2: dummyOut,
}
invariants = append(invariants, invar)
// add the relationships to the called args
invar = &interfaces.EqualityInvariant{
Expr1: cfavInvar.Args[0],
@@ -180,7 +187,7 @@ func (obj *SchedulePolyFunc) Unify(expr interfaces.Expr) ([]interfaces.Invariant
optsTypeKnown := false
// speculate about the type?
if typ, err := cfavInvar.Args[1].Type(); err == nil {
if typ, exists := solved[cfavInvar.Args[1]]; exists {
optsTypeKnown = true
if typ.Kind != types.KindStruct {
return nil, fmt.Errorf("second arg must be of kind struct")
@@ -234,6 +241,14 @@ func (obj *SchedulePolyFunc) Unify(expr interfaces.Expr) ([]interfaces.Invariant
}
invariants = append(invariants, invar)
}
// redundant?
if typ, err := cfavInvar.Args[1].Type(); err == nil {
invar := &interfaces.EqualsInvariant{
Expr: cfavInvar.Args[1],
Type: typ,
}
invariants = append(invariants, invar)
}
// If we're strict, require it, otherwise let
// in whatever, and let Build() deal with it.