val tot_and_then
  (#k: parser_kind)
  (#t:Type)
  (p:tot_parser k t)
  (#k': parser_kind)
  (#t':Type)
  (p': (t -> Tot (tot_parser k' t')))
: Pure (tot_parser (and_then_kind k k') t')
  (requires (
    and_then_cases_injective p'
  ))
  (ensures (fun y ->
    forall x . parse y x == parse (and_then #k p #k' p') x
  ))
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
val tot_and_then
  (#k: parser_kind)
  (#t:Type)
  (p:tot_parser k t)
  (#k': parser_kind)
  (#t':Type)
  (p': (t -> Tot (tot_parser k' t')))
: Pure (tot_parser (and_then_kind k k') t')
  (requires (
    and_then_cases_injective p'
  ))
  (ensures (fun y ->
    forall x . parse y x == parse (and_then #k p #k' p') x
  ))
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
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.Base.parser_kind LowParse.Spec.Base.tot_parser Prims.unit LowParse.Spec.Base.parser_kind_prop_ext LowParse.Spec.Combinators.and_then_kind LowParse.Spec.Combinators.and_then_bare LowParse.Spec.Combinators.and_then_correct LowParse.Spec.Base.tot_bare_parser LowParse.Spec.Combinators.tot_and_then_bare
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
val tot_and_then
  (#k: parser_kind)
  (#t:Type)
  (p:tot_parser k t)
  (#k': parser_kind)
  (#t':Type)
  (p': (t -> Tot (tot_parser k' t')))
: Pure (tot_parser (and_then_kind k k') t')
  (requires (
    and_then_cases_injective p'
  ))
  (ensures (fun y ->
    forall x . parse y x == parse (and_then #k p #k' p') x
  ))
p: LowParse.Spec.Base.tot_parser k t -> p': (_: t -> LowParse.Spec.Base.tot_parser k' t')
  -> Prims.Pure (LowParse.Spec.Base.tot_parser (LowParse.Spec.Combinators.and_then_kind k k') t')