nx_fof_parse.nx source
↩ module page · 340 lines · 13745 B
1// nx_fof_parse.nx -- TPTP FOF formula parser.
2//
3// Per Vampire-displacement roadmap Phase 2. Recursive-descent parser
4// over the FOF connective grammar. Produces an *Fof tree; CNF
5// conversion (Skolemize + distribute) is a separate primitive that
6// consumes the tree.
7//
8// Grammar (TPTP FOF subset, with precedence shown):
9//
10// formula ::= iff (lowest prec)
11// iff ::= imp { "<=>" imp }
12// imp ::= or { "=>" or } (right-assoc)
13// or_expr ::= and_expr { "|" and_expr }
14// and_expr ::= unitary { "&" unitary }
15// unitary ::= "~" unitary
16// | quantified
17// | "(" formula ")"
18// | atom
19// quantified ::= ("!" | "?") "[" var { "," var } "]" ":" unitary
20// atom ::= predicate-application
21// | term "=" term
22// | term "!=" term
23// | term (handled at term level)
24//
25// Multi-var quantifier ![X, Y]: body is sugar for ![X]: ![Y]: body.
26//
27// Returns null on parse failure. Caller can re-parse with debug
28// instrumentation if needed; the next refinement is Result-typed
29// errors with parse-position context.
30
31// nx_safety_envelope:
32// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
33// sil_target: SIL1
34// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
35// verdict: NOT_YET_EVALUATED
36
37import "nx_syscalls.nx"
38import "nx_runtime.nx"
39import "nx_tier.nx"
40import "nx_str.nx"
41import "nx_result.nx"
42import "nx_unify.nx"
43import "nx_tptp_symtab.nx"
44import "nx_tptp_term.nx"
45import "nx_fof.nx"
46
47// ===== Forward declarations =========================================
48// Recursive-descent grammar has natural mutual recursion:
49// unitary -> "(" iff ")" (parens hand back to top)
50// unitary -> quantified
51// quantified -> ":" unitary (body of a quantifier)
52// and -> unitary { "&" unitary }
53// ... up through iff
54// nxc2 supports forward decls via `func name(params) -> type;` -- the
55// later definition graduates the extern slot to a full body.
56func nx_fof_parse_iff(buf: *u8, n: nx_int, pos: *nx_int,
57 symtab: *TptpSymtab, eq_sym: nx_int) -> *Fof;
58func nx_fof_parse_unitary(buf: *u8, n: nx_int, pos: *nx_int,
59 symtab: *TptpSymtab, eq_sym: nx_int) -> *Fof;
60func nx_fof_parse_quantified(buf: *u8, n: nx_int, pos: *nx_int,
61 symtab: *TptpSymtab, eq_sym: nx_int,
62 quant_kind: nx_int) -> *Fof;
63
64// ===== Helpers ======================================================
65// True iff the next non-ws byte is `c`; pos is left at the non-ws byte.
66func nx_fof_peek_is(buf: *u8, n: nx_int, pos: *nx_int, c: nx_int) -> nx_int {
67 nx_tptp_term_skip_ws(buf, n, pos)
68 if pos[0] >= n { return 0 }
69 if (buf[pos[0]] as nx_int) == c { return 1 }
70 return 0
71}
72
73// Consume `c` if next; return 1 on consumed, 0 otherwise.
74func nx_fof_eat(buf: *u8, n: nx_int, pos: *nx_int, c: nx_int) -> nx_int {
75 if nx_fof_peek_is(buf, n, pos, c) == 1 {
76 pos[0] = pos[0] + 1
77 return 1
78 }
79 return 0
80}
81
82// Consume the literal 2-byte sequence (c1, c2) if next. Returns 1 on
83// consumed, 0 otherwise.
84func nx_fof_eat2(buf: *u8, n: nx_int, pos: *nx_int, c1: nx_int, c2: nx_int) -> nx_int {
85 nx_tptp_term_skip_ws(buf, n, pos)
86 if pos[0] + 1 >= n { return 0 }
87 if (buf[pos[0]] as nx_int) != c1 { return 0 }
88 if (buf[pos[0] + 1] as nx_int) != c2 { return 0 }
89 pos[0] = pos[0] + 2
90 return 1
91}
92
93func nx_fof_eat3(buf: *u8, n: nx_int, pos: *nx_int, c1: nx_int, c2: nx_int, c3: nx_int) -> nx_int {
94 nx_tptp_term_skip_ws(buf, n, pos)
95 if pos[0] + 2 >= n { return 0 }
96 if (buf[pos[0]] as nx_int) != c1 { return 0 }
97 if (buf[pos[0] + 1] as nx_int) != c2 { return 0 }
98 if (buf[pos[0] + 2] as nx_int) != c3 { return 0 }
99 pos[0] = pos[0] + 3
100 return 1
101}
102
103// ===== Atom parser ==================================================
104// Parses one positive atom (predicate-app or equation). Differs from
105// nx_tptp_parse_literal in that it does NOT read a leading `~` -- the
106// FOF caller (unitary level) handles negation as a separate FOF NEG
107// node.
108func nx_fof_parse_atom(buf: *u8, n: nx_int, pos: *nx_int,
109 symtab: *TptpSymtab, eq_sym: nx_int) -> *Term {
110 nx_tptp_term_skip_ws(buf, n, pos)
111 if pos[0] >= n { return 0 as *Term }
112
113 let t1: *Term = nx_tptp_parse_term(buf, n, pos, symtab)
114 if (t1 as nx_int) == 0 { return 0 as *Term }
115
116 nx_tptp_term_skip_ws(buf, n, pos)
117 if pos[0] >= n { return t1 }
118
119 let next_c: nx_int = buf[pos[0]] as nx_int
120
121 // Equality: t1 = t2. But '=' is also the prefix of '=>' (implication
122 // at the formula level) and '<=' wouldn't appear here. Peek the
123 // next byte to make sure '=' isn't followed by '>'.
124 if next_c == 61 {
125 var is_implication: nx_int = 0
126 if pos[0] + 1 < n {
127 if (buf[pos[0] + 1] as nx_int) == 62 { is_implication = 1 }
128 }
129 if is_implication == 0 {
130 pos[0] = pos[0] + 1
131 let t2: *Term = nx_tptp_parse_term(buf, n, pos, symtab)
132 if (t2 as nx_int) == 0 { return 0 as *Term }
133 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term
134 let a0: *Term = args
135 a0.kind = t1.kind; a0.sym = t1.sym; a0.n_args = t1.n_args; a0.args = t1.args
136 let a1: *Term = ((args as nx_int) + NX_TERM_BYTES) as *Term
137 a1.kind = t2.kind; a1.sym = t2.sym; a1.n_args = t2.n_args; a1.args = t2.args
138 return nx_term_app(eq_sym, 2, args)
139 }
140 }
141 // != handled at unitary level so it can wrap in NEG cleanly.
142 return t1
143}
144
145// ===== Forward decls ================================================
146// nxc2 supports forward refs through linking; declare names by use.
147func nx_fof_parse_unitary(buf: *u8, n: nx_int, pos: *nx_int,
148 symtab: *TptpSymtab, eq_sym: nx_int) -> *Fof {
149 nx_tptp_term_skip_ws(buf, n, pos)
150 if pos[0] >= n { return 0 as *Fof }
151
152 let c: nx_int = buf[pos[0]] as nx_int
153
154 // Negation: ~ unitary
155 if c == 126 {
156 pos[0] = pos[0] + 1
157 let inner: *Fof = nx_fof_parse_unitary(buf, n, pos, symtab, eq_sym)
158 if (inner as nx_int) == 0 { return 0 as *Fof }
159 return nx_fof_neg(inner)
160 }
161
162 // Universal quantifier: ! [VARS] : unitary
163 if c == 33 {
164 // Distinguish ! from != -- ! followed by '=' is inequality, not
165 // quantifier. But at unitary level, != would only appear as part
166 // of an atom expression; here we expect ! to start a quantifier.
167 // Look-ahead: if next char is '[', it's a quantifier; otherwise
168 // it's not our token.
169 if pos[0] + 1 < n {
170 if (buf[pos[0] + 1] as nx_int) == 91 { // '['
171 pos[0] = pos[0] + 1
172 return nx_fof_parse_quantified(buf, n, pos, symtab, eq_sym, NX_FOF_FORALL)
173 }
174 }
175 }
176
177 // Existential quantifier: ? [VARS] : unitary
178 if c == 63 {
179 pos[0] = pos[0] + 1
180 return nx_fof_parse_quantified(buf, n, pos, symtab, eq_sym, NX_FOF_EXISTS)
181 }
182
183 // Parenthesised formula
184 if c == 40 {
185 pos[0] = pos[0] + 1
186 let inside: *Fof = nx_fof_parse_iff(buf, n, pos, symtab, eq_sym)
187 if (inside as nx_int) == 0 { return 0 as *Fof }
188 nx_tptp_term_skip_ws(buf, n, pos)
189 if pos[0] >= n { return 0 as *Fof }
190 if (buf[pos[0]] as nx_int) != 41 { return 0 as *Fof }
191 pos[0] = pos[0] + 1
192 return inside
193 }
194
195 // Atom or atom-with-operator: parse an atom, then check for !=
196 // (which the FOF level wraps in NEG since equality is the only
197 // operator we treat as a literal-with-sign).
198 let atom: *Term = nx_fof_parse_atom(buf, n, pos, symtab, eq_sym)
199 if (atom as nx_int) == 0 { return 0 as *Fof }
200
201 // After atom, check for !=
202 nx_tptp_term_skip_ws(buf, n, pos)
203 if pos[0] + 1 < n {
204 if (buf[pos[0]] as nx_int) == 33 {
205 if (buf[pos[0] + 1] as nx_int) == 61 {
206 // != -- parse RHS, build eq atom, wrap in NEG.
207 pos[0] = pos[0] + 2
208 let rhs: *Term = nx_tptp_parse_term(buf, n, pos, symtab)
209 if (rhs as nx_int) == 0 { return 0 as *Fof }
210 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term
211 let a0: *Term = args
212 a0.kind = atom.kind; a0.sym = atom.sym; a0.n_args = atom.n_args; a0.args = atom.args
213 let a1: *Term = ((args as nx_int) + NX_TERM_BYTES) as *Term
214 a1.kind = rhs.kind; a1.sym = rhs.sym; a1.n_args = rhs.n_args; a1.args = rhs.args
215 let neq_atom: *Term = nx_term_app(eq_sym, 2, args)
216 return nx_fof_neg(nx_fof_atom(neq_atom))
217 }
218 }
219 }
220
221 return nx_fof_atom(atom)
222}
223
224// Quantified parser: caller has just consumed the quantifier symbol
225// (! or ?). Pos is left looking at the '['.
226func nx_fof_parse_quantified(buf: *u8, n: nx_int, pos: *nx_int,
227 symtab: *TptpSymtab, eq_sym: nx_int,
228 quant_kind: nx_int) -> *Fof {
229 nx_tptp_term_skip_ws(buf, n, pos)
230 if pos[0] >= n { return 0 as *Fof }
231 if (buf[pos[0]] as nx_int) != 91 { return 0 as *Fof } // '['
232 pos[0] = pos[0] + 1
233
234 // Read comma-separated variable list. Build a chain of quantifier
235 // nodes: ![X, Y]: body ==> FORALL(X, FORALL(Y, body))
236 let var_buf: *u8 = sys_mmap(NX_TPTP_SYM_NAME_MAX as i64)
237 let var_ids: *nx_int = sys_mmap((16 * 8) as i64) as *nx_int
238 var n_vars: nx_int = 0
239
240 var done: nx_int = 0
241 while done == 0 {
242 nx_tptp_term_skip_ws(buf, n, pos)
243 let vlen: nx_int = nx_tptp_term_read_ident(buf, n, pos, var_buf)
244 if vlen == 0 { return 0 as *Fof }
245 if nx_tptp_is_variable_name(var_buf) != 1 { return 0 as *Fof }
246 let vid: nx_int = nx_tptp_symtab_intern(symtab, var_buf)
247 if vid < 0 { return 0 as *Fof }
248 if n_vars >= 16 { return 0 as *Fof }
249 var_ids[n_vars] = vid
250 n_vars = n_vars + 1
251 nx_tptp_term_skip_ws(buf, n, pos)
252 if pos[0] >= n { return 0 as *Fof }
253 let nc: nx_int = buf[pos[0]] as nx_int
254 if nc == 44 { pos[0] = pos[0] + 1 } // ','
255 if nc == 93 { pos[0] = pos[0] + 1; done = 1 } // ']'
256 if nc != 44 {
257 if nc != 93 { return 0 as *Fof }
258 }
259 }
260
261 // Expect ':'
262 nx_tptp_term_skip_ws(buf, n, pos)
263 if pos[0] >= n { return 0 as *Fof }
264 if (buf[pos[0]] as nx_int) != 58 { return 0 as *Fof }
265 pos[0] = pos[0] + 1
266
267 // Parse body (unitary level binds tightly; quantifier scope is
268 // exactly one unitary).
269 let body: *Fof = nx_fof_parse_unitary(buf, n, pos, symtab, eq_sym)
270 if (body as nx_int) == 0 { return 0 as *Fof }
271
272 // Build the chain right-to-left: innermost var wraps body, then
273 // outer var wraps that result, etc.
274 var out: *Fof = body
275 var i: nx_int = n_vars - 1
276 while i >= 0 {
277 out = nx_fof_quantified(quant_kind, var_ids[i], out)
278 i = i - 1
279 }
280 return out
281}
282
283// ===== Binary connective levels =====================================
284// and: unitary { "&" unitary } -- left-assoc
285func nx_fof_parse_and(buf: *u8, n: nx_int, pos: *nx_int,
286 symtab: *TptpSymtab, eq_sym: nx_int) -> *Fof {
287 var lhs: *Fof = nx_fof_parse_unitary(buf, n, pos, symtab, eq_sym)
288 if (lhs as nx_int) == 0 { return 0 as *Fof }
289 while nx_fof_eat(buf, n, pos, 38) == 1 { // '&'
290 let rhs: *Fof = nx_fof_parse_unitary(buf, n, pos, symtab, eq_sym)
291 if (rhs as nx_int) == 0 { return 0 as *Fof }
292 lhs = nx_fof_binary(NX_FOF_AND, lhs, rhs)
293 }
294 return lhs
295}
296
297// or: and { "|" and } -- left-assoc
298func nx_fof_parse_or(buf: *u8, n: nx_int, pos: *nx_int,
299 symtab: *TptpSymtab, eq_sym: nx_int) -> *Fof {
300 var lhs: *Fof = nx_fof_parse_and(buf, n, pos, symtab, eq_sym)
301 if (lhs as nx_int) == 0 { return 0 as *Fof }
302 while nx_fof_eat(buf, n, pos, 124) == 1 { // '|'
303 let rhs: *Fof = nx_fof_parse_and(buf, n, pos, symtab, eq_sym)
304 if (rhs as nx_int) == 0 { return 0 as *Fof }
305 lhs = nx_fof_binary(NX_FOF_OR, lhs, rhs)
306 }
307 return lhs
308}
309
310// imp: or { "=>" or } -- right-assoc
311func nx_fof_parse_imp(buf: *u8, n: nx_int, pos: *nx_int,
312 symtab: *TptpSymtab, eq_sym: nx_int) -> *Fof {
313 let lhs: *Fof = nx_fof_parse_or(buf, n, pos, symtab, eq_sym)
314 if (lhs as nx_int) == 0 { return 0 as *Fof }
315 if nx_fof_eat2(buf, n, pos, 61, 62) == 1 { // "=>"
316 let rhs: *Fof = nx_fof_parse_imp(buf, n, pos, symtab, eq_sym)
317 if (rhs as nx_int) == 0 { return 0 as *Fof }
318 return nx_fof_binary(NX_FOF_IMP, lhs, rhs)
319 }
320 return lhs
321}
322
323// iff: imp { "<=>" imp } -- left-assoc
324func nx_fof_parse_iff(buf: *u8, n: nx_int, pos: *nx_int,
325 symtab: *TptpSymtab, eq_sym: nx_int) -> *Fof {
326 var lhs: *Fof = nx_fof_parse_imp(buf, n, pos, symtab, eq_sym)
327 if (lhs as nx_int) == 0 { return 0 as *Fof }
328 while nx_fof_eat3(buf, n, pos, 60, 61, 62) == 1 { // "<=>"
329 let rhs: *Fof = nx_fof_parse_imp(buf, n, pos, symtab, eq_sym)
330 if (rhs as nx_int) == 0 { return 0 as *Fof }
331 lhs = nx_fof_binary(NX_FOF_IFF, lhs, rhs)
332 }
333 return lhs
334}
335
336// Top-level FOF formula parser.
337func nx_fof_parse(buf: *u8, n: nx_int, pos: *nx_int,
338 symtab: *TptpSymtab, eq_sym: nx_int) -> *Fof {
339 return nx_fof_parse_iff(buf, n, pos, symtab, eq_sym)
340}