datalog_structural_model/ir/
structural_term.rs

1//! Context-free term invariants shared by constructors and checked decoding.
2use super::{Atom, ConstantSymbol, GroundAtom, GroundTerm, MAX_TRIPLE_TERM_NESTING, Term};
3use std::{error::Error, fmt};
4
5/// Invalid term structure, independent of variable binding or rule position.
6#[derive(Clone, Debug, Eq, PartialEq, serde::Serialize, serde::Deserialize)]
7#[serde(deny_unknown_fields)]
8pub enum TermShapeError {
9    /// A structured term exceeds the supported nesting depth.
10    TripleTermNestingExceeded {
11        /// Observed nesting depth.
12        depth: usize,
13        /// Supported maximum depth.
14        limit: usize,
15    },
16    /// A Skolem argument is neither a variable nor a constant.
17    InvalidSkolemArguments,
18}
19impl fmt::Display for TermShapeError {
20    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
21        match self {
22            Self::TripleTermNestingExceeded { depth, limit } => {
23                write!(f, "triple term depth {depth} exceeds limit {limit}")
24            }
25            Self::InvalidSkolemArguments => {
26                f.write_str("Skolem arguments must be variables or constants")
27            }
28        }
29    }
30}
31impl Error for TermShapeError {}
32impl Term {
33    /// Construct a structured term with checked nesting and Skolem arguments.
34    /// # Errors
35    /// Rejects excessive nesting or invalid nested Skolem arguments.
36    pub fn try_triple_term(atom: Atom) -> Result<Self, TermShapeError> {
37        let term = Self::TripleTerm(Box::new(atom));
38        term.validate_structure()?;
39        Ok(term)
40    }
41    /// Construct a deterministic head term with flat arguments.
42    /// # Errors
43    /// Rejects arguments other than variables and constants.
44    pub fn try_skolem(name: ConstantSymbol, args: Vec<Self>) -> Result<Self, TermShapeError> {
45        let term = Self::Skolem { name, args };
46        term.validate_structure()?;
47        Ok(term)
48    }
49    /// Check context-free structure. Rule-position and binding checks require
50    /// [`super::Program::validate`].
51    /// # Errors
52    /// Rejects excessive triple depth or non-flat Skolem arguments.
53    pub fn validate_structure(&self) -> Result<(), TermShapeError> {
54        let depth = self.nesting_depth();
55        if depth > MAX_TRIPLE_TERM_NESTING {
56            return Err(TermShapeError::TripleTermNestingExceeded {
57                depth,
58                limit: MAX_TRIPLE_TERM_NESTING,
59            });
60        }
61        match self {
62            Self::Variable(_) | Self::Constant(_) => {}
63            Self::TripleTerm(atom) => {
64                for term in &atom.terms {
65                    term.validate_structure()?;
66                }
67            }
68            Self::Skolem { args, .. } => {
69                if args
70                    .iter()
71                    .any(|term| !matches!(term, Self::Variable(_) | Self::Constant(_)))
72                {
73                    return Err(TermShapeError::InvalidSkolemArguments);
74                }
75            }
76        }
77        Ok(())
78    }
79}
80impl GroundTerm {
81    fn nesting_depth(&self) -> usize {
82        match self {
83            Self::Constant(_) => 0,
84            Self::TripleTerm(atom) => {
85                1 + atom.args.iter().map(Self::nesting_depth).max().unwrap_or(0)
86            }
87        }
88    }
89    /// Construct a grounded structured term with checked nesting.
90    /// # Errors
91    /// Rejects excessive triple-term nesting.
92    pub fn try_triple_term(atom: GroundAtom) -> Result<Self, TermShapeError> {
93        let term = Self::TripleTerm(Box::new(atom));
94        term.validate_structure()?;
95        Ok(term)
96    }
97    /// Check the same nesting invariant used before grounding a program.
98    /// # Errors
99    /// Rejects excessive triple-term nesting.
100    pub fn validate_structure(&self) -> Result<(), TermShapeError> {
101        let depth = self.nesting_depth();
102        if depth > MAX_TRIPLE_TERM_NESTING {
103            return Err(TermShapeError::TripleTermNestingExceeded {
104                depth,
105                limit: MAX_TRIPLE_TERM_NESTING,
106            });
107        }
108        Ok(())
109    }
110}
datalog_structural_model/ir/structural_term.rs

datalog_structural_model/ir/
structural_term.rs
