val serialize_tagged_union_impl
      (#tag_t: Type0)
      (#pt: parser_spec tag_t)
      (#st: serializer_spec pt)
      (st32: serializer_impl st)
      (#data_t: Type0)
      (tag_of_data: (data_t -> GTot tag_t))
      (tag_of_data32: (x: data_t -> Tot (y: tag_t{y == tag_of_data x})))
      (#p: (t: tag_t -> Tot (parser_spec (refine_with_tag tag_of_data t))))
      (#s: (t: tag_t -> Tot (serializer_spec (p t))))
      (s32: (t: tag_t -> Tot (serializer_impl (s t))))
    : Tot (serializer_impl (serialize_tagged_union st tag_of_data s))
val serialize_tagged_union_impl
      (#tag_t: Type0)
      (#pt: parser_spec tag_t)
      (#st: serializer_spec pt)
      (st32: serializer_impl st)
      (#data_t: Type0)
      (tag_of_data: (data_t -> GTot tag_t))
      (tag_of_data32: (x: data_t -> Tot (y: tag_t{y == tag_of_data x})))
      (#p: (t: tag_t -> Tot (parser_spec (refine_with_tag tag_of_data t))))
      (#s: (t: tag_t -> Tot (serializer_spec (p t))))
      (s32: (t: tag_t -> Tot (serializer_impl (s t))))
    : Tot (serializer_impl (serialize_tagged_union st tag_of_data s))
let serialize_tagged_union_impl
  (#tag_t: Type0)
  (#pt: parser_spec tag_t)
  (#st: serializer_spec pt)
  (st32: serializer_impl st)
  (#data_t: Type0)
  (tag_of_data: (data_t -> GTot tag_t))
  (tag_of_data32: ((x: data_t) -> Tot (y: tag_t { y == tag_of_data x } )))
  (#p: (t: tag_t) -> Tot (parser_spec (refine_with_tag tag_of_data t)))
  (#s: (t: tag_t) -> Tot (serializer_spec (p t)))
  (s32: (t: tag_t) -> Tot (serializer_impl (s t)))
: Tot (serializer_impl (serialize_tagged_union st tag_of_data s))
= fun (output: buffer8) (len: U32.t { len == B.len output } ) (x: data_t) ->
  let tg = tag_of_data32 x in
  match st32 output len tg with
  | Some sz1 ->
    let output1 = B.offset output sz1 in
    let len1 = len `U32.sub` sz1 in
    begin match s32 tg output1 len1 x with
    | Some sz2 ->
      let h2 = HST.get () in
      seq_append_slice (B.as_seq h2 output) (U32.v sz1) (U32.v sz2);
      Some (sz1 `U32.add` sz2)
    | _ -> 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"
inline_for_extraction
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

#set-options "--z3rlimit 16"
/
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

    st32: MiniParse.Impl.Base.serializer_impl st ->
    tag_of_data: (_: data_t -> Prims.GTot tag_t) ->
    tag_of_data32: (x: data_t -> y: tag_t{y == tag_of_data x}) ->
    s32: (t: tag_t -> MiniParse.Impl.Base.serializer_impl (s t))
  -> MiniParse.Impl.Base.serializer_impl (MiniParse.Spec.TSum.serialize_tagged_union st
          tag_of_data
          s)
MiniParse.Spec.Base.parser_spec MiniParse.Spec.Base.serializer_spec MiniParse.Impl.Base.serializer_impl Prims.eq2 MiniParse.Spec.TSum.refine_with_tag MiniParse.Impl.Base.buffer8 FStar.UInt32.t LowStar.Monotonic.Buffer.len FStar.UInt8.t LowStar.Buffer.trivial_preorder FStar.Pervasives.Native.Some FStar.UInt32.add Prims.unit MiniParse.Impl.Combinators.seq_append_slice LowStar.Monotonic.Buffer.as_seq FStar.UInt32.v FStar.Pervasives.Native.option FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get FStar.Pervasives.Native.None FStar.UInt32.sub LowStar.Monotonic.Buffer.mbuffer LowStar.Buffer.offset MiniParse.Spec.TSum.parse_tagged_union MiniParse.Spec.TSum.serialize_tagged_union
let serialize_tagged_union_impl
      (#tag_t: Type0)
      (#pt: parser_spec tag_t)
      (#st: serializer_spec pt)
      (st32: serializer_impl st)
      (#data_t: Type0)
      (tag_of_data: (data_t -> GTot tag_t))
      (tag_of_data32: (x: data_t -> Tot (y: tag_t{y == tag_of_data x})))
      (#p: (t: tag_t -> Tot (parser_spec (refine_with_tag tag_of_data t))))
      (#s: (t: tag_t -> Tot (serializer_spec (p t))))
      (s32: (t: tag_t -> Tot (serializer_impl (s t))))
    : Tot (serializer_impl (serialize_tagged_union st tag_of_data s)) =
  
fun (output: buffer8) (len: U32.t{len == B.len output}) (x: data_t) ->
  let tg = tag_of_data32 x in
  match st32 output len tg with
  | Some sz1 ->
    let output1 = B.offset output sz1 in
    let len1 = len `U32.sub` sz1 in
    (match s32 tg output1 len1 x with
      | Some sz2 ->
        let h2 = HST.get () in
        seq_append_slice (B.as_seq h2 output) (U32.v sz1) (U32.v sz2);
        Some (sz1 `U32.add` sz2)
      | _ -> None)
  | _ -> None