pub struct AndThen<Prev, Next>(pub Prev, pub Next);Expand description
Combinator that monadically chains two combinators.
Tuple Fields§
§0: Prev§1: NextTrait Implementations§
Source§impl<'x, I, O, Next: Combinator<'x, I, O>> Combinator<'x, I, O> for AndThen<Variable, Next>where
I: VestInput,
O: VestOutput<I>,
Next::V: SecureSpecCombinator<Type = <Next::Type as View>::V>,
impl<'x, I, O, Next: Combinator<'x, I, O>> Combinator<'x, I, O> for AndThen<Variable, Next>where
I: VestInput,
O: VestOutput<I>,
Next::V: SecureSpecCombinator<Type = <Next::Type as View>::V>,
Source§open spec fn ex_requires(&self) -> bool
open spec fn ex_requires(&self) -> bool
{ self.1.ex_requires() }Source§exec fn serialize(
&self,
v: Self::SType,
data: &mut O,
pos: usize,
) -> Result<usize, SerializeError>
exec fn serialize( &self, v: Self::SType, data: &mut O, pos: usize, ) -> Result<usize, SerializeError>
Source§type Type = <Next as Combinator<'x, I, O>>::Type
type Type = <Next as Combinator<'x, I, O>>::Type
The result type of parsing
Source§type SType = <Next as Combinator<'x, I, O>>::SType
type SType = <Next as Combinator<'x, I, O>>::SType
The input type of serialization, often a reference to
Self::Type.
For “structural” formats though (e.g., crate::regular::sequence::Pair and crate::regular::variant::Choice),
this is the tuple/sum of the corresponding Combinator::SType types.Source§impl<Next: SecureSpecCombinator> SecureSpecCombinator for AndThen<Variable, Next>
impl<Next: SecureSpecCombinator> SecureSpecCombinator for AndThen<Variable, Next>
Source§proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type)
proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type)
Source§proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>)
proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>)
Source§open spec fn is_prefix_secure() -> bool
open spec fn is_prefix_secure() -> bool
{ Variable::is_prefix_secure() }Source§proof fn lemma_prefix_secure(&self, buf: Seq<u8>, s2: Seq<u8>)
proof fn lemma_prefix_secure(&self, buf: Seq<u8>, s2: Seq<u8>)
Source§proof fn lemma_parse_length(&self, s: Seq<u8>)
proof fn lemma_parse_length(&self, s: Seq<u8>)
Source§open spec fn is_productive(&self) -> bool
open spec fn is_productive(&self) -> bool
{ self.0.is_productive() }Source§proof fn lemma_parse_productive(&self, s: Seq<u8>)
proof fn lemma_parse_productive(&self, s: Seq<u8>)
Source§fn corollary_parse_surjective(&self, v: Self::Type)
fn corollary_parse_surjective(&self, v: Self::Type)
Source§fn corollary_serialize_injective_contraposition(
&self,
v1: Self::Type,
v2: Self::Type,
)
fn corollary_serialize_injective_contraposition( &self, v1: Self::Type, v2: Self::Type, )
Source§fn lemma_serialize_productive(&self, v: Self::Type)
fn lemma_serialize_productive(&self, v: Self::Type)
Source§impl<Next: SpecCombinator> SpecCombinator for AndThen<Variable, Next>
impl<Next: SpecCombinator> SpecCombinator for AndThen<Variable, Next>
Source§open spec fn wf(&self, v: Self::Type) -> bool
open spec fn wf(&self, v: Self::Type) -> bool
{ self.1.wf(v) && self.0.wf(self.1.spec_serialize(v)) }Source§open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)>
open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)>
{
if let Some((n, v1)) = self.0.spec_parse(s) {
if let Some((m, v2)) = self.1.spec_parse(v1) {
if m == n { Some((n, v2)) } else { None }
} else {
None
}
} else {
None
}
}Source§open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8>
open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8>
{
let buf1 = self.1.spec_serialize(v);
self.0.spec_serialize(buf1)
}Source§type Type = <Next as SpecCombinator>::Type
type Type = <Next as SpecCombinator>::Type
The view of [
Combinator::Result].Auto Trait Implementations§
impl<Prev, Next> Freeze for AndThen<Prev, Next>
impl<Prev, Next> RefUnwindSafe for AndThen<Prev, Next>where
Prev: RefUnwindSafe,
Next: RefUnwindSafe,
impl<Prev, Next> Send for AndThen<Prev, Next>
impl<Prev, Next> Sync for AndThen<Prev, Next>
impl<Prev, Next> Unpin for AndThen<Prev, Next>
impl<Prev, Next> UnwindSafe for AndThen<Prev, Next>where
Prev: UnwindSafe,
Next: UnwindSafe,
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
§impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__Awhere
VERUS_SPEC__A: From<T>,
impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__Awhere
VERUS_SPEC__A: From<T>,
fn obeys_from_spec() -> bool
fn from_spec(v: T) -> VERUS_SPEC__A
§impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__Awhere
VERUS_SPEC__A: Into<T>,
impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__Awhere
VERUS_SPEC__A: Into<T>,
fn obeys_into_spec() -> bool
fn into_spec(self) -> T
§impl<T, U> IntoSpecImpl<U> for Twhere
U: From<T>,
impl<T, U> IntoSpecImpl<U> for Twhere
U: From<T>,
fn obeys_into_spec() -> bool
fn into_spec(self) -> U
Source§impl<T, U> SpecTryInto<U> for Twhere
U: SpecTryFrom<T>,
impl<T, U> SpecTryInto<U> for Twhere
U: SpecTryFrom<T>,
Source§open spec fn spec_try_into(self) -> Result<U, <U as SpecTryFrom<T>>::Error>
open spec fn spec_try_into(self) -> Result<U, <U as SpecTryFrom<T>>::Error>
{ U::spec_try_from(self) }Source§type Error = <U as SpecTryFrom<T>>::Error
type Error = <U as SpecTryFrom<T>>::Error
The type returned in the event of a conversion error.