nx_lpo_test.nx source

1// nx_lpo_test.nx -- LPO smoke covering all four verdicts + each rule. 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" 9import "nx_lpo.nx" 10 11const SYM_A: nx_int = 100 // const, prec 10 12const SYM_B: nx_int = 101 // const, prec 11 13const SYM_F: nx_int = 200 // unary, prec 20 14const SYM_G: nx_int = 201 // unary, prec 21 15const SYM_H: nx_int = 250 // binary, prec 30 16 17const VAR_X: nx_int = 0 18const VAR_Y: nx_int = 1 19 20func mk_unary(sym: nx_int, child: *Term) -> *Term { 21 let buf: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term 22 buf.kind = child.kind; buf.sym = child.sym 23 buf.n_args = child.n_args; buf.args = child.args 24 return nx_term_app(sym, 1, buf) 25} 26 27func mk_binary(sym: nx_int, c0: *Term, c1: *Term) -> *Term { 28 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term 29 let a0: *Term = args 30 a0.kind = c0.kind; a0.sym = c0.sym; a0.n_args = c0.n_args; a0.args = c0.args 31 let a1: *Term = ((args as nx_int) + NX_TERM_BYTES) as *Term 32 a1.kind = c1.kind; a1.sym = c1.sym; a1.n_args = c1.n_args; a1.args = c1.args 33 return nx_term_app(sym, 2, args) 34} 35 36func mk_state() -> *KboState { 37 let st: *KboState = nx_kbo_new(1) 38 let _r1: *NxResult = nx_kbo_register(st, SYM_A, 1, 10, 0) 39 let _r2: *NxResult = nx_kbo_register(st, SYM_B, 1, 11, 0) 40 let _r3: *NxResult = nx_kbo_register(st, SYM_F, 1, 20, 1) 41 let _r4: *NxResult = nx_kbo_register(st, SYM_G, 1, 21, 1) 42 let _r5: *NxResult = nx_kbo_register(st, SYM_H, 1, 30, 2) 43 return st 44} 45 46func report(name: *u8, expected: nx_int, actual: nx_int) -> nx_int { 47 print(" " as *u8); print(name); print(" -> " as *u8) 48 print(nx_lpo_verdict_name(actual)) 49 if actual == expected { println(" PASS" as *u8); return 0 } 50 print(" (expected " as *u8); print(nx_lpo_verdict_name(expected)); println(") FAIL" as *u8) 51 return 1 52} 53 54func main() -> nx_exit { 55 println("=== LPO smoke ===" as *u8) 56 let st: *KboState = mk_state() 57 var fails: nx_int = 0 58 59 // ---------- Test 1: LPO1 -- proper subterm ------------------- 60 // f(a) vs a -- a is proper subterm of f(a), so f(a) > a. 61 let t1a: *Term = mk_unary(SYM_F, nx_term_const(SYM_A)) 62 let t1b: *Term = nx_term_const(SYM_A) 63 fails = fails + report("1. LPO1 f(a) vs a" as *u8, NX_LPO_GT, nx_lpo_compare(st, t1a, t1b)) 64 65 // ---------- Test 2: EQ on identical -------------------------- 66 let t2a: *Term = mk_unary(SYM_F, nx_term_const(SYM_B)) 67 let t2b: *Term = mk_unary(SYM_F, nx_term_const(SYM_B)) 68 fails = fails + report("2. EQ f(b) vs f(b)" as *u8, NX_LPO_EQ, nx_lpo_compare(st, t2a, t2b)) 69 70 // ---------- Test 3: LPO1 mirror -- LT ------------------------ 71 fails = fails + report("3. LPO1m a vs f(a)" as *u8, NX_LPO_LT, nx_lpo_compare(st, t1b, t1a)) 72 73 // ---------- Test 4: LPO2 -- precedence + dominates args ------ 74 // g(a) vs f(a): prec g > f, and g(a) > a (subterm). So GT. 75 let t4a: *Term = mk_unary(SYM_G, nx_term_const(SYM_A)) 76 let t4b: *Term = mk_unary(SYM_F, nx_term_const(SYM_A)) 77 fails = fails + report("4. LPO2 g(a) vs f(a)" as *u8, NX_LPO_GT, nx_lpo_compare(st, t4a, t4b)) 78 79 // ---------- Test 5: LPO3 -- same head, lex on args ----------- 80 // h(b, a) vs h(a, a): same head, first arg b > a (subterm gives 81 // INCOMP between two consts; but precedence b > a so LPO2 fires 82 // on the arg pair: g(a) actually wait, b and a are CONSTANTS. 83 // For LPO between two constants: nx_term_eq says no, both non-var, 84 // neither is a subterm of the other (constants have no subterms), 85 // precedence b > a so LPO2 fires (g(a) wait no, just two consts). 86 // For LPO2 with constants: f > g and "for all j in args of t" -- 87 // t has no args so the "for all" is vacuously true. -> GT. 88 // So b > a in LPO. Then h(b,a) > h(a,a) since arg-0 differs and 89 // h(b,a) > h(a,k) for k=1 (a vs a is EQ, not GT, so the "remaining 90 // args" check fails... hmm). 91 // 92 // Actually the LPO3 remaining-args check requires GT, not just 93 // not-LT. Let me re-check. For h(b,a) vs h(a,a): 94 // arg 0: b vs a -> GT (LPO2 with vacuous all-args) 95 // remaining (i=1..1): need h(b,a) > a. Subterm check: 96 // a is a proper subterm of h(b,a) (it's arg-1 of h, in args of h). 97 // So h(b,a) > a by LPO1 -> GT. 98 // -> overall GT. 99 let t5a: *Term = mk_binary(SYM_H, nx_term_const(SYM_B), nx_term_const(SYM_A)) 100 let t5b: *Term = mk_binary(SYM_H, nx_term_const(SYM_A), nx_term_const(SYM_A)) 101 fails = fails + report("5. LPO3 h(b,a) vs h(a,a)" as *u8, NX_LPO_GT, nx_lpo_compare(st, t5a, t5b)) 102 103 // ---------- Test 6: INCOMP -- different vars ----------------- 104 let t6a: *Term = nx_term_var(VAR_X) 105 let t6b: *Term = nx_term_var(VAR_Y) 106 fails = fails + report("6. INCOMP X vs Y" as *u8, NX_LPO_INCOMP, nx_lpo_compare(st, t6a, t6b)) 107 108 // ---------- Test 7: var inside non-var ----------------------- 109 // f(X) vs X -- X occurs in f(X), so f(X) > X. 110 let t7a: *Term = mk_unary(SYM_F, nx_term_var(VAR_X)) 111 let t7b: *Term = nx_term_var(VAR_X) 112 fails = fails + report("7. var-in f(X) vs X" as *u8, NX_LPO_GT, nx_lpo_compare(st, t7a, t7b)) 113 114 // ---------- Test 8: var not inside --------------------------- 115 // f(a) vs Y -- Y doesn't occur in f(a) -> INCOMP 116 let t8b: *Term = nx_term_var(VAR_Y) 117 fails = fails + report("8. INCOMP f(a) vs Y" as *u8, NX_LPO_INCOMP, nx_lpo_compare(st, t1a, t8b)) 118 119 // ---------- Test 9: LPO2 with multi-arg ---------------------- 120 // g(a) vs h(a, a): prec g (21) < h (30) -- mirror of LPO2. 121 // h(a,a) > g(a) iff h(a,a) > arg of g(a) which is a. By LPO1, yes. 122 // -> overall LT (from g(a)'s perspective). 123 let t9a: *Term = mk_unary(SYM_G, nx_term_const(SYM_A)) 124 let t9b: *Term = mk_binary(SYM_H, nx_term_const(SYM_A), nx_term_const(SYM_A)) 125 fails = fails + report("9. LPO2m g(a) vs h(a,a)" as *u8, NX_LPO_LT, nx_lpo_compare(st, t9a, t9b)) 126 127 println("" as *u8) 128 if fails == 0 { 129 println("=== ALL 9 LPO tests PASS ===" as *u8) 130 return 0 131 } 132 print("=== " as *u8); print_i64(fails); println(" LPO tests FAILED ===" as *u8) 133 return 1 134}