plg_runtime/
unify.rs

1//! Generic unification over tagged heap words.
2//!
3//! Ports patch-prolog's `unify.rs` semantics to the cell heap: no occurs
4//! check (ISO 8.3.2), trail-recorded bindings, float equality via
5//! `to_bits` (NaN unifies with NaN). Iterative worklist — no recursion,
6//! so pathological terms can't blow the C stack.
7
8use crate::cell::*;
9use crate::machine::Machine;
10
11pub fn unify(m: &mut Machine, a: Word, b: Word) -> bool {
12    let mut work = vec![(a, b)];
13    while let Some((a, b)) = work.pop() {
14        let a = m.deref(a);
15        let b = m.deref(b);
16        if a == b {
17            continue; // same atom/int word, same cell, or same structure
18        }
19        match (tag_of(a), tag_of(b)) {
20            (TAG_REF, _) => m.bind(payload(a) as usize, b),
21            (_, TAG_REF) => m.bind(payload(b) as usize, a),
22            (TAG_ATOM, TAG_ATOM) | (TAG_INT, TAG_INT) => return false, // a != b
23            (TAG_BIG, TAG_BIG) => {
24                let va = m.heap[payload(a) as usize] as i64;
25                let vb = m.heap[payload(b) as usize] as i64;
26                if va != vb {
27                    return false;
28                }
29            }
30            // INT vs BIG: same integer type, compare by value (a boxed
31            // value never fits i61 by construction, so this only matches
32            // defensively).
33            (TAG_INT, TAG_BIG) => {
34                if int_value(a) != m.heap[payload(b) as usize] as i64 {
35                    return false;
36                }
37            }
38            (TAG_BIG, TAG_INT) => {
39                if (m.heap[payload(a) as usize] as i64) != int_value(b) {
40                    return false;
41                }
42            }
43            (TAG_FLT, TAG_FLT) => {
44                // to_bits comparison: NaN == NaN, -0.0 != 0.0 (v1 rule)
45                let fa = m.heap[payload(a) as usize];
46                let fb = m.heap[payload(b) as usize];
47                if fa != fb {
48                    return false;
49                }
50            }
51            (TAG_STR, TAG_STR) => {
52                let ia = payload(a) as usize;
53                let ib = payload(b) as usize;
54                let (fa, na) = unpack_functor(m.heap[ia]);
55                let (fb, nb) = unpack_functor(m.heap[ib]);
56                if fa != fb || na != nb {
57                    return false;
58                }
59                for k in 0..na as usize {
60                    work.push((m.heap[ia + 1 + k], m.heap[ib + 1 + k]));
61                }
62            }
63            (TAG_LST, TAG_LST) => {
64                let ia = payload(a) as usize;
65                let ib = payload(b) as usize;
66                work.push((m.heap[ia + 1], m.heap[ib + 1])); // tails
67                work.push((m.heap[ia], m.heap[ib])); // heads
68            }
69            _ => return false, // different tags never unify
70        }
71    }
72    true
73}
74
75#[cfg(test)]
76mod tests {
77    use super::*;
78    use plg_shared::StringInterner;
79
80    fn machine() -> Box<Machine> {
81        Machine::new(StringInterner::new(), Vec::new())
82    }
83
84    fn put_struct(m: &mut Machine, f: u32, args: &[Word]) -> Word {
85        let idx = m.heap.len();
86        m.heap.push(pack_functor(f, args.len() as u32));
87        m.heap.extend_from_slice(args);
88        make(TAG_STR, idx as u64)
89    }
90
91    fn put_list(m: &mut Machine, head: Word, tail: Word) -> Word {
92        let idx = m.heap.len();
93        m.heap.push(head);
94        m.heap.push(tail);
95        make(TAG_LST, idx as u64)
96    }
97
98    #[test]
99    fn atoms_unify_only_with_same_id() {
100        let mut m = machine();
101        assert!(unify(&mut m, make_atom(1), make_atom(1)));
102        assert!(!unify(&mut m, make_atom(1), make_atom(2)));
103    }
104
105    #[test]
106    fn var_binds_to_atom_and_is_trailed() {
107        let mut m = machine();
108        let v = m.new_var();
109        let t0 = m.trail.len();
110        assert!(unify(&mut m, v, make_atom(3)));
111        assert_eq!(m.deref(v), make_atom(3));
112        assert_eq!(m.trail.len(), t0 + 1);
113    }
114
115    #[test]
116    fn var_var_aliasing() {
117        let mut m = machine();
118        let x = m.new_var();
119        let y = m.new_var();
120        assert!(unify(&mut m, x, y));
121        assert!(unify(&mut m, x, make_int(9)));
122        assert_eq!(int_value(m.deref(y)), 9);
123    }
124
125    #[test]
126    fn structs_unify_recursively() {
127        let mut m = machine();
128        let x = m.new_var();
129        // f(a, X) = f(a, 42)
130        let s1 = put_struct(&mut m, 5, &[make_atom(1), x]);
131        let s2 = put_struct(&mut m, 5, &[make_atom(1), make_int(42)]);
132        assert!(unify(&mut m, s1, s2));
133        assert_eq!(int_value(m.deref(x)), 42);
134        // arity mismatch
135        let s3 = put_struct(&mut m, 5, &[make_atom(1)]);
136        assert!(!unify(&mut m, s1, s3));
137        // functor mismatch
138        let s4 = put_struct(&mut m, 6, &[make_atom(1), make_int(42)]);
139        assert!(!unify(&mut m, s1, s4));
140    }
141
142    #[test]
143    fn lists_unify_elementwise() {
144        let mut m = machine();
145        let x = m.new_var();
146        let nil = make_atom(plg_shared::atom::ATOM_NIL);
147        // [1|X] = [1, 2]
148        let l2 = {
149            let inner = put_list(&mut m, make_int(2), nil);
150            put_list(&mut m, make_int(1), inner)
151        };
152        let l1 = put_list(&mut m, make_int(1), x);
153        assert!(unify(&mut m, l1, l2));
154        // X is now [2]
155        let xd = m.deref(x);
156        assert_eq!(tag_of(xd), TAG_LST);
157    }
158
159    #[test]
160    fn nan_unifies_with_nan() {
161        let mut m = machine();
162        let bits = f64::NAN.to_bits();
163        let f1 = {
164            let i = m.heap.len();
165            m.heap.push(bits);
166            make(TAG_FLT, i as u64)
167        };
168        let f2 = {
169            let i = m.heap.len();
170            m.heap.push(bits);
171            make(TAG_FLT, i as u64)
172        };
173        assert!(unify(&mut m, f1, f2));
174    }
175
176    #[test]
177    fn failed_unify_leaves_partial_bindings_for_caller_rewind() {
178        // The engine relies on choice-point rewind (not unify itself) to
179        // undo partial bindings — same as v1. Verify the trail records them.
180        let mut m = machine();
181        let x = m.new_var();
182        let s1 = put_struct(&mut m, 5, &[x, make_atom(1)]);
183        let s2 = put_struct(&mut m, 5, &[make_atom(2), make_atom(9)]);
184        let tmark = m.trail.len();
185        let hmark = m.heap.len();
186        assert!(!unify(&mut m, s1, s2));
187        m.rewind_to(tmark, hmark);
188        assert_eq!(m.deref(x), x);
189    }
190}
plg_runtime/unify.rs

plg_runtime/
unify.rs
