nx_term_order_test.nx source
↩ module page · 157 lines · 6759 B
1// nx_term_order_test.nx -- KBO smoke covering all four verdicts.
2
3import "nx_syscalls.nx"
4import "nx_runtime.nx"
5import "nx_tier.nx"
6import "nx_result.nx"
7import "nx_unify.nx"
8import "nx_term_order.nx"
9
10// Symbol IDs. Convention: constants 100-199, unary fns 200-249,
11// binary fns 250-299. Higher precedence wins.
12const SYM_A: nx_int = 100 // constant, weight 1, prec 10
13const SYM_B: nx_int = 101 // constant, weight 1, prec 11
14const SYM_C: nx_int = 102 // constant, weight 1, prec 12
15const SYM_F: nx_int = 200 // unary, weight 1, prec 20
16const SYM_G: nx_int = 201 // unary, weight 1, prec 21
17const SYM_H: nx_int = 250 // binary, weight 1, prec 30
18
19// Var ids
20const VAR_X: nx_int = 0
21const VAR_Y: nx_int = 1
22const NX_MAX_VAR: nx_int = 4
23
24// ---------- helpers ------------------------------------------------
25func mk_unary(sym: nx_int, child: *Term) -> *Term {
26 let buf: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
27 buf.kind = child.kind
28 buf.sym = child.sym
29 buf.n_args = child.n_args
30 buf.args = child.args
31 return nx_term_app(sym, 1, buf)
32}
33
34func mk_binary(sym: nx_int, c0: *Term, c1: *Term) -> *Term {
35 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term
36 let a0: *Term = args
37 a0.kind = c0.kind; a0.sym = c0.sym; a0.n_args = c0.n_args; a0.args = c0.args
38 let a1: *Term = ((args as nx_int) + NX_TERM_BYTES) as *Term
39 a1.kind = c1.kind; a1.sym = c1.sym; a1.n_args = c1.n_args; a1.args = c1.args
40 return nx_term_app(sym, 2, args)
41}
42
43func report(name: *u8, expected: nx_int, actual: nx_int) -> nx_int {
44 print(" " as *u8)
45 print(name)
46 print(" -> " as *u8)
47 print(nx_kbo_verdict_name(actual))
48 if actual == expected {
49 println(" PASS" as *u8)
50 return 0
51 }
52 print(" (expected " as *u8)
53 print(nx_kbo_verdict_name(expected))
54 println(") FAIL" as *u8)
55 return 1
56}
57
58func main() -> nx_exit {
59 println("=== KBO smoke ===" as *u8)
60
61 // Register the symbol table with admissible weights + precedences.
62 let st: *KboState = nx_kbo_new(1)
63 let _r1: *NxResult = nx_kbo_register(st, SYM_A, 1, 10, 0)
64 let _r2: *NxResult = nx_kbo_register(st, SYM_B, 1, 11, 0)
65 let _r3: *NxResult = nx_kbo_register(st, SYM_C, 1, 12, 0)
66 let _r4: *NxResult = nx_kbo_register(st, SYM_F, 1, 20, 1)
67 let _r5: *NxResult = nx_kbo_register(st, SYM_G, 1, 21, 1)
68 let _r6: *NxResult = nx_kbo_register(st, SYM_H, 1, 30, 2)
69
70 // Admissibility must hold (w_0 = 1, all constants w = 1, no zero-weight unary).
71 let radm: *NxResult = nx_kbo_check_admissibility(st)
72 if nx_result_is_err(radm) == 1 {
73 println("FAIL: admissibility check rejected an admissible spec" as *u8)
74 return 100
75 }
76 print(" admissibility ok, declared=" as *u8); print_i64(nx_result_unwrap(radm)); println("" as *u8)
77
78 var fails: nx_int = 0
79
80 // ---------- Test 1: weight drives GT -------------------------
81 // f(f(a)) vs a -- weights 3 vs 1. Vars equal (none on either side).
82 // Expected GT.
83 let t1a_inner: *Term = nx_term_const(SYM_A)
84 let t1a_fa: *Term = mk_unary(SYM_F, t1a_inner)
85 let t1a_ffa: *Term = mk_unary(SYM_F, t1a_fa)
86 let t1b: *Term = nx_term_const(SYM_A)
87 let v1: nx_int = nx_kbo_compare(st, t1a_ffa, t1b, NX_MAX_VAR)
88 fails = fails + report("1. f(f(a)) vs a" as *u8, NX_KBO_GT, v1)
89
90 // ---------- Test 2: EQ on identical terms --------------------
91 let t2a: *Term = mk_unary(SYM_F, nx_term_const(SYM_B))
92 let t2b: *Term = mk_unary(SYM_F, nx_term_const(SYM_B))
93 let v2: nx_int = nx_kbo_compare(st, t2a, t2b, NX_MAX_VAR)
94 fails = fails + report("2. f(b) vs f(b)" as *u8, NX_KBO_EQ, v2)
95
96 // ---------- Test 3: LT (reverse of test 1) -------------------
97 let v3: nx_int = nx_kbo_compare(st, t1b, t1a_ffa, NX_MAX_VAR)
98 fails = fails + report("3. a vs f(f(a))" as *u8, NX_KBO_LT, v3)
99
100 // ---------- Test 4: INCOMP on var-mismatch -------------------
101 // f(x) vs g(y) -- equal weights (2 each), var sets differ -> INCOMP.
102 let t4a: *Term = mk_unary(SYM_F, nx_term_var(VAR_X))
103 let t4b: *Term = mk_unary(SYM_G, nx_term_var(VAR_Y))
104 let v4: nx_int = nx_kbo_compare(st, t4a, t4b, NX_MAX_VAR)
105 fails = fails + report("4. f(x) vs g(y)" as *u8, NX_KBO_INCOMP, v4)
106
107 // ---------- Test 5: precedence breaks tie --------------------
108 // g(a) vs f(a) -- equal weights (2), same vars (none), prec g > f
109 let t5a: *Term = mk_unary(SYM_G, nx_term_const(SYM_A))
110 let t5b: *Term = mk_unary(SYM_F, nx_term_const(SYM_A))
111 let v5: nx_int = nx_kbo_compare(st, t5a, t5b, NX_MAX_VAR)
112 fails = fails + report("5. g(a) vs f(a)" as *u8, NX_KBO_GT, v5)
113
114 // ---------- Test 6: lex on equal heads -----------------------
115 // h(b, a) vs h(a, a) -- equal weights (3 each), same head h,
116 // first arg b > a in precedence -> GT.
117 let t6a: *Term = mk_binary(SYM_H, nx_term_const(SYM_B), nx_term_const(SYM_A))
118 let t6b: *Term = mk_binary(SYM_H, nx_term_const(SYM_A), nx_term_const(SYM_A))
119 let v6: nx_int = nx_kbo_compare(st, t6a, t6b, NX_MAX_VAR)
120 fails = fails + report("6. h(b,a) vs h(a,a)" as *u8, NX_KBO_GT, v6)
121
122 // ---------- Test 7: var-dominance gates a weight-driven GT ---
123 // f(x) vs y -- weights 2 vs 1, but var counts on lhs (x=1, y=0)
124 // do NOT dominate rhs (x=0, y=1). Expected INCOMP.
125 let t7a: *Term = mk_unary(SYM_F, nx_term_var(VAR_X))
126 let t7b: *Term = nx_term_var(VAR_Y)
127 let v7: nx_int = nx_kbo_compare(st, t7a, t7b, NX_MAX_VAR)
128 fails = fails + report("7. f(x) vs y" as *u8, NX_KBO_INCOMP, v7)
129
130 // ---------- Test 8: var-dominance allows weight-driven GT ----
131 // f(x) vs x -- weights 2 vs 1, var counts match (x=1 both).
132 // Expected GT.
133 let t8a: *Term = mk_unary(SYM_F, nx_term_var(VAR_X))
134 let t8b: *Term = nx_term_var(VAR_X)
135 let v8: nx_int = nx_kbo_compare(st, t8a, t8b, NX_MAX_VAR)
136 fails = fails + report("8. f(x) vs x" as *u8, NX_KBO_GT, v8)
137
138 // ---------- Test 9: admissibility negative case --------------
139 // Register an under-weight constant -- should reject.
140 let st_bad: *KboState = nx_kbo_new(2) // require w_0 = 2
141 let _rb1: *NxResult = nx_kbo_register(st_bad, SYM_A, 1, 10, 0) // 1 < w_0
142 let rbad: *NxResult = nx_kbo_check_admissibility(st_bad)
143 if nx_result_is_err(rbad) == 0 {
144 println("9. admissibility(bad constant) -> ACCEPTED FAIL" as *u8)
145 fails = fails + 1
146 } else {
147 println("9. admissibility(bad constant) -> rejected PASS" as *u8)
148 }
149
150 println("" as *u8)
151 if fails == 0 {
152 println("=== ALL 9 KBO tests PASS ===" as *u8)
153 return 0
154 }
155 print("=== " as *u8); print_i64(fails); println(" KBO tests FAILED ===" as *u8)
156 return 1
157}