val grows (#a:_) (#b:_) (#inv:DM.t a (opt b) -> Type)
  : FStar.Preorder.preorder (imap a b inv)
let grows #a #b #inv = grows' #a #b #inv
val grows (#a:_) (#b:_) (#inv:DM.t a (opt b) -> Type)
  : FStar.Preorder.preorder (imap a b inv)
let grows #a #b #inv =
grows' #a #b #inv
FStar.Monotonic.DependentMap.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.DependentMap.fsti.checked
FStar.Monotonic.DependentMap.fst
Prims.eqtype FStar.DependentMap.t FStar.Monotonic.DependentMap.opt FStar.Monotonic.DependentMap.grows' FStar.Preorder.preorder FStar.Monotonic.DependentMap.imap
(*
   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

/// `map a b`: Represent the partial map as a list of pairs of points
let map a b = list (x:a & b x)

/// `repr r`: Converts the list of pairs into a DM.t
let rec repr (#a:eqtype) (#b:a -> Type) (r:map a b)
    : GTot (partial_dependent_map a b)
    = match r with
      | [] -> empty_partial_dependent_map
      | (|x, y|)::tl -> DM.upd (repr tl) x (Some y)

/// Three basic operations on map: empty, sel upd
let empty #a #b = []

let rec sel #a #b r x =
    match r with
    | [] -> None
    | (|x', y|)::tl ->
      if x = x' then Some y else sel tl x

let upd #a #b r x v = (|x, v|)::r

////////////////////////////////////////////////////////////////////////////////

/// `grows'` and `grows`: a preorder of invariant-respecting maps
///    - Needs to be introduced in 2 steps because of an F* limitation
let grows' (#a:eqtype) (#b:a -> Type) (#inv:(partial_dependent_map a b -> Type))
           (m1:imap a b inv) (m2:imap a b inv) =
    forall x.{:pattern (Some? (sel m1 x))}
           Some? (sel m1 x) ==>
              Some? (sel m2 x) /\
val grows (#a:_) (#b:_) (#inv:DM.t a (opt b) -> Type)
  : FStar.Preorder.preorder (imap a b inv)
FStar.Preorder.preorder (FStar.Monotonic.DependentMap.imap a b inv)