val get_set
      (#t: Type)
      (sd: struct_def t)
      (x: t)
      (f: field_t sd.fields)
      (v: sd.field_desc.fd_type f)
      (f': field_t sd.fields)
    : Lemma (sd.get (set sd x f v) f' == (if f = f' then v else sd.get x f'))
      [SMTPat (sd.get (set sd x f v) f')]
let get_set (#t: Type) (sd: struct_def t) (x: t) (f: field_t sd.fields) (v: sd.field_desc.fd_type f) (f' : field_t sd.fields) : Lemma
  (sd.get (set sd x f v) f' == (if f = f' then v else sd.get x f'))
  [SMTPat (sd.get (set sd x f v) f')]
= sd.get_mk (set_aux sd x f v) f'
val get_set
      (#t: Type)
      (sd: struct_def t)
      (x: t)
      (f: field_t sd.fields)
      (v: sd.field_desc.fd_type f)
      (f': field_t sd.fields)
    : Lemma (sd.get (set sd x f v) f' == (if f = f' then v else sd.get x f'))
      [SMTPat (sd.get (set sd x f v) f')]
let get_set
      (#t: Type)
      (sd: struct_def t)
      (x: t)
      (f: field_t sd.fields)
      (v: sd.field_desc.fd_type f)
      (f': field_t sd.fields)
    : Lemma (sd.get (set sd x f v) f' == (if f = f' then v else sd.get x f'))
      [SMTPat (sd.get (set sd x f v) f')] =
sd.get_mk (set_aux sd x f v) f'
Steel.ST.C.Types.UserStruct.fsti.checked
Steel.ST.Util.fsti.checked Steel.ST.C.Types.Struct.Aux.fsti.checked Steel.FractionalPermission.fst.checked prims.fst.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked
Steel.ST.C.Types.UserStruct.fsti
Steel.ST.C.Types.UserStruct.struct_def Steel.ST.C.Types.UserStruct.field_t Steel.ST.C.Types.UserStruct.__proj__Mkstruct_def__item__fields Steel.ST.C.Types.Struct.Aux.__proj__Mkfield_description_gen_t__item__fd_type Steel.ST.C.Types.UserStruct.__proj__Mkstruct_def__item__field_desc Steel.ST.C.Types.UserStruct.__proj__Mkstruct_def__item__get_mk Steel.ST.C.Types.UserStruct.set_aux Prims.unit Prims.l_True Prims.squash Prims.eq2 Steel.ST.C.Types.UserStruct.__proj__Mkstruct_def__item__get Steel.ST.C.Types.UserStruct.set Prims.op_Equality Prims.bool Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
module Steel.ST.C.Types.UserStruct
open Steel.ST.Util
open Steel.ST.C.Types.Struct.Aux

module Set = FStar.Set

(* This library allows the user to define their own struct type, with
a constructor from field values, and a destructor to field values for
each field. This may be necessary for recursive structs *)

let set_def
  (#t: eqtype)
  (s: FStar.Set.set t)
  (x: t)
: Tot bool
= FStar.Set.mem x s

noextract
let nonempty_set (t: eqtype) =
  (s: Set.set t { exists x . set_def s x == true })

noextract
let set_snoc // for associativity reasons
(#t: eqtype) (q: FStar.Set.set t) (a: t) : Pure (nonempty_set t)
  (requires True)
  (ensures (fun s ->
    (forall (x: t). {:pattern FStar.Set.mem x s} FStar.Set.mem x s == (x = a || FStar.Set.mem x q))
  ))
= q `FStar.Set.union` FStar.Set.singleton a

[@@noextract_to "krml"]
let field_t (s: Set.set string) : Tot eqtype =
  (f: string { Set.mem f s })

[@@noextract_to "krml"; norm_field_attr]
inline_for_extraction // for field_desc.fd_type
noeq
type struct_def (t: Type) = {
  fields: Set.set string;
  field_desc: field_description_gen_t (field_t fields);
  mk: ((f: field_t fields) -> Tot (field_desc.fd_type f)) -> Tot t;
  get: (t -> (f: field_t fields) -> Tot (field_desc.fd_type f));
  get_mk: (phi: ((f: field_t fields) -> Tot (field_desc.fd_type f))) -> (f: field_t fields) -> Lemma
    (get (mk phi) f == phi f);
  extensionality: (x1: t) -> (x2: t) -> ((f: field_t fields) -> Lemma (get x1 f == get x2 f)) -> Lemma (x1 == x2);
}

let nonempty_set_nonempty_type (x: string) (s: Set.set string) : Lemma
  (requires (x `Set.mem` s))
  (ensures (exists (x: field_t s) . True))
= Classical.exists_intro (fun (_: field_t s) -> True) x

[@@noextract_to "krml"]
let set_aux
  (#t: Type) (sd: struct_def t) (x: t) (f: field_t sd.fields) (v: sd.field_desc.fd_type f) (f': field_t sd.fields)
: Tot (sd.field_desc.fd_type f')
= if f = f' then v else sd.get x f'

[@@noextract_to "krml"]
let set (#t: Type) (sd: struct_def t) (x: t) (f: field_t sd.fields) (v: sd.field_desc.fd_type f) : Tot t =
  sd.mk (set_aux sd x f v)

let get_set (#t: Type) (sd: struct_def t) (x: t) (f: field_t sd.fields) (v: sd.field_desc.fd_type f) (f' : field_t sd.fields) : Lemma
  (sd.get (set sd x f v) f' == (if f = f' then v else sd.get x f'))
val get_set
      (#t: Type)
      (sd: struct_def t)
      (x: t)
      (f: field_t sd.fields)
      (v: sd.field_desc.fd_type f)
      (f': field_t sd.fields)
    : Lemma (sd.get (set sd x f v) f' == (if f = f' then v else sd.get x f'))
      [SMTPat (sd.get (set sd x f v) f')]

    sd: Steel.ST.C.Types.UserStruct.struct_def t ->
    x: t ->
    f: Steel.ST.C.Types.UserStruct.field_t (Mkstruct_def?.fields sd) ->
    v: Mkfield_description_gen_t?.fd_type (Mkstruct_def?.field_desc sd) f ->
    f': Steel.ST.C.Types.UserStruct.field_t (Mkstruct_def?.fields sd)
  -> FStar.Pervasives.Lemma
      (ensures
        Mkstruct_def?.get sd (Steel.ST.C.Types.UserStruct.set sd x f v) f' ==
        (match f = f' with
          | true -> v
          | _ -> Mkstruct_def?.get sd x f'))
      [SMTPat (Mkstruct_def?.get sd (Steel.ST.C.Types.UserStruct.set sd x f v) f')]