pub struct Node { /* private fields */ }Expand description
A child edge in an Expr: a reference-counted subterm together with
the facts about it that the kernel needs in O(1) (structural sharing,
wave5 Stage E; the hash and the three flags added for 0.1.4).
range— the subterm’slooseBVarRange:1 + the largest loose de Bruijn index in the subterm(0 = closed). It lets a substitution or lift decide in O(1) whether a subtree is affected —range <= depthmeans “no loose bvar can be touched, share it unchanged” — without traversing the subtree.cost— the size of the subterm counted as a TREE (a shared subterm once per path to it), saturating atREBUILD_COST_MAX: one unit per node plus one more per leaf, socost(leaf) = 2andcost(internal) = 1 + Σ cost(children). The reduction and def-eq caches read it to keep giant terms out (expr_util::expr_size_within). Through 0.1.4’s first performance pass this was also what a substitution charged to the per-declaration budget for a subtree it shared instead of rebuilding; sharing a subtree now charges one unit (seecrate::fuel).hash— the hash of the subterm’s structure (the kernel-privatestructural_hashmodule documents it).Hashwrites it instead of walking the subterm, and==uses it as a fast negative test.- three flags — whether the subterm contains a free variable, a universe parameter, a universe metavariable. They let the operations that only concern those (abstracting a free variable, instantiating universe parameters, the universe hygiene check of a declaration) pass over everything else without visiting it.
All of them are computed once, bottom-up, in Node::new from the
subterm’s own immediate children (also Nodes), so construction stays
O(nodes) and none of them ever needs a traversal.
§Layout
The facts live in the shared allocation, next to the subterm; a Node is
one pointer. (Through 0.1.3 range and cost sat on the edge beside the
pointer, and the allocation held the bare Expr.) An allocation is the
two reference counts, 16 bytes of facts and a 40-byte Expr — 72 bytes
where the old layout used 80, with the hash and the flags added (the
flags share a word with cost) — and an Expr held by value, as every
cache key is, is 40 bytes where it was 64. Reading a fact dereferences the
edge, which costs nothing extra where it matters: a substitution that
skips a subtree shares it by bumping the reference count stored right
beside the facts, and one that does not skip it walks into it.
Node is a transparent wrapper: it Derefs to the inner Expr, and its
PartialEq/Eq/Hash are those of the subterm (so the instances on
Expr keep exactly their structural meaning). The cached facts are
functions of the subterm and so never change what is equal to what.
Implementations§
Source§impl Node
impl Node
Sourcepub fn new(e: Expr) -> Node
pub fn new(e: Expr) -> Node
Wrap an Expr as a child edge, caching its looseBVarRange, its
tree size, its content flags and the hash of its structure. O(1): each
is read off the cached facts of e’s immediate children (for a Sort
or a Const, off its universe levels).
In a build that tracks the depth of terms
(crate::fuel::TERM_DEPTH_TRACKED) the depth is cached too, and a
subterm deeper than the limit of
crate::fuel::set_term_depth_limit spends the budget of the
declaration being checked.
Sourcepub fn rebuild_cost(&self) -> u32
pub fn rebuild_cost(&self) -> u32
The cached size of this subterm counted as a tree (O(1)); see
Expr::rebuild_cost.
Sourcepub fn as_ptr(&self) -> *const Expr
pub fn as_ptr(&self) -> *const Expr
The address of the shared subterm. Two nodes return the same address exactly when they share one allocation, for as long as either is alive — so the address can key a memo table over a term whose subterms are shared, visiting each shared subterm once.
The pointer is for comparison only. (This replaces rc(), which
exposed the Rc<Expr> the edge used to hold.)
Methods from Deref<Target = Expr>§
Sourcepub fn range(&self) -> u32
pub fn range(&self) -> u32
This node’s looseBVarRange — 1 + the largest loose de Bruijn index,
or 0 if closed. O(1): it reads the immediate children’s cached ranges
(see Node) and combines them, accounting for the binders each child
sits under.
Sourcepub fn rebuild_cost(&self) -> u32
pub fn rebuild_cost(&self) -> u32
The size of this term counted as a TREE — a shared subterm once per
path to it — O(1) from the children’s cached sizes: one unit per node
and one more per leaf, so cost(leaf) = 2 and
cost(internal) = 1 + Σ cost(children), saturating at
REBUILD_COST_MAX. It is what rebuilding the term node by node,
with no sharing, would cost; the caches read it to keep giant terms
out.
Sourcepub fn is_atom(&self) -> bool
pub fn is_atom(&self) -> bool
Check if this expression is an “atom” (cannot be further reduced without context): Sort, BVar, FVar, Const, Lit.
Sourcepub fn as_const_name(&self) -> Option<&Name>
pub fn as_const_name(&self) -> Option<&Name>
Extract the constant name, or None.
Sourcepub fn as_sort_level(&self) -> Option<&Level>
pub fn as_sort_level(&self) -> Option<&Level>
Extract the sort level, or None.
Sourcepub fn app_head_args(&self) -> (&Expr, Vec<&Expr>)
pub fn app_head_args(&self) -> (&Expr, Vec<&Expr>)
Return the head and argument list of an application spine.
For f a b c, returns (&f, [&a, &b, &c]).
Sourcepub fn has_loose_bvar_at(&self, d: u32) -> bool
pub fn has_loose_bvar_at(&self, d: u32) -> bool
Check if this expression has any loose bound variables at depth d.
Sourcepub fn count_bvar_occurrences(&self, idx: u32) -> usize
pub fn count_bvar_occurrences(&self, idx: u32) -> usize
Count occurrences of bound variable BVar(idx) in this expression.
Trait Implementations§
impl Eq for Node
Source§impl Hash for Node
impl Hash for Node
Source§impl PartialEq for Node
impl PartialEq for Node
Source§fn eq(&self, other: &Node) -> bool
fn eq(&self, other: &Node) -> bool
Structural equality of the two subterms, decided without comparing them when it can be: one allocation is equal to itself, and two subterms whose cached hashes differ are different (equal terms always hash equal). Only when the hashes agree are the subterms compared.