Enum Expr 

pub enum Expr {
    Sort(Level),
    BVar(u32),
    FVar(FVarId),
    Const(Name, Vec<Level>),
    App(Node, Node),
    Lam(BinderInfo, Name, Node, Node),
    Pi(BinderInfo, Name, Node, Node),
    Let(Name, Node, Node, Node),
    Lit(Literal),
    Proj(Name, u32, Node),
}

Core expression type.

This is the heart of the kernel. All terms in the type theory are represented as Expr values.

Sub-expressions are held behind Nodes (structural sharing, wave5): an export DAG id referenced by many parents materializes to a single shared node, and clone is an O(1) refcount bump rather than a deep copy. The kernel is single-threaded (the verify pipeline runs on one spawned thread and the wasm target is single-threaded), so the sharing is by Rc — not Arc.

Clone is implemented by hand (not derived) so each clone charges one unit of the deterministic per-declaration resource fuel — see crate::fuel. A clone copies this one node and shares its children (the sub-clones are refcount bumps), so the unit is for the call, not for the size of the term; the walks that build new terms charge for the subterms they reach.

Hash is implemented by hand too: it writes the term’s structural hash, one 64-bit value computed from the hashes the children cache, where the derived implementation walked the whole term. PartialEq is derived; the children compare through Node’s equality, which consults the cached hashes first.

Variants

Sort(Level)

Sort u — universe.

Prop is Sort(Level::Zero). Type is Sort(Level::Succ(Level::Zero)).

BVar(u32)

Bound variable (de Bruijn index, 0-based).

BVar(0) refers to the innermost binder. BVar(n) refers to the n-th enclosing binder.

FVar(FVarId)

Free variable (locally nameless).

Used during type checking to represent local hypotheses.

Const(Name, Vec<Level>)

Named constant with universe level instantiation.

Const(name, levels) represents a global constant with its universe parameters instantiated.

App(Node, Node)

Function application: f a.

Application is always binary. f a b is App(App(f, a), b).

Lam(BinderInfo, Name, Node, Node)

Lambda abstraction: λ (x : type), body.

Pi(BinderInfo, Name, Node, Node)

Dependent function type: Π (x : type), body.

Non-dependent arrows A → B are represented as Pi(Default, _, A, B) where the body doesn’t use BVar(0).

Let(Name, Node, Node, Node)

Let binding: let x : type := val in body.

Lit(Literal)

Literal value (Nat or String).

Proj(Name, u32, Node)

Structure projection: projName.idx struct.

Implementations

impl Expr

pub fn range(&self) -> u32

This node’s looseBVarRange — 1 + the largest loose de Bruijn index, or 0 if closed. O(1): it reads the immediate children’s cached ranges (see Node) and combines them, accounting for the binders each child sits under.

pub fn rebuild_cost(&self) -> u32

The size of this term counted as a TREE — a shared subterm once per path to it — O(1) from the children’s cached sizes: one unit per node and one more per leaf, so cost(leaf) = 2 and cost(internal) = 1 + Σ cost(children), saturating at REBUILD_COST_MAX. It is what rebuilding the term node by node, with no sharing, would cost; the caches read it to keep giant terms out.

impl Expr

pub fn is_sort(&self) -> bool

Check if this is a Sort.

pub fn is_prop(&self) -> bool

Check if this is Prop.

pub fn is_bvar(&self) -> bool

Check if this is a bound variable.

pub fn is_fvar(&self) -> bool

Check if this is a free variable.

pub fn is_app(&self) -> bool

Check if this is an application.

pub fn is_lambda(&self) -> bool

Check if this is a lambda.

pub fn is_pi(&self) -> bool

Check if this is a Pi type.

impl Expr

pub fn is_let(&self) -> bool

Check if this expression is a let binding.

pub fn is_lit(&self) -> bool

Check if this expression is a literal.

pub fn is_const(&self) -> bool

Check if this expression is a named constant.

pub fn is_proj(&self) -> bool

Check if this expression is a projection.

pub fn is_atom(&self) -> bool

Check if this expression is an “atom” (cannot be further reduced without context): Sort, BVar, FVar, Const, Lit.

pub fn as_bvar(&self) -> Option<u32>

Extract the bound variable index, or None.

pub fn as_fvar(&self) -> Option<FVarId>

Extract the free variable ID, or None.

pub fn as_const_name(&self) -> Option<&Name>

Extract the constant name, or None.

pub fn as_sort_level(&self) -> Option<&Level>

Extract the sort level, or None.

pub fn app_head_args(&self) -> (&Expr, Vec<&Expr>)

Return the head and argument list of an application spine.

For f a b c, returns (&f, [&a, &b, &c]).

pub fn app_arity(&self) -> usize

Return the number of arguments in an application spine.

pub fn pi_arity(&self) -> usize

Count the number of leading Pi binders.

pub fn lam_arity(&self) -> usize

Count the number of leading Lambda binders.

pub fn size(&self) -> usize

Compute the AST size (total number of nodes).

pub fn ast_depth(&self) -> usize

Compute the AST depth (longest path to a leaf).

pub fn mk_app_many(self, args: &[Expr]) -> Expr

Apply this expression to a list of arguments.

e.mk_app_many(&[a, b, c]) returns ((e a) b) c.

pub fn has_loose_bvar_at(&self, d: u32) -> bool

Check if this expression has any loose bound variables at depth d.

pub fn count_bvar_occurrences(&self, idx: u32) -> usize

Count occurrences of bound variable BVar(idx) in this expression.

pub fn is_closed(&self) -> bool

Check if this expression is closed (no loose bound variables).

pub fn free_vars(&self) -> HashSet<FVarId>

Collect all free variable IDs occurring in this expression.

pub fn constants(&self) -> HashSet<Name>

Collect all constant names occurring in this expression.

Trait Implementations

impl AsRef<Expr> for Node

fn as_ref(&self) -> &Expr

Converts this type into a shared reference of the (usually inferred) input type.

impl Borrow<Expr> for Node

fn borrow(&self) -> &Expr

Immutably borrows from an owned value.

impl Clone for Expr

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Expr

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

Formats the value using the given formatter.

impl Display for Expr

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

Formats the value using the given formatter.

impl Eq for Expr

impl Hash for Expr

fn hash<H: Hasher>(&self, state: &mut H)

Writes the term’s structural hash — one 64-bit value, O(1) in the size of the term. Consistent with the derived PartialEq: the hash covers exactly the fields equality compares.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for Expr

fn eq(&self, other: &Self) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for Expr