Enum Sum 

pub enum Sum<A, B> {
    Inl(A),
    Inr(B),
}

The sum type.

Variants

Inl(A)

Left injection.

Inr(B)

Right injection.

Implementations

impl<A, B> Sum<A, B>

pub fn arrow_Inl_0(self) -> A

pub fn arrow_Inr_0(self) -> B

Trait Implementations

impl<A, B, TA, TB> ByteLen<Sum<TA, TB>> for Choice<A, B>

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

open spec fn exec_inv(&self) -> bool

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

}

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

impl<A, B, TA, TB> ByteLen<Sum<TA, TB>> for Sum<A, B>

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

open spec fn exec_inv(&self) -> bool

{
    match self {
        super::Sum::Inl(a) => a.exec_inv(),
        super::Sum::Inr(b) => b.exec_inv(),
    }
}

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

impl<A: Clone, B: Clone> Clone for Sum<A, B>

exec fn clone(&self) -> Self

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

Performs copy-assignment from source.

impl<A: Consistency, B: Consistency> Consistency for Sum<A, B>

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

{
    match (self, v) {
        (Sum::Inl(a), Sum::Inl(va)) => a.consistent(va),
        (Sum::Inr(b), Sum::Inr(vb)) => b.consistent(vb),
        _ => false,
    }
}

type Val = Sum<<A as Consistency>::Val, <B as Consistency>::Val>

The type of values whose consistency is being checked.

impl<A: Debug, B: Debug> Debug for Sum<A, B>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<A: DeepView, B: DeepView> DeepView for Sum<A, B>

open spec fn deep_view(&self) -> Self::V

{
    match self {
        super::Sum::Inl(a) => super::Sum::Inl(a.deep_view()),
        super::Sum::Inr(b) => super::Sum::Inr(b.deep_view()),
    }
}

type V = Sum<<A as DeepView>::V, <B as DeepView>::V>

impl<A, B, TA, TB> DerOrd<Sum<TA, TB>> for Choice<A, B>

where TA: DeepView, TB: DeepView, A: DerOrd<TA>, B: DerOrd<TB>,

proof fn lemma_der_serialize_len(&self, value: Sum<TA::V, TB::V>)

open spec fn der_remaining( &self, value: Sum<TA::V, TB::V>, state: ChoiceDerState<A::State, B::State>, ) -> Seq<u8>

{
    match (value, state) {
        (Sum::Inl(value), ChoiceDerState::Left(state)) => {
            self.0.der_remaining(value, state)
        }
        (Sum::Inr(value), ChoiceDerState::Right(state)) => {
            self.1.der_remaining(value, state)
        }
        _ => Seq::empty(),
    }
}

open spec fn der_state_valid( &self, value: Sum<TA::V, TB::V>, state: ChoiceDerState<A::State, B::State>, ) -> bool

{
    match (value, state) {
        (Sum::Inl(value), ChoiceDerState::Left(state)) => {
            self.0.der_state_valid(value, state)
        }
        (Sum::Inr(value), ChoiceDerState::Right(state)) => {
            self.1.der_state_valid(value, state)
        }
        _ => false,
    }
}

exec fn der_start(&self, v: &Sum<TA, TB>) -> state : ChoiceDerState<A::State, B::State>

exec fn der_next( &self, v: &Sum<TA, TB>, state: &mut ChoiceDerState<A::State, B::State>, ) -> next : Option<u8>

fn der_leq(&self, left: &T, right: &T) -> bool

impl<A, B> EquivSerializers for Sum<A, B>

where A: EquivSerializers, B: EquivSerializers,

open spec fn equiv_inv(&self) -> bool

{
    match self {
        Sum::Inl(a) => a.equiv_inv(),
        Sum::Inr(b) => b.equiv_inv(),
    }
}

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

impl<A, B> EquivSerializersGeneral for Sum<A, B>

where A: EquivSerializersGeneral, B: EquivSerializersGeneral,

