Struct Arena 

pub struct Arena { /* private fields */ }

Arena for interning terms with hash-consing

Implementations

impl Arena

pub fn new() -> Self

Create a new term arena

pub fn intern(&mut self, kind: TermKind) -> TermId

Intern a term and return its ID

pub fn get(&self, id: TermId) -> Option<&Term>

Get a term by its ID

pub fn get_term(&self, id: TermId) -> Option<&Term>

Get a term by its ID (alias for compatibility)

pub fn kind(&self, id: TermId) -> Option<&TermKind>

Get the kind of a term by its ID

pub fn terms(&self) -> usize

Get the number of terms in the arena

pub fn stats(&self) -> &ArenaStats

Get arena statistics

pub fn cache_hit_rate(&self) -> f64

Get cache efficiency (hit rate)

pub fn clear_stats(&mut self)

Clear all statistics

pub fn mk_sort(&mut self, level: LevelId) -> TermId

Create a sort term

pub fn mk_const(&mut self, name: SymbolId, levels: Vec<LevelId>) -> TermId

Create a constant term

pub fn mk_var(&mut self, index: u32) -> TermId

Create a variable term

pub fn mk_app(&mut self, func: TermId, arg: TermId) -> TermId

Create an application term

pub fn mk_lam(&mut self, binder: Binder, body: TermId) -> TermId

Create a lambda term

pub fn mk_pi(&mut self, binder: Binder, body: TermId) -> TermId

Create a Pi term

pub fn mk_let(&mut self, binder: Binder, value: TermId, body: TermId) -> TermId

Create a let term

pub fn mk_mvar(&mut self, id: MetaVarId) -> TermId

Create a metavariable term

pub fn mk_nat(&mut self, n: u64) -> TermId

Create a natural number literal

pub fn mk_app_spine(&mut self, func: TermId, args: &[TermId]) -> TermId

Create a spine of applications (f x y z)

pub fn mk_level_zero(&mut self) -> LevelId

Create a zero universe level

Trait Implementations

impl Default for Arena

fn default() -> Self

Returns the “default value” for a type.