Trait ParserRecBody 

pub trait ParserRecBody<I: InputBuf>: SpecRecBody {
    type EP: DeepView<V = Self::Param>;
    type O: DeepView<V = Self::T>;

    // Required method
    fn parse_body<Exec>(
        &self,
        param: &Self::EP,
        verus_tmp_spec_rec: Ghost<ParamRecSpecs<Self::Param, Self::T>>,
        exec_rec: Exec,
        ibuf: &I,
    ) -> PResult<Self::O>
       where Exec: Fn(&Self::EP, &I) -> PResult<Self::O>;
}

Executable parsing for one recursive unfolding.

Required Associated Types

type EP: DeepView<V = Self::Param>

type O: DeepView<V = Self::T>

Required Methods

fn parse_body<Exec>( &self, param: &Self::EP, verus_tmp_spec_rec: Ghost<ParamRecSpecs<Self::Param, Self::T>>, exec_rec: Exec, ibuf: &I, ) -> PResult<Self::O>

where Exec: Fn(&Self::EP, &I) -> PResult<Self::O>,

Execute one recursive unfolding, using exec_rec for all recursive positions in the body.

spec_rec is the ghost/spec callback bundle corresponding to exec_rec.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors

impl<'i> ParserRecBody<&'i [u8]> for BerAnyRecBody

Available on crate feature alloc only.

type EP = ()

type O = CapturedAnyOwned

impl<'i> ParserRecBody<&'i [u8]> for BerBitStringRecBody

Available on crate feature alloc only.

type EP = Tag

type O = BitStringOwned

impl<'i> ParserRecBody<&'i [u8]> for BerOctetStringRecBody

Available on crate feature alloc only.

type EP = Tag

type O = Vec<u8>

impl<'i> ParserRecBody<&'i [u8]> for CborRecBody<false>

where CborRecBody<false>: SpecRecBody<Param = (), T = CborValueSpec, Body = CborBodyFmt<false>>,

type EP = ()

type O = CborValue<'i>

impl<'i> ParserRecBody<&'i [u8]> for CborRecBody<true>

where CborRecBody<true>: SpecRecBody<Param = (), T = CborValueSpec, Body = CborBodyFmt<true>>,

type EP = ()

type O = CborValue<'i>