nx_isabelle_ingest_test.nx source
↩ module page · 32 lines · 1112 B
1// nx_isabelle_ingest_test.nx -- smoke for Isabelle I0 statement parser.
2
3import "syscalls.nx"
4import "nx_isabelle_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 // Isabelle/HOL declarations:
11 // theorem T1: "statement"
12 // lemma L1: "statement"
13 // definition D1: "definition"
14 // axiomatization where A1: "statement"
15 let s: *u8 = "theorem T1 lemma L1 definition D1 axiomatization A1 theorem T2"
16 var k: i64 = 0
17 while s[k] != 0 {
18 src[k] = s[k]
19 k = k + 1
20 }
21 let n: i64 = k
22
23 let db: *IsaDb = nx_isa_ingest_corpus(src, n)
24 // Expected: 2 theorems + 1 lemma + 1 definition + 1 axiomatization = 5 decls.
25 if db.n_decls != 5 { return 10 }
26 if nx_isa_count_kind(db, NX_ISA_TOK_THEOREM) != 2 { return 11 }
27 if nx_isa_count_kind(db, NX_ISA_TOK_LEMMA) != 1 { return 12 }
28 if nx_isa_count_kind(db, NX_ISA_TOK_DEFINITION) != 1 { return 13 }
29 if nx_isa_count_kind(db, NX_ISA_TOK_AXIOMATIZATION) != 1 { return 14 }
30
31 return 0
32}