nx_tptp_symtab.nx source
↩ module page · 120 lines · 4325 B
1// nx_tptp_symtab.nx -- TPTP identifier -> integer id table.
2//
3// Per Vampire-displacement roadmap Phase 1.6: feeds the formula
4// parser. Maps TPTP identifiers to the integer sym_id / var_id
5// space that nx_unify Term structs use.
6//
7// TPTP convention:
8// First character UPPERCASE -> variable (X, Y, Var0)
9// First character lowercase -> function or predicate or constant
10// (arity is determined by use site)
11//
12// Variables are scoped to a single clause in TPTP CNF semantics --
13// the parser MUST call nx_tptp_symtab_reset_vars between clauses to
14// give each clause fresh variable ids. Symbols persist globally so
15// the same predicate name in different clauses gets the same sym_id.
16
17// nx_safety_envelope:
18// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
19// sil_target: SIL1
20// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
21// verdict: NOT_YET_EVALUATED
22
23import "nx_syscalls.nx"
24import "nx_runtime.nx"
25import "nx_tier.nx"
26import "nx_str.nx"
27import "nx_result.nx"
28
29const NX_TPTP_SYM_MAX: nx_int = 256
30const NX_TPTP_SYM_NAME_MAX: nx_int = 64
31const NX_TPTP_VAR_MAX: nx_int = 64
32
33// Symbols (predicates / functions / constants) get ids starting here
34// to leave room for callers to reserve low ids (e.g. equality at 50).
35const NX_TPTP_SYM_BASE: nx_int = 1000
36
37struct TptpSymtab {
38 sym_names: *u8, // flat NX_TPTP_SYM_MAX * NX_TPTP_SYM_NAME_MAX
39 n_sym: nx_int,
40
41 var_names: *u8, // flat NX_TPTP_VAR_MAX * NX_TPTP_SYM_NAME_MAX
42 n_var: nx_int,
43}
44
45const NX_TPTP_SYMTAB_BYTES: nx_int = 32
46
47func nx_tptp_symtab_new() -> *TptpSymtab {
48 let st: *TptpSymtab = (sys_mmap(NX_TPTP_SYMTAB_BYTES as i64)) as *TptpSymtab
49 st.sym_names = sys_mmap((NX_TPTP_SYM_MAX * NX_TPTP_SYM_NAME_MAX) as i64)
50 st.n_sym = 0
51 st.var_names = sys_mmap((NX_TPTP_VAR_MAX * NX_TPTP_SYM_NAME_MAX) as i64)
52 st.n_var = 0
53 return st
54}
55
56// Reset only the variable bindings. Call between clauses.
57func nx_tptp_symtab_reset_vars(st: *TptpSymtab) {
58 st.n_var = 0
59}
60
61// True iff first char of name is uppercase A-Z (TPTP variable).
62func nx_tptp_is_variable_name(name: *u8) -> nx_int {
63 let c: nx_int = name[0] as nx_int
64 if c < 65 { return 0 } // 'A'
65 if c > 90 { return 0 } // 'Z'
66 return 1
67}
68
69// Get a pointer to the i-th name slot in the names buffer.
70func nx_tptp_sym_name_at(st: *TptpSymtab, i: nx_int) -> *u8 {
71 return ((st.sym_names as nx_int) + (i * NX_TPTP_SYM_NAME_MAX)) as *u8
72}
73
74func nx_tptp_var_name_at(st: *TptpSymtab, i: nx_int) -> *u8 {
75 return ((st.var_names as nx_int) + (i * NX_TPTP_SYM_NAME_MAX)) as *u8
76}
77
78// Intern a name. Returns the integer id. Allocates a new entry if
79// the name hasn't been seen yet (in the appropriate variable / symbol
80// namespace). Returns -1 on capacity exhaustion.
81func nx_tptp_symtab_intern(st: *TptpSymtab, name: *u8) -> nx_int {
82 if nx_tptp_is_variable_name(name) == 1 {
83 // Look up
84 var i: nx_int = 0
85 while i < st.n_var {
86 let existing: *u8 = nx_tptp_var_name_at(st, i)
87 if nx_str_eq(existing, name) == 1 { return i }
88 i = i + 1
89 }
90 // Allocate
91 if st.n_var >= NX_TPTP_VAR_MAX { return 0 - 1 }
92 let slot: *u8 = nx_tptp_var_name_at(st, st.n_var)
93 let _c: *u8 = nx_str_cpy(slot, name)
94 let id: nx_int = st.n_var
95 st.n_var = st.n_var + 1
96 return id
97 }
98 // Symbol path
99 var j: nx_int = 0
100 while j < st.n_sym {
101 let existing2: *u8 = nx_tptp_sym_name_at(st, j)
102 if nx_str_eq(existing2, name) == 1 { return NX_TPTP_SYM_BASE + j }
103 j = j + 1
104 }
105 if st.n_sym >= NX_TPTP_SYM_MAX { return 0 - 1 }
106 let slot2: *u8 = nx_tptp_sym_name_at(st, st.n_sym)
107 let _c2: *u8 = nx_str_cpy(slot2, name)
108 let sid: nx_int = NX_TPTP_SYM_BASE + st.n_sym
109 st.n_sym = st.n_sym + 1
110 return sid
111}
112
113// Reverse lookup -- name for a sym_id (returns null if not found).
114// Useful for error messages / debugging.
115func nx_tptp_symtab_name_for(st: *TptpSymtab, sym_id: nx_int) -> *u8 {
116 if sym_id < NX_TPTP_SYM_BASE { return 0 as *u8 }
117 let idx: nx_int = sym_id - NX_TPTP_SYM_BASE
118 if idx >= st.n_sym { return 0 as *u8 }
119 return nx_tptp_sym_name_at(st, idx)
120}