nx_qed_db_test.nx source
↩ module page · 69 lines · 2928 B
1// nx_qed_db_test.nx -- smoke for the QED-compatible database.
2
3import "syscalls.nx"
4import "nx_axioms.nx"
5import "nx_qed_db.nx"
6
7func main() -> i64 {
8 let db: *QedDb = nx_qed_db_alloc()
9 if db.n_entries != 0 { return 1 }
10 if db.capacity < 100 { return 2 }
11 if db.next_id != 1 { return 3 }
12
13 // Insert a NishiLang-local theorem (Pythagorean).
14 let axioms_py: *i64 = (sys_mmap(24)) as *i64
15 axioms_py[0] = NX_AX_GEO_TWO_POINTS_DETERMINE_LINE
16 axioms_py[1] = NX_AX_ALG_DISTRIBUTIVITY
17 axioms_py[2] = NX_AX_ALG_COMMUTATIVITY
18 let id1: i64 = nx_qed_insert(db, "Pythagorean.theorem",
19 NX_QED_SYS_NISHILANG_LOCAL,
20 axioms_py, 3, 12345,
21 NX_QED_VERIFY_LOCAL_PROVED)
22 if id1 != 1 { return 10 }
23 if db.n_entries != 1 { return 11 }
24
25 // Insert a TRUSTED_LEAN entry (no local proof; trust Lean's kernel).
26 let axioms_lean: *i64 = (sys_mmap(16)) as *i64
27 axioms_lean[0] = NX_AX_PEANO_PA5_INDUCTION
28 let id2: i64 = nx_qed_insert(db, "Nat.add_comm",
29 NX_QED_SYS_LEAN_MATHLIB,
30 axioms_lean, 1, 67890,
31 NX_QED_VERIFY_TRUSTED_LEAN)
32 if id2 != 2 { return 20 }
33
34 // Insert a MetaMath entry.
35 let id3: i64 = nx_qed_insert(db, "ax-mp",
36 NX_QED_SYS_METAMATH_SETMM,
37 axioms_lean, 1, 11111,
38 NX_QED_VERIFY_TRUSTED_METAMATH)
39 if id3 != 3 { return 30 }
40
41 // Insert a Mizar entry.
42 let id4: i64 = nx_qed_insert(db, "ARYTM_2:1",
43 NX_QED_SYS_MIZAR_MML,
44 axioms_lean, 1, 22222,
45 NX_QED_VERIFY_TRUSTED_MIZAR)
46 if id4 != 4 { return 40 }
47
48 // Counts by system.
49 if nx_qed_count_by_system(db, NX_QED_SYS_NISHILANG_LOCAL) != 1 { return 50 }
50 if nx_qed_count_by_system(db, NX_QED_SYS_LEAN_MATHLIB) != 1 { return 51 }
51 if nx_qed_count_by_system(db, NX_QED_SYS_METAMATH_SETMM) != 1 { return 52 }
52 if nx_qed_count_by_system(db, NX_QED_SYS_MIZAR_MML) != 1 { return 53 }
53 if nx_qed_count_by_system(db, NX_QED_SYS_COQ_STDLIB) != 0 { return 54 }
54
55 // Counts by verify.
56 if nx_qed_count_by_verify(db, NX_QED_VERIFY_LOCAL_PROVED) != 1 { return 60 }
57 if nx_qed_count_by_verify(db, NX_QED_VERIFY_TRUSTED_LEAN) != 1 { return 61 }
58 if nx_qed_count_by_verify(db, NX_QED_VERIFY_UNVERIFIED) != 0 { return 62 }
59
60 // Find by name.
61 if nx_qed_find_by_name(db, "Pythagorean.theorem") != 1 { return 70 }
62 if nx_qed_find_by_name(db, "Nat.add_comm") != 2 { return 71 }
63 if nx_qed_find_by_name(db, "nonexistent.thing") != -1 { return 72 }
64
65 // Emit db to stderr for inspection.
66 nx_qed_emit_all(2, db)
67
68 return 0
69}