Struct Permute3 

pub struct Permute3<A, B, C>(pub A, pub B, pub C);

Permute3<A, B, C> parses any permutation of A, B, C and produces (A::PVal, (B::PVal, C::PVal))

Permute3(A, B, C) ::= Alt(
    (A, Permute2(B, C)),
    Alt(
        Mapped((B, Permute2(A, C)), swap2),
        Mapped((C, Permute2(A, B)), swap3),
    )
)

Tuple Fields

0: A

1: B

2: C

Trait Implementations

impl<A, B, C, TA, TB, TC> ByteLen<(TA, (TB, TC))> for Permute3<A, B, C>

where TA: DeepView, TB: DeepView, TC: DeepView, A: ByteLen<TA>, B: ByteLen<TB>, C: ByteLen<TC>,

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& self.1.exec_inv()
    &&& self.2.exec_inv()

}

exec fn length(&self, v: &(TA, (TB, TC))) -> len : usize

impl<A: Clone, B: Clone, C: Clone> Clone for Permute3<A, B, C>

exec fn clone(&self) -> cloned : Self

ensures

call_ensures(A::clone, (&self.0,), cloned.0),

call_ensures(B::clone, (&self.1,), cloned.1),

call_ensures(C::clone, (&self.2,), cloned.2),

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<A, B, C> Consistency for Permute3<A, B, C>

where A: Consistency, B: Consistency, C: Consistency,

open spec fn consistent(&self, v: Self::Val) -> bool

{ Pair(self.0, Pair(self.1, self.2)).consistent(v) }

type Val = (<A as Consistency>::Val, (<B as Consistency>::Val, <C as Consistency>::Val))

The type of values whose consistency is being checked.

impl<A, B, C> EquivSerializers for Permute3<A, B, C>

where A: EquivSerializersGeneral, B: EquivSerializersGeneral, C: EquivSerializers,

open spec fn equiv_inv(&self) -> bool

{
    &&& self.0.equiv_general_inv()
    &&& self.1.equiv_general_inv()
    &&& self.2.equiv_inv()

}

proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal)

impl<A, B, C> EquivSerializersGeneral for Permute3<A, B, C>

where A: EquivSerializersGeneral, B: EquivSerializersGeneral, C: EquivSerializersGeneral,

open spec fn equiv_general_inv(&self) -> bool

{
    &&& self.0.equiv_general_inv()
    &&& self.1.equiv_general_inv()
    &&& self.2.equiv_general_inv()

}

proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>)

impl<A, B, C> GoodSerializer for Permute3<A, B, C>

where A: GoodSerializer, B: GoodSerializer, C: GoodSerializer,

open spec fn serialize_inv(&self) -> bool

{
    &&& self.0.serialize_inv()
    &&& self.1.serialize_inv()
    &&& self.2.serialize_inv()

}

proof fn lemma_serialize_len(&self, v: Self::SVal)

impl<A: MinMaxByteLen, B: MinMaxByteLen, C: MinMaxByteLen> MinMaxByteLen for Permute3<A, B, C>

open spec fn min(&self) -> nat

{ Pair(self.0, super::Permute2(self.1, self.2)).min() }

open spec fn max(&self) -> nat

{ Pair(self.0, super::Permute2(self.1, self.2)).max() }

proof fn lemma_min_max_byte_len(&self, v: Self::T)

impl<A, B, C> NonTailFmt for Permute3<A, B, C>

where A: NonTailFmt, B: NonTailFmt, C: NonTailFmt,

open spec fn serialize_dps_inv(&self) -> bool

{
    &&& self.0.serialize_dps_inv()
    &&& self.1.serialize_dps_inv()
    &&& self.2.serialize_dps_inv()

}

proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>)

proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>)

impl<I, A, B, C> Parser<I> for Permute3<A, B, C>

where I: InputBuf, A: Parser<I> + SafeParser, B: Parser<I> + SafeParser, C: Parser<I> + SafeParser,

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& self.0.safe_inv()
    &&& self.1.exec_inv()
    &&& self.1.safe_inv()
    &&& self.2.exec_inv()
    &&& self.2.safe_inv()

}

exec fn parse(&self, ibuf: &I) -> PResult<Self::PT>

type PT = (<A as Parser<I>>::PT, (<B as Parser<I>>::PT, <C as Parser<I>>::PT))

Executable value returned by this parser.

impl<A, B, C, TA, TB, TC> Prepare<(TA, (TB, TC))> for Permute3<A, B, C>

where TA: DeepView, TB: DeepView, TC: DeepView, A: Prepare<TA>, B: Prepare<TB>, C: Prepare<TC>,

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& self.1.exec_inv()
    &&& self.2.exec_inv()

}

exec fn prepare(&self, v: &(TA, (TB, TC))) -> checked : Result<usize, PreSerializeError>

impl<A: Productive, B: Productive, C: Productive> Productive for Permute3<A, B, C>

open spec fn productive_inv(&self) -> bool

