nx_coq_ingest.nx source
↩ module page · 226 lines · 7869 B
1// nx_coq_ingest.nx -- Coq stdlib + MathComp statement-level ingester (C0).
2//
3// Coq's surface syntax for declarations:
4// Theorem NAME : TYPE. Proof. ... Qed.
5// Lemma NAME : TYPE. Proof. ... Qed.
6// Definition NAME : TYPE := VALUE.
7// Axiom NAME : TYPE.
8// Fixpoint NAME ... := ...
9// Inductive NAME : TYPE := ...
10// (* comment *)
11//
12// We do NOT implement Coq's CIC kernel. Statement-level ingest only.
13//
14// genealogy_id: coquand_huet_1988 + coq_team
15// lineage_id: formal_statement_parsing + dependent_type_theory
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_axioms.nx"
25import "nx_lex.nx"
26import "nx_ascii.nx"
27
28const NX_COQ_TOK_NONE: i64 = 0
29const NX_COQ_TOK_THEOREM: i64 = 1
30const NX_COQ_TOK_LEMMA: i64 = 2
31const NX_COQ_TOK_DEFINITION: i64 = 3
32const NX_COQ_TOK_AXIOM: i64 = 4
33const NX_COQ_TOK_FIXPOINT: i64 = 5
34const NX_COQ_TOK_INDUCTIVE: i64 = 6
35const NX_COQ_TOK_IDENT: i64 = 7
36
37const NX_COQ_MAX_NAME_LEN: i64 = 256
38const NX_COQ_MAX_DECLS: i64 = 65536
39
40struct CoqDecl {
41 kind: i64,
42 name: *u8,
43}
44
45const NX_COQ_DECL_BYTES: i64 = 16
46
47struct CoqDb {
48 decls: *CoqDecl,
49 n_decls: i64,
50 capacity: i64,
51}
52
53func nx_coq_db_alloc() -> *CoqDb {
54 let raw: *u8 = sys_mmap(24)
55 let db: *CoqDb = raw as *CoqDb
56 db.decls = (sys_mmap(NX_COQ_MAX_DECLS * NX_COQ_DECL_BYTES)) as *CoqDecl
57 db.n_decls = 0
58 db.capacity = NX_COQ_MAX_DECLS
59 return db
60}
61
62func nx_coq_decl_at(db: *CoqDb, i: i64) -> *CoqDecl {
63 return (((db.decls as i64) + i * NX_COQ_DECL_BYTES) as *CoqDecl)
64}
65
66// is_ws canonical in nx_lex.nx (nx_lex_is_ws).
67
68// is_alpha (is_id_start) canonical in nx_ascii.nx.
69
70// is_alnum (alpha + _ + digit + ' + .) canonical in nx_lex (nx_lex_is_id_cont_qualified).
71
72// Skip whitespace + (* ... *) block comments.
73func nx_coq_skip_ws(buf: *u8, pos: *i64, len: i64) -> i64 {
74 var progress: i64 = 1
75 while progress == 1 {
76 progress = 0
77 while pos[0] < len {
78 let c: i64 = buf[pos[0]]
79 if nx_lex_is_ws(c) == 1 { pos[0] = pos[0] + 1; progress = 1 }
80 if nx_lex_is_ws(c) == 0 {
81 if c == 40 { // '('
82 if pos[0] + 1 < len {
83 if buf[pos[0] + 1] == 42 { // '(*'
84 pos[0] = pos[0] + 2
85 var depth: i64 = 1
86 while depth > 0 {
87 if pos[0] >= len { depth = 0; pos[0] = len }
88 if pos[0] + 1 < len {
89 if buf[pos[0]] == 42 {
90 if buf[pos[0] + 1] == 41 {
91 pos[0] = pos[0] + 2
92 depth = depth - 1
93 }
94 }
95 }
96 if depth > 0 { pos[0] = pos[0] + 1 }
97 }
98 progress = 1
99 }
100 }
101 }
102 if c != 40 { return 0 }
103 if pos[0] + 1 < len {
104 if buf[pos[0] + 1] != 42 { return 0 }
105 }
106 }
107 }
108 }
109 return 0
110}
111
112func nx_coq_next_token(buf: *u8, pos: *i64, len: i64, out_label: *u8) -> i64 {
113 nx_coq_skip_ws(buf, pos, len)
114 if pos[0] >= len { return NX_COQ_TOK_NONE }
115 let c0: i64 = buf[pos[0]]
116 if nx_ascii_is_id_start(c0) == 1 {
117 var i: i64 = 0
118 while pos[0] < len {
119 let c: i64 = buf[pos[0]]
120 if nx_lex_is_id_cont_qualified(c) == 0 {
121 out_label[i] = 0
122 // Keyword detection.
123 if i == 7 {
124 if out_label[0] == 84 { // 'T'
125 if out_label[1] == 104 { return NX_COQ_TOK_THEOREM }
126 }
127 }
128 if i == 5 {
129 if out_label[0] == 76 { // 'L'
130 if out_label[1] == 101 { return NX_COQ_TOK_LEMMA }
131 }
132 if out_label[0] == 65 { // 'A'
133 if out_label[1] == 120 { return NX_COQ_TOK_AXIOM }
134 }
135 }
136 if i == 10 {
137 if out_label[0] == 68 { return NX_COQ_TOK_DEFINITION } // 'D'
138 }
139 if i == 8 {
140 if out_label[0] == 70 { return NX_COQ_TOK_FIXPOINT } // 'F'
141 }
142 if i == 9 {
143 if out_label[0] == 73 { return NX_COQ_TOK_INDUCTIVE } // 'I'
144 }
145 return NX_COQ_TOK_IDENT
146 }
147 if i < NX_COQ_MAX_NAME_LEN - 1 {
148 out_label[i] = c
149 i = i + 1
150 }
151 pos[0] = pos[0] + 1
152 }
153 out_label[i] = 0
154 return NX_COQ_TOK_IDENT
155 }
156 pos[0] = pos[0] + 1
157 return NX_COQ_TOK_NONE
158}
159
160func nx_coq_record_decl(db: *CoqDb, kind: i64, label: *u8) -> i64 {
161 if db.n_decls >= db.capacity { return -1 }
162 let d: *CoqDecl = nx_coq_decl_at(db, db.n_decls)
163 d.kind = kind
164 let name_copy: *u8 = sys_mmap(NX_COQ_MAX_NAME_LEN)
165 var i: i64 = 0
166 while i < NX_COQ_MAX_NAME_LEN {
167 name_copy[i] = label[i]
168 if label[i] == 0 { i = NX_COQ_MAX_NAME_LEN }
169 if i < NX_COQ_MAX_NAME_LEN { i = i + 1 }
170 }
171 d.name = name_copy
172 db.n_decls = db.n_decls + 1
173 return 0
174}
175
176func nx_coq_ingest_corpus(buf: *u8, len: i64) -> *CoqDb {
177 let db: *CoqDb = nx_coq_db_alloc()
178 let pos: *i64 = (sys_mmap(8)) as *i64
179 pos[0] = 0
180 let label: *u8 = sys_mmap(NX_COQ_MAX_NAME_LEN)
181
182 while pos[0] < len {
183 let tok: i64 = nx_coq_next_token(buf, pos, len, label)
184 // Unknown punctuation -- skip, don't abort. next_token already
185 // advanced pos past the offending byte.
186 if tok == NX_COQ_TOK_NONE {
187 if pos[0] >= len { pos[0] = len }
188 }
189 if tok == NX_COQ_TOK_THEOREM {
190 let t2: i64 = nx_coq_next_token(buf, pos, len, label)
191 if t2 == NX_COQ_TOK_IDENT { nx_coq_record_decl(db, NX_COQ_TOK_THEOREM, label) }
192 }
193 if tok == NX_COQ_TOK_LEMMA {
194 let t2: i64 = nx_coq_next_token(buf, pos, len, label)
195 if t2 == NX_COQ_TOK_IDENT { nx_coq_record_decl(db, NX_COQ_TOK_LEMMA, label) }
196 }
197 if tok == NX_COQ_TOK_DEFINITION {
198 let t2: i64 = nx_coq_next_token(buf, pos, len, label)
199 if t2 == NX_COQ_TOK_IDENT { nx_coq_record_decl(db, NX_COQ_TOK_DEFINITION, label) }
200 }
201 if tok == NX_COQ_TOK_AXIOM {
202 let t2: i64 = nx_coq_next_token(buf, pos, len, label)
203 if t2 == NX_COQ_TOK_IDENT { nx_coq_record_decl(db, NX_COQ_TOK_AXIOM, label) }
204 }
205 if tok == NX_COQ_TOK_FIXPOINT {
206 let t2: i64 = nx_coq_next_token(buf, pos, len, label)
207 if t2 == NX_COQ_TOK_IDENT { nx_coq_record_decl(db, NX_COQ_TOK_FIXPOINT, label) }
208 }
209 if tok == NX_COQ_TOK_INDUCTIVE {
210 let t2: i64 = nx_coq_next_token(buf, pos, len, label)
211 if t2 == NX_COQ_TOK_IDENT { nx_coq_record_decl(db, NX_COQ_TOK_INDUCTIVE, label) }
212 }
213 }
214 return db
215}
216
217func nx_coq_count_kind(db: *CoqDb, kind: i64) -> i64 {
218 var c: i64 = 0
219 var i: i64 = 0
220 while i < db.n_decls {
221 let d: *CoqDecl = nx_coq_decl_at(db, i)
222 if d.kind == kind { c = c + 1 }
223 i = i + 1
224 }
225 return c
226}