nx_mizar_ingest_test.nx source
↩ module page · 29 lines · 1040 B
1// nx_mizar_ingest_test.nx -- smoke for Mizar M0 statement parser.
2
3import "syscalls.nx"
4import "nx_mizar_ingest.nx"
5
6func main() -> i64 {
7 let src: *u8 = sys_mmap(512)
8 var i: i64 = 0
9 while i < 512 { src[i] = 0; i = i + 1 }
10 // Mizar keywords recognized at M0: theorem / definition / scheme / lemma.
11 // Keyword detection requires whitespace separation.
12 let s: *u8 = "theorem definition scheme lemma theorem"
13 var k: i64 = 0
14 while s[k] != 0 {
15 src[k] = s[k]
16 k = k + 1
17 }
18 let n: i64 = k
19
20 let db: *MizarDb = nx_mizar_ingest_corpus(src, n)
21 // Expected: 2 theorems + 1 definition + 1 scheme + 1 lemma = 5 decls.
22 if db.n_decls != 5 { return 10 }
23 if nx_mizar_count_kind(db, NX_MIZAR_KIND_THEOREM) != 2 { return 11 }
24 if nx_mizar_count_kind(db, NX_MIZAR_KIND_DEFINITION) != 1 { return 12 }
25 if nx_mizar_count_kind(db, NX_MIZAR_KIND_SCHEME) != 1 { return 13 }
26 if nx_mizar_count_kind(db, NX_MIZAR_KIND_LEMMA) != 1 { return 14 }
27
28 return 0
29}