{-# LANGUAGE CPP #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE UndecidableInstances #-}

module Language.Embedded.Concurrent.CMD (
    TID, ThreadId (..),
    CID, Chan (..),
    ChanSize (..),
    timesSizeOf, timesSize, plusSize,
    ThreadCMD (..),
    ChanCMD (..),
    Closeable, Uncloseable
  ) where



#if __GLASGOW_HASKELL__ < 710
import Control.Applicative
import Data.Typeable
#endif
import qualified Control.Chan as Chan
import qualified Control.Concurrent as CC
import Control.Monad.Operational.Higher
import Control.Monad.Reader
import Data.Dynamic
import Data.IORef
import Data.Ix (Ix)
import Data.Maybe (fromMaybe)

import Control.Monads
import Language.Embedded.Traversal
import Language.Embedded.Expression
import Language.Embedded.Imperative.CMD
import Language.Embedded.Imperative (getArr, setArr)



type TID = VarId
type CID = VarId

-- | A "flag" which may be waited upon. A flag starts of unset, and can be set
--   using 'setFlag'. Once set, the flag stays set forever.
data Flag a = Flag (IORef Bool) (CC.MVar a)

-- | Create a new, unset 'Flag'.
newFlag :: IO (Flag a)
newFlag :: IO (Flag a)
newFlag = IORef Bool -> MVar a -> Flag a
forall a. IORef Bool -> MVar a -> Flag a
Flag (IORef Bool -> MVar a -> Flag a)
-> IO (IORef Bool) -> IO (MVar a -> Flag a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> IO (IORef Bool)
forall a. a -> IO (IORef a)
newIORef Bool
False IO (MVar a -> Flag a) -> IO (MVar a) -> IO (Flag a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IO (MVar a)
forall a. IO (MVar a)
CC.newEmptyMVar

-- | Set a 'Flag'; guaranteed not to block.
--   If @setFlag@ is called on a flag which was already set, the value of said
--   flag is not updated.
--   @setFlag@ returns the status of the flag prior to the call: is the flag
--   was already set the return value is @True@, otherwise it is @False@.
setFlag :: Flag a -> a -> IO Bool
setFlag :: Flag a -> a -> IO Bool
setFlag (Flag IORef Bool
flag MVar a
var) a
val = do
  Bool
set <- IORef Bool -> (Bool -> (Bool, Bool)) -> IO Bool
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef IORef Bool
flag ((Bool -> (Bool, Bool)) -> IO Bool)
-> (Bool -> (Bool, Bool)) -> IO Bool
forall a b. (a -> b) -> a -> b
$ \Bool
set -> (Bool
True, Bool
set)
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
set) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ MVar a -> a -> IO ()
forall a. MVar a -> a -> IO ()
CC.putMVar MVar a
var a
val
  Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
set

-- | Wait until the given flag becomes set, then return its value. If the flag
--   is already set, return the value immediately.
waitFlag :: Flag a -> IO a
waitFlag :: Flag a -> IO a
waitFlag (Flag IORef Bool
_ MVar a
var) = MVar a -> (a -> IO a) -> IO a
forall a b. MVar a -> (a -> IO b) -> IO b
CC.withMVar MVar a
var a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return

data ThreadId
  = TIDRun CC.ThreadId (Flag ())
  | TIDComp TID
    deriving (Typeable)

instance Show ThreadId where
  show :: ThreadId -> String
show (TIDRun ThreadId
tid Flag ()
_) = ThreadId -> String
forall a. Show a => a -> String
show ThreadId
tid
  show (TIDComp String
tid)  = String
tid

data Closeable
data Uncloseable

-- | A bounded channel.
data Chan t a
  = ChanRun (Chan.Chan Dynamic)
  | ChanComp CID

-- | Channel size specification. For each possible element type, it shows how
--   many elements of them could be stored in the given channel at once.
data ChanSize exp pred i where
  OneSize   :: (pred a, Integral i) => proxy a -> exp i -> ChanSize exp pred i
  TimesSize :: Integral i => exp i -> ChanSize exp pred i -> ChanSize exp pred i
  PlusSize  :: Integral i => ChanSize exp pred i -> ChanSize exp pred i -> ChanSize exp pred i

mapSizeExp :: (exp i -> exp' i) -> ChanSize exp pred i -> ChanSize exp' pred i
mapSizeExp :: (exp i -> exp' i) -> ChanSize exp pred i -> ChanSize exp' pred i
mapSizeExp exp i -> exp' i
f (OneSize proxy a
t exp i
sz) = proxy a -> exp' i -> ChanSize exp' pred i
forall k (pred :: k -> Constraint) (a :: k) i (proxy :: k -> *)
       (exp :: * -> *).
(pred a, Integral i) =>
proxy a -> exp i -> ChanSize exp pred i
OneSize proxy a
t (exp i -> exp' i
f exp i
sz)
mapSizeExp exp i -> exp' i
f (TimesSize exp i
n ChanSize exp pred i
sz) = exp' i -> ChanSize exp' pred i -> ChanSize exp' pred i
forall k i (exp :: * -> *) (pred :: k -> Constraint).
Integral i =>
exp i -> ChanSize exp pred i -> ChanSize exp pred i
TimesSize (exp i -> exp' i
f exp i
n) ((exp i -> exp' i) -> ChanSize exp pred i -> ChanSize exp' pred i
forall k (exp :: * -> *) i (exp' :: * -> *)
       (pred :: k -> Constraint).
(exp i -> exp' i) -> ChanSize exp pred i -> ChanSize exp' pred i
mapSizeExp exp i -> exp' i
f ChanSize exp pred i
sz)
mapSizeExp exp i -> exp' i
f (PlusSize ChanSize exp pred i
a ChanSize exp pred i
b) = ChanSize exp' pred i
-> ChanSize exp' pred i -> ChanSize exp' pred i
forall k i (exp :: * -> *) (pred :: k -> Constraint).
Integral i =>
ChanSize exp pred i -> ChanSize exp pred i -> ChanSize exp pred i
PlusSize ((exp i -> exp' i) -> ChanSize exp pred i -> ChanSize exp' pred i
forall k (exp :: * -> *) i (exp' :: * -> *)
       (pred :: k -> Constraint).
(exp i -> exp' i) -> ChanSize exp pred i -> ChanSize exp' pred i
mapSizeExp exp i -> exp' i
f ChanSize exp pred i
a) ((exp i -> exp' i) -> ChanSize exp pred i -> ChanSize exp' pred i
forall k (exp :: * -> *) i (exp' :: * -> *)
       (pred :: k -> Constraint).
(exp i -> exp' i) -> ChanSize exp pred i -> ChanSize exp' pred i
mapSizeExp exp i -> exp' i
f ChanSize exp pred i
b)

mapSizeExpA :: (Functor m, Monad m)
            => (exp i -> m (exp' i))
            -> ChanSize exp pred i
            -> m (ChanSize exp' pred i)
mapSizeExpA :: (exp i -> m (exp' i))
-> ChanSize exp pred i -> m (ChanSize exp' pred i)
mapSizeExpA exp i -> m (exp' i)
f (OneSize proxy a
t exp i
sz) = proxy a -> exp' i -> ChanSize exp' pred i
forall k (pred :: k -> Constraint) (a :: k) i (proxy :: k -> *)
       (exp :: * -> *).
(pred a, Integral i) =>
proxy a -> exp i -> ChanSize exp pred i
OneSize proxy a
t (exp' i -> ChanSize exp' pred i)
-> m (exp' i) -> m (ChanSize exp' pred i)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> exp i -> m (exp' i)
f exp i
sz
mapSizeExpA exp i -> m (exp' i)
f (TimesSize exp i
n ChanSize exp pred i
sz) = do
  exp' i
n' <- exp i -> m (exp' i)
f exp i
n
  ChanSize exp' pred i
sz' <- (exp i -> m (exp' i))
-> ChanSize exp pred i -> m (ChanSize exp' pred i)
forall k (m :: * -> *) (exp :: * -> *) i (exp' :: * -> *)
       (pred :: k -> Constraint).
(Functor m, Monad m) =>
(exp i -> m (exp' i))
-> ChanSize exp pred i -> m (ChanSize exp' pred i)
mapSizeExpA exp i -> m (exp' i)
f ChanSize exp pred i
sz
  ChanSize exp' pred i -> m (ChanSize exp' pred i)
forall (m :: * -> *) a. Monad m => a -> m a
return (ChanSize exp' pred i -> m (ChanSize exp' pred i))
-> ChanSize exp' pred i -> m (ChanSize exp' pred i)
forall a b. (a -> b) -> a -> b
$ exp' i -> ChanSize exp' pred i -> ChanSize exp' pred i
forall k i (exp :: * -> *) (pred :: k -> Constraint).
Integral i =>
exp i -> ChanSize exp pred i -> ChanSize exp pred i
TimesSize exp' i
n' ChanSize exp' pred i
sz'
mapSizeExpA exp i -> m (exp' i)
f (PlusSize ChanSize exp pred i
a ChanSize exp pred i
b) = do
  ChanSize exp' pred i
a' <- (exp i -> m (exp' i))
-> ChanSize exp pred i -> m (ChanSize exp' pred i)
forall k (m :: * -> *) (exp :: * -> *) i (exp' :: * -> *)
       (pred :: k -> Constraint).
(Functor m, Monad m) =>
(exp i -> m (exp' i))
-> ChanSize exp pred i -> m (ChanSize exp' pred i)
mapSizeExpA exp i -> m (exp' i)
f ChanSize exp pred i
a
  ChanSize exp' pred i
b' <- (exp i -> m (exp' i))
-> ChanSize exp pred i -> m (ChanSize exp' pred i)
forall k (m :: * -> *) (exp :: * -> *) i (exp' :: * -> *)
       (pred :: k -> Constraint).
(Functor m, Monad m) =>
(exp i -> m (exp' i))
-> ChanSize exp pred i -> m (ChanSize exp' pred i)
mapSizeExpA exp i -> m (exp' i)
f ChanSize exp pred i
b
  ChanSize exp' pred i -> m (ChanSize exp' pred i)
forall (m :: * -> *) a. Monad m => a -> m a
return (ChanSize exp' pred i -> m (ChanSize exp' pred i))
-> ChanSize exp' pred i -> m (ChanSize exp' pred i)
forall a b. (a -> b) -> a -> b
$ ChanSize exp' pred i
-> ChanSize exp' pred i -> ChanSize exp' pred i
forall k i (exp :: * -> *) (pred :: k -> Constraint).
Integral i =>
ChanSize exp pred i -> ChanSize exp pred i -> ChanSize exp pred i
PlusSize ChanSize exp' pred i
a' ChanSize exp' pred i
b'

-- | Takes 'n' times the size of type refered by proxy.
timesSizeOf :: (pred a, Integral i) => exp i -> proxy a -> ChanSize exp pred i
timesSizeOf :: exp i -> proxy a -> ChanSize exp pred i
timesSizeOf = (proxy a -> exp i -> ChanSize exp pred i)
-> exp i -> proxy a -> ChanSize exp pred i
forall a b c. (a -> b -> c) -> b -> a -> c
flip proxy a -> exp i -> ChanSize exp pred i
forall k (pred :: k -> Constraint) (a :: k) i (proxy :: k -> *)
       (exp :: * -> *).
(pred a, Integral i) =>
proxy a -> exp i -> ChanSize exp pred i
OneSize

-- | Multiplies a channel size specification with a scalar.
timesSize :: Integral i => exp i -> ChanSize exp pred i -> ChanSize exp pred i
timesSize :: exp i -> ChanSize exp pred i -> ChanSize exp pred i
timesSize = exp i -> ChanSize exp pred i -> ChanSize exp pred i
forall k i (exp :: * -> *) (pred :: k -> Constraint).
Integral i =>
exp i -> ChanSize exp pred i -> ChanSize exp pred i
TimesSize

-- | Adds two channel size specifications together.
plusSize :: Integral i => ChanSize exp pred i -> ChanSize exp pred i -> ChanSize exp pred i
plusSize :: ChanSize exp pred i -> ChanSize exp pred i -> ChanSize exp pred i
plusSize = ChanSize exp pred i -> ChanSize exp pred i -> ChanSize exp pred i
forall k i (exp :: * -> *) (pred :: k -> Constraint).
Integral i =>
ChanSize exp pred i -> ChanSize exp pred i -> ChanSize exp pred i
PlusSize

data ThreadCMD fs a where
  ForkWithId :: (ThreadId -> prog ()) -> ThreadCMD (Param3 prog exp pred) ThreadId
  Kill       :: ThreadId -> ThreadCMD (Param3 prog exp pred) ()
  Wait       :: ThreadId -> ThreadCMD (Param3 prog exp pred) ()
  Sleep      :: Integral i => exp i -> ThreadCMD (Param3 prog exp pred) ()

data ChanCMD fs a where
  NewChan   :: ChanSize exp pred i -> ChanCMD (Param3 prog exp pred) (Chan t c)
  CloseChan :: Chan Closeable c -> ChanCMD (Param3 prog exp pred) ()
  ReadOK    :: Chan Closeable c -> ChanCMD (Param3 prog exp pred) (Val Bool)

  ReadOne   :: (Typeable a, pred a)
            => Chan t c -> ChanCMD (Param3 prog exp pred) (Val a)
  WriteOne  :: (Typeable a, pred a)
            => Chan t c -> exp a -> ChanCMD (Param3 prog exp pred) (Val Bool)

  ReadChan  :: (Typeable a, pred a, pred i, Ix i, Integral i)
            => Chan t c -> exp i -> exp i
            -> Arr i a -> ChanCMD (Param3 prog exp pred) (Val Bool)
  WriteChan :: (Typeable a, pred a, pred i, Ix i, Integral i)
            => Chan t c -> exp i -> exp i
            -> Arr i a -> ChanCMD (Param3 prog exp pred) (Val Bool)

instance HFunctor ThreadCMD where
  hfmap :: (forall b. f b -> g b)
-> ThreadCMD '(f, fs) a -> ThreadCMD '(g, fs) a
hfmap forall b. f b -> g b
f (ForkWithId ThreadId -> prog ()
p) = (ThreadId -> g ()) -> ThreadCMD (Param3 g exp pred) ThreadId
forall k2 (prog :: * -> *) (exp :: * -> *) (pred :: k2).
(ThreadId -> prog ()) -> ThreadCMD (Param3 prog exp pred) ThreadId
ForkWithId ((ThreadId -> g ()) -> ThreadCMD (Param3 g exp pred) ThreadId)
-> (ThreadId -> g ()) -> ThreadCMD (Param3 g exp pred) ThreadId
forall a b. (a -> b) -> a -> b
$ f () -> g ()
forall b. f b -> g b
f (f () -> g ()) -> (ThreadId -> f ()) -> ThreadId -> g ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThreadId -> f ()
ThreadId -> prog ()
p
  hfmap forall b. f b -> g b
_ (Kill ThreadId
tid)     = ThreadId -> ThreadCMD (Param3 g exp pred) ()
forall k2 (prog :: * -> *) (exp :: * -> *) (pred :: k2).
ThreadId -> ThreadCMD (Param3 prog exp pred) ()
Kill ThreadId
tid
  hfmap forall b. f b -> g b
_ (Wait ThreadId
tid)     = ThreadId -> ThreadCMD (Param3 g exp pred) ()
forall k2 (prog :: * -> *) (exp :: * -> *) (pred :: k2).
ThreadId -> ThreadCMD (Param3 prog exp pred) ()
Wait ThreadId
tid
  hfmap forall b. f b -> g b
_ (Sleep exp i
tid)    = exp i -> ThreadCMD (Param3 g exp pred) ()
forall k2 i (exp :: * -> *) (prog :: * -> *) (pred :: k2).
Integral i =>
exp i -> ThreadCMD (Param3 prog exp pred) ()
Sleep exp i
tid

instance HBifunctor ThreadCMD where
  hbimap :: (forall b. f b -> g b)
-> (forall b. i b -> j b)
-> ThreadCMD '(f, '(i, fs)) a
-> ThreadCMD '(g, '(j, fs)) a
hbimap forall b. f b -> g b
f forall b. i b -> j b
_ (ForkWithId ThreadId -> prog ()
p) = (ThreadId -> g ()) -> ThreadCMD (Param3 g j pred) ThreadId
forall k2 (prog :: * -> *) (exp :: * -> *) (pred :: k2).
(ThreadId -> prog ()) -> ThreadCMD (Param3 prog exp pred) ThreadId
ForkWithId ((ThreadId -> g ()) -> ThreadCMD (Param3 g j pred) ThreadId)
-> (ThreadId -> g ()) -> ThreadCMD (Param3 g j pred) ThreadId
forall a b. (a -> b) -> a -> b
$ f () -> g ()
forall b. f b -> g b
f (f () -> g ()) -> (ThreadId -> f ()) -> ThreadId -> g ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThreadId -> f ()
ThreadId -> prog ()
p
  hbimap forall b. f b -> g b
_ forall b. i b -> j b
_ (Kill ThreadId
tid)     = ThreadId -> ThreadCMD (Param3 g j pred) ()
forall k2 (prog :: * -> *) (exp :: * -> *) (pred :: k2).
ThreadId -> ThreadCMD (Param3 prog exp pred) ()
Kill ThreadId
tid
  hbimap forall b. f b -> g b
_ forall b. i b -> j b
_ (Wait ThreadId
tid)     = ThreadId -> ThreadCMD (Param3 g j pred) ()
forall k2 (prog :: * -> *) (exp :: * -> *) (pred :: k2).
ThreadId -> ThreadCMD (Param3 prog exp pred) ()
Wait ThreadId
tid
  hbimap forall b. f b -> g b
_ forall b. i b -> j b
g (Sleep exp i
us)     = j i -> ThreadCMD (Param3 g j pred) ()
forall k2 i (exp :: * -> *) (prog :: * -> *) (pred :: k2).
Integral i =>
exp i -> ThreadCMD (Param3 prog exp pred) ()
Sleep (j i -> ThreadCMD (Param3 g j pred) ())
-> j i -> ThreadCMD (Param3 g j pred) ()
forall a b. (a -> b) -> a -> b
$ i i -> j i
forall b. i b -> j b
g i i
exp i
us

instance DryInterp ThreadCMD where
  dryInterp :: ThreadCMD '(m, fs) a -> m a
dryInterp (ForkWithId ThreadId -> prog ()
_) = (String -> ThreadId) -> m String -> m ThreadId
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM String -> ThreadId
TIDComp (m String -> m ThreadId) -> m String -> m ThreadId
forall a b. (a -> b) -> a -> b
$ String -> m String
forall (m :: * -> *). MonadSupply m => String -> m String
freshStr String
"t"
  dryInterp (Kill ThreadId
_)       = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  dryInterp (Wait ThreadId
_)       = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  dryInterp (Sleep exp i
_)      = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

instance (ThreadCMD :<: instr) => Reexpressible ThreadCMD instr env where
  reexpressInstrEnv :: (forall b.
 exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b))
-> ThreadCMD
     '(ReaderT env (ProgramT instr '(exp2, fs) m), '(exp1, fs)) a
-> ReaderT env (ProgramT instr '(exp2, fs) m) a
reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (ForkWithId ThreadId -> prog ()
p) = (env -> ProgramT instr (Param2 exp2 pred) m ThreadId)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ThreadId
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((env -> ProgramT instr (Param2 exp2 pred) m ThreadId)
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ThreadId)
-> (env -> ProgramT instr (Param2 exp2 pred) m ThreadId)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ThreadId
forall a b. (a -> b) -> a -> b
$ \env
env ->
      ThreadCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ThreadId
-> ProgramT instr (Param2 exp2 pred) m ThreadId
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (ThreadCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ThreadId
 -> ProgramT instr (Param2 exp2 pred) m ThreadId)
-> ThreadCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ThreadId
-> ProgramT instr (Param2 exp2 pred) m ThreadId
forall a b. (a -> b) -> a -> b
$ (ThreadId -> ProgramT instr (Param2 exp2 pred) m ())
-> ThreadCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ThreadId
forall k2 (prog :: * -> *) (exp :: * -> *) (pred :: k2).
(ThreadId -> prog ()) -> ThreadCMD (Param3 prog exp pred) ThreadId
ForkWithId ((ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
 -> env -> ProgramT instr (Param2 exp2 pred) m ())
-> env
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
-> env -> ProgramT instr (Param2 exp2 pred) m ()
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT env
env (ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
 -> ProgramT instr (Param2 exp2 pred) m ())
-> (ThreadId
    -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ThreadId
-> ProgramT instr (Param2 exp2 pred) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThreadId -> prog ()
ThreadId -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
p)
  reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (Kill ThreadId
tid) = ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m ()
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall a b. (a -> b) -> a -> b
$ ThreadCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (ThreadCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
 -> ProgramT instr (Param2 exp2 pred) m ())
-> ThreadCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall a b. (a -> b) -> a -> b
$ ThreadId
-> ThreadCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall k2 (prog :: * -> *) (exp :: * -> *) (pred :: k2).
ThreadId -> ThreadCMD (Param3 prog exp pred) ()
Kill ThreadId
tid
  reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (Wait ThreadId
tid) = ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m ()
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall a b. (a -> b) -> a -> b
$ ThreadCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (ThreadCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
 -> ProgramT instr (Param2 exp2 pred) m ())
-> ThreadCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall a b. (a -> b) -> a -> b
$ ThreadId
-> ThreadCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall k2 (prog :: * -> *) (exp :: * -> *) (pred :: k2).
ThreadId -> ThreadCMD (Param3 prog exp pred) ()
Wait ThreadId
tid
  reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (Sleep exp i
us) = (ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m ()
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> (exp2 i -> ProgramT instr (Param2 exp2 pred) m ())
-> exp2 i
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThreadCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (ThreadCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
 -> ProgramT instr (Param2 exp2 pred) m ())
-> (exp2 i
    -> ThreadCMD
         '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ())
-> exp2 i
-> ProgramT instr (Param2 exp2 pred) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. exp2 i
-> ThreadCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall k2 i (exp :: * -> *) (prog :: * -> *) (pred :: k2).
Integral i =>
exp i -> ThreadCMD (Param3 prog exp pred) ()
Sleep) (exp2 i -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (exp2 i)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< exp1 i -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 i)
forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp exp1 i
exp i
us

instance HFunctor ChanCMD where
  hfmap :: (forall (b :: k). f b -> g b)
-> ChanCMD '(f, fs) a -> ChanCMD '(g, fs) a
hfmap forall (b :: k). f b -> g b
_ (NewChan ChanSize exp pred i
sz)        = ChanSize exp pred i -> ChanCMD (Param3 g exp pred) (Chan t c)
forall k k k (exp :: * -> *) (pred :: * -> Constraint) i
       (prog :: k) (t :: k) (c :: k).
ChanSize exp pred i -> ChanCMD (Param3 prog exp pred) (Chan t c)
NewChan ChanSize exp pred i
sz
  hfmap forall (b :: k). f b -> g b
_ (ReadOne Chan t c
c)         = Chan t c -> ChanCMD (Param3 g exp pred) (Val a)
forall k k k a (pred :: * -> Constraint) (t :: k) (a :: k)
       (pred :: k) (t :: * -> *).
(Typeable a, pred a) =>
Chan t a -> ChanCMD (Param3 pred t pred) (Val a)
ReadOne Chan t c
c
  hfmap forall (b :: k). f b -> g b
_ (ReadChan Chan t c
c exp i
f exp i
t Arr i a
a)  = Chan t c
-> exp i
-> exp i
-> Arr i a
-> ChanCMD (Param3 g exp pred) (Val Bool)
forall k k k c (exp :: * -> Constraint) prog (t :: k) (c :: k)
       (exp :: * -> *) (prog :: k).
(Typeable c, exp c, exp prog, Ix prog, Integral prog) =>
Chan t c
-> exp prog
-> exp prog
-> Arr prog c
-> ChanCMD (Param3 prog exp exp) (Val Bool)
ReadChan Chan t c
c exp i
f exp i
t Arr i a
a
  hfmap forall (b :: k). f b -> g b
_ (WriteOne Chan t c
c exp a
x)      = Chan t c -> exp a -> ChanCMD (Param3 g exp pred) (Val Bool)
forall k k k a (pred :: * -> Constraint) (t :: k) (c :: k)
       (exp :: * -> *) (prog :: k).
(Typeable a, pred a) =>
Chan t c -> exp a -> ChanCMD (Param3 prog exp pred) (Val Bool)
WriteOne Chan t c
c exp a
x
  hfmap forall (b :: k). f b -> g b
_ (WriteChan Chan t c
c exp i
f exp i
t Arr i a
a) = Chan t c
-> exp i
-> exp i
-> Arr i a
-> ChanCMD (Param3 g exp pred) (Val Bool)
forall k k k c (exp :: * -> Constraint) prog (t :: k) (c :: k)
       (exp :: * -> *) (prog :: k).
(Typeable c, exp c, exp prog, Ix prog, Integral prog) =>
Chan t c
-> exp prog
-> exp prog
-> Arr prog c
-> ChanCMD (Param3 prog exp exp) (Val Bool)
WriteChan Chan t c
c exp i
f exp i
t Arr i a
a
  hfmap forall (b :: k). f b -> g b
_ (CloseChan Chan Closeable c
c)       = Chan Closeable c -> ChanCMD (Param3 g exp pred) ()
forall k k (c :: k) (prog :: k) (c :: * -> *)
       (prog :: * -> Constraint).
Chan Closeable c -> ChanCMD (Param3 prog c prog) ()
CloseChan Chan Closeable c
c
  hfmap forall (b :: k). f b -> g b
_ (ReadOK Chan Closeable c
c)          = Chan Closeable c -> ChanCMD (Param3 g exp pred) (Val Bool)
forall k k (c :: k) (prog :: k) (exp :: * -> *)
       (pred :: * -> Constraint).
Chan Closeable c -> ChanCMD (Param3 prog exp pred) (Val Bool)
ReadOK Chan Closeable c
c

instance HBifunctor ChanCMD where
  hbimap :: (forall b. f b -> g b)
-> (forall b. i b -> j b)
-> ChanCMD '(f, '(i, fs)) a
-> ChanCMD '(g, '(j, fs)) a
hbimap forall b. f b -> g b
_ forall b. i b -> j b
f (NewChan ChanSize exp pred i
sz)         = ChanSize j pred i -> ChanCMD (Param3 g j pred) (Chan t c)
forall k k k (exp :: * -> *) (pred :: * -> Constraint) i
       (prog :: k) (t :: k) (c :: k).
ChanSize exp pred i -> ChanCMD (Param3 prog exp pred) (Chan t c)
NewChan ((i i -> j i) -> ChanSize i pred i -> ChanSize j pred i
forall k (exp :: * -> *) i (exp' :: * -> *)
       (pred :: k -> Constraint).
(exp i -> exp' i) -> ChanSize exp pred i -> ChanSize exp' pred i
mapSizeExp i i -> j i
forall b. i b -> j b
f ChanSize i pred i
ChanSize exp pred i
sz)
  hbimap forall b. f b -> g b
_ forall b. i b -> j b
_ (ReadOne Chan t c
c)          = Chan t c -> ChanCMD (Param3 g j pred) (Val a)
forall k k k a (pred :: * -> Constraint) (t :: k) (a :: k)
       (pred :: k) (t :: * -> *).
(Typeable a, pred a) =>
Chan t a -> ChanCMD (Param3 pred t pred) (Val a)
ReadOne Chan t c
c
  hbimap forall b. f b -> g b
_ forall b. i b -> j b
f (ReadChan Chan t c
c exp i
n exp i
n' Arr i a
a)  = Chan t c
-> j i -> j i -> Arr i a -> ChanCMD (Param3 g j pred) (Val Bool)
forall k k k c (exp :: * -> Constraint) prog (t :: k) (c :: k)
       (exp :: * -> *) (prog :: k).
(Typeable c, exp c, exp prog, Ix prog, Integral prog) =>
Chan t c
-> exp prog
-> exp prog
-> Arr prog c
-> ChanCMD (Param3 prog exp exp) (Val Bool)
ReadChan Chan t c
c (i i -> j i
forall b. i b -> j b
f i i
exp i
n) (i i -> j i
forall b. i b -> j b
f i i
exp i
n') Arr i a
a
  hbimap forall b. f b -> g b
_ forall b. i b -> j b
f (WriteOne Chan t c
c exp a
x)       = Chan t c -> j a -> ChanCMD (Param3 g j pred) (Val Bool)
forall k k k a (pred :: * -> Constraint) (t :: k) (c :: k)
       (exp :: * -> *) (prog :: k).
(Typeable a, pred a) =>
Chan t c -> exp a -> ChanCMD (Param3 prog exp pred) (Val Bool)
WriteOne Chan t c
c (i a -> j a
forall b. i b -> j b
f i a
exp a
x)
  hbimap forall b. f b -> g b
_ forall b. i b -> j b
f (WriteChan Chan t c
c exp i
n exp i
n' Arr i a
a) = Chan t c
-> j i -> j i -> Arr i a -> ChanCMD (Param3 g j pred) (Val Bool)
forall k k k c (exp :: * -> Constraint) prog (t :: k) (c :: k)
       (exp :: * -> *) (prog :: k).
(Typeable c, exp c, exp prog, Ix prog, Integral prog) =>
Chan t c
-> exp prog
-> exp prog
-> Arr prog c
-> ChanCMD (Param3 prog exp exp) (Val Bool)
WriteChan Chan t c
c (i i -> j i
forall b. i b -> j b
f i i
exp i
n) (i i -> j i
forall b. i b -> j b
f i i
exp i
n') Arr i a
a
  hbimap forall b. f b -> g b
_ forall b. i b -> j b
_ (CloseChan Chan Closeable c
c    )    = Chan Closeable c -> ChanCMD (Param3 g j pred) ()
forall k k (c :: k) (prog :: k) (c :: * -> *)
       (prog :: * -> Constraint).
Chan Closeable c -> ChanCMD (Param3 prog c prog) ()
CloseChan Chan Closeable c
c
  hbimap forall b. f b -> g b
_ forall b. i b -> j b
_ (ReadOK Chan Closeable c
c)           = Chan Closeable c -> ChanCMD (Param3 g j pred) (Val Bool)
forall k k (c :: k) (prog :: k) (exp :: * -> *)
       (pred :: * -> Constraint).
Chan Closeable c -> ChanCMD (Param3 prog exp pred) (Val Bool)
ReadOK Chan Closeable c
c

instance DryInterp ChanCMD where
  dryInterp :: ChanCMD '(m, fs) a -> m a
dryInterp (NewChan ChanSize exp pred i
_)         = (String -> Chan t c) -> m String -> m (Chan t c)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM String -> Chan t c
forall k k (t :: k) (a :: k). String -> Chan t a
ChanComp (m String -> m (Chan t c)) -> m String -> m (Chan t c)
forall a b. (a -> b) -> a -> b
$ String -> m String
forall (m :: * -> *). MonadSupply m => String -> m String
freshStr String
"chan"
  dryInterp (ReadOne Chan t c
_)         = (String -> Val a) -> m String -> m (Val a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM String -> Val a
forall a. String -> Val a
ValComp (m String -> m (Val a)) -> m String -> m (Val a)
forall a b. (a -> b) -> a -> b
$ String -> m String
forall (m :: * -> *). MonadSupply m => String -> m String
freshStr String
"v"
  dryInterp (ReadChan Chan t c
_ exp i
_ exp i
_ Arr i a
_)  = (String -> Val Bool) -> m String -> m (Val Bool)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM String -> Val Bool
forall a. String -> Val a
ValComp (m String -> m (Val Bool)) -> m String -> m (Val Bool)
forall a b. (a -> b) -> a -> b
$ String -> m String
forall (m :: * -> *). MonadSupply m => String -> m String
freshStr String
"v"
  dryInterp (WriteOne Chan t c
_ exp a
_)      = (String -> Val Bool) -> m String -> m (Val Bool)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM String -> Val Bool
forall a. String -> Val a
ValComp (m String -> m (Val Bool)) -> m String -> m (Val Bool)
forall a b. (a -> b) -> a -> b
$ String -> m String
forall (m :: * -> *). MonadSupply m => String -> m String
freshStr String
"v"
  dryInterp (WriteChan Chan t c
_ exp i
_ exp i
_ Arr i a
_) = (String -> Val Bool) -> m String -> m (Val Bool)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM String -> Val Bool
forall a. String -> Val a
ValComp (m String -> m (Val Bool)) -> m String -> m (Val Bool)
forall a b. (a -> b) -> a -> b
$ String -> m String
forall (m :: * -> *). MonadSupply m => String -> m String
freshStr String
"v"
  dryInterp (CloseChan Chan Closeable c
_)       = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  dryInterp (ReadOK Chan Closeable c
_)          = (String -> Val Bool) -> m String -> m (Val Bool)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM String -> Val Bool
forall a. String -> Val a
ValComp (m String -> m (Val Bool)) -> m String -> m (Val Bool)
forall a b. (a -> b) -> a -> b
$ String -> m String
forall (m :: * -> *). MonadSupply m => String -> m String
freshStr String
"v"

instance (ChanCMD :<: instr) => Reexpressible ChanCMD instr env where
  reexpressInstrEnv :: (forall b.
 exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b))
-> ChanCMD
     '(ReaderT env (ProgramT instr '(exp2, fs) m), '(exp1, fs)) a
-> ReaderT env (ProgramT instr '(exp2, fs) m) a
reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (NewChan ChanSize exp pred i
sz) =
      ProgramT instr (Param2 exp2 pred) m (Chan t c)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Chan t c)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m (Chan t c)
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Chan t c))
-> (ChanSize exp2 pred i
    -> ProgramT instr (Param2 exp2 pred) m (Chan t c))
-> ChanSize exp2 pred i
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Chan t c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChanCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Chan t c)
-> ProgramT instr (Param2 exp2 pred) m (Chan t c)
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (ChanCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Chan t c)
 -> ProgramT instr (Param2 exp2 pred) m (Chan t c))
-> (ChanSize exp2 pred i
    -> ChanCMD
         '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred)
         (Chan t c))
-> ChanSize exp2 pred i
-> ProgramT instr (Param2 exp2 pred) m (Chan t c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChanSize exp2 pred i
-> ChanCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Chan t c)
forall k k k (exp :: * -> *) (pred :: * -> Constraint) i
       (prog :: k) (t :: k) (c :: k).
ChanSize exp pred i -> ChanCMD (Param3 prog exp pred) (Chan t c)
NewChan (ChanSize exp2 pred i
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Chan t c))
-> ReaderT
     env (ProgramT instr (Param2 exp2 pred) m) (ChanSize exp2 pred i)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Chan t c)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (exp1 i -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 i))
-> ChanSize exp1 pred i
-> ReaderT
     env (ProgramT instr '(exp2, fs) m) (ChanSize exp2 pred i)
forall k (m :: * -> *) (exp :: * -> *) i (exp' :: * -> *)
       (pred :: k -> Constraint).
(Functor m, Monad m) =>
(exp i -> m (exp' i))
-> ChanSize exp pred i -> m (ChanSize exp' pred i)
mapSizeExpA exp1 i -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 i)
forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp ChanSize exp1 pred i
ChanSize exp pred i
sz
  reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (ReadOne Chan t c
c) = ProgramT instr (Param2 exp2 pred) m (Val a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m (Val a)
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val a))
-> ProgramT instr (Param2 exp2 pred) m (Val a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val a)
forall a b. (a -> b) -> a -> b
$ ChanCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a)
-> ProgramT instr (Param2 exp2 pred) m (Val a)
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (ChanCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a)
 -> ProgramT instr (Param2 exp2 pred) m (Val a))
-> ChanCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a)
-> ProgramT instr (Param2 exp2 pred) m (Val a)
forall a b. (a -> b) -> a -> b
$ Chan t c
-> ChanCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val a)
forall k k k a (pred :: * -> Constraint) (t :: k) (a :: k)
       (pred :: k) (t :: * -> *).
(Typeable a, pred a) =>
Chan t a -> ChanCMD (Param3 pred t pred) (Val a)
ReadOne Chan t c
c
  reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (ReadChan Chan t c
c exp i
f exp i
t Arr i a
a) = do
      exp2 i
rf <- exp1 i -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 i)
forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp exp1 i
exp i
f
      exp2 i
rt <- exp1 i -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 i)
forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp exp1 i
exp i
t
      ProgramT instr (Param2 exp2 pred) m (Val Bool)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val Bool)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m (Val Bool)
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val Bool))
-> ProgramT instr (Param2 exp2 pred) m (Val Bool)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val Bool)
forall a b. (a -> b) -> a -> b
$ ChanCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val Bool)
-> ProgramT instr (Param2 exp2 pred) m (Val Bool)
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (ChanCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val Bool)
 -> ProgramT instr (Param2 exp2 pred) m (Val Bool))
-> ChanCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val Bool)
-> ProgramT instr (Param2 exp2 pred) m (Val Bool)
forall a b. (a -> b) -> a -> b
$ Chan t c
-> exp2 i
-> exp2 i
-> Arr i a
-> ChanCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val Bool)
forall k k k c (exp :: * -> Constraint) prog (t :: k) (c :: k)
       (exp :: * -> *) (prog :: k).
(Typeable c, exp c, exp prog, Ix prog, Integral prog) =>
Chan t c
-> exp prog
-> exp prog
-> Arr prog c
-> ChanCMD (Param3 prog exp exp) (Val Bool)
ReadChan Chan t c
c exp2 i
rf exp2 i
rt Arr i a
a
  reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (WriteOne Chan t c
c exp a
x)  = ProgramT instr (Param2 exp2 pred) m (Val Bool)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val Bool)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m (Val Bool)
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val Bool))
-> (exp2 a -> ProgramT instr (Param2 exp2 pred) m (Val Bool))
-> exp2 a
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChanCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val Bool)
-> ProgramT instr (Param2 exp2 pred) m (Val Bool)
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (ChanCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val Bool)
 -> ProgramT instr (Param2 exp2 pred) m (Val Bool))
-> (exp2 a
    -> ChanCMD
         '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred)
         (Val Bool))
-> exp2 a
-> ProgramT instr (Param2 exp2 pred) m (Val Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Chan t c
-> exp2 a
-> ChanCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val Bool)
forall k k k a (pred :: * -> Constraint) (t :: k) (c :: k)
       (exp :: * -> *) (prog :: k).
(Typeable a, pred a) =>
Chan t c -> exp a -> ChanCMD (Param3 prog exp pred) (Val Bool)
WriteOne Chan t c
c (exp2 a
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val Bool))
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (exp2 a)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val Bool)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< exp1 a -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 a)
forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp exp1 a
exp a
x
  reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (WriteChan Chan t c
c exp i
f exp i
t Arr i a
a) = do
      exp2 i
rf <- exp1 i -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 i)
forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp exp1 i
exp i
f
      exp2 i
rt <- exp1 i -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 i)
forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp exp1 i
exp i
t
      ProgramT instr (Param2 exp2 pred) m (Val Bool)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val Bool)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m (Val Bool)
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val Bool))
-> ProgramT instr (Param2 exp2 pred) m (Val Bool)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val Bool)
forall a b. (a -> b) -> a -> b
$ ChanCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val Bool)
-> ProgramT instr (Param2 exp2 pred) m (Val Bool)
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (ChanCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val Bool)
 -> ProgramT instr (Param2 exp2 pred) m (Val Bool))
-> ChanCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val Bool)
-> ProgramT instr (Param2 exp2 pred) m (Val Bool)
forall a b. (a -> b) -> a -> b
$ Chan t c
-> exp2 i
-> exp2 i
-> Arr i a
-> ChanCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val Bool)
forall k k k c (exp :: * -> Constraint) prog (t :: k) (c :: k)
       (exp :: * -> *) (prog :: k).
(Typeable c, exp c, exp prog, Ix prog, Integral prog) =>
Chan t c
-> exp prog
-> exp prog
-> Arr prog c
-> ChanCMD (Param3 prog exp exp) (Val Bool)
WriteChan Chan t c
c exp2 i
rf exp2 i
rt Arr i a
a
  reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (CloseChan Chan Closeable c
c)   = ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m ()
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ())
-> ProgramT instr (Param2 exp2 pred) m ()
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) ()
forall a b. (a -> b) -> a -> b
$ ChanCMD '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (ChanCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
 -> ProgramT instr (Param2 exp2 pred) m ())
-> ChanCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
-> ProgramT instr (Param2 exp2 pred) m ()
forall a b. (a -> b) -> a -> b
$ Chan Closeable c
-> ChanCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) ()
forall k k (c :: k) (prog :: k) (c :: * -> *)
       (prog :: * -> Constraint).
