Struct FnParser 

pub struct FnParser<I: View<V = Seq<u8>>, O: DeepView, Spec: SpecParser<PVal = O::V>, Exec: Fn(&I) -> PResult<O>> {
    pub exec_fn: Exec,
    pub spec_fn: Ghost<Spec>,
    pub _marker: PhantomData<(I, O)>,
}

Pairs an executable parser closure with a ghost specification parser.

Fields

exec_fn: Exec

spec_fn: Ghost<Spec>

_marker: PhantomData<(I, O)>

Implementations

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

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

pub exec fn new(exec_fn: Exec, Ghost(spec_fn): Ghost<Spec>) -> parser : Self

requires

spec_fn.safe_inv(),

spec_fn.productive_inv(),

forall |i: &I| #[trigger] call_requires(exec_fn, (i,)),

forall |i: &I, r: PResult<O>| {
    #[trigger] call_ensures(exec_fn, (i,), r)
        ==> parse_matches_spec(r, spec_fn.spec_parse(i@))
},

ensures

parser.exec_inv(),

parser.safe_inv(),

parser.productive_inv(),

parser.spec_fn == spec_fn,

Constructs a safe, productive parser callback with a ghost specification.

Trait Implementations

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

open spec fn exec_inv(&self) -> bool

{
    &&& forall |i: &I| #[trigger] call_requires(self.exec_fn, (i,))
    &&& forall |i: &I, r: PResult<O>| {
        #[trigger] call_ensures(self.exec_fn, (i,), r)
            ==> {
                let Ghost(spec_fn) = self.spec_fn;
                parse_matches_spec(r, spec_fn.spec_parse(i@))
            }
    }

}

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

type PT = O

Executable value returned by this parser.

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

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

open spec fn productive_inv(&self) -> bool

{
    let Ghost(spec_fn) = self.spec_fn;
    spec_fn.productive_inv()
}

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

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

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

open spec fn safe_inv(&self) -> bool

{
    let Ghost(spec_fn) = self.spec_fn;
    spec_fn.safe_inv()
}

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

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

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

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

{
    let Ghost(spec_fn) = self.spec_fn;
    spec_fn.spec_parse(ibuf)
}

type PVal = <O as DeepView>::V

The type of parsed values.