nx_fof_parse_test.nx source
↩ module page · 133 lines · 5420 B
1// nx_fof_parse_test.nx -- FOF parser smoke covering each connective +
2// quantifier + nesting + precedence.
3
4import "nx_syscalls.nx"
5import "nx_runtime.nx"
6import "nx_tier.nx"
7import "nx_str.nx"
8import "nx_result.nx"
9import "nx_unify.nx"
10import "nx_tptp_symtab.nx"
11import "nx_tptp_term.nx"
12import "nx_fof.nx"
13import "nx_fof_parse.nx"
14
15const SYM_EQ: nx_int = 50
16
17func mk_input(s: *u8) -> *u8 {
18 let len: nx_int = nx_str_len(s)
19 let buf: *u8 = sys_mmap((len + 1) as i64)
20 var i: nx_int = 0
21 while i < len { buf[i] = s[i]; i = i + 1 }
22 buf[len] = 0
23 return buf
24}
25
26func parse(input: *u8) -> *Fof {
27 let len: nx_int = nx_str_len(input)
28 let buf: *u8 = mk_input(input)
29 let st: *TptpSymtab = nx_tptp_symtab_new()
30 let pos: *nx_int = sys_mmap(8) as *nx_int
31 pos[0] = 0
32 return nx_fof_parse(buf, len, pos, st, SYM_EQ)
33}
34
35func report(name: *u8, expected_kind: nx_int, actual: *Fof) -> nx_int {
36 print(" " as *u8); print(name); print(" -> " as *u8)
37 if (actual as nx_int) == 0 { println("NULL FAIL" as *u8); return 1 }
38 print(nx_fof_kind_name(actual.kind))
39 if actual.kind == expected_kind {
40 println(" PASS" as *u8); return 0
41 }
42 print(" (expected " as *u8); print(nx_fof_kind_name(expected_kind)); println(") FAIL" as *u8)
43 return 1
44}
45
46func main() -> nx_exit {
47 println("=== FOF parser smoke ===" as *u8)
48 var fails: nx_int = 0
49
50 // Atoms / unitary
51 fails = fails + report("1. p(a)" as *u8, NX_FOF_ATOM, parse("p(a)" as *u8))
52 fails = fails + report("2. ~p(a)" as *u8, NX_FOF_NEG, parse("~p(a)" as *u8))
53
54 // Binary connectives
55 fails = fails + report("3. p & q" as *u8, NX_FOF_AND, parse("p(a) & q(a)" as *u8))
56 fails = fails + report("4. p | q" as *u8, NX_FOF_OR, parse("p(a) | q(a)" as *u8))
57 fails = fails + report("5. p => q" as *u8, NX_FOF_IMP, parse("p(a) => q(a)" as *u8))
58 fails = fails + report("6. p <=> q" as *u8, NX_FOF_IFF, parse("p(a) <=> q(a)" as *u8))
59
60 // Quantifiers
61 fails = fails + report("7. ![X]: p(X)" as *u8, NX_FOF_FORALL, parse("![X]: p(X)" as *u8))
62 fails = fails + report("8. ?[X]: p(X)" as *u8, NX_FOF_EXISTS, parse("?[X]: p(X)" as *u8))
63
64 // Multi-var quantifier nests as FORALL chain
65 let f9: *Fof = parse("![X, Y]: p(X)" as *u8)
66 if (f9 as nx_int) == 0 {
67 println("9. ![X,Y]: p(X) -> NULL FAIL" as *u8); fails = fails + 1
68 } else {
69 if f9.kind == NX_FOF_FORALL {
70 if f9.left.kind == NX_FOF_FORALL {
71 if f9.left.left.kind == NX_FOF_ATOM {
72 println("9. ![X,Y]: p(X) -> FORALL(FORALL(ATOM)) PASS" as *u8)
73 } else { println("9. inner kind wrong FAIL" as *u8); fails = fails + 1 }
74 } else { println("9. middle kind wrong FAIL" as *u8); fails = fails + 1 }
75 } else { println("9. outer kind wrong FAIL" as *u8); fails = fails + 1 }
76 }
77
78 // Inequality lifts to NEG of equality
79 let f10: *Fof = parse("a != b" as *u8)
80 if (f10 as nx_int) == 0 {
81 println("10. a != b -> NULL FAIL" as *u8); fails = fails + 1
82 } else {
83 if f10.kind == NX_FOF_NEG {
84 if f10.left.kind == NX_FOF_ATOM {
85 println("10. a != b -> NEG(ATOM) PASS" as *u8)
86 } else { println("10. inner wrong FAIL" as *u8); fails = fails + 1 }
87 } else { println("10. outer not NEG FAIL" as *u8); fails = fails + 1 }
88 }
89
90 // Precedence: a & b | c parses as (a & b) | c (& binds tighter than |)
91 let f11: *Fof = parse("p(a) & q(a) | r(a)" as *u8)
92 if (f11 as nx_int) == 0 {
93 println("11. p & q | r -> NULL FAIL" as *u8); fails = fails + 1
94 } else {
95 if f11.kind == NX_FOF_OR {
96 if f11.left.kind == NX_FOF_AND {
97 println("11. p & q | r -> OR(AND(p,q), r) PASS" as *u8)
98 } else { println("11. left not AND -- precedence wrong FAIL" as *u8); fails = fails + 1 }
99 } else { println("11. top not OR FAIL" as *u8); fails = fails + 1 }
100 }
101
102 // Parenthesised override: (p | q) & r
103 let f12: *Fof = parse("(p(a) | q(a)) & r(a)" as *u8)
104 if (f12 as nx_int) == 0 {
105 println("12. (p|q) & r -> NULL FAIL" as *u8); fails = fails + 1
106 } else {
107 if f12.kind == NX_FOF_AND {
108 if f12.left.kind == NX_FOF_OR {
109 println("12. (p|q) & r -> AND(OR(p,q), r) PASS" as *u8)
110 } else { println("12. left not OR -- parens broken FAIL" as *u8); fails = fails + 1 }
111 } else { println("12. top not AND FAIL" as *u8); fails = fails + 1 }
112 }
113
114 // Nested quantifier + binary: ![X]: (p(X) => q(X))
115 let f13: *Fof = parse("![X]: (p(X) => q(X))" as *u8)
116 if (f13 as nx_int) == 0 {
117 println("13. ![X]: (p=>q) -> NULL FAIL" as *u8); fails = fails + 1
118 } else {
119 if f13.kind == NX_FOF_FORALL {
120 if f13.left.kind == NX_FOF_IMP {
121 println("13. ![X]: (p=>q) -> FORALL(IMP) PASS" as *u8)
122 } else { println("13. body not IMP FAIL" as *u8); fails = fails + 1 }
123 } else { println("13. outer not FORALL FAIL" as *u8); fails = fails + 1 }
124 }
125
126 println("" as *u8)
127 if fails == 0 {
128 println("=== ALL 13 FOF parser tests PASS ===" as *u8)
129 return 0
130 }
131 print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
132 return 1
133}