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)]
34pub enum Literal {
35    /// Positive literal — the body atom must match a fact.
36    Positive(Atom),
37    /// Negative literal — the body atom must **not** match any
38    /// fact.
39    Negative(Atom),
40    /// Built-in filter expression evaluated against the current
41    /// candidate binding.
42    Filter(BuiltinFilter),
43    /// `BIND(expr AS ?var)` — extend the current candidate
44    /// binding with a computed value. `var` must be fresh
45    /// (untouched by any earlier positive atom or `Bind`); every
46    /// variable inside `expr` must be bound by an earlier
47    /// positive atom or `Bind`.
48    Bind {
49        /// The fresh variable produced by this bind.
50        var: VariableSymbol,
51        /// The expression to compute. Evaluated against the
52        /// current candidate binding.
53        expr: BindExpr,
54    },
55    /// Aggregation sub-query — fold the inner body into a
56    /// per-group aggregate result that the outer body sees as a
57    /// freshly-bound variable. See [`AggregateBody`] for the
58    /// scoping and inner-body restrictions; the evaluator wiring
59    /// is a deferred extension follow-up.
60    Aggregate(AggregateBody),
61}
62
63impl Literal {
64    /// Access the underlying atom, when this literal carries one.
65    ///
66    /// Returns `None` for [`Literal::Filter`], [`Literal::Bind`],
67    /// and [`Literal::Aggregate`] — none of which carries a
68    /// single fact-matching atom in its top-level position.
69    /// (An aggregate's inner literals live inside
70    /// [`AggregateBody::inner_body`].)
71    #[must_use]
72    pub fn atom(&self) -> Option<&Atom> {
73        match self {
74            Self::Positive(atom) | Self::Negative(atom) => Some(atom),
75            Self::Filter(_) | Self::Bind { .. } | Self::Aggregate(_) => None,
76        }
77    }
78
79    /// True when the literal is positive.
80    #[must_use]
81    pub fn is_positive(&self) -> bool {
82        matches!(self, Self::Positive(_))
83    }
84
85    /// True when the literal is negated.
86    #[must_use]
87    pub fn is_negative(&self) -> bool {
88        matches!(self, Self::Negative(_))
89    }
90
91    /// True when the literal is a [`BuiltinFilter`] guard.
92    #[must_use]
93    pub fn is_filter(&self) -> bool {
94        matches!(self, Self::Filter(_))
95    }
96
97    /// True when the literal is a `BIND(expr AS ?var)` form.
98    #[must_use]
99    pub fn is_bind(&self) -> bool {
100        matches!(self, Self::Bind { .. })
101    }
102
103    /// True when the literal is an aggregation sub-query.
104    #[must_use]
105    pub fn is_aggregate(&self) -> bool {
106        matches!(self, Self::Aggregate(_))
107    }
108}
datalog_structural_model/ir/literal.rs

datalog_structural_model/ir/
literal.rs
