Enum ParseError

pub enum ParseError {
    BadProofLen(usize),
    StmtCmdConv(u8),
    ProofCmdConv(u8, u32),
    UnifyCmdConv(u8, u32),
    Trace(&'static str, u32, Box<ParseError>),
    Exhausted(&'static str, u32),
    BadMagic {
        parsed_magic: [u8; 4],
    },
    Unaligned,
    SuspectHeader,
    IncompleteHeader {
        file_len: usize,
    },
    BadVersion {
        parsed_version: u8,
    },
    BadSorts(Range<usize>),
    BadTerms(Range<usize>),
    BadThms(Range<usize>),
    BadProofs(Range<usize>),
    BadIndexParse {
        p_index: usize,
    },
    DuplicateIndexTable {
        p_index: usize,
        id: [u8; 4],
    },
    BadIndexLookup {
        p_index: Option<usize>,
    },
    SorryError,
    StrError(&'static str, usize),
    IoError(Error),
}

An error during parsing of an MMB file.

Variants

BadProofLen(usize)

If a malformed mmb file tries to sneak in a declar with a (cmd, data) pair whose data is a 0, try_next_decl will loop forever.

StmtCmdConv(u8)

The u8 could not be converted to a StmtCmd via TryFrom

ProofCmdConv(u8, u32)

The pair could not be converted to a ProofCmd via TryFrom

UnifyCmdConv(u8, u32)

The pair could not be converted to a UnifyCmd via TryFrom

Trace(&'static str, u32, Box<ParseError>)

Wrap other errors to allow for some backtracing.

Exhausted(&'static str, u32)

Something using an mmb file unexpectedly exhausted its input source.

BadMagic

The parser wasn’t able to find the mmb magic number in the expected location.

Fields

parsed_magic: [u8; 4]

The magic value that we actually found

Unaligned

The file is not aligned to a multiple of 8 bytes, which is required for parsing the term table. (This is generally true automatically for buffers sourced from a file or mmap, but it has to be explicitly ensured in unit tests.)

SuspectHeader

The header parsed “correctly”, but the data in the header indicates that either the header’s numbers are off, or the rest of the MMB file is bad. For example, a header stating that the term declarations begin at a position greater than the length of the MMB file.

IncompleteHeader

Used in cases where the parser fails trying to get the header, because there were too few bytes in the file to form a full header. Users might like to know how long the actual file was, just as a sanity check.

Fields

file_len: usize

The file length

BadVersion

The version is unrecognized.

Fields

parsed_version: u8

The MMB file version, greater than MM0B_VERSION

BadSorts(Range<usize>)

The portion of the mmb file that’s supposed to contain sorts was malformed.

BadTerms(Range<usize>)

The portion of the mmb file that’s supposed to contain terms was malformed.

BadThms(Range<usize>)

The portion of the mmb file that’s supposed to contain thms was malformed.

BadProofs(Range<usize>)

The portion of the mmb file that’s supposed to contain proofs was malformed.

BadIndexParse

There was an issue parsing the index

Fields

p_index: usize

The (ostensible) location of the index in the file

DuplicateIndexTable

An index table ID was used more than once, for an ID that does not accept duplicates

Fields

p_index: usize

The location of the index in the file

id: [u8; 4]

The duplicate ID

BadIndexLookup

An index lookup failed

Fields

p_index: Option<usize>

The (ostensible) location of the index in the file, or None if there is no index

SorryError

A ‘sorry’ was detected and the function has no support for it

StrError(&'static str, usize)

An error with the provided message and location.

IoError(Error)

An error in IO.

Trait Implementations

impl Debug for ParseError

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for ParseError

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl From<Error> for ParseError

fn from(e: Error) -> Self

Converts to this type from the input type.