nx_five_systems_test.nx source
↩ module page · 83 lines · 3350 B
1// nx_five_systems_test.nx -- verify all five source adapters work
2// end-to-end through the pipeline.
3
4import "syscalls.nx"
5import "nx_axioms.nx"
6import "nx_theorem_ingest.nx"
7import "nx_lean_ingest.nx"
8import "nx_mizar_ingest.nx"
9import "nx_coq_ingest.nx"
10import "nx_hol_ingest.nx"
11import "nx_isabelle_ingest.nx"
12
13func main() -> i64 {
14 let buf: *u8 = sys_mmap(512)
15
16 // === MetaMath ===
17 var i: i64 = 0
18 while i < 512 { buf[i] = 0; i = i + 1 }
19 let mm: *u8 = "ax-1 $a wff $. thm1 $p wff $= ax-1 $."
20 var k: i64 = 0
21 while mm[k] != 0 { buf[k] = mm[k]; k = k + 1 }
22 let mm_db: *IngestDb = nx_ingest_corpus(buf, k)
23 if mm_db.n_theorems < 1 { return 1 }
24
25 // === Lean ===
26 var i2: i64 = 0
27 while i2 < 512 { buf[i2] = 0; i2 = i2 + 1 }
28 let ln: *u8 = "theorem Nat_add_comm lemma helper axiom ax_choice"
29 var k2: i64 = 0
30 while ln[k2] != 0 { buf[k2] = ln[k2]; k2 = k2 + 1 }
31 let ln_db: *LeanDb = nx_lean_ingest_corpus(buf, k2)
32 if ln_db.n_decls != 3 { return 2 }
33
34 // === Mizar ===
35 var i3: i64 = 0
36 while i3 < 512 { buf[i3] = 0; i3 = i3 + 1 }
37 let mz: *u8 = "theorem definition scheme theorem lemma"
38 var k3: i64 = 0
39 while mz[k3] != 0 { buf[k3] = mz[k3]; k3 = k3 + 1 }
40 let mz_db: *MizarDb = nx_mizar_ingest_corpus(buf, k3)
41 if mz_db.n_decls < 4 { return 3 }
42
43 // === Coq ===
44 var i4: i64 = 0
45 while i4 < 512 { buf[i4] = 0; i4 = i4 + 1 }
46 let cq: *u8 = "Theorem add_comm Lemma helper Definition pred Axiom choice Fixpoint factorial"
47 var k4: i64 = 0
48 while cq[k4] != 0 { buf[k4] = cq[k4]; k4 = k4 + 1 }
49 let cq_db: *CoqDb = nx_coq_ingest_corpus(buf, k4)
50 if cq_db.n_decls != 5 { return 4 }
51 if nx_coq_count_kind(cq_db, NX_COQ_TOK_THEOREM) != 1 { return 5 }
52 if nx_coq_count_kind(cq_db, NX_COQ_TOK_LEMMA) != 1 { return 6 }
53 if nx_coq_count_kind(cq_db, NX_COQ_TOK_DEFINITION) != 1 { return 7 }
54 if nx_coq_count_kind(cq_db, NX_COQ_TOK_AXIOM) != 1 { return 8 }
55 if nx_coq_count_kind(cq_db, NX_COQ_TOK_FIXPOINT) != 1 { return 9 }
56
57 // === HOL Light ===
58 var i5: i64 = 0
59 while i5 < 512 { buf[i5] = 0; i5 = i5 + 1 }
60 let hl: *u8 = "let ADD_COMM = prove let TWO_DEF = define let CHOICE = new_axiom"
61 var k5: i64 = 0
62 while hl[k5] != 0 { buf[k5] = hl[k5]; k5 = k5 + 1 }
63 let hl_db: *HolDb = nx_hol_ingest_corpus(buf, k5)
64 if hl_db.n_decls != 3 { return 10 }
65 if nx_hol_count_kind(hl_db, NX_HOL_TOK_PROVE) != 1 { return 11 }
66 if nx_hol_count_kind(hl_db, NX_HOL_TOK_DEFINE) != 1 { return 12 }
67 if nx_hol_count_kind(hl_db, NX_HOL_TOK_AXIOM) != 1 { return 13 }
68
69 // === Isabelle / HOL ===
70 var i6: i64 = 0
71 while i6 < 512 { buf[i6] = 0; i6 = i6 + 1 }
72 let isa: *u8 = "theorem add_comm lemma helper definition pred axiomatization choice"
73 var k6: i64 = 0
74 while isa[k6] != 0 { buf[k6] = isa[k6]; k6 = k6 + 1 }
75 let isa_db: *IsaDb = nx_isa_ingest_corpus(buf, k6)
76 if isa_db.n_decls != 4 { return 14 }
77 if nx_isa_count_kind(isa_db, NX_ISA_TOK_THEOREM) != 1 { return 15 }
78 if nx_isa_count_kind(isa_db, NX_ISA_TOK_LEMMA) != 1 { return 16 }
79 if nx_isa_count_kind(isa_db, NX_ISA_TOK_DEFINITION) != 1 { return 17 }
80 if nx_isa_count_kind(isa_db, NX_ISA_TOK_AXIOMATIZATION) != 1 { return 18 }
81
82 return 0
83}