Enum Node 

pub enum Node {
    Sort(LevelId),
    Var(Symbol),
    Global(Symbol),
    Const {
        name: Symbol,
        levels: Box<[LevelId]>,
    },
    Pi {
        param: Symbol,
        param_type: TermId,
        body_type: TermId,
    },
    Lambda {
        param: Symbol,
        param_type: TermId,
        body: TermId,
    },
    App(TermId, TermId),
    Match {
        discriminant: TermId,
        motive: TermId,
        cases: Box<[TermId]>,
    },
    Fix {
        name: Symbol,
        body: TermId,
    },
    MutualFix {
        defs: Box<[(Symbol, TermId)]>,
        index: usize,
    },
    Let {
        name: Symbol,
        ty: TermId,
        value: TermId,
        body: TermId,
    },
    Lit(LitId),
    Hole,
    Bound(u32),
}

One term node with its children replaced by handles — the flat shape that makes the store a DAG rather than a tree.

The match arms below mirror Term’s thirteen kernel variants ONE FOR ONE, and every match over Node in this file is wildcard-free on purpose: a new Term variant must answer here rather than slip past under a _. Term::Annotated has no node: the store keys on the erased term, so an annotated term interns to its term’s node.

Variants

Sort(LevelId)

Term::Sort.

Var(Symbol)

Term::Var.

Global(Symbol)

Term::Global.

Const

Term::Const.

Fields

name: Symbol

The declaration name.

levels: Box<[LevelId]>

The explicit universe arguments.

Pi

Term::Pi.

Fields

param: Symbol

The bound name.

param_type: TermId

The domain.

body_type: TermId

The codomain, in which param is bound.

Lambda

Term::Lambda.

Fields

param: Symbol

The bound name.

param_type: TermId

The domain.

body: TermId

The body, in which param is bound.

App(TermId, TermId)

Term::App.

Match

Term::Match.

Fields

discriminant: TermId

The scrutinee.

motive: TermId

The return-type motive.

cases: Box<[TermId]>

One branch per constructor, in declaration order.

Fix

Term::Fix.

Fields

name: Symbol

The self-reference name, bound in body.

body: TermId

The fixpoint body.

MutualFix

Term::MutualFix.

Fields

defs: Box<[(Symbol, TermId)]>

The block’s definitions; every name is bound in every body.

index: usize

Which definition this occurrence denotes.

Let

Term::Let.

Fields

name: Symbol

The bound name, bound in body.

ty: TermId

The ascribed type.

value: TermId

The bound value.

body: TermId

The body.

Lit(LitId)

Term::Lit.

Hole

Term::Hole.

Bound(u32)

A DE BRUIJN LEVEL — a bound-variable occurrence in an α-CANONICAL form.

TermStore::intern never produces this: no Term can spell it, which is exactly why it is a node and not a reserved NAME. A reserved name could collide with a free variable a user actually wrote, and the collision would silently conflate two terms that are not α-equivalent. A node shape cannot collide with anything.

Implementations

impl Node

pub fn for_each_child(&self, f: &mut impl FnMut(TermId))

Visit this node’s term children, in their canonical order.

This is the SINGLE source of truth for child order. Node::child_count and Node::rebuild_with are both defined against it, and term_store_extra::rebuild_with_round_trips_every_variant locks the three together.

pub fn child_count(&self) -> usize

How many term children this node has.

pub fn rebuild_with(&self, children: &[TermId]) -> Node

This node with its children replaced, positionally, by children.

Panics

Panics if children.len() != self.child_count() — a caller that miscounts is a bug, not a recoverable condition.

Trait Implementations

impl Clone for Node

fn clone(&self) -> Node

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Node

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

Formats the value using the given formatter.

impl Hash for Node

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 Node

fn eq(&self, other: &Node) -> 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 Node

impl StructuralPartialEq for Node