-- Definitions for the protected memory monad:

--#include "Alfa/Tuples.alfa"

--#include "Monads.alfa"

--#include "MemMonads.alfa"

--#include "Alfa/Bool.alfa"

--#include "Alfa/MaybeProp.alfa"

package Protected where
  open Tuples  use  Pair,  Unit,  unit,  pair,  fst,  snd
  open Booleans  use  Bool,  if
  public open MaybeDefs  use  Maybe,  maybe
  open Monads  use  Monad,  return,  (>>=),  (>>),  liftM
  open MemMonads  use  MemMonad
  -- Environment+exception monad transformer:
  EnvEx (M::Set -> Set)(E::Set)(A::Set) :: Set
    = E -> M (Maybe A)
  inst (M::Set -> Set)(E::Set)(m::Monad M) :: Monad (EnvEx M E)
    = struct {
        unit = \(A::Set) -> \(x::A) -> \(e::E) -> m.unit (Maybe A) (Just@_ x);
        bind =
          \(A::Set) ->
          \(B::Set) ->
          \(m1::EnvEx M E A) ->
          \(xm2::(h'::A) -> EnvEx M E B) ->
          \(e::E) ->
          m.bind (Maybe A) (Maybe B) (m1 e) (maybe A (M (Maybe B)) (m.unit (Maybe B) Nothing@_) (\(a::A) -> xm2 a e));}
  Protect (M::Set -> Set)(A::Set) :: Set -> Set
    = EnvEx M (A -> Bool)
  protect (M::Set -> Set)(A::Set)(B::Set)(W::Set)(mm::MemMonad M A W)(a::A)(m::M B) :: Protect M A B
    = \(valid::(h::A) -> Bool) -> if (M (Maybe B)) (valid a) (liftM B (Maybe B) M mm.monad (\(b::B) -> Just@_ b) m) (mm.monad.unit (Maybe B) Nothing@_)
  -- Adding protection to a memory monad:
  mmprot (M::Set -> Set)(A::Set)(W::Set)(mm::MemMonad M A W) :: MemMonad (Protect M A) A W
    = struct {
        monad = inst M (A -> Bool) mm.monad;
        rd = \(a::A) -> protect M A W W mm a (mm.rd a);
        wr = \(a::A) -> \(w::W) -> protect M A Tuples.Unit W mm a (mm.wr a w);}
  runProtected (M::Set -> Set)(A::Set)(W::Set)(B::Set)(mm::MemMonad M A W)(b::B)(valid::A -> Bool)(m::Protect M A B) :: M B
    = liftM (Maybe B) B M mm.monad (maybe B B b (\(b::B) -> b)) (m valid)
{-# Alfa unfoldgoals off
brief on
hidetypeannots off
wide

nd
hiding on
var "maybe" hide 2
var "protect" hide 4
var "runProtected" hide 4
var "mmprot" hide 3
 #-}