-- | This module defines `Choreo`, the monad for writing choreographies,
--   and the closely related `Located` data type.
--   Not everything here is user-friendly; this is were we declare the foundational concepts.
--   These get repackaged in more convienent ways in "Choreography.Choreography"
--   and "Choreography.Choreography.Batteries".
module Choreography.Core
  ( -- * The `Choreo` monad and its operators
    Choreo,
    broadcast',
    -- , ChoreoSig(..)  I can't think of any reasons why we _should_ export this, nor any reason why we shouldn't...
    locally',
    congruently',
    conclave,

    -- * Running choreographies
    epp,
    runChoreo,

    -- * Located values
    Located (),
    Unwrap,
    Unwraps,
    flatten,
    othersForget,
    wrap, -- consider renaming or removing.
  )
where

import Choreography.Locations
import Choreography.Network
import Control.Monad.Freer
import Data.List (delete)
import GHC.TypeLits

-- | A single value known to many parties.
data Located (ls :: [LocTy]) a
  = Wrap a
  | Empty

-- | Wrap a value as a located value.
--   This should be safe to export, while exporting the constuctor would enable pattern matching.
wrap :: a -> Located l a
wrap :: forall a (l :: [LocTy]). a -> Located l a
wrap = a -> Located l a
forall (ls :: [LocTy]) a. a -> Located ls a
Wrap

-- | Unwraps values known to the specified party.
--   You should not be able to build such a function in normal code;
--   these functions are afforded only for use in "local" computation.
type Unwrap (q :: LocTy) = forall ls a. Member q ls -> Located ls a -> a

-- | Unwraps values known to the specified list of parties.
--   You should not be able to build such a function in normal code;
--   these functions are afforded only for use in "local" computation.
--   (Could be dangerous if the list is empty,
--   but the API is designed so that no value of type `Unwraps '[]` will ever actually get evaluated.)
type Unwraps (qs :: [LocTy]) = forall ls a. Subset qs ls -> Located ls a -> a

-- | Unwrap a `Located` value.
--   Unwrapping a empty located value will throw an exception; THIS SHOULD NOT BE EXPORTED!
unwrap :: Unwrap q
unwrap :: forall (q :: LocTy) (ls :: [LocTy]) a.
Member q ls -> Located ls a -> a
unwrap Member q ls
_ (Wrap a
a) = a
a
unwrap Member q ls
_ Located ls a
Empty = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"Located: This should never happen for a well-typed choreography."

-- | Un-nest located values.
flatten :: Subset ls ms -> Subset ls ns -> Located ms (Located ns a) -> Located ls a

infix 3 `flatten`

flatten :: forall (ls :: [LocTy]) (ms :: [LocTy]) (ns :: [LocTy]) a.
Subset ls ms
-> Subset ls ns -> Located ms (Located ns a) -> Located ls a
flatten Subset ls ms
_ Subset ls ns
_ Located ms (Located ns a)
Empty = Located ls a
forall (ls :: [LocTy]) a. Located ls a
Empty
flatten Subset ls ms
_ Subset ls ns
_ (Wrap Located ns a
Empty) = Located ls a
forall (ls :: [LocTy]) a. Located ls a
Empty
flatten Subset ls ms
_ Subset ls ns
_ (Wrap (Wrap a
a)) = a -> Located ls a
forall (ls :: [LocTy]) a. a -> Located ls a
Wrap a
a

-- | Cast a `Located` value to a smaller ownership set; useful when working with functions whos arguments have explict ownership sets.
othersForget :: Subset ls owners -> Located owners a -> Located ls a
othersForget :: forall (ls :: [LocTy]) (owners :: [LocTy]) a.
Subset ls owners -> Located owners a -> Located ls a
othersForget Subset ls owners
_ Located owners a
Empty = Located ls a
forall (ls :: [LocTy]) a. Located ls a
Empty
othersForget Subset ls owners
_ (Wrap a
a) = a -> Located ls a
forall (ls :: [LocTy]) a. a -> Located ls a
Wrap a
a

