-- | Basic concurrency primitives.
--
-- To compile the C code resulting from 'Language.Embedded.Backend.C.compile'
-- for programs with concurrency primitives, use something like
--
-- > cc -std=c99 -Iinclude csrc/chan.c -lpthread YOURPROGRAM.c
module Language.Embedded.Concurrent
  ( ThreadId (..)
  , Chan (..)
  , ChanSize (..)
  , ThreadCMD
  , ChanCMD
  , Closeable, Uncloseable
  , fork, forkWithId, asyncKillThread, killThread, waitThread, delayThread
  , timesSizeOf, timesSize, plusSize
  , newChan, newCloseableChan
  , readChan, writeChan
  , readChanBuf, writeChanBuf
  , closeChan, lastChanReadOK
  , newChan', newCloseableChan'
  , readChan', writeChan'
  , readChanBuf', writeChanBuf'
  ) where

import Control.Monad.Operational.Higher
import Data.Ix
import Data.Typeable

import Language.Embedded.Concurrent.Backend.C ()
import Language.Embedded.Concurrent.CMD
import Language.Embedded.Expression
import Language.Embedded.Imperative.CMD (Arr)



-- | Fork off a computation as a new thread.
fork :: (ThreadCMD :<: instr)
     => ProgramT instr (Param2 exp pred) m ()
     -> ProgramT instr (Param2 exp pred) m ThreadId
fork :: ProgramT instr (Param2 exp pred) m ()
-> ProgramT instr (Param2 exp pred) m ThreadId
fork = (ThreadId -> ProgramT instr (Param2 exp pred) m ())
-> ProgramT instr (Param2 exp pred) m ThreadId
forall k1 (instr :: (* -> *, (* -> *, (k1, *))) -> * -> *)
       (exp :: * -> *) (pred :: k1) (m :: * -> *).
(ThreadCMD :<: instr) =>
(ThreadId -> ProgramT instr (Param2 exp pred) m ())
-> ProgramT instr (Param2 exp pred) m ThreadId
forkWithId ((ThreadId -> ProgramT instr (Param2 exp pred) m ())
 -> ProgramT instr (Param2 exp pred) m ThreadId)
-> (ProgramT instr (Param2 exp pred) m ()
    -> ThreadId -> ProgramT instr (Param2 exp pred) m ())
-> ProgramT instr (Param2 exp pred) m ()
-> ProgramT instr (Param2 exp pred) m ThreadId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProgramT instr (Param2 exp pred) m ()
-> ThreadId -> ProgramT instr (Param2 exp pred) m ()
forall a b. a -> b -> a
const

-- | Fork off a computation as a new thread, with access to its own thread ID.
forkWithId :: (ThreadCMD :<: instr)
           => (ThreadId -> ProgramT instr (Param2 exp pred) m ())
           -> ProgramT instr (Param2 exp pred) m ThreadId
forkWithId :: (ThreadId -> ProgramT instr (Param2 exp pred) m ())
-> ProgramT instr (Param2 exp pred) m ThreadId
forkWithId = instr
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ThreadId
-> ProgramT instr (Param2 exp pred) m ThreadId
forall k (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *)
       a.
instr '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleton (instr
   '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ThreadId
 -> ProgramT instr (Param2 exp pred) m ThreadId)
