Trait Parser 

pub trait Parser<Input: View<V = Seq<u8>>>: SpecParser {
    type PT: DeepView<V = Self::PVal>;

    // Required method
    exec fn parse(&self, ibuf: &Input) -> r : PResult<Self::PT>;

    // Provided method
    open spec fn exec_inv(&self) -> bool { ... }
}

An executable parser proved equivalent to a pure SpecParser.

Input is normally &[u8]. Successful parsing returns both the consumed byte count and a value whose deep view is exactly the value returned by SpecParser::spec_parse.

Required Associated Types

type PT: DeepView<V = Self::PVal>

Executable value returned by this parser.

Required Methods

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

requires

self.exec_inv(),

ensures

parse_matches_spec(r, self.spec_parse(ibuf@)),

Parses a prefix of ibuf.

Provided Methods

open spec fn exec_inv(&self) -> bool

{ true }

Extra invariant required by this parser’s executable implementation.

Most formats leave this as true; functional and recursive parser callbacks use it to connect executable code to their specifications.

Implementations on Foreign Types

impl<I, P> Parser<I> for &P

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

open spec fn exec_inv(&self) -> bool

{ (*self).exec_inv() }

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

type PT = <P as Parser<I>>::PT

impl<I, T, Spec, Exec> Parser<I> for (Spec, Exec)

where I: View<V = Seq<u8>>, T: DeepView<V = Spec::PVal>, Spec: SpecParser, Exec: Fn(&I) -> PResult<T>,

open spec fn exec_inv(&self) -> bool

{
    &&& forall |i: &I| call_requires(self.1, (i,))
    &&& forall |i: &I, r: PResult<T>| {
        call_ensures(self.1, (i,), r) ==> parse_matches_spec(r, self.spec_parse(i@))
    }

}

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

type PT = T

Implementors

impl Parser<&[u8]> for BerLengthFmt

type PT = BerLength

impl Parser<&[u8]> for ObjectIdentifierFmt

Available on crate feature alloc only.

type PT = ObjectIdentifier

impl Parser<&[u8]> for TagFmt

type PT = Tag

impl Parser<&[u8]> for I8

type PT = i8

impl Parser<&[u8]> for I16Be

type PT = i16

impl Parser<&[u8]> for I16Le

type PT = i16

impl Parser<&[u8]> for I32Be

type PT = i32

impl Parser<&[u8]> for I32Le

type PT = i32

impl Parser<&[u8]> for I64Be

type PT = i64

impl Parser<&[u8]> for I64Le

type PT = i64

impl Parser<&[u8]> for U8

type PT = u8

impl Parser<&[u8]> for U16Be

type PT = u16

impl Parser<&[u8]> for U16Le

type PT = u16

impl Parser<&[u8]> for U24Be

type PT = u32

impl Parser<&[u8]> for U24Le

type PT = u32

impl Parser<&[u8]> for U32Be

type PT = u32

impl Parser<&[u8]> for U32Le

type PT = u32

impl Parser<&[u8]> for U64Be

type PT = u64

impl Parser<&[u8]> for U64Le

type PT = u64

impl<'a, const DER: bool> Parser<&'a [u8]> for AnyFmt<DER>

type PT = Any<'a>

impl<'a, const DER: bool> Parser<&'a [u8]> for RealFmt<DER>

type PT = Real<'a, DER>

impl<'i> Parser<&'i [u8]> for BerEndFmt

type PT = ()

impl<'i> Parser<&'i [u8]> for Integer8Fmt

type PT = i8

impl<'i> Parser<&'i [u8]> for Integer16Fmt

type PT = i16

impl<'i> Parser<&'i [u8]> for BmpStringFmt

Available on crate feature alloc only.

type PT = BmpString

impl<'i> Parser<&'i [u8]> for EnumeratedFmt

type PT = Integer<'i>

impl<'i> Parser<&'i [u8]> for Ia5StringFmt

type PT = Ia5String<'i>

impl<'i> Parser<&'i [u8]> for IntegerFmt

type PT = Integer<'i>

impl<'i> Parser<&'i [u8]> for PrintableStringFmt

type PT = PrintableString<'i>

