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, serde::Serialize, serde::Deserialize)]
30#[serde(try_from = "super::serde_input::TermInput")]
31pub enum Term {
32 /// Variable term.
33 Variable(VariableSymbol),
34 /// Constant term.
35 Constant(ConstantSymbol),
36 /// Quoted-triple term: an inner [`Atom`] used as a value in
37 /// the enclosing atom. Conceptually represents `<< s p o >>`
38 /// per RDF 1.2 N-Triples-star syntax.
39 TripleTerm(Box<Atom>),
40 /// `SKOLEM(name, arg_1, …, arg_n)` — a deterministic fresh-IRI
41 /// minting function (extension). Permitted in rule heads only;
42 /// arguments must be [`Self::Variable`] or [`Self::Constant`]
43 /// (no nested SKOLEM, no quoted-triple terms).
44 Skolem {
45 /// Label that namespaces the skolemized IRI — typically a
46 /// short ASCII tag like `"example-key"` so collisions across
47 /// independent rule sets stay scoped per author.
48 name: ConstantSymbol,
49 /// Argument terms whose ground values feed the
50 /// content-addressed hash. Must be variables or constants.
51 args: Vec<Term>,
52 },
53}
54
55impl Term {
56 pub(super) fn collect_variables(&self, out: &mut std::collections::BTreeSet<VariableSymbol>) {
57 match self {
58 Self::Variable(var) => {
59 out.insert(var.clone());
60 }
61 Self::Constant(_) => {}
62 Self::TripleTerm(atom) => {
63 for term in &atom.terms {
64 term.collect_variables(out);
65 }
66 }
67 Self::Skolem { args, .. } => {
68 for term in args {
69 term.collect_variables(out);
70 }
71 }
72 }
73 }
74
75 /// Depth of the term's triple-term nesting. `0` for plain
76 /// variables, constants, and SKOLEM terms (a SKOLEM produces a
77 /// flat IRI so it doesn't extend the triple-term tree);
78 /// `1 + max_child_depth` for a `TripleTerm` whose inner atom
79 /// contains other terms.
80 #[must_use]
81 pub(super) fn nesting_depth(&self) -> usize {
82 match self {
83 Self::Variable(_) | Self::Constant(_) | Self::Skolem { .. } => 0,
84 Self::TripleTerm(atom) => 1 + atom.nesting_depth(),
85 }
86 }
87
88 /// Returns `true` when the term is a `SKOLEM(...)` function
89 /// call. Used by body-atom validation to reject SKOLEM terms
90 /// outside head positions.
91 #[must_use]
92 pub fn is_skolem(&self) -> bool {
93 matches!(self, Self::Skolem { .. })
94 }
95}
96
97/// Maximum allowed nesting depth for [`Term::TripleTerm`]
98/// variants. Programs whose triple-term nesting exceeds this
99/// limit are rejected at
100/// [`Program::validate`](super::program::Program::validate) time.
101///
102/// The bound exists because unification cost grows with nesting
103/// and because the W3C RDF-star CG has not specified a
104/// normative bound — see
105/// [rdf12-triple-term-reasoning.mdx](the RDF-star specification)
106/// for the rationale.
107pub const MAX_TRIPLE_TERM_NESTING: usize = 4;
108
109/// Display a [`Term`]: variables as `?<name>`, constants as their
110/// raw symbol, and triple terms as `<< s p o >>` per
111/// N-Triples-star syntax.
112impl fmt::Display for Term {
113 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
114 match self {
115 Self::Variable(var) => write!(f, "?{}", var.as_str()),
116 Self::Constant(c) => write!(f, "{}", c.as_str()),
117 Self::TripleTerm(atom) => {
118 // RDF-star convention: `<< s p o >>` for the
119 // 2-arity case (subject + object as the inner
120 // atom's `terms`, predicate as the inner atom's
121 // `predicate`). For other arities — which are
122 // valid as a Datalog encoding even though they
123 // are not standard RDF triples — fall back to
124 // `<< pred(t1, t2, …) >>` so the print still
125 // round-trips through a developer's eye.
126 if atom.terms.len() == 2 {
127 write!(
128 f,
129 "<< {} {} {} >>",
130 atom.terms[0],
131 atom.predicate.as_str(),
132 atom.terms[1],
133 )
134 } else {
135 write!(f, "<< {atom} >>")
136 }
137 }
138 Self::Skolem { name, args } => {
139 write!(f, "SKOLEM({}", name.as_str())?;
140 for arg in args {
141 write!(f, ", {arg}")?;
142 }
143 write!(f, ")")
144 }
145 }
146 }
147}