From 0f30f4724903af2e7aa9a5c8aa3b13b7311eb05c Mon Sep 17 00:00:00 2001 From: James Shubin Date: Sun, 23 May 2021 19:31:11 -0400 Subject: [PATCH] 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. --- lang/funcs/core/world/schedule_func.go | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/lang/funcs/core/world/schedule_func.go b/lang/funcs/core/world/schedule_func.go index 248855ae..c930dbf1 100644 --- a/lang/funcs/core/world/schedule_func.go +++ b/lang/funcs/core/world/schedule_func.go @@ -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.