nx_isabelle_ingest.nx source
↩ module page · 200 lines · 6587 B
1// nx_isabelle_ingest.nx -- Isabelle/HOL .thy statement-level ingester (I0).
2//
3// Isabelle/HOL .thy file declarations:
4// theorem NAME: "<statement>"
5// <proof>
6// lemma NAME: "<statement>" by ...
7// definition NAME: "<definition>"
8// axiomatization where NAME: "<axiom>"
9// (* comment *)
10//
11// genealogy_id: nipkow_paulson_wenzel_2002
12// lineage_id: higher_order_logic + isar_proof_language
13
14// nx_safety_envelope:
15// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
16// sil_target: SIL1
17// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
18// verdict: NOT_YET_EVALUATED
19
20import "nx_syscalls.nx"
21import "nx_axioms.nx"
22import "nx_lex.nx"
23import "nx_ascii.nx"
24
25const NX_ISA_TOK_NONE: i64 = 0
26const NX_ISA_TOK_THEOREM: i64 = 1
27const NX_ISA_TOK_LEMMA: i64 = 2
28const NX_ISA_TOK_DEFINITION: i64 = 3
29const NX_ISA_TOK_AXIOMATIZATION: i64 = 4
30const NX_ISA_TOK_IDENT: i64 = 5
31
32const NX_ISA_MAX_NAME_LEN: i64 = 256
33const NX_ISA_MAX_DECLS: i64 = 65536
34
35struct IsaDecl {
36 kind: i64,
37 name: *u8,
38}
39
40const NX_ISA_DECL_BYTES: i64 = 16
41
42struct IsaDb {
43 decls: *IsaDecl,
44 n_decls: i64,
45 capacity: i64,
46}
47
48func nx_isa_db_alloc() -> *IsaDb {
49 let raw: *u8 = sys_mmap(24)
50 let db: *IsaDb = raw as *IsaDb
51 db.decls = (sys_mmap(NX_ISA_MAX_DECLS * NX_ISA_DECL_BYTES)) as *IsaDecl
52 db.n_decls = 0
53 db.capacity = NX_ISA_MAX_DECLS
54 return db
55}
56
57func nx_isa_decl_at(db: *IsaDb, i: i64) -> *IsaDecl {
58 return (((db.decls as i64) + i * NX_ISA_DECL_BYTES) as *IsaDecl)
59}
60
61// is_ws canonical in nx_lex.nx.
62
63// is_alpha (is_id_start) canonical in nx_ascii.nx.
64
65// is_alnum (alpha + _ + digit + ') canonical in nx_lex (nx_lex_is_id_cont_math).
66
67func nx_isa_skip_ws(buf: *u8, pos: *i64, len: i64) -> i64 {
68 var progress: i64 = 1
69 while progress == 1 {
70 progress = 0
71 while pos[0] < len {
72 let c: i64 = buf[pos[0]]
73 if nx_lex_is_ws(c) == 1 { pos[0] = pos[0] + 1; progress = 1 }
74 if nx_lex_is_ws(c) == 0 {
75 if c == 40 {
76 if pos[0] + 1 < len {
77 if buf[pos[0] + 1] == 42 {
78 pos[0] = pos[0] + 2
79 var depth: i64 = 1
80 while depth > 0 {
81 if pos[0] >= len { depth = 0; pos[0] = len }
82 if pos[0] + 1 < len {
83 if buf[pos[0]] == 42 {
84 if buf[pos[0] + 1] == 41 {
85 pos[0] = pos[0] + 2
86 depth = depth - 1
87 }
88 }
89 }
90 if depth > 0 { pos[0] = pos[0] + 1 }
91 }
92 progress = 1
93 }
94 }
95 }
96 if c != 40 { return 0 }
97 if pos[0] + 1 < len {
98 if buf[pos[0] + 1] != 42 { return 0 }
99 }
100 }
101 }
102 }
103 return 0
104}
105
106func nx_isa_next_token(buf: *u8, pos: *i64, len: i64, out_label: *u8) -> i64 {
107 nx_isa_skip_ws(buf, pos, len)
108 if pos[0] >= len { return NX_ISA_TOK_NONE }
109 let c0: i64 = buf[pos[0]]
110 if nx_ascii_is_id_start(c0) == 1 {
111 var i: i64 = 0
112 while pos[0] < len {
113 let c: i64 = buf[pos[0]]
114 if nx_lex_is_id_cont_math(c) == 0 {
115 out_label[i] = 0
116 if i == 7 {
117 if out_label[0] == 116 { return NX_ISA_TOK_THEOREM } // theorem
118 }
119 if i == 5 {
120 if out_label[0] == 108 { return NX_ISA_TOK_LEMMA } // lemma
121 }
122 if i == 10 {
123 if out_label[0] == 100 { return NX_ISA_TOK_DEFINITION } // definition
124 }
125 if i == 14 {
126 if out_label[0] == 97 { return NX_ISA_TOK_AXIOMATIZATION } // axiomatization
127 }
128 return NX_ISA_TOK_IDENT
129 }
130 if i < NX_ISA_MAX_NAME_LEN - 1 {
131 out_label[i] = c
132 i = i + 1
133 }
134 pos[0] = pos[0] + 1
135 }
136 out_label[i] = 0
137 return NX_ISA_TOK_IDENT
138 }
139 pos[0] = pos[0] + 1
140 return NX_ISA_TOK_NONE
141}
142
143func nx_isa_record_decl(db: *IsaDb, kind: i64, label: *u8) -> i64 {
144 if db.n_decls >= db.capacity { return -1 }
145 let d: *IsaDecl = nx_isa_decl_at(db, db.n_decls)
146 d.kind = kind
147 let name_copy: *u8 = sys_mmap(NX_ISA_MAX_NAME_LEN)
148 var i: i64 = 0
149 while i < NX_ISA_MAX_NAME_LEN {
150 name_copy[i] = label[i]
151 if label[i] == 0 { i = NX_ISA_MAX_NAME_LEN }
152 if i < NX_ISA_MAX_NAME_LEN { i = i + 1 }
153 }
154 d.name = name_copy
155 db.n_decls = db.n_decls + 1
156 return 0
157}
158
159func nx_isa_ingest_corpus(buf: *u8, len: i64) -> *IsaDb {
160 let db: *IsaDb = nx_isa_db_alloc()
161 let pos: *i64 = (sys_mmap(8)) as *i64
162 pos[0] = 0
163 let label: *u8 = sys_mmap(NX_ISA_MAX_NAME_LEN)
164
165 while pos[0] < len {
166 let tok: i64 = nx_isa_next_token(buf, pos, len, label)
167 // Unknown punctuation -- skip, don't abort.
168 if tok == NX_ISA_TOK_NONE {
169 if pos[0] >= len { pos[0] = len }
170 }
171 if tok == NX_ISA_TOK_THEOREM {
172 let t2: i64 = nx_isa_next_token(buf, pos, len, label)
173 if t2 == NX_ISA_TOK_IDENT { nx_isa_record_decl(db, NX_ISA_TOK_THEOREM, label) }
174 }
175 if tok == NX_ISA_TOK_LEMMA {
176 let t2: i64 = nx_isa_next_token(buf, pos, len, label)
177 if t2 == NX_ISA_TOK_IDENT { nx_isa_record_decl(db, NX_ISA_TOK_LEMMA, label) }
178 }
179 if tok == NX_ISA_TOK_DEFINITION {
180 let t2: i64 = nx_isa_next_token(buf, pos, len, label)
181 if t2 == NX_ISA_TOK_IDENT { nx_isa_record_decl(db, NX_ISA_TOK_DEFINITION, label) }
182 }
183 if tok == NX_ISA_TOK_AXIOMATIZATION {
184 let t2: i64 = nx_isa_next_token(buf, pos, len, label)
185 if t2 == NX_ISA_TOK_IDENT { nx_isa_record_decl(db, NX_ISA_TOK_AXIOMATIZATION, label) }
186 }
187 }
188 return db
189}
190
191func nx_isa_count_kind(db: *IsaDb, kind: i64) -> i64 {
192 var c: i64 = 0
193 var i: i64 = 0
194 while i < db.n_decls {
195 let d: *IsaDecl = nx_isa_decl_at(db, i)
196 if d.kind == kind { c = c + 1 }
197 i = i + 1
198 }
199 return c
200}