Struct Permute2 

pub struct Permute2<P1, P2>(pub P1, pub P2);

Permute2<P1, P2> parses either (P1, P2) or (P2, P1) and produces (P1::PVal, P2::PVal)

Permute2 ::= Alt((P1, P2), Mapped((P2, P1), swap))

Tuple Fields

0: P1

1: P2

Trait Implementations

impl<P1, P2, T1, T2> ByteLen<(T1, T2)> for Permute2<P1, P2>

where T1: DeepView, T2: DeepView, P1: ByteLen<T1>, P2: ByteLen<T2>,

open spec fn exec_inv(&self) -> bool

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

}

exec fn length(&self, v: &(T1, T2)) -> len : usize

impl<P1: Clone, P2: Clone> Clone for Permute2<P1, P2>

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

ensures

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

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

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

Performs copy-assignment from source.

impl<P1, P2> Consistency for Permute2<P1, P2>

where P1: Consistency, P2: Consistency,

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

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

type Val = (<P1 as Consistency>::Val, <P2 as Consistency>::Val)

The type of values whose consistency is being checked.

impl<P1, P2> EquivSerializers for Permute2<P1, P2>

where P1: EquivSerializersGeneral, P2: EquivSerializers,

open spec fn equiv_inv(&self) -> bool

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

}

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

impl<P1, P2> EquivSerializersGeneral for Permute2<P1, P2>

where P1: EquivSerializersGeneral, P2: EquivSerializersGeneral,

open spec fn equiv_general_inv(&self) -> bool

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

}

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

impl<P1, P2> GoodSerializer for Permute2<P1, P2>

where P1: GoodSerializer, P2: GoodSerializer,

open spec fn serialize_inv(&self) -> bool

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

}

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

impl<P1: MinMaxByteLen, P2: MinMaxByteLen> MinMaxByteLen for Permute2<P1, P2>

open spec fn min(&self) -> nat

{ Pair(self.0, self.1).min() }

open spec fn max(&self) -> nat

{ Pair(self.0, self.1).max() }

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

impl<P1, P2> NonTailFmt for Permute2<P1, P2>

where P1: NonTailFmt, P2: NonTailFmt,

open spec fn serialize_dps_inv(&self) -> bool

{
    &&& self.0.serialize_dps_inv()
    &&& self.1.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, P1, P2> Parser<I> for Permute2<P1, P2>

where I: InputBuf, P1: Parser<I> + SafeParser, P2: 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()

}

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

type PT = (<P1 as Parser<I>>::PT, <P2 as Parser<I>>::PT)

Executable value returned by this parser.

impl<P1, P2, T1, T2> Prepare<(T1, T2)> for Permute2<P1, P2>

where T1: DeepView, T2: DeepView, P1: Prepare<T1>, P2: Prepare<T2>,

open spec fn exec_inv(&self) -> bool

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

}

exec fn prepare(&self, v: &(T1, T2)) -> checked : Result<usize, PreSerializeError>

impl<P1: Productive, P2: Productive> Productive for Permute2<P1, P2>

open spec fn productive_inv(&self) -> bool

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

}

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

impl<P1, P2> SPRoundTripDps for Permute2<P1, P2>

where P1: SPRoundTripDps + NonTailFmt, P2: SPRoundTripDps,

open spec fn unambiguous(&self) -> bool

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

}

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

impl<P1: SafeParser, P2: SafeParser> SafeParser for Permute2<P1, P2>

open spec fn safe_inv(&self) -> bool

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

}

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

impl<Output: OutputBuf, P1, P2, T1, T2> Serializer<Output, (T1, T2)> for Permute2<P1, P2>

where T1: DeepView, T2: DeepView, P1: Serializer<Output, T1>, P2: Serializer<Output, T2>,

open spec fn exec_inv(&self) -> bool

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

}

exec fn serialize_into(&self, v: &(T1, T2), obuf: &mut Output)

impl<P1: SoundParser, P2: SoundParser> SoundParser for Permute2<P1, P2>

open spec fn sound_inv(&self) -> bool

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

}

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

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

impl<P1: SpecByteLen, P2: SpecByteLen> SpecByteLen for Permute2<P1, P2>

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

{ Pair(self.0, self.1).byte_len(v) }

type T = (<P1 as SpecByteLen>::T, <P2 as SpecByteLen>::T)

The type of values whose byte length is being computed.

impl<P1, P2> SpecParser for Permute2<P1, P2>

where P1: SpecParser, P2: SpecParser,

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

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

type PVal = (<P1 as SpecParser>::PVal, <P2 as SpecParser>::PVal)

The type of parsed values.

impl<P1, P2> SpecSerializer for Permute2<P1, P2>

where P1: SpecSerializer, P2: SpecSerializer,

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

{ Pair(self.0, self.1).spec_serialize(v) }

type SVal = (<P1 as SpecSerializer>::SVal, <P2 as SpecSerializer>::SVal)

The type of values to be serialized.

impl<P1, P2> SpecSerializerDps for Permute2<P1, P2>

where P1: SpecSerializerDps, P2: SpecSerializerDps,

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

{ Pair(self.0, self.1).spec_serialize_dps(v, obuf) }

type SValue = (<P1 as SpecSerializerDps>::SValue, <P2 as SpecSerializerDps>::SValue)

The type of values to be serialized.

impl<P1: StaticByteLen, P2: StaticByteLen> StaticByteLen for Permute2<P1, P2>

open spec fn static_byte_len() -> nat

{ P1::static_byte_len() + P2::static_byte_len() }

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

impl<P1: ValueByteLen, P2: ValueByteLen> ValueByteLen for Permute2<P1, P2>

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

{ <crate::combinators::Pair<P1, P2> as ValueByteLen>::value_byte_len(v) }

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

impl<P1: Copy, P2: Copy> Copy for Permute2<P1, P2>