Struct VarSubstitution 

pub struct VarSubstitution { /* private fields */ }

用于表示「变量替换」的字典

• 🎯NAL-6中的「变量替换」「变量代入」

Implementations

impl VarSubstitution

pub fn new() -> Self

构造函数

pub fn from(map: impl Into<HashMap<Term, Term>>) -> Self

从其它构造出「散列映射」的地方构造

pub fn from_pairs(pairs: impl IntoIterator<Item = (Term, Term)>) -> Self

从其它构造出「散列映射」的地方构造

pub fn get(&self, key: &Term) -> Option<&Term>

尝试获取「替代项」

• 🎯变量替换

pub fn chain_get(&self, key: &Term) -> Option<&Term>

链式获取「变量替换」最终点

• 🚩一路查找到头
• 📄{A -> B, B -> C}, A => Some(C)
• 📄{A -> B, B -> C}, B => Some(C)
• 📄{A -> B, B -> C}, C => None

pub fn has(&self, key: &Term) -> bool

尝试判断「是否有键」

• 🎯变量重命名

pub fn len(&self) -> usize

获取「可替换的变量个数」

• 🚩映射的大小
• 🎯变量重命名

pub fn is_empty(&self) -> bool

判断「是否为空」

• 🎯变量替换后检查「是否已替换」

pub fn put(&mut self, key: &Term, value: Term)

设置「替代项」

• 🎯寻找可替换变量，并返回结果
• 🚩只在没有键时复制key，并且总是覆盖value值

pub fn reduce_identities(&mut self)

删除映射中的「恒等替换」

• 📄$1 => $1

impl VarSubstitution

🆕将上述方法放在映射表的方法上

pub fn apply_to(&self, to: CompoundTermRefMut<'_>)

将映射表的替换模式应用到「复合词项可变引用」上

• 🎯用于「只需单个替换」的情况
  • 📄首先出自「条件演绎/归纳」

pub fn apply_to_term(&self, to: &mut Term)

尝试将映射表的替换模式应用到任意词项上

• 🎯用于「先应用，再判断词项类型」的情况

Trait Implementations

impl Clone for VarSubstitution

fn clone(&self) -> VarSubstitution

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for VarSubstitution

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

Formats the value using the given formatter.

impl Default for VarSubstitution

fn default() -> VarSubstitution

Returns the “default value” for a type.