nx_tptp.nx source
↩ module page · 253 lines · 9218 B
1// nx_tptp.nx -- TPTP (Thousands of Problems for Theorem Provers) format
2// reader. Foundation for CASC competition entry.
3//
4// Per user 2026-05-14: "we need to win our qed system must be a leap
5// forward from the bits up". TPTP at tptp.org defines the canonical
6// benchmark format every CASC entrant must read. This is bits-up:
7// no external Vampire/E/Otter dependency; pure NishiLang substrate.
8//
9// TPTP FOF format (subset supported here):
10// fof(<name>, <role>, <formula>).
11// where:
12// <name> = identifier (a000_1, my_axiom, etc.)
13// <role> = axiom | hypothesis | conjecture | lemma | definition | ...
14// <formula> = first-order logic expression
15//
16// CNF format:
17// cnf(<name>, <role>, <literal-disjunction>).
18//
19// Subset implemented today: name + role extraction. Formula parsing
20// queued for nx_tptp_formula.nx (next session).
21
22// nx_safety_envelope:
23// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
24// sil_target: SIL1
25// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
26// verdict: NOT_YET_EVALUATED
27
28import "nx_syscalls.nx"
29import "nx_runtime.nx"
30import "nx_tier.nx"
31import "nx_str.nx"
32import "nx_result.nx"
33
34// ===== Role enum (sealed) ===========================================
35const NX_TPTP_ROLE_AXIOM: nx_int = 1
36const NX_TPTP_ROLE_HYPOTHESIS: nx_int = 2
37const NX_TPTP_ROLE_CONJECTURE: nx_int = 3
38const NX_TPTP_ROLE_LEMMA: nx_int = 4
39const NX_TPTP_ROLE_DEFINITION: nx_int = 5
40const NX_TPTP_ROLE_NEG_CONJ: nx_int = 6
41const NX_TPTP_ROLE_PLAIN: nx_int = 7
42const NX_TPTP_ROLE_UNKNOWN: nx_int = 0
43
44func nx_tptp_role_name(r: nx_int) -> *u8 {
45 if r == NX_TPTP_ROLE_AXIOM { return "axiom" as *u8 }
46 if r == NX_TPTP_ROLE_HYPOTHESIS { return "hypothesis" as *u8 }
47 if r == NX_TPTP_ROLE_CONJECTURE { return "conjecture" as *u8 }
48 if r == NX_TPTP_ROLE_LEMMA { return "lemma" as *u8 }
49 if r == NX_TPTP_ROLE_DEFINITION { return "definition" as *u8 }
50 if r == NX_TPTP_ROLE_NEG_CONJ { return "negated_conjecture" as *u8 }
51 if r == NX_TPTP_ROLE_PLAIN { return "plain" as *u8 }
52 return "unknown" as *u8
53}
54
55func nx_tptp_role_from_str(s: *u8) -> nx_int {
56 if nx_str_eq(s, "axiom" as *u8) == 1 { return NX_TPTP_ROLE_AXIOM }
57 if nx_str_eq(s, "hypothesis" as *u8) == 1 { return NX_TPTP_ROLE_HYPOTHESIS }
58 if nx_str_eq(s, "conjecture" as *u8) == 1 { return NX_TPTP_ROLE_CONJECTURE }
59 if nx_str_eq(s, "lemma" as *u8) == 1 { return NX_TPTP_ROLE_LEMMA }
60 if nx_str_eq(s, "definition" as *u8) == 1 { return NX_TPTP_ROLE_DEFINITION }
61 if nx_str_eq(s, "negated_conjecture" as *u8) == 1 { return NX_TPTP_ROLE_NEG_CONJ }
62 if nx_str_eq(s, "plain" as *u8) == 1 { return NX_TPTP_ROLE_PLAIN }
63 return NX_TPTP_ROLE_UNKNOWN
64}
65
66// ===== Statement form: kind + name + role + raw formula =============
67const NX_TPTP_KIND_FOF: nx_int = 1
68const NX_TPTP_KIND_CNF: nx_int = 2
69const NX_TPTP_KIND_THF: nx_int = 3
70const NX_TPTP_KIND_TFF: nx_int = 4
71
72struct TptpStmt {
73 kind: nx_int,
74 name: *u8,
75 role: nx_int,
76 fml: *u8, // raw formula text (parsing queued)
77}
78
79const NX_TPTP_STMT_BYTES: nx_int = 32
80
81// Parser state: buffer + position.
82struct TptpReader {
83 buf: *u8,
84 n: nx_int,
85 pos: nx_int,
86 stmts: *TptpStmt,
87 n_stmts: nx_int,
88 capacity: nx_int,
89}
90
91const NX_TPTP_MAX_STMTS: nx_int = 4096
92const NX_TPTP_READER_BYTES: nx_int = 40
93const NX_TPTP_IDENT_CAP: nx_int = 128
94
95func nx_tptp_reader_new(buf: *u8, n: nx_int) -> *TptpReader {
96 let r: *TptpReader = (sys_mmap(NX_TPTP_READER_BYTES as i64)) as *TptpReader
97 r.buf = buf
98 r.n = n
99 r.pos = 0
100 r.stmts = (sys_mmap((NX_TPTP_MAX_STMTS * NX_TPTP_STMT_BYTES) as i64)) as *TptpStmt
101 r.n_stmts = 0
102 r.capacity = NX_TPTP_MAX_STMTS
103 return r
104}
105
106// Skip whitespace + comments (% to end-of-line, /* */ blocks).
107func nx_tptp_skip_ws(r: *TptpReader) {
108 var p: nx_int = r.pos
109 while p < r.n {
110 let c: nx_int = r.buf[p] as nx_int
111 if c == 32 { p = p + 1 } // space
112 if c == 9 { p = p + 1 } // tab
113 if c == 10 { p = p + 1 } // newline
114 if c == 13 { p = p + 1 } // cr
115 if c == 37 { // '%' line comment
116 while p < r.n {
117 if r.buf[p] == 10 { p = p + 1; p = p - 1 } // hack to exit inner
118 if r.buf[p] == 10 { p = p + 1; p = r.n }
119 p = p + 1
120 }
121 }
122 if c != 32 {
123 if c != 9 {
124 if c != 10 {
125 if c != 13 {
126 if c != 37 { r.pos = p; return }
127 }
128 }
129 }
130 }
131 }
132 r.pos = p
133}
134
135// Read an identifier (lowercase letter or digit or _) into out_buf.
136// Returns length.
137func nx_tptp_read_ident(r: *TptpReader, out_buf: *u8) -> nx_int {
138 var len: nx_int = 0
139 while r.pos < r.n {
140 let c: nx_int = r.buf[r.pos] as nx_int
141 var is_id: nx_int = 0
142 if c >= 97 { if c <= 122 { is_id = 1 } } // a-z
143 if c >= 48 { if c <= 57 { is_id = 1 } } // 0-9
144 if c == 95 { is_id = 1 } // _
145 if c >= 65 { if c <= 90 { is_id = 1 } } // A-Z (TPTP allows)
146 if is_id == 0 { out_buf[len] = 0; return len }
147 if len < (NX_TPTP_IDENT_CAP - 1) {
148 out_buf[len] = r.buf[r.pos]
149 len = len + 1
150 }
151 r.pos = r.pos + 1
152 }
153 out_buf[len] = 0
154 return len
155}
156
157// Skip the formula portion until matching closing paren + dot. Naive:
158// counts parens; works for simple TPTP problems. Returns start + end.
159func nx_tptp_read_fml_raw(r: *TptpReader, out_start: *nx_int, out_end: *nx_int) -> nx_int {
160 nx_tptp_skip_ws(r)
161 out_start[0] = r.pos
162 var depth: nx_int = 0
163 while r.pos < r.n {
164 let c: nx_int = r.buf[r.pos] as nx_int
165 if c == 40 { depth = depth + 1; r.pos = r.pos + 1 } // (
166 if c != 40 {
167 if c == 41 {
168 if depth == 0 {
169 out_end[0] = r.pos
170 return 1
171 }
172 depth = depth - 1
173 r.pos = r.pos + 1
174 }
175 if c != 41 { r.pos = r.pos + 1 }
176 }
177 }
178 out_end[0] = r.pos
179 return 0
180}
181
182// Try to read one TPTP statement. On success, populates a slot in
183// r.stmts and returns OK. On EOF returns ERR(NOT_FOUND).
184func nx_tptp_read_stmt(r: *TptpReader) -> *NxResult {
185 nx_tptp_skip_ws(r)
186 if r.pos >= r.n { return nx_result_err(NX_ERR_NOT_FOUND) }
187 if r.n_stmts >= r.capacity { return nx_result_err(NX_ERR_INVALID_STATE) }
188
189 // Read kind: "fof" | "cnf" | "thf" | "tff"
190 let kind_buf: *u8 = sys_mmap(16)
191 let kind_len: nx_int = nx_tptp_read_ident(r, kind_buf)
192 if kind_len < 3 { return nx_result_err(NX_ERR_PARSE_FAILED) }
193 var kind: nx_int = 0
194 if nx_str_eq(kind_buf, "fof" as *u8) == 1 { kind = NX_TPTP_KIND_FOF }
195 if nx_str_eq(kind_buf, "cnf" as *u8) == 1 { kind = NX_TPTP_KIND_CNF }
196 if nx_str_eq(kind_buf, "thf" as *u8) == 1 { kind = NX_TPTP_KIND_THF }
197 if nx_str_eq(kind_buf, "tff" as *u8) == 1 { kind = NX_TPTP_KIND_TFF }
198 if kind == 0 { return nx_result_err(NX_ERR_PARSE_FAILED) }
199
200 // Expect '('
201 nx_tptp_skip_ws(r)
202 if r.pos >= r.n { return nx_result_err(NX_ERR_PARSE_FAILED) }
203 if r.buf[r.pos] != 40 { return nx_result_err(NX_ERR_PARSE_FAILED) }
204 r.pos = r.pos + 1
205
206 // Read name
207 nx_tptp_skip_ws(r)
208 let name_buf: *u8 = sys_mmap(NX_TPTP_IDENT_CAP as i64)
209 let name_len: nx_int = nx_tptp_read_ident(r, name_buf)
210 if name_len < 1 { return nx_result_err(NX_ERR_PARSE_FAILED) }
211
212 // Expect ','
213 nx_tptp_skip_ws(r)
214 if r.pos >= r.n { return nx_result_err(NX_ERR_PARSE_FAILED) }
215 if r.buf[r.pos] != 44 { return nx_result_err(NX_ERR_PARSE_FAILED) }
216 r.pos = r.pos + 1
217
218 // Read role
219 nx_tptp_skip_ws(r)
220 let role_buf: *u8 = sys_mmap(64)
221 let role_len: nx_int = nx_tptp_read_ident(r, role_buf)
222 if role_len < 1 { return nx_result_err(NX_ERR_PARSE_FAILED) }
223 let role: nx_int = nx_tptp_role_from_str(role_buf)
224
225 // Allocate slot and write
226 let raw_slot: *u8 = ((r.stmts as nx_int) + (r.n_stmts * NX_TPTP_STMT_BYTES)) as *u8
227 let slot: *TptpStmt = raw_slot as *TptpStmt
228 slot.kind = kind
229 slot.name = name_buf
230 slot.role = role
231 slot.fml = role_buf // formula parser queued; raw role string in slot for now
232 r.n_stmts = r.n_stmts + 1
233
234 // Skip to next statement marker '.' (consume + stop).
235 var stop: nx_int = 0
236 while stop == 0 {
237 if r.pos >= r.n { stop = 1 }
238 if stop == 0 {
239 let c: nx_int = r.buf[r.pos] as nx_int
240 r.pos = r.pos + 1
241 if c == 46 { stop = 1 } // '.' end of stmt; r.pos now points past it
242 }
243 }
244
245 return nx_result_ok(1)
246}
247
248func nx_tptp_n_stmts(r: *TptpReader) -> nx_int { return r.n_stmts }
249func nx_tptp_stmt_at(r: *TptpReader, idx: nx_int) -> *TptpStmt {
250 if idx < 0 { return 0 as *TptpStmt }
251 if idx >= r.n_stmts { return 0 as *TptpStmt }
252 return ((r.stmts as nx_int) + (idx * NX_TPTP_STMT_BYTES)) as *TptpStmt
253}