tensorlogic_compiler/dead_code/
free_vars.rs

1//! Free-variable analysis used to decide whether Let bindings are dead.
2
3use tensorlogic_ir::TLExpr;
4
5use super::types::DeadCodeEliminator;
6
7impl DeadCodeEliminator {
8    /// Returns `true` if `var` appears free (as a predicate argument or
9    /// inside a binder that does *not* shadow it) anywhere in `expr`.
10    ///
11    /// Variable occurrences in TLExpr live in two places:
12    /// 1. `Term::Var(name)` inside `Pred` args
13    /// 2. `AllDifferent { variables }` variable name lists
14    /// 3. Any binder (`Exists`, `ForAll`, `Let`, `Lambda`, `LeastFixpoint`, etc.)
15    ///    that introduces a new scope — we stop counting the variable as free
16    ///    inside the scope if the binder's name equals `var`.
17    pub fn is_free(&self, var: &str, expr: &TLExpr) -> bool {
18        self.is_free_in(var, expr, false)
19    }
20
21    /// Internal helper for `is_free`, carrying a `shadowed` flag.
22    pub(super) fn is_free_in(&self, var: &str, expr: &TLExpr, shadowed: bool) -> bool {
23        if shadowed {
24            return false;
25        }
26        match expr {
27            TLExpr::Pred { args, .. } => args
28                .iter()
29                .any(|t| matches!(t, tensorlogic_ir::Term::Var(v) if v == var)),
30
31            TLExpr::And(l, r)
32            | TLExpr::Or(l, r)
33            | TLExpr::Imply(l, r)
34            | TLExpr::Add(l, r)
35            | TLExpr::Sub(l, r)
36            | TLExpr::Mul(l, r)
37            | TLExpr::Div(l, r)
38            | TLExpr::Pow(l, r)
39            | TLExpr::Mod(l, r)
40            | TLExpr::Min(l, r)
41            | TLExpr::Max(l, r)
42            | TLExpr::Eq(l, r)
43            | TLExpr::Lt(l, r)
44            | TLExpr::Gt(l, r)
45            | TLExpr::Lte(l, r)
46            | TLExpr::Gte(l, r) => self.is_free_in(var, l, false) || self.is_free_in(var, r, false),
47
48            TLExpr::TNorm { left, right, .. } | TLExpr::TCoNorm { left, right, .. } => {
49                self.is_free_in(var, left, false) || self.is_free_in(var, right, false)
50            }
51
52            TLExpr::FuzzyImplication {
53                premise,
54                conclusion,
55                ..
56            } => self.is_free_in(var, premise, false) || self.is_free_in(var, conclusion, false),
57
58            TLExpr::Not(e)
59            | TLExpr::Score(e)
60            | TLExpr::Abs(e)
61            | TLExpr::Floor(e)
62            | TLExpr::Ceil(e)
63            | TLExpr::Round(e)
64            | TLExpr::Sqrt(e)
65            | TLExpr::Exp(e)
66            | TLExpr::Log(e)
67            | TLExpr::Sin(e)
68            | TLExpr::Cos(e)
69            | TLExpr::Tan(e)
70            | TLExpr::Box(e)
71            | TLExpr::Diamond(e)
72            | TLExpr::Next(e)
73            | TLExpr::Eventually(e)
74            | TLExpr::Always(e) => self.is_free_in(var, e, false),
75
76            TLExpr::FuzzyNot { expr, .. } => self.is_free_in(var, expr, false),
77
78            TLExpr::WeightedRule { rule, .. } => self.is_free_in(var, rule, false),
79
80            TLExpr::Until { before, after }
81            | TLExpr::Release {
82                released: before,
83                releaser: after,
84            }
85            | TLExpr::WeakUntil { before, after }
86            | TLExpr::StrongRelease {
87                released: before,
88                releaser: after,
89            } => self.is_free_in(var, before, false) || self.is_free_in(var, after, false),
90
91            TLExpr::Exists {
92                var: binder, body, ..
93            }
94            | TLExpr::ForAll {
95                var: binder, body, ..
96            }
97            | TLExpr::SoftExists {
98                var: binder, body, ..
99            }
100            | TLExpr::SoftForAll {
101                var: binder, body, ..
102            } => self.is_free_in(var, body, binder == var),
103
104            TLExpr::Aggregate {
105                var: binder,
106                body,
107                group_by,
108                ..
109            } => {
110                let in_body = self.is_free_in(var, body, binder == var);
111                let in_group = group_by
112                    .as_ref()
113                    .map(|gs| gs.iter().any(|g| g == var))
114                    .unwrap_or(false);
115                in_body || in_group
116            }
117
118            TLExpr::Let {
119                var: binder,
120                value,
121                body,
122            } => self.is_free_in(var, value, false) || self.is_free_in(var, body, binder == var),
123
124            TLExpr::Lambda {
125                var: binder, body, ..
126            } => self.is_free_in(var, body, binder == var),
127
128            TLExpr::Apply { function, argument } => {
129                self.is_free_in(var, function, false) || self.is_free_in(var, argument, false)
130            }
131
132            TLExpr::SetMembership { element, set }
133            | TLExpr::SetUnion {
134                left: element,
135                right: set,
136            }
137            | TLExpr::SetIntersection {
138                left: element,
139                right: set,
140            }
141            | TLExpr::SetDifference {
142                left: element,
143                right: set,
144            } => self.is_free_in(var, element, false) || self.is_free_in(var, set, false),
145
146            TLExpr::SetCardinality { set } => self.is_free_in(var, set, false),
147
148            TLExpr::SetComprehension {
149                var: binder,
150                condition,
151                ..
152            } => self.is_free_in(var, condition, binder == var),
153
154            TLExpr::CountingExists {
155                var: binder, body, ..
156            }
157            | TLExpr::CountingForAll {
158                var: binder, body, ..
159            }
160            | TLExpr::ExactCount {
161                var: binder, body, ..
162            }
163            | TLExpr::Majority {
164                var: binder, body, ..
165            } => self.is_free_in(var, body, binder == var),
166
167            TLExpr::LeastFixpoint { var: binder, body }
168            | TLExpr::GreatestFixpoint { var: binder, body } => {
169                self.is_free_in(var, body, binder == var)
170            }
171
172            TLExpr::At { formula, .. } => self.is_free_in(var, formula, false),
173            TLExpr::Somewhere { formula } | TLExpr::Everywhere { formula } => {
174                self.is_free_in(var, formula, false)
175            }
176
177            TLExpr::Explain { formula } => self.is_free_in(var, formula, false),
178
179            TLExpr::AllDifferent { variables } => variables.iter().any(|v| v == var),
180
181            TLExpr::GlobalCardinality {
182                variables, values, ..
183            } => {
184                variables.iter().any(|v| v == var)
185                    || values.iter().any(|e| self.is_free_in(var, e, false))
186            }
187
188            TLExpr::ProbabilisticChoice { alternatives } => alternatives
189                .iter()
190                .any(|(_, e)| self.is_free_in(var, e, false)),
191
192            TLExpr::IfThenElse {
193                condition,
194                then_branch,
195                else_branch,
196            } => {
197                self.is_free_in(var, condition, false)
198                    || self.is_free_in(var, then_branch, false)
199                    || self.is_free_in(var, else_branch, false)
200            }
201
202            TLExpr::Constant(_)
203            | TLExpr::EmptySet
204            | TLExpr::Nominal { .. }
205            | TLExpr::Abducible { .. }
206            | TLExpr::SymbolLiteral(_) => false,
207
208            TLExpr::Match { scrutinee, arms } => {
209                self.is_free_in(var, scrutinee, false)
210                    || arms.iter().any(|(_, b)| self.is_free_in(var, b, false))
211            }
212        }
213    }
214}
tensorlogic_compiler/dead_code/free_vars.rs

tensorlogic_compiler/dead_code/
free_vars.rs