open spec fn equiv_general_inv(&self) -> bool

{
    match self {
        Sum::Inl(a) => a.equiv_general_inv(),
        Sum::Inr(b) => b.equiv_general_inv(),
    }
}

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

impl<A: GoodSerializer, B: GoodSerializer> GoodSerializer for Sum<A, B>

open spec fn serialize_inv(&self) -> bool

{
    match self {
        Sum::Inl(a) => a.serialize_inv(),
        Sum::Inr(b) => b.serialize_inv(),
    }
}

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

impl<A: MinMaxByteLen, B: MinMaxByteLen> MinMaxByteLen for Sum<A, B>

open spec fn min(&self) -> nat

{
    match self {
        Sum::Inl(a) => a.min(),
        Sum::Inr(b) => b.min(),
    }
}

open spec fn max(&self) -> nat

{
    match self {
        Sum::Inl(a) => a.max(),
        Sum::Inr(b) => b.max(),
    }
}

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

impl<A: NoLookAhead, B: NoLookAhead> NoLookAhead for Sum<A, B>

open spec fn no_lookahead_inv(&self) -> bool

{
    match self {
        Sum::Inl(a) => a.no_lookahead_inv(),
        Sum::Inr(b) => b.no_lookahead_inv(),
    }
}

proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>)

fn corollary_non_extensible(&self, i1: Seq<u8>, i2: Seq<u8>)

impl<A: NonMalleable, B: NonMalleable> NonMalleable for Sum<A, B>

open spec fn nonmal_inv(&self) -> bool

{
    match self {
        Sum::Inl(a) => a.nonmal_inv(),
        Sum::Inr(b) => b.nonmal_inv(),
    }
}

proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>)

impl<A, B> NonTailFmt for Sum<A, B>

where A: NonTailFmt, B: NonTailFmt,

open spec fn serialize_dps_inv(&self) -> bool

{
    match self {
        Sum::Inl(a) => a.serialize_dps_inv(),
        Sum::Inr(b) => b.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> Parser<I> for Sum<A, B>

where I: View<V = Seq<u8>>, A: Parser<I>, B: Parser<I>,

open spec fn exec_inv(&self) -> bool

{
    match self {
        super::Sum::Inl(a) => a.exec_inv(),
        super::Sum::Inr(b) => b.exec_inv(),
    }
}

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

type PT = Sum<<A as Parser<I>>::PT, <B as Parser<I>>::PT>

Executable value returned by this parser.

impl<A: PartialEq, B: PartialEq> PartialEq for Sum<A, B>

fn eq(&self, other: &Sum<A, B>) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<A, B, TA, TB> Prepare<Sum<TA, TB>> for Choice<A, B>

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

open spec fn exec_inv(&self) -> bool

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

}

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

impl<A, B, TA, TB> Prepare<Sum<TA, TB>> for Sum<A, B>

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

open spec fn exec_inv(&self) -> bool

{
    match self {
        super::Sum::Inl(a) => a.exec_inv(),
        super::Sum::Inr(b) => b.exec_inv(),
    }
}

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

impl<A: Productive, B: Productive> Productive for Sum<A, B>

open spec fn productive_inv(&self) -> bool

{
    match self {
        Sum::Inl(a) => a.productive_inv(),
        Sum::Inr(b) => b.productive_inv(),
    }
}

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

impl<A: SPRoundTripDps, B: SPRoundTripDps> SPRoundTripDps for Sum<A, B>

open spec fn unambiguous(&self) -> bool

{
    match self {
        Sum::Inl(a) => a.unambiguous(),
        Sum::Inr(b) => b.unambiguous(),
    }
}

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

impl<A: SafeParser, B: SafeParser> SafeParser for Sum<A, B>

open spec fn safe_inv(&self) -> bool

{
    match self {
        Sum::Inl(a) => a.safe_inv(),
        Sum::Inr(b) => b.safe_inv(),
    }
}

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

impl<Output: OutputBuf, A, B, TA, TB> Serializer<Output, Sum<TA, TB>> for Choice<A, B>

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

open spec fn exec_inv(&self) -> bool

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

}

