val maybe_enum_key_of_repr (#key #repr: eqtype) (e: enum key repr) (r: repr)
    : Tot (maybe_enum_key e)
let maybe_enum_key_of_repr
  (#key #repr: eqtype)
  (e: enum key repr)
  (r: repr)
: Tot (maybe_enum_key e)
= if list_mem r (list_map snd e)
  then Known (enum_key_of_repr e r)
  else Unknown r
val maybe_enum_key_of_repr (#key #repr: eqtype) (e: enum key repr) (r: repr)
    : Tot (maybe_enum_key e)
let maybe_enum_key_of_repr (#key #repr: eqtype) (e: enum key repr) (r: repr)
    : Tot (maybe_enum_key e) =
if list_mem r (list_map snd e) then Known (enum_key_of_repr e r) else Unknown r
LowParse.Spec.Enum.fst.checked
prims.fst.checked LowParse.Spec.Combinators.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
LowParse.Spec.Enum.fst
Prims.eqtype LowParse.Spec.Enum.enum LowParse.Spec.Enum.list_mem LowParse.Spec.Enum.list_map FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.snd LowParse.Spec.Enum.Known LowParse.Spec.Enum.enum_key_of_repr Prims.bool LowParse.Spec.Enum.Unknown LowParse.Spec.Enum.maybe_enum_key
module LowParse.Spec.Enum
include LowParse.Spec.Combinators

module L = FStar.List.Tot

[@Norm]
let rec list_map
  (#a #b: Type)
  (f: (a -> Tot b))
  (l: list a)
: Tot (l' : list b { l' == L.map f l } )
= match l with
  | [] -> []
  | a :: q -> f a :: list_map f q

type enum (key: eqtype) (repr: eqtype) = (l: list (key * repr) {
  L.noRepeats (list_map fst l) /\
  L.noRepeats (list_map snd l)
})

[@Norm]
let rec list_mem
  (#t: eqtype)
  (x: t)
  (l: list t)
: Tot (y: bool { y == true <==> L.mem x l == true } )
= match l with
  | [] -> false
  | a :: q -> (x = a || list_mem x q)

inline_for_extraction
let enum_key (#key #repr: eqtype) (e: enum key repr) : Tot eqtype = (s: key { list_mem s (list_map fst e) } )

inline_for_extraction
let make_enum_key (#key #repr: eqtype) (e: enum key repr) (k: key) : Pure (enum_key e)
  (requires (list_mem k (list_map fst e)))
  (ensures (fun k' -> k == (k' <: key)))
= k

inline_for_extraction
let enum_repr (#key #repr: eqtype) (e: enum key repr) : Tot eqtype = (r: repr { list_mem r (list_map snd e) } )

let flip (#a #b: Type) (c: (a * b)) : Tot (b * a) = let (ca, cb) = c in (cb, ca)

let rec map_flip_flip (#a #b: Type) (l: list (a * b)) : Lemma
  (list_map flip (list_map flip l) == l)
= match l with
  | [] -> ()
  | _ :: q -> map_flip_flip q

let rec map_fst_flip (#a #b: Type) (l: list (a * b)) : Lemma
  (list_map fst (list_map flip l) == list_map snd l)
= match l with
  | [] -> ()
  | _ :: q -> map_fst_flip q

let rec map_snd_flip (#a #b: Type) (l: list (a * b)) : Lemma
  (list_map snd (list_map flip l) == list_map fst l)
= match l with
  | [] -> ()
  | _ :: q -> map_snd_flip q

let rec assoc_mem_snd
  (#a #b: eqtype)
  (l: list (a * b))
  (x: a)
  (y: b)
: Lemma
  (requires (L.assoc x l == Some y))
  (ensures (list_mem y (list_map snd l) == true))
  (decreases l)
= let ((x', y') :: l') = l in
  if x' = x
  then ()
  else assoc_mem_snd l' x y

let rec assoc_flip_elim
  (#a #b: eqtype)
  (l: list (a * b))
  (y: b)
  (x: a)
: Lemma
  (requires (
    L.noRepeats (list_map fst l) /\
    L.noRepeats (list_map snd l) /\
    L.assoc y (list_map flip l) == Some x
  ))
  (ensures (
    L.assoc x l == Some y
  ))
  (decreases l)
= let ((x', y') :: l') = l in
  if y' = y
  then ()
  else begin
    if x' = x
    then begin
      assert (list_mem x' (list_map fst l') == false);
      assoc_mem_snd (list_map flip l') y x;
      map_snd_flip l';
      assert False
    end
    else
      assoc_flip_elim l' y x
  end

let rec assoc_flip_intro
  (#a #b: eqtype)
  (l: list (a * b))
  (y: b)
  (x: a)
: Lemma
  (requires (
    L.noRepeats (list_map fst l) /\
    L.noRepeats (list_map snd l) /\
    L.assoc x l == Some y
  ))
  (ensures (
    L.assoc y (list_map flip l) == Some x
  ))
= map_fst_flip l;
  map_snd_flip l;
  map_flip_flip l;
  assoc_flip_elim (list_map flip l) x y

let enum_key_of_repr
  (#key #repr: eqtype)
  (e: enum key repr)
  (r: enum_repr e)
: Pure (enum_key e)
  (requires True)
  (ensures (fun y -> L.assoc y e == Some r))
= map_fst_flip e;
  let e' = list_map #(key * repr) #(repr * key) flip e in
  L.assoc_mem r e';
  let k = Some?.v (L.assoc r e') in
  assoc_flip_elim e r k;
  L.assoc_mem k e;
  (k <: enum_key e)

let parse_enum_key_cond
  (#key #repr: eqtype)
  (e: enum key repr)
  (r: repr)
: GTot bool
= list_mem r (list_map snd e)

let parse_enum_key_synth
  (#key #repr: eqtype)
  (e: enum key repr)
  (r: repr { parse_enum_key_cond e r == true } )
: GTot (enum_key e)
= enum_key_of_repr e r

let parse_enum_key
  (#k: parser_kind)
  (#key #repr: eqtype)
  (p: parser k repr)
  (e: enum key repr)
: Tot (parser (parse_filter_kind k) (enum_key e))
= (p
    `parse_filter`
    parse_enum_key_cond e
  )
  `parse_synth`
  parse_enum_key_synth e

let enum_repr_of_key
  (#key #repr: eqtype)
  (e: enum key repr)
  (k: enum_key e)
: Pure (enum_repr e)
  (requires True)
  (ensures (fun r -> L.assoc k e == Some r))
= L.assoc_mem k e;
  let r = Some?.v (L.assoc k e) in
  assoc_flip_intro e r k;
  L.assoc_mem r (list_map flip e);
  map_fst_flip e;
  (r <: enum_repr e)

let enum_repr_of_key_of_repr
  (#key #repr: eqtype)
  (e: enum key repr)
  (r: enum_repr e)
: Lemma
  (enum_repr_of_key e (enum_key_of_repr e r) == r)
= ()

let enum_key_of_repr_of_key
  (#key #repr: eqtype)
  (e: enum key repr)
  (k: enum_key e)
: Lemma
  (enum_key_of_repr e (enum_repr_of_key e k) == k)
= assoc_flip_intro e (enum_repr_of_key e k) k

let serialize_enum_key_synth_recip 
  (#key #repr: eqtype)
  (e: enum key repr)
  (k: enum_key e)
: GTot (r: repr { parse_enum_key_cond e r == true } )
= enum_repr_of_key e k

let serialize_enum_key_synth_inverse
  (#key #repr: eqtype)
  (e: enum key repr)
: Lemma
  (synth_inverse (parse_enum_key_synth e) (serialize_enum_key_synth_recip e))
= Classical.forall_intro (enum_key_of_repr_of_key e)

let serialize_enum_key
  (#k: parser_kind)
  (#key #repr: eqtype)
  (p: parser k repr)
  (s: serializer p)
  (e: enum key repr)
: Tot (serializer (parse_enum_key p e))
= serialize_enum_key_synth_inverse e;
  serialize_synth
    (parse_filter p (parse_enum_key_cond e))
    (parse_enum_key_synth e)
    (serialize_filter s (parse_enum_key_cond e))
    (serialize_enum_key_synth_recip e)
    ()

let serialize_enum_key_eq
  (#k: parser_kind)
  (#key #repr: eqtype)
  (#p: parser k repr)
  (s: serializer p)
  (e: enum key repr)
  (x: enum_key e)
: Lemma
  (serialize (serialize_enum_key p s e) x == serialize s (enum_repr_of_key e x))
= serialize_enum_key_synth_inverse e;
  serialize_synth_eq
    (parse_filter p (parse_enum_key_cond e))
    (parse_enum_key_synth e)
    (serialize_filter s (parse_enum_key_cond e))
    (serialize_enum_key_synth_recip e)
    ()
    x

inline_for_extraction
let unknown_enum_repr (#key #repr: eqtype) (e: enum key repr) : Tot Type =
  (r: repr { list_mem r (list_map snd e) == false } )

type maybe_enum_key (#key #repr: eqtype) (e: enum key repr) =
| Known of (enum_key e)
| Unknown of (unknown_enum_repr e)

let maybe_enum_key_of_repr
  (#key #repr: eqtype)
  (e: enum key repr)
  (r: repr)
val maybe_enum_key_of_repr (#key #repr: eqtype) (e: enum key repr) (r: repr)
    : Tot (maybe_enum_key e)
e: LowParse.Spec.Enum.enum key repr -> r: repr -> LowParse.Spec.Enum.maybe_enum_key e