Struct Header

Source
#[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>, }
Expand description

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 id, data fields that are parsed by MmbIndexBuilder::build.

Implementations§

Source§

impl Header

Source

pub fn check(&self, mmb: &[u8]) -> Result<(), ParseError>

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§

Source§

impl AsBytes for Header

Source§

fn as_bytes(&self) -> &[u8]

Gets the bytes of this value. Read more
Source§

fn as_bytes_mut(&mut self) -> &mut [u8]
where Self: FromBytes,

Gets the bytes of this value mutably. Read more
Source§

impl Clone for Header

Source§

fn clone(&self) -> Header

Returns a duplicate of the value. Read more
1.0.0 · Source§

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source. Read more
Source§

impl Debug for Header

Source§

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

Formats the value using the given formatter. Read more
Source§

impl Default for Header

Source§

fn default() -> Header

Returns the “default value” for a type. Read more
Source§

impl FromBytes for Header

Source§

fn new_zeroed() -> Self
where Self: Sized,

Creates an instance of Self from zeroed bytes.
Source§

impl Copy for Header

Auto Trait Implementations§

§

impl Freeze for Header

§

impl RefUnwindSafe for Header

§

impl Send for Header

§

impl Sync for Header

§

impl Unpin for Header

§

impl UnwindSafe for Header

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> CloneToUninit for T
where T: Clone,

Source§

unsafe fn clone_to_uninit(&self, dest: *mut u8)

🔬This is a nightly-only experimental API. (clone_to_uninit)
Performs copy-assignment from self to dest. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

Source§

impl<T> ToOwned for T
where T: Clone,

Source§

type Owned = T

The resulting type after obtaining ownership.
Source§

fn to_owned(&self) -> T

Creates owned data from borrowed data, usually by cloning. Read more
Source§

fn clone_into(&self, target: &mut T)

Uses borrowed data to replace owned data, usually by cloning. Read more
Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.