nx_mizar_stream_ingest.nx source
↩ module page · 110 lines · 3633 B
1// nx_mizar_stream_ingest.nx -- Mizar parser -> 5-defense runner.
2//
3// Synthesizes the canonical MML key "<ARTICLE>:th <N>" so dedup works
4// despite Mizar's multi-field identity (article, number, label).
5//
6// genealogy_id: mizar_to_qed_2026 + ingest_runner_composition
7// lineage_id: source_adapter_multi_field_key
8
9// nx_safety_envelope:
10// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
11// sil_target: SIL1
12// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
13// verdict: NOT_YET_EVALUATED
14
15import "nx_syscalls.nx"
16import "nx_tier.nx"
17import "nx_strconv.nx"
18import "nx_mizar_ingest.nx"
19import "nx_ingest_runner.nx"
20
21func nx_miz_strlen(s: *u8) -> nx_size {
22 var n: nx_size = 0
23 while s[n] != 0 { n = n + 1 }
24 return n
25}
26
27func nx_miz_str_copy(dst: *u8, off: nx_size, src: *u8) -> nx_size {
28 var i: nx_size = 0
29 while src[i] != 0 {
30 dst[off + i] = src[i]
31 i = i + 1
32 }
33 return off + i
34}
35
36func nx_miz_kind_tag(kind: nx_int, out: *u8) -> nx_size {
37 if kind == NX_MIZAR_KIND_THEOREM { out[0] = 116; out[1] = 104; out[2] = 32 }
38 if kind == NX_MIZAR_KIND_DEFINITION { out[0] = 100; out[1] = 101; out[2] = 102 }
39 if kind == NX_MIZAR_KIND_SCHEME { out[0] = 115; out[1] = 99; out[2] = 104 }
40 if kind == NX_MIZAR_KIND_LEMMA { out[0] = 108; out[1] = 101; out[2] = 109 }
41 if kind == NX_MIZAR_KIND_NONE { out[0] = 117; out[1] = 110; out[2] = 107 }
42 return 3
43}
44
45func nx_miz_key_build(d: *MizarDecl, key_out: *u8) -> nx_size {
46 var o: nx_size = nx_miz_str_copy(key_out, 0, d.article)
47 key_out[o] = 58 as u8
48 o = o + 1
49 nx_miz_kind_tag(d.kind as nx_int, ((key_out as nx_size) + o) as *u8)
50 o = o + 3
51 key_out[o] = 32 as u8
52 o = o + 1
53 let nbuf: *u8 = sys_mmap(NX_BUF_TINY)
54 let nlen: nx_int = nx_strconv_format_i64(d.number, nbuf)
55 var i: nx_size = 0
56 while i < (nlen as nx_size) {
57 key_out[o + i] = nbuf[i]
58 i = i + 1
59 }
60 o = o + (nlen as nx_size)
61 key_out[o] = 0
62 return o
63}
64
65func nx_miz_row_build(d: *MizarDecl, out: *u8) -> nx_size {
66 let p1: *u8 = "{\"source\":\"mizar\",\"kind\":" as *u8
67 var o: nx_size = nx_miz_str_copy(out, 0, p1)
68 let k: nx_int = d.kind as nx_int
69 out[o] = (0x30 + k) as u8
70 o = o + 1
71 let p2: *u8 = ",\"article\":\"" as *u8
72 o = nx_miz_str_copy(out, o, p2)
73 o = nx_miz_str_copy(out, o, d.article)
74 let p3: *u8 = "\",\"number\":" as *u8
75 o = nx_miz_str_copy(out, o, p3)
76 let nbuf: *u8 = sys_mmap(NX_BUF_TINY)
77 let nlen: nx_int = nx_strconv_format_i64(d.number, nbuf)
78 var i: nx_size = 0
79 while i < (nlen as nx_size) {
80 out[o + i] = nbuf[i]
81 i = i + 1
82 }
83 o = o + (nlen as nx_size)
84 let p4: *u8 = ",\"label\":\"" as *u8
85 o = nx_miz_str_copy(out, o, p4)
86 if (d.label as nx_size) != 0 { o = nx_miz_str_copy(out, o, d.label) }
87 let p5: *u8 = "\"}" as *u8
88 o = nx_miz_str_copy(out, o, p5)
89 return o
90}
91
92func nx_mizar_stream_offer_all(
93 db: *MizarDb,
94 run: *NxIngestRun,
95 row_buf: *u8,
96 key_buf: *u8
97) -> nx_int {
98 var n_emitted: nx_int = 0
99 var i: nx_int = 0
100 while i < db.n_decls {
101 let d: *MizarDecl = nx_mizar_decl_at(db, i)
102 let key_len: nx_size = nx_miz_key_build(d, key_buf)
103 let row_len: nx_size = nx_miz_row_build(d, row_buf)
104 let v: nx_int = nx_ingest_run_offer(run, key_buf, key_len, row_buf, row_len)
105 if v == NX_OFFER_EMITTED { n_emitted = n_emitted + 1 }
106 if v == NX_OFFER_BUDGET_HALT { return n_emitted }
107 i = i + 1
108 }
109 return n_emitted
110}