nx_corpus_drive.nx source
↩ module page · 143 lines · 4360 B
1// nx_corpus_drive.nx -- unified theorem-corpus ingestion driver.
2//
3// Reads a source file (any of MetaMath / Lean / Mizar / Coq / HOL /
4// Isabelle), dispatches to the appropriate adapter, emits one
5// JSONL record per identified declaration to stdout.
6//
7// Usage:
8// nx_corpus_drive <file_path> <source_type>
9//
10// where <source_type> is one of:
11// metamath lean mizar coq hol isabelle
12//
13// Output format per line:
14// {"source":"<type>","file":"<basename>","kind":N,"number":N}
15//
16// This is the auto-ingestion entry point. Bash driver
17// nx_corpus_drive.sh walks a corpus directory and invokes this for
18// every recognized file, accumulating the unified corpus JSONL.
19
20// nx_safety_envelope:
21// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
22// sil_target: SIL1
23// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
24// verdict: NOT_YET_EVALUATED
25
26import "syscalls.nx"
27import "runtime.nx"
28import "nx_theorem_ingest.nx"
29import "nx_lean_ingest.nx"
30import "nx_mizar_ingest.nx"
31import "nx_coq_ingest.nx"
32import "nx_hol_ingest.nx"
33import "nx_isabelle_ingest.nx"
34
35// ===== JSONL emit helpers ==============================================
36
37func emit_record(source: *u8, kind: i64, number: i64) -> i64 {
38 print("{\"source\":\"" as *u8)
39 print(source)
40 print("\",\"kind\":" as *u8)
41 print_i64(kind)
42 print(",\"number\":" as *u8)
43 print_i64(number)
44 println("}" as *u8)
45 return 0
46}
47
48// ===== Per-source drivers ==============================================
49
50func drive_metamath(buf: *u8, len: i64) -> i64 {
51 let db: *IngestDb = nx_ingest_corpus(buf, len)
52 var i: i64 = 0
53 while i < db.n_theorems {
54 // MetaMath uses theorem labels; we emit number = i+1 (sequential).
55 emit_record("metamath" as *u8, 1, i + 1)
56 i = i + 1
57 }
58 return 0
59}
60
61func drive_lean(buf: *u8, len: i64) -> i64 {
62 let db: *LeanDb = nx_lean_ingest_corpus(buf, len)
63 var i: i64 = 0
64 while i < db.n_decls {
65 let d: *LeanDecl = nx_lean_decl_at(db, i)
66 emit_record("lean" as *u8, d.kind, i + 1)
67 i = i + 1
68 }
69 return 0
70}
71
72func drive_mizar(buf: *u8, len: i64) -> i64 {
73 let db: *MizarDb = nx_mizar_ingest_corpus(buf, len)
74 var i: i64 = 0
75 while i < db.n_decls {
76 let d: *MizarDecl = nx_mizar_decl_at(db, i)
77 emit_record("mizar" as *u8, d.kind, d.number)
78 i = i + 1
79 }
80 return 0
81}
82
83func drive_coq(buf: *u8, len: i64) -> i64 {
84 let db: *CoqDb = nx_coq_ingest_corpus(buf, len)
85 var i: i64 = 0
86 while i < db.n_decls {
87 let d: *CoqDecl = nx_coq_decl_at(db, i)
88 emit_record("coq" as *u8, d.kind, i + 1)
89 i = i + 1
90 }
91 return 0
92}
93
94func drive_hol(buf: *u8, len: i64) -> i64 {
95 let db: *HolDb = nx_hol_ingest_corpus(buf, len)
96 var i: i64 = 0
97 while i < db.n_decls {
98 let d: *HolDecl = nx_hol_decl_at(db, i)
99 emit_record("hol" as *u8, d.kind, i + 1)
100 i = i + 1
101 }
102 return 0
103}
104
105func drive_isabelle(buf: *u8, len: i64) -> i64 {
106 let db: *IsaDb = nx_isa_ingest_corpus(buf, len)
107 var i: i64 = 0
108 while i < db.n_decls {
109 let d: *IsaDecl = nx_isa_decl_at(db, i)
110 emit_record("isabelle" as *u8, d.kind, i + 1)
111 i = i + 1
112 }
113 return 0
114}
115
116// ===== Entry =============================================================
117
118func main(argc: i64, argv: *i64) -> i64 {
119 if argc < 3 {
120 println("usage: nx_corpus_drive <file_path> <source_type>" as *u8)
121 return 1
122 }
123 let path: *u8 = (argv[1]) as *u8
124 let stype: *u8 = (argv[2]) as *u8
125
126 let out_len: *i64 = (sys_mmap(8)) as *i64
127 out_len[0] = 0
128 let buf: *u8 = sys_read_file(path, out_len)
129 if (buf as i64) == 0 {
130 println("read_file_failed" as *u8)
131 return 2
132 }
133 let n: i64 = out_len[0]
134
135 if streq(stype, "metamath" as *u8) == 1 { return drive_metamath(buf, n) }
136 if streq(stype, "lean" as *u8) == 1 { return drive_lean(buf, n) }
137 if streq(stype, "mizar" as *u8) == 1 { return drive_mizar(buf, n) }
138 if streq(stype, "coq" as *u8) == 1 { return drive_coq(buf, n) }
139 if streq(stype, "hol" as *u8) == 1 { return drive_hol(buf, n) }
140 if streq(stype, "isabelle" as *u8) == 1 { return drive_isabelle(buf, n) }
141 println("unknown_source_type" as *u8)
142 return 3
143}