Skip to main content

plg_runtime/builtins/
miscops.rs

1//! Miscellaneous deterministic builtins: `succ/2`, `plus/3`,
2//! `unify_with_occurs_check/2`, `write/1`, `writeln/1`, `nl/0`.
3//!
4//! Ported byte-for-byte from patch-prolog v1 (`solver.rs` arms,
5//! `unify.rs` occurs-check unifier). Notes:
6//! - `succ/2` both modes; `succ(X, 0)` fails; negatives raise
7//!   `domain_error(not_less_than_zero, _)`; both-unbound raises
8//!   instantiation.
9//! - `plus/3` supports the three integer modes (any one argument
10//!   unbound); fewer than two bound raises instantiation.
11//! - `unify_with_occurs_check/2` uses a LOCAL occurs-checking unifier
12//!   (iterative; does not touch the shared `unify.rs`).
13//! - `write/1` / `writeln/1` use v1's `term_to_string` (infix operators,
14//!   `[a, b]` lists, floats via `{}`), printed immediately. `write` adds
15//!   no newline; `writeln` and `nl` add one.
16
17use crate::cell::*;
18use crate::machine::Machine;
19use crate::render::term_to_string;
20use crate::unify::unify;
21use std::io::Write as _;
22
23#[inline]
24fn mref<'a>(m: *mut Machine) -> &'a mut Machine {
25    unsafe { &mut *m }
26}
27
28/// Extract an i64 from an integer word (immediate or boxed).
29fn int_of(m: &Machine, w: Word) -> Option<i64> {
30    match tag_of(w) {
31        TAG_INT => Some(int_value(w)),
32        TAG_BIG => Some(m.heap[payload(w) as usize] as i64),
33        _ => None,
34    }
35}
36
37/// Materialize an i64 as a heap word (immediate INT or boxed BIG).
38fn int_word(m: &mut Machine, n: i64) -> Word {
39    if (INT_MIN..=INT_MAX).contains(&n) {
40        make_int(n)
41    } else {
42        let idx = m.heap.len();
43        m.heap.push(n as u64);
44        make(TAG_BIG, idx as u64)
45    }
46}
47
48/// `succ/2`: `S = X + 1` over non-negative integers, both modes.
49#[unsafe(no_mangle)]
50pub extern "C" fn plg_rt_b_succ_2(m: *mut Machine, x: u64, s: u64, site_id: u32) -> i32 {
51    let _site = crate::machine::ErrorSiteGuard::enter(m, site_id);
52    let m = mref(m);
53    let wx = m.deref(x);
54    let ws = m.deref(s);
55    let xi = int_of(m, wx);
56    let si = int_of(m, ws);
57    match (xi, si) {
58        (Some(xv), _) if xv >= 0 => match xv.checked_add(1) {
59            Some(r) => {
60                let rw = int_word(m, r);
61                unify(m, s, rw) as i32
62            }
63            None => {
64                crate::errors::evaluation(m, "int_overflow", "succ/2: integer overflow");
65                0
66            }
67        },
68        (_, Some(sv)) if sv > 0 => {
69            let rw = int_word(m, sv - 1);
70            unify(m, x, rw) as i32
71        }
72        (_, Some(0)) => 0, // succ(X, 0) fails
73        (Some(_), _) => {
74            // X is a negative integer.
75            crate::errors::domain_error(
76                m,
77                "not_less_than_zero",
78                wx,
79                "succ/2: argument must be non-negative",
80            );
81            0
82        }
83        (_, Some(_)) => {
84            // S is a negative integer.
85            crate::errors::domain_error(
86                m,
87                "not_less_than_zero",
88                ws,
89                "succ/2: successor must be non-negative",
90            );
91            0
92        }
93        _ => {
94            crate::errors::instantiation(m, "succ/2: at least one argument must be an integer");
95            0
96        }
97    }
98}
99
100/// `plus/3`: `Z = X + Y` over integers; any single unbound is solved for.
101#[unsafe(no_mangle)]
102pub extern "C" fn plg_rt_b_plus_3(m: *mut Machine, x: u64, y: u64, z: u64, site_id: u32) -> i32 {
103    let _site = crate::machine::ErrorSiteGuard::enter(m, site_id);
104    let m = mref(m);
105    let wx = int_of(m, m.deref(x));
106    let wy = int_of(m, m.deref(y));
107    let wz = int_of(m, m.deref(z));
108    let overflow = |m: &mut Machine| {
109        crate::errors::evaluation(m, "int_overflow", "plus/3: integer overflow");
110        0
111    };
112    match (wx, wy, wz) {
113        (Some(xv), Some(yv), _) => match xv.checked_add(yv) {
114            Some(r) => {
115                let rw = int_word(m, r);
116                unify(m, z, rw) as i32
117            }
118            None => overflow(m),
119        },
120        (Some(xv), _, Some(zv)) => match zv.checked_sub(xv) {
121            Some(r) => {
122                let rw = int_word(m, r);
123                unify(m, y, rw) as i32
124            }
125            None => overflow(m),
126        },
127        (_, Some(yv), Some(zv)) => match zv.checked_sub(yv) {
128            Some(r) => {
129                let rw = int_word(m, r);
130                unify(m, x, rw) as i32
131            }
132            None => overflow(m),
133        },
134        _ => {
135            crate::errors::instantiation(m, "plus/3: at least two arguments must be integers");
136            0
137        }
138    }
139}
140
141/// `unify_with_occurs_check/2`: like `=/2` but fails rather than build a
142/// cyclic term. Local iterative implementation — bindings are trailed so
143/// the caller's choice-point rewind undoes a partial unification.
144#[unsafe(no_mangle)]
145pub extern "C" fn plg_rt_b_unify_with_occurs_check_2(m: *mut Machine, a: u64, b: u64) -> i32 {
146    let m = mref(m);
147    unify_oc(m, a, b) as i32
148}
149
150/// Iterative occurs-checking unification over tagged heap words.
151fn unify_oc(m: &mut Machine, a: Word, b: Word) -> bool {
152    let mut work = vec![(a, b)];
153    while let Some((a, b)) = work.pop() {
154        let a = m.deref(a);
155        let b = m.deref(b);
156        if a == b {
157            continue;
158        }
159        match (tag_of(a), tag_of(b)) {
160            (TAG_REF, _) => {
161                if occurs(m, payload(a) as usize, b) {
162                    return false;
163                }
164                m.bind(payload(a) as usize, b);
165            }
166            (_, TAG_REF) => {
167                if occurs(m, payload(b) as usize, a) {
168                    return false;
169                }
170                m.bind(payload(b) as usize, a);
171            }
172            (TAG_ATOM, TAG_ATOM) | (TAG_INT, TAG_INT) => return false,
173            (TAG_BIG, TAG_BIG) => {
174                if m.heap[payload(a) as usize] as i64 != m.heap[payload(b) as usize] as i64 {
175                    return false;
176                }
177            }
178            (TAG_INT, TAG_BIG) => {
179                if int_value(a) != m.heap[payload(b) as usize] as i64 {
180                    return false;
181                }
182            }
183            (TAG_BIG, TAG_INT) => {
184                if m.heap[payload(a) as usize] as i64 != int_value(b) {
185                    return false;
186                }
187            }
188            (TAG_FLT, TAG_FLT) => {
189                if m.heap[payload(a) as usize] != m.heap[payload(b) as usize] {
190                    return false;
191                }
192            }
193            (TAG_STR, TAG_STR) => {
194                let ia = payload(a) as usize;
195                let ib = payload(b) as usize;
196                let (fa, na) = unpack_functor(m.heap[ia]);
197                let (fb, nb) = unpack_functor(m.heap[ib]);
198                if fa != fb || na != nb {
199                    return false;
200                }
201                for k in 0..na as usize {
202                    work.push((m.heap[ia + 1 + k], m.heap[ib + 1 + k]));
203                }
204            }
205            (TAG_LST, TAG_LST) => {
206                let ia = payload(a) as usize;
207                let ib = payload(b) as usize;
208                work.push((m.heap[ia + 1], m.heap[ib + 1]));
209                work.push((m.heap[ia], m.heap[ib]));
210            }
211            _ => return false,
212        }
213    }
214    true
215}
216
217/// Does the variable at heap index `var` occur within `term`? Iterative
218/// walk following bound refs; structures and lists are descended.
219fn occurs(m: &Machine, var: usize, term: Word) -> bool {
220    let mut work = vec![term];
221    while let Some(w) = work.pop() {
222        let w = m.deref(w);
223        match tag_of(w) {
224            TAG_REF if payload(w) as usize == var => return true,
225            TAG_REF => {}
226            TAG_STR => {
227                let idx = payload(w) as usize;
228                let (_, n) = unpack_functor(m.heap[idx]);
229                for k in 0..n as usize {
230                    work.push(m.heap[idx + 1 + k]);
231                }
232            }
233            TAG_LST => {
234                let idx = payload(w) as usize;
235                work.push(m.heap[idx]);
236                work.push(m.heap[idx + 1]);
237            }
238            _ => {}
239        }
240    }
241    false
242}
243
244/// `write/1`: print the term (v1 `term_to_string`), no trailing newline.
245#[unsafe(no_mangle)]
246pub extern "C" fn plg_rt_b_write_1(m: *mut Machine, term: u64) -> i32 {
247    let m = mref(m);
248    let s = term_to_string(m, term);
249    print!("{s}");
250    let _ = std::io::stdout().flush();
251    1
252}
253
254/// `writeln/1`: `write/1` followed by a newline.
255#[unsafe(no_mangle)]
256pub extern "C" fn plg_rt_b_writeln_1(m: *mut Machine, term: u64) -> i32 {
257    let m = mref(m);
258    let s = term_to_string(m, term);
259    println!("{s}");
260    1
261}
262
263/// `nl/0`: print a newline. Always succeeds.
264#[unsafe(no_mangle)]
265pub extern "C" fn plg_rt_b_nl_0(_m: *mut Machine) -> i32 {
266    println!();
267    1
268}
269
270#[cfg(test)]
271mod tests {
272    use super::*;
273    use crate::machine::NO_SITE;
274    use plg_shared::StringInterner;
275
276    fn machine() -> Box<Machine> {
277        Machine::new(StringInterner::new(), Vec::new())
278    }
279
280    // Thin wrappers: existing tests exercise behavior, not provenance.
281    fn succ(m: *mut Machine, x: u64, s: u64) -> i32 {
282        plg_rt_b_succ_2(m, x, s, NO_SITE)
283    }
284    fn plus(m: *mut Machine, x: u64, y: u64, z: u64) -> i32 {
285        plg_rt_b_plus_3(m, x, y, z, NO_SITE)
286    }
287
288    fn msg(m: &Machine) -> &str {
289        m.error.as_ref().unwrap().message.as_str()
290    }
291
292    fn str_term(m: &mut Machine, name: &str, args: &[Word]) -> Word {
293        let f = m.atoms.intern(name);
294        let idx = m.heap.len();
295        m.heap.push(pack_functor(f, args.len() as u32));
296        m.heap.extend_from_slice(args);
297        make(TAG_STR, idx as u64)
298    }
299
300    #[test]
301    fn succ_both_modes() {
302        let mut m = machine();
303        let x = m.new_var();
304        let mp = &mut *m as *mut Machine;
305        assert_eq!(succ(mp, make_int(3), x), 1);
306        assert_eq!(int_value(m.deref(x)), 4);
307
308        let y = m.new_var();
309        let mp = &mut *m as *mut Machine;
310        assert_eq!(succ(mp, y, make_int(5)), 1);
311        assert_eq!(int_value(m.deref(y)), 4);
312    }
313
314    #[test]
315    fn succ_zero_and_negative() {
316        let mut m = machine();
317        let y = m.new_var();
318        let mp = &mut *m as *mut Machine;
319        // succ(X, 0) fails (no predecessor)
320        assert_eq!(succ(mp, y, make_int(0)), 0);
321        assert!(m.error.is_none());
322
323        // succ(-1, X) → domain_error
324        let mut m = machine();
325        let x = m.new_var();
326        let mp = &mut *m as *mut Machine;
327        assert_eq!(succ(mp, make_int(-1), x), 0);
328        assert_eq!(
329            msg(&m),
330            "error(domain_error(not_less_than_zero, -1), succ/2: argument must be non-negative)"
331        );
332
333        // succ(X, Y) both unbound → instantiation
334        let mut m = machine();
335        let x = m.new_var();
336        let y = m.new_var();
337        let mp = &mut *m as *mut Machine;
338        assert_eq!(succ(mp, x, y), 0);
339        assert_eq!(
340            msg(&m),
341            "error(instantiation_error, succ/2: at least one argument must be an integer)"
342        );
343    }
344
345    #[test]
346    fn plus_three_modes_and_error() {
347        let mut m = machine();
348        let z = m.new_var();
349        let mp = &mut *m as *mut Machine;
350        assert_eq!(plus(mp, make_int(2), make_int(3), z), 1);
351        assert_eq!(int_value(m.deref(z)), 5);
352
353        let y = m.new_var();
354        let mp = &mut *m as *mut Machine;
355        assert_eq!(plus(mp, make_int(2), y, make_int(5)), 1);
356        assert_eq!(int_value(m.deref(y)), 3);
357
358        let x = m.new_var();
359        let mp = &mut *m as *mut Machine;
360        assert_eq!(plus(mp, x, make_int(3), make_int(5)), 1);
361        assert_eq!(int_value(m.deref(x)), 2);
362
363        // two unbound → instantiation
364        let mut m = machine();
365        let x = m.new_var();
366        let y = m.new_var();
367        let mp = &mut *m as *mut Machine;
368        assert_eq!(plus(mp, x, y, make_int(5)), 0);
369        assert_eq!(
370            msg(&m),
371            "error(instantiation_error, plus/3: at least two arguments must be integers)"
372        );
373    }
374
375    #[test]
376    fn occurs_check_rejects_cycle() {
377        let mut m = machine();
378        let x = m.new_var();
379        // unify_with_occurs_check(X, f(X)) must FAIL.
380        let fx = str_term(&mut m, "f", &[x]);
381        let mp = &mut *m as *mut Machine;
382        assert_eq!(plg_rt_b_unify_with_occurs_check_2(mp, x, fx), 0);
383        assert!(m.error.is_none());
384        // X still unbound (no binding committed).
385        assert_eq!(m.deref(x), x);
386    }
387
388    #[test]
389    fn occurs_check_allows_acyclic() {
390        let mut m = machine();
391        let x = m.new_var();
392        let a = make_atom(m.atoms.intern("a"));
393        let mp = &mut *m as *mut Machine;
394        assert_eq!(plg_rt_b_unify_with_occurs_check_2(mp, x, a), 1);
395        assert_eq!(m.deref(x), a);
396
397        // structural unify with shared subterm but no cycle
398        let mut m = machine();
399        let y = m.new_var();
400        let s1 = str_term(&mut m, "g", &[y, make_int(1)]);
401        let s2 = str_term(&mut m, "g", &[make_int(2), make_int(1)]);
402        let mp = &mut *m as *mut Machine;
403        assert_eq!(plg_rt_b_unify_with_occurs_check_2(mp, s1, s2), 1);
404        assert_eq!(int_value(m.deref(y)), 2);
405    }
406
407    #[test]
408    fn nl_always_succeeds() {
409        let mut m = machine();
410        let mp = &mut *m as *mut Machine;
411        assert_eq!(plg_rt_b_nl_0(mp), 1);
412    }
413
414    #[test]
415    fn write_returns_success() {
416        // We can't easily capture stdout here, but the call must succeed
417        // and not mutate the heap-visible term.
418        let mut m = machine();
419        let s = str_term(&mut m, "+", &[make_int(1), make_int(2)]);
420        let mp = &mut *m as *mut Machine;
421        assert_eq!(plg_rt_b_write_1(mp, s), 1);
422        assert_eq!(plg_rt_b_writeln_1(mp, s), 1);
423        // sanity: rendering matches v1 infix form
424        assert_eq!(term_to_string(&m, s), "1 + 2");
425    }
426}