exec fn serialize_into(&self, v: &Sum<TA, TB>, obuf: &mut Output)

impl<Output: OutputBuf, A, B, TA, TB> Serializer<Output, Sum<TA, TB>> for Sum<A, B>

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

open spec fn exec_inv(&self) -> bool

{
    match self {
        super::Sum::Inl(a) => a.exec_inv(),
        super::Sum::Inr(b) => b.exec_inv(),
    }
}

exec fn serialize_into(&self, v: &Sum<TA, TB>, obuf: &mut Output)

impl<A: SoundParser, B: SoundParser> SoundParser for Sum<A, B>

open spec fn sound_inv(&self) -> bool

{
    match self {
        Sum::Inl(a) => a.sound_inv(),
        Sum::Inr(b) => b.sound_inv(),
    }
}

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

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

impl<A, B> SpecByteLen for Sum<A, B>

where A: SpecByteLen, B: SpecByteLen,

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

{
    match (self, v) {
        (Sum::Inl(a), Sum::Inl(va)) => a.byte_len(va),
        (Sum::Inr(b), Sum::Inr(vb)) => b.byte_len(vb),
        _ => 0,
    }
}

type T = Sum<<A as SpecByteLen>::T, <B as SpecByteLen>::T>

The type of values whose byte length is being computed.

impl<A: SpecParser, B: SpecParser> SpecParser for Sum<A, B>

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

{
    match self {
        Sum::Inl(a) => {
            match a.spec_parse(ibuf) {
                Some((n, va)) => Some((n, Sum::Inl(va))),
                None => None,
            }
        }
        Sum::Inr(b) => {
            match b.spec_parse(ibuf) {
                Some((n, vb)) => Some((n, Sum::Inr(vb))),
                None => None,
            }
        }
    }
}

type PVal = Sum<<A as SpecParser>::PVal, <B as SpecParser>::PVal>

The type of parsed values.

impl<A, B> SpecSerializer for Sum<A, B>

where A: SpecSerializer, B: SpecSerializer,

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

{
    match (self, v) {
        (Sum::Inl(a), Sum::Inl(va)) => a.spec_serialize(va),
        (Sum::Inr(b), Sum::Inr(vb)) => b.spec_serialize(vb),
        _ => Seq::empty(),
    }
}

type SVal = Sum<<A as SpecSerializer>::SVal, <B as SpecSerializer>::SVal>

The type of values to be serialized.

impl<A, B> SpecSerializerDps for Sum<A, B>

where A: SpecSerializerDps, B: SpecSerializerDps,

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

{
    match (self, v) {
        (Sum::Inl(a), Sum::Inl(va)) => a.spec_serialize_dps(va, obuf),
        (Sum::Inr(b), Sum::Inr(vb)) => b.spec_serialize_dps(vb, obuf),
        _ => obuf,
    }
}

type SValue = Sum<<A as SpecSerializerDps>::SValue, <B as SpecSerializerDps>::SValue>

The type of values to be serialized.

impl<A: ValueByteLen, B: ValueByteLen> ValueByteLen for Sum<A, B>

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

{
    match v {
        Sum::Inl(va) => A::value_byte_len(va),
        Sum::Inr(vb) => B::value_byte_len(vb),
    }
}

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

impl<A: View, B: View> View for Sum<A, B>

open spec fn view(&self) -> Self::V

{
    match self {
        super::Sum::Inl(a) => super::Sum::Inl(a@),
        super::Sum::Inr(b) => super::Sum::Inr(b@),
    }
}

type V = Sum<<A as View>::V, <B as View>::V>

impl<A: Copy, B: Copy> Copy for Sum<A, B>

impl<A: Eq, B: Eq> Eq for Sum<A, B>

impl<A, B> StructuralPartialEq for Sum<A, B>