val bind
      (a b: Type)
      (state: Type u#2)
      (rel: P.preorder state)
      (req_f: pre_t state)
      (ens_f: post_t state a)
      (req_g: (a -> pre_t state))
      (ens_g: (a -> post_t state b))
      (f: repr a state rel req_f ens_f)
      (g: (x: a -> repr b state rel (req_g x) (ens_g x)))
    : repr b
      state
      rel
      (fun s0 -> req_f s0 /\ (forall x s1. ens_f s0 x s1 ==> (req_g x) s1))
      (fun s0 r s2 -> req_f s0 /\ (exists x s1. ens_f s0 x s1 /\ (req_g x) s1 /\ (ens_g x) s1 r s2))
let bind
      (a:Type)
      (b:Type)
      (state:Type u#2)
      (rel:P.preorder state)
      (req_f:pre_t state)
      (ens_f:post_t state a)
      (req_g:a -> pre_t state)
      (ens_g:a -> post_t state b)
      (f:repr a state rel req_f ens_f)
      (g:(x:a -> repr b state rel (req_g x) (ens_g x)))
    : repr b state rel
      (fun s0 -> req_f s0 /\ (forall x s1. ens_f s0 x s1 ==> (req_g x) s1))
      (fun s0 r s2 -> req_f s0 /\ (exists x s1. ens_f s0 x s1 /\ (req_g x) s1 /\ (ens_g x) s1 r s2))
    =
  fun s0 ->
    let x, s1 = f s0 in
    (g x) s1
val bind
      (a b: Type)
      (state: Type u#2)
      (rel: P.preorder state)
      (req_f: pre_t state)
      (ens_f: post_t state a)
      (req_g: (a -> pre_t state))
      (ens_g: (a -> post_t state b))
      (f: repr a state rel req_f ens_f)
      (g: (x: a -> repr b state rel (req_g x) (ens_g x)))
    : repr b
      state
      rel
      (fun s0 -> req_f s0 /\ (forall x s1. ens_f s0 x s1 ==> (req_g x) s1))
      (fun s0 r s2 -> req_f s0 /\ (exists x s1. ens_f s0 x s1 /\ (req_g x) s1 /\ (ens_g x) s1 r s2))
let bind
      (a b: Type)
      (state: Type u#2)
      (rel: P.preorder state)
      (req_f: pre_t state)
      (ens_f: post_t state a)
      (req_g: (a -> pre_t state))
      (ens_g: (a -> post_t state b))
      (f: repr a state rel req_f ens_f)
      (g: (x: a -> repr b state rel (req_g x) (ens_g x)))
    : repr b
      state
      rel
      (fun s0 -> req_f s0 /\ (forall x s1. ens_f s0 x s1 ==> (req_g x) s1))
      (fun s0 r s2 -> req_f s0 /\ (exists x s1. ens_f s0 x s1 /\ (req_g x) s1 /\ (ens_g x) s1 r s2)) =
fun s0 ->
  let x, s1 = f s0 in
  (g x) s1
FStar.MST.fst.checked
prims.fst.checked FStar.Witnessed.Core.fsti.checked FStar.Preorder.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.MSTTotal.fst.checked FStar.Monotonic.Pure.fst.checked
FStar.MST.fst
FStar.Preorder.preorder FStar.MST.pre_t FStar.MST.post_t FStar.MST.repr FStar.Pervasives.Native.tuple2 Prims.l_and Prims.l_Forall Prims.l_imp Prims.l_Exists
(*
   Copyright 2020 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.MST

module P = FStar.Preorder
module W = FStar.Witnessed.Core
open FStar.Monotonic.Pure

type pre_t (state:Type u#2) = state -> Type0
type post_t (state:Type u#2) (a:Type u#a) = state -> a -> state -> Type0

type repr
      (a:Type)
      (state:Type u#2)
      (rel:P.preorder state)
      (req:pre_t state)
      (ens:post_t state a)
    =
  s0:state ->
  DIV (a & state)
    (as_pure_wp (fun p ->
                        req s0 /\
                        (forall (x:a) (s1:state). (ens s0 x s1 /\ rel s0 s1) ==> p (x, s1))))

let return
      (a:Type)
      (x:a)
      (state:Type u#2)
      (rel:P.preorder state)
    : repr a state rel
      (fun _ -> True)
      (fun s0 r s1 -> r == x /\ s0 == s1)
    =
  fun s0 -> x, s0

let bind
      (a:Type)
      (b:Type)
      (state:Type u#2)
      (rel:P.preorder state)
      (req_f:pre_t state)
      (ens_f:post_t state a)
      (req_g:a -> pre_t state)
      (ens_g:a -> post_t state b)
      (f:repr a state rel req_f ens_f)
      (g:(x:a -> repr b state rel (req_g x) (ens_g x)))
    : repr b state rel
      (fun s0 -> req_f s0 /\ (forall x s1. ens_f s0 x s1 ==> (req_g x) s1))
      (fun s0 r s2 -> req_f s0 /\ (exists x s1. ens_f s0 x s1 /\ (req_g x) s1 /\ (ens_g x) s1 r s2))
val bind
      (a b: Type)
      (state: Type u#2)
      (rel: P.preorder state)
      (req_f: pre_t state)
      (ens_f: post_t state a)
      (req_g: (a -> pre_t state))
      (ens_g: (a -> post_t state b))
      (f: repr a state rel req_f ens_f)
      (g: (x: a -> repr b state rel (req_g x) (ens_g x)))
    : repr b
      state
      rel
      (fun s0 -> req_f s0 /\ (forall x s1. ens_f s0 x s1 ==> (req_g x) s1))
      (fun s0 r s2 -> req_f s0 /\ (exists x s1. ens_f s0 x s1 /\ (req_g x) s1 /\ (ens_g x) s1 r s2))

    a: Type ->
    b: Type ->
    state: Type ->
    rel: FStar.Preorder.preorder state ->
    req_f: FStar.MST.pre_t state ->
    ens_f: FStar.MST.post_t state a ->
    req_g: (_: a -> FStar.MST.pre_t state) ->
    ens_g: (_: a -> FStar.MST.post_t state b) ->
    f: FStar.MST.repr a state rel req_f ens_f ->
    g: (x: a -> FStar.MST.repr b state rel (req_g x) (ens_g x))
  -> FStar.MST.repr b
      state
      rel
      (fun s0 -> req_f s0 /\ (forall (x: a) (s1: state). ens_f s0 x s1 ==> req_g x s1))
      (fun s0 r s2 ->
          req_f s0 /\ (exists (x: a) (s1: state). ens_f s0 x s1 /\ req_g x s1 /\ ens_g x s1 r s2))