Method feasibleAlternatives

analysis/validation.go:1107–1286

feasibleAlternatives returns feasible alternatives for a subgoal p(e1...eN). We consider a relation type expression (from decl), the given list of arguments, the type assignments to variable symbols, and a type context that collects type variables with associated type constrains. Returns list of alt

(
	pred ast.PredicateSym, relTypeExpr ast.BaseTerm, args []ast.BaseTerm,
	varRanges map[ast.Variable]ast.BaseTerm,
	typeCtx map[ast.Variable]ast.BaseTerm)

// that collects type variables with associated type constrains.
// Returns list of alternatives and list of type contexts with new type constraints.
func (bc *BoundsAnalyzer) feasibleAlternatives(
	pred ast.PredicateSym, relTypeExpr ast.BaseTerm, args []ast.BaseTerm,
	varRanges map[ast.Variable]ast.BaseTerm,
	typeCtx map[ast.Variable]ast.BaseTerm) ([]ast.BaseTerm, []map[ast.Variable]ast.BaseTerm, error) {
	if pred.Symbol == symbols.ListMember.Symbol {
		tpe := boundOfArg(args[1], varRanges, bc.nameTrie)
		if tpe == ast.AnyBound {
			return []ast.BaseTerm{symbols.NewRelType(ast.AnyBound, symbols.NewListType(ast.AnyBound))}, nil, nil
		}
		if symbols.IsListTypeExpression(tpe) {
			elemTpe, err := symbols.ListTypeArg(tpe)
			if err != nil {
				return nil, nil, err
			}
			var bound ast.BaseTerm
			if v, ok := args[0].(ast.Variable); ok {
				if _, ok := varRanges[v]; ok {
					bound = varRanges[v]
				} else {
					bound = elemTpe // a new variable binding
				}
			} else {
				bound = boundOfArg(args[0], varRanges, bc.nameTrie)
			}
			// TODO: typing context must give lower bounds as well.
			meet := symbols.LowerBound(typeCtx, []ast.BaseTerm{bound, elemTpe})
			if !meet.Equals(symbols.EmptyType) {
				return []ast.BaseTerm{symbols.NewRelType(meet, tpe)}, []map[ast.Variable]ast.BaseTerm{typeCtx}, nil
			}
			return nil, nil, fmt.Errorf("pred %v on args %v cannot succeed var ranges %v", pred, args, varRanges)
		}
	}
	if pred.Symbol == symbols.MatchPrefix.Symbol {
		tpe := boundOfArg(args[0], varRanges, bc.nameTrie)
		prefix := args[1]
		meet := symbols.LowerBound(nil /*TODO*/, []ast.BaseTerm{tpe, prefix})
		if !meet.Equals(symbols.EmptyType) {
			return []ast.BaseTerm{symbols.NewRelType(meet, ast.NameBound)}, []map[ast.Variable]ast.BaseTerm{typeCtx}, nil
		}
		return nil, nil, fmt.Errorf("pred %v cannot succeed: type %v is incompatible with %v", pred, tpe, prefix)
	}

	if pred.Symbol == symbols.MatchEntry.Symbol {
		tpe := boundOfArg(args[0], varRanges, bc.nameTrie)
		if symbols.IsMapTypeExpression(tpe) {
			keyType, valTpe, err := symbols.MapTypeArgs(tpe)
			if err != nil {
				return nil, nil, err
			}
			var bound ast.BaseTerm
			if v, ok := args[1].(ast.Variable); ok {
				if _, ok := varRanges[v]; ok {
					bound = varRanges[v]
				} else {
					bound = tpe // a new variable binding
				}
			} else {
				bound = boundOfArg(args[1], varRanges, bc.nameTrie)