val loc_all_regions_from (#aloc: aloc_t) (#c: cls aloc) (preserve_liveness: bool) (r: HS.rid)
    : GTot (loc c)
let loc_all_regions_from
  (#aloc: aloc_t) (#c: cls aloc)
  (preserve_liveness: bool)
  (r: HS.rid)
: GTot (loc c)
= loc_regions preserve_liveness (HS.mod_set (Set.singleton r))
val loc_all_regions_from (#aloc: aloc_t) (#c: cls aloc) (preserve_liveness: bool) (r: HS.rid)
    : GTot (loc c)
let loc_all_regions_from (#aloc: aloc_t) (#c: cls aloc) (preserve_liveness: bool) (r: HS.rid)
    : GTot (loc c) =
loc_regions preserve_liveness (HS.mod_set (Set.singleton r))
FStar.ModifiesGen.fsti.checked
prims.fst.checked FStar.Set.fsti.checked FStar.Preorder.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked
FStar.ModifiesGen.fsti
FStar.ModifiesGen.aloc_t FStar.ModifiesGen.cls Prims.bool FStar.Monotonic.HyperHeap.rid FStar.ModifiesGen.loc_regions FStar.Monotonic.HyperHeap.mod_set FStar.Set.singleton FStar.ModifiesGen.loc
(*
   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 FStar.ModifiesGen

module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST

(*** The modifies clause *)

(* NOTE: aloc cannot be a member of the class, because of OCaml
   extraction. So it must be a parameter of the class instead. *)

type aloc_t = HS.rid -> nat -> Tot Type

noeq
type cls (aloc: aloc_t) : Type = | Cls:
  (aloc_includes: (
    (#r: HS.rid) ->
    (#a: nat) ->
    aloc r a ->
    aloc r a ->
    GTot Type0
  )) ->
  (aloc_includes_refl: (
    (#r: HS.rid) ->
    (#a: nat) ->
    (x: aloc r a) ->
    Lemma
    (aloc_includes x x)
  )) ->
  (aloc_includes_trans: (
    (#r: HS.rid) ->
    (#a: nat) ->
    (x1: aloc r a) ->
    (x2: aloc r a) ->
    (x3: aloc r a) ->
    Lemma
    (requires (aloc_includes x1 x2 /\ aloc_includes x2 x3))
    (ensures (aloc_includes x1 x3))
  )) ->
  (aloc_disjoint: (
    (#r: HS.rid) ->
    (#a: nat) ->
    (x1: aloc r a) ->
    (x2: aloc r a) ->
    GTot Type0
  )) ->
  (aloc_disjoint_sym: (
    (#r: HS.rid) ->
    (#a: nat) ->
    (x1: aloc r a) ->
    (x2: aloc r a) ->
    Lemma
    (aloc_disjoint x1 x2 <==> aloc_disjoint x2 x1)
  )) ->
  (aloc_disjoint_includes: (
    (#r: HS.rid) ->
    (#a: nat) ->
    (larger1: aloc r a) ->
    (larger2: aloc r a) ->
    (smaller1: aloc r a) ->
    (smaller2: aloc r a) ->
    Lemma
    (requires (aloc_disjoint larger1 larger2 /\ larger1 `aloc_includes` smaller1 /\ larger2 `aloc_includes` smaller2))
    (ensures (aloc_disjoint smaller1 smaller2))
  )) ->
  (aloc_preserved: (
    (#r: HS.rid) ->
    (#a: nat) ->
    aloc r a ->
    HS.mem ->
    HS.mem ->
    GTot Type0
  )) ->
  (aloc_preserved_refl: (
    (#r: HS.rid) ->
    (#a: nat) ->
    (x: aloc r a) ->
    (h: HS.mem) ->
    Lemma
    (aloc_preserved x h h)
  )) ->
  (aloc_preserved_trans: (
    (#r: HS.rid) ->
    (#a: nat) ->
    (x: aloc r a) ->
    (h1: HS.mem) ->
    (h2: HS.mem) ->
    (h3: HS.mem) ->
    Lemma
    (requires (aloc_preserved x h1 h2 /\ aloc_preserved x h2 h3))
    (ensures (aloc_preserved x h1 h3))
  )) ->
  (* if any reference at this address is preserved, then any location at this address is preserved *)
  (same_mreference_aloc_preserved: (
    (#r: HS.rid) ->
    (#a: nat) ->
    (b: aloc r a) ->
    (h1: HS.mem) ->
    (h2: HS.mem) ->
    (f: (
      (a' : Type0) ->
      (pre: Preorder.preorder a') ->
      (r': HS.mreference a' pre) ->
      Lemma
      (requires (h1 `HS.contains` r' /\ r == HS.frameOf r' /\ a == HS.as_addr r'))
      (ensures (h2 `HS.contains` r' /\ h1 `HS.sel` r' == h2 `HS.sel` r'))
    )) ->
    Lemma
    (aloc_preserved b h1 h2)
  )) ->
  cls aloc

val loc (#aloc: aloc_t u#x) (c: cls aloc) : Tot (Type u#x)

val loc_none (#aloc: aloc_t) (#c: cls aloc): Tot (loc c)

val loc_union
  (#aloc: aloc_t) (#c: cls aloc)
  (s1 s2: loc c)
: GTot (loc c)

(** The following is useful to make Z3 cut matching loops with
modifies_trans and modifies_refl *)
val loc_union_idem
  (#aloc: aloc_t) (#c: cls aloc)
  (s: loc c)
: Lemma
  (loc_union s s == s)

val loc_union_comm
  (#aloc: aloc_t) (#c: cls aloc)
  (s1 s2: loc c)
: Lemma
  (loc_union s1 s2 == loc_union s2 s1)

val loc_union_assoc
  (#aloc: aloc_t) (#c: cls aloc)
  (s1 s2 s3: loc c)
: Lemma
  (loc_union s1 (loc_union s2 s3) == loc_union (loc_union s1 s2) s3)

val loc_union_loc_none_l
  (#aloc: aloc_t) (#c: cls aloc)
  (s: loc c)
: Lemma
  (loc_union loc_none s == s)

val loc_union_loc_none_r
  (#aloc: aloc_t) (#c: cls aloc)
  (s: loc c)
: Lemma
  (loc_union s loc_none == s)


val loc_of_aloc
  (#aloc: aloc_t) (#c: cls aloc)
  (#r: HS.rid)
  (#n: nat)
  (b: aloc r n)
: GTot (loc c)

val loc_of_aloc_not_none
  (#aloc: aloc_t) (#c: cls aloc)
  (#r: HS.rid)
  (#n: nat)
  (b: aloc r n)
: Lemma (loc_of_aloc #_ #c b == loc_none ==> False)

val loc_addresses
  (#aloc: aloc_t) (#c: cls aloc)
  (preserve_liveness: bool)
  (r: HS.rid)
  (n: Set.set nat)
: GTot (loc c)

val loc_regions
  (#aloc: aloc_t) (#c: cls aloc)
  (preserve_liveness: bool)
  (r: Set.set HS.rid)
: GTot (loc c)

let loc_mreference
  (#aloc: aloc_t) (#c: cls aloc)
  (#a: Type)
  (#p: Preorder.preorder a)
  (b: HS.mreference a p)
: GTot (loc c)
= loc_addresses true (HS.frameOf b) (Set.singleton (HS.as_addr b))

let loc_freed_mreference
  (#aloc: aloc_t) (#c: cls aloc)
  (#a: Type)
  (#p: Preorder.preorder a)
  (b: HS.mreference a p)
: GTot (loc c)
= loc_addresses false (HS.frameOf b) (Set.singleton (HS.as_addr b))

let loc_region_only
  (#aloc: aloc_t) (#c: cls aloc)
  (preserve_liveness: bool)
  (r: HS.rid)
: GTot (loc c)
= loc_regions preserve_liveness (Set.singleton r)

let loc_all_regions_from
  (#aloc: aloc_t) (#c: cls aloc)
  (preserve_liveness: bool)
  (r: HS.rid)
val loc_all_regions_from (#aloc: aloc_t) (#c: cls aloc) (preserve_liveness: bool) (r: HS.rid)
    : GTot (loc c)
preserve_liveness: Prims.bool -> r: FStar.Monotonic.HyperHeap.rid
  -> Prims.GTot (FStar.ModifiesGen.loc c)