Method checkClauses

analysis/validation.go:1063–1100

checkRelTypes takes a pred that has a declaration supplied by the user. It checks every clause, including unit clauses ("initial facts").

(decl *ast.Decl)

// checkRelTypes takes a pred that has a declaration supplied by the user.
// It checks every clause, including unit clauses ("initial facts").
func (bc *BoundsAnalyzer) checkClauses(decl *ast.Decl) error {
	pred := decl.DeclaredAtom.Predicate
	clauses := bc.RulesMap[pred]

	declaredRelTypeExpr, err := symbols.RelTypeExprFromDecl(*decl)
	if err != nil {
		return err
	}

	// Handle unit clauses (initial facts). We inferred some relation types, each must
	// conform to the declaration (at least one alternative among declared ones).
	if initialFactRelTypes, ok := bc.initialFactMap[pred]; ok {
		for _, inferred := range symbols.RelTypeAlternatives(initialFactRelTypes) {
			typeCtx := symbols.GetTypeContext(declaredRelTypeExpr)
			if !symbols.SetConforms(typeCtx, inferred, declaredRelTypeExpr) {
				return fmt.Errorf("found unit clause with %v that does not conform to any decl %v", inferred, declaredRelTypeExpr)
			}
		}
	}

	for _, clause := range clauses {
		ic := newInferContext(bc, decl, &clause)
		inferredRelTypeExpr, err := ic.inferRelTypesFromClause()
		if err != nil {
			return err
		}
		typeCtx := symbols.GetTypeContext(declaredRelTypeExpr)
		if !symbols.SetConforms(typeCtx, inferredRelTypeExpr, declaredRelTypeExpr) {
			var rules strings.Builder
			for _, r := range bc.RulesMap[pred] {
				rules.WriteString(r.String() + "\n")
			}
			return fmt.Errorf("type mismatch for pred %v rule: %s \n inferred: %v\nvs declared %v",
				decl.DeclaredAtom, clause, inferredRelTypeExpr, declaredRelTypeExpr)
		}
	}
	return nil
}

// feasibleAlternatives returns feasible alternatives for a subgoal p(e1...eN).
// We consider a relation type expression (from decl), the given list of