impl<'i> Parser<&'i [u8]> for TeletexStringFmt

type PT = TeletexString<'i>

impl<'i> Parser<&'i [u8]> for UniversalStringFmt

Available on crate feature alloc only.

type PT = String

impl<'i> Parser<&'i [u8]> for Utf8StringFmt

type PT = &'i str

impl<'i> Parser<&'i [u8]> for CborInitialFmt

type PT = CborInitial

impl<'i, C> Parser<&'i [u8]> for BerSequenceFmt<C>

where C: SpecCombinator + Parser<&'i [u8]> + SafeParser + Copy,

type PT = <C as Parser<&'i [u8]>>::PT

impl<'i, C> Parser<&'i [u8]> for BerSequenceOfFmt<C>

where C: SpecCombinator + Parser<&'i [u8]> + Productive + Copy,

Available on crate feature alloc only.

type PT = Vec<<C as Parser<&'i [u8]>>::PT>

impl<'i, C> Parser<&'i [u8]> for SetOfFmt<C>

where C: Parser<&'i [u8]> + SafeParser + Productive + Copy,

Available on crate feature alloc only.

type PT = Vec<<C as Parser<&'i [u8]>>::PT>

impl<'i, C, const LIMIT: usize> Parser<&'i [u8]> for BerCharStringFmt<C, LIMIT>

where C: BerDecoderOwned,

Available on crate feature alloc only.

type PT = <C as BerDecoderOwned>::Owned

impl<'i, Content, const DER: bool> Parser<&'i [u8]> for ASN1Fmt<Content, DER>

where Content: SpecCombinator + Parser<&'i [u8]>,

type PT = <Content as Parser<&'i [u8]>>::PT

impl<'i, const DER: bool> Parser<&'i [u8]> for BitStringFmt<DER>

type PT = BitString<'i, DER>

impl<'i, const DER: bool> Parser<&'i [u8]> for GeneralizedTimeFmt<DER>

type PT = GeneralizedTime<'i>

impl<'i, const DER: bool> Parser<&'i [u8]> for UtcTimeFmt<DER>

type PT = UtcTime

impl<'i, const DET: bool> Parser<&'i [u8]> for CborHeadFmt<DET>

type PT = CborHead

impl<'i, const DET: bool, const LIMIT: usize> Parser<&'i [u8]> for CborFmt<DET, LIMIT>

where CborRecBody<DET>: SpecRecBody<Param = (), T = CborValueSpec, Body = CborBodyFmt<DET>> + ParserRecBody<&'i [u8], EP = (), O = CborValue<'i>>, <CborRecBody<DET> as SpecRecBody>::Body: Productive,

type PT = CborValue<'i>

impl<'i, const LIMIT: usize> Parser<&'i [u8]> for BerAnyFmt<LIMIT>

Available on crate feature alloc only.

type PT = AnyOwned

impl<'i, const LIMIT: usize> Parser<&'i [u8]> for BerBitStringFmt<LIMIT>

Available on crate feature alloc only.

type PT = BitStringOwned

impl<'i, const LIMIT: usize> Parser<&'i [u8]> for BerOctetStringFmt<LIMIT>

Available on crate feature alloc only.

type PT = Vec<u8>

impl<'i, const MINIMAL: bool> Parser<&'i [u8]> for VarInt<MINIMAL>

type PT = u64

impl<I, A> Parser<I> for Opt<A>

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

type PT = Option<<A as Parser<I>>::PT>

impl<I, A> Parser<I> for OptionalEnd<A>

where I: InputBuf, A: Parser<I> + SafeParser,

type PT = Option<<A as Parser<I>>::PT>

impl<I, A> Parser<I> for RepeatTillEnd<A>

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

Available on crate feature alloc only.

type PT = Vec<<A as Parser<I>>::PT>

impl<I, A, AVal, B> Parser<I> for Preceded<A, AVal, B, false>

where I: InputBuf, A: Parser<I, PT = AVal> + SafeParser<PVal = AVal>, B: Parser<I> + SafeParser, AVal: DeepView<V = AVal>,

type PT = <B as Parser<I>>::PT

impl<I, A, AVal, B> Parser<I> for Preceded<A, AVal, B, true>

