{-# LANGUAGE BlockArguments     #-}
{-# LANGUAGE GADTs              #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE LambdaCase         #-}

-- | This module defines `Choreo`, the monad for writing choreographies.
module Choreography.Choreo where

import Control.Applicative(empty)
import Control.Monad.State.Strict(StateT, execStateT, modify')
import Data.Foldable(foldMap')
import Data.Functor(($>))
import Data.List(delete)
import Data.Maybe(fromMaybe)
import Data.Proxy(Proxy(..))
import Data.Set(Set)
import Data.Set qualified as S
import GHC.TypeLits(KnownSymbol)

import Choreography.Location
import Choreography.Network
import Control.Monad.Freer

-- * The Choreo monad

-- | A constrained version of `unwrap` that only unwraps values located at a
-- specific location.
type Unwrap l = forall a. a @ l -> a

-- | Effect signature for the `Choreo` monad. @m@ is a monad that represents
-- local computations.
data ChoreoSig m a where
  Local :: (KnownSymbol l)
        => Proxy l
        -> (Unwrap l -> m a)
        -> ChoreoSig m (a @ l)

  Comm :: (Show a, Read a, KnownSymbol l, KnownSymbol l')
       => Proxy l
       -> a @ l
       -> Proxy l'
       -> ChoreoSig m (a @ l')

  Cond :: (Show a, Read a, KnownSymbol l)
       => Proxy l
       -> a @ l
       -> (a -> Choreo m b)
       -> ChoreoSig m b

  Cond_ :: (Bounded a, Enum a, Show a, Read a, KnownSymbol l)
        => Proxy l
        -> a @ l
        -> (a -> Choreo m (b @ l))
        -> ChoreoSig m (b @ l)

-- | Monad for writing choreographies.
type Choreo m = Freer (ChoreoSig m)

-- | Run a `Choreo` monad directly.
runChoreo :: Monad m => Choreo m a -> m a
runChoreo :: forall (m :: * -> *) a. Monad m => Choreo m a -> m a
runChoreo = (forall a1. ChoreoSig m a1 -> m a1) -> Freer (ChoreoSig m) a -> m a
forall (m :: * -> *) (f :: * -> *) a.
Monad m =>
(forall a1. f a1 -> m a1) -> Freer f a -> m a
interpFreer ChoreoSig m a1 -> m a1
forall a1. ChoreoSig m a1 -> m a1
forall (m :: * -> *) a. Monad m => ChoreoSig m a -> m a
handler
  where
    handler :: Monad m => ChoreoSig m a -> m a
    handler :: forall (m :: * -> *) a. Monad m => ChoreoSig m a -> m a
handler (Local Proxy l
_ Unwrap l -> m a
m)   = a -> a @ l
forall a (l :: Symbol). a -> a @ l
wrap (a -> a @ l) -> m a -> m (a @ l)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Unwrap l -> m a
m (a @ l) -> a
Unwrap l
forall a (l :: Symbol). (a @ l) -> a
unwrap
    handler (Comm Proxy l
_ a @ l
a Proxy l'
_)  = a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ (a -> a @ l'
forall a (l :: Symbol). a -> a @ l
wrap (a -> a @ l') -> ((a @ l) -> a) -> (a @ l) -> a @ l'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a @ l) -> a
forall a (l :: Symbol). (a @ l) -> a
unwrap) a @ l
a
    handler (Cond Proxy l
_ a @ l
a a -> Choreo m a
c)  = Choreo m a -> m a
forall (m :: * -> *) a. Monad m => Choreo m a -> m a
runChoreo (Choreo m a -> m a) -> Choreo m a -> m a
forall a b. (a -> b) -> a -> b
$ a -> Choreo m a
c ((a @ l) -> a
forall a (l :: Symbol). (a @ l) -> a
unwrap a @ l
a)
    handler (Cond_ Proxy l
_ a @ l
a a -> Choreo m (b @ l)
c) = Choreo m (b @ l) -> m (b @ l)
forall (m :: * -> *) a. Monad m => Choreo m a -> m a
runChoreo (Choreo m (b @ l) -> m (b @ l)) -> Choreo m (b @ l) -> m (b @ l)
forall a b. (a -> b) -> a -> b
$ a -> Choreo m (b @ l)
c ((a @ l) -> a
forall a (l :: Symbol). (a @ l) -> a
unwrap a @ l
a)

-- Static analysis

insertLoc :: KnownSymbol l => Proxy l -> Set LocTm -> Set LocTm
insertLoc :: forall (l :: Symbol).
KnownSymbol l =>
Proxy l -> Set LocTm -> Set LocTm
insertLoc = LocTm -> Set LocTm -> Set LocTm
forall a. Ord a => a -> Set a -> Set a
S.insert (LocTm -> Set LocTm -> Set LocTm)
-> (Proxy l -> LocTm) -> Proxy l -> Set LocTm -> Set LocTm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy l -> LocTm
forall (l :: Symbol). KnownSymbol l => Proxy l -> LocTm
toLocTm

insertLocs :: [LocTm] -> Set LocTm -> Set LocTm
insertLocs :: [LocTm] -> Set LocTm -> Set LocTm
insertLocs = Set LocTm -> Set LocTm -> Set LocTm
forall a. Ord a => Set a -> Set a -> Set a
S.union (Set LocTm -> Set LocTm -> Set LocTm)
-> ([LocTm] -> Set LocTm) -> [LocTm] -> Set LocTm -> Set LocTm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [LocTm] -> Set LocTm
forall a. Ord a => [a] -> Set a
S.fromList

-- | Apply function `f` to every possible value of type `a`, and collect all the resulting `participants`.
enumerate :: (Bounded a, Enum a) => [LocTm] -> (a -> Choreo m b) -> Set LocTm
enumerate :: forall a (m :: * -> *) b.
(Bounded a, Enum a) =>
[LocTm] -> (a -> Choreo m b) -> Set LocTm
enumerate [LocTm]
ls a -> Choreo m b
f = (a -> Set LocTm) -> [a] -> Set LocTm
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap' ([LocTm] -> Choreo m b -> Set LocTm
forall (m :: * -> *) a. [LocTm] -> Choreo m a -> Set LocTm
participants [LocTm]
ls (Choreo m b -> Set LocTm) -> (a -> Choreo m b) -> a -> Set LocTm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Choreo m b
f) [a
forall a. Bounded a => a
minBound ..]

-- | Compute the set of locations participating in this choreography.
participants :: [LocTm] -> Choreo m a -> Set LocTm
participants :: forall (m :: * -> *) a. [LocTm] -> Choreo m a -> Set LocTm
participants [LocTm]
ls = Set LocTm -> Maybe (Set LocTm) -> Set LocTm
forall a. a -> Maybe a -> a
fromMaybe ([LocTm] -> Set LocTm
forall a. Ord a => [a] -> Set a
S.fromList [LocTm]
ls) (Maybe (Set LocTm) -> Set LocTm)
-> (Freer (ChoreoSig m) a -> Maybe (Set LocTm))
-> Freer (ChoreoSig m) a
-> Set LocTm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StateT (Set LocTm) Maybe a -> Set LocTm -> Maybe (Set LocTm)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
`execStateT` Set LocTm
forall a. Set a
S.empty) (StateT (Set LocTm) Maybe a -> Maybe (Set LocTm))
-> (Freer (ChoreoSig m) a -> StateT (Set LocTm) Maybe a)
-> Freer (ChoreoSig m) a
-> Maybe (Set LocTm)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a1. ChoreoSig m a1 -> StateT (Set LocTm) Maybe a1)
-> Freer (ChoreoSig m) a -> StateT (Set LocTm) Maybe a
forall (m :: * -> *) (f :: * -> *) a.
Monad m =>
(forall a1. f a1 -> m a1) -> Freer f a -> m a
interpFreer ChoreoSig m a1 -> StateT (Set LocTm) Maybe a1
forall a1. ChoreoSig m a1 -> StateT (Set LocTm) Maybe a1
forall (m :: * -> *) a. ChoreoSig m a -> StateT (Set LocTm) Maybe a
handler
  where
    handler :: ChoreoSig m a -> StateT (Set LocTm) Maybe a
    handler :: forall (m :: * -> *) a. ChoreoSig m a -> StateT (Set LocTm) Maybe a
handler = \case
      Local Proxy l
l Unwrap l -> m a
_   -> (Set LocTm -> Set LocTm) -> StateT (Set LocTm) Maybe ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (Proxy l -> Set LocTm -> Set LocTm
forall (l :: Symbol).
KnownSymbol l =>
Proxy l -> Set LocTm -> Set LocTm
insertLoc Proxy l
l)                StateT (Set LocTm) Maybe () -> a -> StateT (Set LocTm) Maybe a
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> a
a @ l
forall a (l :: Symbol). a @ l
Empty
      Comm Proxy l
l a @ l
_ Proxy l'
l' -> (Set LocTm -> Set LocTm) -> StateT (Set LocTm) Maybe ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (Proxy l -> Set LocTm -> Set LocTm
forall (l :: Symbol).
KnownSymbol l =>
Proxy l -> Set LocTm -> Set LocTm
insertLoc Proxy l
l (Set LocTm -> Set LocTm)
-> (Set LocTm -> Set LocTm) -> Set LocTm -> Set LocTm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy l' -> Set LocTm -> Set LocTm
forall (l :: Symbol).
KnownSymbol l =>
Proxy l -> Set LocTm -> Set LocTm
insertLoc Proxy l'
l') StateT (Set LocTm) Maybe () -> a -> StateT (Set LocTm) Maybe a
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> a
a @ l'
forall a (l :: Symbol). a @ l
Empty
      Cond Proxy l
_ a @ l
_ a -> Choreo m a
_  -> (Set LocTm -> Set LocTm) -> StateT (Set LocTm) Maybe ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' ([LocTm] -> Set LocTm -> Set LocTm
insertLocs [LocTm]
ls)              StateT (Set LocTm) Maybe ()
-> StateT (Set LocTm) Maybe a -> StateT (Set LocTm) Maybe a
forall a b.
StateT (Set LocTm) Maybe a
-> StateT (Set LocTm) Maybe b -> StateT (Set LocTm) Maybe b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT (Set LocTm) Maybe a
forall a. StateT (Set LocTm) Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
      Cond_ Proxy l
l a @ l
_ a -> Choreo m (b @ l)
f -> (Set LocTm -> Set LocTm) -> StateT (Set LocTm) Maybe ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (Proxy l -> Set LocTm -> Set LocTm
forall (l :: Symbol).
KnownSymbol l =>
Proxy l -> Set LocTm -> Set LocTm
insertLoc Proxy l
l (Set LocTm -> Set LocTm)
-> (Set LocTm -> Set LocTm) -> Set LocTm -> Set LocTm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set LocTm -> Set LocTm -> Set LocTm
forall a. Ord a => Set a -> Set a -> Set a
S.union ([LocTm] -> (a -> Choreo m (b @ l)) -> Set LocTm
forall a (m :: * -> *) b.
(Bounded a, Enum a) =>
[LocTm] -> (a -> Choreo m b) -> Set LocTm
enumerate [LocTm]
ls a -> Choreo m (b @ l)
f)) StateT (Set LocTm) Maybe () -> a -> StateT (Set LocTm) Maybe a
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> a
b @ l
forall a (l :: Symbol). a @ l
Empty

-- | Endpoint projection.
epp :: [LocTm] -> Choreo m a -> LocTm -> Network m a
epp :: forall (m :: * -> *) a.
[LocTm] -> Choreo m a -> LocTm -> Network m a
epp [LocTm]
ls Choreo m a
c LocTm
l' = (forall a1. ChoreoSig m a1 -> Freer (NetworkSig m) a1)
-> Choreo m a -> Freer (NetworkSig m) a
forall (m :: * -> *) (f :: * -> *) a.
Monad m =>
(forall a1. f a1 -> m a1) -> Freer f a -> m a
interpFreer ChoreoSig m a1 -> Network m a1
forall a1. ChoreoSig m a1 -> Freer (NetworkSig m) a1
forall (m :: * -> *) a. ChoreoSig m a -> Network m a
handler Choreo m a
c
  where
    handler :: ChoreoSig m a -> Network m a
    handler :: forall (m :: * -> *) a. ChoreoSig m a -> Network m a
handler (Local Proxy l
l Unwrap l -> m a
m)
      | Proxy l -> LocTm
forall (l :: Symbol). KnownSymbol l => Proxy l -> LocTm
toLocTm Proxy l
l LocTm -> LocTm -> Bool
forall a. Eq a => a -> a -> Bool
== LocTm
l' = a -> a @ l
forall a (l :: Symbol). a -> a @ l
wrap (a -> a @ l)
-> Freer (NetworkSig m) a -> Freer (NetworkSig m) (a @ l)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a -> Freer (NetworkSig m) a
forall (m :: * -> *) a. m a -> Network m a
run (Unwrap l -> m a
m (a @ l) -> a
Unwrap l
forall a (l :: Symbol). (a @ l) -> a
unwrap)
      | Bool
otherwise       = a -> Freer (NetworkSig m) a
forall a. a -> Freer (NetworkSig m) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a @ l
forall a (l :: Symbol). a @ l
Empty
    handler (Comm Proxy l
s a @ l
a Proxy l'
r)
      | LocTm
l' LocTm -> LocTm -> Bool
forall a. Eq a => a -> a -> Bool
== LocTm
s' Bool -> Bool -> Bool
&& LocTm
s' LocTm -> LocTm -> Bool
forall a. Eq a => a -> a -> Bool
== LocTm
r' = a -> Freer (NetworkSig m) a
forall a. a -> Freer (NetworkSig m) a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Freer (NetworkSig m) a) -> a -> Freer (NetworkSig m) a
forall a b. (a -> b) -> a -> b
$ a -> a @ l'
forall a (l :: Symbol). a -> a @ l
wrap ((a @ l) -> a
forall a (l :: Symbol). (a @ l) -> a
unwrap a @ l
a)
      | LocTm
s' LocTm -> LocTm -> Bool
forall a. Eq a => a -> a -> Bool
== LocTm
l'             = a -> LocTm -> Network m ()
forall a (m :: * -> *). Show a => a -> LocTm -> Network m ()
send ((a @ l) -> a
forall a (l :: Symbol). (a @ l) -> a
unwrap a @ l
a) LocTm
r' Network m () -> Freer (NetworkSig m) a -> Freer (NetworkSig m) a
forall a b.
Freer (NetworkSig m) a
-> Freer (NetworkSig m) b -> Freer (NetworkSig m) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> Freer (NetworkSig m) a
forall a. a -> Freer (NetworkSig m) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a @ l'
forall a (l :: Symbol). a @ l
Empty
      | LocTm
r' LocTm -> LocTm -> Bool
forall a. Eq a => a -> a -> Bool
== LocTm
l'             = a -> a @ l'
forall a (l :: Symbol). a -> a @ l
wrap (a -> a @ l')
-> Freer (NetworkSig m) a -> Freer (NetworkSig m) (a @ l')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LocTm -> Freer (NetworkSig m) a
forall a (m :: * -> *). Read a => LocTm -> Network m a
recv LocTm
s'
      | Bool
otherwise            = a -> Freer (NetworkSig m) a
forall a. a -> Freer (NetworkSig m) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a @ l'
forall a (l :: Symbol). a @ l
Empty
      where
        s' :: LocTm
s' = Proxy l -> LocTm
forall (l :: Symbol). KnownSymbol l => Proxy l -> LocTm
toLocTm Proxy l
s
        r' :: LocTm
r' = Proxy l' -> LocTm
forall (l :: Symbol). KnownSymbol l => Proxy l -> LocTm
toLocTm Proxy l'
r
    handler (Cond Proxy l
l a @ l
a a -> Choreo m a
c)
      | Proxy l -> LocTm
forall (l :: Symbol). KnownSymbol l => Proxy l -> LocTm
toLocTm Proxy l
l LocTm -> LocTm -> Bool
forall a. Eq a => a -> a -> Bool
== LocTm
l' = a -> [LocTm] -> Network m ()
forall a (m :: * -> *). Show a => a -> [LocTm] -> Network m ()
broadcast ((a @ l) -> a
forall a (l :: Symbol). (a @ l) -> a
unwrap a @ l
a) (LocTm -> [LocTm] -> [LocTm]
forall a. Eq a => a -> [a] -> [a]
delete LocTm
l' [LocTm]
ls) Network m () -> Freer (NetworkSig m) a -> Freer (NetworkSig m) a
forall a b.
Freer (NetworkSig m) a
-> Freer (NetworkSig m) b -> Freer (NetworkSig m) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [LocTm] -> Choreo m a -> LocTm -> Freer (NetworkSig m) a
forall (m :: * -> *) a.
[LocTm] -> Choreo m a -> LocTm -> Network m a
epp [LocTm]
ls (a -> Choreo m a
c ((a @ l) -> a
forall a (l :: Symbol). (a @ l) -> a
unwrap a @ l
a)) LocTm
l'
      | Bool
otherwise       = LocTm -> Network m a
forall a (m :: * -> *). Read a => LocTm -> Network m a
recv (Proxy l -> LocTm
forall (l :: Symbol). KnownSymbol l => Proxy l -> LocTm
toLocTm Proxy l
l) Network m a
-> (a -> Freer (NetworkSig m) a) -> Freer (NetworkSig m) a
forall a b.
Freer (NetworkSig m) a
-> (a -> Freer (NetworkSig m) b) -> Freer (NetworkSig m) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x -> [LocTm] -> Choreo m a -> LocTm -> Freer (NetworkSig m) a
forall (m :: * -> *) a.
[LocTm] -> Choreo m a -> LocTm -> Network m a
epp [LocTm]
ls (a -> Choreo m a
c a
x) LocTm
l'
    handler (Cond_ Proxy l
pl a @ l
a a -> Choreo m (b @ l)
c)
      | LocTm
l LocTm -> LocTm -> Bool
forall a. Eq a => a -> a -> Bool
== LocTm
l'         = a -> [LocTm] -> Network m ()
forall a (m :: * -> *). Show a => a -> [LocTm] -> Network m ()
broadcast ((a @ l) -> a
forall a (l :: Symbol). (a @ l) -> a
unwrap a @ l
a) (Set LocTm -> [LocTm]
forall a. Set a -> [a]
S.toList (Set LocTm -> [LocTm]) -> Set LocTm -> [LocTm]
forall a b. (a -> b) -> a -> b
$ LocTm -> Set LocTm -> Set LocTm
forall a. Ord a => a -> Set a -> Set a
S.delete LocTm
l Set LocTm
ls') Network m ()
-> Freer (NetworkSig m) (b @ l) -> Freer (NetworkSig m) (b @ l)
forall a b.
Freer (NetworkSig m) a
-> Freer (NetworkSig m) b -> Freer (NetworkSig m) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [LocTm]
-> Choreo m (b @ l) -> LocTm -> Freer (NetworkSig m) (b @ l)
forall (m :: * -> *) a.
[LocTm] -> Choreo m a -> LocTm -> Network m a
epp [LocTm]
ls (a -> Choreo m (b @ l)
c ((a @ l) -> a
forall a (l :: Symbol). (a @ l) -> a
unwrap a @ l
a)) LocTm
l'
      | LocTm -> Set LocTm -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member LocTm
l' Set LocTm
ls' = LocTm -> Network m a
forall a (m :: * -> *). Read a => LocTm -> Network m a
recv LocTm
l Network m a
-> (a -> Freer (NetworkSig m) a) -> Freer (NetworkSig m) a
forall a b.
Freer (NetworkSig m) a
-> (a -> Freer (NetworkSig m) b) -> Freer (NetworkSig m) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x -> [LocTm]
-> Choreo m (b @ l) -> LocTm -> Freer (NetworkSig m) (b @ l)
forall (m :: * -> *) a.
[LocTm] -> Choreo m a -> LocTm -> Network m a
epp [LocTm]
ls (a -> Choreo m (b @ l)
c a
x) LocTm
l'
      | Bool
otherwise       = a -> Freer (NetworkSig m) a
forall a. a -> Freer (NetworkSig m) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
b @ l
forall a (l :: Symbol). a @ l
Empty
      where
        l :: LocTm
l = Proxy l -> LocTm
forall (l :: Symbol). KnownSymbol l => Proxy l -> LocTm
toLocTm Proxy l
pl
        ls' :: Set LocTm
ls' = [LocTm] -> (a -> Choreo m (b @ l)) -> Set LocTm
forall a (m :: * -> *) b.
(Bounded a, Enum a) =>
[LocTm] -> (a -> Choreo m b) -> Set LocTm
enumerate [LocTm]
ls a -> Choreo m (b @ l)
c

-- * Choreo operations

-- | Perform a local computation at a given location.
locally :: KnownSymbol l
        => Proxy l           -- ^ Location performing the local computation.
        -> (Unwrap l -> m a) -- ^ The local computation given a constrained
                             -- unwrap funciton.
        -> Choreo m (a @ l)
locally :: forall (l :: Symbol) (m :: * -> *) a.
KnownSymbol l =>
Proxy l -> (Unwrap l -> m a) -> Choreo m (a @ l)
locally Proxy l
l Unwrap l -> m a
m = ChoreoSig m (a @ l) -> Freer (ChoreoSig m) (a @ l)
forall (f :: * -> *) a. f a -> Freer f a
toFreer (Proxy l -> (Unwrap l -> m a) -> ChoreoSig m (a @ l)
forall (a :: Symbol) (m :: * -> *) l.
KnownSymbol a =>
Proxy a -> (Unwrap a -> m l) -> ChoreoSig m (l @ a)
Local Proxy l
l Unwrap l -> m a
m)

-- | Communication between a sender and a receiver.
(~>) :: (Show a, Read a, KnownSymbol l, KnownSymbol l')
     => (Proxy l, a @ l)  -- ^ A pair of a sender's location and a value located
                          -- at the sender
     -> Proxy l'          -- ^ A receiver's location.
     -> Choreo m (a @ l')
~> :: forall a (l :: Symbol) (l' :: Symbol) (m :: * -> *).
(Show a, Read a, KnownSymbol l, KnownSymbol l') =>
(Proxy l, a @ l) -> Proxy l' -> Choreo m (a @ l')
(~>) (Proxy l
l, a @ l
a) Proxy l'
l' = ChoreoSig m (a @ l') -> Freer (ChoreoSig m) (a @ l')
forall (f :: * -> *) a. f a -> Freer f a
toFreer (Proxy l -> (a @ l) -> Proxy l' -> ChoreoSig m (a @ l')
forall a (l :: Symbol) (b :: Symbol) (m :: * -> *).
(Show a, Read a, KnownSymbol l, KnownSymbol b) =>
Proxy l -> (a @ l) -> Proxy b -> ChoreoSig m (a @ b)
Comm Proxy l
l a @ l
a Proxy l'
l')

-- | Conditionally execute choreographies based on a located value.
cond :: (Show a, Read a, KnownSymbol l)
     => (Proxy l, a @ l)  -- ^ A pair of a location and a scrutinee located on
                          -- it.
     -> (a -> Choreo m b) -- ^ A function that describes the follow-up
                          -- choreographies based on the value of scrutinee.
     -> Choreo m b
cond :: forall a (l :: Symbol) (m :: * -> *) b.
(Show a, Read a, KnownSymbol l) =>
(Proxy l, a @ l) -> (a -> Choreo m b) -> Choreo m b
cond (Proxy l
l, a @ l
a) a -> Choreo m b
c = ChoreoSig m b -> Choreo m b
forall (f :: * -> *) a. f a -> Freer f a
toFreer (Proxy l -> (a @ l) -> (a -> Choreo m b) -> ChoreoSig m b
forall a (l :: Symbol) (m :: * -> *) b.
(Show a, Read a, KnownSymbol l) =>
Proxy l -> (a @ l) -> (a -> Choreo m b) -> ChoreoSig m b
Cond Proxy l
l a @ l
a a -> Choreo m b
c)

-- | Conditionally execute choreographies at participating locations,
-- based on a located value.
cond_ :: (Bounded a, Enum a, Show a, Read a, KnownSymbol l)
      => (Proxy l, a @ l)        -- ^ A pair of a location and a scrutinee located on
                                 -- it.
      -> (a -> Choreo m (b @ l)) -- ^ A function that describes the follow-up
                                 -- choreographies based on the value of scrutinee.
      -> Choreo m (b @ l)
cond_ :: forall a (l :: Symbol) (m :: * -> *) b.
(Bounded a, Enum a, Show a, Read a, KnownSymbol l) =>
(Proxy l, a @ l) -> (a -> Choreo m (b @ l)) -> Choreo m (b @ l)
cond_ (Proxy l
l, a @ l
a) a -> Choreo m (b @ l)
c = ChoreoSig m (b @ l) -> Choreo m (b @ l)
forall (f :: * -> *) a. f a -> Freer f a
toFreer (Proxy l
-> (a @ l) -> (a -> Choreo m (b @ l)) -> ChoreoSig m (b @ l)
forall a (l :: Symbol) (m :: * -> *) b.
(Bounded a, Enum a, Show a, Read a, KnownSymbol l) =>
Proxy l
-> (a @ l) -> (a -> Choreo m (b @ l)) -> ChoreoSig m (b @ l)
Cond_ Proxy l
l a @ l
a a -> Choreo m (b @ l)
c)

-- | A variant of `~>` that sends the result of a local computation.
(~~>) :: (Show a, Read a, KnownSymbol l, KnownSymbol l')
      => (Proxy l, Unwrap l -> m a) -- ^ A pair of a sender's location and a local
                                    -- computation.
      -> Proxy l'                   -- ^ A receiver's location.
      -> Choreo m (a @ l')
~~> :: forall a (l :: Symbol) (l' :: Symbol) (m :: * -> *).
(Show a, Read a, KnownSymbol l, KnownSymbol l') =>
(Proxy l, Unwrap l -> m a) -> Proxy l' -> Choreo m (a @ l')
(~~>) (Proxy l
l, Unwrap l -> m a
m) Proxy l'
l' = do
  a @ l
x <- Proxy l
l Proxy l -> (Unwrap l -> m a) -> Choreo m (a @ l)
forall (l :: Symbol) (m :: * -> *) a.
KnownSymbol l =>
Proxy l -> (Unwrap l -> m a) -> Choreo m (a @ l)
`locally` Unwrap l -> m a
m
  (Proxy l
l, a @ l
x) (Proxy l, a @ l) -> Proxy l' -> Choreo m (a @ l')
forall a (l :: Symbol) (l' :: Symbol) (m :: * -> *).
(Show a, Read a, KnownSymbol l, KnownSymbol l') =>
(Proxy l, a @ l) -> Proxy l' -> Choreo m (a @ l')
~> Proxy l'
l'

-- | A variant of `cond` that conditonally executes choregraphies based on the
-- result of a local computation.
cond' :: (Show a, Read a, KnownSymbol l)
      => (Proxy l, Unwrap l -> m a) -- ^ A pair of a location and a local
                                    -- computation.
      -> (a -> Choreo m b)          -- ^ A function that describes the follow-up
                                    -- choreographies based on the result of the
                                    -- local computation.
      -> Choreo m b
cond' :: forall a (l :: Symbol) (m :: * -> *) b.
(Show a, Read a, KnownSymbol l) =>
(Proxy l, Unwrap l -> m a) -> (a -> Choreo m b) -> Choreo m b
cond' (Proxy l
l, Unwrap l -> m a
m) a -> Choreo m b
c = do
  a @ l
x <- Proxy l
l Proxy l -> (Unwrap l -> m a) -> Choreo m (a @ l)
forall (l :: Symbol) (m :: * -> *) a.
KnownSymbol l =>
Proxy l -> (Unwrap l -> m a) -> Choreo m (a @ l)
`locally` Unwrap l -> m a
m
  (Proxy l, a @ l) -> (a -> Choreo m b) -> Choreo m b
forall a (l :: Symbol) (m :: * -> *) b.
(Show a, Read a, KnownSymbol l) =>
(Proxy l, a @ l) -> (a -> Choreo m b) -> Choreo m b
cond (Proxy l
l, a @ l
x) a -> Choreo m b
c

-- | A variant of `cond_` that conditonally executes choregraphies at participating locations,
-- based on the result of a local computation.
cond_' :: (Bounded a, Enum a, Show a, Read a, KnownSymbol l)
       => (Proxy l, Unwrap l -> m a) -- ^ A pair of a location and a local
                                     -- computation.
       -> (a -> Choreo m (b @ l))    -- ^ A function that describes the follow-up
                                     -- choreographies based on the result of the
                                     -- local computation.
       -> Choreo m (b @ l)
cond_' :: forall a (l :: Symbol) (m :: * -> *) b.
(Bounded a, Enum a, Show a, Read a, KnownSymbol l) =>
(Proxy l, Unwrap l -> m a)
-> (a -> Choreo m (b @ l)) -> Choreo m (b @ l)
cond_' (Proxy l
l, Unwrap l -> m a
m) a -> Choreo m (b @ l)
c = do
  a @ l
x <- Proxy l
l Proxy l -> (Unwrap l -> m a) -> Choreo m (a @ l)
forall (l :: Symbol) (m :: * -> *) a.
KnownSymbol l =>
Proxy l -> (Unwrap l -> m a) -> Choreo m (a @ l)
`locally` Unwrap l -> m a
m
  (Proxy l, a @ l) -> (a -> Choreo m (b @ l)) -> Choreo m (b @ l)
forall a (l :: Symbol) (m :: * -> *) b.
(Bounded a, Enum a, Show a, Read a, KnownSymbol l) =>
(Proxy l, a @ l) -> (a -> Choreo m (b @ l)) -> Choreo m (b @ l)
cond_ (Proxy l
l, a @ l
x) a -> Choreo m (b @ l)
c