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