Struct Context 

pub struct Context {
    pub env: Env,
    pub scope: Vec<VarInContext>,
    pub fiber_env: FiberEnv,
    pub fiber_scope: Vec<FiberVarInContext>,
}

The variable context during elaboration.

Carries two scopes: the base context (env/scope) of ordinary terms typed by BaseTyV, and a separate fiber context (fiber_env/fiber_scope) of instance generators and sub-instance imports typed by FiberTyV. The fiber scope is populated only while elaborating an instance body; the two never alias, so neither lookup can see the other’s variables. See crate::tt::toplevel for why the two worlds are distinct.

Fields

env: Env

Stores the value of each of the base variables in context.

scope: Vec<VarInContext>

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

fiber_env: FiberEnv

Stores the value of each fiber variable in context.

fiber_scope: Vec<FiberVarInContext>

Stores the names and fiber types of each fiber variable in context.

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<BaseTyV>, )

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

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

Lookup a base variable by name.

pub fn push_fiber(&mut self, name: VarName, label: LabelSegment, ty: FiberTyV)

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

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

Lookup a fiber variable by name.

Trait Implementations

impl Default for Context

fn default() -> Self

Returns the “default value” for a type.