Struct Repeat 

pub struct Repeat<A, B>(pub A, pub B);

Zero-or-more A followed by terminator B: sugar for Pair(Star<A>, B).

Unambiguity

Requires disjoint_domains(A, B).

Tuple Fields

0: A

1: B

Trait Implementations

impl<A, B, TA, TB> ByteLen<(&[TA], TB)> for Repeat<A, B>

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

open spec fn exec_inv(&self) -> bool

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

}

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

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

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

ensures

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

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

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

Performs copy-assignment from source.

impl<A, B> Consistency for Repeat<A, B>

where A: Consistency, B: Consistency,

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

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

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

The type of values whose consistency is being checked.

impl<A: EquivSerializersGeneral, B: EquivSerializers> EquivSerializers for Repeat<A, B>

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<A: EquivSerializersGeneral, B: EquivSerializersGeneral> EquivSerializersGeneral for Repeat<A, B>

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<A: GoodSerializer, B: GoodSerializer> GoodSerializer for Repeat<A, B>

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<A: NoLookAhead, B: NoLookAhead> NoLookAhead for Repeat<A, B>

open spec fn no_lookahead_inv(&self) -> bool

{
    &&& self.0.no_lookahead_inv()
    &&& self.1.no_lookahead_inv()
    &&& disjoint_domains(self.0, self.1)

}

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 Repeat<A, B>

open spec fn nonmal_inv(&self) -> bool

{ Pair(super::Star(self.0), self.1).nonmal_inv() }

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

impl<A: NonTailFmt, B: NonTailFmt> NonTailFmt for Repeat<A, B>

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, A, B> Parser<I> for Repeat<A, B>

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

Available on crate feature alloc only.

open spec fn exec_inv(&self) -> bool

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

}

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

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

Executable value returned by this parser.

impl<A, B, TA, TB> Prepare<(&[TA], TB)> for Repeat<A, B>

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

open spec fn exec_inv(&self) -> bool

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

}

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

impl<A: SafeParser, B: Productive> Productive for Repeat<A, B>

open spec fn productive_inv(&self) -> bool

{ self.1.productive_inv() }

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

impl<A: SPRoundTripDps + NonTailFmt, B: SPRoundTripDps> SPRoundTripDps for Repeat<A, B>

open spec fn unambiguous(&self) -> bool

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

}

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

impl<A, B> SafeParser for Repeat<A, B>

where A: SafeParser, B: SafeParser,

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, A, B, TA, TB> Serializer<Output, (&[TA], TB)> for Repeat<A, B>

where TA: DeepView, TB: DeepView, A: Serializer<Output, TA> + Copy, 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: &(&[TA], TB), obuf: &mut Output)

impl<A, B> SoundParser for Repeat<A, B>

where A: SoundParser, B: SoundParser,

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<A: SpecByteLen, B: SpecByteLen> SpecByteLen for Repeat<A, B>

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

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

type T = (Seq<<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 Repeat<A, B>

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

{ Pair(super::Star(self.0), self.1).spec_parse(ibuf) }

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

The type of parsed values.

impl<A: SpecSerializer, B: SpecSerializer> SpecSerializer for Repeat<A, B>

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

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

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

The type of values to be serialized.

impl<A: SpecSerializerDps, B: SpecSerializerDps> SpecSerializerDps for Repeat<A, B>

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

{ Pair(super::Star(self.0), self.1).spec_serialize_dps(vs, obuf) }

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

The type of values to be serialized.

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

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

{ <Pair<super::Star<A>, B> as ValueByteLen>::value_byte_len(v) }

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

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