Crate mm0b_parser[−][src]
Import and export functionality for MMB binary proof format
See mm0-c/verifier.c
for information on the MMB format.
Modules
cmd | Constants used in the MMB specification. |
Macros
exhausted | Something using an mmb file unexpectedly exhausted its input source. |
make_index_trait | Constructs a new trait for accessing a subcomponent of the [ |
trace | Wrap other errors to allow for some backtracing. |
Structs
DeclIter | An iterator over the declaration stream. |
Header | The header of an MMB file, which is always in the first bytes of the file.
It is followed by a |
HypListRef | A handle to an list of hypothesis names in the index. |
HypNames | This index subcomponent supplies names for sorts, terms, and theorems. |
HypsEntryRef | A handle to an symbol name entry in the index. |
MmbFile | A parsed |
NameEntry | An individual symbol name entry in the index. |
NameEntryRef | A handle to an symbol name entry in the index. |
ProofIter | An iterator over a proof command stream. |
SortData | A sort entry in the file header. Each sort is one byte, which can be any combination
of the modifiers in |
SymbolNames | This index subcomponent supplies names for sorts, terms, and theorems. |
TableEntry | An index table entry, which is essentially an ID describing the table format, and some additional data to find the actual table. |
TermEntry | An entry in the term table, which describes the “signature” of the term/def, the information needed to apply the term and use it in theorems. |
TermRef | A reference to an entry in the term table. |
ThmEntry | An entry in the term table, which describes the “signature” of the axiom/theorem, the information needed to apply the theorem to use it in other theorems. |
ThmRef | A reference to an entry in the theorem table. |
Type | An argument binder in a term/def or axiom/theorem. |
UnifyIter | An iterator over a unify command stream. |
VarListRef | A handle to an list of variable names in the index. |
VarNames | This index subcomponent supplies names for sorts, terms, and theorems. |
Enums
NumdStmtCmd |
|
ParseError | An error during parsing of an |
ProofCmd | A proof command, which acts on a stack machine with the following components: |
StmtCmd | The main part of the proof consists of a sequence of declarations, and these commands denote the different kind of declaration that can be introduced. |
UnifyCmd | Unify commands appear in the header data for a |
Constants
MAX_BOUND_VARS | The maximum number of bound variables supported by the MMB format. |
TYPE_BOUND_MASK | bound mask: |
TYPE_DEPS_MASK | deps mask: |
TYPE_SORT_MASK |
|
Traits
HasHypNames | A trait for looking up a subcomponent of the data of [ |
HasSymbolNames | A trait for looking up a subcomponent of the data of [ |
HasVarNames | A trait for looking up a subcomponent of the data of [ |
MmbIndexBuilder | A trait for populating the |
NoHypNames | Signals that this type does not implement the respective index trait. |
NoSymbolNames | Signals that this type does not implement the respective index trait. |
NoVarNames | Signals that this type does not implement the respective index trait. |
Functions
cstr_from_bytes_prefix | Construct a |
find_header_error | In the event that |
parse_cmd | From a (full) mmb file and a start position, parse the raw data
for a command, which is a |
try_next_cmd | Return the raw command data (a pair |
u32_as_usize | Converts |
write_cmd_bytes | This is like [ |
Type Definitions
Arg | Newtype for |
BareMmbFile | An MMB file parser with no index parser. |
BasicIndex | A basic index, usable for getting names of declarations and variables. |
BasicMmbFile | An MMB file parser with a basic index, usable for getting names of declarations and variables. |