Trait ParserRecBody 

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

    // Required method
    exec fn parse_body<Exec>(
        &self,
        param: &Self::EP,
        Ghost(spec_rec): Ghost<ParamRecSpecs<Self::Param, Self::T>>,
        exec_rec: Exec,
        ibuf: &I,
    ) -> r : 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

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

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

requires

forall |p: Self::Param| #[trigger] spec_rec(p).safe_inv(),

forall |p: Self::Param| #[trigger] spec_rec(p).productive_inv(),

forall |pp: &Self::EP, i: &I| call_requires(exec_rec, (pp, i)),

forall |pp: &Self::EP, i: &I, rr: PResult<Self::O>| {
    call_ensures(exec_rec, (pp, i), rr)
        ==> parse_matches_spec(rr, spec_rec(pp.deep_view()).2(i@))
},

ensures

parse_matches_spec(r, self.spec_body(param.deep_view(), spec_rec).spec_parse(ibuf@)),

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", so this trait is not object safe.

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>