pub trait Productive: SafeParser {
// Required method
broadcast proof fn lemma_productive(&self, s: Seq<u8>);
// Provided method
open spec fn productive_inv(&self) -> bool { ... }
}Expand description
Productivity for parsers.
A productive parser always consumes at least one byte when it succeeds.
Inherently unproductive combinators are:
Empty: Always succeeds and never consumes any bytes.Eof: Asserts the end of the input. It only succeeds if the buffer is entirely empty, thus always consuming 0 bytes.Tail: Consumes all remaining bytes in the buffer. If the buffer is already empty, it successfully consumes 0 bytes.Opt<A>: Evaluates an optional field. IfAfails,Opt<A>successfully returnsNonewhile consuming 0 bytes.Star<A>: The Kleene star for zero-or-more repetitions. It can successfully parse zero occurrences ofA, consuming 0 bytes.OptionalEnd<C>&RepeatTillEnd<C>: These are syntax sugar forOptional<C, Eof>andRepeat<C, Eof>.
The above combinators still implement the Productive trait in order for sequencing combinators
like Pair to remain productive, but their productive_inv would return false (so lemma_productive would not apply to them).
Required Methods§
Sourcebroadcast proof fn lemma_productive(&self, s: Seq<u8>)
broadcast proof fn lemma_productive(&self, s: Seq<u8>)
requires
self.safe_inv(),self.productive_inv(),#[trigger] self.spec_parse(s) matches Some((n, _)) ==> n > 0,Provided Methods§
Sourceopen spec fn productive_inv(&self) -> bool
open spec fn productive_inv(&self) -> bool
{ true }Implementations on Foreign Types§
Source§impl<P: Productive> Productive for &P
impl<P: Productive> Productive for &P
Source§open spec fn productive_inv(&self) -> bool
open spec fn productive_inv(&self) -> bool
{ (*self).productive_inv() }Source§proof fn lemma_productive(&self, s: Seq<u8>)
proof fn lemma_productive(&self, s: Seq<u8>)
Source§impl<Spec, Exec> Productive for (Spec, Exec)where
Spec: Productive,
impl<Spec, Exec> Productive for (Spec, Exec)where
Spec: Productive,
Source§open spec fn productive_inv(&self) -> bool
open spec fn productive_inv(&self) -> bool
{ self.0.productive_inv() }Source§proof fn lemma_productive(&self, input: Seq<u8>)
proof fn lemma_productive(&self, input: Seq<u8>)
Source§impl<SpecP, Cnstcy, Blen> Productive for (SpecP, Cnstcy, Blen)
impl<SpecP, Cnstcy, Blen> Productive for (SpecP, Cnstcy, Blen)
Source§open spec fn productive_inv(&self) -> bool
open spec fn productive_inv(&self) -> bool
{
let (p, _, _) = *self;
let p_fn = |ibuf| p.spec_parse(ibuf);
productive_parser(p_fn)
}