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            // Beta.1 enhancements
144            TLExpr::Lambda { body, .. } => body.validate_arity_recursive(seen),
145            TLExpr::Apply { function, argument } => {
146                let mut new_seen = seen.clone();
147                function.collect_and_check_arity(&mut new_seen)?;
148                argument.collect_and_check_arity(&mut new_seen)?;
149                Ok(())
150            }
151            TLExpr::SetMembership { element, set }
152            | TLExpr::SetUnion {
153                left: element,
154                right: set,
155            }
156            | TLExpr::SetIntersection {
157                left: element,
158                right: set,
159            }
160            | TLExpr::SetDifference {
161                left: element,
162                right: set,
163            } => {
164                let mut new_seen = seen.clone();
165                element.collect_and_check_arity(&mut new_seen)?;
166                set.collect_and_check_arity(&mut new_seen)?;
167                Ok(())
168            }
169            TLExpr::SetCardinality { set } => set.validate_arity_recursive(seen),
170            TLExpr::EmptySet => Ok(()),
171            TLExpr::SetComprehension { condition, .. } => condition.validate_arity_recursive(seen),
172            TLExpr::CountingExists { body, .. }
173            | TLExpr::CountingForAll { body, .. }
174            | TLExpr::ExactCount { body, .. }
175            | TLExpr::Majority { body, .. } => body.validate_arity_recursive(seen),
176            TLExpr::LeastFixpoint { body, .. } | TLExpr::GreatestFixpoint { body, .. } => {
177                body.validate_arity_recursive(seen)
178            }
179            TLExpr::Nominal { .. } => Ok(()),
180            TLExpr::At { formula, .. } => formula.validate_arity_recursive(seen),
181            TLExpr::Somewhere { formula } | TLExpr::Everywhere { formula } => {
182                formula.validate_arity_recursive(seen)
183            }
184            TLExpr::AllDifferent { .. } => Ok(()),
185            TLExpr::GlobalCardinality { values, .. } => {
186                let mut new_seen = seen.clone();
187                for val in values {
188                    val.collect_and_check_arity(&mut new_seen)?;
189                }
190                Ok(())
191            }
192            TLExpr::Abducible { .. } => Ok(()),
193            TLExpr::Explain { formula } => formula.validate_arity_recursive(seen),
194
195            TLExpr::Constant(_) => Ok(()),
196        }
197    }
198
199    pub(crate) fn collect_and_check_arity(
200        &self,
201        seen: &mut HashMap<String, usize>,
202    ) -> Result<(), String> {
203        match self {
204            TLExpr::Pred { name, args } => {
205                if let Some(&expected_arity) = seen.get(name) {
206                    if expected_arity != args.len() {
207                        return Err(format!(
208                            "Predicate '{}' has inconsistent arity: expected {}, found {}",
209                            name,
210                            expected_arity,
211                            args.len()
212                        ));
213                    }
214                } else {
215                    seen.insert(name.clone(), args.len());
216                }
217                Ok(())
218            }
219            TLExpr::And(l, r)
220            | TLExpr::Or(l, r)
221            | TLExpr::Imply(l, r)
222            | TLExpr::Add(l, r)
223            | TLExpr::Sub(l, r)
224            | TLExpr::Mul(l, r)
225            | TLExpr::Div(l, r)
226            | TLExpr::Pow(l, r)
227            | TLExpr::Mod(l, r)
228            | TLExpr::Min(l, r)
229            | TLExpr::Max(l, r)
230            | TLExpr::Eq(l, r)
231            | TLExpr::Lt(l, r)
232            | TLExpr::Gt(l, r)
233            | TLExpr::Lte(l, r)
234            | TLExpr::Gte(l, r) => {
235                l.collect_and_check_arity(seen)?;
236                r.collect_and_check_arity(seen)?;
237                Ok(())
238            }
239            TLExpr::Not(e)
240            | TLExpr::Score(e)
241            | TLExpr::Abs(e)
242            | TLExpr::Floor(e)
243            | TLExpr::Ceil(e)
244            | TLExpr::Round(e)
245            | TLExpr::Sqrt(e)
246            | TLExpr::Exp(e)
247            | TLExpr::Log(e)
248            | TLExpr::Sin(e)
249            | TLExpr::Cos(e)
250            | TLExpr::Tan(e)
251            | TLExpr::Box(e)
252            | TLExpr::Diamond(e)
253            | TLExpr::Next(e)
254            | TLExpr::Eventually(e)
255            | TLExpr::Always(e) => e.collect_and_check_arity(seen),
256            TLExpr::Until { before, after } => {
257                before.collect_and_check_arity(seen)?;
258                after.collect_and_check_arity(seen)?;
259                Ok(())
260            }
261            TLExpr::Exists { body, .. } | TLExpr::ForAll { body, .. } => {
262                body.collect_and_check_arity(seen)
263            }
264            TLExpr::Aggregate { body, .. } => body.collect_and_check_arity(seen),
265            TLExpr::IfThenElse {
266                condition,
267                then_branch,
268                else_branch,
269            } => {
270                condition.collect_and_check_arity(seen)?;
271                then_branch.collect_and_check_arity(seen)?;
272                else_branch.collect_and_check_arity(seen)?;
273                Ok(())
274            }
275            TLExpr::Let { value, body, .. } => {
276                value.collect_and_check_arity(seen)?;
277                body.collect_and_check_arity(seen)?;
278                Ok(())
279            }
280
281            // Fuzzy logic operators
282            TLExpr::TNorm { left, right, .. } | TLExpr::TCoNorm { left, right, .. } => {
283                left.collect_and_check_arity(seen)?;
284                right.collect_and_check_arity(seen)?;
285                Ok(())
286            }
287            TLExpr::FuzzyNot { expr, .. } => expr.collect_and_check_arity(seen),
288            TLExpr::FuzzyImplication {
289                premise,
290                conclusion,
291                ..
292            } => {
293                premise.collect_and_check_arity(seen)?;
294                conclusion.collect_and_check_arity(seen)?;
295                Ok(())
296            }
297
298            // Probabilistic operators
299            TLExpr::SoftExists { body, .. } | TLExpr::SoftForAll { body, .. } => {
300                body.collect_and_check_arity(seen)
301            }
302            TLExpr::WeightedRule { rule, .. } => rule.collect_and_check_arity(seen),
303            TLExpr::ProbabilisticChoice { alternatives } => {
304                for (_, expr) in alternatives {
305                    expr.collect_and_check_arity(seen)?;
306                }
307                Ok(())
308            }
309
310            // Extended temporal logic
311            TLExpr::Release { released, releaser }
312            | TLExpr::WeakUntil {
313                before: released,
314                after: releaser,
315            }
316            | TLExpr::StrongRelease { released, releaser } => {
317                released.collect_and_check_arity(seen)?;
318                releaser.collect_and_check_arity(seen)?;
319                Ok(())
320            }
321
322            // Beta.1 enhancements
323            TLExpr::Lambda { body, .. } => body.collect_and_check_arity(seen),
324            TLExpr::Apply { function, argument } => {
325                function.collect_and_check_arity(seen)?;
326                argument.collect_and_check_arity(seen)?;
327                Ok(())
328            }
329            TLExpr::SetMembership { element, set }
330            | TLExpr::SetUnion {
331                left: element,
332                right: set,
333            }
334            | TLExpr::SetIntersection {
335                left: element,
336                right: set,
337            }
338            | TLExpr::SetDifference {
339                left: element,
340                right: set,
341            } => {
342                element.collect_and_check_arity(seen)?;
343                set.collect_and_check_arity(seen)?;
344                Ok(())
345            }
346            TLExpr::SetCardinality { set } => set.collect_and_check_arity(seen),
347            TLExpr::EmptySet => Ok(()),
348            TLExpr::SetComprehension { condition, .. } => condition.collect_and_check_arity(seen),
349            TLExpr::CountingExists { body, .. }
350            | TLExpr::CountingForAll { body, .. }
351            | TLExpr::ExactCount { body, .. }
352            | TLExpr::Majority { body, .. } => body.collect_and_check_arity(seen),
353            TLExpr::LeastFixpoint { body, .. } | TLExpr::GreatestFixpoint { body, .. } => {
354                body.collect_and_check_arity(seen)
355            }
356            TLExpr::Nominal { .. } => Ok(()),
357            TLExpr::At { formula, .. } => formula.collect_and_check_arity(seen),
358            TLExpr::Somewhere { formula } | TLExpr::Everywhere { formula } => {
359                formula.collect_and_check_arity(seen)
360            }
361            TLExpr::AllDifferent { .. } => Ok(()),
362            TLExpr::GlobalCardinality { values, .. } => {
363                for val in values {
364                    val.collect_and_check_arity(seen)?;
365                }
366                Ok(())
367            }
368            TLExpr::Abducible { .. } => Ok(()),
369            TLExpr::Explain { formula } => formula.collect_and_check_arity(seen),
370
371            TLExpr::Constant(_) => Ok(()),
372        }
373    }
374}
tensorlogic_ir/expr/validation.rs

tensorlogic_ir/expr/
validation.rs
