-- | Operations for writing choreographies.
module Choreography.Choreography where

import Choreography.Core
import Choreography.Locations
import Choreography.Locations.Batteries (ExplicitMember (..))
import GHC.TypeLits

-- * Computation /per se/

-- | Perform a local computation at a given location.
locally ::
  (KnownSymbol (l :: LocTy)) =>
  -- | Location performing the local computation.
  Member l ps ->
  -- | The local computation, which can use a constrained unwrap function.
  (Unwrap l -> m a) ->
  Choreo ps m (Located '[l] a)

infix 4 `locally`

locally :: forall (l :: LocTy) (ps :: [LocTy]) (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 = Subset '[l] ps -> Choreo '[l] m a -> Choreo ps m (Located '[l] a)
forall (ls :: [LocTy]) (ps :: [LocTy]) (m :: * -> *) a.
KnownSymbols ls =>
Subset ls ps -> Choreo ls m a -> Choreo ps m (Located ls a)
conclave (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) (Choreo '[l] m a -> Choreo ps m (Located '[l] a))
-> Choreo '[l] m a -> Choreo ps m (Located '[l] a)
forall a b. (a -> b) -> a -> b
$ (Unwrap l -> m a) -> Choreo '[l] m a
forall (l :: LocTy) (m :: * -> *) a.
KnownSymbol l =>
(Unwrap l -> m a) -> Choreo '[l] m a
locally' Unwrap l -> m a
m

-- | Perform the exact same pure computation in replicate at multiple locations.
--   The computation can not use anything local to an individual party, including their identity.
congruently ::
  forall ls a ps m.
  (KnownSymbols ls) =>
  Subset ls ps ->
  (Unwraps ls -> a) ->
  Choreo ps m (Located ls a)

infix 4 `congruently`

congruently :: forall (ls :: [LocTy]) a (ps :: [LocTy]) (m :: * -> *).
KnownSymbols ls =>
Subset ls ps -> (Unwraps ls -> a) -> Choreo ps m (Located ls a)
congruently Subset ls ps
ls Unwraps ls -> a
a = Subset ls ps -> Choreo ls m a -> Choreo ps m (Located ls a)
forall (ls :: [LocTy]) (ps :: [LocTy]) (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 a -> Choreo ps m (Located ls a))
-> Choreo ls m a -> Choreo ps m (Located ls a)
forall a b. (a -> b) -> a -> b
$ (Unwraps ls -> a) -> Choreo ls m a
forall (ls :: [LocTy]) a (m :: * -> *).
KnownSymbols ls =>
(Unwraps ls -> a) -> Choreo ls m a
congruently' Unwraps ls -> a
a

-- | Unwrap a value known to the entire census.
naked ::
  (KnownSymbols ps) =>
  Subset ps qs ->
  Located qs a ->
  Choreo ps m a
naked :: forall (ps :: [LocTy]) (qs :: [LocTy]) a (m :: * -> *).
KnownSymbols ps =>
Subset ps qs -> Located qs a -> Choreo ps m a
naked Subset ps qs
ownership Located qs a
a = (Unwraps ps -> a) -> Choreo ps m a
forall (ls :: [LocTy]) a (m :: * -> *).
KnownSymbols ls =>
(Unwraps ls -> a) -> Choreo ls m a
congruently' (\Unwraps ps
un -> Subset ps qs -> Located qs a -> a
Unwraps ps
un Subset ps qs
ownership Located qs a
a)

-- * Communication

-- | Writing out the first argument to `~>` can be done a few different ways depending on context, represented by this class.
class (KnownSymbol loc) => CanSend struct loc val owners census | struct -> loc val owners census where
  presentToSend :: struct -> Member loc census
  ownsMessagePayload :: struct -> Member loc owners
  structMessagePayload :: struct -> Located owners val

instance (KnownSymbol l) => CanSend (Member l ps, (Member l ls, Located ls a)) l a ls ps where
  presentToSend :: (Member l ps, (Member l ls, Located ls a)) -> Member l ps
presentToSend = (Member l ps, (Member l ls, Located ls a)) -> Member l ps
forall a b. (a, b) -> a
fst
  ownsMessagePayload :: (Member l ps, (Member l ls, Located ls a)) -> Member l ls
ownsMessagePayload = (Member l ls, Located ls a) -> Member l ls
forall a b. (a, b) -> a
fst ((Member l ls, Located ls a) -> Member l ls)
-> ((Member l ps, (Member l ls, Located ls a))
    -> (Member l ls, Located ls a))
-> (Member l ps, (Member l ls, Located ls a))
-> Member l ls
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Member l ps, (Member l ls, Located ls a))
-> (Member l ls, Located ls a)
forall a b. (a, b) -> b
snd
  structMessagePayload :: (Member l ps, (Member l ls, Located ls a)) -> Located ls a
structMessagePayload = (Member l ls, Located ls a) -> Located ls a
forall a b. (a, b) -> b
snd ((Member l ls, Located ls a) -> Located ls a)
-> ((Member l ps, (Member l ls, Located ls a))
    -> (Member l ls, Located ls a))
