Method getOrInferRelTypes

analysis/validation.go:1313–1349

While checking a rule, we want to look up possible relation types. If we find several applicable ones, we return the feasible ones.

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

// While checking a rule, we want to look up possible relation types.
// If we find several applicable ones, we return the feasible ones.
func (bc *BoundsAnalyzer) getOrInferRelTypes(
	pred ast.PredicateSym,
	args []ast.BaseTerm,
	varRanges map[ast.Variable]ast.BaseTerm,
	typeCtx map[ast.Variable]ast.BaseTerm) ([]ast.BaseTerm, error) {

	if relType, ok := bc.relTypeMap[pred]; ok {
		tpe, _, err := bc.feasibleAlternatives(pred, relType, args, varRanges, typeCtx)
		return tpe, err
	}

	if relType, ok := bc.inferred[pred]; ok {
		tpe, _, err := bc.feasibleAlternatives(pred, relType, args, varRanges, typeCtx)
		return tpe, err
	}

	if bc.visiting[pred] {
		// We are asking for pred in a recursive call. Use [any ... any]
		relType, err := symbols.RelTypeExprFromDecl(*bc.programInfo.Decls[pred])
		if err != nil {
			return nil, err
		}
		return []ast.BaseTerm{relType}, nil
	}

	bc.visiting[pred] = true
	defer delete(bc.visiting, pred)

	relTypeExpr, err := bc.inferRelTypes(pred)
	if err != nil {
		return nil, err
	}
	bc.inferred[pred] = relTypeExpr
	tpe, _, err := bc.feasibleAlternatives(pred, relTypeExpr, args, varRanges, nil /*TODO map[ast.Variable]bool*/)
	return tpe, err

}

// inferRelType infers a relation type from rules when no decl is available.
// inferRelType ensures that bc.inferred[pred] is populated with the inferred relation type.