mrs-unify 0.1.0

First-order unification and matching algorithms
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122

//! First-order unification and matching algorithms.
//!
//! This crate provides algorithms for finding substitutions that make terms equal:
//!
//! - [`unify`] - Most general unifier (MGU) of two terms
//! - [`match_term`] - One-way matching: find a substitution making a pattern equal to a target
//!
//! Multiple algorithm implementations are available for educational comparison:
//!
//! - [`robinson`] - Classic recursive algorithm (simple, easy to understand)
//!
//! # Examples
//!
//! ```
//! use mrs_core::{Term, SymbolTable};
//! use mrs_unify::unify;
//!
//! let mut syms = SymbolTable::new();
//! let f = syms.intern("f");
//! let a = syms.intern("a");
//!
//! // Unify f(X, a) with f(b, Y)
//! let b = syms.intern("b");
//! let t1 = Term::app(f, vec![Term::var(0), Term::constant(a)]);
//! let t2 = Term::app(f, vec![Term::constant(b), Term::var(1)]);
//!
//! let mgu = unify(&t1, &t2).unwrap();
//! // X -> b, Y -> a
//! assert_eq!(mgu.apply_term(&Term::var(0)), Term::constant(b));
//! assert_eq!(mgu.apply_term(&Term::var(1)), Term::constant(a));
//! ```

pub mod matching;
pub mod robinson;

use std::fmt;

use mrs_core::Substitution;
use mrs_core::term::Term;

/// Error type for unification failures.
#[derive(Clone, Debug, Eq, PartialEq)]
pub enum UnifyError {
    /// The two terms have different top-level function symbols.
    SymbolClash { left: String, right: String },
    /// The two terms have different numbers of arguments.
    ArityMismatch { expected: usize, found: usize },
    /// A variable occurs in the term it would be unified with (infinite term).
    OccursCheck { var: u32 },
}

impl fmt::Display for UnifyError {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            UnifyError::SymbolClash { left, right } => {
                write!(f, "symbol clash: {} vs {}", left, right)
            }
            UnifyError::ArityMismatch { expected, found } => {
                write!(f, "arity mismatch: expected {}, found {}", expected, found)
            }
            UnifyError::OccursCheck { var } => {
                write!(f, "occurs check failed for X{}", var)
            }
        }
    }
}

impl std::error::Error for UnifyError {}

/// Result type for unification.
pub type UnifyResult = Result<Substitution, UnifyError>;

/// Unifies two terms, returning their most general unifier (MGU).
///
/// Uses Robinson's algorithm. Returns `Err` if the terms cannot be unified.
///
/// # Examples
///
/// ```
/// use mrs_core::{Term, SymbolTable};
/// use mrs_unify::unify;
///
/// let mut syms = SymbolTable::new();
/// let f = syms.intern("f");
/// let a = syms.intern("a");
///
/// // Unify X with a
/// let mgu = unify(&Term::var(0), &Term::constant(a)).unwrap();
/// assert_eq!(mgu.apply_term(&Term::var(0)), Term::constant(a));
///
/// // Cannot unify f(a) with a (symbol clash)
/// let t1 = Term::app(f, vec![Term::constant(a)]);
/// assert!(unify(&t1, &Term::constant(a)).is_err());
/// ```
pub fn unify(s: &Term, t: &Term) -> UnifyResult {
    robinson::unify(s, t)
}

/// Matches a pattern against a target term (one-way unification).
///
/// Only variables in the pattern are bound; the target is treated as ground.
/// Returns `Err` if the pattern cannot be matched against the target.
///
/// # Examples
///
/// ```
/// use mrs_core::{Term, SymbolTable};
/// use mrs_unify::match_term;
///
/// let mut syms = SymbolTable::new();
/// let f = syms.intern("f");
/// let a = syms.intern("a");
///
/// // Match f(X) against f(a) -> X = a
/// let pattern = Term::app(f, vec![Term::var(0)]);
/// let target = Term::app(f, vec![Term::constant(a)]);
/// let sub = match_term(&pattern, &target).unwrap();
/// assert_eq!(sub.apply_term(&Term::var(0)), Term::constant(a));
/// ```
pub fn match_term(pattern: &Term, target: &Term) -> UnifyResult {
    matching::match_term(pattern, target)
}