Method inferRelTypes

analysis/validation.go:1353–1381

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.

(pred ast.PredicateSym)

// 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.
func (bc *BoundsAnalyzer) inferRelTypes(pred ast.PredicateSym) (ast.BaseTerm, error) {
	if existing, ok := bc.relTypeMap[pred]; ok {
		return existing, nil
	}
	if existing, ok := bc.inferred[pred]; ok {
		return existing, nil
	}

	var alternatives []ast.BaseTerm
	if initialFactRelTypeExpr, ok := bc.initialFactMap[pred]; ok {
		alternatives = symbols.RelTypeAlternatives(initialFactRelTypeExpr)
	}

	clauses := bc.RulesMap[pred]
	for _, clause := range clauses {
		ic := newInferContextNoDecl(bc, &pred, &clause)
		relType, err := ic.inferRelTypesFromClause()
		if err != nil {
			return nil, err
		}
		for _, alternative := range symbols.RelTypeAlternatives(relType) {
			if !symbols.SetConforms(nil /*TODO*/, alternative, symbols.RelTypeFromAlternatives(alternatives)) {
				alternatives = append(alternatives, alternative)
			}
		}
	}
	bc.inferred[pred] = symbols.RelTypeFromAlternatives(alternatives)
	return bc.inferred[pred], nil
}

func checkFunApply(z ast.ApplyFn, fnTpe ast.BaseTerm, varRanges map[ast.Variable]ast.BaseTerm, nameTrie symbols.NameTrie) (ast.BaseTerm, error) {
	if fnTpe.Equals(symbols.EmptyType) {