code wiki / (root) / nx_isabelle_ingest.nx

nx_isabelle_ingest.nx

buildroot/runtime/nx_isabelle_ingest.nx

6587 B200 linesdepth 5pulls 6 transitivereach 6 importersview sourcekind librarytopic isabelle
docsdependenciesstructsconstsfunctions

about

nx_isabelle_ingest.nx -- Isabelle/HOL .thy statement-level ingester (I0). Isabelle/HOL .thy file declarations: theorem NAME: "<statement>" <proof> lemma NAME: "<statement>" by ... definition NAME: "<definition>" axiomatization where NAME: "<axiom>" (* comment *) genealogy_id: nipkow_paulson_wenzel_2002 lineage_id: higher_order_logic + isar_proof_language

dependencies 4 imports · 6 importers

nx_syscalls.nx nx_axioms.nx nx_lex.nx nx_ascii.nx nx_isabelle_ingest.nx nx_corpus_drive.nx nx_five_systems_test.nx nx_isabelle_dir_ingest.nx nx_isabelle_ingest_test.nx nx_isabelle_stream_ingest.nx nx_isabelle_stream_ingest_test.nx

imports: nx_syscalls.nxnx_axioms.nxnx_lex.nxnx_ascii.nx

imported by: nx_corpus_drive.nxnx_five_systems_test.nxnx_isabelle_dir_ingest.nxnx_isabelle_ingest_test.nxnx_isabelle_stream_ingest.nxnx_isabelle_stream_ingest_test.nx

structs

35struct IsaDecl
42struct IsaDb

consts

25const NX_ISA_TOK_NONE: i64 = 0
26const NX_ISA_TOK_THEOREM: i64 = 1
27const NX_ISA_TOK_LEMMA: i64 = 2
28const NX_ISA_TOK_DEFINITION: i64 = 3
29const NX_ISA_TOK_AXIOMATIZATION: i64 = 4
30const NX_ISA_TOK_IDENT: i64 = 5
32const NX_ISA_MAX_NAME_LEN: i64 = 256
33const NX_ISA_MAX_DECLS: i64 = 65536
40const NX_ISA_DECL_BYTES: i64 = 16

functions

48func nx_isa_db_alloc() -> *IsaDb
called by 1: nx_isa_ingest_corpus calls 1: sys_mmap
57func nx_isa_decl_at(db: *IsaDb, i: i64) -> *IsaDecl
called by 4: drive_isabellenx_isa_record_declnx_isa_count_kindnx_isabelle_stream_offer_all
67func nx_isa_skip_ws(buf: *u8, pos: *i64, len: i64) -> i64
called by 1: nx_isa_next_token calls 1: nx_lex_is_ws
106func nx_isa_next_token(buf: *u8, pos: *i64, len: i64, out_label: *u8) -> i64
called by 1: nx_isa_ingest_corpus calls 3: nx_isa_skip_wsnx_ascii_is_id_startnx_lex_is_id_cont_math
143func nx_isa_record_decl(db: *IsaDb, kind: i64, label: *u8) -> i64
called by 1: nx_isa_ingest_corpus calls 2: nx_isa_decl_atsys_mmap
159func nx_isa_ingest_corpus(buf: *u8, len: i64) -> *IsaDb
called by 5: drive_isabellemainmainmainmain calls 4: nx_isa_db_allocsys_mmapnx_isa_next_tokennx_isa_record_decl
191func nx_isa_count_kind(db: *IsaDb, kind: i64) -> i64
called by 2: mainmain calls 1: nx_isa_decl_at