nx_hol_stream_ingest.nx source
↩ module page · 65 lines · 1934 B
1// nx_hol_stream_ingest.nx -- HOL Light parser -> 5-defense runner.
2//
3// Output JSONL row: {"source":"hol","kind":N,"name":"..."}
4//
5// genealogy_id: hol_light_to_qed_2026 + ingest_runner_composition
6// lineage_id: source_adapter
7
8// nx_safety_envelope:
9// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
10// sil_target: SIL1
11// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
12// verdict: NOT_YET_EVALUATED
13
14import "nx_syscalls.nx"
15import "nx_tier.nx"
16import "nx_hol_ingest.nx"
17import "nx_ingest_runner.nx"
18
19func nx_hol_strlen(s: *u8) -> nx_size {
20 var n: nx_size = 0
21 while s[n] != 0 { n = n + 1 }
22 return n
23}
24
25func nx_hol_str_copy(dst: *u8, off: nx_size, src: *u8) -> nx_size {
26 var i: nx_size = 0
27 while src[i] != 0 {
28 dst[off + i] = src[i]
29 i = i + 1
30 }
31 return off + i
32}
33
34func nx_hol_row_build(d: *HolDecl, out: *u8) -> nx_size {
35 let p1: *u8 = "{\"source\":\"hol\",\"kind\":" as *u8
36 var o: nx_size = nx_hol_str_copy(out, 0, p1)
37 let k: nx_int = d.kind as nx_int
38 out[o] = (0x30 + k) as u8
39 o = o + 1
40 let p2: *u8 = ",\"name\":\"" as *u8
41 o = nx_hol_str_copy(out, o, p2)
42 o = nx_hol_str_copy(out, o, d.name)
43 let p3: *u8 = "\"}" as *u8
44 o = nx_hol_str_copy(out, o, p3)
45 return o
46}
47
48func nx_hol_stream_offer_all(
49 db: *HolDb,
50 run: *NxIngestRun,
51 row_buf: *u8
52) -> nx_int {
53 var n_emitted: nx_int = 0
54 var i: nx_int = 0
55 while i < db.n_decls {
56 let d: *HolDecl = nx_hol_decl_at(db, i)
57 let row_len: nx_size = nx_hol_row_build(d, row_buf)
58 let key_len: nx_size = nx_hol_strlen(d.name)
59 let v: nx_int = nx_ingest_run_offer(run, d.name, key_len, row_buf, row_len)
60 if v == NX_OFFER_EMITTED { n_emitted = n_emitted + 1 }
61 if v == NX_OFFER_BUDGET_HALT { return n_emitted }
62 i = i + 1
63 }
64 return n_emitted
65}