{
    &&& self.0.productive_inv()
    &&& self.1.productive_inv()
    &&& self.2.productive_inv()

}

proof fn lemma_productive(&self, ibuf: Seq<u8>)

impl<A, B, C> SPRoundTripDps for Permute3<A, B, C>

where A: SPRoundTripDps + NonTailFmt, B: SPRoundTripDps + NonTailFmt, C: SPRoundTripDps,

open spec fn unambiguous(&self) -> bool

{
    &&& self.0.unambiguous()
    &&& self.1.unambiguous()
    &&& self.2.unambiguous()
    &&& self.0.serialize_dps_inv()
    &&& self.1.serialize_dps_inv()

}

proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>)

impl<A: SafeParser, B: SafeParser, C: SafeParser> SafeParser for Permute3<A, B, C>

open spec fn safe_inv(&self) -> bool

{
    &&& self.0.safe_inv()
    &&& self.1.safe_inv()
    &&& self.2.safe_inv()

}

proof fn lemma_parse_safe(&self, ibuf: Seq<u8>)

impl<Output: OutputBuf, A, B, C, TA, TB, TC> Serializer<Output, (TA, (TB, TC))> for Permute3<A, B, C>

where TA: DeepView, TB: DeepView, TC: DeepView, A: Serializer<Output, TA>, B: Serializer<Output, TB>, C: Serializer<Output, TC>,

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& self.1.exec_inv()
    &&& self.2.exec_inv()

}

exec fn serialize_into(&self, v: &(TA, (TB, TC)), obuf: &mut Output)

impl<A: SoundParser, B: SoundParser, C: SoundParser> SoundParser for Permute3<A, B, C>

open spec fn sound_inv(&self) -> bool

{
    &&& self.0.sound_inv()
    &&& self.1.sound_inv()
    &&& self.2.sound_inv()

}

proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>)

proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>)

impl<A: SpecByteLen, B: SpecByteLen, C: SpecByteLen> SpecByteLen for Permute3<A, B, C>

open spec fn byte_len(&self, v: Self::T) -> nat

{ Pair(self.0, super::Permute2(self.1, self.2)).byte_len(v) }

type T = (<A as SpecByteLen>::T, (<B as SpecByteLen>::T, <C as SpecByteLen>::T))

The type of values whose byte length is being computed.

impl<A, B, C> SpecParser for Permute3<A, B, C>

where A: SpecParser, B: SpecParser, C: SpecParser,

open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)>

{
    let inner = Alt::<
        _,
        _,
        false,
    >(
        Pair(self.0, super::Permute2(self.1, self.2)),
        Alt::<
            _,
            _,
            false,
        >(
            Mapped {
                inner: Pair(self.1, super::Permute2(self.0, self.2)),
                mapper: |i| super::swap3_1(i),
            },
            Mapped {
                inner: Pair(self.2, super::Permute2(self.0, self.1)),
                mapper: |i| super::swap3_2(i),
            },
        ),
    );
    inner.spec_parse(ibuf)
}

type PVal = (<A as SpecParser>::PVal, (<B as SpecParser>::PVal, <C as SpecParser>::PVal))

The type of parsed values.

impl<A, B, C> SpecSerializer for Permute3<A, B, C>

where A: SpecSerializer, B: SpecSerializer, C: SpecSerializer,

open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8>

{ Pair(self.0, super::Permute2(self.1, self.2)).spec_serialize(v) }

type SVal = (<A as SpecSerializer>::SVal, (<B as SpecSerializer>::SVal, <C as SpecSerializer>::SVal))

The type of values to be serialized.

impl<A, B, C> SpecSerializerDps for Permute3<A, B, C>

where A: SpecSerializerDps, B: SpecSerializerDps, C: SpecSerializerDps,

open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8>

{ Pair(self.0, super::Permute2(self.1, self.2)).spec_serialize_dps(v, obuf) }

type SValue = (<A as SpecSerializerDps>::SValue, (<B as SpecSerializerDps>::SValue, <C as SpecSerializerDps>::SValue))

The type of values to be serialized.

impl<A: StaticByteLen, B: StaticByteLen, C: StaticByteLen> StaticByteLen for Permute3<A, B, C>

open spec fn static_byte_len() -> nat

{ A::static_byte_len() + <super::Permute2<B, C> as StaticByteLen>::static_byte_len() }

proof fn lemma_static_len_matches_byte_len(&self, v: Self::T)

impl<A: ValueByteLen, B: ValueByteLen, C: ValueByteLen> ValueByteLen for Permute3<A, B, C>

open spec fn value_byte_len(v: Self::T) -> nat

{
    <crate::combinators::Pair<
        A,
        super::Permute2<B, C>,
    > as ValueByteLen>::value_byte_len(v)
}

proof fn lemma_value_len_matches_byte_len(&self, v: Self::T)

impl<A: Copy, B: Copy, C: Copy> Copy for Permute3<A, B, C>