Struct mm0b_parser::MmbFile

#[non_exhaustive]
pub struct MmbFile<'a, X = BasicIndex<'a>> {
    pub header: Header,
    pub buf: &'a [u8],
    pub sorts: &'a [SortData],
    pub terms: &'a [TermEntry],
    pub thms: &'a [ThmEntry],
    pub index: X,
}

A parsed MMB file, as a borrowed type. This does only shallow parsing; additional parsing is done on demand via functions on this type.

Fields (Non-exhaustive)

Non-exhaustive structs could have additional fields added in future. Therefore, non-exhaustive structs cannot be constructed in external crates using the traditional Struct { .. } syntax; cannot be matched against without a wildcard ..; and struct update syntax will not work.

header: Header

The file’s header.

buf: &'a [u8]

The full file

sorts: &'a [SortData]

The sort table

terms: &'a [TermEntry]

The term table

thms: &'a [ThmEntry]

The theorem table

index: X

The index, if provided.

Implementations

impl<'a, X> MmbFile<'a, X>

pub fn bad_index_lookup(&self) -> ParseError

For error reporting after the initial parse.

pub fn p_index(&self) -> Option<usize>

For error reporting after the initial parse.

pub fn bad_index_parse(&self) -> ParseError

Returns a bad index parse error, for error reporting during index parsing.

impl<'a, X: MmbIndexBuilder<'a>> MmbFile<'a, X>

pub fn parse(buf: &'a [u8]) -> Result<Self, ParseError>

Parse a MmbFile from a file, provided as a byte slice. This does the minimum checking to construct the parsed object, it is not a verifier.

impl<'a, X> MmbFile<'a, X>

pub fn sort(&self, n: SortId) -> Option<SortData>

Get the sort data for a SortId.

pub fn term(&self, n: TermId) -> Option<TermRef<'a>>

Get the term data for a TermId.

pub fn thm(&self, n: ThmId) -> Option<ThmRef<'a>>

Get the theorem data for a ThmId.

pub fn proof(&self) -> DeclIter<'a>

Get the proof stream for the file.

impl<'a, X: HasSymbolNames<'a>> MmbFile<'a, X>

pub fn sort_index(&self, n: SortId) -> Option<NameEntryRef<'a>>

Get the index entry for a sort.

pub fn term_index(&self, n: TermId) -> Option<NameEntryRef<'a>>

Get the index entry for a term.

pub fn thm_index(&self, n: ThmId) -> Option<NameEntryRef<'a>>

Get the index entry for a theorem.

pub fn stmt_index(&self, stmt: NumdStmtCmd) -> Option<NameEntryRef<'a>>

Convenience function for getting an index without having to destructure the StmtCmd every time.

pub fn try_sort_name(&self, n: SortId) -> Option<&'a str>

Get the name of a sort, if present.

pub fn try_term_name(&self, n: TermId) -> Option<&'a str>

Get the name of a term, if present.

pub fn try_thm_name(&self, n: ThmId) -> Option<&'a str>

Get the name of a theorem, if present.

pub fn sort_name(&self, n: SortId) -> Cow<'a, str>

Get the name of a sort, supplying a default name of the form s123 if the index is not present.

pub fn term_name(&self, n: TermId) -> Cow<'a, str>

Get the name of a term, supplying a default name of the form t123 if the index is not present.

pub fn thm_name(&self, n: ThmId) -> Cow<'a, str>

Get the name of a theorem, supplying a default name of the form T123 if the index is not present.

impl<'a, X: HasVarNames<'a>> MmbFile<'a, X>

pub fn term_vars_opt(&self, n: TermId) -> Option<VarListRef<'a>>

Get the list of variables used in a term, or None if the index does not exist.

pub fn term_vars(&self, n: TermId) -> VarListRef<'a>

Get the list of variables used in a term.

pub fn thm_vars_opt(&self, n: ThmId) -> Option<VarListRef<'a>>

Get the list of variables used in a theorem, or None if the index does not exist.

pub fn thm_vars(&self, n: ThmId) -> VarListRef<'a>

Get the list of variables used in a theorem.

pub fn stmt_vars(&self, stmt: NumdStmtCmd) -> VarListRef<'a>

Convenience function for getting an index without having to destructure the StmtCmd every time.

impl<'a, X: HasHypNames<'a>> MmbFile<'a, X>

pub fn thm_hyps_opt(&self, n: ThmId) -> Option<HypListRef<'a>>

Get the hypothesis name list for a theorem.

pub fn thm_hyps(&self, n: ThmId) -> HypListRef<'a>

Get the hypothesis name list for a theorem.

pub fn stmt_hyps(&self, stmt: NumdStmtCmd) -> HypListRef<'a>

Convenience function for getting an index without having to destructure the StmtCmd every time.

Trait Implementations

impl<'a, X: Debug> Debug for MmbFile<'a, X>

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

Formats the value using the given formatter.

impl<'a, X: Default> Default for MmbFile<'a, X>

fn default() -> MmbFile<'a, X>

Returns the “default value” for a type.