Trait mmb_parser::visitor::Visitor[−][src]

pub trait Visitor<'a> {
    type Binder: From<u64>;
    type Sort: From<u8>;
    type Statement: From<Statement>;
    type Unify: UnifyStream;
    type Proof: ProofStream;
    fn parse_sort(&mut self, sort: Self::Sort);

    fn parse_statement(
        &mut self, 
        statement: Self::Statement, 
        offset: usize, 
        slice: &'a [u8], 
        proof: Option<(usize, usize)>
    );

    fn try_reserve_binder_slice(
        &mut self, 
        nr: usize
    ) -> Option<(&mut [Self::Binder], usize)>;

    fn start_unify_stream(&mut self) -> &mut Self::Unify;

    fn start_proof_stream(&mut self) -> &mut Self::Proof;

    fn parse_term(
        &mut self, 
        sort_idx: u8, 
        binders: (usize, usize), 
        ret_ty: Self::Binder, 
        unify: &'a [u8], 
        unify_indices: (usize, usize)
    );

    fn parse_theorem(
        &mut self, 
        binders: (usize, usize), 
        unify: &'a [u8], 
        unify_indices: (usize, usize)
    );
}

Associated Types

type Binder: From<u64>[src]

type Sort: From<u8>[src]

type Statement: From<Statement>[src]

type Unify: UnifyStream[src]

type Proof: ProofStream[src]

Loading content...

Required methods

fn parse_sort(&mut self, sort: Self::Sort)[src]

fn parse_statement(
    &mut self,
    statement: Self::Statement,
    offset: usize,
    slice: &'a [u8],
    proof: Option<(usize, usize)>
)[src]

fn try_reserve_binder_slice(
    &mut self,
    nr: usize
) -> Option<(&mut [Self::Binder], usize)>[src]

fn start_unify_stream(&mut self) -> &mut Self::Unify[src]

fn start_proof_stream(&mut self) -> &mut Self::Proof[src]

fn parse_term(
    &mut self,
    sort_idx: u8,
    binders: (usize, usize),
    ret_ty: Self::Binder,
    unify: &'a [u8],
    unify_indices: (usize, usize)
)[src]

fn parse_theorem(
    &mut self,
    binders: (usize, usize),
    unify: &'a [u8],
    unify_indices: (usize, usize)
)[src]

Loading content...

Implementors

Loading content...