nx_lean_ingest_test.nx source
↩ module page · 27 lines · 883 B
1// nx_lean_ingest_test.nx -- smoke for the Lean statement parser.
2
3import "syscalls.nx"
4import "nx_lean_ingest.nx"
5
6func main() -> i64 {
7 // Build a tiny Lean-style corpus in memory.
8 let src: *u8 = sys_mmap(512)
9 var i: i64 = 0
10 while i < 512 { src[i] = 0; i = i + 1 }
11 let s: *u8 = "axiom ax_choice theorem Nat_add_comm lemma helper_lemma theorem polynomial_FA"
12 var k: i64 = 0
13 while s[k] != 0 {
14 src[k] = s[k]
15 k = k + 1
16 }
17 let n: i64 = k
18
19 let db: *LeanDb = nx_lean_ingest_corpus(src, n)
20 // Expected: 1 axiom + 2 theorems + 1 lemma = 4 decls.
21 if db.n_decls != 4 { return 10 }
22 if nx_lean_count_kind(db, NX_LEAN_TOK_AXIOM) != 1 { return 11 }
23 if nx_lean_count_kind(db, NX_LEAN_TOK_THEOREM) != 2 { return 12 }
24 if nx_lean_count_kind(db, NX_LEAN_TOK_LEMMA) != 1 { return 13 }
25
26 return 0
27}