Struct LogicEnv 

pub struct LogicEnv { /* private fields */ }

A unification substitution: bindings from logic variables to terms.

Carries a resolution depth so renamed clause variables stay distinct across recursive calls.

Implementations

impl LogicEnv

pub fn new() -> Self

Creates an empty environment at depth zero.

pub fn with_depth(depth: usize) -> Self

Creates an empty environment recorded at the given resolution depth.

pub fn depth(&self) -> usize

Returns the resolution depth recorded for this environment.

pub fn set_depth(&mut self, depth: usize)

Sets the recorded resolution depth.

pub fn apply(&self, expr: &Expr) -> Expr

Applies the substitution to expr, recursively replacing bound variables with their values.

pub fn get(&self, var: &Symbol) -> Option<&Expr>

Returns the term directly bound to var, if any.

pub fn bind( &mut self, var: Symbol, value: Expr, occurs_check: OccursCheck, ) -> Result<()>

Binds var to value, honoring the OccursCheck policy.

Returns an error when an enabled occurs check detects that var occurs in value (which would build a cyclic term).

pub fn unify( &mut self, left: &Expr, right: &Expr, occurs_check: OccursCheck, ) -> Result<bool>

Unifies two terms, extending the substitution in place.

Returns true when the terms unify and false on a structural mismatch; errors propagate only from a failed occurs check.

pub fn free_vars(&self, expr: &Expr) -> Vec<Symbol>

Collects the distinct logic variables appearing in expr.

pub fn to_shape_bindings(&self, _cx: &mut Cx) -> Result<ShapeBindings>

Projects the current bindings into kernel ShapeBindings.

pub fn as_shape_match(&self, cx: &mut Cx) -> Result<ShapeMatch>

Builds an accepting kernel ShapeMatch whose captures are this environment’s bindings.

Trait Implementations

impl Clone for LogicEnv

fn clone(&self) -> LogicEnv

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LogicEnv

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

Formats the value using the given formatter.

impl Default for LogicEnv

fn default() -> LogicEnv

Returns the “default value” for a type.

impl Eq for LogicEnv

impl PartialEq for LogicEnv

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