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 index 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.

DefBuilder

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.

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 hypothesis names for theorems.

HypsEntryRef

A handle to an symbol name entry in the index.

Mm0Writer

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.

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.

ThmBuilder

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.

ThmEntry

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.

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 variable names for 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 index data.

HasSymbolNames

A trait for looking up a subcomponent of the index data.

HasVarNames

A trait for looking up a subcomponent of the index data.

MmbIndexBuilder

A trait for populating the data field on the index X of an MmbFile 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.

Reopen

An implementation of Reopen is a writer that can be closed and reopened to read what was just written.

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

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:

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 Aliases

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.