Struct Context 

pub struct Context { /* private fields */ }

Local typing context

Uses de Bruijn indices: variable #0 is the most recently bound, #1 is the one before that, etc.

Implementations

impl Context

pub fn new() -> Self

Create a new empty context

pub fn push(&mut self, entry: ContextEntry)

Push a new binding onto the context

pub fn push_var(&mut self, name: SymbolId, ty: TermId)

Push a simple variable binding

pub fn pop(&mut self) -> Option<ContextEntry>

Pop the most recent binding

pub fn len(&self) -> usize

Get the number of entries in the context

pub fn is_empty(&self) -> bool

Check if the context is empty

pub fn lookup(&self, index: u32) -> Option<&ContextEntry>

Look up a variable by de Bruijn index

Index 0 refers to the most recently bound variable

pub fn type_of(&self, index: u32) -> Option<TermId>

Get the type of a variable by de Bruijn index

pub fn value_of(&self, index: u32) -> Option<TermId>

Get the value of a variable (if it’s a let binding)

pub fn extend(&mut self, entries: impl IntoIterator<Item = ContextEntry>)

Extend the context with multiple entries

pub fn with_entries( &self, entries: impl IntoIterator<Item = ContextEntry>, ) -> Self

Create a new context by extending this one

pub fn entries(&self) -> &[ContextEntry]

Get all entries (for iteration)

pub fn clear(&mut self)

Clear the context

pub fn truncate(&mut self, len: usize)

Truncate the context to a specific length

pub fn mark(&self) -> usize

Save the current context length (for later restoration)

pub fn restore(&mut self, mark: usize)

Restore context to a previous mark

Trait Implementations

impl Clone for Context

fn clone(&self) -> Context

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Context

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for Context

fn default() -> Context

Returns the “default value” for a type.