nx_theorem_ingest_test.nx source
↩ module page · 39 lines · 1524 B
1// nx_theorem_ingest_test.nx -- smoke for theorem ingestion (P0 scope).
2
3import "syscalls.nx"
4import "nx_theorem_ingest.nx"
5
6func main() -> i64 {
7 // Build a tiny MetaMath-style corpus in memory and ingest it.
8 //
9 // Contents:
10 // $( comment $) -- skipped
11 // ax-1 $a wff $. -- axiom (label "ax-1")
12 // ax-mp $a wff $. -- modus ponens axiom
13 // pa5 $a wff $. -- Peano induction axiom
14 // thm1 $p wff $= ax-1 ax-mp $. -- proof citing two axioms
15 // thm2 $p wff $= pa5 ax-1 ax-mp $. -- proof citing three
16 //
17 // Expected: 3 axiom registrations + 2 proofs verified PASS.
18 let src: *u8 = sys_mmap(512)
19 var i: i64 = 0
20 while i < 512 { src[i] = 0; i = i + 1 }
21
22 // "$( c $) ax-1 $a wff $. ax-mp $a wff $. pa5 $a wff $. thm1 $p wff $= ax-1 ax-mp $. thm2 $p wff $= pa5 ax-1 ax-mp $."
23 let s: *u8 = "$( c $) ax-1 $a wff $. ax-mp $a wff $. pa5 $a wff $. thm1 $p wff $= ax-1 ax-mp $. thm2 $p wff $= pa5 ax-1 ax-mp $."
24 var k: i64 = 0
25 while s[k] != 0 {
26 src[k] = s[k]
27 k = k + 1
28 }
29 let n: i64 = k
30
31 let db: *IngestDb = nx_ingest_corpus(src, n)
32 // We expect 3 axioms + 2 proofs = 5 theorems registered.
33 if db.n_theorems < 3 { return 10 }
34 // Both proofs should have PASSED verify.
35 if db.n_passed != 2 { return 20 }
36 if db.n_rejected != 0 { return 21 }
37
38 return 0
39}