mrs_unify/
lib.rs

1//! First-order unification and matching algorithms.
2//!
3//! This crate provides algorithms for finding substitutions that make terms equal:
4//!
5//! - [`unify`] - Most general unifier (MGU) of two terms
6//! - [`match_term`] - One-way matching: find a substitution making a pattern equal to a target
7//!
8//! Multiple algorithm implementations are available for educational comparison:
9//!
10//! - [`robinson`] - Classic recursive algorithm (simple, easy to understand)
11//!
12//! # Examples
13//!
14//! ```
15//! use mrs_core::{Term, SymbolTable};
16//! use mrs_unify::unify;
17//!
18//! let mut syms = SymbolTable::new();
19//! let f = syms.intern("f");
20//! let a = syms.intern("a");
21//!
22//! // Unify f(X, a) with f(b, Y)
23//! let b = syms.intern("b");
24//! let t1 = Term::app(f, vec![Term::var(0), Term::constant(a)]);
25//! let t2 = Term::app(f, vec![Term::constant(b), Term::var(1)]);
26//!
27//! let mgu = unify(&t1, &t2).unwrap();
28//! // X -> b, Y -> a
29//! assert_eq!(mgu.apply_term(&Term::var(0)), Term::constant(b));
30//! assert_eq!(mgu.apply_term(&Term::var(1)), Term::constant(a));
31//! ```
32
33pub mod matching;
34pub mod robinson;
35
36use std::fmt;
37
38use mrs_core::Substitution;
39use mrs_core::term::Term;
40
41/// Error type for unification failures.
42#[derive(Clone, Debug, Eq, PartialEq)]
43pub enum UnifyError {
44    /// The two terms have different top-level function symbols.
45    SymbolClash { left: String, right: String },
46    /// The two terms have different numbers of arguments.
47    ArityMismatch { expected: usize, found: usize },
48    /// A variable occurs in the term it would be unified with (infinite term).
49    OccursCheck { var: u32 },
50}
51
52impl fmt::Display for UnifyError {
53    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
54        match self {
55            UnifyError::SymbolClash { left, right } => {
56                write!(f, "symbol clash: {} vs {}", left, right)
57            }
58            UnifyError::ArityMismatch { expected, found } => {
59                write!(f, "arity mismatch: expected {}, found {}", expected, found)
60            }
61            UnifyError::OccursCheck { var } => {
62                write!(f, "occurs check failed for X{}", var)
63            }
64        }
65    }
66}
67
68impl std::error::Error for UnifyError {}
69
70/// Result type for unification.
71pub type UnifyResult = Result<Substitution, UnifyError>;
72
73/// Unifies two terms, returning their most general unifier (MGU).
74///
75/// Uses Robinson's algorithm. Returns `Err` if the terms cannot be unified.
76///
77/// # Examples
78///
79/// ```
80/// use mrs_core::{Term, SymbolTable};
81/// use mrs_unify::unify;
82///
83/// let mut syms = SymbolTable::new();
84/// let f = syms.intern("f");
85/// let a = syms.intern("a");
86///
87/// // Unify X with a
88/// let mgu = unify(&Term::var(0), &Term::constant(a)).unwrap();
89/// assert_eq!(mgu.apply_term(&Term::var(0)), Term::constant(a));
90///
91/// // Cannot unify f(a) with a (symbol clash)
92/// let t1 = Term::app(f, vec![Term::constant(a)]);
93/// assert!(unify(&t1, &Term::constant(a)).is_err());
94/// ```
95pub fn unify(s: &Term, t: &Term) -> UnifyResult {
96    robinson::unify(s, t)
97}
98
99/// Unifies two terms with commutativity support for a set of binary symbols.
100///
101/// Delegates to [`robinson::unify_comm`]. See that function for details.
102///
103/// # Examples
104///
105/// ```
106/// use std::collections::HashSet;
107/// use mrs_core::{Term, SymbolTable};
108/// use mrs_unify::unify_comm;
109///
110/// let mut syms = SymbolTable::new();
111/// let f = syms.intern("f");
112/// let a = syms.intern("a");
113/// let b = syms.intern("b");
114///
115/// // f(a,b) ~ f(b,a) with f commutative
116/// let mut comm = HashSet::new();
117/// comm.insert(f);
118/// let t1 = Term::app(f, vec![Term::constant(a), Term::constant(b)]);
119/// let t2 = Term::app(f, vec![Term::constant(b), Term::constant(a)]);
120/// assert!(unify_comm(&t1, &t2, &comm).is_ok());
121/// ```
122pub fn unify_comm(
123    s: &Term,
124    t: &Term,
125    comm: &std::collections::HashSet<mrs_core::SymbolId>,
126) -> UnifyResult {
127    robinson::unify_comm(s, t, comm)
128}
129
130/// Matches a pattern against a target term (one-way unification).
131///
132/// Only variables in the pattern are bound; the target is treated as ground.
133/// Returns `Err` if the pattern cannot be matched against the target.
134///
135/// # Examples
136///
137/// ```
138/// use mrs_core::{Term, SymbolTable};
139/// use mrs_unify::match_term;
140///
141/// let mut syms = SymbolTable::new();
142/// let f = syms.intern("f");
143/// let a = syms.intern("a");
144///
145/// // Match f(X) against f(a) -> X = a
146/// let pattern = Term::app(f, vec![Term::var(0)]);
147/// let target = Term::app(f, vec![Term::constant(a)]);
148/// let sub = match_term(&pattern, &target).unwrap();
149/// assert_eq!(sub.apply_term(&Term::var(0)), Term::constant(a));
150/// ```
151pub fn match_term(pattern: &Term, target: &Term) -> UnifyResult {
152    matching::match_term(pattern, target)
153}
mrs_unify/lib.rs

mrs_unify/
lib.rs
