datalog_structural_model/ir/
program.rs

1//! Datalog [`Program`] — an ordered set of [`Rule`]s plus
2//! validation and stratification entry points.
3
4use super::equality_mode::EqualityMode;
5use super::error::ProgramValidationError;
6use super::literal::Literal;
7use super::rule::Rule;
8use crate::stratify::{Stratification, stratify};
9
10/// Datalog program as an ordered set of rules.
11#[derive(Clone, Debug, Default, Eq, PartialEq, serde::Serialize, serde::Deserialize)]
12#[serde(try_from = "super::serde_input::ProgramInput")]
13pub struct Program {
14    /// Program rules.
15    pub rules: Vec<Rule>,
16}
17
18impl Program {
19    /// Construct a program only when all safety and stratification checks pass.
20    /// # Errors
21    /// Returns the same structural failures as [`Self::validate`].
22    pub fn try_new(rules: Vec<Rule>) -> Result<Self, ProgramValidationError> {
23        let program = Self { rules };
24        program.validate()?;
25        Ok(program)
26    }
27
28    /// Validate all rules in the program for safety and
29    /// stratifiability.
30    ///
31    /// Runs two checks:
32    ///
33    /// 1. **Safety** — every rule must be range-restricted; head variables and
34    ///    variables inside negated body literals must also appear in some
35    ///    positive body literal.
36    /// 2. **Stratifiability** — the predicate dependency graph must have no
37    ///    cycle that includes a negation edge (see [`Program::stratify`]).
38    ///
39    /// # Errors
40    ///
41    /// Returns [`ProgramValidationError::UnsafeRule`] on a safety
42    /// failure, [`ProgramValidationError::UnsafeNegation`] when a
43    /// negated body literal references a variable that no positive
44    /// literal binds, or
45    /// [`ProgramValidationError::UnstratifiableNegation`] when the
46    /// program contains a recursive cycle through negation.
47    pub fn validate(&self) -> Result<(), ProgramValidationError> {
48        self.validate_with_equality_mode(EqualityMode::Default)
49    }
50
51    /// Validate the program under a specified equality-reasoning
52    /// mode (extension).
53    ///
54    /// Runs the same safety / stratification / triple-term-nesting
55    /// checks as [`Self::validate`] and additionally rejects
56    /// negation and aggregation when
57    /// `equality_mode == EqualityMode::SameAs`. The two features
58    /// interact non-monotonically with `owl:sameAs` rewriting; see
59    /// [`EqualityMode`] for the semantic rationale.
60    ///
61    /// # Errors
62    ///
63    /// Returns the same errors as [`Self::validate`] plus
64    /// [`ProgramValidationError::NegationUnderEqualityMode`] or
65    /// [`ProgramValidationError::AggregationUnderEqualityMode`]
66    /// when the corresponding feature is used under
67    /// [`EqualityMode::SameAs`].
68    pub fn validate_with_equality_mode(
69        &self,
70        equality_mode: EqualityMode,
71    ) -> Result<(), ProgramValidationError> {
72        if equality_mode == EqualityMode::SameAs {
73            check_equality_mode_compatibility(&self.rules)?;
74        }
75        for (index, rule) in self.rules.iter().enumerate() {
76            rule.validate_term_shapes(index)?;
77            let unsafe_head = rule.unsafe_head_variables();
78            if !unsafe_head.is_empty() {
79                return Err(ProgramValidationError::UnsafeRule {
80                    rule_index: index,
81                    variables: unsafe_head,
82                });
83            }
84            let unsafe_neg = rule.unsafe_negative_variables();
85            if !unsafe_neg.is_empty() {
86                return Err(ProgramValidationError::UnsafeNegation {
87                    rule_index: index,
88                    variables: unsafe_neg,
89                });
90            }
91            let unsafe_filter = rule.unsafe_filter_variables();
92            if !unsafe_filter.is_empty() {
93                return Err(ProgramValidationError::UnsafeFilter {
94                    rule_index: index,
95                    variables: unsafe_filter,
96                });
97            }
98            let unsafe_bind = rule.unsafe_bind_variables();
99            if !unsafe_bind.is_empty() {
100                return Err(ProgramValidationError::UnsafeBind {
101                    rule_index: index,
102                    variables: unsafe_bind,
103                });
104            }
105            if rule.has_nested_aggregate_in_inner_body() {
106                return Err(ProgramValidationError::NestedAggregateInInnerBody {
107                    rule_index: index,
108                });
109            }
110            let unsafe_aggregate = rule.unsafe_aggregate_variables();
111            if !unsafe_aggregate.is_empty() {
112                return Err(ProgramValidationError::UnsafeAggregate {
113                    rule_index: index,
114                    variables: unsafe_aggregate,
115                });
116            }
117        }
118        // Stratification check — reject programs with recursion
119        // through negation.
120        self.stratify()?;
121        Ok(())
122    }
123
124    /// Compute the program's stratification.
125    ///
126    /// Builds the predicate dependency graph (edges from each body
127    /// predicate to the head predicate, tagged with polarity),
128    /// collapses strongly connected components, checks that no SCC
129    /// contains an internal negation edge, and assigns each
130    /// predicate to a stratum such that every negation edge goes
131    /// from a lower stratum to a strictly higher one.
132    ///
133    /// # Errors
134    ///
135    /// Returns [`ProgramValidationError::UnstratifiableNegation`]
136    /// when a cycle in the dependency graph contains a negation
137    /// edge.
138    pub fn stratify(&self) -> Result<Stratification, ProgramValidationError> {
139        stratify(self).map_err(ProgramValidationError::from)
140    }
141}
142
143/// extension — reject negation / aggregation under
144/// [`EqualityMode::SameAs`]. Walks each rule's body and surfaces
145/// the first offending literal as
146/// [`ProgramValidationError::NegationUnderEqualityMode`] or
147/// [`ProgramValidationError::AggregationUnderEqualityMode`].
148fn check_equality_mode_compatibility(rules: &[Rule]) -> Result<(), ProgramValidationError> {
149    for (index, rule) in rules.iter().enumerate() {
150        for lit in &rule.body {
151            match lit {
152                Literal::Negative(_) => {
153                    return Err(ProgramValidationError::NegationUnderEqualityMode {
154                        rule_index: index,
155                    });
156                }
157                Literal::Aggregate(_) => {
158                    return Err(ProgramValidationError::AggregationUnderEqualityMode {
159                        rule_index: index,
160                    });
161                }
162                Literal::Positive(_) | Literal::Filter(_) | Literal::Bind { .. } => {}
163            }
164        }
165    }
166    Ok(())
167}
datalog_structural_model/ir/program.rs

datalog_structural_model/ir/
program.rs