Chan Closeable c -> ChanCMD (Param3 prog c prog) ()
CloseChan Chan Closeable c
c
  reexpressInstrEnv forall b.
exp1 b -> ReaderT env (ProgramT instr '(exp2, fs) m) (exp2 b)
reexp (ReadOK Chan Closeable c
c)      = ProgramT instr (Param2 exp2 pred) m (Val Bool)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val Bool)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ProgramT instr (Param2 exp2 pred) m (Val Bool)
 -> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val Bool))
-> ProgramT instr (Param2 exp2 pred) m (Val Bool)
-> ReaderT env (ProgramT instr (Param2 exp2 pred) m) (Val Bool)
forall a b. (a -> b) -> a -> b
$ ChanCMD
  '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val Bool)
-> ProgramT instr (Param2 exp2 pred) m (Val Bool)
forall k (i :: (* -> *, k) -> * -> *)
       (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *) a.
(i :<: instr) =>
i '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleInj (ChanCMD
   '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val Bool)
 -> ProgramT instr (Param2 exp2 pred) m (Val Bool))
-> ChanCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val Bool)
-> ProgramT instr (Param2 exp2 pred) m (Val Bool)
forall a b. (a -> b) -> a -> b
$ Chan Closeable c
-> ChanCMD
     '(ProgramT instr (Param2 exp2 pred) m, Param2 exp2 pred) (Val Bool)
