`nx_tptp_term.nx` source

↩ module page · 142 lines · 5140 B
1// nx_tptp_term.nx -- TPTP term grammar -> *Term constructor.
2//
3// TPTP term grammar (subset, sufficient for CNF problems):
4//   term      ::= variable | constant | function "(" term { "," term } ")"
5//   variable  ::= [A-Z][A-Za-z0-9_]*
6//   constant  ::= [a-z][A-Za-z0-9_]*
7//   function  ::= [a-z][A-Za-z0-9_]*    (constant with arguments)
8//
9// Caller passes (buf, length, *pos, symtab); on success the function
10// returns the parsed *Term and advances *pos past the term.  On parse
11// failure returns null *Term (use nx_tptp_term_last_err to inspect).
12
13// nx_safety_envelope:
14//   intended_use:       AUTO_APPLIED -- primitive-specific tuning queued
15//   sil_target:         SIL1
16//   evidence:           [bulk_applied_2026-05-16, see-file-comment-for-detail]
17//   verdict:            NOT_YET_EVALUATED
18
19import "nx_syscalls.nx"
20import "nx_runtime.nx"
21import "nx_tier.nx"
22import "nx_str.nx"
23import "nx_result.nx"
24import "nx_unify.nx"
25import "nx_tptp_symtab.nx"
26
27const NX_TPTP_TERM_MAX_ARGS: nx_int = 8
28
29// Skip whitespace at *pos.
30func nx_tptp_term_skip_ws(buf: *u8, n: nx_int, pos: *nx_int) {
31    var p: nx_int = pos[0]
32    while p < n {
33        let c: nx_int = buf[p] as nx_int
34        if c == 32 { p = p + 1 }
35        if c != 32 {
36            if c == 9 { p = p + 1 }
37            if c != 9 {
38                if c == 10 { p = p + 1 }
39                if c != 10 {
40                    if c == 13 { p = p + 1 }
41                    if c != 13 { pos[0] = p; return }
42                }
43            }
44        }
45    }
46    pos[0] = p
47}
48
49// Read identifier into out_buf, returns length.  out_buf is null-
50// terminated.  Returns 0 if no identifier.
51func nx_tptp_term_read_ident(buf: *u8, n: nx_int, pos: *nx_int, out_buf: *u8) -> nx_int {
52    var p: nx_int = pos[0]
53    var len: nx_int = 0
54    while p < n {
55        let c: nx_int = buf[p] as nx_int
56        var is_id: nx_int = 0
57        if c >= 65 { if c <= 90  { is_id = 1 } }   // A-Z
58        if c >= 97 { if c <= 122 { is_id = 1 } }   // a-z
59        if c >= 48 { if c <= 57  { is_id = 1 } }   // 0-9
60        if c == 95 { is_id = 1 }                   // _
61        if is_id == 0 {
62            out_buf[len] = 0
63            pos[0] = p
64            return len
65        }
66        if len < (NX_TPTP_SYM_NAME_MAX - 1) {
67            out_buf[len] = buf[p]
68            len = len + 1
69        }
70        p = p + 1
71    }
72    out_buf[len] = 0
73    pos[0] = p
74    return len
75}
76
77// Forward declaration for mutual recursion through arglist parsing.
78// (nxc2 supports forward refs via order-independent linking.)
79func nx_tptp_parse_term(buf: *u8, n: nx_int, pos: *nx_int,
80                        symtab: *TptpSymtab) -> *Term {
81    nx_tptp_term_skip_ws(buf, n, pos)
82    if pos[0] >= n { return 0 as *Term }
83
84    let name_buf: *u8 = sys_mmap(NX_TPTP_SYM_NAME_MAX as i64)
85    let len: nx_int = nx_tptp_term_read_ident(buf, n, pos, name_buf)
86    if len == 0 { return 0 as *Term }
87
88    // Variable?
89    if nx_tptp_is_variable_name(name_buf) == 1 {
90        let var_id: nx_int = nx_tptp_symtab_intern(symtab, name_buf)
91        if var_id < 0 { return 0 as *Term }
92        return nx_term_var(var_id)
93    }
94
95    // Symbol -- look ahead to see if there's an arg list.
96    let sym_id: nx_int = nx_tptp_symtab_intern(symtab, name_buf)
97    if sym_id < 0 { return 0 as *Term }
98
99    nx_tptp_term_skip_ws(buf, n, pos)
100    if pos[0] >= n { return nx_term_const(sym_id) }
101    let next_c: nx_int = buf[pos[0]] as nx_int
102    if next_c != 40 { return nx_term_const(sym_id) }  // not '('
103
104    // Function application -- consume '(', parse args, expect ')'
105    pos[0] = pos[0] + 1     // consume '('
106
107    let args_buf: *Term = (sys_mmap((NX_TPTP_TERM_MAX_ARGS * NX_TERM_BYTES) as i64)) as *Term
108    var n_args: nx_int = 0
109    var done: nx_int = 0
110    while done == 0 {
111        nx_tptp_term_skip_ws(buf, n, pos)
112        if pos[0] >= n { return 0 as *Term }
113        let lookc: nx_int = buf[pos[0]] as nx_int
114        if lookc == 41 {                                // ')' -- end of args (zero-arg case)
115            pos[0] = pos[0] + 1
116            done = 1
117        }
118        if done == 0 {
119            let arg_t: *Term = nx_tptp_parse_term(buf, n, pos, symtab)
120            if (arg_t as nx_int) == 0 { return 0 as *Term }
121            if n_args >= NX_TPTP_TERM_MAX_ARGS { return 0 as *Term }
122            // Copy arg into flat args buffer.
123            let dest: *Term = ((args_buf as nx_int) + (n_args * NX_TERM_BYTES)) as *Term
124            dest.kind   = arg_t.kind
125            dest.sym    = arg_t.sym
126            dest.n_args = arg_t.n_args
127            dest.args   = arg_t.args
128            n_args = n_args + 1
129
130            nx_tptp_term_skip_ws(buf, n, pos)
131            if pos[0] >= n { return 0 as *Term }
132            let sepc: nx_int = buf[pos[0]] as nx_int
133            if sepc == 44 { pos[0] = pos[0] + 1 }      // ',' -- next arg
134            if sepc != 44 {
135                if sepc == 41 { pos[0] = pos[0] + 1; done = 1 }   // ')' -- end
136                if sepc != 41 { return 0 as *Term }    // unexpected
137            }
138        }
139    }
140    if n_args == 0 { return nx_term_const(sym_id) }
141    return nx_term_app(sym_id, n_args, args_buf)
142}
nx_tptp_term.nx source

`nx_tptp_term.nx` source
