nx_tptp_test.nx source
↩ module page · 55 lines · 1973 B
1// nx_tptp_test.nx -- smoke for the TPTP foundation reader.
2
3import "nx_syscalls.nx"
4import "nx_runtime.nx"
5import "nx_tier.nx"
6import "nx_result.nx"
7import "nx_tptp.nx"
8
9func main() -> nx_exit {
10 println("=== TPTP foundation reader smoke ===" as *u8)
11
12 // Inline TPTP-format buffer (3 FOF statements + 1 CNF).
13 let src: *u8 = "fof(ax1, axiom, p(X) | q(X)). fof(my_hyp, hypothesis, r(a)). fof(goal_xyz, conjecture, p(b)). cnf(c1, axiom, ~p(X) | q(X))." as *u8
14 var n: nx_int = 0
15 while src[n] != 0 { n = n + 1 }
16 print(" input bytes: " as *u8); print_i64(n); println("" as *u8)
17
18 let r: *TptpReader = nx_tptp_reader_new(src, n)
19 var count: nx_int = 0
20 while count < 16 {
21 let res: *NxResult = nx_tptp_read_stmt(r)
22 if nx_result_is_err(res) == 1 {
23 count = 16 // break
24 }
25 if nx_result_is_err(res) == 0 { count = count + 1 }
26 }
27
28 let n_stmts: nx_int = nx_tptp_n_stmts(r)
29 print(" parsed statements: " as *u8); print_i64(n_stmts); println("" as *u8)
30 if n_stmts < 3 { return 1 } // expect at least 3 (CNF parser may differ)
31
32 // Inspect each
33 var i: nx_int = 0
34 while i < n_stmts {
35 let s: *TptpStmt = nx_tptp_stmt_at(r, i)
36 print(" [" as *u8); print_i64(i)
37 print("] kind=" as *u8); print_i64(s.kind)
38 print(" name='" as *u8); print(s.name); print("'" as *u8)
39 print(" role=" as *u8); print(nx_tptp_role_name(s.role)); println("" as *u8)
40 i = i + 1
41 }
42
43 // Verify specific statements
44 let s0: *TptpStmt = nx_tptp_stmt_at(r, 0)
45 if s0.kind != NX_TPTP_KIND_FOF { return 10 }
46 if s0.role != NX_TPTP_ROLE_AXIOM { return 11 }
47
48 let s2: *TptpStmt = nx_tptp_stmt_at(r, 2)
49 if s2.role != NX_TPTP_ROLE_CONJECTURE { return 12 }
50
51 println("" as *u8)
52 println("=== TPTP foundation reader smoke PASS ===" as *u8)
53 println("(formula parser + unification + resolution queued for next sessions)" as *u8)
54 return 0
55}