datalog_structural_model/stratify/
types.rs

1//! Public stratification result types and error.
2
3use std::collections::{BTreeMap, BTreeSet};
4
5use crate::ir::{Atom, ConstantSymbol, PredicateSymbol, Term};
6
7/// Stratification of a Datalog¬ program.
8#[derive(Clone, Debug, Eq, PartialEq)]
9pub struct Stratification {
10    /// Strata ordered by ascending index. Stratum `k` must be
11    /// evaluated to a fixed point before stratum `k+1`.
12    pub strata: Vec<Stratum>,
13    /// Map from predicate to its stratum index. context-aware rolls up
14    /// the underlying `(predicate, head-graph-class)` dependency
15    /// nodes by taking the **maximum** stratum across head-graph
16    /// classes of the same predicate — so a producer that emits
17    /// facts in more than one graph class is scheduled late
18    /// enough for every downstream consumer.
19    pub predicate_stratum: BTreeMap<PredicateSymbol, usize>,
20}
21
22impl Stratification {
23    /// Returns the stratum index for a predicate, or `None` if
24    /// the predicate does not appear in the program (pure EDB
25    /// predicates not derived by any rule).
26    #[must_use]
27    pub fn stratum_of(&self, predicate: &PredicateSymbol) -> Option<usize> {
28        self.predicate_stratum.get(predicate).copied()
29    }
30}
31
32/// A single stratum — the set of predicates defined together.
33#[derive(Clone, Debug, Default, Eq, PartialEq)]
34pub struct Stratum {
35    /// Predicates whose rules must be evaluated to a fixed point
36    /// within this stratum.
37    pub predicates: BTreeSet<PredicateSymbol>,
38}
39
40/// Stratification failure.
41#[derive(Clone, Debug, Eq, PartialEq)]
42pub enum StratificationError {
43    /// The predicate dependency graph contains a cycle that
44    /// passes through a negation edge.
45    UnstratifiableCycle {
46        /// Every predicate in the offending strongly connected
47        /// component.
48        predicates: Vec<PredicateSymbol>,
49    },
50}
51
52/// Classification of a rule head's trailing graph slot (context-aware).
53///
54/// Stratification keys dependency-graph nodes on
55/// `(PredicateSymbol, HeadGraphClass)` so a producer that pins
56/// every inferred quad to a fixed graph
57/// (`GraphExpr::Literal { graph }` in the reasoner — head ends in
58/// a constant graph IRI) creates a node that's distinct from a
59/// producer emitting into a body-inherited graph
60/// (`GraphExpr::InheritFromBody { .. }` — head ends in a graph
61/// variable like `__g0`). Downstream consumers that constrain
62/// their body graph slot to a constant IRI then depend only on
63/// the producers compatible with that graph.
64///
65/// For the canonical RDFS / OWL-RL profile every rule head ends
66/// in a graph variable (context-aware's `InheritFromBody { 0 }` default),
67/// so every node collapses to [`HeadGraphClass::Inherit`] and the
68/// per-predicate strata that come out the other end match the
69/// pre-context-aware algorithm bit-for-bit.
70#[derive(Clone, Debug, Eq, Hash, Ord, PartialEq, PartialOrd)]
71pub(super) enum HeadGraphClass {
72    /// Head has no trailing term — pre-context-aware narrow atoms
73    /// (predicate-only facts or rules whose head atom is
74    /// constructed without a graph slot).
75    Narrow,
76    /// Head's trailing graph term is a variable — the inferred
77    /// quad inherits its graph from whichever body atom binds
78    /// that variable, so the rule contributes facts to every
79    /// graph class its body atom matches.
80    Inherit,
81    /// Head's trailing graph term is a constant IRI — every
82    /// inferred quad lands in this fixed graph.
83    Literal(ConstantSymbol),
84}
85
86impl HeadGraphClass {
87    /// Classify a head atom's trailing term.
88    ///
89    /// The classification mirrors how the reasoner's
90    /// `GraphExpr` rewrites head atoms at compile time
91    /// ([`super::super`] of this module sees only the resulting
92    /// term, not the original `GraphExpr`):
93    ///
94    /// - trailing `Term::Variable` → [`HeadGraphClass::Inherit`]
95    /// - trailing `Term::Constant` → [`HeadGraphClass::Literal`]
96    /// - no trailing term → [`HeadGraphClass::Narrow`]
97    /// - trailing `Term::TripleTerm` / `Term::Skolem` collapses to
98    ///   [`HeadGraphClass::Inherit`] because both produce a value computed from
99    ///   body bindings rather than a fixed IRI known at compile time.
100    #[must_use]
101    pub(super) fn classify(head: &Atom) -> Self {
102        match head.terms.last() {
103            None => Self::Narrow,
104            Some(Term::Constant(c)) => Self::Literal(c.clone()),
105            Some(Term::Variable(_) | Term::TripleTerm(_) | Term::Skolem { .. }) => Self::Inherit,
106        }
107    }
108}
datalog_structural_model/stratify/types.rs

datalog_structural_model/stratify/
types.rs
