Method EnsureDecl

analysis/validation.go:217–276

EnsureDecl ensures that every predicate in the program is declared. It also ensures consistency of temporal usage.

(clauses []ast.Clause)

// EnsureDecl ensures that every predicate in the program is declared.
// It also ensures consistency of temporal usage.
func (a *Analyzer) EnsureDecl(clauses []ast.Clause) error {
	extraByName := byName(a.extraPredicates)
	declByName := byName(a.decl)
	for _, c := range clauses {
		pred := c.Head.Predicate
		name := pred.Symbol
		// Check that the name was not defined previously (in a separate source).
		// We may permit "distributing" definitions over source files later.
		if decl, ok := a.extraPredicates[pred]; ok {
			if decl.IsExtensional() && len(c.Premises) == 0 {
				continue
			}
			return fmt.Errorf("predicate %v was defined previously %v", decl.DeclaredAtom.Predicate, decl)
		}
		if decl, ok := extraByName[name]; ok { // different arity
			return fmt.Errorf(
				"predicate %v was defined previously", decl.DeclaredAtom.Predicate)
		}

		// If we already have a declaration, check if it is compatible.
		// Note that we may have multiple declarations for the same predicate
		// (e.g. one from use and one from package).
		if decl, ok := a.decl[pred]; ok {
			// If we have an existing declaration, check for temporal consistency
			if c.HeadTime != nil && !c.HeadTime.IsEternal() {
				if !decl.IsTemporal() && !decl.IsMaybeTemporal() {
					return fmt.Errorf("predicate %v is not declared temporal but used with temporal annotation in %v", pred, c)
				}
			}
			continue
		}
		// Check that the name was not defined in the same source with a different arity.
		if decl, ok := declByName[name]; ok {
			return fmt.Errorf("%v does not match arity of %v", c.Head, decl.DeclaredAtom)
		}

		var (
			synthDecl ast.Decl
			err       error
		)
		if c.Premises != nil {
			synthDecl, err = ast.NewSyntheticDecl(c.Head) // preserve variable names.
		} else {
			synthDecl = ast.NewSyntheticDeclFromSym(pred)
		}
		if err != nil {
			return err
		}

		// If this is a synthetic declaration and we have a temporal annotation,
		// mark it as "MaybeTemporal" so we can check consistency later.
		if c.HeadTime != nil && !c.HeadTime.IsEternal() {
			synthDecl.Descr = append(synthDecl.Descr, ast.NewAtom(ast.DescrMaybeTemporal))
		}

		a.decl[pred] = synthDecl
		declByName[pred.Symbol] = a.decl[pred]
	}