rust-unify 0.1.0

A unification algorithum implementation in rust.
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

#[macro_use]
extern crate maplit;

mod robinsons;

use std::fmt;

pub use robinsons::unify;

#[derive(Hash, PartialEq, Eq, Debug, Clone)]
pub enum Term<T> {
    Variable(T),
    Constant(T),
    Composite(T, Vec<Term<T>>),
}

impl fmt::Display for Term<String> {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        match self {
            &Term::Variable(ref name) => write!(f, "{}", name),
            &Term::Constant(ref value) => write!(f, "{}", value),
            &Term::Composite(ref name, ref terms) => {
                let terms: Vec<String> = terms.iter().map(|t| format!("{}", t)).collect();

                write!(f, "{}({})", name, terms.join(", "))
            }
        }
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_robinsons() {
        let a = &Term::Constant("a");
        assert_eq!(robinsons::unify(a, a), Some(hashmap!{}));

        let b = &Term::Constant("b");
        assert_eq!(robinsons::unify(a, b), None);

        let _x = &Term::Variable("X");
        assert_eq!(robinsons::unify(_x, _x), Some(hashmap!{}));
        assert_eq!(robinsons::unify(a, _x), Some(hashmap!{_x => a}));
        assert_eq!(robinsons::unify(_x, a), Some(hashmap!{_x => a}));
        assert_eq!(robinsons::unify(a, _x), Some(hashmap!{_x => a}));

        let _y = &Term::Variable("Y");
        assert_eq!(robinsons::unify(_x, _y), Some(hashmap!{_x => _y}));
        assert_eq!(robinsons::unify(_y, _x), Some(hashmap!{_y => _x}));

        let f1 = &Term::Composite("f", vec![Term::Constant("a")]);
        assert_eq!(robinsons::unify(f1, f1), Some(hashmap!{}));

        let f2 = &Term::Composite("f", vec![Term::Constant("b")]);
        assert_eq!(robinsons::unify(f1, f2), None);

        let f3 = &Term::Composite("f", vec![Term::Variable("X")]);
        assert_eq!(robinsons::unify(f1, f3), Some(hashmap!{_x => a}));
        assert_eq!(robinsons::unify(f2, f3), Some(hashmap!{_x => b}));

        let f4 = &Term::Composite("f", vec![Term::Variable("Y")]);
        assert_eq!(robinsons::unify(f3, f4), Some(hashmap!{_x => _y}));

        let g1 = &Term::Composite("g", vec![Term::Constant("a")]);
        assert_eq!(robinsons::unify(f1, g1), None);

        let g2 = &Term::Composite("g", vec![Term::Variable("X")]);
        assert_eq!(robinsons::unify(f3, g2), None);

        let g3 = &Term::Composite("g", vec![Term::Variable("Y")]);
        assert_eq!(robinsons::unify(f3, g3), None);

        let g4 = &Term::Composite("g", vec![Term::Variable("Y"), Term::Variable("Z")]);
        assert_eq!(robinsons::unify(f3, g4), None);

        let fg1 = &Term::Composite("f", vec![Term::Composite("g", vec![Term::Variable("X")])]);
        assert_eq!(robinsons::unify(fg1, f4), Some(hashmap!{_y => g2}));

        let fg2 = &Term::Composite(
            "f",
            vec![
                Term::Composite("g", vec![Term::Variable("X")]),
                Term::Variable("X"),
            ],
        );
        let f5 = &Term::Composite("f", vec![Term::Variable("Y"), Term::Constant("a")]);
        assert_eq!(robinsons::unify(fg2, f5), Some(hashmap!{_x => a, _y => g2}));

        assert_eq!(robinsons::unify(_x, f3), None);
    }
}