datalog_structural_model/ir/
term.rs

1//! Datalog [`Term`] enum and the triple-term nesting bound.
2
3use std::fmt;
4
5use super::atom::Atom;
6use super::symbols::{ConstantSymbol, VariableSymbol};
7
8/// Datalog term (`variable`, `constant`, `quoted-triple term`,
9/// or `SKOLEM(name, args...)` function call).
10///
11/// The `TripleTerm` variant lets rules name quoted-triple
12/// arguments per RDF 1.2 / RDF-star, encoded as a 2-arity
13/// [`Atom`] whose predicate is the triple's predicate IRI and
14/// whose `terms` slot holds `[subject, object]`. Nesting is
15/// bounded by [`MAX_TRIPLE_TERM_NESTING`] to keep unification
16/// cost finite — programs that exceed the limit are rejected at
17/// [`Program::validate`](super::program::Program::validate) time.
18///
19/// The `Skolem` variant (extension) is a deterministic fresh-IRI
20/// minting operator: given a label and a tuple of argument terms,
21/// the evaluator produces a stable
22/// `urn:example:skolem:<label>:<hash>` IRI that's content-addressed
23/// from the argument bindings. SKOLEM is only meaningful in head
24/// positions — body atoms that carry a `Skolem` term are rejected
25/// at validation time as
26/// [`super::error::ProgramValidationError::SkolemInBodyAtom`]
27/// because a SKOLEM term has no pattern semantics (it's a
28/// function, not a wildcard).
29#[derive(Clone, Debug, Eq, Hash, PartialEq)]
30pub enum Term {
31    /// Variable term.
32    Variable(VariableSymbol),
33    /// Constant term.
34    Constant(ConstantSymbol),
35    /// Quoted-triple term: an inner [`Atom`] used as a value in
36    /// the enclosing atom. Conceptually represents `<< s p o >>`
37    /// per RDF 1.2 N-Triples-star syntax.
38    TripleTerm(Box<Atom>),
39    /// `SKOLEM(name, arg_1, …, arg_n)` — a deterministic fresh-IRI
40    /// minting function (extension). Permitted in rule heads only;
41    /// arguments must be [`Self::Variable`] or [`Self::Constant`]
42    /// (no nested SKOLEM, no quoted-triple terms).
43    Skolem {
44        /// Label that namespaces the skolemized IRI — typically a
45        /// short ASCII tag like `"example-key"` so collisions across
46        /// independent rule sets stay scoped per author.
47        name: ConstantSymbol,
48        /// Argument terms whose ground values feed the
49        /// content-addressed hash. Must be variables or constants.
50        args: Vec<Term>,
51    },
52}
53
54impl Term {
55    #[must_use]
56    pub(super) fn variable_name(&self) -> Option<&VariableSymbol> {
57        match self {
58            Self::Variable(var) => Some(var),
59            Self::Constant(_) | Self::TripleTerm(_) | Self::Skolem { .. } => None,
60        }
61    }
62
63    /// Depth of the term's triple-term nesting. `0` for plain
64    /// variables, constants, and SKOLEM terms (a SKOLEM produces a
65    /// flat IRI so it doesn't extend the triple-term tree);
66    /// `1 + max_child_depth` for a `TripleTerm` whose inner atom
67    /// contains other terms.
68    #[must_use]
69    pub(super) fn nesting_depth(&self) -> usize {
70        match self {
71            Self::Variable(_) | Self::Constant(_) | Self::Skolem { .. } => 0,
72            Self::TripleTerm(atom) => 1 + atom.nesting_depth(),
73        }
74    }
75
76    /// Returns `true` when the term is a `SKOLEM(...)` function
77    /// call. Used by body-atom validation to reject SKOLEM terms
78    /// outside head positions.
79    #[must_use]
80    pub fn is_skolem(&self) -> bool {
81        matches!(self, Self::Skolem { .. })
82    }
83}
84
85/// Maximum allowed nesting depth for [`Term::TripleTerm`]
86/// variants. Programs whose triple-term nesting exceeds this
87/// limit are rejected at
88/// [`Program::validate`](super::program::Program::validate) time.
89///
90/// The bound exists because unification cost grows with nesting
91/// and because the W3C RDF-star CG has not specified a
92/// normative bound — see
93/// [rdf12-triple-term-reasoning.mdx](the RDF-star specification)
94/// for the rationale.
95pub const MAX_TRIPLE_TERM_NESTING: usize = 4;
96
97/// Display a [`Term`]: variables as `?<name>`, constants as their
98/// raw symbol, and triple terms as `<< s p o >>` per
99/// N-Triples-star syntax.
100impl fmt::Display for Term {
101    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
102        match self {
103            Self::Variable(var) => write!(f, "?{}", var.as_str()),
104            Self::Constant(c) => write!(f, "{}", c.as_str()),
105            Self::TripleTerm(atom) => {
106                // RDF-star convention: `<< s p o >>` for the
107                // 2-arity case (subject + object as the inner
108                // atom's `terms`, predicate as the inner atom's
109                // `predicate`). For other arities — which are
110                // valid as a Datalog encoding even though they
111                // are not standard RDF triples — fall back to
112                // `<< pred(t1, t2, …) >>` so the print still
113                // round-trips through a developer's eye.
114                if atom.terms.len() == 2 {
115                    write!(
116                        f,
117                        "<< {} {} {} >>",
118                        atom.terms[0],
119                        atom.predicate.as_str(),
120                        atom.terms[1],
121                    )
122                } else {
123                    write!(f, "<< {atom} >>")
124                }
125            }
126            Self::Skolem { name, args } => {
127                write!(f, "SKOLEM({}", name.as_str())?;
128                for arg in args {
129                    write!(f, ", {arg}")?;
130                }
131                write!(f, ")")
132            }
133        }
134    }
135}
datalog_structural_model/ir/term.rs

datalog_structural_model/ir/
term.rs
