val interp_as_wp (#a: _) (t: rwtree a) : st_wp a
val interp_as_wp (#a: _) (t: rwtree a) : st_wp a
let rec interp_as_wp #a (t : rwtree a) : st_wp a =
  match t with
  | Return x -> return_wp x
  | Op Read _ k ->
    bind_wp read_wp (fun s -> interp_as_wp (k s))
  | Op Write s k ->
    bind_wp (write_wp s) (fun (o:unit) -> interp_as_wp (k o))
module AlgForAll

open FStar.Calc
module FE = FStar.FunctionalExtensionality
module F = FStar.FunctionalExtensionality
module W = FStar.WellFounded
module T = FStar.Tactics.V2
module ID5 = ID5
open Alg

type rwtree a = Alg.tree a [Read; Write]
let tbind : #a:_ -> #b:_ -> rwtree a -> (a -> rwtree b) -> rwtree b = fun c f -> Alg.bind _ _ c f

let st_wp0 (a:Type) : Type = state -> (a & state -> Type0) -> Type0

let st_monotonic #a (w : st_wp0 a) : Type0 =
  //forall s0 p1 p2. (forall r. p1 r ==> p2 r) ==> w s0 p1 ==> w s0 p2
  // ^ this version seems to be less SMT-friendly
  forall s0 p1 p2. (forall x s1. p1 (x, s1) ==> p2 (x, s1)) ==> w s0 p1 ==> w s0 p2

let st_wp (a:Type) = wp:st_wp0 a{st_monotonic wp}

unfold
let return_wp #a x : st_wp a = fun s0 p -> p (x, s0)

unfold
let bind_wp #a #b (w : st_wp a) (wf : a -> st_wp b)
  : st_wp b
  = fun s0 p -> w s0 (fun (y, s1) -> wf y s1 p)

unfold
let read_wp : st_wp state = fun s0 p -> p (s0, s0)

unfold
let write_wp : state -> st_wp unit = fun s _ p -> p ((), s)
/
prims.fst.checked ID5.fst.checked FStar.WellFounded.fst.checked FStar.Tactics.V2.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.Pure.fst.checked FStar.FunctionalExtensionality.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked Alg.fst.checked
AlgForAll.fst
t: AlgForAll.rwtree a -> AlgForAll.st_wp a
AlgForAll.rwtree AlgForAll.return_wp Alg.op_inp Alg.Read Alg.op_out Alg.tree0 AlgForAll.bind_wp Alg.state AlgForAll.read_wp AlgForAll.interp_as_wp AlgForAll.st_wp Alg.Write Prims.unit AlgForAll.write_wp
let rec interp_as_wp #a (t: rwtree a) : st_wp a =
  
match t with
| Return x -> return_wp x
| Op Read _ k -> bind_wp read_wp (fun s -> interp_as_wp (k s))
| Op Write s k -> bind_wp (write_wp s) (fun (o: unit) -> interp_as_wp (k o))