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); } }