CheckRule checks arity and that every variable appearing is bound. A variable is bound when: - it appears in a positive atom, or - is unified (via an equality) with a constant or bound variable. These form the basis for datalog safety (ensuring termination). We permit mode declaration that modify th
(clause ast.Clause)
| 515 | // - is unified (via an equality) with a constant or bound variable. |
| 516 | // Also checks that every function application expression has the right number of arguments. |
| 517 | func (a *Analyzer) CheckRule(clause ast.Clause) error { |
| 518 | clause = clause.ReplaceWildcards() |
| 519 | var ( |
| 520 | boundVars = make(map[ast.Variable]bool) |
| 521 | headVars = make(map[ast.Variable]bool) |
| 522 | seenVars = make(map[ast.Variable]bool) |
| 523 | ) |
| 524 | ast.AddVars(clause.Head, headVars) |
| 525 | ast.AddVars(clause.Head, seenVars) |
| 526 | // Check that if the head predicate is temporal, the clause has a temporal annotation. |
| 527 | if decl, ok := a.decl[clause.Head.Predicate]; ok { |
| 528 | if (decl.IsTemporal() || decl.IsMaybeTemporal()) && clause.HeadTime == nil { |
| 529 | return fmt.Errorf("temporal predicate %v defined without temporal annotation", clause.Head.Predicate) |
| 530 | } |
| 531 | } |
| 532 | |
| 533 | if clause.HeadTime != nil { |
| 534 | if clause.HeadTime.Start.Type == ast.VariableBound { |
| 535 | headVars[clause.HeadTime.Start.Variable] = true |
| 536 | seenVars[clause.HeadTime.Start.Variable] = true |
| 537 | } |
| 538 | if clause.HeadTime.End.Type == ast.VariableBound { |
| 539 | headVars[clause.HeadTime.End.Variable] = true |
| 540 | seenVars[clause.HeadTime.End.Variable] = true |
| 541 | } |
| 542 | } |
| 543 | uf := unionfind.New() |
| 544 | |
| 545 | if decl, ok := a.decl[clause.Head.Predicate]; ok { |
| 546 | |
| 547 | mode := unifyModes(decl.Modes()) |
| 548 | for _, v := range variablesForArgMode(clause.Head, mode, ast.ArgModeInput) { |
| 549 | boundVars[v] = true |
| 550 | } |
| 551 | } |
| 552 | |
| 553 | if clause.Premises != nil { |
| 554 | for _, premise := range clause.Premises { |
| 555 | ast.AddVars(premise, seenVars) |
| 556 | switch p := premise.(type) { |
| 557 | case ast.Atom: |
| 558 | if err := checkAtomArity(p); err != nil { |
| 559 | return err |
| 560 | } |
| 561 | // This is after rewriting, so we can assume that evaluation proceeds left-to-right, |
| 562 | // we only need to check that variables have been bound by some earlier subgoal. |
| 563 | if !p.Predicate.IsBuiltin() { |
| 564 | if decl, ok := a.decl[p.Predicate]; ok && len(decl.Modes()) > 0 { |
| 565 | for _, v := range variablesForArgMode(p, unifyModes(decl.Modes()), ast.ArgModeOutput|ast.ArgModeInputOutput) { |
| 566 | boundVars[v] = true |
| 567 | } |
| 568 | } else { |
| 569 | ast.AddVars(p, boundVars) |
| 570 | } |
| 571 | |
| 572 | // Validate that if the predicate is temporal, it is not used as a bare atom here. |
| 573 | if decl, ok := a.decl[p.Predicate]; ok { |
| 574 | if decl.IsTemporal() || decl.IsMaybeTemporal() { |