nx_hol_ingest.nx

buildroot/runtime/nx_hol_ingest.nx

7356 B215 linesdepth 5pulls 6 transitivereach 6 importersview sourcekind librarytopic hol

docs dependencies structs consts functions

about

nx_hol_ingest.nx -- HOL Light statement-level ingester (H0). HOL Light uses OCaml-embedded syntax: let NAME = prove (`<term>`, <tactic_script>);; let NAME = define `<recursive>`;; let NAME = new_axiom `<axiom>`;; let NAME = REWRITE_RULE [...] <theorem>;; (* OCaml comment *) We recognize the "let NAME = prove" pattern as the primary theorem declaration form, and "let NAME = new_axiom" for axioms. genealogy_id: harrison_hol_light_1996 lineage_id: higher_order_logic + statement_parsing

dependencies 4 imports · 6 importers

imports: nx_syscalls.nxnx_axioms.nxnx_lex.nxnx_ascii.nx

imported by: nx_corpus_drive.nxnx_five_systems_test.nxnx_hol_dir_ingest.nxnx_hol_ingest_test.nxnx_hol_stream_ingest.nxnx_hol_stream_ingest_test.nx

structs

39	struct HolDecl
46	struct HolDb

consts

27	const NX_HOL_TOK_NONE: i64 = 0
28	const NX_HOL_TOK_LET: i64 = 1
29	const NX_HOL_TOK_PROVE: i64 = 2
30	const NX_HOL_TOK_AXIOM: i64 = 3 // new_axiom
31	const NX_HOL_TOK_DEFINE: i64 = 4
32	const NX_HOL_TOK_IDENT: i64 = 5
33	const NX_HOL_TOK_EQUALS: i64 = 6
34	const NX_HOL_TOK_SEMICOLON: i64 = 7
36	const NX_HOL_MAX_NAME_LEN: i64 = 256
37	const NX_HOL_MAX_DECLS: i64 = 65536
44	const NX_HOL_DECL_BYTES: i64 = 16

functions

52	func nx_hol_db_alloc() -> *HolDb called by 1: nx_hol_ingest_corpus calls 1: sys_mmap
61	func nx_hol_decl_at(db: HolDb, i: i64) -> HolDecl called by 4: drive_hol nx_hol_record_decl nx_hol_count_kind nx_hol_stream_offer_all
72	func nx_hol_skip_ws(buf: u8, pos: i64, len: i64) -> i64 called by 1: nx_hol_next_token calls 1: nx_lex_is_ws
111	func nx_hol_next_token(buf: u8, pos: i64, len: i64, out_label: *u8) -> i64 called by 1: nx_hol_ingest_corpus calls 3: nx_hol_skip_ws nx_ascii_is_id_start nx_lex_is_id_cont_math
150	func nx_hol_record_decl(db: HolDb, kind: i64, label: u8) -> i64 called by 1: nx_hol_ingest_corpus calls 2: nx_hol_decl_at sys_mmap
167	func nx_hol_ingest_corpus(buf: u8, len: i64) -> HolDb called by 5: drive_hol main main main main calls 4: nx_hol_db_alloc sys_mmap nx_hol_next_token nx_hol_record_decl
206	func nx_hol_count_kind(db: *HolDb, kind: i64) -> i64 called by 2: main main calls 1: nx_hol_decl_at