where I: InputBuf, A: Parser<I, PT = AVal> + SafeParser<PVal = AVal>, B: Parser<I> + SafeParser, AVal: DeepView<V = AVal> + PartialEq + Structural,

type PT = <B as Parser<I>>::PT

impl<I, A, B> Parser<I> for Sum<A, B>

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

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

impl<I, A, B> Parser<I> for Choice<A, B>

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

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

impl<I, A, B> Parser<I> for Optional<A, B>

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

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

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.

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

impl<I, A, B> Parser<I> for Bind<A, B>

where I: InputBuf, A: Parser<I> + SafeParser, B::O: Parser<I> + SafeParser, B: MapRef<A::PT, Input = A::PVal>,

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

impl<I, A, B> Parser<I> for Pair<A, B>

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

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

impl<I, A, B, BVal> Parser<I> for Terminated<A, B, BVal, false>

where I: InputBuf, A: Parser<I> + SafeParser, B: Parser<I, PT = BVal> + SafeParser<PVal = BVal>, BVal: DeepView<V = BVal>,

type PT = <A as Parser<I>>::PT

impl<I, A, B, BVal> Parser<I> for Terminated<A, B, BVal, true>

where I: InputBuf, A: Parser<I> + SafeParser, B: Parser<I, PT = BVal> + SafeParser<PVal = BVal>, BVal: DeepView<V = BVal> + PartialEq + Structural,

type PT = <A as Parser<I>>::PT

impl<I, A, B, C> Parser<I> for Permute3<A, B, C>

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

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

impl<I, A, B, C, D> Parser<I> for Permute4<A, B, C, D>

where I: InputBuf, A: Parser<I> + SafeParser, B: Parser<I> + SafeParser, C: Parser<I> + SafeParser, D: Parser<I> + SafeParser,

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

impl<I, A, B, C, D, E> Parser<I> for Permute5<A, B, C, D, E>

where I: InputBuf, A: Parser<I> + SafeParser, B: Parser<I> + SafeParser, C: Parser<I> + SafeParser, D: Parser<I> + SafeParser, E: Parser<I> + SafeParser,

type PT = (<A as Parser<I>>::PT, (<B as Parser<I>>::PT, (<C as Parser<I>>::PT, (<D as Parser<I>>::PT, <E as Parser<I>>::PT))))

impl<I, A, PredFn> Parser<I> for Refined<A, PredFn>

where I: View<V = Seq<u8>>, A: Parser<I>, PredFn: Pred<A::PT>,

type PT = <A as Parser<I>>::PT

impl<I, Field, Rest, const DER: bool> Parser<I> for DefaultedFmt<Field, Field::T, Rest, DER>

where I: InputBuf, Field: Parser<I, PT = Field::T> + SafeParser<PVal = Field::T> + SpecByteLen, Rest: Parser<I> + SafeParser<PVal = Rest::T> + SpecByteLen, Field::T: DeepView<V = Field::T> + PartialEq + Structural + Copy,

type PT = (<Field as Parser<I>>::PT, <Rest as Parser<I>>::PT)

impl<I, Inner> Parser<I> for Cond<Inner>

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

type PT = <Inner as Parser<I>>::PT

impl<I, Inner> Parser<I> for Named<Inner>

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

type PT = <Inner as Parser<I>>::PT

impl<I, Inner> Parser<I> for Ref<Inner>

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

type PT = <Inner as Parser<I>>::PT

impl<I, Inner> Parser<I> for Star<Inner>

where I: InputBuf, Inner: Parser<I> + Productive,

Available on crate feature alloc only.

type PT = Vec<<Inner as Parser<I>>::PT>

impl<I, Inner, M, MRev> Parser<I> for Mapped<Inner, BiMap<M, MRev>>

where I: View<V = Seq<u8>>, Inner: Parser<I>, M: Map<Inner::PT, Input = Inner::PVal>, MRev: SpecMap<Input = M::Output, Output = M::Input>,

type PT = <M as Map<<Inner as Parser<I>>::PT>>::O

impl<I, Inner, N> Parser<I> for RepeatN<Inner, N>

