nx_hol_ingest.nx source
↩ module page · 215 lines · 7356 B
1// nx_hol_ingest.nx -- HOL Light statement-level ingester (H0).
2//
3// HOL Light uses OCaml-embedded syntax:
4// let NAME = prove (`<term>`, <tactic_script>);;
5// let NAME = define `<recursive>`;;
6// let NAME = new_axiom `<axiom>`;;
7// let NAME = REWRITE_RULE [...] <theorem>;;
8// (* OCaml comment *)
9//
10// We recognize the "let NAME = prove" pattern as the primary
11// theorem declaration form, and "let NAME = new_axiom" for axioms.
12//
13// genealogy_id: harrison_hol_light_1996
14// lineage_id: higher_order_logic + statement_parsing
15
16// nx_safety_envelope:
17// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
18// sil_target: SIL1
19// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
20// verdict: NOT_YET_EVALUATED
21
22import "nx_syscalls.nx"
23import "nx_axioms.nx"
24import "nx_lex.nx"
25import "nx_ascii.nx"
26
27const NX_HOL_TOK_NONE: i64 = 0
28const NX_HOL_TOK_LET: i64 = 1
29const NX_HOL_TOK_PROVE: i64 = 2
30const NX_HOL_TOK_AXIOM: i64 = 3 // new_axiom
31const NX_HOL_TOK_DEFINE: i64 = 4
32const NX_HOL_TOK_IDENT: i64 = 5
33const NX_HOL_TOK_EQUALS: i64 = 6
34const NX_HOL_TOK_SEMICOLON: i64 = 7
35
36const NX_HOL_MAX_NAME_LEN: i64 = 256
37const NX_HOL_MAX_DECLS: i64 = 65536
38
39struct HolDecl {
40 kind: i64,
41 name: *u8,
42}
43
44const NX_HOL_DECL_BYTES: i64 = 16
45
46struct HolDb {
47 decls: *HolDecl,
48 n_decls: i64,
49 capacity: i64,
50}
51
52func nx_hol_db_alloc() -> *HolDb {
53 let raw: *u8 = sys_mmap(24)
54 let db: *HolDb = raw as *HolDb
55 db.decls = (sys_mmap(NX_HOL_MAX_DECLS * NX_HOL_DECL_BYTES)) as *HolDecl
56 db.n_decls = 0
57 db.capacity = NX_HOL_MAX_DECLS
58 return db
59}
60
61func nx_hol_decl_at(db: *HolDb, i: i64) -> *HolDecl {
62 return (((db.decls as i64) + i * NX_HOL_DECL_BYTES) as *HolDecl)
63}
64
65// is_ws canonical in nx_lex.nx.
66
67// is_alpha (is_id_start) canonical in nx_ascii.nx.
68
69// is_alnum (alpha + _ + digit + ') canonical in nx_lex (nx_lex_is_id_cont_math).
70
71// Skip whitespace + (* ... *) OCaml comments.
72func nx_hol_skip_ws(buf: *u8, pos: *i64, len: i64) -> i64 {
73 var progress: i64 = 1
74 while progress == 1 {
75 progress = 0
76 while pos[0] < len {
77 let c: i64 = buf[pos[0]]
78 if nx_lex_is_ws(c) == 1 { pos[0] = pos[0] + 1; progress = 1 }
79 if nx_lex_is_ws(c) == 0 {
80 if c == 40 {
81 if pos[0] + 1 < len {
82 if buf[pos[0] + 1] == 42 {
83 pos[0] = pos[0] + 2
84 var depth: i64 = 1
85 while depth > 0 {
86 if pos[0] >= len { depth = 0; pos[0] = len }
87 if pos[0] + 1 < len {
88 if buf[pos[0]] == 42 {
89 if buf[pos[0] + 1] == 41 {
90 pos[0] = pos[0] + 2
91 depth = depth - 1
92 }
93 }
94 }
95 if depth > 0 { pos[0] = pos[0] + 1 }
96 }
97 progress = 1
98 }
99 }
100 }
101 if c != 40 { return 0 }
102 if pos[0] + 1 < len {
103 if buf[pos[0] + 1] != 42 { return 0 }
104 }
105 }
106 }
107 }
108 return 0
109}
110
111func nx_hol_next_token(buf: *u8, pos: *i64, len: i64, out_label: *u8) -> i64 {
112 nx_hol_skip_ws(buf, pos, len)
113 if pos[0] >= len { return NX_HOL_TOK_NONE }
114 let c0: i64 = buf[pos[0]]
115 if c0 == 61 { pos[0] = pos[0] + 1; return NX_HOL_TOK_EQUALS }
116 if c0 == 59 { pos[0] = pos[0] + 1; return NX_HOL_TOK_SEMICOLON }
117 if nx_ascii_is_id_start(c0) == 1 {
118 var i: i64 = 0
119 while pos[0] < len {
120 let c: i64 = buf[pos[0]]
121 if nx_lex_is_id_cont_math(c) == 0 {
122 out_label[i] = 0
123 if i == 3 {
124 if out_label[0] == 108 { return NX_HOL_TOK_LET } // 'let'
125 }
126 if i == 5 {
127 if out_label[0] == 112 { return NX_HOL_TOK_PROVE } // 'prove'
128 }
129 if i == 9 {
130 if out_label[0] == 110 { return NX_HOL_TOK_AXIOM } // 'new_axiom'
131 }
132 if i == 6 {
133 if out_label[0] == 100 { return NX_HOL_TOK_DEFINE } // 'define'
134 }
135 return NX_HOL_TOK_IDENT
136 }
137 if i < NX_HOL_MAX_NAME_LEN - 1 {
138 out_label[i] = c
139 i = i + 1
140 }
141 pos[0] = pos[0] + 1
142 }
143 out_label[i] = 0
144 return NX_HOL_TOK_IDENT
145 }
146 pos[0] = pos[0] + 1
147 return NX_HOL_TOK_NONE
148}
149
150func nx_hol_record_decl(db: *HolDb, kind: i64, label: *u8) -> i64 {
151 if db.n_decls >= db.capacity { return -1 }
152 let d: *HolDecl = nx_hol_decl_at(db, db.n_decls)
153 d.kind = kind
154 let name_copy: *u8 = sys_mmap(NX_HOL_MAX_NAME_LEN)
155 var i: i64 = 0
156 while i < NX_HOL_MAX_NAME_LEN {
157 name_copy[i] = label[i]
158 if label[i] == 0 { i = NX_HOL_MAX_NAME_LEN }
159 if i < NX_HOL_MAX_NAME_LEN { i = i + 1 }
160 }
161 d.name = name_copy
162 db.n_decls = db.n_decls + 1
163 return 0
164}
165
166// Parse pattern: let <ident> = <prove|new_axiom|define> ...
167func nx_hol_ingest_corpus(buf: *u8, len: i64) -> *HolDb {
168 let db: *HolDb = nx_hol_db_alloc()
169 let pos: *i64 = (sys_mmap(8)) as *i64
170 pos[0] = 0
171 let label: *u8 = sys_mmap(NX_HOL_MAX_NAME_LEN)
172 let name_save: *u8 = sys_mmap(NX_HOL_MAX_NAME_LEN)
173
174 while pos[0] < len {
175 let tok: i64 = nx_hol_next_token(buf, pos, len, label)
176 // Unknown punctuation -- skip, don't abort.
177 if tok == NX_HOL_TOK_NONE {
178 if pos[0] >= len { pos[0] = len }
179 }
180 if tok == NX_HOL_TOK_LET {
181 // Next ident is the name.
182 let t2: i64 = nx_hol_next_token(buf, pos, len, label)
183 if t2 == NX_HOL_TOK_IDENT {
184 // save name
185 var i: i64 = 0
186 while i < NX_HOL_MAX_NAME_LEN {
187 name_save[i] = label[i]
188 if label[i] == 0 { i = NX_HOL_MAX_NAME_LEN }
189 if i < NX_HOL_MAX_NAME_LEN { i = i + 1 }
190 }
191 // Expect '='
192 let t3: i64 = nx_hol_next_token(buf, pos, len, label)
193 if t3 == NX_HOL_TOK_EQUALS {
194 // Next token tells us the kind.
195 let t4: i64 = nx_hol_next_token(buf, pos, len, label)
196 if t4 == NX_HOL_TOK_PROVE { nx_hol_record_decl(db, NX_HOL_TOK_PROVE, name_save) }
197 if t4 == NX_HOL_TOK_AXIOM { nx_hol_record_decl(db, NX_HOL_TOK_AXIOM, name_save) }
198 if t4 == NX_HOL_TOK_DEFINE { nx_hol_record_decl(db, NX_HOL_TOK_DEFINE, name_save) }
199 }
200 }
201 }
202 }
203 return db
204}
205
206func nx_hol_count_kind(db: *HolDb, kind: i64) -> i64 {
207 var c: i64 = 0
208 var i: i64 = 0
209 while i < db.n_decls {
210 let d: *HolDecl = nx_hol_decl_at(db, i)
211 if d.kind == kind { c = c + 1 }
212 i = i + 1
213 }
214 return c
215}