datalog_structural_model/ir/error.rs
1//! [`ProgramValidationError`] and its `Display` / `Error` /
2//! `From` integration with [`StratificationError`].
3
4use std::error::Error;
5use std::fmt;
6
7use super::symbols::{PredicateSymbol, VariableSymbol};
8use crate::stratify::StratificationError;
9
10/// Program validation failures.
11#[derive(Clone, Debug, Eq, PartialEq)]
12pub enum ProgramValidationError {
13 /// Rule is unsafe because one or more head variables are
14 /// missing from the positive body literals.
15 UnsafeRule {
16 /// Rule index in [`Program::rules`](super::program::Program::rules).
17 rule_index: usize,
18 /// Missing variables.
19 variables: Vec<VariableSymbol>,
20 },
21 /// Rule has a negated body literal whose variables are not
22 /// bound by any positive body literal (range-restriction
23 /// violation — negation-as-failure requires the negated atom
24 /// to be ground at evaluation time).
25 UnsafeNegation {
26 /// Rule index in [`Program::rules`](super::program::Program::rules).
27 rule_index: usize,
28 /// Unbound variables in negated literals.
29 variables: Vec<VariableSymbol>,
30 },
31 /// Rule has a [`Literal::Filter`](super::literal::Literal::Filter)
32 /// referencing variables that no positive body literal binds.
33 /// Filters guard candidate bindings; they cannot introduce
34 /// new ones.
35 UnsafeFilter {
36 /// Rule index in [`Program::rules`](super::program::Program::rules).
37 rule_index: usize,
38 /// Unbound variables in filter expressions.
39 variables: Vec<VariableSymbol>,
40 },
41 /// Rule has a [`Literal::Bind`](super::literal::Literal::Bind)
42 /// whose `expr` references a variable not bound by an earlier
43 /// positive atom or `Bind`, or whose output `var` shadows a
44 /// variable that is already bound by an earlier positive atom
45 /// or `Bind`. Both cases produce undefined evaluation order
46 /// under sequential rule-body semantics.
47 UnsafeBind {
48 /// Rule index in [`Program::rules`](super::program::Program::rules).
49 rule_index: usize,
50 /// Offending variables — either an unbound expression
51 /// reference or a colliding output name.
52 variables: Vec<VariableSymbol>,
53 },
54 /// Rule has a
55 /// [`Literal::Aggregate`](super::literal::Literal::Aggregate)
56 /// that violates aggregation safety:
57 ///
58 /// - `input_var` or a `group_by` key is not bound by the inner body.
59 /// - `result_var` is not fresh (collides with an outer-rule binding).
60 /// - An inner negative literal or filter references a variable that no
61 /// inner positive atom or `BIND` produces.
62 /// - An inner `BIND` references a variable not bound by an earlier inner
63 /// positive atom or `BIND`, or its output variable collides with an
64 /// existing inner-scope binding.
65 ///
66 /// Nested aggregates inside an aggregate's inner body surface
67 /// separately as [`Self::NestedAggregateInInnerBody`].
68 UnsafeAggregate {
69 /// Rule index in [`Program::rules`](super::program::Program::rules).
70 rule_index: usize,
71 /// Offending variables.
72 variables: Vec<VariableSymbol>,
73 },
74 /// Rule has a [`Literal::Aggregate`](super::literal::Literal::Aggregate)
75 /// whose `inner_body` itself contains a nested
76 /// `Literal::Aggregate`. Nested aggregation is out of scope —
77 /// the evaluator only folds a flat inner sub-query — and the
78 /// inner aggregate's stratification dependencies would
79 /// require an extra rewriting pass. Authors that need
80 /// aggregation over an aggregate's output should lift the
81 /// inner aggregate into its own intermediate rule whose
82 /// head feeds the outer aggregate's `inner_body`.
83 NestedAggregateInInnerBody {
84 /// Rule index in [`Program::rules`](super::program::Program::rules).
85 rule_index: usize,
86 },
87 /// Program contains a recursive cycle through a negation
88 /// edge. Such programs have no unique least fixed point under
89 /// stratified negation-as-failure semantics.
90 UnstratifiableNegation {
91 /// Predicate symbols whose stratification could not be
92 /// resolved. Includes every predicate in the offending
93 /// strongly connected component.
94 predicates: Vec<PredicateSymbol>,
95 },
96 /// Rule contains a [`Literal::Negative`](super::literal::Literal::Negative)
97 /// while equality mode is
98 /// [`EqualityMode::SameAs`](super::EqualityMode::SameAs).
99 ///
100 /// Under equality-driven rewriting, terms get rewritten across
101 /// equality classes, which interacts
102 /// non-deterministically with negation-as-failure (the set
103 /// the negated atom is evaluated against changes shape as
104 /// equality classes merge). Programs that combine negation with
105 /// equality mode are rejected for this reason. This
106 /// crate enforces the same restriction so semantics stay stable
107 /// under the equality rewrite.
108 NegationUnderEqualityMode {
109 /// Rule index in [`Program::rules`](super::program::Program::rules).
110 rule_index: usize,
111 },
112 /// Rule contains a
113 /// [`Literal::Aggregate`](super::literal::Literal::Aggregate)
114 /// while equality mode is
115 /// [`EqualityMode::SameAs`](super::EqualityMode::SameAs).
116 ///
117 /// Aggregation depends on the *complete* extension of its
118 /// inner predicates. Under equality mode that extension is
119 /// non-monotonic as equality classes merge term identities,
120 /// which would silently change aggregate results across
121 /// reasoning rounds. This crate rejects the combination.
122 AggregationUnderEqualityMode {
123 /// Rule index in [`Program::rules`](super::program::Program::rules).
124 rule_index: usize,
125 },
126 /// Rule has a body atom (positive, negative, filter, bind, or
127 /// aggregate inner atom) that carries a
128 /// [`Term::Skolem`](super::term::Term::Skolem) term. SKOLEM is
129 /// a deterministic IRI-minting function and is only
130 /// well-defined in head positions — using it as a body pattern
131 /// would be a no-op match (the freshly-minted IRI never unifies
132 /// with anything in the EDB). See extension.
133 SkolemInBodyAtom {
134 /// Rule index in [`Program::rules`](super::program::Program::rules).
135 rule_index: usize,
136 },
137 /// Rule contains a
138 /// [`Term::TripleTerm`](super::term::Term::TripleTerm) nested
139 /// deeper than
140 /// [`MAX_TRIPLE_TERM_NESTING`](super::term::MAX_TRIPLE_TERM_NESTING)
141 /// in either the head or a body atom. Unification cost grows
142 /// with nesting; the bound exists to keep evaluation finite.
143 TripleTermNestingExceeded {
144 /// Rule index in [`Program::rules`](super::program::Program::rules).
145 rule_index: usize,
146 /// Observed nesting depth (always >
147 /// `MAX_TRIPLE_TERM_NESTING`).
148 depth: usize,
149 /// Configured limit at the time of validation.
150 limit: usize,
151 },
152}
153
154impl From<StratificationError> for ProgramValidationError {
155 fn from(err: StratificationError) -> Self {
156 let StratificationError::UnstratifiableCycle { predicates } = err;
157 Self::UnstratifiableNegation { predicates }
158 }
159}
160
161impl fmt::Display for ProgramValidationError {
162 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
163 match self {
164 Self::UnsafeRule {
165 rule_index,
166 variables,
167 } => {
168 write!(
169 f,
170 "rule at index {rule_index} is unsafe; missing head variables in body: "
171 )?;
172 for (idx, var) in variables.iter().enumerate() {
173 if idx > 0 {
174 write!(f, ", ")?;
175 }
176 write!(f, "{}", var.as_str())?;
177 }
178 Ok(())
179 }
180 Self::UnsafeNegation {
181 rule_index,
182 variables,
183 } => {
184 write!(
185 f,
186 "rule at index {rule_index} has unsafe negation; variables in negated \
187 literals are not bound by positive body: "
188 )?;
189 for (idx, var) in variables.iter().enumerate() {
190 if idx > 0 {
191 write!(f, ", ")?;
192 }
193 write!(f, "{}", var.as_str())?;
194 }
195 Ok(())
196 }
197 Self::UnsafeFilter {
198 rule_index,
199 variables,
200 } => {
201 write!(
202 f,
203 "rule at index {rule_index} has an unsafe filter; variables in filter \
204 expressions are not bound by positive body: "
205 )?;
206 for (idx, var) in variables.iter().enumerate() {
207 if idx > 0 {
208 write!(f, ", ")?;
209 }
210 write!(f, "{}", var.as_str())?;
211 }
212 Ok(())
213 }
214 Self::UnsafeBind {
215 rule_index,
216 variables,
217 } => {
218 write!(
219 f,
220 "rule at index {rule_index} has an unsafe BIND; offending variables \
221 (unbound expr reference or colliding output name): "
222 )?;
223 for (idx, var) in variables.iter().enumerate() {
224 if idx > 0 {
225 write!(f, ", ")?;
226 }
227 write!(f, "{}", var.as_str())?;
228 }
229 Ok(())
230 }
231 Self::UnsafeAggregate {
232 rule_index,
233 variables,
234 } => {
235 write!(
236 f,
237 "rule at index {rule_index} has an unsafe aggregate; offending variables \
238 (unbound input / group-by, colliding result_var, or unsupported inner \
239 literal): "
240 )?;
241 for (idx, var) in variables.iter().enumerate() {
242 if idx > 0 {
243 write!(f, ", ")?;
244 }
245 write!(f, "{}", var.as_str())?;
246 }
247 Ok(())
248 }
249 Self::NestedAggregateInInnerBody { rule_index } => {
250 write!(
251 f,
252 "rule at index {rule_index} has an aggregate whose inner body contains a \
253 nested aggregate; nested aggregation is not supported — lift the inner \
254 aggregate into its own rule"
255 )
256 }
257 Self::NegationUnderEqualityMode { rule_index } => {
258 write!(
259 f,
260 "rule at index {rule_index} contains a negative literal while equality mode \
261 is `SameAs`; negation and equality rewriting are mutually \
262 exclusive (extension)"
263 )
264 }
265 Self::AggregationUnderEqualityMode { rule_index } => {
266 write!(
267 f,
268 "rule at index {rule_index} contains an aggregate body literal while equality \
269 mode is `SameAs`; aggregation and equality rewriting are \
270 mutually exclusive (extension)"
271 )
272 }
273 Self::UnstratifiableNegation { predicates } => {
274 write!(f, "program contains a recursive cycle through negation: ")?;
275 for (idx, p) in predicates.iter().enumerate() {
276 if idx > 0 {
277 write!(f, ", ")?;
278 }
279 write!(f, "{}", p.as_str())?;
280 }
281 Ok(())
282 }
283 Self::SkolemInBodyAtom { rule_index } => {
284 write!(
285 f,
286 "rule at index {rule_index} has a body atom carrying a SKOLEM term; \
287 SKOLEM is only allowed in head atoms (extension)"
288 )
289 }
290 Self::TripleTermNestingExceeded {
291 rule_index,
292 depth,
293 limit,
294 } => {
295 write!(
296 f,
297 "rule at index {rule_index} contains a triple-term nested {depth} deep; \
298 limit is {limit}"
299 )
300 }
301 }
302 }
303}
304
305impl Error for ProgramValidationError {}