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