rust_unify/
lib.rs

1#[macro_use]
2extern crate maplit;
3
4mod robinsons;
5
6use std::fmt;
7
8pub use robinsons::unify;
9
10#[derive(Hash, PartialEq, Eq, Debug, Clone)]
11pub enum Term<T> {
12    Variable(T),
13    Constant(T),
14    Composite(T, Vec<Term<T>>),
15}
16
17impl fmt::Display for Term<String> {
18    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
19        match self {
20            &Term::Variable(ref name) => write!(f, "{}", name),
21            &Term::Constant(ref value) => write!(f, "{}", value),
22            &Term::Composite(ref name, ref terms) => {
23                let terms: Vec<String> = terms.iter().map(|t| format!("{}", t)).collect();
24
25                write!(f, "{}({})", name, terms.join(", "))
26            }
27        }
28    }
29}
30
31#[cfg(test)]
32mod tests {
33    use super::*;
34
35    #[test]
36    fn test_robinsons() {
37        let a = &Term::Constant("a");
38        assert_eq!(robinsons::unify(a, a), Some(hashmap!{}));
39
40        let b = &Term::Constant("b");
41        assert_eq!(robinsons::unify(a, b), None);
42
43        let _x = &Term::Variable("X");
44        assert_eq!(robinsons::unify(_x, _x), Some(hashmap!{}));
45        assert_eq!(robinsons::unify(a, _x), Some(hashmap!{_x => a}));
46        assert_eq!(robinsons::unify(_x, a), Some(hashmap!{_x => a}));
47        assert_eq!(robinsons::unify(a, _x), Some(hashmap!{_x => a}));
48
49        let _y = &Term::Variable("Y");
50        assert_eq!(robinsons::unify(_x, _y), Some(hashmap!{_x => _y}));
51        assert_eq!(robinsons::unify(_y, _x), Some(hashmap!{_y => _x}));
52
53        let f1 = &Term::Composite("f", vec![Term::Constant("a")]);
54        assert_eq!(robinsons::unify(f1, f1), Some(hashmap!{}));
55
56        let f2 = &Term::Composite("f", vec![Term::Constant("b")]);
57        assert_eq!(robinsons::unify(f1, f2), None);
58
59        let f3 = &Term::Composite("f", vec![Term::Variable("X")]);
60        assert_eq!(robinsons::unify(f1, f3), Some(hashmap!{_x => a}));
61        assert_eq!(robinsons::unify(f2, f3), Some(hashmap!{_x => b}));
62
63        let f4 = &Term::Composite("f", vec![Term::Variable("Y")]);
64        assert_eq!(robinsons::unify(f3, f4), Some(hashmap!{_x => _y}));
65
66        let g1 = &Term::Composite("g", vec![Term::Constant("a")]);
67        assert_eq!(robinsons::unify(f1, g1), None);
68
69        let g2 = &Term::Composite("g", vec![Term::Variable("X")]);
70        assert_eq!(robinsons::unify(f3, g2), None);
71
72        let g3 = &Term::Composite("g", vec![Term::Variable("Y")]);
73        assert_eq!(robinsons::unify(f3, g3), None);
74
75        let g4 = &Term::Composite("g", vec![Term::Variable("Y"), Term::Variable("Z")]);
76        assert_eq!(robinsons::unify(f3, g4), None);
77
78        let fg1 = &Term::Composite("f", vec![Term::Composite("g", vec![Term::Variable("X")])]);
79        assert_eq!(robinsons::unify(fg1, f4), Some(hashmap!{_y => g2}));
80
81        let fg2 = &Term::Composite(
82            "f",
83            vec![
84                Term::Composite("g", vec![Term::Variable("X")]),
85                Term::Variable("X"),
86            ],
87        );
88        let f5 = &Term::Composite("f", vec![Term::Variable("Y"), Term::Constant("a")]);
89        assert_eq!(robinsons::unify(fg2, f5), Some(hashmap!{_x => a, _y => g2}));
90
91        assert_eq!(robinsons::unify(_x, f3), None);
92    }
93}
rust_unify/lib.rs

rust_unify/
lib.rs
