Struct Context 

pub struct Context { /* private fields */ }

Type checking context.

Implementations

impl Context

pub fn new() -> Self

Create a new empty context.

pub fn with_start_fvar(start: u64) -> Self

Create with a starting fvar id (to avoid conflicts).

pub fn fresh_fvar(&mut self) -> FVarId

Generate a fresh free variable ID.

pub fn push_local(&mut self, name: Name, ty: Expr, val: Option<Expr>) -> FVarId

Push a local variable declaration (without value).

pub fn push_local_with_binder( &mut self, name: Name, binder_info: BinderInfo, ty: Expr, val: Option<Expr>, ) -> FVarId

Push a local variable declaration with binder info.

pub fn mk_local_decl( &mut self, name: Name, binder_info: BinderInfo, ty: Expr, ) -> Expr

Create a local declaration and return the free variable expression.

pub fn mk_let_decl(&mut self, name: Name, ty: Expr, val: Expr) -> Expr

Create a let declaration and return the free variable expression.

pub fn pop_local(&mut self) -> Option<LocalVar>

Pop the last local variable from the context.

pub fn save(&self) -> ContextSnapshot

Save the current state as a snapshot.

pub fn restore(&mut self, snapshot: &ContextSnapshot)

Restore to a previous snapshot.

pub fn get_local(&self, fvar: FVarId) -> Option<&LocalVar>

Get a local variable by free variable ID.

pub fn get_type(&self, fvar: FVarId) -> Option<&Expr>

Get the type of a free variable.

pub fn get_value(&self, fvar: FVarId) -> Option<&Expr>

Get the value of a let-bound free variable.

pub fn is_let(&self, fvar: FVarId) -> bool

Check if a free variable is a let-binding.

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

Get a local variable by name (searches from innermost to outermost).

pub fn num_locals(&self) -> usize

Get the number of local variables.

pub fn is_empty(&self) -> bool

Check if the context is empty.

pub fn all_locals(&self) -> &[LocalVar]

Get all local variables.

pub fn get_fvars(&self) -> Vec<Expr>

Get all free variable expressions in the context.

pub fn mk_lambda(&self, fvars: &[FVarId], body: Expr) -> Expr

Build a lambda abstraction from the context’s free variables.

Given free variables [x₁, x₂, ..., xₙ] in the context, builds λ (x₁ : τ₁) (x₂ : τ₂) ... (xₙ : τₙ), body where body has all free variables replaced by bound variables.

pub fn mk_pi(&self, fvars: &[FVarId], body: Expr) -> Expr

Build a Pi/forall type from the context’s free variables.

Given free variables [x₁, x₂, ..., xₙ], builds ∀ (x₁ : τ₁) (x₂ : τ₂) ... (xₙ : τₙ), body

pub fn clear(&mut self)

Clear the context.

pub fn with_local<F, R>(&mut self, name: Name, ty: Expr, f: F) -> R

where F: FnOnce(&mut Self, FVarId) -> R,

Execute a function with a temporary local declaration.

The local is automatically popped when the function returns.

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() -> Self

Returns the “default value” for a type.