Struct mm0b_parser::Header [−][src]
#[repr(C, align(8))]pub struct Header { pub magic: [u8; 4], pub version: u8, pub num_sorts: u8, pub reserved: [u8; 2], pub num_terms: U32<LE>, pub num_thms: U32<LE>, pub p_terms: U32<LE>, pub p_thms: U32<LE>, pub p_proof: U32<LE>, pub reserved2: [u8; 4], pub p_index: U64<LE>, }
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).
Fields
magic: [u8; 4]
The magic number, which is used to identify this as an mmb file. Must be
equal to MM0B_MAGIC
= "MM0B"
.
version: u8
The MMB format version number. Must equal MM0B_VERSION
= 1.
num_sorts: u8
The number of sorts in the file. This is limited to 128.
reserved: [u8; 2]
Padding.
num_terms: U32<LE>
The number of terms and defs in the file.
num_thms: U32<LE>
The number of axioms and theorems in the file.
p_terms: U32<LE>
The pointer to the term table of type [
TermEntry
; num_terms]
.
p_thms: U32<LE>
The pointer to the theorem table of type [
ThmEntry
; num_thms]
.
p_proof: U32<LE>
The pointer to the declaration stream.
reserved2: [u8; 4]
Padding.
p_index: U64<LE>
The pointer to the index header, an array of 1 + num_sorts + num_terms + num_thms
pointers to [IndexEntry
] nodes.
Implementations
impl Header
[src]
pub fn check(&self, mmb: &[u8]) -> Result<(), ParseError>
[src]
On top of the magic number and version checks, perform a non-exhaustive list of miscellaneous checks to see whether there are issues with the header that won’t be caught by the type system or the integer parsers.
For example, none of the pointers in the header should be greater than the length of the file, the terms pointer should be less than the theorems pointer, etc.
Trait Implementations
impl AsBytes for Header
[src]
fn only_derive_is_allowed_to_implement_this_trait() where
Self: Sized,
[src]
Self: Sized,
pub fn as_bytes(&self) -> &[u8]ⓘ
[src]
pub fn as_bytes_mut(&mut self) -> &mut [u8]ⓘ where
Self: FromBytes,
[src]
Self: FromBytes,
impl Clone for Header
[src]
impl Copy for Header
[src]
impl Debug for Header
[src]
impl Default for Header
[src]
impl FromBytes for Header
[src]
fn only_derive_is_allowed_to_implement_this_trait() where
Self: Sized,
[src]
Self: Sized,
Auto Trait Implementations
impl RefUnwindSafe for Header
impl Send for Header
impl Sync for Header
impl Unpin for Header
impl UnwindSafe for Header
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> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
pub fn to_owned(&self) -> T
[src]
pub fn clone_into(&self, target: &mut T)
[src]
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>,