Enum Expr 

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

Core expression type.

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

We use Box for sub-expressions for simplicity in Phase 0. In later phases, these will be Idx<Expr> pointing into an arena.

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(Box<Expr>, Box<Expr>)

Function application: f a.

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

Lam(BinderInfo, Name, Box<Expr>, Box<Expr>)

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

Pi(BinderInfo, Name, Box<Expr>, Box<Expr>)

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, Box<Expr>, Box<Expr>, Box<Expr>)

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

Lit(Literal)

Literal value (Nat or String).

Proj(Name, u32, Box<Expr>)

Structure projection: projName.idx struct.

Implementations

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 Clone for Expr

fn clone(&self) -> Expr

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 Hash for Expr

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

Feeds this value into the given Hasher.

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: &Expr) -> bool

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for Expr

impl StructuralPartialEq for Expr