forall k k (c :: k) (prog :: k) (exp :: * -> *)
       (pred :: * -> Constraint).
Chan Closeable c -> ChanCMD (Param3 prog exp pred) (Val Bool)
ReadOK Chan Closeable c
c

runThreadCMD :: ThreadCMD (Param3 IO IO pred) a -> IO a
runThreadCMD :: ThreadCMD (Param3 IO IO pred) a -> IO a
runThreadCMD (ForkWithId ThreadId -> prog ()
p) = do
  Flag ()
f <- IO (Flag ())
forall a. IO (Flag a)
newFlag
  MVar ThreadId
tidvar <- IO (MVar ThreadId)
forall a. IO (MVar a)
CC.newEmptyMVar
  ThreadId
cctid <- IO () -> IO ThreadId
CC.forkIO (IO () -> IO ThreadId)
-> (IO Bool -> IO ()) -> IO Bool -> IO ThreadId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO Bool -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (IO Bool -> IO ThreadId) -> IO Bool -> IO ThreadId
forall a b. (a -> b) -> a -> b
$ MVar ThreadId -> IO ThreadId
forall a. MVar a -> IO a
CC.takeMVar MVar ThreadId
tidvar IO ThreadId -> (ThreadId -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ThreadId -> prog ()
ThreadId -> IO ()
p IO () -> IO Bool -> IO Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Flag () -> () -> IO Bool
forall a. Flag a -> a -> IO Bool
setFlag Flag ()
f ()
  let tid :: ThreadId
tid = ThreadId -> Flag () -> ThreadId
TIDRun ThreadId
cctid Flag ()
f
  MVar ThreadId -> ThreadId -> IO ()
forall a. MVar a -> a -> IO ()
CC.putMVar MVar ThreadId
tidvar ThreadId
tid
  ThreadId -> IO ThreadId
forall (m :: * -> *) a. Monad m => a -> m a
return ThreadId
tid
runThreadCMD (Kill (TIDRun ThreadId
t Flag ()
f)) = do
  Flag () -> () -> IO Bool
forall a. Flag a -> a -> IO Bool
setFlag Flag ()
f ()
  ThreadId -> IO ()
CC.killThread ThreadId
t
  () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
runThreadCMD (Wait (TIDRun ThreadId
_ Flag ()
f)) = do
  Flag () -> IO ()
forall a. Flag a -> IO a
waitFlag Flag ()
f
runThreadCMD (Sleep exp i
us) = do
  i
us' <- exp i
IO i
us
  Int -> IO ()
CC.threadDelay (Int -> IO ()) -> Int -> IO ()
forall a b. (a -> b) -> a -> b
$ i -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral i
us'

runChanCMD :: forall pred a. ChanCMD (Param3 IO IO pred) a -> IO a
runChanCMD :: ChanCMD (Param3 IO IO pred) a -> IO a
runChanCMD (NewChan ChanSize exp pred i
sz) = do
  Int
sz' <- ChanSize IO pred i -> IO Int
forall k (pred :: k -> Constraint) i. ChanSize IO pred i -> IO Int
evalChanSize ChanSize exp pred i
ChanSize IO pred i
sz
  Chan Dynamic -> Chan t c
forall k k (t :: k) (a :: k). Chan Dynamic -> Chan t a
ChanRun (Chan Dynamic -> Chan t c) -> IO (Chan Dynamic) -> IO (Chan t c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> IO (Chan Dynamic)
forall a. Int -> IO (Chan a)
Chan.newChan Int
sz'
runChanCMD (ReadOne (ChanRun Chan Dynamic
c)) =
  a -> Val a
forall a. a -> Val a
ValRun (a -> Val a) -> ([Dynamic] -> a) -> [Dynamic] -> Val a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dynamic -> a
forall a. Typeable a => Dynamic -> a
convertDynamic (Dynamic -> a) -> ([Dynamic] -> Dynamic) -> [Dynamic] -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Dynamic] -> Dynamic
forall a. [a] -> a
head ([Dynamic] -> Val a) -> IO [Dynamic] -> IO (Val a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Chan Dynamic -> Int -> IO [Dynamic]
forall a. Chan a -> Int -> IO [a]
Chan.readChan Chan Dynamic
c Int
1
runChanCMD (ReadChan (ChanRun Chan Dynamic
c) exp i
off exp i
len Arr i a
arr) = do
  i
off' <- exp i
IO i
off
  i
len' <- exp i
IO i
len
  [Dynamic]
xs <- Chan Dynamic -> Int -> IO [Dynamic]
forall a. Chan a -> Int -> IO [a]
Chan.readChan Chan Dynamic
c (Int -> IO [Dynamic]) -> Int -> IO [Dynamic]
forall a b. (a -> b) -> a -> b
$ i -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (i
len' i -> i -> i
forall a. Num a => a -> a -> a
- i
off')
  let xs' :: [a]
xs' = (Dynamic -> a) -> [Dynamic] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map Dynamic -> a
forall a. Typeable a => Dynamic -> a
convertDynamic [Dynamic]
xs
  (forall b. IO b -> IO b)
-> Program ArrCMD '(IO, Param1 pred) () -> IO ()
forall k (i :: (* -> *, (* -> *, k)) -> * -> *) (m :: * -> *)
       (fs :: k) (exp :: * -> *) a.
(InterpBi i m fs, HBifunctor i, Functor m, Monad m) =>
(forall b. exp b -> m b) -> Program i '(exp, fs) a -> m a
interpretBi forall a. a -> a
forall b. IO b -> IO b
id (Program ArrCMD '(IO, Param1 pred) () -> IO ())
-> Program ArrCMD '(IO, Param1 pred) () -> IO ()
forall a b. (a -> b) -> a -> b
$ [(i, a)]
-> ((i, a) -> Program ArrCMD '(IO, Param1 pred) ())
-> Program ArrCMD '(IO, Param1 pred) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([i] -> [a] -> [(i, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [i
off' .. ] [a]
xs') (((i, a) -> Program ArrCMD '(IO, Param1 pred) ())
 -> Program ArrCMD '(IO, Param1 pred) ())
-> ((i, a) -> Program ArrCMD '(IO, Param1 pred) ())
-> Program ArrCMD '(IO, Param1 pred) ()
forall a b. (a -> b) -> a -> b
$ \(i
i, a
x) -> do
    Arr i a -> IO i -> IO a -> Program ArrCMD '(IO, Param1 pred) ()
forall (pred :: * -> Constraint) a i
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (exp :: * -> *) (m :: * -> *).
(pred a, pred i, Integral i, Ix i, ArrCMD :<: instr) =>
Arr i a -> exp i -> exp a -> ProgramT instr (Param2 exp pred) m ()
setArr Arr i a
arr (i -> IO i
forall (m :: * -> *) a. Monad m => a -> m a
return i
i) (a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x) :: Program ArrCMD (Param2 IO pred) ()
  Bool -> Val Bool
forall a. a -> Val a
ValRun (Bool -> Val Bool) -> IO Bool -> IO (Val Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Chan Dynamic -> IO Bool
forall a. Chan a -> IO Bool
Chan.lastReadOK Chan Dynamic
c
runChanCMD (WriteOne (ChanRun Chan Dynamic
c) exp a
x) =
  Bool -> Val Bool
forall a. a -> Val a
ValRun (Bool -> Val Bool) -> IO Bool -> IO (Val Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Chan Dynamic -> [Dynamic] -> IO Bool
forall a. Chan a -> [a] -> IO Bool
Chan.writeChan Chan Dynamic
c ([Dynamic] -> IO Bool) -> (a -> [Dynamic]) -> a -> IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dynamic -> [Dynamic]
forall (m :: * -> *) a. Monad m => a -> m a
return (Dynamic -> [Dynamic]) -> (a -> Dynamic) -> a -> [Dynamic]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn (a -> IO Bool) -> IO a -> IO Bool
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< exp a
IO a
x)
runChanCMD (WriteChan (ChanRun Chan Dynamic
c) exp i
off exp i
len (Arr i a
arr :: Arr ix el)) = do
  i
off' <- exp i
IO i
off
  i
len' <- exp i
IO i
len
  [IO a]
xs <- (forall b. IO b -> IO b)
-> Program ArrCMD '(IO, Param1 pred) [IO a] -> IO [IO a]
forall k (i :: (* -> *, (* -> *, k)) -> * -> *) (m :: * -> *)
       (fs :: k) (exp :: * -> *) a.
(InterpBi i m fs, HBifunctor i, Functor m, Monad m) =>
(forall b. exp b -> m b) -> Program i '(exp, fs) a -> m a
interpretBi forall a. a -> a
forall b. IO b -> IO b
id (Program ArrCMD '(IO, Param1 pred) [IO a] -> IO [IO a])
-> Program ArrCMD '(IO, Param1 pred) [IO a] -> IO [IO a]
forall a b. (a -> b) -> a -> b
$ [i]
-> (i -> ProgramT ArrCMD '(IO, Param1 pred) Identity (IO a))
-> Program ArrCMD '(IO, Param1 pred) [IO a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [i
off' .. i
off' i -> i -> i
forall a. Num a => a -> a -> a
+ i
len' i -> i -> i
forall a. Num a => a -> a -> a
- i
1] ((i -> ProgramT ArrCMD '(IO, Param1 pred) Identity (IO a))
 -> Program ArrCMD '(IO, Param1 pred) [IO a])
-> (i -> ProgramT ArrCMD '(IO, Param1 pred) Identity (IO a))
-> Program ArrCMD '(IO, Param1 pred) [IO a]
forall a b. (a -> b) -> a -> b
$ \i
i -> do
    Arr i a
-> IO i -> ProgramT ArrCMD '(IO, Param1 pred) Identity (IO a)
forall (pred :: * -> Constraint) a i (exp :: * -> *)
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (m :: * -> *).
(pred a, pred i, FreeExp exp, FreePred exp a, Integral i, Ix i,
 ArrCMD :<: instr, Monad m) =>
Arr i a -> exp i -> ProgramT instr (Param2 exp pred) m (exp a)
getArr Arr i a
arr (i -> IO i
forall (m :: * -> *) a. Monad m => a -> m a
return i
i) :: Program ArrCMD (Param2 IO pred) (IO el)
  Bool -> Val Bool
forall a. a -> Val a
ValRun (Bool -> Val Bool) -> IO Bool -> IO (Val Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Chan Dynamic -> [Dynamic] -> IO Bool
forall a. Chan a -> [a] -> IO Bool
Chan.writeChan Chan Dynamic
c ([Dynamic] -> IO Bool) -> IO [Dynamic] -> IO Bool
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (a -> Dynamic) -> [a] -> [Dynamic]
forall a b. (a -> b) -> [a] -> [b]
map a -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn ([a] -> [Dynamic]) -> IO [a] -> IO [Dynamic]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [IO a] -> IO [a]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [IO a]
xs)
runChanCMD (CloseChan (ChanRun Chan Dynamic
c)) = Chan Dynamic -> IO ()
forall a. Chan a -> IO ()
Chan.closeChan Chan Dynamic
c
runChanCMD (ReadOK    (ChanRun Chan Dynamic
c)) = Bool -> Val Bool
forall a. a -> Val a
ValRun (Bool -> Val Bool) -> IO Bool -> IO (Val Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Chan Dynamic -> IO Bool
forall a. Chan a -> IO Bool
Chan.lastReadOK Chan Dynamic
c

instance InterpBi ThreadCMD IO (Param1 pred) where
  interpBi :: ThreadCMD '(IO, '(IO, Param1 pred)) a -> IO a
interpBi = ThreadCMD '(IO, '(IO, Param1 pred)) a -> IO a
forall k2 (pred :: k2) a.
ThreadCMD '(IO, '(IO, Param1 pred)) a -> IO a
runThreadCMD
instance InterpBi ChanCMD IO (Param1 pred) where
  interpBi :: ChanCMD '(IO, '(IO, Param1 pred)) a -> IO a
interpBi = ChanCMD '(IO, '(IO, Param1 pred)) a -> IO a
forall (pred :: * -> Constraint) a.
ChanCMD '(IO, '(IO, Param1 pred)) a -> IO a
runChanCMD

evalChanSize :: ChanSize IO pred i -> IO Int
evalChanSize :: ChanSize IO pred i -> IO Int
evalChanSize (OneSize proxy a
_ IO i
sz) = do
  i
sz' <- IO i
sz
  Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ i -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral i
sz'
evalChanSize (TimesSize IO i
n ChanSize IO pred i
sz) = do
  i
n' <- IO i
n
  Int
sz' <- ChanSize IO pred i -> IO Int
forall k (pred :: k -> Constraint) i. ChanSize IO pred i -> IO Int
evalChanSize ChanSize IO pred i
sz
  Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ i -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral i
n' Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
sz'
evalChanSize (PlusSize ChanSize IO pred i
a ChanSize IO pred i
b) = do
  Int
a' <- ChanSize IO pred i -> IO Int
forall k (pred :: k -> Constraint) i. ChanSize IO pred i -> IO Int
evalChanSize ChanSize IO pred i
a
  Int
b' <- ChanSize IO pred i -> IO Int
forall k (pred :: k -> Constraint) i. ChanSize IO pred i -> IO Int
evalChanSize ChanSize IO pred i
b
  Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ Int
a' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
b'

convertDynamic :: Typeable a => Dynamic -> a
convertDynamic :: Dynamic -> a
convertDynamic = a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe (String -> a
forall a. HasCallStack => String -> a
error String
"readChan: unknown element") (Maybe a -> a) -> (Dynamic -> Maybe a) -> Dynamic -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dynamic -> Maybe a
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic

instance FreeExp IO
  where
    type FreePred IO = Typeable
    constExp :: a -> IO a
constExp = a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return
    varExp :: String -> IO a
varExp   = String -> String -> IO a
forall a. HasCallStack => String -> a
error String
"varExp: unimplemented over IO"