`nx_unify_test.nx` source

1// nx_unify_test.nx -- Robinson unification smoke.
2
3import "nx_syscalls.nx"
4import "nx_runtime.nx"
5import "nx_tier.nx"
6import "nx_result.nx"
7import "nx_unify.nx"
8
9// Symbol IDs (substitute for a real symbol table)
10const SYM_A: nx_int = 100
11const SYM_B: nx_int = 101
12const SYM_F: nx_int = 200
13const SYM_G: nx_int = 201
14
15// Var IDs
16const VAR_X: nx_int = 1
17const VAR_Y: nx_int = 2
18const VAR_Z: nx_int = 3
19
20func main() -> nx_exit {
21    println("=== Robinson unification smoke ===" as *u8)
22
23    // === Test 1: unify(x, a) -> {x -> a}  =============================
24    let t1a: *Term = nx_term_var(VAR_X)
25    let t1b: *Term = nx_term_const(SYM_A)
26    let s1: *Subst = nx_subst_new()
27    let r1: *NxResult = nx_unify(t1a, t1b, s1)
28    if nx_result_is_err(r1) == 1 { println("FAIL: t1 expected OK" as *u8); return 1 }
29    if s1.n != 1 { return 2 }
30    let bound: *Term = nx_subst_lookup(s1, VAR_X)
31    if (bound as nx_int) == 0 { return 3 }
32    if bound.kind != NX_TERM_CONST { return 4 }
33    if bound.sym != SYM_A { return 5 }
34    println("  Test 1 unify(x, a) -> {x -> a}  PASS" as *u8)
35
36    // === Test 2: unify(f(x), f(a)) -> {x -> a}  =======================
37    let arg2a: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
38    arg2a.kind = NX_TERM_VAR; arg2a.sym = VAR_X; arg2a.n_args = 0; arg2a.args = 0 as *Term
39    let t2a: *Term = nx_term_app(SYM_F, 1, arg2a)
40
41    let arg2b: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
42    arg2b.kind = NX_TERM_CONST; arg2b.sym = SYM_A; arg2b.n_args = 0; arg2b.args = 0 as *Term
43    let t2b: *Term = nx_term_app(SYM_F, 1, arg2b)
44
45    let s2: *Subst = nx_subst_new()
46    let r2: *NxResult = nx_unify(t2a, t2b, s2)
47    if nx_result_is_err(r2) == 1 { println("FAIL: t2 expected OK" as *u8); return 10 }
48    println("  Test 2 unify(f(x), f(a)) -> {x -> a}  PASS" as *u8)
49
50    // === Test 3: unify(a, b) -> ERR  ==================================
51    let t3a: *Term = nx_term_const(SYM_A)
52    let t3b: *Term = nx_term_const(SYM_B)
53    let s3: *Subst = nx_subst_new()
54    let r3: *NxResult = nx_unify(t3a, t3b, s3)
55    if nx_result_is_err(r3) == 0 { println("FAIL: t3 expected ERR" as *u8); return 20 }
56    if nx_result_err_code(r3) != NX_ERR_TAG_MISMATCH { return 21 }
57    println("  Test 3 unify(a, b) -> ERR=TAG_MISMATCH  PASS" as *u8)
58
59    // === Test 4: unify(x, f(x)) -> ERR occurs check  ==================
60    let arg4: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
61    arg4.kind = NX_TERM_VAR; arg4.sym = VAR_X; arg4.n_args = 0; arg4.args = 0 as *Term
62    let t4b: *Term = nx_term_app(SYM_F, 1, arg4)
63    let t4a: *Term = nx_term_var(VAR_X)
64    let s4: *Subst = nx_subst_new()
65    let r4: *NxResult = nx_unify(t4a, t4b, s4)
66    if nx_result_is_err(r4) == 0 { println("FAIL: t4 expected occurs-check ERR" as *u8); return 30 }
67    if nx_result_err_code(r4) != NX_ERR_INVALID_STATE { return 31 }
68    println("  Test 4 unify(x, f(x)) -> ERR=INVALID_STATE (occurs check)  PASS" as *u8)
69
70    // === Test 5: unify(f(x, b), f(a, y)) -> {x -> a, y -> b}  =========
71    let args5a: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term
72    let arg5a0: *Term = args5a
73    arg5a0.kind = NX_TERM_VAR; arg5a0.sym = VAR_X; arg5a0.n_args = 0; arg5a0.args = 0 as *Term
74    let arg5a1: *Term = ((args5a as nx_int) + NX_TERM_BYTES) as *Term
75    arg5a1.kind = NX_TERM_CONST; arg5a1.sym = SYM_B; arg5a1.n_args = 0; arg5a1.args = 0 as *Term
76    let t5a: *Term = nx_term_app(SYM_F, 2, args5a)
77
78    let args5b: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term
79    let arg5b0: *Term = args5b
80    arg5b0.kind = NX_TERM_CONST; arg5b0.sym = SYM_A; arg5b0.n_args = 0; arg5b0.args = 0 as *Term
81    let arg5b1: *Term = ((args5b as nx_int) + NX_TERM_BYTES) as *Term
82    arg5b1.kind = NX_TERM_VAR; arg5b1.sym = VAR_Y; arg5b1.n_args = 0; arg5b1.args = 0 as *Term
83    let t5b: *Term = nx_term_app(SYM_F, 2, args5b)
84
85    let s5: *Subst = nx_subst_new()
86    let r5: *NxResult = nx_unify(t5a, t5b, s5)
87    if nx_result_is_err(r5) == 1 { println("FAIL: t5 expected OK" as *u8); return 40 }
88    if s5.n != 2 { return 41 }
89    println("  Test 5 unify(f(x, b), f(a, y)) -> {x -> a, y -> b}  PASS" as *u8)
90
91    println("" as *u8)
92    println("=== ALL 5 Robinson unification tests PASS ===" as *u8)
93    return 0
94}
nx_unify_test.nx source

`nx_unify_test.nx` source
