Struct mm0b_parser::MmbFile[−][src]

pub struct MmbFile<'a, X = BasicIndex<'a>> {
    pub header: Header,
    pub index: X,
    // some fields omitted
}

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

header: Header

The file’s header.

index: X

The index, if provided.

Implementations

impl<'a, X> MmbFile<'a, X>[src]

#[must_use]
pub fn bad_index_lookup(&self) -> ParseError[src]

For error reporting after the initial parse.

#[must_use]
pub fn p_index(&self) -> Option<usize>[src]

For error reporting after the initial parse.

pub fn bad_index_parse(&self) -> ParseError[src]

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

impl<'a, X: MmbIndexBuilder<'a>> MmbFile<'a, X>[src]

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

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>[src]

#[must_use]
pub fn sort(&self, n: SortId) -> Option<SortData>[src]

Get the sort data for a SortId.

#[must_use]
pub fn term(&self, n: TermId) -> Option<TermRef<'a>>[src]

Get the term data for a TermId.

#[must_use]
pub fn thm(&self, n: ThmId) -> Option<ThmRef<'a>>[src]

Get the theorem data for a ThmId.

#[must_use]
pub fn proof(&self) -> DeclIter<'a>ⓘ

Notable traits for DeclIter<'a>

impl<'a> Iterator for DeclIter<'a> type Item = Result<(NumdStmtCmd, ProofIter<'a>), ParseError>;
[src]

Get the proof stream for the file.

impl<'a, X: HasSymbolNames<'a>> MmbFile<'a, X>[src]

#[must_use]
pub fn sort_index(&self, n: SortId) -> Option<NameEntryRef<'a>>[src]

Get the index entry for a sort.

#[must_use]
pub fn term_index(&self, n: TermId) -> Option<NameEntryRef<'a>>[src]

Get the index entry for a term.

#[must_use]
pub fn thm_index(&self, n: ThmId) -> Option<NameEntryRef<'a>>[src]

Get the index entry for a theorem.

#[must_use]
pub fn stmt_index(&self, stmt: NumdStmtCmd) -> Option<NameEntryRef<'a>>[src]

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

#[must_use]
pub fn term_name(&self, n: TermId) -> Cow<'a, str>[src]

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

#[must_use]
pub fn thm_name(&self, n: ThmId) -> Cow<'a, str>[src]

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

#[must_use]
pub fn sort_name(&self, n: SortId) -> Cow<'a, str>[src]

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

impl<'a, X: HasVarNames<'a>> MmbFile<'a, X>[src]

#[must_use]
pub fn term_vars_opt(&self, n: TermId) -> Option<VarListRef<'a>>[src]

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

#[must_use]
pub fn term_vars(&self, n: TermId) -> VarListRef<'a>[src]

Get the list of variables used in a term.

#[must_use]
pub fn thm_vars_opt(&self, n: ThmId) -> Option<VarListRef<'a>>[src]

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

#[must_use]
pub fn thm_vars(&self, n: ThmId) -> VarListRef<'a>[src]

Get the list of variables used in a theorem.

#[must_use]
pub fn stmt_vars(&self, stmt: NumdStmtCmd) -> VarListRef<'a>[src]

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

impl<'a, X: HasHypNames<'a>> MmbFile<'a, X>[src]

#[must_use]
pub fn thm_hyps_opt(&self, n: ThmId) -> Option<HypListRef<'a>>[src]

Get the hypothesis name list for a theorem.

#[must_use]
pub fn thm_hyps(&self, n: ThmId) -> HypListRef<'a>[src]

Get the hypothesis name list for a theorem.

#[must_use]
pub fn stmt_hyps(&self, stmt: NumdStmtCmd) -> HypListRef<'a>[src]

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>[src]

impl<'a, X: Default> Default for MmbFile<'a, X>[src]

Auto Trait Implementations

impl<'a, X> RefUnwindSafe for MmbFile<'a, X> where
    X: RefUnwindSafe, 

impl<'a, X> Send for MmbFile<'a, X> where
    X: Send, 

impl<'a, X> Sync for MmbFile<'a, X> where
    X: Sync, 

impl<'a, X> Unpin for MmbFile<'a, X> where
    X: Unpin, 

impl<'a, X> UnwindSafe for MmbFile<'a, X> where
    X: UnwindSafe, 

Blanket Implementations

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

impl<T> Borrow<T> for T where
    T: ?Sized, [src]

impl<T> BorrowMut<T> for T where
    T: ?Sized, [src]

impl<T> From<T> for T[src]

impl<T, U> Into<U> for T where
    U: From<T>, [src]

impl<T, U> TryFrom<U> for T where
    U: Into<T>, [src]

type Error = Infallible

The type returned in the event of a conversion error.

impl<T, U> TryInto<U> for T where
    U: TryFrom<T>, [src]

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

The type returned in the event of a conversion error.