Trait SpecRecBody 

pub trait SpecRecBody {
    type Param;
    type T;
    type Body: SpecCombinator<T = Self::T>;

    // Required method
    spec fn spec_body(
        &self,
        param: Self::Param,
        rec: ParamRecSpecs<Self::Param, Self::T>,
    ) -> Self::Body;
}

Defines one level of a recursive format for use with super::FixWith.

Required Associated Types

type Param

type T

type Body: SpecCombinator<T = Self::T>

Required Methods

spec fn spec_body( &self, param: Self::Param, rec: ParamRecSpecs<Self::Param, Self::T>, ) -> Self::Body

Define one recursive unfolding for param, where rec provides callbacks for all recursive positions in the body.

Dyn Compatibility

This trait is dyn compatible.

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

Implementors

impl SpecRecBody for BerAnyRecBody

type Param = ()

type T = Captured<AnySpec>

type Body = Capture<Mapped<Bind<TagFmt, FnSpec<(Tag,), Sum<Bind<BerLengthFmt, FnSpec<(BerLength,), Sum<ExactLen<Tail, usize>, Sum<Repeat<(FnSpec<(Captured<AnySpec>,), bool>, FnSpec<(Captured<AnySpec>,), nat>, FnSpec<(Seq<u8>,), Option<(int, Captured<AnySpec>)>>, FnSpec<(Captured<AnySpec>,), Seq<u8>>, FnSpec<(Captured<AnySpec>, Seq<u8>), Seq<u8>>), Pair<Const<TagFmt, Tag>, Const<U8, u8>>>, Void>>>>, Void>>>, (FnSpec<((Tag, Sum<(BerLength, Sum<Seq<u8>, Sum<(Seq<Captured<AnySpec>>, (Tag, u8)), ExecNever>>), ExecNever>),), AnySpec>, FnSpec<(AnySpec,), (Tag, Sum<(BerLength, Sum<Seq<u8>, Sum<(Seq<Captured<AnySpec>>, (Tag, u8)), ExecNever>>), ExecNever>)>)>>

impl SpecRecBody for BerBitStringRecBody

type Param = Tag

type T = BitStringSpec

type Body = Mapped<Refined<Bind<TagFmt, FnSpec<(Tag,), Sum<Bind<LengthFmt<BER>, FnSpec<(usize,), ExactLen<BitStringFmt<BER>, usize>>>, Sum<Bind<BerLengthFmt, FnSpec<(BerLength,), Sum<ExactLen<RepeatTillEnd<(FnSpec<(BitStringSpec,), bool>, FnSpec<(BitStringSpec,), nat>, FnSpec<(Seq<u8>,), Option<(int, BitStringSpec)>>, FnSpec<(BitStringSpec,), Seq<u8>>, FnSpec<(BitStringSpec, Seq<u8>), Seq<u8>>)>, usize>, Repeat<(FnSpec<(BitStringSpec,), bool>, FnSpec<(BitStringSpec,), nat>, FnSpec<(Seq<u8>,), Option<(int, BitStringSpec)>>, FnSpec<(BitStringSpec,), Seq<u8>>, FnSpec<(BitStringSpec, Seq<u8>), Seq<u8>>), Pair<Const<TagFmt, Tag>, Const<U8, u8>>>>>>, Void>>>>, FnSpec<((Tag, Sum<(usize, BitStringSpec), Sum<(BerLength, Sum<Seq<BitStringSpec>, (Seq<BitStringSpec>, (Tag, u8))>), ExecNever>>),), bool>>, (FnSpec<((Tag, Sum<(usize, BitStringSpec), Sum<(BerLength, Sum<Seq<BitStringSpec>, (Seq<BitStringSpec>, (Tag, u8))>), ExecNever>>),), BitStringSpec>, FnSpec<(BitStringSpec,), (Tag, Sum<(usize, BitStringSpec), Sum<(BerLength, Sum<Seq<BitStringSpec>, (Seq<BitStringSpec>, (Tag, u8))>), ExecNever>>)>)>

impl SpecRecBody for BerOctetStringRecBody

type Param = Tag

type T = Seq<u8>

type Body = Mapped<Bind<TagFmt, FnSpec<(Tag,), Sum<Bind<LengthFmt<BER>, FnSpec<(usize,), ExactLen<Tail, usize>>>, Sum<Bind<BerLengthFmt, FnSpec<(BerLength,), Sum<ExactLen<RepeatTillEnd<(FnSpec<(Seq<u8>,), bool>, FnSpec<(Seq<u8>,), nat>, FnSpec<(Seq<u8>,), Option<(int, Seq<u8>)>>, FnSpec<(Seq<u8>,), Seq<u8>>, FnSpec<(Seq<u8>, Seq<u8>), Seq<u8>>)>, usize>, Repeat<(FnSpec<(Seq<u8>,), bool>, FnSpec<(Seq<u8>,), nat>, FnSpec<(Seq<u8>,), Option<(int, Seq<u8>)>>, FnSpec<(Seq<u8>,), Seq<u8>>, FnSpec<(Seq<u8>, Seq<u8>), Seq<u8>>), Pair<Const<TagFmt, Tag>, Const<U8, u8>>>>>>, Void>>>>, (FnSpec<((Tag, Sum<(usize, Seq<u8>), Sum<(BerLength, Sum<Seq<Seq<u8>>, (Seq<Seq<u8>>, (Tag, u8))>), ExecNever>>),), Seq<u8>>, FnSpec<(Seq<u8>,), (Tag, Sum<(usize, Seq<u8>), Sum<(BerLength, Sum<Seq<Seq<u8>>, (Seq<Seq<u8>>, (Tag, u8))>), ExecNever>>)>)>

impl<const DET: bool> SpecRecBody for CborRecBody<DET>

type Param = ()

type T = CborValueSpec

type Body = CborBodyFmt<DET>

impl<const MINIMAL: bool> SpecRecBody for ULeb128RecBody<MINIMAL>

type Param = ()

type T = nat

type Body = Alt<Mapped<Refined<U8, FnSpec<(u8,), bool>>, TermByteFromToNat>, Mapped<Pair<Mapped<Refined<U8, FnSpec<(u8,), bool>>, LowBitsMask>, Refined<(FnSpec<(nat,), bool>, FnSpec<(nat,), nat>, FnSpec<(Seq<u8>,), Option<(int, nat)>>, FnSpec<(nat,), Seq<u8>>, FnSpec<(nat, Seq<u8>), Seq<u8>>), FnSpec<(nat,), bool>>>, (FnSpec<((u8, nat),), nat>, FnSpec<(nat,), (u8, nat)>)>>