pub enum ProgramValidationError {
UnsafeRule {
rule_index: usize,
variables: Vec<VariableSymbol>,
},
UnsafeNegation {
rule_index: usize,
variables: Vec<VariableSymbol>,
},
UnsafeFilter {
rule_index: usize,
variables: Vec<VariableSymbol>,
},
UnsafeBind {
rule_index: usize,
variables: Vec<VariableSymbol>,
},
UnsafeAggregate {
rule_index: usize,
variables: Vec<VariableSymbol>,
},
NestedAggregateInInnerBody {
rule_index: usize,
},
UnstratifiableNegation {
predicates: Vec<PredicateSymbol>,
},
NegationUnderEqualityMode {
rule_index: usize,
},
AggregationUnderEqualityMode {
rule_index: usize,
},
SkolemInBodyAtom {
rule_index: usize,
},
TripleTermNestingExceeded {
rule_index: usize,
depth: usize,
limit: usize,
},
}Expand description
Program validation failures.
Variants§
UnsafeRule
Rule is unsafe because one or more head variables are missing from the positive body literals.
Fields
rule_index: usizeRule index in Program::rules.
variables: Vec<VariableSymbol>Missing variables.
UnsafeNegation
Rule has a negated body literal whose variables are not bound by any positive body literal (range-restriction violation — negation-as-failure requires the negated atom to be ground at evaluation time).
Fields
rule_index: usizeRule index in Program::rules.
variables: Vec<VariableSymbol>Unbound variables in negated literals.
UnsafeFilter
Rule has a Literal::Filter
referencing variables that no positive body literal binds.
Filters guard candidate bindings; they cannot introduce
new ones.
Fields
rule_index: usizeRule index in Program::rules.
variables: Vec<VariableSymbol>Unbound variables in filter expressions.
UnsafeBind
Rule has a Literal::Bind
whose expr references a variable not bound by an earlier
positive atom or Bind, or whose output var shadows a
variable that is already bound by an earlier positive atom
or Bind. Both cases produce undefined evaluation order
under sequential rule-body semantics.
Fields
rule_index: usizeRule index in Program::rules.
variables: Vec<VariableSymbol>Offending variables — either an unbound expression reference or a colliding output name.
UnsafeAggregate
Rule has a
Literal::Aggregate
that violates aggregation safety:
input_varor agroup_bykey is not bound by the inner body.result_varis not fresh (collides with an outer-rule binding).- An inner negative literal or filter references a variable that no
inner positive atom or
BINDproduces. - An inner
BINDreferences a variable not bound by an earlier inner positive atom orBIND, or its output variable collides with an existing inner-scope binding.
Nested aggregates inside an aggregate’s inner body surface
separately as Self::NestedAggregateInInnerBody.
Fields
rule_index: usizeRule index in Program::rules.
variables: Vec<VariableSymbol>Offending variables.
NestedAggregateInInnerBody
Rule has a Literal::Aggregate
whose inner_body itself contains a nested
Literal::Aggregate. Nested aggregation is out of scope —
the evaluator only folds a flat inner sub-query — and the
inner aggregate’s stratification dependencies would
require an extra rewriting pass. Authors that need
aggregation over an aggregate’s output should lift the
inner aggregate into its own intermediate rule whose
head feeds the outer aggregate’s inner_body.
Fields
rule_index: usizeRule index in Program::rules.
UnstratifiableNegation
Program contains a recursive cycle through a negation edge. Such programs have no unique least fixed point under stratified negation-as-failure semantics.
Fields
predicates: Vec<PredicateSymbol>Predicate symbols whose stratification could not be resolved. Includes every predicate in the offending strongly connected component.
NegationUnderEqualityMode
Rule contains a Literal::Negative
while equality mode is
EqualityMode::SameAs.
Under equality-driven rewriting, terms get rewritten across equality classes, which interacts non-deterministically with negation-as-failure (the set the negated atom is evaluated against changes shape as equality classes merge). Programs that combine negation with equality mode are rejected for this reason. This crate enforces the same restriction so semantics stay stable under the equality rewrite.
Fields
rule_index: usizeRule index in Program::rules.
AggregationUnderEqualityMode
Rule contains a
Literal::Aggregate
while equality mode is
EqualityMode::SameAs.
Aggregation depends on the complete extension of its inner predicates. Under equality mode that extension is non-monotonic as equality classes merge term identities, which would silently change aggregate results across reasoning rounds. This crate rejects the combination.
Fields
rule_index: usizeRule index in Program::rules.
SkolemInBodyAtom
Rule has a body atom (positive, negative, filter, bind, or
aggregate inner atom) that carries a
Term::Skolem term. SKOLEM is
a deterministic IRI-minting function and is only
well-defined in head positions — using it as a body pattern
would be a no-op match (the freshly-minted IRI never unifies
with anything in the EDB). See extension.
Fields
rule_index: usizeRule index in Program::rules.
TripleTermNestingExceeded
Rule contains a
Term::TripleTerm nested
deeper than
MAX_TRIPLE_TERM_NESTING
in either the head or a body atom. Unification cost grows
with nesting; the bound exists to keep evaluation finite.
Trait Implementations§
Source§impl Clone for ProgramValidationError
impl Clone for ProgramValidationError
Source§impl Debug for ProgramValidationError
impl Debug for ProgramValidationError
Source§impl Display for ProgramValidationError
impl Display for ProgramValidationError
impl Eq for ProgramValidationError
Source§impl Error for ProgramValidationError
impl Error for ProgramValidationError
1.30.0 · Source§fn source(&self) -> Option<&(dyn Error + 'static)>
fn source(&self) -> Option<&(dyn Error + 'static)>
1.0.0 · Source§fn description(&self) -> &str
fn description(&self) -> &str
use the Display impl or to_string()