val tot_parse_fret (#t #t': Type) (f: (t -> Tot t')) (v: t) : Tot (tot_parser parse_ret_kind t')
let tot_parse_fret (#t #t':Type) (f: t -> Tot t') (v:t) : Tot (tot_parser parse_ret_kind t') =
  [@inline_let] let _ = parser_kind_prop_equiv parse_ret_kind (tot_parse_fret' f v) in
  tot_parse_fret' f v
val tot_parse_fret (#t #t': Type) (f: (t -> Tot t')) (v: t) : Tot (tot_parser parse_ret_kind t')
let tot_parse_fret (#t #t': Type) (f: (t -> Tot t')) (v: t) : Tot (tot_parser parse_ret_kind t') =
[@@ inline_let ]let _ = parser_kind_prop_equiv parse_ret_kind (tot_parse_fret' f v) in
tot_parse_fret' f v
LowParse.Spec.Combinators.fst.checked
prims.fst.checked LowParse.Spec.Base.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Tactics.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.Spec.Combinators.fst
LowParse.Spec.Combinators.tot_parse_fret' Prims.unit LowParse.Spec.Base.parser_kind_prop_equiv LowParse.Spec.Combinators.parse_ret_kind LowParse.Spec.Base.tot_parser
module LowParse.Spec.Combinators
include LowParse.Spec.Base

module Seq = FStar.Seq
module U8 = FStar.UInt8
module U32 = FStar.UInt32

module T = FStar.Tactics

#reset-options "--using_facts_from '* -FStar.Tactis -FStar.Reflection'"

let and_then #k #t p #k' #t' p' =
  let f : bare_parser t' = and_then_bare p p' in
  and_then_correct p p' ;
  f

let and_then_eq
  (#k: parser_kind)
  (#t:Type)
  (p:parser k t)
  (#k': parser_kind)
  (#t':Type)
  (p': (t -> Tot (parser k' t')))
  (input: bytes)
: Lemma
  (requires (and_then_cases_injective p'))
  (ensures (parse (and_then p p') input == and_then_bare p p' input))
= ()

let tot_and_then_bare (#t:Type) (#t':Type)
                (p:tot_bare_parser t)
                (p': (t -> Tot (tot_bare_parser t'))) :
                Tot (tot_bare_parser t') =
    fun (b: bytes) ->
    match p b with
    | Some (v, l) ->
      begin
	let p'v = p' v in
	let s' : bytes = Seq.slice b l (Seq.length b) in
	match p'v s' with
	| Some (v', l') ->
	  let res : consumed_length b = l + l' in
	  Some (v', res)
	| None -> None
      end
    | None -> None

let tot_and_then #k #t p #k' #t' p' =
  let f : tot_bare_parser t' = tot_and_then_bare p p' in
  and_then_correct #k p #k' p' ;
  parser_kind_prop_ext (and_then_kind k k') (and_then_bare p p') f;
  f

let parse_synth
  (#k: parser_kind)
  (#t1: Type)
  (#t2: Type)
  (p1: parser k t1)
  (f2: t1 -> GTot t2)
: Pure (parser k t2)
  (requires (
    synth_injective f2
  ))
  (ensures (fun _ -> True))
= coerce (parser k t2) (and_then p1 (fun v1 -> parse_fret f2 v1))

let parse_synth_eq
  (#k: parser_kind)
  (#t1: Type)
  (#t2: Type)
  (p1: parser k t1)
  (f2: t1 -> GTot t2)
  (b: bytes)
: Lemma
  (requires (synth_injective f2))
  (ensures (parse (parse_synth p1 f2) b == parse_synth' p1 f2 b))
= ()

unfold
let tot_parse_fret' (#t #t':Type) (f: t -> Tot t') (v:t) : Tot (tot_bare_parser t') =
  fun (b: bytes) -> Some (f v, (0 <: consumed_length b))

unfold
val tot_parse_fret (#t #t': Type) (f: (t -> Tot t')) (v: t) : Tot (tot_parser parse_ret_kind t')
f: (_: t -> t') -> v: t -> LowParse.Spec.Base.tot_parser LowParse.Spec.Combinators.parse_ret_kind t'