Struct TryMap 

pub struct TryMap<Inner, M> {
    pub inner: Inner,
    pub mapper: M,
}

TryMap { inner, mapper } is the derived combinator Mapped { inner: Refined(inner, |v| mapper.wf_in(v)), mapper }.

Parsing fails when the parsed inner value does not satisfy mapper.wf_in. Serialization maps values back with mapper.spec_map_rev, and consistency requires both mapper.wf_out(v) and that the reverse-mapped inner value is consistent and satisfies mapper.wf_in.

Fields

inner: Inner

The inner combinator whose values are being transformed.

mapper: M

The mapping between the inner and outer value types.

Implementations

impl<Inner, M: SpecMapper> TryMap<Inner, M>

pub open spec fn inner(&self) -> TryMapInner<Inner, M>

{
    super::Mapped {
        inner: Refined(self.inner, |v: M::In| self.mapper.wf_in(v)),
        mapper: self.mapper,
    }
}

Trait Implementations

impl<Inner: Clone, M: Clone> Clone for TryMap<Inner, M>

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

ensures

call_ensures(Inner::clone, (&self.inner,), cloned.inner),

call_ensures(M::clone, (&self.mapper,), cloned.mapper),

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

Performs copy-assignment from source.

impl<Inner, M> Consistency for TryMap<Inner, M>

where Inner: Consistency, M: SpecMapper<In = Inner::Val>,

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

{ self.inner().consistent(v) }

type Val = <M as SpecMapper>::Out

The type of values whose consistency is being checked.

impl<Inner, M> EquivSerializers for TryMap<Inner, M>

where Inner: EquivSerializers, M: SpecMapper<In = Inner::SVal>,

open spec fn equiv_inv(&self) -> bool

{ self.inner().equiv_inv() }

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

impl<Inner, M> EquivSerializersGeneral for TryMap<Inner, M>

where Inner: EquivSerializersGeneral, M: SpecMapper<In = Inner::SVal>,

open spec fn equiv_general_inv(&self) -> bool

{ self.inner().equiv_general_inv() }

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

impl<Inner, M> GoodSerializer for TryMap<Inner, M>

where Inner: GoodSerializer, M: SpecMapper<In = Inner::SVal>,

open spec fn serialize_inv(&self) -> bool

{ self.inner().serialize_inv() }

proof fn lemma_serialize_len(&self, v: M::Out)

impl<Inner, M> MinMaxByteLen for TryMap<Inner, M>

where Inner: MinMaxByteLen, M: SpecMapper<In = Inner::T>,

open spec fn min(&self) -> nat

{ self.inner().min() }

open spec fn max(&self) -> nat

{ self.inner().max() }

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

impl<Inner, M> NoLookAhead for TryMap<Inner, M>

where Inner: NoLookAhead, M: LossyMapper<In = Inner::PVal>,

open spec fn no_lookahead_inv(&self) -> bool

{ self.inner().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<Inner, M> NonMalleable for TryMap<Inner, M>

where Inner: SoundParser + NonMalleable, M: LosslessMapper<In = Inner::PVal>,

open spec fn nonmal_inv(&self) -> bool

{ self.inner().nonmal_inv() }

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

impl<Inner, M> NonTailFmt for TryMap<Inner, M>

where Inner: NonTailFmt, M: SpecMapper<In = Inner::SValue>,

open spec fn serialize_dps_inv(&self) -> bool

{ self.inner().serialize_dps_inv() }

proof fn lemma_serialize_dps_prepend(&self, v: M::Out, obuf: Seq<u8>)

proof fn lemma_serialize_dps_len(&self, v: M::Out, obuf: Seq<u8>)

impl<Inner, M> Productive for TryMap<Inner, M>

where Inner: Productive, M: SpecMapper<In = Inner::PVal>,

open spec fn productive_inv(&self) -> bool

{ self.inner().productive_inv() }

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

impl<Inner, M> SPRoundTripDps for TryMap<Inner, M>

where Inner: SPRoundTripDps, M: LossyMapper<In = Inner::T>,

open spec fn unambiguous(&self) -> bool

{ self.inner().unambiguous() }

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

impl<Inner, M> SafeParser for TryMap<Inner, M>

where Inner: SafeParser, M: SpecMapper<In = Inner::PVal>,

open spec fn safe_inv(&self) -> bool

{ self.inner().safe_inv() }

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

impl<Inner, M> SoundParser for TryMap<Inner, M>

where Inner: SoundParser, M: LosslessMapper<In = Inner::PVal>,

open spec fn sound_inv(&self) -> bool

{ self.inner().sound_inv() }

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

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

impl<Inner, M> SpecByteLen for TryMap<Inner, M>

where Inner: SpecByteLen, M: SpecMapper<In = Inner::T>,

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

{ self.inner().byte_len(v) }

type T = <M as SpecMapper>::Out

The type of values whose byte length is being computed.

impl<Inner, M> SpecParser for TryMap<Inner, M>

where Inner: SpecParser, M: SpecMapper<In = Inner::PVal>,

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

{ self.inner().spec_parse(ibuf) }

type PVal = <M as SpecMapper>::Out

The type of parsed values.

impl<Inner, M> SpecSerializer for TryMap<Inner, M>

where Inner: SpecSerializer, M: SpecMapper<In = Inner::SVal>,

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

{ self.inner().spec_serialize(v) }

type SVal = <M as SpecMapper>::Out

The type of values to be serialized.

impl<Inner, M> SpecSerializerDps for TryMap<Inner, M>

where Inner: SpecSerializerDps, M: SpecMapper<In = Inner::SValue>,

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

{ self.inner().spec_serialize_dps(v, obuf) }

type SValue = <M as SpecMapper>::Out

The type of values to be serialized.

impl<Inner, M> StaticByteLen for TryMap<Inner, M>

where Inner: StaticByteLen, M: SpecMapper<In = Inner::T>,

open spec fn static_byte_len() -> nat

{ TryMapInner::<Inner, M>::static_byte_len() }

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

impl<Inner: Copy, M: Copy> Copy for TryMap<Inner, M>