val synth_sum_case_inverse (s: sum) (k: sum_key s)
    : Lemma (synth_inverse (synth_sum_case s k) (synth_sum_case_recip s k))
let synth_sum_case_inverse (s: sum) (k: sum_key s) : Lemma
  (synth_inverse (synth_sum_case s k) (synth_sum_case_recip s k))
= Classical.forall_intro (Sum?.synth_case_synth_case_recip s)
val synth_sum_case_inverse (s: sum) (k: sum_key s)
    : Lemma (synth_inverse (synth_sum_case s k) (synth_sum_case_recip s k))
let synth_sum_case_inverse (s: sum) (k: sum_key s)
    : Lemma (synth_inverse (synth_sum_case s k) (synth_sum_case_recip s k)) =
Classical.forall_intro (Sum?.synth_case_synth_case_recip s)
LowParse.Spec.Sum.fst.checked
prims.fst.checked LowParse.Spec.Enum.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
LowParse.Spec.Sum.fst
LowParse.Spec.Sum.sum LowParse.Spec.Sum.sum_key FStar.Classical.forall_intro LowParse.Spec.Sum.__proj__Sum__item__data Prims.eq2 LowParse.Spec.Sum.__proj__Sum__item__synth_case LowParse.Spec.Sum.__proj__Sum__item__tag_of_data LowParse.Spec.Sum.synth_case_recip' LowParse.Spec.Sum.__proj__Sum__item__key LowParse.Spec.Sum.__proj__Sum__item__repr LowParse.Spec.Sum.__proj__Sum__item__e LowParse.Spec.Sum.__proj__Sum__item__type_of_tag LowParse.Spec.Sum.__proj__Sum__item__synth_case_recip LowParse.Spec.Sum.__proj__Sum__item__synth_case_synth_case_recip Prims.unit Prims.l_True Prims.squash LowParse.Spec.Combinators.synth_inverse LowParse.Spec.Sum.sum_type_of_tag LowParse.Spec.Sum.sum_cases LowParse.Spec.Sum.synth_sum_case LowParse.Spec.Sum.synth_sum_case_recip Prims.Nil FStar.Pervasives.pattern
module LowParse.Spec.Sum
include LowParse.Spec.Enum

module Seq = FStar.Seq

