-- | A zoo of helpful derived functions for writing choreographies.
module Choreography.Choreography.Batteries where

import Choreography.Choreography
import Choreography.Core
import Choreography.Locations
import Control.Monad (void)
import GHC.TypeLits

-- * Computation /per se/

-- | Perform a local computation, yielding nothing.
locally_ ::
  (KnownSymbol l) =>
  Member l ps ->
  (Unwrap l -> m ()) ->
  Choreo ps m ()

infix 4 `locally_`

locally_ :: forall (l :: Symbol) (ps :: [Symbol]) (m :: * -> *).
KnownSymbol l =>
Member l ps -> (Unwrap l -> m ()) -> Choreo ps m ()
locally_ Member l ps
l Unwrap l -> m ()
m = Freer (ChoreoSig ps m) (Located '[l] ())
-> Freer (ChoreoSig ps m) ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Freer (ChoreoSig ps m) (Located '[l] ())
 -> Freer (ChoreoSig ps m) ())
-> Freer (ChoreoSig ps m) (Located '[l] ())
-> Freer (ChoreoSig ps m) ()
forall a b. (a -> b) -> a -> b
$ Member l ps
-> (Unwrap l -> m ()) -> Freer (ChoreoSig ps m) (Located '[l] ())
forall (l :: Symbol) (ps :: [Symbol]) (m :: * -> *) a.
KnownSymbol l =>
Member l ps -> (Unwrap l -> m a) -> Choreo ps m (Located '[l] a)
locally Member l ps
l Unwrap l -> m ()
m

-- | Perform a local computation that doesn't need to unwrap any existing `Located` values.
_locally ::
  (KnownSymbol l) =>
  Member l ps ->
  m a ->
  Choreo ps m (Located '[l] a)

infix 4 `_locally`

_locally :: forall (l :: Symbol) (ps :: [Symbol]) (m :: * -> *) a.
KnownSymbol l =>
Member l ps -> m a -> Choreo ps m (Located '[l] a)
_locally Member l ps
l m a
m = Member l ps
-> ((forall {ls :: [Symbol]} {a}. Member l ls -> Located ls a -> a)
    -> m a)
-> Freer (ChoreoSig ps m) (Located '[l] a)
forall (l :: Symbol) (ps :: [Symbol]) (m :: * -> *) a.
KnownSymbol l =>
Member l ps -> (Unwrap l -> m a) -> Choreo ps m (Located '[l] a)
locally Member l ps
l (((forall {ls :: [Symbol]} {a}. Member l ls -> Located ls a -> a)
  -> m a)
 -> Freer (ChoreoSig ps m) (Located '[l] a))
-> ((forall {ls :: [Symbol]} {a}. Member l ls -> Located ls a -> a)
    -> m a)
-> Freer (ChoreoSig ps m) (Located '[l] a)
forall a b. (a -> b) -> a -> b
$ m a
-> (forall {ls :: [Symbol]} {a}. Member l ls -> Located ls a -> a)
-> m a
forall a b. a -> b -> a
const m a
m

-- | Perform a local computation that doesn't need to unwrap any existing `Located` values and yields nothing.
_locally_ :: (KnownSymbol l) => Member l ps -> m () -> Choreo ps m ()

infix 4 `_locally_`

_locally_ :: forall (l :: Symbol) (ps :: [Symbol]) (m :: * -> *).
KnownSymbol l =>
Member l ps -> m () -> Choreo ps m ()
_locally_ Member l ps
l m ()
m = Freer (ChoreoSig ps m) (Located '[l] ())
-> Freer (ChoreoSig ps m) ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Freer (ChoreoSig ps m) (Located '[l] ())
 -> Freer (ChoreoSig ps m) ())
-> Freer (ChoreoSig ps m) (Located '[l] ())
-> Freer (ChoreoSig ps m) ()
forall a b. (a -> b) -> a -> b
$ Member l ps
-> (Unwrap l -> m ()) -> Freer (ChoreoSig ps m) (Located '[l] ())
forall (l :: Symbol) (ps :: [Symbol]) (m :: * -> *) a.
KnownSymbol l =>
Member l ps -> (Unwrap l -> m a) -> Choreo ps m (Located '[l] a)
locally Member l ps
l (m () -> Unwrap l -> m ()
forall a b. a -> b -> a
const m ()
m)

-- | Perform a pure computation at a single location.
purely ::
  forall l a ps m.
  (KnownSymbol l) =>
  Member l ps ->
  (Unwrap l -> a) ->
  Choreo ps m (Located '[l] a)

infix 4 `purely`

purely :: forall (l :: Symbol) a (ps :: [Symbol]) (m :: * -> *).
KnownSymbol l =>
Member l ps -> (Unwrap l -> a) -> Choreo ps m (Located '[l] a)
purely Member l ps
l Unwrap l -> a
a =
  Subset '[l] ps
-> (Unwraps '[l] -> a) -> Choreo ps m (Located '[l] a)
forall (ls :: [Symbol]) a (ps :: [Symbol]) (m :: * -> *).
KnownSymbols ls =>
Subset ls ps -> (Unwraps ls -> a) -> Choreo ps m (Located ls a)
congruently
    ((forall (x :: Symbol). Member x '[l] -> Member x ps)
-> Subset '[l] ps
forall {k} (xs :: [k]) (ys :: [k]).
(forall (x :: k). Member x xs -> Member x ys) -> Subset xs ys
Subset \Member x '[l]
First -> Member l ps
Member x ps
l)
    ( \Unwraps '[l]
un ->
        let un' :: Unwrap l -- There is definitley a nicer way to write this...
            un' :: Unwrap l
un' Member l ls
mem = Subset '[l] ls -> Located ls a -> a
Unwraps '[l]
un ((forall (x :: Symbol). Member x '[l] -> Member x ls)
-> Subset '[l] ls
forall {k} (xs :: [k]) (ys :: [k]).
(forall (x :: k). Member x xs -> Member x ys) -> Subset xs ys
Subset \Member x '[l]
First -> Member l ls
Member x ls
mem)
         in Unwrap l -> a
a Member l ls -> Located ls a -> a
Unwrap l
un'
    )

-- * Communication

-- | A variant of `~>` that sends the result of a local computation.
(~~>) ::
  forall a l ls' m ps.
  (Show a, Read a, KnownSymbol l, KnownSymbols ls') =>
  -- | A pair of a sender's location and a local computation.
  (Member l ps, Unwrap l -> m a) ->
  -- | A receiver's location.
  Subset ls' ps ->
  Choreo ps m (Located ls' a)

infix 4 ~~>

~~> :: forall a (l :: Symbol) (ls' :: [Symbol]) (m :: * -> *)
       (ps :: [Symbol]).
(Show a, Read a, KnownSymbol l, KnownSymbols ls') =>
(Member l ps, Unwrap l -> m a)
-> Subset ls' ps -> Choreo ps m (Located ls' a)
(~~>) (Member l ps
l, Unwrap l -> m a
m) Subset ls' ps
ls' = do
  Located '[l] a
x <- Member l ps -> (Unwrap l -> m a) -> Choreo ps m (Located '[l] a)
forall (l :: Symbol) (ps :: [Symbol]) (m :: * -> *) a.
KnownSymbol l =>
Member l ps -> (Unwrap l -> m a) -> Choreo ps m (Located '[l] a)
locally Member l ps
l Unwrap l -> m a
m
  (Member l ps
l, Located '[l] a
x) (Member l ps, Located '[l] a)
-> Subset ls' ps -> Choreo ps m (Located ls' a)
forall a (l :: Symbol) (ls' :: [Symbol]) s (ls :: [Symbol])
       (ps :: [Symbol]) (m :: * -> *).
(Show a, Read a, KnownSymbol l, KnownSymbols ls',
 CanSend s l a ls ps) =>
s -> Subset ls' ps -> Choreo ps m (Located ls' a)
~> Subset ls' ps
ls'

-- | A variant of `~>` that sends the result of a local action that doesn't use existing `Located` variables.
(-~>) ::
  forall a l ls' m ps.
  (Show a, Read a, KnownSymbol l, KnownSymbols ls') =>
  -- | A pair of a sender's location and a local computation.
  (Member l ps, m a) ->
  -- | A receiver's location.
  Subset ls' ps ->
  Choreo ps m (Located ls' a)

infix 4 -~>

-~> :: forall a (l :: Symbol) (ls' :: [Symbol]) (m :: * -> *)
       (ps :: [Symbol]).
(Show a, Read a, KnownSymbol l, KnownSymbols ls') =>
(Member l ps, m a) -> Subset ls' ps -> Choreo ps m (Located ls' a)
(-~>) (Member l ps
l, m a
m) Subset ls' ps
ls' = do
  Located '[l] a
x <- Member l ps
l Member l ps -> m a -> Choreo ps m (Located '[l] a)
forall (l :: Symbol) (ps :: [Symbol]) (m :: * -> *) a.
KnownSymbol l =>
Member l ps -> m a -> Choreo ps m (Located '[l] a)
`_locally` m a
m
  (Member l ps
l, Located '[l] a
x) (Member l ps, Located '[l] a)
-> Subset ls' ps -> Choreo ps m (Located ls' a)
forall a (l :: Symbol) (ls' :: [Symbol]) s (ls :: [Symbol])
       (ps :: [Symbol]) (m :: * -> *).
(Show a, Read a, KnownSymbol l, KnownSymbols ls',
 CanSend s l a ls ps) =>
s -> Subset ls' ps -> Choreo ps m (Located ls' a)
~> Subset ls' ps
ls'

-- | A variant of `~>` that doesn't use the local monad.
(*~>) ::
  forall a l ls' m ps.
  (Show a, Read a, KnownSymbol l, KnownSymbols ls') =>
  -- | A pair of a sender's location and a local computation.
  (Member l ps, Unwrap l -> a) ->
  -- | A receiver's location.
  Subset ls' ps ->
  Choreo ps m (Located ls' a)

infix 4 *~>

*~> :: forall a (l :: Symbol) (ls' :: [Symbol]) (m :: * -> *)
       (ps :: [Symbol]).
(Show a, Read a, KnownSymbol l, KnownSymbols ls') =>
(Member l ps, Unwrap l -> a)
-> Subset ls' ps -> Choreo ps m (Located ls' a)
(*~>) (Member l ps
l, Unwrap l -> a
m) Subset ls' ps
ls' = do
  Located '[l] a
x <- Member l ps
l Member l ps -> Subset '[] ps -> Subset '[l] ps
forall {k} (x :: k) (ys :: [k]) (xs :: [k]).
Member x ys -> Subset xs ys -> Subset (x : xs) ys
@@ Subset '[] ps
forall {k} (ys :: [k]). Subset '[] ys
nobody Subset '[l] ps
-> (Unwraps '[l] -> a) -> Choreo ps m (Located '[l] a)
forall (ls :: [Symbol]) a (ps :: [Symbol]) (m :: * -> *).
KnownSymbols ls =>
Subset ls ps -> (Unwraps ls -> a) -> Choreo ps m (Located ls a)
`congruently` \Unwraps '[l]
uns -> Unwrap l -> a
m (Unwrap l -> a) -> Unwrap l -> a
forall a b. (a -> b) -> a -> b
$ Subset '[l] ls -> Located ls a -> a
Unwraps '[l]
uns (Subset '[l] ls -> Located ls a -> a)
-> (Member l ls -> Subset '[l] ls)
-> Member l ls
-> Located ls a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Member l ls -> Subset '[] ls -> Subset '[l] ls
forall {k} (x :: k) (ys :: [k]) (xs :: [k]).
Member x ys -> Subset xs ys -> Subset (x : xs) ys
@@ Subset '[] ls
forall {k} (ys :: [k]). Subset '[] ys
nobody)
  (Member l ps
l, Located '[l] a
x) (Member l ps, Located '[l] a)
-> Subset ls' ps -> Choreo ps m (Located ls' a)
forall a (l :: Symbol) (ls' :: [Symbol]) s (ls :: [Symbol])
       (ps :: [Symbol]) (m :: * -> *).
(Show a, Read a, KnownSymbol l, KnownSymbols ls',
 CanSend s l a ls ps) =>
s -> Subset ls' ps -> Choreo ps m (Located ls' a)
~> Subset ls' ps
ls'

-- * Conclaves

-- | Conditionally execute choreographies based on a located value. Automatically conclaves.
cond ::
  (KnownSymbols ls) =>
  -- | Tuple: Proof all the parties involved know the branch-guard
  -- and are present, the branch guard
  (Subset ls ps, (Subset ls qs, Located qs a)) ->
  -- | The body of the conditional as a function from the unwrapped value.
  (a -> Choreo ls m b) ->
  Choreo ps m (Located ls b)
cond :: forall (ls :: [Symbol]) (ps :: [Symbol]) (qs :: [Symbol]) a
       (m :: * -> *) b.
KnownSymbols ls =>
(Subset ls ps, (Subset ls qs, Located qs a))
-> (a -> Choreo ls m b) -> Choreo ps m (Located ls b)
cond (Subset ls ps
ls, (Subset ls qs
owns, Located qs a
a)) a -> Choreo ls m b
c = Subset ls ps -> Choreo ls m b -> Choreo ps m (Located ls b)
forall (ls :: [Symbol]) (ps :: [Symbol]) (m :: * -> *) a.
KnownSymbols ls =>
Subset ls ps -> Choreo ls m a -> Choreo ps m (Located ls a)
conclave Subset ls ps
ls (Choreo ls m b -> Choreo ps m (Located ls b))
-> Choreo ls m b -> Choreo ps m (Located ls b)
forall a b. (a -> b) -> a -> b
$ Subset ls qs -> Located qs a -> Choreo ls m a
forall (ps :: [Symbol]) (qs :: [Symbol]) a (m :: * -> *).
KnownSymbols ps =>
Subset ps qs -> Located qs a -> Choreo ps m a
naked Subset ls qs
owns Located qs a
a Choreo ls m a -> (a -> Choreo ls m b) -> Choreo ls m b
forall a b.
Freer (ChoreoSig ls m) a
-> (a -> Freer (ChoreoSig ls m) b) -> Freer (ChoreoSig ls m) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Choreo ls m b
c