-> ((ThreadId -> ProgramT instr (Param2 exp pred) m ())
    -> instr
         '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ThreadId)
-> (ThreadId -> ProgramT instr (Param2 exp pred) m ())
-> ProgramT instr (Param2 exp pred) m ThreadId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThreadCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ThreadId
-> instr
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ThreadId
forall k k1 (sub :: k -> k1 -> *) (sup :: k -> k1 -> *) (fs :: k)
       (a :: k1).
(sub :<: sup) =>
sub fs a -> sup fs a
inj (ThreadCMD
   '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ThreadId
 -> instr
      '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ThreadId)
-> ((ThreadId -> ProgramT instr (Param2 exp pred) m ())
    -> ThreadCMD
         '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ThreadId)
-> (ThreadId -> ProgramT instr (Param2 exp pred) m ())
-> instr
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ThreadId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ThreadId -> ProgramT instr (Param2 exp pred) m ())
-> ThreadCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ThreadId
forall k2 (prog :: * -> *) (exp :: * -> *) (pred :: k2).
(ThreadId -> prog ()) -> ThreadCMD (Param3 prog exp pred) ThreadId
ForkWithId

-- | Forcibly terminate a thread, then continue execution immediately.
asyncKillThread :: (ThreadCMD :<: instr)
                => ThreadId -> ProgramT instr (Param2 exp pred) m ()
asyncKillThread :: ThreadId -> ProgramT instr (Param2 exp pred) m ()
asyncKillThread = instr '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp pred) m ()
forall k (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *)
       a.
instr '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleton (instr '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> (ThreadId
    -> instr '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ())
-> ThreadId
-> ProgramT instr (Param2 exp pred) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThreadCMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> instr '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall k k1 (sub :: k -> k1 -> *) (sup :: k -> k1 -> *) (fs :: k)
       (a :: k1).
(sub :<: sup) =>
sub fs a -> sup fs a
inj (ThreadCMD
   '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
 -> instr '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ())
-> (ThreadId
    -> ThreadCMD
         '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ())
-> ThreadId
-> instr '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThreadId
-> ThreadCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall k2 (prog :: * -> *) (exp :: * -> *) (pred :: k2).
ThreadId -> ThreadCMD (Param3 prog exp pred) ()
Kill

-- | Forcibly terminate a thread. Blocks until the thread is actually dead.
killThread :: (ThreadCMD :<: instr, Monad m)
           => ThreadId -> ProgramT instr (Param2 exp pred) m ()
killThread :: ThreadId -> ProgramT instr (Param2 exp pred) m ()
killThread ThreadId
t = do
  instr '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp pred) m ()
forall k (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *)
       a.
instr '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleton (instr '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> (ThreadCMD
      '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
    -> instr '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ())
-> ThreadCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp pred) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThreadCMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> instr '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall k k1 (sub :: k -> k1 -> *) (sup :: k -> k1 -> *) (fs :: k)
       (a :: k1).
(sub :<: sup) =>
sub fs a -> sup fs a
inj (ThreadCMD
   '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> ThreadCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp pred) m ()
forall a b. (a -> b) -> a -> b
$ ThreadId
-> ThreadCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall k2 (prog :: * -> *) (exp :: * -> *) (pred :: k2).
ThreadId -> ThreadCMD (Param3 prog exp pred) ()
Kill ThreadId
t
  ThreadId -> ProgramT instr (Param2 exp pred) m ()
forall k2 (instr :: (* -> *, (* -> *, (k2, *))) -> * -> *)
       (exp :: * -> *) (pred :: k2) (m :: * -> *).
(ThreadCMD :<: instr) =>
ThreadId -> ProgramT instr (Param2 exp pred) m ()
waitThread ThreadId
t

-- | Wait for a thread to terminate.
waitThread :: (ThreadCMD :<: instr)
           => ThreadId -> ProgramT instr (Param2 exp pred) m ()
waitThread :: ThreadId -> ProgramT instr (Param2 exp pred) m ()
waitThread = instr '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp pred) m ()
forall k (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *)
       a.
instr '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleton (instr '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> (ThreadId
    -> instr '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ())
-> ThreadId
-> ProgramT instr (Param2 exp pred) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThreadCMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> instr '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall k k1 (sub :: k -> k1 -> *) (sup :: k -> k1 -> *) (fs :: k)
       (a :: k1).
(sub :<: sup) =>
sub fs a -> sup fs a
inj (ThreadCMD
   '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
 -> instr '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ())
-> (ThreadId
    -> ThreadCMD
         '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ())
-> ThreadId
-> instr '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThreadId
-> ThreadCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall k2 (prog :: * -> *) (exp :: * -> *) (pred :: k2).
ThreadId -> ThreadCMD (Param3 prog exp pred) ()
Wait

-- | Sleep for a given amount of microseconds. Implemented with `usleep`.
--   A C compiler might require a feature test macro to be defined,
--   otherwise it emits a warning about an implicitly declared function.
--   For more details, see: http://man7.org/linux/man-pages/man3/usleep.3.html
delayThread :: (Integral i, ThreadCMD :<: instr)
           => exp i -> ProgramT instr (Param2 exp pred) m ()
delayThread :: exp i -> ProgramT instr (Param2 exp pred) m ()
delayThread = instr '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp pred) m ()
forall k (instr :: (* -> *, k) -> * -> *) (fs :: k) (m :: * -> *)
       a.
instr '(ProgramT instr fs m, fs) a -> ProgramT instr fs m a
singleton (instr '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> (exp i
    -> instr '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ())
-> exp i
-> ProgramT instr (Param2 exp pred) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThreadCMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> instr '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall k k1 (sub :: k -> k1 -> *) (sup :: k -> k1 -> *) (fs :: k)
       (a :: k1).
(sub :<: sup) =>
sub fs a -> sup fs a
inj (ThreadCMD
   '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
 -> instr '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ())
-> (exp i
    -> ThreadCMD
         '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ())
-> exp i
-> instr '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. exp i
-> ThreadCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall k2 i (exp :: * -> *) (prog :: * -> *) (pred :: k2).
Integral i =>
exp i -> ThreadCMD (Param3 prog exp pred) ()
Sleep


--------------------------------------------------------------------------------
-- Channel frontend
--------------------------------------------------------------------------------

-- | Create a new channel. Writing a reference type to a channel will copy
--   contents into the channel, so modifying it post-write is completely
--   safe.
newChan :: forall a i exp pred instr m
        .  (pred a, Integral i, ChanCMD :<: instr)
        => exp i
        -> ProgramT instr (Param2 exp pred) m (Chan Uncloseable a)
newChan :: exp i -> ProgramT instr (Param2 exp pred) m (Chan Uncloseable a)
newChan exp i
n = ChanSize exp pred i
-> ProgramT instr (Param2 exp pred) m (Chan Uncloseable a)
forall k i
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (exp :: * -> *) (pred :: * -> Constraint) (m :: * -> *) (a :: k).
(Integral i, ChanCMD :<: instr) =>
ChanSize exp pred i
-> ProgramT instr (Param2 exp pred) m (Chan Uncloseable a)
newChan' (ChanSize exp pred i
 -> ProgramT instr (Param2 exp pred) m (Chan Uncloseable a))
-> ChanSize exp pred i
-> ProgramT instr (Param2 exp pred) m (Chan Uncloseable a)
forall a b. (a -> b) -> a -> b
$ exp i
n exp i -> Proxy a -> ChanSize exp pred i
forall k (pred :: k -> Constraint) (a :: k) i (exp :: * -> *)
       (proxy :: k -> *).
(pred a, Integral i) =>
exp i -> proxy a -> ChanSize exp pred i
`timesSizeOf` (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a)

newCloseableChan :: forall a i exp pred instr m
                 .  (pred a, Integral i, ChanCMD :<: instr)
                 => exp i
                 -> ProgramT instr (Param2 exp pred) m (Chan Closeable a)
newCloseableChan :: exp i -> ProgramT instr (Param2 exp pred) m (Chan Closeable a)
newCloseableChan exp i
n = ChanSize exp pred i
-> ProgramT instr (Param2 exp pred) m (Chan Closeable a)
forall k i
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (exp :: * -> *) (pred :: * -> Constraint) (m :: * -> *) (a :: k).
(Integral i, ChanCMD :<: instr) =>
ChanSize exp pred i
-> ProgramT instr (Param2 exp pred) m (Chan Closeable a)
newCloseableChan' (ChanSize exp pred i
 -> ProgramT instr (Param2 exp pred) m (Chan Closeable a))
-> ChanSize exp pred i
-> ProgramT instr (Param2 exp pred) m (Chan Closeable a)
forall a b. (a -> b) -> a -> b
$ exp i
n exp i -> Proxy a -> ChanSize exp pred i
forall k (pred :: k -> Constraint) (a :: k) i (exp :: * -> *)
       (proxy :: k -> *).
(pred a, Integral i) =>
exp i -> proxy a -> ChanSize exp pred i
`timesSizeOf` (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a)


-- | Read an element from a channel. If channel is empty, blocks until there
--   is an item available.
--   If 'closeChan' has been called on the channel *and* if the channel is
--   empty, @readChan@ returns an undefined value immediately.
readChan :: ( Typeable a, pred a
            , FreeExp exp, FreePred exp a
            , ChanCMD :<: instr, Monad m )
         => Chan t a
         -> ProgramT instr (Param2 exp pred) m (exp a)
readChan :: Chan t a -> ProgramT instr (Param2 exp pred) m (exp a)
readChan = Chan t a -> ProgramT instr (Param2 exp pred) m (exp a)
forall k k a (pred :: * -> Constraint) (exp :: * -> *)
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (m :: * -> *) (t :: k) (c :: k).
(Typeable a, pred a, FreeExp exp, FreePred exp a,
 ChanCMD :<: instr, Monad m) =>
Chan t c -> ProgramT instr (Param2 exp pred) m (exp a)
readChan'

-- | Read an arbitrary number of elements from a channel into an array.
--   The semantics are the same as for 'readChan', where "channel is empty"
--   is defined as "channel contains less data than requested".
--   Returns @False@ without reading any data if the channel is closed.
readChanBuf :: ( Typeable a, pred a, pred i
               , Ix i, Integral i
               , FreeExp exp, FreePred exp Bool
               , ChanCMD :<: instr, Monad m )
            => Chan t a
            -> exp i -- ^ Offset in array to start writing
            -> exp i -- ^ Elements to read
            -> Arr i a
            -> ProgramT instr (Param2 exp pred) m (exp Bool)
readChanBuf :: Chan t a
-> exp i
-> exp i
-> Arr i a
-> ProgramT instr (Param2 exp pred) m (exp Bool)
readChanBuf = Chan t a
-> exp i
-> exp i
-> Arr i a
-> ProgramT instr (Param2 exp pred) m (exp Bool)
forall k k a (pred :: * -> Constraint) i (exp :: * -> *)
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (m :: * -> *) (t :: k) (c :: k).
(Typeable a, pred a, pred i, Ix i, Integral i, FreeExp exp,
 FreePred exp Bool, ChanCMD :<: instr, Monad m) =>
Chan t c
-> exp i
-> exp i
-> Arr i a
-> ProgramT instr (Param2 exp pred) m (exp Bool)
readChanBuf'

-- | Write a data element to a channel.
--   If 'closeChan' has been called on the channel, all calls to @writeChan@
--   become non-blocking no-ops and return @False@, otherwise returns @True@.
--   If the channel is full, this function blocks until there's space in the
--   queue.
writeChan :: ( Typeable a, pred a
             , FreeExp exp, FreePred exp Bool
             , ChanCMD :<: instr, Monad m )
          => Chan t a
          -> exp a
          -> ProgramT instr (Param2 exp pred) m (exp Bool)
writeChan :: Chan t a -> exp a -> ProgramT instr (Param2 exp pred) m (exp Bool)
writeChan = Chan t a -> exp a -> ProgramT instr (Param2 exp pred) m (exp Bool)
forall k k a (pred :: * -> Constraint) (exp :: * -> *)
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (m :: * -> *) (t :: k) (c :: k).
(Typeable a, pred a, FreeExp exp, FreePred exp Bool,
 ChanCMD :<: instr, Monad m) =>
Chan t c -> exp a -> ProgramT instr (Param2 exp pred) m (exp Bool)
writeChan'

-- | Write an arbitrary number of elements from an array into an channel.
--   The semantics are the same as for 'writeChan', where "channel is full"
--   is defined as "channel has insufficient free space to store all written
--   data".
writeChanBuf :: ( Typeable a, pred a, pred i
                , Ix i, Integral i
                , FreeExp exp, FreePred exp Bool
                , ChanCMD :<: instr, Monad m )
             => Chan t a
             -> exp i -- ^ Offset in array to start reading
             -> exp i -- ^ Elements to write
             -> Arr i a
             -> ProgramT instr (Param2 exp pred) m (exp Bool)
writeChanBuf :: Chan t a
-> exp i
-> exp i
-> Arr i a
-> ProgramT instr (Param2 exp pred) m (exp Bool)
writeChanBuf = Chan t a
-> exp i
-> exp i
-> Arr i a
-> ProgramT instr (Param2 exp pred) m (exp Bool)
forall k k a (pred :: * -> Constraint) i (exp :: * -> *)
       (instr :: (* -> *, (* -> *, (* -> Constraint, *))) -> * -> *)
       (m :: * -> *) (t :: k) (c :: k).
(Typeable a, pred a, pred i, Ix i, Integral i, FreeExp exp,
 FreePred exp Bool, ChanCMD :<: instr, Monad m) =>
Chan t c
-> exp i
-> exp i
-> Arr i a
-> ProgramT instr (Param2 exp pred) m (exp Bool)
writeChanBuf'

-- | When 'readChan' was last called on the given channel, did the read
--   succeed?
--   Always returns @True@ unless 'closeChan' has been called on the channel.
--   Always returns @True@ if the channel has never been read.
lastChanReadOK :: (FreeExp exp, FreePred exp Bool, ChanCMD :<: instr, Monad m)
               => Chan Closeable c
               -> ProgramT instr (Param2 exp pred) m (exp Bool)
lastChanReadOK :: Chan Closeable c -> ProgramT instr (Param2 exp pred) m (exp Bool)
lastChanReadOK = (Val Bool -> exp Bool)
-> ProgramT instr (Param2 exp pred) m (Val Bool)
-> ProgramT instr (Param2 exp pred) m (exp Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Val Bool -> exp Bool
forall (exp :: * -> *) a.
(FreeExp exp, FreePred exp a) =>
Val a -> exp a
valToExp (ProgramT instr (Param2 exp pred) m (Val Bool)
 -> ProgramT instr (Param2 exp pred) m (exp Bool))
-> (Chan Closeable c
    -> ProgramT instr (Param2 exp pred) m (Val Bool))
-> Chan Closeable c
-> ProgramT instr (Param2 exp pred) m (exp Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChanCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val Bool)
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) (Val Bool)
 -> ProgramT instr (Param2 exp pred) m (Val Bool))
-> (Chan Closeable c
    -> ChanCMD
         '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val Bool))
-> Chan Closeable c
-> ProgramT instr (Param2 exp pred) m (Val Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Chan Closeable c
-> ChanCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val Bool)
forall k k (exp :: k) (pred :: k) (exp :: * -> *)
       (pred :: * -> Constraint).
Chan Closeable exp -> ChanCMD (Param3 pred exp pred) (Val Bool)
ReadOK

-- | Close a channel. All subsequent write operations will be no-ops.
--   After the channel is drained, all subsequent read operations will be
--   no-ops as well.
closeChan :: (ChanCMD :<: instr)
          => Chan Closeable c
          -> ProgramT instr (Param2 exp pred) m ()
closeChan :: Chan Closeable c -> ProgramT instr (Param2 exp pred) m ()
closeChan = ChanCMD '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) ()
 -> ProgramT instr (Param2 exp pred) m ())
-> (Chan Closeable c
    -> ChanCMD
         '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ())
-> Chan Closeable c
-> ProgramT instr (Param2 exp pred) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Chan Closeable c
-> ChanCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) ()
forall k k (c :: k) (prog :: k) (exp :: * -> *)
       (pred :: * -> Constraint).
Chan Closeable c -> ChanCMD (Param3 prog exp pred) ()
CloseChan


--------------------------------------------------------------------------------
-- Unsafe channel primitives
--------------------------------------------------------------------------------

newChan' :: (Integral i, ChanCMD :<: instr)
         => ChanSize exp pred i
         -> ProgramT instr (Param2 exp pred) m (Chan Uncloseable a)
newChan' :: ChanSize exp pred i
-> ProgramT instr (Param2 exp pred) m (Chan Uncloseable a)
newChan' = ChanCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred)
  (Chan Uncloseable a)
-> ProgramT instr (Param2 exp pred) m (Chan Uncloseable 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 exp pred) m, Param2 exp pred)
   (Chan Uncloseable a)
 -> ProgramT instr (Param2 exp pred) m (Chan Uncloseable a))
-> (ChanSize exp pred i
    -> ChanCMD
         '(ProgramT instr (Param2 exp pred) m, Param2 exp pred)
         (Chan Uncloseable a))
-> ChanSize exp pred i
-> ProgramT instr (Param2 exp pred) m (Chan Uncloseable a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChanSize exp pred i
-> ChanCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred)
     (Chan Uncloseable a)
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

newCloseableChan' :: (Integral i, ChanCMD :<: instr)
                  => ChanSize exp pred i
                  -> ProgramT instr (Param2 exp pred) m (Chan Closeable a)
newCloseableChan' :: ChanSize exp pred i
-> ProgramT instr (Param2 exp pred) m (Chan Closeable a)
newCloseableChan' = ChanCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred)
  (Chan Closeable a)
-> ProgramT instr (Param2 exp pred) m (Chan Closeable 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 exp pred) m, Param2 exp pred)
   (Chan Closeable a)
 -> ProgramT instr (Param2 exp pred) m (Chan Closeable a))
-> (ChanSize exp pred i
    -> ChanCMD
         '(ProgramT instr (Param2 exp pred) m, Param2 exp pred)
         (Chan Closeable a))
-> ChanSize exp pred i
-> ProgramT instr (Param2 exp pred) m (Chan Closeable a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChanSize exp pred i
-> ChanCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred)
     (Chan Closeable a)
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

readChan' :: ( Typeable a, pred a
             , FreeExp exp, FreePred exp a
             , ChanCMD :<: instr, Monad m )
          => Chan t c
          -> ProgramT instr (Param2 exp pred) m (exp a)
readChan' :: Chan t c -> ProgramT instr (Param2 exp pred) m (exp a)
readChan' = (Val a -> exp a)
-> ProgramT instr (Param2 exp pred) m (Val a)
-> ProgramT instr (Param2 exp pred) m (exp a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Val a -> exp a
forall (exp :: * -> *) a.
(FreeExp exp, FreePred exp a) =>
Val a -> exp a
valToExp (ProgramT instr (Param2 exp pred) m (Val a)
 -> ProgramT instr (Param2 exp pred) m (exp a))
-> (Chan t c -> ProgramT instr (Param2 exp pred) m (Val a))
-> Chan t c
-> ProgramT instr (Param2 exp pred) m (exp a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChanCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val a)
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) (Val a)
 -> ProgramT instr (Param2 exp pred) m (Val a))
-> (Chan t c
    -> ChanCMD
         '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val a))
-> Chan t c
-> ProgramT instr (Param2 exp pred) m (Val a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Chan t c
-> ChanCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 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

readChanBuf' :: ( Typeable a, pred a, pred i
                , Ix i, Integral i
                , FreeExp exp, FreePred exp Bool
                , ChanCMD :<: instr, Monad m )
             => Chan t c
             -> exp i -- ^ Offset in array to start writing
             -> exp i -- ^ Elements to read
             -> Arr i a
             -> ProgramT instr (Param2 exp pred) m (exp Bool)
readChanBuf' :: Chan t c
-> exp i
-> exp i
-> Arr i a
-> ProgramT instr (Param2 exp pred) m (exp Bool)
readChanBuf' Chan t c
ch exp i
off exp i
sz Arr i a
arr = (Val Bool -> exp Bool)
-> ProgramT instr (Param2 exp pred) m (Val Bool)
-> ProgramT instr (Param2 exp pred) m (exp Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Val Bool -> exp Bool
forall (exp :: * -> *) a.
(FreeExp exp, FreePred exp a) =>
Val a -> exp a
valToExp (ProgramT instr (Param2 exp pred) m (Val Bool)
 -> ProgramT instr (Param2 exp pred) m (exp Bool))
-> (ChanCMD
      '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val Bool)
    -> ProgramT instr (Param2 exp pred) m (Val Bool))
-> ChanCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val Bool)
-> ProgramT instr (Param2 exp pred) m (exp Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChanCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val Bool)
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) (Val Bool)
 -> ProgramT instr (Param2 exp pred) m (exp Bool))
-> ChanCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val Bool)
-> ProgramT instr (Param2 exp pred) m (exp Bool)
forall a b. (a -> b) -> a -> b
$ Chan t c
-> exp i
-> exp i
-> Arr i a
-> ChanCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 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
ch exp i
off exp i
sz Arr i a
arr

writeChan' :: ( Typeable a, pred a
              , FreeExp exp, FreePred exp Bool
              , ChanCMD :<: instr, Monad m )
           => Chan t c
           -> exp a
           -> ProgramT instr (Param2 exp pred) m (exp Bool)