data ChoreoSig (ps :: [LocTy]) m a where
  Locally ::
    (KnownSymbol l) =>
    (Unwrap l -> m a) ->
    ChoreoSig '[l] m a
  Congruently ::
    (KnownSymbols ls) =>
    (Unwraps ls -> a) ->
    ChoreoSig ls m a
  Broadcast ::
    (Show a, Read a, KnownSymbol l) =>
    Member l ps -> -- from
    (Member l ls, Located ls a) -> -- value
    ChoreoSig ps m a
  Conclave ::
    (KnownSymbols ls) =>
    Subset ls ps ->
    Choreo ls m b ->
    ChoreoSig ps m (Located ls b)

-- | Monad for writing choreographies.
--     @ps@ is the "census", the list of parties who are present in (that part of) the choreography.
--     @m@ is the local monad afforded to parties by `locally'`.
type Choreo ps m = Freer (ChoreoSig ps m) -- Haddock will complain about not knowning where ChoreoSig is. IDK how to fix it; maybe we should just export

-- | Run a `Choreo` monad with centralized semantics.
--   This basically pretends that the choreography is a single-threaded program and runs it all at once,
--   ignoring all the location aspects.
runChoreo :: forall p ps b m. (Monad m) => Choreo (p ': ps) m b -> m b
runChoreo :: forall (p :: LocTy) (ps :: [LocTy]) b (m :: * -> *).
Monad m =>
Choreo (p : ps) m b -> m b
runChoreo = (forall b. ChoreoSig (p : ps) m b -> m b)
-> Freer (ChoreoSig (p : ps) m) b -> m b
forall (m :: * -> *) (f :: * -> *) a.
Monad m =>
(forall b. f b -> m b) -> Freer f a -> m a
interpFreer ChoreoSig (p : ps) m b -> m b
forall a. Monad m => ChoreoSig (p : ps) m a -> m a
forall b. ChoreoSig (p : ps) m b -> m b
handler
  where
    handler :: (Monad m) => ChoreoSig (p ': ps) m a -> m a
    handler :: forall a. Monad m => ChoreoSig (p : ps) m a -> m a
handler (Locally Unwrap l -> m a
m) = Unwrap l -> m a
m Member l ls -> Located ls a -> a
Unwrap l
forall (q :: LocTy) (ls :: [LocTy]) a.
Member q ls -> Located ls a -> a
unwrap
    handler (Congruently Unwraps (p : ps) -> a
f) =
      let unwraps :: forall c ls. Subset (p ': ps) ls -> Located ls c -> c
          unwraps :: forall c (ls :: [LocTy]). Subset (p : ps) ls -> Located ls c -> c
unwraps = Member p ls -> Located ls c -> c
forall (q :: LocTy) (ls :: [LocTy]) a.
Member q ls -> Located ls a -> a
unwrap (Member p ls -> Located ls c -> c)
-> (Subset (p : ps) ls -> Member p ls)
-> Subset (p : ps) ls
-> Located ls c
-> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Subset forall (x :: LocTy). Member x (p : ps) -> Member x ls
mx) -> Member p (p : ps) -> Member p ls
forall (x :: LocTy). Member x (p : ps) -> Member x ls
mx Member p (p : ps)
forall {k} (xs1 :: [k]) (x :: k) (xs' :: [k]).
(xs1 ~ (x : xs')) =>
Member x (x : xs')
First) -- wish i could write this better.
       in a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> m a) -> (Unwraps (p : ps) -> a) -> Unwraps (p : ps) -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unwraps (p : ps) -> a
f (Unwraps (p : ps) -> m a) -> Unwraps (p : ps) -> m a
forall a b. (a -> b) -> a -> b
$ Subset (p : ps) ls -> Located ls a -> a
Unwraps (p : ps)
forall c (ls :: [LocTy]). Subset (p : ps) ls -> Located ls c -> c
unwraps
    handler (Broadcast Member l (p : ps)
_ (Member l ls
p, Located ls a
a)) = a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ Member l ls -> Located ls a -> a
forall (q :: LocTy) (ls :: [LocTy]) a.
Member q ls -> Located ls a -> a
unwrap Member l ls
p Located ls a
a
    handler (Conclave (Subset ls (p : ps)
_ :: Subset ls (p ': ps)) Choreo ls m b
c) = case forall (ls :: [LocTy]). KnownSymbols ls => TySpine ls
tySpine @ls of
      TySpine ls
TyNil -> a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
Located '[] b
forall (ls :: [LocTy]) a. Located ls a
Empty
      TySpine ls
TyCons -> b -> Located (h : ts) b
forall a (l :: [LocTy]). a -> Located l a
wrap (b -> Located (h : ts) b) -> m b -> m (Located (h : ts) b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Choreo (h : ts) m b -> m b
forall (p :: LocTy) (ps :: [LocTy]) b (m :: * -> *).
Monad m =>
Choreo (p : ps) m b -> m b
runChoreo Choreo ls m b
Choreo (h : ts) m b
c

-- | Endpoint projection.
epp ::
  forall ps b m.
  (Monad m, KnownSymbols ps) =>
  -- | A choreography
  Choreo ps m b ->
  -- | A `String` identifying a party.
  --   At present there is no enforcement that the party will actually be in the census of the choreography;
  --   some bugs may be possible if it is not.
  LocTm ->
  -- | Returns the implementation of the party's role in the choreography.
  Network m b
epp :: forall (ps :: [LocTy]) b (m :: * -> *).
(Monad m, KnownSymbols ps) =>
Choreo ps m b -> [Char] -> Network m b
epp Choreo ps m b
c [Char]
l' = (forall b. ChoreoSig ps m b -> Freer (NetworkSig m) b)
-> Choreo ps m b -> Freer (NetworkSig m) b
forall (m :: * -> *) (f :: * -> *) a.
Monad m =>
(forall b. f b -> m b) -> Freer f a -> m a
interpFreer ChoreoSig ps m b -> Network m b
forall b. ChoreoSig ps m b -> Freer (NetworkSig m) b
handler Choreo ps m b
c
  where
    handler :: ChoreoSig ps m a -> Network m a
    handler :: forall b. ChoreoSig ps m b -> Freer (NetworkSig m) b
handler (Locally Unwrap l -> m a
m) = m a -> Network m a
forall (m :: * -> *) a. m a -> Network m a
run (m a -> Network m a) -> m a -> Network m a
forall a b. (a -> b) -> a -> b
$ Unwrap l -> m a
m Member l ls -> Located ls a -> a
Unwrap l
forall (q :: LocTy) (ls :: [LocTy]) a.
Member q ls -> Located ls a -> a
unwrap
    handler (Congruently Unwraps ps -> a
f) =
      let unwraps :: forall c ls. Subset ps ls -> Located ls c -> c
          unwraps :: forall c (ls :: [LocTy]). Subset ps ls -> Located ls c -> c
unwraps = case forall (ls :: [LocTy]). KnownSymbols ls => TySpine ls
tySpine @ps of
            TySpine ps
TyNil -> [Char] -> Subset ps ls -> Located ls c -> c
forall a. HasCallStack => [Char] -> a
error [Char]
"Undefined projection: the census is empty."
            TySpine ps
TyCons -> Member h ls -> Located ls c -> c
forall (q :: LocTy) (ls :: [LocTy]) a.
Member q ls -> Located ls a -> a
unwrap (Member h ls -> Located ls c -> c)
-> (Subset ps ls -> Member h ls)
-> Subset ps ls
-> Located ls c
-> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Subset forall (x :: LocTy). Member x ps -> Member x ls
mx) -> Member h ps -> Member h ls
forall (x :: LocTy). Member x ps -> Member x ls
mx Member h ps
Member h (h : ts)
forall {k} (xs1 :: [k]) (x :: k) (xs' :: [k]).
(xs1 ~ (x : xs')) =>
Member x (x : xs')
First) -- wish i could write this better.
       in a -> Network m a
forall a. a -> Freer (NetworkSig m) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> Network m a)
-> (Unwraps ps -> a) -> Unwraps ps -> Network m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unwraps ps -> a
f (Unwraps ps -> Network m a) -> Unwraps ps -> Network m a
forall a b. (a -> b) -> a -> b
$ Subset ps ls -> Located ls a -> a
Unwraps ps
forall c (ls :: [LocTy]). Subset ps ls -> Located ls c -> c
unwraps
    handler (Broadcast Member l ps
s (Member l ls
l, Located ls a
a)) = do
      let sender :: [Char]
sender = Member l ps -> [Char]
forall (l :: LocTy) (ps :: [LocTy]).
KnownSymbol l =>
Member l ps -> [Char]
toLocTm Member l ps
s
      let otherRecipients :: [[Char]]
otherRecipients = [Char]
sender [Char] -> [[Char]] -> [[Char]]
forall a. Eq a => a -> [a] -> [a]
`delete` Subset ps ps -> [[Char]]
forall (ls :: [LocTy]) (ps :: [LocTy]).
KnownSymbols ls =>
Subset ls ps -> [[Char]]
toLocs (Subset ps ps
forall {k} (xs :: [k]). Subset xs xs
refl :: Subset ps ps)
      if [Char]
sender [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
l'
        then do
          a -> [[Char]] -> Network m ()
forall a (m :: * -> *). Show a => a -> [[Char]] -> Network m ()
send (Member l ls -> Located ls a -> a
forall (q :: LocTy) (ls :: [LocTy]) a.
Member q ls -> Located ls a -> a
unwrap Member l ls
l Located ls a
a) [[Char]]
otherRecipients
          a -> Network m a
forall a. a -> Freer (NetworkSig m) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> Network m a)
-> (Located ls a -> a) -> Located ls a -> Network m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Member l ls -> Located ls a -> a
forall (q :: LocTy) (ls :: [LocTy]) a.
Member q ls -> Located ls a -> a
unwrap Member l ls
l (Located ls a -> Network m a) -> Located ls a -> Network m a
forall a b. (a -> b) -> a -> b
$ Located ls a
a
        else [Char] -> Network m a
forall a (m :: * -> *). Read a => [Char] -> Network m a
recv [Char]
sender
    handler (Conclave Subset ls ps
proof Choreo ls m b
ch)
      | [Char]
l' [Char] -> [[Char]] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Subset ls ps -> [[Char]]
forall (ls :: [LocTy]) (ps :: [LocTy]).
KnownSymbols ls =>
Subset ls ps -> [[Char]]
toLocs Subset ls ps
proof = b -> Located ls b
forall a (l :: [LocTy]). a -> Located l a
wrap (b -> Located ls b)
-> Freer (NetworkSig m) b -> Freer (NetworkSig m) (Located ls b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Choreo ls m b -> [Char] -> Freer (NetworkSig m) b
forall (ps :: [LocTy]) b (m :: * -> *).
(Monad m, KnownSymbols ps) =>
Choreo ps m b -> [Char] -> Network m b
epp Choreo ls m b
ch [Char]
l'
      | Bool
otherwise = a -> Network m a
forall a. a -> Freer (NetworkSig m) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
Located ls b
forall (ls :: [LocTy]) a. Located ls a
Empty

-- | Access to the inner "local" monad.
--   Since the type of `locally'` restricts the census to a single party, you'll usually want to use
--   `Choreography.Choreography.locally` instead.
locally' ::
  (KnownSymbol l) =>
  -- | The local action(s), which can use an unwraper function.
  (Unwrap l -> m a) ->
  Choreo '[l] m a
locally' :: forall (l :: LocTy) (m :: * -> *) a.
KnownSymbol l =>
(Unwrap l -> m a) -> Choreo '[l] m a
locally' Unwrap l -> m a
m = ChoreoSig '[l] m a -> Freer (ChoreoSig '[l] m) a
forall (f :: * -> *) a. f a -> Freer f a
toFreer ((Unwrap l -> m a) -> ChoreoSig '[l] m a
forall (ls :: LocTy) (m :: * -> *) a.
KnownSymbol ls =>
(Unwrap ls -> m a) -> ChoreoSig '[ls] m a
Locally Unwrap l -> m a
m)

-- | Perform the exact same computation in replicate at all participating locations.
--   The computation can not use anything local to an individual party, including their identity.
congruently' ::
  (KnownSymbols ls) =>
  -- | The computation, which can use an unwraper function.
  (Unwraps ls -> a) ->
  Choreo ls m a

infix 4 `congruently'`

congruently' :: forall (ls :: [LocTy]) a (m :: * -> *).
KnownSymbols ls =>
(Unwraps ls -> a) -> Choreo ls m a
congruently' Unwraps ls -> a
f = ChoreoSig ls m a -> Freer (ChoreoSig ls m) a
forall (f :: * -> *) a. f a -> Freer f a
toFreer ((Unwraps ls -> a) -> ChoreoSig ls m a
forall (ls :: [LocTy]) a (m :: * -> *).
KnownSymbols ls =>
(Unwraps ls -> a) -> ChoreoSig ls m a
Congruently Unwraps ls -> a
f)

-- | Communicate a value to all present parties.
broadcast' ::
  (Show a, Read a, KnownSymbol l) =>
  -- | Proof the sender is present
  Member l ps ->
  -- | Proof the sender knows the value, the value.
  (Member l ls, Located ls a) ->
  Choreo ps m a

infix 4 `broadcast'`

broadcast' :: 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 ps
l (Member l ls, Located ls a)
a = ChoreoSig ps m a -> Freer (ChoreoSig ps m) a
forall (f :: * -> *) a. f a -> Freer f a
toFreer (Member l ps -> (Member l ls, Located ls a) -> ChoreoSig ps m a
forall a (ls :: LocTy) (ps :: [LocTy]) (b :: [LocTy])
       (m :: * -> *).
(Show a, Read a, KnownSymbol ls) =>
Member ls ps -> (Member ls b, Located b a) -> ChoreoSig ps m a
Broadcast Member l ps
l (Member l ls, Located ls a)
a)

-- | Lift a choreography of involving fewer parties into the larger party space.
--   Adds a `Located ls` layer to the return type.
conclave ::
  (KnownSymbols ls) =>
  Subset ls ps ->
  Choreo ls m a ->
  Choreo ps m (Located ls a)

infix 4 `conclave`

conclave :: 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
proof Choreo ls m a
ch = ChoreoSig ps m (Located ls a)
-> Freer (ChoreoSig ps m) (Located ls a)
forall (f :: * -> *) a. f a -> Freer f a
toFreer (ChoreoSig ps m (Located ls a)
 -> Freer (ChoreoSig ps m) (Located ls a))
-> ChoreoSig ps m (Located ls a)
-> Freer (ChoreoSig ps m) (Located ls a)
forall a b. (a -> b) -> a -> b
$ Subset ls ps -> Choreo ls m a -> ChoreoSig ps m (Located ls a)
forall (ls :: [LocTy]) (ps :: [LocTy]) (m :: * -> *) b.
KnownSymbols ls =>
Subset ls ps -> Choreo ls m b -> ChoreoSig ps m (Located ls b)
Conclave Subset ls ps
proof Choreo ls m a
ch