Struct DiscTree 

pub struct DiscTree<T> { /* private fields */ }

A discrimination tree mapping term/expression patterns to payloads.

Term and expression patterns share one tree — their key alphabets are disjoint by construction, so they never cross-match.

Implementations

impl<T> DiscTree<T>

pub fn new() -> Self

pub fn insert_term(&mut self, pattern: &ProofTerm, value: T)

Index a term pattern (its Variables are the wildcard positions).

pub fn insert_expr(&mut self, pattern: &ProofExpr, value: T)

Index an expression pattern (its Variables are the wildcard positions).

pub fn candidates_term(&self, query: &ProofTerm) -> Vec<&T>

Every pattern that could one-sided match the query term (superset — confirm with crate::unify::match_term_pattern).

pub fn candidates_expr(&self, query: &ProofExpr) -> Vec<&T>

Every pattern that could one-sided match the query expression (superset — confirm with crate::unify::match_expr_pattern).

Trait Implementations

impl<T> Default for DiscTree<T>

fn default() -> Self

Returns the “default value” for a type.