nx_mizar_stream_ingest_test.nx source
↩ module page · 48 lines · 1608 B
1// nx_mizar_stream_ingest_test.nx -- Mizar parser -> defense stack.
2
3import "nx_syscalls.nx"
4import "nx_tier.nx"
5import "nx_mizar_ingest.nx"
6import "nx_ingest_runner.nx"
7import "nx_mizar_stream_ingest.nx"
8import "nx_bloom_capacity.nx"
9
10func main() -> nx_exit {
11 let prefix: *u8 = "/tmp/nx_miz_si_t1" as *u8
12 let ckpt: *u8 = "/tmp/nx_miz_si_t1.checkpoint" as *u8
13
14 let corpus: *u8 = sys_mmap(512)
15 var i: nx_int = 0
16 while i < 512 { corpus[i] = 0; i = i + 1 }
17 let src: *u8 = "theorem definition scheme lemma theorem" as *u8
18 var k: nx_int = 0
19 while src[k] != 0 { corpus[k] = src[k]; k = k + 1 }
20 let corpus_len: nx_int = k
21
22 let db: *MizarDb = nx_mizar_ingest_corpus(corpus, corpus_len)
23 if db.n_decls < 1 { return 11 }
24
25 let run: *NxIngestRun = nx_ingest_run_new(
26 prefix,
27 100000 as nx_size, 4096 as nx_size,
28 100, NX_BLOOM_PROFILE_1PCT,
29 ckpt, 60000)
30 if run == (0 as *NxIngestRun) { return 21 }
31
32 let row_buf: *u8 = sys_mmap(512)
33 let key_buf: *u8 = sys_mmap(NX_BUF_SMALL)
34
35 let n1: nx_int = nx_mizar_stream_offer_all(db, run, row_buf, key_buf)
36 if n1 != db.n_decls { return 22 }
37 if nx_ingest_run_n_emitted(run) != db.n_decls { return 23 }
38
39 let n2: nx_int = nx_mizar_stream_offer_all(db, run, row_buf, key_buf)
40 if n2 != 0 { return 31 }
41 if nx_ingest_run_n_duplicate(run) != db.n_decls { return 32 }
42
43 if nx_ingest_run_n_shards(run) < 1 { return 41 }
44 nx_ingest_run_close(run)
45 let cp: *NxCheckpoint = nx_checkpoint_open(ckpt)
46 if nx_checkpoint_get(cp) != db.n_decls { return 51 }
47 return 0
48}