Struct ExprKey 

pub struct ExprKey(pub Expr);

Structural key derived from the content of one Expr node.

Two ExprKey values are equal if and only if the corresponding Expr values are structurally identical (same variant, same fields). This is precisely the condition under which hash-consing must return the same Idx<Expr>.

Internally the key clones the Expr so that the HashMap<ExprKey, …> owns its keys independently of any arena.

Tuple Fields

0: Expr

Implementations

impl ExprKey

pub fn new(expr: Expr) -> Self

Construct an ExprKey from an owned Expr.

pub fn from_ref(expr: &Expr) -> Self

Construct an ExprKey from a reference, cloning the expression.

pub fn into_inner(self) -> Expr

Return the inner Expr.

pub fn inner(&self) -> &Expr

Borrow the inner Expr.

impl ExprKey

pub fn sort(level: Level) -> Self

Key for Expr::Sort(level).

pub fn bvar(idx: u32) -> Self

Key for Expr::BVar(idx).

pub fn fvar(id: FVarId) -> Self

Key for Expr::FVar(id).

pub fn const_(name: Name, levels: Vec<Level>) -> Self

Key for Expr::Const(name, levels).

pub fn app(f: Expr, a: Expr) -> Self

Key for Expr::App(f, a).

pub fn lam(bi: BinderInfo, name: Name, dom: Expr, body: Expr) -> Self

Key for Expr::Lam(bi, name, dom, body).

pub fn pi(bi: BinderInfo, name: Name, dom: Expr, cod: Expr) -> Self

Key for Expr::Pi(bi, name, dom, cod).

pub fn let_(name: Name, ty: Expr, val: Expr, body: Expr) -> Self

Key for Expr::Let(name, ty, val, body).

pub fn lit(lit: Literal) -> Self

Key for Expr::Lit(lit).

pub fn proj(name: Name, idx: u32, struct_expr: Expr) -> Self

Key for Expr::Proj(name, idx, struct_expr).

Trait Implementations

impl Clone for ExprKey

fn clone(&self) -> ExprKey

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ExprKey

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

Formats the value using the given formatter.

impl Hash for ExprKey

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 ExprKey

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

impl StructuralPartialEq for ExprKey