Struct LocalVarEnv 

pub(crate) struct LocalVarEnv {
    local_var_gen: IndexGen<LocalVar>,
    fvars: UnordMap<Name, LocalVar>,
    layers: Vec<Vec<LocalVar>>,
    pub(crate) reverse_map: UnordMap<LocalVar, Expr>,
    pretty_var_map: PrettyMap<LocalVar>,
}

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.

pretty_var_map: PrettyMap<LocalVar>

Implementations

impl LocalVarEnv

fn new() -> Self

pub(crate) fn fresh_name(&mut self) -> LocalVar

fn insert_fvar_map( &mut self, name: Name, provenance: NameProvenance, ) -> 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 push_layer(&mut self, layer: Vec<LocalVar>)

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>