Crate mm0b_parser

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 [MmbIndex] data, with automatic impls for (), (A, B) and the subcomponent itself.
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 sorts: [SortData; num_sorts] array (which we keep separate because of the dependency).
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 MMB file, as a borrowed type. This does only shallow parsing; additional parsing is done on demand via functions on this type.
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 Modifiers::sort_data: PURE, STRICT, PROVABLE, FREE.
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	StmtCmd aware of its position (represented by a typesafe integer) in the mmb file relative to other declarations.
ParseError	An error during parsing of an MMB file.
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 def or axiom/theorem. They are executed by the ProofCmd::Thm command in order to perform substitutions. The state of the unify stack machine is:

Constants

MAX_BOUND_VARS	The maximum number of bound variables supported by the MMB format.
TYPE_BOUND_MASK	bound mask: 10000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000
TYPE_DEPS_MASK	deps mask: 00000000_11111111_11111111_11111111_11111111_11111111_11111111_11111111
TYPE_SORT_MASK	10000000_11111111_11111111_11111111_11111111_11111111_11111111_11111111

Traits

HasHypNames	A trait for looking up a subcomponent of the data of [MmbIndex].
HasSymbolNames	A trait for looking up a subcomponent of the data of [MmbIndex].
HasVarNames	A trait for looking up a subcomponent of the data of [MmbIndex].
MmbIndexBuilder	A trait for populating the data field on [MmbIndex] given a table entry.
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 &CStr from a prefix byte slice, by terminating at the first nul character. The second output is the remainder of the slice.
find_header_error	In the event that MmbFile::parse fails when parsing the header, use this to get a more detailed error report (since the zerocopy parser for Header is just pass/fail). This method will panic if it’s not able to find a problem with the header, since a disagreement with MmbFile::parse means something else is going on that needs to looked at.
parse_cmd	From a (full) mmb file and a start position, parse the raw data for a command, which is a [(u8, u32)] pair of (cmd, data). Also returns the new start position, which is the old position plus the size of cmd, and the size of data which varies despite ending up as a u32.
try_next_cmd	Return the raw command data (a pair [(u8, u32)]) while ensuring that an iterator which is literally empty has terminated at the correct location, where the correct location is signalled by the presence of a 0 command.
u32_as_usize	Converts n from u32 to usize or panics (which should not happen since we don’t support 16 bit systems).
write_cmd_bytes	This is like [write_cmd], but it is followed by the byte array buf, and the initial data field is the length of the entire expression (the initial command byte, the data field, and the buffer). This can’t be expressed with write_cmd directly because of the circular dependency where the value of data determines the size of the initial command, which affects the value of data.

Type Definitions

Arg	Newtype for Type that makes some situations easier to read.
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.