Merge pull request #12 from ShapeOfMatter/multicast

Multicast

examples/Bank2PC.hs

@@ -54,6 +54,7 @@ import Data.List.Split (splitOn)
 import Data.Maybe (mapMaybe)
 import Data.Proxy (Proxy(Proxy))
 import GHC.TypeLits (KnownSymbol, symbolVal)
+import Logic.Propositional (introAnd)
 import Test.QuickCheck (Arbitrary, arbitrary, elements, listOf, listOf1)
 import Text.Read (readMaybe)
 
@@ -63,7 +64,7 @@ $(mkLoc "alice")
 $(mkLoc "bob")
 type Participants = ["client", "coordinator", "alice", "bob"]
 
-type State = (Int @ "alice", Int @ "bob")
+type State = (Located '["alice"] Int, Located '["bob"] Int)
 
 type Action = (String, Int)
 
@@ -120,23 +121,23 @@ parse s = tx
 -- Otherwise, it will keep the state unchanged.
 handleTransaction :: (Monad m) =>
                      State ->
-                     Transaction @ "coordinator" ->
-                     Choreo Participants m (Bool @ "coordinator", State)
+                     Located '["coordinator"] Transaction  ->
+                     Choreo Participants m (Located '["coordinator"] Bool, State)
 handleTransaction (aliceBalance, bobBalance) tx = do
   -- Voting Phase
-  txa <- (coordinator, tx) ~> alice
-  voteAlice <- (alice, \un -> do { return $ fst $ validate "alice" (un aliceBalance) (un txa) }) ~~> coordinator
-  txb <- (coordinator, tx) ~> bob
-  voteBob <- (bob, \un -> do { return $ fst $ validate "bob" (un bobBalance) (un txb) }) ~~> coordinator
+  txa <- (coordinator `introAnd` coordinator, tx) ~> (alice @@ nobody)
+  voteAlice <- (alice, \un -> do { return $ fst $ validate "alice" (un alice aliceBalance) (un alice txa) }) ~~> (coordinator @@ nobody)
+  txb <- (coordinator `introAnd` coordinator, tx) ~> (bob @@ nobody)
+  voteBob <- (bob, \un -> do { return $ fst $ validate "bob" (un bob bobBalance) (un bob txb) }) ~~> (coordinator @@ nobody)
 
   -- Check if the transaction can be committed
-  canCommit <- coordinator `locally` \un -> do return $ un voteAlice && un voteBob
+  canCommit <- coordinator `locally` \un -> do return $ un coordinator voteAlice && un coordinator voteBob
 
   -- Commit Phase
-  cond (coordinator, canCommit) \case
+  cond (coordinator `introAnd` coordinator, canCommit) \case
     True -> do
-      aliceBalance' <- alice `locally` \un -> do return $ snd $ validate "alice" (un aliceBalance) (un txa)
-      bobBalance' <- bob `locally` \un -> do return $ snd $ validate "bob" (un bobBalance) (un txb)
+      aliceBalance' <- alice `locally` \un -> do return $ snd $ validate "alice" (un alice aliceBalance) (un alice txa)
+      bobBalance' <- bob `locally` \un -> do return $ snd $ validate "bob" (un bob bobBalance) (un bob txb)
       return (canCommit, (aliceBalance', bobBalance'))
     False -> do
       return (canCommit, (aliceBalance, bobBalance))
@@ -145,13 +146,13 @@ handleTransaction (aliceBalance, bobBalance) tx = do
 bank :: State -> Choreo Participants (CLI m) ()
 bank state = do
   tx <- (client, \_ -> parse <$> getstr "Command? (alice|bob {amount};)+"
-        ) ~~> coordinator
+        ) ~~> (coordinator @@ nobody)
   (committed, state') <- handleTransaction state tx
-  committed' <- (coordinator, committed) ~> client
-  client `locally_` \un -> putOutput "Committed?" (un committed')
-  alice `locally_` \un -> putOutput "Alice's balance:" (un (fst state'))
-  bob `locally_` \un -> putOutput "Bob's balance:" (un (snd state'))
-  cond' (coordinator, \un -> return $ null $ un tx) (`unless` bank state') -- repeat
+  committed' <- (coordinator `introAnd` coordinator, committed) ~> (client @@ nobody)
+  client `locally_` \un -> putOutput "Committed?" (un client committed')
+  alice `locally_` \un -> putOutput "Alice's balance:" (un alice (fst state'))
+  bob `locally_` \un -> putOutput "Bob's balance:" (un bob (snd state'))
+  cond' (coordinator, \un -> return $ null $ un coordinator tx) (`unless` bank state') -- repeat
 
 -- | `startBank` is a choreography that initializes the states and starts the bank application.
 startBank :: Choreo Participants (CLI m) ()

examples/Bookseller0Network.hs

@@ -25,26 +25,26 @@ buyer :: Network (CLI m) ()
 buyer = do
   budget <- run $ getInput @Int "Enter your total budget:"
   title <- run $ getstr "Enter the title of the book to buy:"
-  send title "seller"
+  send title ["seller"]
   price <- recv "seller"
   if price <= budget
   then do
-    send True "seller"
+    send True ["seller"]
     (deliveryDate :: Day) <- recv "seller"
     run $ putOutput "The book will be delivered on:" deliveryDate
   else do
-    send False "seller"
+    send False ["seller"]
     run $ putNote "The book's price is out of the budget"
 
 seller :: Network (CLI m) ()
 seller = do
   database <- run $ getInput "Enter the book database (for `Read`):"
   title <- recv "buyer"
-  send (database `priceOf` title) "buyer"
+  send (database `priceOf` title) ["buyer"]
   decision <- recv "buyer"
   if decision
   then do
-    send (database `deliveryDateOf` title) "buyer"
+    send (database `deliveryDateOf` title) ["buyer"]
   else do
     return ()
 

examples/Bookseller1Simple.hs

@@ -66,6 +66,8 @@ Homotopy Type Theory
 
 module Bookseller1Simple where
 
+import Logic.Propositional (introAnd)
+
 import Choreography
 import System.Environment
 
@@ -83,16 +85,16 @@ bookseller = do
   buyer_budget <- buyer `_locally` getInput "Enter your total budget:"
   title <- buyer `_locally` getstr "Enter the title of the book to buy:"
 
-  title' <- (buyer, title) ~> seller
-  price <- seller `locally` \un -> return $ priceOf (un database) (un title')
-  price' <- (seller, price) ~> buyer
-  decision <- buyer `locally` \un -> return $ un price' <= un buyer_budget
+  title' <- (buyer `introAnd` buyer, title) ~> (seller @@ nobody)
+  price <- seller `locally` \un -> return $ priceOf (un seller database) (un seller title')
+  price' <- (seller `introAnd` seller, price) ~> (buyer @@ nobody)
+  decision <- buyer `locally` \un -> return $ un buyer price' <= un buyer buyer_budget
 
-  cond (buyer, decision) \case
+  cond (buyer `introAnd` buyer, decision) \case
     True  -> do
-      deliveryDate  <- seller `locally` \un -> return $ deliveryDateOf (un database) (un title')
-      deliveryDate' <- (seller, deliveryDate) ~> buyer
-      buyer `locally_` \un -> putOutput "The book will be delivered on " $ un deliveryDate'
+      deliveryDate  <- seller `locally` \un -> return $ deliveryDateOf (un seller database) (un seller title')
+      deliveryDate' <- (seller `introAnd` seller, deliveryDate) ~> (buyer @@ nobody)
+      buyer `locally_` \un -> putOutput "The book will be delivered on:" $ un buyer deliveryDate'
     False -> do
       buyer `_locally_` putNote "The book's price is out of the budget"
 
@@ -101,17 +103,18 @@ bookseller' :: Choreo Participants (CLI m) ()
 bookseller' = do
   database <- seller `_locally` getInput "Enter the book database (for `Read`):"
   buyer_budget <- buyer `_locally` getInput "Enter your total budget:"
-  title <- (buyer, \_ -> getstr "Enter the title of the book to buy:") ~~> seller
-  price <- (seller, \un -> return $ priceOf (un database) (un title)) ~~> buyer
+  title <- (buyer, \_ -> getstr "Enter the title of the book to buy:") ~~> (seller @@ nobody)
+  price <- (seller, \un -> return $ priceOf (un seller database) (un seller title)) ~~> (buyer @@ nobody)
 
-  cond' (buyer, \un -> return $ un price <= un buyer_budget) \case
+  cond' (buyer, \un -> return $ un buyer price <= un buyer buyer_budget) \case
     True  -> do
-      deliveryDate <- (seller, \un -> return $ deliveryDateOf (un database) (un title)) ~~> buyer
-      buyer `locally_` \un -> putOutput "The book will be delivered on:" $ un deliveryDate
+      deliveryDate <- (seller, \un -> return $ deliveryDateOf (un seller database) (un seller title)) ~~> (buyer @@ nobody)
+      buyer `locally_` \un -> putOutput "The book will be delivered on:" $ un buyer deliveryDate
     False -> do
       buyer `_locally_` putNote "The book's price is out of the budget"
 
 
+
 main :: IO ()
 main = do
   [loc] <- getArgs

examples/Bookseller2HigherOrder.hs

@@ -55,6 +55,7 @@ module Bookseller2HigherOrder where
 
 import Choreography
 import System.Environment
+import Logic.Propositional (introAnd)
 
 import CLI
 import Data (deliveryDateOf, priceOf)
@@ -67,39 +68,40 @@ type Participants = ["buyer", "seller", "buyer2"]
 
 -- | `bookseller` is a choreography that implements the bookseller protocol.
 -- This version takes a choreography `mkDecision` that implements the decision making process.
-bookseller :: (Int @ "buyer" -> Choreo Participants (CLI m) (Bool @ "buyer")) -> Choreo Participants (CLI m) ()
+bookseller :: (Located '["buyer"] Int -> Choreo Participants (CLI m) (Located '["buyer"] Bool))
+              -> Choreo Participants (CLI m) ()
 bookseller mkDecision = do
   database <- seller `_locally` getInput "Enter the book database (for `Read`):"
-  title <- (buyer, \_ -> getstr "Enter the title of the book to buy:") ~~> seller
+  title <- (buyer, \_ -> getstr "Enter the title of the book to buy:") ~~> (seller @@ nobody)
 
   -- the seller checks the price of the book and sends it to the buyer
-  price <- (seller, \un -> return $ priceOf (un database) (un title)) ~~> buyer
+  price <- (seller, \un -> return $ priceOf (un seller database) (un seller title)) ~~> (buyer @@ nobody)
 
   -- the buyer makes a decision using the `mkDecision` choreography
   decision <- mkDecision price
 
   -- if the buyer decides to buy the book, the seller sends the delivery date to the buyer
-  cond (buyer, decision) \case
+  cond (buyer `introAnd` buyer, decision) \case
     True  -> do
-      deliveryDate <- (seller, \un -> return $ deliveryDateOf (un database) (un title)) ~~> buyer
-      buyer `locally_` \un -> putstr "The book will be delivered on:" $ show (un deliveryDate)
+      deliveryDate <- (seller, \un -> return $ deliveryDateOf (un seller database) (un seller title)) ~~> (buyer @@ nobody)
+      buyer `locally_` \un -> putstr "The book will be delivered on:" $ show (un buyer deliveryDate)
 
     False -> do
       buyer `locally_` \_ -> putNote "The book's price is out of the budget"
 
 -- | `mkDecision1` checks if buyer's budget is greater than the price of the book
-mkDecision1 :: Int @ "buyer" -> Choreo Participants (CLI m) (Bool @ "buyer")
+mkDecision1 :: Located '["buyer"] Int -> Choreo Participants (CLI m) (Located '["buyer"] Bool)
 mkDecision1 price = do
   budget <- buyer `_locally` getInput "What are you willing to pay?"
-  buyer `locally` \un -> return $ un price <= un budget
+  buyer `locally` \un -> return $ un buyer price <= un buyer budget
 
 -- | `mkDecision2` asks buyer2 how much they're willing to contribute and checks
 -- if the buyer's budget is greater than the price of the book minus buyer2's contribution
-mkDecision2 :: Int @ "buyer" -> Choreo Participants (CLI m) (Bool @ "buyer")
+mkDecision2 :: Located '["buyer"] Int -> Choreo Participants (CLI m) (Located '["buyer"] Bool)
 mkDecision2 price = do
   contrib1 <- buyer `_locally` getInput "What are you willing to pay?"
-  contrib2 <- (buyer2, \_ -> getInput "How much you're willing to contribute?") ~~> buyer
-  buyer `locally` \un -> return $ un price - un contrib2 <= un contrib1
+  contrib2 <- (buyer2, \_ -> getInput "How much you're willing to contribute?") ~~> (buyer @@ nobody)
+  buyer `locally` \un -> return $ un buyer price - un buyer contrib2 <= un buyer contrib1
 
 main :: IO ()
 main = do

examples/Bookseller3LocPoly.hs

@@ -36,15 +36,15 @@ bookseller someBuyer = do
   database <- seller `_locally` getInput "Enter the book database (for `Read`):"
   buyer_budget <- theBuyer `_locally` getInput "Enter your total budget:"
   -- the buyer reads the title of the book and sends it to the seller
-  title <- (theBuyer, \_ -> getstr "Enter the title of the book to buy") ~~> seller
+  title <- (theBuyer, \_ -> getstr "Enter the title of the book to buy") ~~> (seller @@ nobody)
   -- the seller checks the price of the book and sends it to the buyer
-  price <- (seller, \un -> return $ priceOf (un database) (un title)) ~~> theBuyer
+  price <- (seller, \un -> return $ priceOf (un seller database) (un seller title)) ~~> (theBuyer @@ nobody)
 
-  cond' (theBuyer, \un -> return $ un price <= un buyer_budget) \case
+  cond' (theBuyer, \un -> return $ un explicitMember price <= un explicitMember buyer_budget) \case
     True  -> do
-      deliveryDate <- (seller, \un -> return $ deliveryDateOf (un database) (un title)) ~~> theBuyer
+      deliveryDate <- (seller, \un -> return $ deliveryDateOf (un seller database) (un seller title)) ~~> (theBuyer @@ nobody)
 
-      theBuyer `locally_` \un -> putOutput "The book will be delivered on:" $ un deliveryDate
+      theBuyer `locally_` \un -> putOutput "The book will be delivered on:" $ un explicitMember deliveryDate
 
     False -> do
       theBuyer `_locally_` putNote "The book's price is out of the budget"

examples/DiffieHellman.hs

@@ -39,6 +39,9 @@ module DiffieHellman where
 import Choreography (mkHttpConfig, runChoreography)
 import Choreography.Choreo
 import Choreography.Location
+import CLI
+import Control.Monad.Cont (MonadIO)
+import Logic.Propositional (introAnd)
 import System.Environment
 import System.Random
 
@@ -59,57 +62,48 @@ $(mkLoc "bob")
 
 type Participants = ["alice", "bob"]
 
-diffieHellman :: Choreo Participants IO (Integer @ "alice", Integer @ "bob")
+diffieHellman :: (MonadIO m) =>
+                 Choreo Participants (CLI m) ()
 diffieHellman = do
   -- wait for alice to initiate the process
-  _ <- alice `locally` \_ -> do
-    putStrLn "enter to start key exchange..."
-    getLine
-  bob `locally_` \_ -> do
-    putStrLn "waiting for alice to initiate key exchange"
+  _ <- alice `locally` \_ -> getstr "enter to start key exchange..."
+  bob `locally_` \_ -> putNote "waiting for alice to initiate key exchange"
 
   -- alice picks p and g and sends them to bob
   pa <-
     alice `locally` \_ -> do
       x <- randomRIO (200, 1000 :: Int)
       return $ primeNums !! x
-  pb <- (alice, pa) ~> bob
-  ga <- alice `locally` \un -> do randomRIO (10, un pa)
-  gb <- (alice, ga) ~> bob
+  pb <- (alice `introAnd` alice, pa) ~> (bob @@ nobody)
+  ga <- alice `locally` \un -> do randomRIO (10, un alice pa)
+  gb <- (alice `introAnd` alice, ga) ~> (bob @@ nobody)
 
   -- alice and bob select secrets
   a <- alice `locally` \_ -> do randomRIO (200, 1000 :: Integer)
   b <- bob `locally` \_ -> do randomRIO (200, 1000 :: Integer)
 
   -- alice and bob computes numbers that they exchange
-  a' <- alice `locally` \un -> do return $ un ga ^ un a `mod` un pa
-  b' <- bob `locally` \un -> do return $ un gb ^ un b `mod` un pb
+  a' <- alice `locally` \un -> do return $ un alice ga ^ un alice a `mod` un alice pa
+  b' <- bob `locally` \un -> do return $ un bob gb ^ un bob b `mod` un bob pb
 
   -- exchange numbers
-  a'' <- (alice, a') ~> bob
-  b'' <- (bob, b') ~> alice
+  a'' <- (alice `introAnd` alice, a') ~> (bob @@ nobody)
+  b'' <- (bob `introAnd` bob, b') ~> (alice @@ nobody)
 
   -- compute shared key
-  s1 <-
-    alice `locally` \un ->
-      let s = un b'' ^ un a `mod` un pa
-       in do
-            putStrLn ("alice's shared key: " ++ show s)
-            return s
-  s2 <-
-    bob `locally` \un ->
-      let s = un a'' ^ un b `mod` un pb
-       in do
-            putStrLn ("bob's shared key: " ++ show s)
-            return s
-  return (s1, s2)
+  alice `locally_` \un ->
+      let s = un alice b'' ^ un alice a `mod` un alice pa
+       in putOutput "alice's shared key:" s
+  bob `locally_` \un ->
+      let s = un bob a'' ^ un bob b `mod` un bob pb
+      in putOutput "bob's shared key:" s
 
 main :: IO ()
 main = do
   [loc] <- getArgs
   _ <- case loc of
-    "alice" -> runChoreography config diffieHellman "alice"
-    "bob" -> runChoreography config diffieHellman "bob"
+    "alice" -> runCLIIO $ runChoreography config diffieHellman "alice"
+    "bob" -> runCLIIO $ runChoreography config diffieHellman "bob"
     _ -> error "unknown party"
   return ()
   where

examples/KVS1Simple.hs

@@ -34,6 +34,7 @@ import Choreography.Network.Http
 import Data.IORef
 import Data.Map (Map)
 import Data.Map qualified as Map
+import Logic.Propositional (introAnd)
 import System.Environment
 
 $(mkLoc "client")
@@ -76,18 +77,18 @@ handleRequest request stateRef = case request of
 
 -- | `kvs` is a choreography that processes a single request located at the client and returns the response.
 kvs ::
-  Request @ "client" ->
-  IORef State @ "server" ->
-  Choreo Participants IO (Response @ "client")
+  Located '["client"] Request ->
+  Located '["server"] (IORef State) ->
+  Choreo Participants IO (Located '["client"] Response)
 kvs request stateRef = do
   -- send the request to the server
-  request' <- (client, request) ~> server
+  request' <- (client `introAnd` client, request) ~> (server @@ nobody)
   -- the server handles the response and creates a response
   response <-
     server `locally` \un ->
-      handleRequest (un request') (un stateRef)
+      handleRequest (un server request') (un server stateRef)
   -- send the response back to the client
-  (server, response) ~> client
+  (server `introAnd` server, response) ~> (client @@ nobody)
 
 -- | `mainChoreo` is a choreography that serves as the entry point of the program.
 -- It initializes the state and loops forever.
@@ -97,11 +98,11 @@ mainChoreo = do
   stateRef <- server `locally` \_ -> newIORef (Map.empty :: State)
   loop stateRef
   where
-    loop :: IORef State @ "server" -> Choreo Participants IO ()
+    loop :: Located '["server"] (IORef State) -> Choreo Participants IO ()
     loop stateRef = do
       request <- client `_locally` readRequest
       response <- kvs request stateRef
-      client `locally_` \un -> do putStrLn ("> " ++ show (un response))
+      client `locally_` \un -> do putStrLn ("> " ++ show (un client response))
       loop stateRef
 
 main :: IO ()