charon_lib/transform/
unbind_item_vars.rs

1//! Replace variables bound at the top-level with `Free` vars. This is for convenience for
2//! consumers of the charon ast.
3use derive_generic_visitor::*;
4use index_vec::Idx;
5
6use crate::ast::*;
7
8use super::{TransformCtx, ctx::TransformPass};
9
10/// Replace variables bound at the top-level with `Free` vars.
11#[derive(Default, Visitor)]
12pub(crate) struct UnbindVarVisitor {
13    // Tracks the depth of binders we're inside of.
14    binder_depth: DeBruijnId,
15}
16
17impl VisitorWithBinderDepth for UnbindVarVisitor {
18    fn binder_depth_mut(&mut self) -> &mut DeBruijnId {
19        &mut self.binder_depth
20    }
21}
22impl VisitAstMut for UnbindVarVisitor {
23    fn visit<'a, T: AstVisitable>(&'a mut self, x: &mut T) -> ControlFlow<Self::Break> {
24        VisitWithBinderDepth::new(self).visit(x)
25    }
26
27    fn exit_de_bruijn_var<T: AstVisitable + Idx>(&mut self, var: &mut DeBruijnVar<T>) {
28        match var {
29            DeBruijnVar::Bound(dbid, varid) if *dbid == self.binder_depth => {
30                *var = DeBruijnVar::Free(*varid)
31            }
32            DeBruijnVar::Bound(..) => {}
33            DeBruijnVar::Free(_) => unreachable!("Found unexpected free variable"),
34        }
35    }
36}
37
38pub struct Check;
39impl TransformPass for Check {
40    fn transform_ctx(&self, ctx: &mut TransformCtx) {
41        let mut visitor = UnbindVarVisitor::default();
42        for mut item in ctx.translated.all_items_mut() {
43            let _ = item.drive_mut(&mut visitor);
44        }
45    }
46}
charon_lib/transform/unbind_item_vars.rs

charon_lib/transform/
unbind_item_vars.rs
