tensorlogic_ir/expr/
validation.rs

1//! Expression validation (arity checking).
2
3use std::collections::HashMap;
4
5use super::TLExpr;
6
7impl TLExpr {
8    /// Validate that all predicates with the same name have consistent arity
9    pub fn validate_arity(&self) -> Result<(), String> {
10        self.validate_arity_recursive(&HashMap::new())
11    }
12
13    fn validate_arity_recursive(&self, seen: &HashMap<String, usize>) -> Result<(), String> {
14        match self {
15            TLExpr::Pred { name, args } => {
16                if let Some(&expected_arity) = seen.get(name) {
17                    if expected_arity != args.len() {
18                        return Err(format!(
19                            "Predicate '{}' has inconsistent arity: expected {}, found {}",
20                            name,
21                            expected_arity,
22                            args.len()
23                        ));
24                    }
25                }
26                let mut new_seen = seen.clone();
27                new_seen.insert(name.clone(), args.len());
28                Ok(())
29            }
30            TLExpr::And(l, r)
31            | TLExpr::Or(l, r)
32            | TLExpr::Imply(l, r)
33            | TLExpr::Add(l, r)
34            | TLExpr::Sub(l, r)
35            | TLExpr::Mul(l, r)
36            | TLExpr::Div(l, r)
37            | TLExpr::Pow(l, r)
38            | TLExpr::Mod(l, r)
39            | TLExpr::Min(l, r)
40            | TLExpr::Max(l, r)
41            | TLExpr::Eq(l, r)
42            | TLExpr::Lt(l, r)
43            | TLExpr::Gt(l, r)
44            | TLExpr::Lte(l, r)
45            | TLExpr::Gte(l, r) => {
46                let mut new_seen = seen.clone();
47
48                l.collect_and_check_arity(&mut new_seen)?;
49                r.collect_and_check_arity(&mut new_seen)?;
50
51                Ok(())
52            }
53            TLExpr::Not(e)
54            | TLExpr::Score(e)
55            | TLExpr::Abs(e)
56            | TLExpr::Floor(e)
57            | TLExpr::Ceil(e)
58            | TLExpr::Round(e)
59            | TLExpr::Sqrt(e)
60            | TLExpr::Exp(e)
61            | TLExpr::Log(e)
62            | TLExpr::Sin(e)
63            | TLExpr::Cos(e)
64            | TLExpr::Tan(e)
65            | TLExpr::Box(e)
66            | TLExpr::Diamond(e)
67            | TLExpr::Next(e)
68            | TLExpr::Eventually(e)
69            | TLExpr::Always(e) => e.validate_arity_recursive(seen),
70            TLExpr::Until { before, after } => {
71                let mut new_seen = seen.clone();
72                before.collect_and_check_arity(&mut new_seen)?;
73                after.collect_and_check_arity(&mut new_seen)?;
74                Ok(())
75            }
76            TLExpr::Exists { body, .. } | TLExpr::ForAll { body, .. } => {
77                body.validate_arity_recursive(seen)
78            }
79            TLExpr::Aggregate { body, .. } => body.validate_arity_recursive(seen),
80            TLExpr::IfThenElse {
81                condition,
82                then_branch,
83                else_branch,
84            } => {
85                let mut new_seen = seen.clone();
86                condition.collect_and_check_arity(&mut new_seen)?;
87                then_branch.collect_and_check_arity(&mut new_seen)?;
88                else_branch.collect_and_check_arity(&mut new_seen)?;
89                Ok(())
90            }
91            TLExpr::Let { value, body, .. } => {
92                let mut new_seen = seen.clone();
93                value.collect_and_check_arity(&mut new_seen)?;
94                body.collect_and_check_arity(&mut new_seen)?;
95                Ok(())
96            }
97
98            // Fuzzy logic operators
99            TLExpr::TNorm { left, right, .. } | TLExpr::TCoNorm { left, right, .. } => {
100                let mut new_seen = seen.clone();
101                left.collect_and_check_arity(&mut new_seen)?;
102                right.collect_and_check_arity(&mut new_seen)?;
103                Ok(())
104            }
105            TLExpr::FuzzyNot { expr, .. } => expr.validate_arity_recursive(seen),
106            TLExpr::FuzzyImplication {
107                premise,
108                conclusion,
109                ..
110            } => {
111                let mut new_seen = seen.clone();
112                premise.collect_and_check_arity(&mut new_seen)?;
113                conclusion.collect_and_check_arity(&mut new_seen)?;
114                Ok(())
115            }
116
117            // Probabilistic operators
118            TLExpr::SoftExists { body, .. } | TLExpr::SoftForAll { body, .. } => {
119                body.validate_arity_recursive(seen)
120            }
121            TLExpr::WeightedRule { rule, .. } => rule.validate_arity_recursive(seen),
122            TLExpr::ProbabilisticChoice { alternatives } => {
123                let mut new_seen = seen.clone();
124                for (_, expr) in alternatives {
125                    expr.collect_and_check_arity(&mut new_seen)?;
126                }
127                Ok(())
128            }
129
130            // Extended temporal logic
131            TLExpr::Release { released, releaser }
132            | TLExpr::WeakUntil {
133                before: released,
134                after: releaser,
135            }
136            | TLExpr::StrongRelease { released, releaser } => {
137                let mut new_seen = seen.clone();
138                released.collect_and_check_arity(&mut new_seen)?;
139                releaser.collect_and_check_arity(&mut new_seen)?;
140                Ok(())
141            }
142
143            TLExpr::Constant(_) => Ok(()),
144        }
145    }
146
147    pub(crate) fn collect_and_check_arity(
148        &self,
149        seen: &mut HashMap<String, usize>,
150    ) -> Result<(), String> {
151        match self {
152            TLExpr::Pred { name, args } => {
153                if let Some(&expected_arity) = seen.get(name) {
154                    if expected_arity != args.len() {
155                        return Err(format!(
156                            "Predicate '{}' has inconsistent arity: expected {}, found {}",
157                            name,
158                            expected_arity,
159                            args.len()
160                        ));
161                    }
162                } else {
163                    seen.insert(name.clone(), args.len());
164                }
165                Ok(())
166            }
167            TLExpr::And(l, r)
168            | TLExpr::Or(l, r)
169            | TLExpr::Imply(l, r)
170            | TLExpr::Add(l, r)
171            | TLExpr::Sub(l, r)
172            | TLExpr::Mul(l, r)
173            | TLExpr::Div(l, r)
174            | TLExpr::Pow(l, r)
175            | TLExpr::Mod(l, r)
176            | TLExpr::Min(l, r)
177            | TLExpr::Max(l, r)
178            | TLExpr::Eq(l, r)
179            | TLExpr::Lt(l, r)
180            | TLExpr::Gt(l, r)
181            | TLExpr::Lte(l, r)
182            | TLExpr::Gte(l, r) => {
183                l.collect_and_check_arity(seen)?;
184                r.collect_and_check_arity(seen)?;
185                Ok(())
186            }
187            TLExpr::Not(e)
188            | TLExpr::Score(e)
189            | TLExpr::Abs(e)
190            | TLExpr::Floor(e)
191            | TLExpr::Ceil(e)
192            | TLExpr::Round(e)
193            | TLExpr::Sqrt(e)
194            | TLExpr::Exp(e)
195            | TLExpr::Log(e)
196            | TLExpr::Sin(e)
197            | TLExpr::Cos(e)
198            | TLExpr::Tan(e)
199            | TLExpr::Box(e)
200            | TLExpr::Diamond(e)
201            | TLExpr::Next(e)
202            | TLExpr::Eventually(e)
203            | TLExpr::Always(e) => e.collect_and_check_arity(seen),
204            TLExpr::Until { before, after } => {
205                before.collect_and_check_arity(seen)?;
206                after.collect_and_check_arity(seen)?;
207                Ok(())
208            }
209            TLExpr::Exists { body, .. } | TLExpr::ForAll { body, .. } => {
210                body.collect_and_check_arity(seen)
211            }
212            TLExpr::Aggregate { body, .. } => body.collect_and_check_arity(seen),
213            TLExpr::IfThenElse {
214                condition,
215                then_branch,
216                else_branch,
217            } => {
218                condition.collect_and_check_arity(seen)?;
219                then_branch.collect_and_check_arity(seen)?;
220                else_branch.collect_and_check_arity(seen)?;
221                Ok(())
222            }
223            TLExpr::Let { value, body, .. } => {
224                value.collect_and_check_arity(seen)?;
225                body.collect_and_check_arity(seen)?;
226                Ok(())
227            }
228
229            // Fuzzy logic operators
230            TLExpr::TNorm { left, right, .. } | TLExpr::TCoNorm { left, right, .. } => {
231                left.collect_and_check_arity(seen)?;
232                right.collect_and_check_arity(seen)?;
233                Ok(())
234            }
235            TLExpr::FuzzyNot { expr, .. } => expr.collect_and_check_arity(seen),
236            TLExpr::FuzzyImplication {
237                premise,
238                conclusion,
239                ..
240            } => {
241                premise.collect_and_check_arity(seen)?;
242                conclusion.collect_and_check_arity(seen)?;
243                Ok(())
244            }
245
246            // Probabilistic operators
247            TLExpr::SoftExists { body, .. } | TLExpr::SoftForAll { body, .. } => {
248                body.collect_and_check_arity(seen)
249            }
250            TLExpr::WeightedRule { rule, .. } => rule.collect_and_check_arity(seen),
251            TLExpr::ProbabilisticChoice { alternatives } => {
252                for (_, expr) in alternatives {
253                    expr.collect_and_check_arity(seen)?;
254                }
255                Ok(())
256            }
257
258            // Extended temporal logic
259            TLExpr::Release { released, releaser }
260            | TLExpr::WeakUntil {
261                before: released,
262                after: releaser,
263            }
264            | TLExpr::StrongRelease { released, releaser } => {
265                released.collect_and_check_arity(seen)?;
266                releaser.collect_and_check_arity(seen)?;
267                Ok(())
268            }
269
270            TLExpr::Constant(_) => Ok(()),
271        }
272    }
273}
tensorlogic_ir/expr/validation.rs

tensorlogic_ir/expr/
validation.rs