-> (Member l ps, (Member l ls, Located ls a))
-> Located ls a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Member l ps, (Member l ls, Located ls a))
-> (Member l ls, Located ls a)
forall a b. (a, b) -> b
snd

instance (KnownSymbol l, ExplicitMember l ls) => CanSend (Member l ps, Located ls a) l a ls ps where
  presentToSend :: (Member l ps, Located ls a) -> Member l ps
presentToSend = (Member l ps, Located ls a) -> Member l ps
forall a b. (a, b) -> a
fst
  ownsMessagePayload :: (Member l ps, Located ls a) -> Member l ls
ownsMessagePayload = Member l ls -> (Member l ps, Located ls a) -> Member l ls
forall a b. a -> b -> a
const Member l ls
forall k (x :: k) (xs :: [k]). ExplicitMember x xs => Member x xs
explicitMember
  structMessagePayload :: (Member l ps, Located ls a) -> Located ls a
structMessagePayload = (Member l ps, Located ls a) -> Located ls a
forall a b. (a, b) -> b
snd

instance (KnownSymbol l) => CanSend (Member l ls, Subset ls ps, Located ls a) l a ls ps where
  presentToSend :: (Member l ls, Subset ls ps, Located ls a) -> Member l ps
presentToSend (Member l ls
m, Subset ls ps
s, Located ls a
_) = Subset ls ps -> forall (x :: LocTy). Member x ls -> Member x ps
forall {k} (xs :: [k]) (ys :: [k]).
Subset xs ys -> forall (x :: k). Member x xs -> Member x ys
inSuper Subset ls ps
s Member l ls
m
  ownsMessagePayload :: (Member l ls, Subset ls ps, Located ls a) -> Member l ls
ownsMessagePayload (Member l ls
m, Subset ls ps
_, Located ls a
_) = Member l ls
m
  structMessagePayload :: (Member l ls, Subset ls ps, Located ls a) -> Located ls a
structMessagePayload (Member l ls
_, Subset ls ps
_, Located ls a
p) = Located ls a
p

-- | Send a value from one party to the entire census.
broadcast ::
  forall l a ps ls m s.
  (Show a, Read a, KnownSymbol l, KnownSymbols ps, CanSend s l a ls ps) =>
  s ->
  Choreo ps m a
broadcast :: forall (l :: LocTy) a (ps :: [LocTy]) (ls :: [LocTy]) (m :: * -> *)
       s.
(Show a, Read a, KnownSymbol l, KnownSymbols ps,
 CanSend s l a ls ps) =>
s -> Choreo ps m a
broadcast s
s = Member l ps -> (Member l ls, Located ls a) -> Choreo ps m a
forall a (l :: LocTy) (ps :: [LocTy]) (ls :: [LocTy])
       (m :: * -> *).
(Show a, Read a, KnownSymbol l) =>
Member l ps -> (Member l ls, Located ls a) -> Choreo ps m a
broadcast' (s -> Member l ps
forall struct (loc :: LocTy) val (owners :: [LocTy])
       (census :: [LocTy]).
CanSend struct loc val owners census =>
struct -> Member loc census
presentToSend s
s) (s -> Member l ls
forall struct (loc :: LocTy) val (owners :: [LocTy])
       (census :: [LocTy]).
CanSend struct loc val owners census =>
struct -> Member loc owners
ownsMessagePayload s
s, s -> Located ls a
forall struct (loc :: LocTy) val (owners :: [LocTy])
       (census :: [LocTy]).
CanSend struct loc val owners census =>
struct -> Located owners val
structMessagePayload s
s)

