datalog_structural_model/ir/
literal.rs

1//! Body literal — positive/negated atom, filter, `BIND`, or
2//! aggregation.
3
4use super::aggregate::AggregateBody;
5use super::atom::Atom;
6use super::bind::BindExpr;
7use super::filter::BuiltinFilter;
8use super::symbols::VariableSymbol;
9
10/// Datalog body literal — a positive or negated atom, a built-in
11/// filter expression, or a built-in `BIND(expr AS ?var)` form.
12///
13/// Rule bodies in Datalog¬ are conjunctions of literals. Positive
14/// literals must match facts in the database; negative literals
15/// must **not** match. Negation semantics follow the stratified
16/// negation-as-failure convention: every negated atom references
17/// only predicates in strictly lower strata, so the set of facts
18/// the negation is evaluated against is already closed by the time
19/// the rule fires.
20///
21/// `Filter` literals carry a [`BuiltinFilter`] expression that
22/// guards the current candidate binding — the evaluator drops a
23/// binding whenever the filter does not evaluate to `true`.
24///
25/// `Bind` literals carry a [`BindExpr`] expression and a fresh
26/// variable name; the evaluator extends the current candidate
27/// binding with `var → eval(expr, binding)` and the new variable
28/// is then visible to all subsequent body literals (including
29/// further `Bind`s, `Filter`s, the rule head, and SPARQL-style
30/// constraints over computed values). Filter and bind literals
31/// participate in safety analysis but contribute no edges to the
32/// predicate dependency graph used by stratification.
33#[derive(Clone, Debug, Eq, Hash, PartialEq, serde::Serialize, serde::Deserialize)]
34#[serde(deny_unknown_fields)]
35pub enum Literal {
36    /// Positive literal — the body atom must match a fact.
37    Positive(Atom),
38    /// Negative literal — the body atom must **not** match any
39    /// fact.
40    Negative(Atom),
41    /// Built-in filter expression evaluated against the current
42    /// candidate binding.
43    Filter(BuiltinFilter),
44    /// `BIND(expr AS ?var)` — extend the current candidate
45    /// binding with a computed value. `var` must be fresh
46    /// (untouched by any earlier positive atom or `Bind`); every
47    /// variable inside `expr` must be bound by an earlier
48    /// positive atom or `Bind`.
49    Bind {
50        /// The fresh variable produced by this bind.
51        var: VariableSymbol,
52        /// The expression to compute. Evaluated against the
53        /// current candidate binding.
54        expr: BindExpr,
55    },
56    /// Aggregation sub-query — fold the inner body into a
57    /// per-group aggregate result that the outer body sees as a
58    /// freshly-bound variable. See [`AggregateBody`] for the
59    /// scoping and inner-body restrictions; the evaluator wiring
60    /// is a deferred extension follow-up.
61    Aggregate(AggregateBody),
62}
63
64impl Literal {
65    /// Access the underlying atom, when this literal carries one.
66    ///
67    /// Returns `None` for [`Literal::Filter`], [`Literal::Bind`],
68    /// and [`Literal::Aggregate`] — none of which carries a
69    /// single fact-matching atom in its top-level position.
70    /// (An aggregate's inner literals live inside
71    /// [`AggregateBody::inner_body`].)
72    #[must_use]
73    pub fn atom(&self) -> Option<&Atom> {
74        match self {
75            Self::Positive(atom) | Self::Negative(atom) => Some(atom),
76            Self::Filter(_) | Self::Bind { .. } | Self::Aggregate(_) => None,
77        }
78    }
79
80    /// True when the literal is positive.
81    #[must_use]
82    pub fn is_positive(&self) -> bool {
83        matches!(self, Self::Positive(_))
84    }
85
86    /// True when the literal is negated.
87    #[must_use]
88    pub fn is_negative(&self) -> bool {
89        matches!(self, Self::Negative(_))
90    }
91
92    /// True when the literal is a [`BuiltinFilter`] guard.
93    #[must_use]
94    pub fn is_filter(&self) -> bool {
95        matches!(self, Self::Filter(_))
96    }
97
98    /// True when the literal is a `BIND(expr AS ?var)` form.
99    #[must_use]
100    pub fn is_bind(&self) -> bool {
101        matches!(self, Self::Bind { .. })
102    }
103
104    /// True when the literal is an aggregation sub-query.
105    #[must_use]
106    pub fn is_aggregate(&self) -> bool {
107        matches!(self, Self::Aggregate(_))
108    }
109}
datalog_structural_model/ir/literal.rs

datalog_structural_model/ir/
literal.rs
