Struct LocalVarEnv 

struct LocalVarEnv {
    local_var_gen: IndexGen<LocalVar>,
    fvars: UnordMap<Name, LocalVar>,
    layers: Vec<Vec<LocalVar>>,
    reverse_map: UnordMap<LocalVar, Expr>,
}

Environment used to map from rty::Var to a fixpoint::LocalVar.

Fields

local_var_gen: IndexGen<LocalVar>

fvars: UnordMap<Name, LocalVar>

layers: Vec<Vec<LocalVar>>

Layers of late bound variables

reverse_map: UnordMap<LocalVar, Expr>

While it might seem like the signature should be UnordMap<fixpoint::LocalVar, rty::Var>, we encode the arguments to kvars (which can be arbitrary expressions) as local variables; thus we need to keep the output as an rty::Expr to reflect this.

Implementations

impl LocalVarEnv

fn new() -> Self

fn fresh_name(&mut self) -> LocalVar

fn insert_fvar_map(&mut self, name: Name) -> LocalVar

fn remove_fvar_map(&mut self, name: Name)

fn push_layer_with_fresh_names(&mut self, count: usize)

Push a layer of bound variables assigning a fresh fixpoint::LocalVar to each one

fn pop_layer(&mut self) -> Vec<LocalVar>

fn get_fvar(&self, name: Name) -> Option<LocalVar>

fn get_late_bvar( &self, debruijn: DebruijnIndex, var: BoundVar, ) -> Option<LocalVar>