Struct ShapeMask 

pub struct ShapeMask(/* private fields */);

The set of NodeShapes occurring anywhere in a subterm — one u16, computed once at interning time and answered in O(1) thereafter.

The Lean design this copies

Lean’s Expr carries a 64-bit Expr.Data word in every node, and four of its bits are exactly this idea: hasFVar, hasExprMVar, hasLevelMVar, hasLevelParam (Lean/Expr.lean:121-124). Expr.mkAppData propagates all four with a single OR of the two children’s words — ((fData ||| aData) &&& (15 <<< 40)) ||| … (Lean/Expr.lean:193) — so an application’s bits cost one instruction rather than a traversal. What they BUY is visible at Lean/Expr.lean:1661: let rec visit (e : Expr) := if !e.hasFVar then false else …, a walk that stops before it starts.

Ours widens the idea from four hand-picked predicates to one bit per node kind, which is what lets beta_zeta_normal_form decide in O(1) whether a term can hold a redex it does not own. The cost is the same: one OR per child at interning time, in TermStore::compute_info.

Implementations

impl ShapeMask

pub const NONE: ShapeMask

The empty mask — no shape occurs.

pub const BETA_ZETA: ShapeMask

The shapes a term made only of Sort, Var, Global, App, Lambda, Pi and Let can have — the admissible surface of beta_zeta_normal_form. Its complement is Const, Match, Fix, MutualFix, Lit, Hole and Bound.

pub fn contains(self, shape: NodeShape) -> bool

Whether shape occurs anywhere in the subterm.

pub fn subset_of(self, other: ShapeMask) -> bool

Whether every shape in this mask is also in other.

pub fn union(self, other: ShapeMask) -> ShapeMask

The union of two masks.

pub fn with(self, shape: NodeShape) -> ShapeMask

This mask with shape added.

pub fn bits(self) -> u16

The raw bits, for a caller that wants to store or compare them.

Trait Implementations

impl Clone for ShapeMask

fn clone(&self) -> ShapeMask

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ShapeMask

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

Formats the value using the given formatter.

impl Default for ShapeMask

fn default() -> ShapeMask

Returns the “default value” for a type.

impl Hash for ShapeMask

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 ShapeMask

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

impl Eq for ShapeMask

impl StructuralPartialEq for ShapeMask