code wiki / (root) / nx_coq_ingest.nx

nx_coq_ingest.nx

buildroot/runtime/nx_coq_ingest.nx

7869 B226 linesdepth 5pulls 6 transitivereach 6 importersview sourcekind librarytopic coq
docsdependenciesstructsconstsfunctions

about

nx_coq_ingest.nx -- Coq stdlib + MathComp statement-level ingester (C0). Coq's surface syntax for declarations: Theorem NAME : TYPE. Proof. ... Qed. Lemma NAME : TYPE. Proof. ... Qed. Definition NAME : TYPE := VALUE. Axiom NAME : TYPE. Fixpoint NAME ... := ... Inductive NAME : TYPE := ... (* comment *) We do NOT implement Coq's CIC kernel. Statement-level ingest only. genealogy_id: coquand_huet_1988 + coq_team lineage_id: formal_statement_parsing + dependent_type_theory

dependencies 4 imports · 6 importers

nx_syscalls.nx nx_axioms.nx nx_lex.nx nx_ascii.nx nx_coq_ingest.nx nx_coq_dir_ingest.nx nx_coq_ingest_test.nx nx_coq_stream_ingest.nx nx_coq_stream_ingest_test.nx nx_corpus_drive.nx nx_five_systems_test.nx

imports: nx_syscalls.nxnx_axioms.nxnx_lex.nxnx_ascii.nx

imported by: nx_coq_dir_ingest.nxnx_coq_ingest_test.nxnx_coq_stream_ingest.nxnx_coq_stream_ingest_test.nxnx_corpus_drive.nxnx_five_systems_test.nx

structs

40struct CoqDecl
47struct CoqDb

consts

28const NX_COQ_TOK_NONE: i64 = 0
29const NX_COQ_TOK_THEOREM: i64 = 1
30const NX_COQ_TOK_LEMMA: i64 = 2
31const NX_COQ_TOK_DEFINITION: i64 = 3
32const NX_COQ_TOK_AXIOM: i64 = 4
33const NX_COQ_TOK_FIXPOINT: i64 = 5
34const NX_COQ_TOK_INDUCTIVE: i64 = 6
35const NX_COQ_TOK_IDENT: i64 = 7
37const NX_COQ_MAX_NAME_LEN: i64 = 256
38const NX_COQ_MAX_DECLS: i64 = 65536
45const NX_COQ_DECL_BYTES: i64 = 16

functions

53func nx_coq_db_alloc() -> *CoqDb
called by 1: nx_coq_ingest_corpus calls 1: sys_mmap
62func nx_coq_decl_at(db: *CoqDb, i: i64) -> *CoqDecl
called by 4: nx_coq_record_declnx_coq_count_kindnx_coq_stream_offer_alldrive_coq
73func nx_coq_skip_ws(buf: *u8, pos: *i64, len: i64) -> i64
called by 1: nx_coq_next_token calls 1: nx_lex_is_ws
112func nx_coq_next_token(buf: *u8, pos: *i64, len: i64, out_label: *u8) -> i64
called by 1: nx_coq_ingest_corpus calls 3: nx_coq_skip_wsnx_ascii_is_id_startnx_lex_is_id_cont_qualified
160func nx_coq_record_decl(db: *CoqDb, kind: i64, label: *u8) -> i64
called by 1: nx_coq_ingest_corpus calls 2: nx_coq_decl_atsys_mmap
176func nx_coq_ingest_corpus(buf: *u8, len: i64) -> *CoqDb
called by 5: mainmainmaindrive_coqmain calls 4: nx_coq_db_allocsys_mmapnx_coq_next_tokennx_coq_record_decl
217func nx_coq_count_kind(db: *CoqDb, kind: i64) -> i64
called by 2: mainmain calls 1: nx_coq_decl_at