nx_coq_ingest_test.nx source
↩ module page · 31 lines · 1153 B
1// nx_coq_ingest_test.nx -- smoke for Coq C0 statement parser.
2
3import "syscalls.nx"
4import "nx_coq_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 // Coq declaration keywords: Theorem / Lemma / Definition / Axiom /
11 // Fixpoint / Inductive. Case-sensitive per Coq convention.
12 let s: *u8 = "Theorem T1 Lemma L1 Definition D1 Axiom A1 Fixpoint F1 Inductive I1"
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: *CoqDb = nx_coq_ingest_corpus(src, n)
21 // Expected: 1 of each token type = 6 decls.
22 if db.n_decls != 6 { return 10 }
23 if nx_coq_count_kind(db, NX_COQ_TOK_THEOREM) != 1 { return 11 }
24 if nx_coq_count_kind(db, NX_COQ_TOK_LEMMA) != 1 { return 12 }
25 if nx_coq_count_kind(db, NX_COQ_TOK_DEFINITION) != 1 { return 13 }
26 if nx_coq_count_kind(db, NX_COQ_TOK_AXIOM) != 1 { return 14 }
27 if nx_coq_count_kind(db, NX_COQ_TOK_FIXPOINT) != 1 { return 15 }
28 if nx_coq_count_kind(db, NX_COQ_TOK_INDUCTIVE) != 1 { return 16 }
29
30 return 0
31}