meta_language/translation/ir/
rename.rs

1//! Capture-avoiding renaming and traversal helpers over checked expressions and propositions.
2
3use super::{
4    BTreeSet, Binder, Case, Comparison, Effect, Env, Expr, FnDecl, Hints, Main, Node, Param,
5    Pattern, Plan, PlanCase, Prop, Scope, Split, TheoremDecl,
6};
7
8/// Renames every binder in an expression; `env` maps source names to target names.
9///
10/// # Panics
11/// On a variable the environment does not bind, which a checked program never has.
12pub fn rename_expr(expr: &Expr, env: &Env, scope: &mut Scope<'_>) -> Expr {
13    match &expr.node {
14        Node::Var { name } => {
15            let renamed = env
16                .get(name)
17                .unwrap_or_else(|| panic!("unbound variable {name}"));
18            Expr {
19                node: Node::Var {
20                    name: renamed.clone(),
21                },
22                ..expr.clone()
23            }
24        }
25        Node::Let { name, value, body } => {
26            let value = rename_expr(value, env, scope);
27            let fresh = scope.fresh(name);
28            let mut inner = env.clone();
29            inner.insert(name.clone(), fresh.clone());
30            let body = rename_expr(body, &inner, scope);
31            Expr {
32                node: Node::Let {
33                    name: fresh,
34                    value: Box::new(value),
35                    body: Box::new(body),
36                },
37                ..expr.clone()
38            }
39        }
40        Node::Match { scrutinee, cases } => {
41            let scrutinee = rename_expr(scrutinee, env, scope);
42            let cases = cases
43                .iter()
44                .map(|kase| {
45                    let mut inner = env.clone();
46                    let pattern = match &kase.pattern {
47                        Pattern::NatSucc { name } => {
48                            let fresh = scope.fresh(name);
49                            inner.insert(name.clone(), fresh.clone());
50                            Pattern::NatSucc { name: fresh }
51                        }
52                        Pattern::Bind { name } => {
53                            let fresh = scope.fresh(name);
54                            inner.insert(name.clone(), fresh.clone());
55                            Pattern::Bind { name: fresh }
56                        }
57                        Pattern::Ctor { data, ctor, binds } => Pattern::Ctor {
58                            data: data.clone(),
59                            ctor: ctor.clone(),
60                            binds: binds
61                                .iter()
62                                .map(|bind| {
63                                    bind.as_ref().map(|bind| {
64                                        let fresh = scope.fresh(bind);
65                                        inner.insert(bind.clone(), fresh.clone());
66                                        fresh
67                                    })
68                                })
69                                .collect(),
70                        },
71                        other => other.clone(),
72                    };
73                    Case {
74                        pattern,
75                        body: rename_expr(&kase.body, &inner, scope),
76                    }
77                })
78                .collect();
79            Expr {
80                node: Node::Match {
81                    scrutinee: Box::new(scrutinee),
82                    cases,
83                },
84                ..expr.clone()
85            }
86        }
87        _ => expr.map_children(&mut |child| rename_expr(child, env, scope)),
88    }
89}
90
91pub fn rename_prop(prop: &Prop, env: &Env, scope: &mut Scope<'_>) -> Prop {
92    let both = |left: &Prop, right: &Prop, scope: &mut Scope<'_>| {
93        let left = rename_prop(left, env, scope);
94        (Box::new(left), Box::new(rename_prop(right, env, scope)))
95    };
96    match prop {
97        Prop::Forall { binders, body } => {
98            let mut inner = env.clone();
99            let binders = binders
100                .iter()
101                .map(|binder| {
102                    let name = scope.fresh(&binder.name);
103                    inner.insert(binder.name.clone(), name.clone());
104                    Binder {
105                        name,
106                        ty: binder.ty.clone(),
107                    }
108                })
109                .collect();
110            Prop::Forall {
111                binders,
112                body: Box::new(rename_prop(body, &inner, scope)),
113            }
114        }
115        Prop::And { left, right } => {
116            let (left, right) = both(left, right, scope);
117            Prop::And { left, right }
118        }
119        Prop::Or { left, right } => {
120            let (left, right) = both(left, right, scope);
121            Prop::Or { left, right }
122        }
123        Prop::Implies { left, right } => {
124            let (left, right) = both(left, right, scope);
125            Prop::Implies { left, right }
126        }
127        Prop::Not { arg } => Prop::Not {
128            arg: Box::new(rename_prop(arg, env, scope)),
129        },
130        Prop::Bool { expr } => Prop::Bool {
131            expr: rename_expr(expr, env, scope),
132        },
133        other => {
134            let (op, comparison) = other.comparison().expect("comparison");
135            let left = rename_expr(&comparison.left, env, scope);
136            let right = rename_expr(&comparison.right, env, scope);
137            Prop::compare(
138                op,
139                Comparison {
140                    left,
141                    right,
142                    domain: comparison.domain.clone(),
143                    same_value: comparison.same_value,
144                },
145            )
146        }
147    }
148}
149
150/// Whether a function lifted from a loop calls itself only in tail position.
151///
152/// An emitter can then print those calls as the next iteration of a loop, so
153/// a loop of a million iterations needs no million stack frames.
154#[must_use]
155pub fn tail_loop(entry: &FnDecl) -> bool {
156    entry.generated && entry.recursive && tail_calls_only(&entry.body, &entry.full_name, true)
157}
158
159fn tail_calls_only(expr: &Expr, name: &str, tail: bool) -> bool {
160    match &expr.node {
161        Node::Call { func, args } => {
162            (tail || func != name) && args.iter().all(|arg| tail_calls_only(arg, name, false))
163        }
164        Node::If {
165            cond,
166            then,
167            otherwise,
168        } => {
169            tail_calls_only(cond, name, false)
170                && tail_calls_only(then, name, tail)
171                && tail_calls_only(otherwise, name, tail)
172        }
173        Node::Let { value, body, .. } => {
174            tail_calls_only(value, name, false) && tail_calls_only(body, name, tail)
175        }
176        Node::Print { text, body } => {
177            tail_calls_only(text, name, false) && tail_calls_only(body, name, tail)
178        }
179        Node::Match { scrutinee, cases } => {
180            tail_calls_only(scrutinee, name, false)
181                && cases
182                    .iter()
183                    .all(|kase| tail_calls_only(&kase.body, name, tail))
184        }
185        _ => expr
186            .children()
187            .into_iter()
188            .all(|child| tail_calls_only(child, name, false)),
189    }
190}
191
192/// A function's parameters and body with target local names.
193pub fn rename_function(
194    entry: &FnDecl,
195    ident: &dyn Fn(&str) -> String,
196    reserved: &BTreeSet<String>,
197) -> (Vec<Param>, Expr) {
198    let mut scope = Scope::new(ident, reserved);
199    let mut env = Env::new();
200    let params = entry
201        .params
202        .iter()
203        .map(|param| {
204            let name = scope.fresh(&param.name);
205            env.insert(param.name.clone(), name.clone());
206            Param {
207                name,
208                ..param.clone()
209            }
210        })
211        .collect();
212    let body = rename_expr(&entry.body, &env, &mut scope);
213    (params, body)
214}
215
216/// A theorem's binders, proposition and proof plan with target local names.
217pub fn rename_theorem(
218    entry: &TheoremDecl,
219    ident: &dyn Fn(&str) -> String,
220    reserved: &BTreeSet<String>,
221) -> (Vec<Binder>, Prop, Plan) {
222    let mut scope = Scope::new(ident, reserved);
223    let mut env = Env::new();
224    let binders = entry
225        .binders
226        .iter()
227        .map(|binder| {
228            let name = scope.fresh(&binder.name);
229            env.insert(binder.name.clone(), name.clone());
230            Binder {
231                name,
232                ty: binder.ty.clone(),
233            }
234        })
235        .collect();
236    let prop = rename_prop(&entry.prop, &env, &mut scope.child());
237    let plan = rename_plan(&entry.proof.plan, &env, &scope);
238    (binders, prop, plan)
239}
240
241pub(super) fn rename_plan(plan: &Plan, env: &Env, scope: &Scope<'_>) -> Plan {
242    let split = match plan {
243        Plan::Close { hints } => {
244            return Plan::Close {
245                hints: Hints {
246                    hyps: hints
247                        .hyps
248                        .iter()
249                        .map(|name| env.get(name).unwrap_or(name).clone())
250                        .collect(),
251                    ..hints.clone()
252                },
253            };
254        }
255        Plan::Induction(split) | Plan::Cases(split) => split,
256    };
257    let renamed = Split {
258        // A split variable is always a theorem binder, so the environment names it.
259        variable: env.get(&split.variable).cloned().unwrap_or_default(),
260        ty: split.ty.clone(),
261        cases: split
262            .cases
263            .iter()
264            .map(|kase| {
265                let mut inner = env.clone();
266                let mut case_scope = scope.child();
267                let mut rename = |name: &String| {
268                    let fresh = case_scope.fresh(name);
269                    inner.insert(name.clone(), fresh.clone());
270                    fresh
271                };
272                let fields = kase.fields.iter().map(&mut rename).collect();
273                let ihs = kase.ihs.iter().map(&mut rename).collect();
274                PlanCase {
275                    ctor: kase.ctor.clone(),
276                    fields,
277                    ihs,
278                    recursive: kase.recursive.clone(),
279                    plan: rename_plan(&kase.plan, &inner, &case_scope),
280                }
281            })
282            .collect(),
283    };
284    match plan {
285        Plan::Induction(_) => Plan::Induction(renamed),
286        _ => Plan::Cases(renamed),
287    }
288}
289
290/// The main effects with target local names.
291pub fn rename_main(
292    main: &Main,
293    ident: &dyn Fn(&str) -> String,
294    reserved: &BTreeSet<String>,
295) -> Vec<Effect> {
296    let mut scope = Scope::new(ident, reserved);
297    let mut env = Env::new();
298    main.effects
299        .iter()
300        .map(|effect| match effect {
301            Effect::Let {
302                name,
303                value,
304                constant,
305                span,
306            } => {
307                let value = rename_expr(value, &env, &mut scope);
308                let fresh = scope.fresh(name);
309                env.insert(name.clone(), fresh.clone());
310                Effect::Let {
311                    name: fresh,
312                    value,
313                    constant: *constant,
314                    span: *span,
315                }
316            }
317            Effect::Unwrap {
318                name,
319                pair,
320                data,
321                ctors,
322                ty,
323                span,
324            } => {
325                let pair = rename_expr(pair, &env, &mut scope);
326                let fresh = scope.fresh(name);
327                env.insert(name.clone(), fresh.clone());
328                Effect::Unwrap {
329                    name: fresh,
330                    pair,
331                    data: data.clone(),
332                    ctors: ctors.clone(),
333                    ty: ty.clone(),
334                    span: *span,
335                }
336            }
337            Effect::Print { expr, span } => Effect::Print {
338                expr: rename_expr(expr, &env, &mut scope),
339                span: *span,
340            },
341            Effect::Assert { prop, span } => Effect::Assert {
342                prop: rename_prop(prop, &env, &mut scope),
343                span: *span,
344            },
345            Effect::Output { expr, span } => Effect::Output {
346                expr: rename_expr(expr, &env, &mut scope),
347                span: *span,
348            },
349        })
350        .collect()
351}
352
353/// True when any expression of the given kind occurs in the tree.
354#[must_use]
355pub fn contains_kind(expr: &Expr, kind: &str) -> bool {
356    expr.kind() == kind
357        || expr
358            .children()
359            .into_iter()
360            .any(|child| contains_kind(child, kind))
361}
362
363/// True when any expression of the given kind occurs in the proposition.
364#[must_use]
365pub fn prop_contains_kind(prop: &Prop, kind: &str) -> bool {
366    prop_exprs(prop)
367        .into_iter()
368        .any(|expr| contains_kind(expr, kind))
369}
370
371/// The expressions of a proposition, left to right.
372#[must_use]
373pub fn prop_exprs(prop: &Prop) -> Vec<&Expr> {
374    match prop {
375        Prop::Forall { body, .. } => prop_exprs(body),
376        Prop::And { left, right } | Prop::Or { left, right } | Prop::Implies { left, right } => {
377            let mut exprs = prop_exprs(left);
378            exprs.extend(prop_exprs(right));
379            exprs
380        }
381        Prop::Not { arg } => prop_exprs(arg),
382        Prop::Bool { expr } => vec![expr],
383        other => {
384            let (_, comparison) = other.comparison().expect("comparison");
385            vec![&comparison.left, &comparison.right]
386        }
387    }
388}
meta_language/translation/ir/rename.rs

meta_language/translation/ir/
rename.rs