-- | Communication between a sender and a list of receivers.
(~>) ::
  (Show a, Read a, KnownSymbol l, KnownSymbols ls', CanSend s l a ls ps) =>
  -- | The message argument can take three forms:
  --
  --   >  (Member sender census, wrapped owners a) -- where sender is explicitly listed in owners
  --
  --   >  (Member sender owners, Subset owners census, wrapped owners a)
  --
  --   >  (Member sender census, (Member sender owners, wrapped owners a)
  s ->
  -- | The recipients.
  Subset ls' ps ->
  Choreo ps m (Located ls' a)

infix 4 ~>

s
s ~> :: forall a (l :: LocTy) (ls' :: [LocTy]) s (ls :: [LocTy])
       (ps :: [LocTy]) (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
rs = do
  Located (l : ls') a
x :: a <- Subset (l : ls') ps
-> Choreo (l : ls') m a -> Choreo ps m (Located (l : ls') a)
forall (ls :: [LocTy]) (ps :: [LocTy]) (m :: * -> *) a.
KnownSymbols ls =>
Subset ls ps -> Choreo ls m a -> Choreo ps m (Located ls a)
conclave (s -> Member l ps
forall struct (loc :: LocTy) val (owners :: [LocTy])
       (census :: [LocTy]).
CanSend struct loc val owners census =>
struct -> Member loc census
presentToSend s
s Member l ps -> Subset ls' ps -> Subset (l : ls') ps
forall {k} (x :: k) (ys :: [k]) (xs :: [k]).
Member x ys -> Subset xs ys -> Subset (x : xs) ys
@@ Subset ls' ps
rs) (Choreo (l : ls') m a -> Choreo ps m (Located (l : ls') a))
-> Choreo (l : ls') m a -> Choreo ps m (Located (l : ls') a)
forall a b. (a -> b) -> a -> b
$ Member l (l : ls')
-> (Member l ls, Located ls a) -> Choreo (l : ls') m a
forall a (l :: LocTy) (ps :: [LocTy]) (ls :: [LocTy])
       (m :: * -> *).
(Show a, Read a, KnownSymbol l) =>
Member l ps -> (Member l ls, Located ls a) -> Choreo ps m a
broadcast' Member l (l : ls')
forall {k} (xs1 :: [k]) (x :: k) (xs' :: [k]).
(xs1 ~ (x : xs')) =>
Member x (x : xs')
First (s -> Member l ls
forall struct (loc :: LocTy) val (owners :: [LocTy])
       (census :: [LocTy]).
CanSend struct loc val owners census =>
struct -> Member loc owners
ownsMessagePayload s
s, s -> Located ls a
forall struct (loc :: LocTy) val (owners :: [LocTy])
       (census :: [LocTy]).
CanSend struct loc val owners census =>
struct -> Located owners val
structMessagePayload s
s)
  Subset ls' ps -> (Unwraps ls' -> a) -> Choreo ps m (Located ls' a)
forall (ls :: [LocTy]) a (ps :: [LocTy]) (m :: * -> *).
KnownSymbols ls =>
Subset ls ps -> (Unwraps ls -> a) -> Choreo ps m (Located ls a)
congruently Subset ls' ps
rs (\Unwraps ls'
un -> Subset ls' (l : ls') -> Located (l : ls') a -> a
Unwraps ls'
un Subset ls' (l : ls')
forall {a} (xs :: [a]) (x :: a) (xs' :: [a]).
(xs ~ (x : xs')) =>
Subset xs' (x : xs')
consSet Located (l : ls') a
x)

-- * Conclaves

-- | Lift a choreography involving fewer parties into the larger party space.
--   This version, where the returned value is Located at the entire conclave, does not add a Located layer.
conclaveToAll :: forall ls a ps m. (KnownSymbols ls) => Subset ls ps -> Choreo ls m (Located ls a) -> Choreo ps m (Located ls a)

infix 4 `conclaveToAll`

conclaveToAll :: forall (ls :: [LocTy]) a (ps :: [LocTy]) (m :: * -> *).
KnownSymbols ls =>
Subset ls ps
-> Choreo ls m (Located ls a) -> Choreo ps m (Located ls a)
conclaveToAll = (Subset ls ps
-> Subset ls ls
-> Choreo ls m (Located ls a)
-> Choreo ps m (Located ls a)
forall (ls :: [LocTy]) a (rs :: [LocTy]) (ps :: [LocTy])
       (m :: * -> *).
KnownSymbols ls =>
Subset ls ps
-> Subset rs ls
-> Choreo ls m (Located rs a)
-> Choreo ps m (Located rs a)
`conclaveTo` (forall (xs :: [LocTy]). Subset xs xs
forall {k} (xs :: [k]). Subset xs xs
refl @ls))

-- | Lift a choreography of involving fewer parties into the larger party space.
--   This version, where the returned value is already Located, does not add a Located layer.
conclaveTo ::
  forall ls a rs ps m.
  (KnownSymbols ls) =>
  Subset ls ps ->
  Subset rs ls ->
  Choreo ls m (Located rs a) ->
  Choreo ps m (Located rs a)

infix 4 `conclaveTo`

conclaveTo :: forall (ls :: [LocTy]) a (rs :: [LocTy]) (ps :: [LocTy])
       (m :: * -> *).
KnownSymbols ls =>
Subset ls ps
-> Subset rs ls
-> Choreo ls m (Located rs a)
-> Choreo ps m (Located rs a)
conclaveTo Subset ls ps
subcensus Subset rs ls
recipients Choreo ls m (Located rs a)
ch = Subset rs ls
-> Subset rs rs -> Located ls (Located rs a) -> Located rs a
forall (ls :: [LocTy]) (ms :: [LocTy]) (ns :: [LocTy]) a.
Subset ls ms
-> Subset ls ns -> Located ms (Located ns a) -> Located ls a
flatten Subset rs ls
recipients (forall (xs :: [LocTy]). Subset xs xs
forall {k} (xs :: [k]). Subset xs xs
refl @rs) (Located ls (Located rs a) -> Located rs a)
-> Freer (ChoreoSig ps m) (Located ls (Located rs a))
-> Freer (ChoreoSig ps m) (Located rs a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Subset ls ps
subcensus Subset ls ps
-> Choreo ls m (Located rs a)
-> Freer (ChoreoSig ps m) (Located ls (Located rs a))
forall (ls :: [LocTy]) (ps :: [LocTy]) (m :: * -> *) a.
KnownSymbols ls =>
Subset ls ps -> Choreo ls m a -> Choreo ps m (Located ls a)
`conclave` Choreo ls m (Located rs a)
ch)