let synth_case_recip'
    (#key: eqtype)
    (#repr: eqtype)
    (e: enum key repr)
    (#data: Type)
    (tag_of_data: (data -> Tot (enum_key e)))
    (type_of_tag: (enum_key e -> Tot Type))
    (synth_case_recip: ((k: enum_key e) -> (x: refine_with_tag tag_of_data k) -> Tot (type_of_tag k)))
    (x: data)
: GTot (type_of_tag (tag_of_data x))
= synth_case_recip (tag_of_data x) x

noeq
type sum =
| Sum:
    (key: eqtype) ->
    (repr: eqtype) ->
    (e: enum key repr) ->
    (data: Type) ->
    (tag_of_data: (data -> Tot (enum_key e))) ->
    (type_of_tag: (enum_key e -> Tot Type)) ->
    (synth_case: ((x: enum_key e) -> (y: type_of_tag x) -> Tot (refine_with_tag tag_of_data x))) ->
    (synth_case_recip: ((k: enum_key e) -> (x: refine_with_tag tag_of_data k) -> Tot (type_of_tag k))) ->
    (synth_case_recip_synth_case: (
      (x: enum_key e) ->
      (y: type_of_tag x) ->
      Lemma
      (synth_case_recip' e tag_of_data type_of_tag synth_case_recip (synth_case x y) == y)
    )) ->
    (synth_case_synth_case_recip: (
      (x: data) ->
      Lemma
      (synth_case (tag_of_data x) (synth_case_recip' e tag_of_data type_of_tag synth_case_recip x) == x)
    )) ->
    sum

inline_for_extraction
let sum_key_type (t: sum) : Tot eqtype =
  match t with (Sum key _ _ _ _ _ _ _ _ _) -> key

inline_for_extraction
let sum_repr_type (t: sum) : Tot eqtype =
  match t with (Sum _ repr _ _ _ _ _ _ _ _) -> repr

inline_for_extraction
let sum_enum (t: sum) : Tot (enum (sum_key_type t) (sum_repr_type t)) =
  match t with (Sum _ _ e _ _ _ _ _ _ _) -> e

inline_for_extraction
let sum_key (t: sum) : Tot Type =
  enum_key (sum_enum t)

inline_for_extraction
let sum_key_type_of_sum_key (t: sum) (k: sum_key t) : Pure (sum_key_type t)
  (requires True)
  (ensures (fun k' -> k' == (k <: sum_key_type t)))
= k

inline_for_extraction
let sum_type (t: sum) : Tot Type =
  match t with
  | Sum _ _ _ data _ _ _ _ _ _ -> data

inline_for_extraction
let sum_tag_of_data (t: sum) : Tot ((x: sum_type t) -> Tot (sum_key t)) =
  match t with
  | Sum _ _ _ _ tag_of_data _ _ _ _ _ -> tag_of_data

inline_for_extraction
let sum_cases (t: sum) (x: sum_key t) : Type =
  refine_with_tag #(sum_key t) #(sum_type t) (sum_tag_of_data t) x

inline_for_extraction
let sum_type_of_tag (t: sum) : (x: sum_key t) -> Type =
  match t with
  | Sum _ _ _ _ _ type_of_tag _ _ _ _ -> type_of_tag

let weaken_parse_cases_kind
  (s: sum)
  (f: (x: sum_key s) -> Tot (k: parser_kind & parser k (sum_type_of_tag s x)))
: Tot parser_kind
= let keys : list (sum_key_type s) = List.Tot.map fst (sum_enum s) in
  glb_list_of #(sum_key_type s) (fun (x: sum_key_type s) ->
    if List.Tot.mem x keys
    then let (| k, _ |) = f x in k
    else default_parser_kind
  ) (List.Tot.map fst (sum_enum s))

inline_for_extraction
let synth_sum_case (s: sum) : (k: sum_key s) -> (x: sum_type_of_tag s k) -> Tot (sum_cases s k) =
  match s with
  | Sum _ _ _ _ _ _ synth_case _ _ _ -> synth_case

let synth_sum_case_injective (s: sum) (k: sum_key s) : Lemma
  (synth_injective (synth_sum_case s k))
= Classical.forall_intro (Sum?.synth_case_recip_synth_case s k)

let parse_sum_cases
  (s: sum)
  (f: (x: sum_key s) -> Tot (k: parser_kind & parser k (sum_type_of_tag s x)))
  (x: sum_key s)
: Tot (parser (weaken_parse_cases_kind s f) (sum_cases s x))
= synth_sum_case_injective s x;
  weaken (weaken_parse_cases_kind s f) (dsnd (f x)) `parse_synth` (synth_sum_case s x)

let parse_sum_cases_eq
  (s: sum)
  (f: (x: sum_key s) -> Tot (k: parser_kind & parser k (sum_type_of_tag s x)))
  (x: sum_key s)
  (input: bytes)
: Lemma
  (parse (parse_sum_cases s f x) input == (match parse (dsnd (f x)) input with
  | None -> None
  | Some (y, consumed) -> Some (synth_sum_case s x y, consumed)
  ))
= synth_sum_case_injective s x;
  parse_synth_eq (weaken (weaken_parse_cases_kind s f) (dsnd (f x))) (synth_sum_case s x) input

let parse_sum_cases'
  (s: sum)
  (f: (x: sum_key s) -> Tot (k: parser_kind & parser k (sum_type_of_tag s x)))
  (x: sum_key s)
: Tot (parser (dfst (f x)) (sum_cases s x))
=
  synth_sum_case_injective s x;
  dsnd (f x) `parse_synth` synth_sum_case s x

let parse_sum_cases_eq'
  (s: sum)
  (f: (x: sum_key s) -> Tot (k: parser_kind & parser k (sum_type_of_tag s x)))
  (x: sum_key s)
  (input: bytes)
: Lemma
  (parse (parse_sum_cases s f x) input == parse (parse_sum_cases' s f x) input)
= synth_sum_case_injective s x;
  parse_synth_eq (weaken (weaken_parse_cases_kind s f) (dsnd (f x))) (synth_sum_case s x) input;
  parse_synth_eq (dsnd (f x)) (synth_sum_case s x) input

let parse_sum'
  (#kt: parser_kind)
  (t: sum)
  (p: parser kt (sum_repr_type t))
  (#k: parser_kind)
  (pc: ((x: sum_key t) -> Tot (parser k (sum_cases t x))))
: Tot (parser (and_then_kind (parse_filter_kind kt) k) (sum_type t))
= parse_tagged_union
    #(parse_filter_kind kt)
    #(sum_key t)
    (parse_enum_key p (sum_enum t))
    #(sum_type t)
    (sum_tag_of_data t)
    #k
    pc

inline_for_extraction
let parse_sum_kind
  (kt: parser_kind)
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
: Tot parser_kind
= and_then_kind (parse_filter_kind kt) (weaken_parse_cases_kind t pc)

let parse_sum
  (#kt: parser_kind)
  (t: sum)
  (p: parser kt (sum_repr_type t))
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
: Tot (parser (parse_sum_kind kt t pc) (sum_type t))
= parse_sum' t p (parse_sum_cases t pc)

let parse_sum_eq'
  (#kt: parser_kind)
  (t: sum)
  (p: parser kt (sum_repr_type t))
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (input: bytes)
: Lemma
  (parse (parse_sum t p pc) input == (match parse (parse_enum_key p (sum_enum t)) input with
  | None -> None
  | Some (k, consumed_k) ->
    let input_k = Seq.slice input consumed_k (Seq.length input) in
    begin match
//      parse (synth_sum_case_injective t k; parse_synth (dsnd (pc k)) (synth_sum_case t k)) input_k
      parse (parse_sum_cases' t pc k) input_k
    with
    | None -> None
    | Some (x, consumed_x) -> Some ((x <: sum_type t), consumed_k + consumed_x)
    end
  ))
= parse_tagged_union_eq_gen
    #(parse_filter_kind kt)
    #(sum_key t)
    (parse_enum_key p (sum_enum t))
    #(sum_type t)
    (sum_tag_of_data t)
    (parse_sum_cases t pc)
    (parse_enum_key p (sum_enum t))
    (fun input -> ())
    (fun k -> dfst (pc k))
    (parse_sum_cases' t pc)
    (fun k input -> parse_sum_cases_eq' t pc k input)
    input

let parse_sum_eq
  (#kt: parser_kind)
  (t: sum)
  (p: parser kt (sum_repr_type t))
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (input: bytes)
: Lemma
  (parse (parse_sum t p pc) input == (match parse (parse_enum_key p (sum_enum t)) input with
  | None -> None
  | Some (k, consumed_k) ->
    let input_k = Seq.slice input consumed_k (Seq.length input) in
    begin match parse (dsnd (pc k)) input_k with
    | None -> None
    | Some (x, consumed_x) -> Some ((synth_sum_case t k x <: sum_type t), consumed_k + consumed_x)
    end
  ))
= parse_sum_eq' t p pc input;
  match parse (parse_enum_key p (sum_enum t)) input with
  | None -> ()
  | Some (k, consumed_k) ->
    let input_k = Seq.slice input consumed_k (Seq.length input) in
    synth_sum_case_injective t k;
    parse_synth_eq (dsnd (pc k)) (synth_sum_case t k) input_k

let parse_sum_eq''
  (#kt: parser_kind)
  (t: sum)
  (p: parser kt (sum_repr_type t))
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (input: bytes)
: Lemma
  (parse (parse_sum t p pc) input == (match parse p input with
  | None -> None
  | Some (k', consumed_k) ->
    let input_k = Seq.slice input consumed_k (Seq.length input) in
    let k = maybe_enum_key_of_repr (sum_enum t) k' in
    begin match k with
    | Known k ->
      begin match parse (dsnd (pc k)) input_k with
      | None -> None
      | Some (x, consumed_x) -> Some ((synth_sum_case t k x <: sum_type t), consumed_k + consumed_x)
      end
    | _ -> None
    end
  ))
= parse_sum_eq t p pc input;
  parse_enum_key_eq p (sum_enum t) input

inline_for_extraction
let synth_sum_case_recip (s: sum) (k: sum_key s) (x: sum_cases s k) : Tot (sum_type_of_tag s k) =
  match s with (Sum _ _ _ _ _ _ _ synth_case_recip _ _) ->
  synth_case_recip k x

let synth_sum_case_inverse (s: sum) (k: sum_key s) : Lemma
val synth_sum_case_inverse (s: sum) (k: sum_key s)
    : Lemma (synth_inverse (synth_sum_case s k) (synth_sum_case_recip s k))
s: LowParse.Spec.Sum.sum -> k: LowParse.Spec.Sum.sum_key s
  -> FStar.Pervasives.Lemma
    (ensures
      LowParse.Spec.Combinators.synth_inverse (LowParse.Spec.Sum.synth_sum_case s k)
        (LowParse.Spec.Sum.synth_sum_case_recip s k))