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::{ctx::TransformPass, TransformCtx};
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 VisitAstMut for UnbindVarVisitor {
18    fn enter_region_binder<T: AstVisitable>(&mut self, _: &mut RegionBinder<T>) {
19        self.binder_depth = self.binder_depth.incr()
20    }
21    fn exit_region_binder<T: AstVisitable>(&mut self, _: &mut RegionBinder<T>) {
22        self.binder_depth = self.binder_depth.decr()
23    }
24    fn enter_binder<T: AstVisitable>(&mut self, _: &mut Binder<T>) {
25        self.binder_depth = self.binder_depth.incr()
26    }
27    fn exit_binder<T: AstVisitable>(&mut self, _: &mut Binder<T>) {
28        self.binder_depth = self.binder_depth.decr()
29    }
30
31    fn exit_de_bruijn_var<T: AstVisitable + Idx>(&mut self, var: &mut DeBruijnVar<T>) {
32        match var {
33            DeBruijnVar::Bound(dbid, varid) if *dbid == self.binder_depth => {
34                *var = DeBruijnVar::Free(*varid)
35            }
36            DeBruijnVar::Bound(..) => {}
37            DeBruijnVar::Free(_) => unreachable!("Found unexpected free variable"),
38        }
39    }
40}
41
42pub struct Check;
43impl TransformPass for Check {
44    fn transform_ctx(&self, ctx: &mut TransformCtx) {
45        let mut visitor = UnbindVarVisitor::default();
46        for mut item in ctx.translated.all_items_mut() {
47            let _ = item.drive_mut(&mut visitor);
48        }
49    }
50}
charon_lib/transform/unbind_item_vars.rs

charon_lib/transform/
unbind_item_vars.rs
