nx_mizar_ingest.nx source
↩ module page · 233 lines · 7453 B
1// nx_mizar_ingest.nx -- ingest Mizar .miz theorem-level statements (M0).
2//
3// Mizar's syntax for declarations we track:
4// theorem :: label
5// <statement>
6// proof
7// <proof script>
8// end;
9//
10// definition let ... ; func ... ; ... end;
11// scheme :: label
12// <scheme body>
13// end;
14//
15// notation / registration / reservation -- skipped at M0
16//
17// MML identifier construction:
18// ARTICLE = uppercase filename without .miz
19// Each theorem gets a sequential number; identifier = ARTICLE:th N
20// Each definition gets ARTICLE:def N
21// Each scheme gets ARTICLE:sch N
22//
23// We do NOT parse Mizar's typed FOL. We do NOT verify proofs.
24// At M0, we extract the identifier list with stable QED-format names.
25// At M1+ we'll parse statements and feed them through nx_prover.
26//
27// genealogy_id: trybulec_mizar_1972 + bancerek_mml + wiedijk_qed_1994
28// lineage_id: formal_statement_parsing + typed_fol
29// axioms: NX_AX_ZFC_SEPARATION
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 "syscalls.nx"
38import "nx_axioms.nx"
39import "nx_lex.nx"
40
41// ===== sealed kinds =====================================================
42
43const NX_MIZAR_KIND_NONE: i64 = 0
44const NX_MIZAR_KIND_THEOREM: i64 = 1
45const NX_MIZAR_KIND_DEFINITION: i64 = 2
46const NX_MIZAR_KIND_SCHEME: i64 = 3
47const NX_MIZAR_KIND_LEMMA: i64 = 4
48
49// ===== entry structure =================================================
50
51const NX_MIZAR_MAX_NAME_LEN: i64 = 128
52
53struct MizarDecl {
54 kind: i64,
55 article: *u8, // null-terminated
56 number: i64, // 1-indexed within article
57 label: *u8, // optional :: label, may be empty
58}
59
60const NX_MIZAR_DECL_BYTES: i64 = 32
61
62struct MizarDb {
63 decls: *MizarDecl,
64 n_decls: i64,
65 capacity: i64,
66 th_counter: i64,
67 def_counter: i64,
68 sch_counter: i64,
69}
70
71const NX_MIZAR_MAX_DECLS: i64 = 1024
72
73func nx_mizar_db_alloc(article_name: *u8) -> *MizarDb {
74 let raw: *u8 = sys_mmap(48)
75 let db: *MizarDb = raw as *MizarDb
76 db.decls = (sys_mmap(NX_MIZAR_MAX_DECLS * NX_MIZAR_DECL_BYTES)) as *MizarDecl
77 db.n_decls = 0
78 db.capacity = NX_MIZAR_MAX_DECLS
79 db.th_counter = 0
80 db.def_counter = 0
81 db.sch_counter = 0
82 return db
83}
84
85func nx_mizar_decl_at(db: *MizarDb, i: i64) -> *MizarDecl {
86 return (((db.decls as i64) + i * NX_MIZAR_DECL_BYTES) as *MizarDecl)
87}
88
89// ===== tokenizer ========================================================
90
91// is_ws canonical in nx_lex.nx.
92
93// Skip whitespace + :: comment lines.
94func nx_mizar_skip_ws(buf: *u8, pos: *i64, len: i64) -> i64 {
95 var progress: i64 = 1
96 while progress == 1 {
97 progress = 0
98 while pos[0] < len {
99 let c: i64 = buf[pos[0]]
100 if nx_lex_is_ws(c) == 1 {
101 pos[0] = pos[0] + 1
102 progress = 1
103 }
104 if nx_lex_is_ws(c) == 0 { return 0 }
105 }
106 }
107 return 0
108}
109
110// Match a literal keyword starting at pos. Returns 1 + advances pos
111// past the keyword if matched; 0 otherwise.
112func nx_mizar_match_kw(buf: *u8, pos: *i64, len: i64, kw: *u8) -> i64 {
113 let start: i64 = pos[0]
114 var i: i64 = 0
115 while kw[i] != 0 {
116 if pos[0] + i >= len { return 0 }
117 if buf[pos[0] + i] != kw[i] { return 0 }
118 i = i + 1
119 }
120 // Must be followed by whitespace, ::, ;, or other non-alpha.
121 let next_pos: i64 = pos[0] + i
122 if next_pos < len {
123 let c: i64 = buf[next_pos]
124 // alpha-num check: a-z, A-Z, 0-9, _ are continuation
125 if c >= 65 { if c <= 90 { return 0 } }
126 if c >= 97 { if c <= 122 { return 0 } }
127 if c >= 48 { if c <= 57 { return 0 } }
128 if c == 95 { return 0 }
129 }
130 pos[0] = pos[0] + i
131 return 1
132}
133
134// Skip to end-of-line (for :: comments).
135func nx_mizar_skip_to_newline(buf: *u8, pos: *i64, len: i64) -> i64 {
136 while pos[0] < len {
137 if buf[pos[0]] == 10 { pos[0] = pos[0] + 1; return 0 }
138 pos[0] = pos[0] + 1
139 }
140 return 0
141}
142
143// ===== ingestion driver ================================================
144
145func nx_mizar_ingest_corpus(buf: *u8, len: i64) -> *MizarDb {
146 let db: *MizarDb = nx_mizar_db_alloc("MML" as *u8)
147 let pos: *i64 = (sys_mmap(8)) as *i64
148 pos[0] = 0
149
150 while pos[0] < len {
151 nx_mizar_skip_ws(buf, pos, len)
152 if pos[0] >= len { return db }
153
154 // ":: comment" line -- check for double-colon
155 if pos[0] + 1 < len {
156 if buf[pos[0]] == 58 {
157 if buf[pos[0] + 1] == 58 {
158 pos[0] = pos[0] + 2
159 nx_mizar_skip_to_newline(buf, pos, len)
160 }
161 }
162 }
163
164 nx_mizar_skip_ws(buf, pos, len)
165 if pos[0] >= len { return db }
166
167 // theorem
168 if nx_mizar_match_kw(buf, pos, len, "theorem") == 1 {
169 if db.n_decls < db.capacity {
170 let d: *MizarDecl = nx_mizar_decl_at(db, db.n_decls)
171 d.kind = NX_MIZAR_KIND_THEOREM
172 d.article = "MML" as *u8
173 db.th_counter = db.th_counter + 1
174 d.number = db.th_counter
175 d.label = "" as *u8
176 db.n_decls = db.n_decls + 1
177 }
178 // skip to 'end;' or next theorem keyword
179 }
180 // definition
181 if nx_mizar_match_kw(buf, pos, len, "definition") == 1 {
182 if db.n_decls < db.capacity {
183 let d: *MizarDecl = nx_mizar_decl_at(db, db.n_decls)
184 d.kind = NX_MIZAR_KIND_DEFINITION
185 d.article = "MML" as *u8
186 db.def_counter = db.def_counter + 1
187 d.number = db.def_counter
188 d.label = "" as *u8
189 db.n_decls = db.n_decls + 1
190 }
191 }
192 // scheme
193 if nx_mizar_match_kw(buf, pos, len, "scheme") == 1 {
194 if db.n_decls < db.capacity {
195 let d: *MizarDecl = nx_mizar_decl_at(db, db.n_decls)
196 d.kind = NX_MIZAR_KIND_SCHEME
197 d.article = "MML" as *u8
198 db.sch_counter = db.sch_counter + 1
199 d.number = db.sch_counter
200 d.label = "" as *u8
201 db.n_decls = db.n_decls + 1
202 }
203 }
204 // lemma (treated as theorem for our purposes)
205 if nx_mizar_match_kw(buf, pos, len, "lemma") == 1 {
206 if db.n_decls < db.capacity {
207 let d: *MizarDecl = nx_mizar_decl_at(db, db.n_decls)
208 d.kind = NX_MIZAR_KIND_LEMMA
209 d.article = "MML" as *u8
210 db.th_counter = db.th_counter + 1
211 d.number = db.th_counter
212 d.label = "" as *u8
213 db.n_decls = db.n_decls + 1
214 }
215 }
216
217 // Advance by 1 if we didn't match anything.
218 if pos[0] < len { pos[0] = pos[0] + 1 }
219 }
220 return db
221}
222
223// Count by kind.
224func nx_mizar_count_kind(db: *MizarDb, kind: i64) -> i64 {
225 var c: i64 = 0
226 var i: i64 = 0
227 while i < db.n_decls {
228 let d: *MizarDecl = nx_mizar_decl_at(db, i)
229 if d.kind == kind { c = c + 1 }
230 i = i + 1
231 }
232 return c
233}