Struct Context

pub struct Context {
    pub env: Env,
    pub scope: Vec<VarInContext>,
}

The variable context during elaboration

Fields

env: Env

Stores the value of each of the variables in context

scope: Vec<VarInContext>

Stores the names and types of each of the variables in context.

We allow the type to be “none” as a hack for the self variable before we know the type of the self variable.

Implementations

impl Context

pub fn new() -> Self

Create an empty context.

pub fn checkpoint(&self) -> ContextCheckpoint

Create a checkpoint from the current state of the context.

pub fn reset_to(&mut self, c: ContextCheckpoint)

Reset the context to a previously-saved checkpoint.

pub fn push_scope( &mut self, name: VarName, label: LabelSegment, ty: Option<TyV>, )

Add a new variable to scope (note: does not add it to the environment)

pub fn lookup( &self, name: VarName, ) -> Option<(BwdIdx, LabelSegment, Option<TyV>)>

Lookup a variable by name

Trait Implementations

impl Default for Context

fn default() -> Self

Returns the “default value” for a type.