Struct HashConsArena 

pub struct HashConsArena { /* private fields */ }

A hash-consing wrapper around Arena<Expr>.

Every mk_* method checks a HashMap<ExprKey, Idx<Expr>> before allocating. If an equal node already exists in the arena the existing Idx is returned (a hit). Otherwise the node is allocated and indexed (a miss).

Structural sharing guarantee

For any two calls mk_foo(…args…) with structurally identical arguments, the returned Idx<Expr> values are equal. This means:

• O(1) equality of deduplicated nodes via index comparison
• Significantly reduced arena memory for expression-heavy workloads (e.g. type checking with many repeated sub-expressions)

Implementations

impl HashConsArena

pub fn new() -> Self

Creates an empty HashConsArena.

pub fn with_capacity(cap: usize) -> Self

Creates a HashConsArena with pre-allocated capacity for cap nodes.

pub fn get(&self, idx: Idx<Expr>) -> &Expr

Retrieve the Expr stored at idx.

pub fn len(&self) -> usize

Returns the number of distinct nodes in the arena.

pub fn is_empty(&self) -> bool

Returns true when no nodes have been allocated.

pub fn stats(&self) -> HashConsStats

Returns a statistics snapshot.

pub fn arena(&self) -> &Arena<Expr>

Borrow the underlying Arena<Expr> for read-only access.

pub fn mk_sort(&mut self, level: Level) -> Idx<Expr>

Allocate (or deduplicate) Expr::Sort(level).

pub fn mk_bvar(&mut self, idx: u32) -> Idx<Expr>

Allocate (or deduplicate) Expr::BVar(idx).

pub fn mk_fvar(&mut self, id: FVarId) -> Idx<Expr>

Allocate (or deduplicate) Expr::FVar(id).

pub fn mk_const(&mut self, name: Name, levels: Vec<Level>) -> Idx<Expr>

Allocate (or deduplicate) Expr::Const(name, levels).

pub fn mk_app(&mut self, f_expr: Expr, a_expr: Expr) -> Idx<Expr>

Allocate (or deduplicate) Expr::App(f_expr, a_expr).

f_expr and a_expr are cloned once to build the ExprKey; no extra clones occur on a cache hit.

pub fn mk_lam( &mut self, bi: BinderInfo, name: Name, dom: Expr, body: Expr, ) -> Idx<Expr>

Allocate (or deduplicate) Expr::Lam(bi, name, dom, body).

pub fn mk_pi( &mut self, bi: BinderInfo, name: Name, dom: Expr, cod: Expr, ) -> Idx<Expr>

Allocate (or deduplicate) Expr::Pi(bi, name, dom, cod).

pub fn mk_let( &mut self, name: Name, ty: Expr, val: Expr, body: Expr, ) -> Idx<Expr>

Allocate (or deduplicate) Expr::Let(name, ty, val, body).

pub fn mk_lit(&mut self, lit: Literal) -> Idx<Expr>

Allocate (or deduplicate) Expr::Lit(lit).

pub fn mk_proj( &mut self, name: Name, field_idx: u32, struct_expr: Expr, ) -> Idx<Expr>

Allocate (or deduplicate) Expr::Proj(name, field_idx, struct_expr).

Trait Implementations

impl Default for HashConsArena

fn default() -> Self

Returns the “default value” for a type.