nx_fof_parse.nx

buildroot/runtime/nx_fof_parse.nx

13745 B340 linesdepth 6pulls 10 transitivereach 5 importersview sourcekind librarytopic fof

docs dependencies structs consts functions

about

nx_fof_parse.nx -- TPTP FOF formula parser. Per Vampire-displacement roadmap Phase 2. Recursive-descent parser over the FOF connective grammar. Produces an *Fof tree; CNF conversion (Skolemize + distribute) is a separate primitive that consumes the tree. Grammar (TPTP FOF subset, with precedence shown): formula ::= iff (lowest prec) iff ::= imp { "<=>" imp } imp ::= or { "=>" or } (right-assoc) or_expr ::= and_expr { "|" and_expr } and_expr ::= unitary { "&" unitary } unitary ::= "~" unitary | quantified | "(" formula ")" | atom quantified ::= ("!" | "?") "[" var { "," var } "]" ":" unitary atom ::= predicate-application | term "=" term | term "!=" term | term (handled at term level) Multi-var quantifier ![X, Y]: body is sugar for ![X]: ![Y]: body. Returns null on parse failure. Caller can re-parse with debug instrumentation if needed; the next refinement is Result-typed errors with parse-position context.

dependencies 9 imports · 5 importers

imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_str.nxnx_result.nxnx_unify.nxnx_tptp_symtab.nxnx_tptp_term.nxnx_fof.nx

imported by: nx_casc_runner_test.nxnx_fof_cnf_test.nxnx_fof_parse_test.nxnx_fof_tseitin_test.nxnx_tptp_load_any.nx

structs

none

consts

none

functions

56	func nx_fof_parse_iff(buf: u8, n: nx_int, pos: nx_int, called by 2: nx_fof_parse_unitary nx_fof_parse
58	func nx_fof_parse_unitary(buf: u8, n: nx_int, pos: nx_int, called by 3: nx_fof_parse_unitary nx_fof_parse_quantified nx_fof_parse_and
60	func nx_fof_parse_quantified(buf: u8, n: nx_int, pos: nx_int, called by 1: nx_fof_parse_unitary
66	func nx_fof_peek_is(buf: u8, n: nx_int, pos: nx_int, c: nx_int) -> nx_int called by 1: nx_fof_eat calls 1: nx_tptp_term_skip_ws
74	func nx_fof_eat(buf: u8, n: nx_int, pos: nx_int, c: nx_int) -> nx_int called by 2: nx_fof_parse_and nx_fof_parse_or calls 1: nx_fof_peek_is
84	func nx_fof_eat2(buf: u8, n: nx_int, pos: nx_int, c1: nx_int, c2: nx_int) -> nx_int called by 1: nx_fof_parse_imp calls 1: nx_tptp_term_skip_ws
93	func nx_fof_eat3(buf: u8, n: nx_int, pos: nx_int, c1: nx_int, c2: nx_int, c3: nx_int) -> nx_int called by 1: nx_fof_parse_iff calls 1: nx_tptp_term_skip_ws
108	func nx_fof_parse_atom(buf: u8, n: nx_int, pos: nx_int, called by 1: nx_fof_parse_unitary calls 4: nx_tptp_term_skip_ws nx_tptp_parse_term sys_mmap nx_term_app
147	func nx_fof_parse_unitary(buf: u8, n: nx_int, pos: nx_int, calls 10: nx_tptp_term_skip_ws nx_fof_parse_unitary nx_fof_neg nx_fof_parse_quantified nx_fof_parse_iff nx_fof_parse_atom+4
226	func nx_fof_parse_quantified(buf: u8, n: nx_int, pos: nx_int, calls 7: nx_tptp_term_skip_ws sys_mmap nx_tptp_term_read_ident nx_tptp_is_variable_name nx_tptp_symtab_intern nx_fof_parse_unitary+1
285	func nx_fof_parse_and(buf: u8, n: nx_int, pos: nx_int, called by 1: nx_fof_parse_or calls 3: nx_fof_parse_unitary nx_fof_eat nx_fof_binary
298	func nx_fof_parse_or(buf: u8, n: nx_int, pos: nx_int, called by 1: nx_fof_parse_imp calls 3: nx_fof_parse_and nx_fof_eat nx_fof_binary
311	func nx_fof_parse_imp(buf: u8, n: nx_int, pos: nx_int, called by 2: nx_fof_parse_imp nx_fof_parse_iff calls 4: nx_fof_parse_or nx_fof_eat2 nx_fof_parse_imp nx_fof_binary
324	func nx_fof_parse_iff(buf: u8, n: nx_int, pos: nx_int, calls 3: nx_fof_parse_imp nx_fof_eat3 nx_fof_binary
337	func nx_fof_parse(buf: u8, n: nx_int, pos: nx_int, called by 4: parse parse parse_to_nnf nx_tptp_load_any_file calls 1: nx_fof_parse_iff