Struct Substitution 

pub struct Substitution { /* private fields */ }

Vec-based substitution with trail for efficient backtracking. Bindings are stored in a Vec indexed by VarId (O(1) lookup/bind). The trail records which VarIds were bound, enabling undo on backtracking.

Implementations

impl Substitution

pub fn new() -> Self

pub fn with_capacity(n: usize) -> Self

Create a substitution pre-sized for the given number of variables.

pub fn trail_mark(&self) -> usize

Get the current trail mark (for backtracking).

pub fn undo_to(&mut self, mark: usize)

Undo all bindings back to the given trail mark.

pub fn walk(&self, term: &Term) -> Term

Dereference: follow variable chains to their ultimate value.

pub fn apply(&self, term: &Term) -> Term

Deep walk: recursively substitute all variables in a term. Handles circular terms (from unification without occurs check) by stopping expansion when a variable cycle is detected.

pub fn unify(&mut self, t1: &Term, t2: &Term) -> bool

Unify two terms. Returns true if unification succeeds. On failure, bindings made during this attempt remain (caller should undo via trail).

pub fn unify_with_occurs_check(&mut self, t1: &Term, t2: &Term) -> bool

Unify with occurs check (ISO 8.2.2). Fails if binding a variable would create a circular term.

Trait Implementations

impl Clone for Substitution

fn clone(&self) -> Substitution

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Substitution

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

Formats the value using the given formatter.

impl Default for Substitution

fn default() -> Self

Returns the “default value” for a type.