Skip to main content

Parser

vest_lib::core::exec::parser

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 methods
    open spec fn exec_inv(&self) -> bool { ... }
    fn min_byte_len(&self) -> usize { ... }
}

Expand description

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.

exec fn min_byte_len(&self) -> usize

A lower bound on the number of bytes one successful parse consumes.

This is a capacity hint for repetition formats.

Formats whose minimum is statically known should override it; the DSL compiler emits an override for every named format it generates.

Dyn Compatibility§

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

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 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 ObjectIdentifierFmt

Available on crate feature alloc only.

type PT = ObjectIdentifier

impl Parser<&[u8]> for TagFmt

type PT = Tag

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, 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, 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, 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, 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 DET: bool> Parser<&'i [u8]> for CborHeadFmt<DET>

type PT = CborHead

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> Parser<&'i [u8]> for BerEndFmt

type PT = ()

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

Available on crate feature alloc only.

type PT = BmpString

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

type PT = CborInitial

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 Integer8Fmt

type PT = i8

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

type PT = i16

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, 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, 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, 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, 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> 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> 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 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 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> 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 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, 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, 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, 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, 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, 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, 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, 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: InputBuf> Parser<I> for Eof

type PT = ()

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

type PT = I

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, I: InputBuf> Parser<I> for Fixed<N>

type PT = I

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

type PT = [u8; N]

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