where I: InputBuf, Inner: Parser<I> + SafeParser, N: AsLen,

Available on crate feature alloc only.

type PT = Vec<<Inner as Parser<I>>::PT>

impl<I, Inner, T> Parser<I> for Const<Inner, T>

where I: InputBuf, Inner: Parser<I, PT = T, PVal = T>, T: DeepView<V = T> + PartialEq + Structural,

type PT = <Inner as SpecParser>::PVal

impl<I, Inner, const N: usize> Parser<I> for Array<N, Inner>

where I: InputBuf, Inner: Parser<I> + SafeParser,

type PT = [<Inner as Parser<I>>::PT; N]

impl<I, Len, Inner> Parser<I> for ExactLen<Inner, Len>

where I: InputBuf, Len: AsLen, Inner: Parser<I>,

type PT = <Inner as Parser<I>>::PT

impl<I, O, Spec, Exec> Parser<I> for FnParser<I, O, Spec, Exec>

where I: View<V = Seq<u8>>, O: DeepView, Spec: SpecParser<PVal = O::V>, Exec: Fn(&I) -> PResult<O>,

type PT = O

impl<I, Of, Tg, TagVal> Parser<I> for SuffixTagged<Of, Tg, TagVal>

where I: InputBuf, Tg: SpecByteLen<T = TagVal> + Parser<I, PT = TagVal, PVal = TagVal> + SafeParser, TagVal: DeepView<V = TagVal> + PartialEq + Structural + Copy, Of: Parser<I> + SafeParser,

type PT = <Of as Parser<I>>::PT

impl<I, P1, P2> Parser<I> for Permute2<P1, P2>

where I: InputBuf, P1: Parser<I> + SafeParser, P2: Parser<I> + SafeParser,

type PT = (<P1 as Parser<I>>::PT, <P2 as Parser<I>>::PT)

impl<I, Tg, TagVal, Of> Parser<I> for PrefixTagged<Tg, TagVal, Of>

where I: InputBuf, Tg: SpecByteLen<T = TagVal> + Parser<I, PT = TagVal, PVal = TagVal> + SafeParser, TagVal: DeepView<V = TagVal> + PartialEq + Structural + Copy, Of: Parser<I> + SafeParser,

type PT = <Of as Parser<I>>::PT

impl<I: InputBuf> Parser<I> for Eof

type PT = ()

impl<I: InputBuf> Parser<I> for Tail

type PT = I

impl<I: InputBuf, A, Then> Parser<I> for AndThen<A, Then>

where A: Parser<I, PT = I, PVal = Seq<u8>>, Then: Parser<I>,

type PT = <Then as Parser<I>>::PT

impl<I: View<V = Seq<u8>>> Parser<I> for Empty

type PT = ()

impl<I: View<V = Seq<u8>>> Parser<I> for Void

type PT = ExecNever

impl<Input, F> Parser<Input> for ImplicitlyTaggedFmt<F>

where Input: InputBuf, F: Retaggable + Parser<Input>,

type PT = <F as Parser<Input>>::PT

impl<Len: AsLen, I: InputBuf> Parser<I> for Varied<Len>

type PT = I

impl<const DER: bool> Parser<&[u8]> for BoolFmt<DER>

type PT = bool

impl<const DER: bool> Parser<&[u8]> for LengthFmt<DER>

type PT = usize

impl<const LIMIT: usize, Body, Param, I> Parser<I> for FixWith<LIMIT, Body, Param>

where I: InputBuf, Param: DeepView<V = Body::Param>, Body: ParserRecBody<I, EP = Param> + ProductiveRecBody, Body::Body: Productive,

type PT = <Body as ParserRecBody<I>>::O

impl<const MINIMAL: bool> Parser<&[u8]> for Base128Fmt<MINIMAL>

type PT = u64

impl<const N: usize> Parser<&[u8]> for Const<Fixed<N>, [u8; N]>

type PT = [u8; N]

impl<const N: usize, I: InputBuf> Parser<I> for Fixed<N>

type PT = I

impl<const NONDETERMINISTIC: bool, I, A, B> Parser<I> for Alt<A, B, NONDETERMINISTIC>

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

type PT = <A as Parser<I>>::PT