nx_hol_ingest_test.nx source
↩ module page · 32 lines · 1073 B
1// nx_hol_ingest_test.nx -- smoke for HOL Light H0 statement parser.
2
3import "syscalls.nx"
4import "nx_hol_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 // HOL Light declarations look like:
11 // let NAME = prove(...);;
12 // let NAME = new_axiom ...;;
13 // let NAME = define ...;;
14 // The H0 ingester recognizes `let` followed by `=` followed by
15 // prove / new_axiom / define keywords.
16 let s: *u8 = "let T1 = prove let A1 = new_axiom let D1 = define let T2 = prove"
17 var k: i64 = 0
18 while s[k] != 0 {
19 src[k] = s[k]
20 k = k + 1
21 }
22 let n: i64 = k
23
24 let db: *HolDb = nx_hol_ingest_corpus(src, n)
25 // Expected: 2 proves + 1 axiom + 1 define = 4 decls.
26 if db.n_decls != 4 { return 10 }
27 if nx_hol_count_kind(db, NX_HOL_TOK_PROVE) != 2 { return 11 }
28 if nx_hol_count_kind(db, NX_HOL_TOK_AXIOM) != 1 { return 12 }
29 if nx_hol_count_kind(db, NX_HOL_TOK_DEFINE) != 1 { return 13 }
30
31 return 0
32}