Crate mm0b_parser[−][src]
Expand description
Import and export functionality for MMB binary proof format
See mm0-c/verifier.c for information on the MMB format.
Modules
Constants used in the MMB specification.
Macros
Something using an mmb file unexpectedly exhausted its input source.
Constructs a new trait for accessing a subcomponent of the index data, with automatic
impls for (), (A, B) and the subcomponent itself.
Wrap other errors to allow for some backtracing.
Structs
An iterator over the declaration stream.
An unfinished definition. The unify and proof streams should be used to write unify and
proof commands, respectively, and when completed the finish function will finalize the
streams and return the TermId of the new definition.
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).
A handle to an list of hypothesis names in the index.
This index subcomponent supplies hypothesis names for theorems.
A handle to an symbol name entry in the index.
An Mm0Writer is a buffer for constructing an MMB file when the total number of
sorts/terms/theorems is not yet known. It renders as much of the file as it can, so that the
actual file write consists mostly of memcpys.
A parsed MMB file, as a borrowed type. This does only shallow parsing;
additional parsing is done on demand via functions on this type.
An individual symbol name entry in the index.
A handle to an symbol name entry in the index.
An iterator over a proof command stream.
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.
This index subcomponent supplies names for sorts, terms, and theorems.
An index table entry, which is essentially an ID describing the table format, and some additional data to find the actual table.
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.
A reference to an entry in the term table.
An unfinished axiom or theorem. The unify and proof streams should be used to write unify
and proof commands, respectively, and when completed the finish function will finalize the
streams and return the ThmId of the new theorem.
An entry in the theorem table, which describes the “signature” of the axiom/theorem, the information needed to apply the theorem to use it in other theorems.
A reference to an entry in the theorem table.
An argument binder in a term/def or axiom/theorem.
An iterator over a unify command stream.
A handle to an list of variable names in the index.
This index subcomponent supplies variable names for terms and theorems.
Enums
StmtCmd aware of its position (represented by a typesafe integer)
in the mmb file relative to other declarations.
An error during parsing of an MMB file.
A proof command, which acts on a stack machine with the following components:
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.
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
The maximum number of bound variables supported by the MMB format.
bound mask: 10000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000
deps mask: 00000000_11111111_11111111_11111111_11111111_11111111_11111111_11111111
10000000_11111111_11111111_11111111_11111111_11111111_11111111_11111111
Traits
A trait for looking up a subcomponent of the index data.
A trait for looking up a subcomponent of the index data.
A trait for looking up a subcomponent of the index data.
A trait for populating the data field on the index X of an MmbFile given a table entry.
Signals that this type does not implement the respective index trait.
Signals that this type does not implement the respective index trait.
Signals that this type does not implement the respective index trait.
An implementation of Reopen is a writer that can be closed and reopened to read what was just
written.
Functions
Construct a &CStr from a prefix byte slice, by terminating at
the first nul character. The second output is the remainder of the slice.
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.
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.
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.
Converts n from u32 to usize or panics (which should not happen since we don’t support
16 bit systems).
Encode the command cmd (one of the STMT_*, PROOF_* or UNIFY_* commands
in this module, which are all 6 bit numbers) with the given data field
according to the following scheme:
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
Newtype for Type that makes some situations easier to read.
An MMB file parser with no index parser.
A basic index, usable for getting names of declarations and variables.
An MMB file parser with a basic index, usable for getting names of declarations and variables.