Enum mm0b_parser::ParseError [−][src]
pub enum ParseError {}Show variants
BadProofLen(usize), StmtCmdConv(u8), IndexKindConv(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
IndexKindConv(u8)
The u8 could not be converted to an [IndexKind] via TryFrom
The pair could not be converted to a ProofCmd via TryFrom
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.
Something using an mmb file unexpectedly exhausted its input source.
The parser wasn’t able to find the mmb magic number in the expected location.
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.)
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.
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 of IncompleteHeader
file_len: usize
The file length
The version is unrecognized.
Fields of BadVersion
parsed_version: u8
The MMB file version, greater than MM0B_VERSION
The portion of the mmb file that’s supposed to contain sorts was malformed.
The portion of the mmb file that’s supposed to contain terms was malformed.
The portion of the mmb file that’s supposed to contain thms was malformed.
The portion of the mmb file that’s supposed to contain proofs was malformed.
There was an issue parsing the index
Fields of BadIndexParse
p_index: usize
The (ostensible) location of the index in the file
An index table ID was used more than once, for an ID that does not accept duplicates
Fields of DuplicateIndexTable
An index lookup failed
Fields of BadIndexLookup
A ‘sorry’ was detected and the function has no support for it
An error with the provided message and location.
IoError(Error)
An error in IO.
Trait Implementations
Auto Trait Implementations
impl !RefUnwindSafe for ParseError
impl Send for ParseError
impl Sync for ParseError
impl Unpin for ParseError
impl !UnwindSafe for ParseError
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
pub fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> ToString for T where
T: Display + ?Sized,
[src]
T: Display + ?Sized,
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
pub fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,