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.

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)>)>>