writeChan' :: Chan t c -> exp a -> ProgramT instr (Param2 exp pred) m (exp Bool)
writeChan' Chan t c
c = (Val Bool -> exp Bool)
-> ProgramT instr (Param2 exp pred) m (Val Bool)
-> ProgramT instr (Param2 exp pred) m (exp Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Val Bool -> exp Bool
forall (exp :: * -> *) a.
(FreeExp exp, FreePred exp a) =>
Val a -> exp a
valToExp (ProgramT instr (Param2 exp pred) m (Val Bool)
 -> ProgramT instr (Param2 exp pred) m (exp Bool))
-> (exp a -> ProgramT instr (Param2 exp pred) m (Val Bool))
-> exp a
-> ProgramT instr (Param2 exp pred) m (exp Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChanCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val Bool)
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) (Val Bool)
 -> ProgramT instr (Param2 exp pred) m (Val Bool))
-> (exp a
    -> ChanCMD
         '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val Bool))
-> exp a
-> ProgramT instr (Param2 exp pred) m (Val Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Chan t c
-> exp a
-> ChanCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 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

writeChanBuf' :: ( Typeable a, pred a, pred i
                 , Ix i, Integral i
                 , FreeExp exp, FreePred exp Bool
                 , ChanCMD :<: instr, Monad m )
              => Chan t c
              -> exp i -- ^ Offset in array to start reading
              -> exp i -- ^ Elements to write
              -> Arr i a
              -> ProgramT instr (Param2 exp pred) m (exp Bool)
writeChanBuf' :: Chan t c
-> exp i
-> exp i
-> Arr i a
-> ProgramT instr (Param2 exp pred) m (exp Bool)
writeChanBuf' Chan t c
ch exp i
off exp i
sz Arr i a
arr = (Val Bool -> exp Bool)
-> ProgramT instr (Param2 exp pred) m (Val Bool)
-> ProgramT instr (Param2 exp pred) m (exp Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Val Bool -> exp Bool
forall (exp :: * -> *) a.
(FreeExp exp, FreePred exp a) =>
Val a -> exp a
valToExp (ProgramT instr (Param2 exp pred) m (Val Bool)
 -> ProgramT instr (Param2 exp pred) m (exp Bool))
-> (ChanCMD
      '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val Bool)
    -> ProgramT instr (Param2 exp pred) m (Val Bool))
-> ChanCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val Bool)
-> ProgramT instr (Param2 exp pred) m (exp Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChanCMD
  '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val Bool)
-> ProgramT instr (Param2 exp 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 exp pred) m, Param2 exp pred) (Val Bool)
 -> ProgramT instr (Param2 exp pred) m (exp Bool))
-> ChanCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 exp pred) (Val Bool)
-> ProgramT instr (Param2 exp pred) m (exp Bool)
forall a b. (a -> b) -> a -> b
$ Chan t c
-> exp i
-> exp i
-> Arr i a
-> ChanCMD
     '(ProgramT instr (Param2 exp pred) m, Param2 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
ch exp i
off exp i
sz Arr i a
arr