val fresh
      (#a: eqtype)
      (#b: (a -> Type))
      (#inv: (DM.t a (opt b) -> Type))
      (#r: HST.erid)
      (t: t r a b inv)
      (x: a)
      (h: HS.mem)
    : GTot Type0
let fresh
    (#a:eqtype)
    (#b:a -> Type)
    (#inv:DM.t a (opt b) -> Type)
    (#r:HST.erid)
    (t:t r a b inv)
    (x:a)
    (h:HS.mem)
  : GTot Type0
  = ~ (defined t x h)
val fresh
      (#a: eqtype)
      (#b: (a -> Type))
      (#inv: (DM.t a (opt b) -> Type))
      (#r: HST.erid)
      (t: t r a b inv)
      (x: a)
      (h: HS.mem)
    : GTot Type0
let fresh
      (#a: eqtype)
      (#b: (a -> Type))
      (#inv: (DM.t a (opt b) -> Type))
      (#r: HST.erid)
      (t: t r a b inv)
      (x: a)
      (h: HS.mem)
    : GTot Type0 =
~(defined t x h)
FStar.Monotonic.DependentMap.fsti.checked
prims.fst.checked FStar.Set.fsti.checked FStar.Preorder.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.DependentMap.fsti.checked
FStar.Monotonic.DependentMap.fsti
Prims.eqtype FStar.DependentMap.t FStar.Monotonic.DependentMap.opt FStar.HyperStack.ST.erid FStar.Monotonic.DependentMap.t FStar.Monotonic.HyperStack.mem Prims.l_not FStar.Monotonic.DependentMap.defined
(*
   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.Monotonic.DependentMap
(** A library for mutable partial, dependent maps,
    that grow monotonically,
    while subject to an invariant on the entire map *)
open FStar.HyperStack.ST

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

/// The logical model of the map is given in terms of DM.t///
let opt (#a:eqtype) (b:a -> Type) = fun (x:a) -> option (b x)
let partial_dependent_map (a:eqtype) (b:a -> Type) =
    DM.t a (opt b)

/// An empty partial, dependent map maps all keys to None
let empty_partial_dependent_map (#a:_) (#b:_)
  : partial_dependent_map a b
  = DM.create #a #(opt b) (fun x -> None)
////////////////////////////////////////////////////////////////////////////////

/// `map a b`: Internally, the model is implemented using this abstract type
///    These maps provide three operations:
///      - empty, sel, upd
///    Which are proven to be in correspondence with the operations on DM.t
///    via the homomorphism `repr` below
val map
    (a:eqtype)
    (b:(a -> Type u#b))
  : Type u#b

/// `repr m`: A ghost function that reveals the internal `map` as a `DM.t`
val repr (#a:_) (#b:_)
    (r:map a b)
  : GTot (partial_dependent_map a b)

/// An `empty : map a b` is equivalent to the `empty_partial_dependent_map`
val empty (#a:_) (#b:_)
  : r:map a b{repr r == empty_partial_dependent_map}

/// Selecting a key from a map `sel r x` is equivalent to selecting it from its `repr`
val sel (#a:_) (#b:_)
    (r:map a b)
    (x:a)
  : Pure (option (b x))
    (requires True)
    (ensures (fun o -> DM.sel (repr r) x == o))

/// Updating a map using `upd r x v` is equivalent to updating its repr
val upd (#a:_) (#b:_)
    (r:map a b)
    (x:a)
    (v:b x)
  : Pure (map a b)
    (requires True)
    (ensures (fun r' -> repr r' == DM.upd (repr r) x (Some v)))

/// `imap a b inv` further augments a map with an invariant on its repr
let imap (a:eqtype) (b: a -> Type) (inv:DM.t a (opt b) -> Type) =
    r:map a b{inv (repr r)}

/// `grows r1 r2` is an abstract preorder on `imap`
val grows (#a:_) (#b:_) (#inv:DM.t a (opt b) -> Type)
  : FStar.Preorder.preorder (imap a b inv)

/// And, finally, the main type of this module:
///
/// `t r a b inv` is a mutable, imap stored in region `r` constrained
///               to evolve according to `grows`
let t (r:HST.erid) (a:eqtype) (b:a -> Type) (inv:DM.t a (opt b) -> Type) =
    m_rref r (imap a b inv) grows

/// `defined t x h`: In state `h`, map `t` is defined at point `x`.
///     - We define these in `Type` rather than `bool`
///       since it is typical for client code to use `defined`
///       as a stable heap predicate, which requires a `heap -> Type`
let defined
    (#a:eqtype)
    (#b:a -> Type)
    (#inv:DM.t a (opt b) -> Type)
    (#r:HST.erid)
    (t:t r a b inv)
    (x:a)
    (h:HS.mem)
  : GTot Type
  = Some? (sel (HS.sel h t) x)

/// `fresh t x h`: The map is not defined at point `x`
let fresh
    (#a:eqtype)
    (#b:a -> Type)
    (#inv:DM.t a (opt b) -> Type)
    (#r:HST.erid)
    (t:t r a b inv)
    (x:a)
    (h:HS.mem)
val fresh
      (#a: eqtype)
      (#b: (a -> Type))
      (#inv: (DM.t a (opt b) -> Type))
      (#r: HST.erid)
      (t: t r a b inv)
      (x: a)
      (h: HS.mem)
    : GTot Type0
t: FStar.Monotonic.DependentMap.t r a b inv -> x: a -> h: FStar.Monotonic.HyperStack.mem
  -> Prims.GTot Type0