val parse_tagged_union_impl
      (#tag_t: Type0)
      (#pt: parser_spec tag_t)
      (pt32: parser_impl pt)
      (#data_t: Type0)
      (tag_of_data: (data_t -> GTot tag_t))
      (#p: (t: tag_t -> Tot (parser_spec (refine_with_tag tag_of_data t))))
      (p32: (t: tag_t -> Tot (parser_impl (p t))))
    : Tot (parser_impl (parse_tagged_union pt tag_of_data p))
val parse_tagged_union_impl
      (#tag_t: Type0)
      (#pt: parser_spec tag_t)
      (pt32: parser_impl pt)
      (#data_t: Type0)
      (tag_of_data: (data_t -> GTot tag_t))
      (#p: (t: tag_t -> Tot (parser_spec (refine_with_tag tag_of_data t))))
      (p32: (t: tag_t -> Tot (parser_impl (p t))))
    : Tot (parser_impl (parse_tagged_union pt tag_of_data p))
let parse_tagged_union_impl
  (#tag_t: Type0)
  (#pt: parser_spec tag_t)
  (pt32: parser_impl pt)
  (#data_t: Type0)
  (tag_of_data: (data_t -> GTot tag_t))
  (#p: (t: tag_t) -> Tot (parser_spec (refine_with_tag tag_of_data t)))
  (p32: (t: tag_t) -> Tot (parser_impl (p t)))
: Tot (parser_impl (parse_tagged_union pt tag_of_data p))
= fun input len ->
  match pt32 input len with
  | Some (tg, consumed_tg) ->
    let len1 = len `U32.sub` consumed_tg in
    let input1 = B.sub input consumed_tg len1 in
    begin match p32 tg input1 len1 with
    | Some (d, consumed_d) ->
      Some ((d <: data_t), consumed_tg `U32.add` consumed_d)
    | _ -> None
    end
  | _ -> None
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module MiniParse.Impl.TSum
include MiniParse.Impl.Combinators
include MiniParse.Spec.TSum

module B = LowStar.Buffer
module M = LowStar.ModifiesPat
module U32 = FStar.UInt32
module HST = FStar.HyperStack.ST

#set-options "--z3rlimit 10"
/
prims.fst.checked MiniParse.Spec.TSum.fst.checked MiniParse.Impl.Combinators.fst.checked LowStar.ModifiesPat.fst.checked LowStar.Buffer.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked
MiniParse.Impl.TSum.fst

    pt32: MiniParse.Impl.Base.parser_impl pt ->
    tag_of_data: (_: data_t -> Prims.GTot tag_t) ->
    p32: (t: tag_t -> MiniParse.Impl.Base.parser_impl (p t))
  -> MiniParse.Impl.Base.parser_impl (MiniParse.Spec.TSum.parse_tagged_union pt tag_of_data p)
MiniParse.Spec.Base.parser_spec MiniParse.Impl.Base.parser_impl MiniParse.Spec.TSum.refine_with_tag MiniParse.Impl.Base.buffer8 FStar.UInt32.t Prims.eq2 LowStar.Monotonic.Buffer.len FStar.UInt8.t LowStar.Buffer.trivial_preorder FStar.Pervasives.Native.Some FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.Mktuple2 FStar.UInt32.add FStar.Pervasives.Native.option FStar.Pervasives.Native.None LowStar.Monotonic.Buffer.mbuffer LowStar.Buffer.sub FStar.Ghost.hide FStar.UInt32.sub MiniParse.Spec.TSum.parse_tagged_union
let parse_tagged_union_impl
      (#tag_t: Type0)
      (#pt: parser_spec tag_t)
      (pt32: parser_impl pt)
      (#data_t: Type0)
      (tag_of_data: (data_t -> GTot tag_t))
      (#p: (t: tag_t -> Tot (parser_spec (refine_with_tag tag_of_data t))))
      (p32: (t: tag_t -> Tot (parser_impl (p t))))
    : Tot (parser_impl (parse_tagged_union pt tag_of_data p)) =
  
fun input len ->
  match pt32 input len with
  | Some (tg, consumed_tg) ->
    let len1 = len `U32.sub` consumed_tg in
    let input1 = B.sub input consumed_tg len1 in
    (match p32 tg input1 len1 with
      | Some (d, consumed_d) -> Some ((d <: data_t), consumed_tg `U32.add` consumed_d)
      | _ -> None)
  | _ -> None