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

use std::collections::HashMap;
use std;

use Term;

fn occurs_check<'a, T>(
    x: &'a Term<T>,
    t: &'a Term<T>,
    subs: &mut HashMap<&'a Term<T>, &'a Term<T>>,
) -> bool
where
    T: std::cmp::Eq + std::hash::Hash,
{
    let mut stack: Vec<&Term<T>> = vec![t];

    fn get_vars<'a, T>(t: &'a Term<T>) -> Vec<&'a Term<T>> {
        match t {
            &Term::Variable(_) => vec![t],
            &Term::Composite(_, ref terms) => {
                let mut v = vec![];
                for term in terms {
                    v.append(&mut get_vars(&term));
                }
                v
            }
            _ => vec![],
        }
    }

    while !stack.is_empty() {
        let t = stack.pop();
        for y in get_vars(t.unwrap()) {
            if x == y {
                return false;
            } else if subs.contains_key(y) {
                stack.push(subs[y]);
            }
        }
    }

    true
}

pub fn unify<'a, T>(s: &'a Term<T>, t: &'a Term<T>) -> Option<HashMap<&'a Term<T>, &'a Term<T>>>
where
    T: std::cmp::Eq + std::hash::Hash,
{
    let mut stack: Vec<(&Term<T>, &Term<T>)> = vec![(s, t)];
    let mut subs: HashMap<&Term<T>, &Term<T>> = HashMap::new();

    while !stack.is_empty() {
        let (mut s, mut t) = stack.pop().unwrap();

        while subs.contains_key(&s) {
            s = subs.get(&s).unwrap()
        }

        while subs.contains_key(&t) {
            t = subs.get(&t).unwrap()
        }

        if s != t {
            match (s, t) {
                (&Term::Variable(_), &Term::Variable(_)) => {
                    subs.insert(s, t);
                }
                (&Term::Variable(_), _) => if occurs_check(s, t, &mut subs) {
                    subs.insert(s, t);
                } else {
                    return None;
                },
                (_, &Term::Variable(_)) => if occurs_check(t, s, &mut subs) {
                    subs.insert(t, s);
                } else {
                    return None;
                },
                (
                    &Term::Composite(ref s_name, ref s_terms),
                    &Term::Composite(ref t_name, ref t_terms),
                ) => if s_name == t_name && s_terms.len() == t_terms.len() {
                    for (s, t) in s_terms.iter().zip(t_terms) {
                        stack.push((s, t));
                    }
                } else {
                    return None;
                },
                (_, _) => return None,
            }
        }
    }

    Some(subs)
}