From dcc8903cd439f536cf211429cd33394068aa10f3 Mon Sep 17 00:00:00 2001 From: Pierre Krafft Date: Tue, 5 Jun 2018 18:28:31 +0200 Subject: [PATCH] Prepare for presentation --- README.md | 14 +-- src/Examples/Main.agda | 4 +- src/Examples/SizedStream.lagda.tex | 6 -- src/Examples/TestSelectiveReceive.lagda.tex | 7 ++ .../Examples/CalculatorProtocol.agda | 77 +++++++++++++++ src/Selective/Examples/Main-generated.agda | 8 +- src/Selective/Examples/Main-template.agda | 6 +- src/Selective/Examples/TestAO.agda | 58 ++++++------ src/Selective/Examples/TestCall2.agda | 84 +++++++++++------ src/Selective/Examples/TestChannel.agda | 93 +++++++++++++++++++ .../Examples/TestSelectiveReceive-calc.agda | 63 +++++++++++++ 11 files changed, 349 insertions(+), 71 deletions(-) create mode 100644 src/Selective/Examples/CalculatorProtocol.agda create mode 100644 src/Selective/Examples/TestChannel.agda create mode 100644 src/Selective/Examples/TestSelectiveReceive-calc.agda diff --git a/README.md b/README.md index 4c59c10..30e8809 100644 --- a/README.md +++ b/README.md @@ -4,20 +4,20 @@ The source code for my Master's Thesis. The work takes inspiration from the lambda-calculus λact, defined in [Mixing Metaphors: Actors as Channels and Channels as Actors](https://arxiv.org/abs/1611.06276), and aims to provide a formalization of type safe Erlang-like actors. -In my formalization Actors are modelled as indexed monads, +In my formalization Actors are modelled as parameterized monads, in a style inspired by Effects from Idris and Koen Claessen's Poor Man's Concurrency Monad. | Dependency | Version | |------------------|------------------------------------------| -| Agda | 8a7ad7f79c09d3a55110b6f92ab07267564601f0 | -| standard-library | 2a40a031e40042e72e245cce17956e5df49fcdd5 | +| Agda | 2.5.4 | +| standard-library | 2ff655cc3b6632ee0e3a52319360177b65ef59ce | ## How to build? -Agda and the standard library are nightlies for Agda 2.5.4. -The simplest way to build Agda is to clone the repo and run +You can follow [Agda's installation guide](http://agda.readthedocs.io/en/latest/getting-started/installation.html) +or build from source. +My preferred way is to to clone the repo, checkout the release-2.5.4 branch and run `stack install --stack-yaml stack-8.2.2.yaml`. -The nightlies are used to get do-notation and solve some bugs with codata. The project itself can be built with make or using agda-mode in emacs. Latex files can be generated with `make latex`, but most of the thesis is kept in ShareLatex. @@ -29,7 +29,7 @@ Latex files can be generated with `make latex`, but most of the thesis is kept i | Simulate | The main worker. Simulates the steps of an environment | | Runtime | Converts a simulation to IO | | ActorMonad | The embedding you use to create different actor programs | -| SimulationEnvironment | The datastructures and proofs used in the simulation | +| SimulationEnvironment | The data structures and proofs used in the simulation | | EnvironmentOperations | Functions modifying the simulation environment | | Examples | Showcases patterns and code used in the thesis | | Selective | Selective receive as a primary operation | diff --git a/src/Examples/Main.agda b/src/Examples/Main.agda index dcbc425..67f28d5 100644 --- a/src/Examples/Main.agda +++ b/src/Examples/Main.agda @@ -1,8 +1,8 @@ module Examples.Main where import Examples.PingPong as PingPong import Examples.InfiniteBind as InfiniteBind -import Examples.SelectiveReceive as SelectiveReceive -import Examples.Call as Call +import Examples.TestSelectiveReceive as SelectiveReceive +import Examples.TestCall as Call open import Runtime open import SimulationEnvironment open import ActorMonad diff --git a/src/Examples/SizedStream.lagda.tex b/src/Examples/SizedStream.lagda.tex index f7b0345..a5eab1a 100644 --- a/src/Examples/SizedStream.lagda.tex +++ b/src/Examples/SizedStream.lagda.tex @@ -15,12 +15,6 @@ \begin{code} open Stream \end{code} -%<*SkipTwice> -\begin{code} -skip-twice : (i : Size) → Stream (↑ (↑ i)) ℕ → Stream i ℕ -skip-twice i s = s .tail (↑ i) .tail i -\end{code} -% %<*Fib> \begin{minipage}{\textwidth} \begin{code} diff --git a/src/Examples/TestSelectiveReceive.lagda.tex b/src/Examples/TestSelectiveReceive.lagda.tex index 5d37d00..674f7bc 100644 --- a/src/Examples/TestSelectiveReceive.lagda.tex +++ b/src/Examples/TestSelectiveReceive.lagda.tex @@ -59,3 +59,10 @@ after-receive \end{code} % +\begin{code} +spawner : ∀ {i} → ActorM i SR-inbox + (List (Message SR-inbox)) + [] + (λ q' → OtherInbox ∷ (waiting-refs q')) +spawner = receive-42-with-reference [] +\end{code} \ No newline at end of file diff --git a/src/Selective/Examples/CalculatorProtocol.agda b/src/Selective/Examples/CalculatorProtocol.agda new file mode 100644 index 0000000..8be20b7 --- /dev/null +++ b/src/Selective/Examples/CalculatorProtocol.agda @@ -0,0 +1,77 @@ +module Selective.Examples.CalculatorProtocol where + +open import Selective.Libraries.Call2 +open import Prelude + +open import Debug +open import Data.Nat.Show using (show) + +ℕ-ReplyMessage : MessageType +ℕ-ReplyMessage = ValueType UniqueTag ∷ [ ValueType ℕ ]ˡ + +ℕ-Reply : InboxShape +ℕ-Reply = [ ℕ-ReplyMessage ]ˡ + +ℕ×ℕ→ℕ-Message : MessageType +ℕ×ℕ→ℕ-Message = ValueType UniqueTag ∷ ReferenceType ℕ-Reply ∷ ValueType ℕ ∷ [ ValueType ℕ ]ˡ + +Calculate : InboxShape +Calculate = [ ℕ×ℕ→ℕ-Message ]ˡ + +CalculateProtocol : ChannelInitiation +CalculateProtocol = record + { request = Calculate + ; response = record { + channel-shape = ℕ-Reply + ; all-tagged = (HasTag _) ∷ [] + } + ; request-tagged = [ HasTag+Ref _ ]ᵃ + } + +ℕ×ℕ→ℕ-ci : ChannelInitiation +ℕ×ℕ→ℕ-ci = record { + request = Calculate + ; response = record { channel-shape = ℕ-Reply ; all-tagged = (HasTag _) ∷ [] } + ; request-tagged = (HasTag+Ref _) ∷ [] } + +Calculator : InboxShape +Calculator = ℕ×ℕ→ℕ-Message ∷ [ ℕ×ℕ→ℕ-Message ]ˡ + +TestBox : InboxShape +TestBox = ℕ-Reply + +calculator-test-actor : ∀{i} → + ∞ActorM (↑ i) Calculator (Lift ⊤) [] (λ _ → []) → + ∞ActorM i TestBox (Lift ℕ) [] (λ _ → []) +calculator-test-actor calculator-actor = do + spawn∞ calculator-actor + Msg Z (_ ∷ n ∷ []) ← call CalculateProtocol (record { + var = Z + ; chosen-field = Z + ; fields = lift 32 ∷ [ lift 10 ]ᵃ + ; session = record { + can-request = [ Z ]ᵐ -- Pick add method + ; response-session = record { + can-receive = [ Z ]ᵐ + ; tag = 0 + } + } + }) + where + Msg (S ()) _ + Msg Z (_ ∷ m ∷ []) ← debug (show n) (call CalculateProtocol (record { + var = Z + ; chosen-field = Z + ; fields = lift n ∷ [ lift 10 ]ᵃ + ; session = record { + can-request = [ S Z ]ᵐ -- Pick multiply method + ; response-session = record { + can-receive = [ Z ]ᵐ + ; tag = 1 + } + } + })) + where + Msg (S ()) _ + debug (show m) (strengthen []) + return m diff --git a/src/Selective/Examples/Main-generated.agda b/src/Selective/Examples/Main-generated.agda index c15c1fd..fe012dd 100644 --- a/src/Selective/Examples/Main-generated.agda +++ b/src/Selective/Examples/Main-generated.agda @@ -6,6 +6,8 @@ import Selective.Examples.Fibonacci as Fib import Selective.Examples.Chat as Chat import Selective.Examples.Bookstore as Bookstore import Selective.Examples.TestAO as TestAO +import Selective.Examples.TestSelectiveReceive as SelectiveReceive +import Selective.Examples.TestSelectiveReceive-calc as SelectiveReceive-calc open import Selective.Runtime open import Selective.SimulationEnvironment @@ -15,10 +17,12 @@ open ∞ActorM pingpongEntry = singleton-env (PingPong.spawner .force) callEntry = singleton-env (Call.calltestActor .force) -call2Entry = singleton-env (Call2.calltestActor .force) +call2Entry = singleton-env (Call2.calculator-test-actor .force) fibEntry = singleton-env (Fib.spawner .force) chatEntry = singleton-env (Chat.chat-supervisor .force) bookstoreEntry = singleton-env (Bookstore.bookstore-supervisor .force) testaoEntry = singleton-env (TestAO.calculator-test-actor .force) +testsrcalcEntry = singleton-env (SelectiveReceive-calc.calculator-test-actor .force) +testsrEntry = singleton-env (SelectiveReceive.receive-42-with-reference) -main = IO.run (run-env call2Entry) +main = IO.run (run-env testsrcalcEntry) diff --git a/src/Selective/Examples/Main-template.agda b/src/Selective/Examples/Main-template.agda index 3cc2207..57c0f5e 100644 --- a/src/Selective/Examples/Main-template.agda +++ b/src/Selective/Examples/Main-template.agda @@ -6,6 +6,8 @@ import Selective.Examples.Fibonacci as Fib import Selective.Examples.Chat as Chat import Selective.Examples.Bookstore as Bookstore import Selective.Examples.TestAO as TestAO +import Selective.Examples.TestSelectiveReceive as SelectiveReceive +import Selective.Examples.TestSelectiveReceive-calc as SelectiveReceive-calc open import Selective.Runtime open import Selective.SimulationEnvironment @@ -15,10 +17,12 @@ open ∞ActorM pingpongEntry = singleton-env (PingPong.spawner .force) callEntry = singleton-env (Call.calltestActor .force) -call2Entry = singleton-env (Call2.calltestActor .force) +call2Entry = singleton-env (Call2.calculator-test-actor .force) fibEntry = singleton-env (Fib.spawner .force) chatEntry = singleton-env (Chat.chat-supervisor .force) bookstoreEntry = singleton-env (Bookstore.bookstore-supervisor .force) testaoEntry = singleton-env (TestAO.calculator-test-actor .force) +testsrcalcEntry = singleton-env (SelectiveReceive-calc.calculator-test-actor .force) +testsrEntry = singleton-env (SelectiveReceive.receive-42-with-reference) main = IO.run (run-env __ENTRY__) diff --git a/src/Selective/Examples/TestAO.agda b/src/Selective/Examples/TestAO.agda index 75e2473..a197f58 100644 --- a/src/Selective/Examples/TestAO.agda +++ b/src/Selective/Examples/TestAO.agda @@ -5,43 +5,39 @@ open import Prelude open import Selective.Libraries.Call2 open import Selective.Libraries.ActiveObjects - open import Debug open import Data.Nat.Show using (show) -AddReplyMessage : MessageType -AddReplyMessage = ValueType UniqueTag ∷ [ ValueType ℕ ]ˡ +ℕ-ReplyMessage : MessageType +ℕ-ReplyMessage = ValueType UniqueTag ∷ [ ValueType ℕ ]ˡ -AddReply : InboxShape -AddReply = [ AddReplyMessage ]ˡ +ℕ-Reply : InboxShape +ℕ-Reply = [ ℕ-ReplyMessage ]ˡ -AddMessage : MessageType -AddMessage = ValueType UniqueTag ∷ ReferenceType AddReply ∷ ValueType ℕ ∷ [ ValueType ℕ ]ˡ +ℕ×ℕ→ℕ-Message : MessageType +ℕ×ℕ→ℕ-Message = ValueType UniqueTag ∷ ReferenceType ℕ-Reply ∷ ValueType ℕ ∷ [ ValueType ℕ ]ˡ -Calculator : InboxShape -Calculator = [ AddMessage ]ˡ +Calculate : InboxShape +Calculate = [ ℕ×ℕ→ℕ-Message ]ˡ -CalculatorProtocol : ChannelInitiation -CalculatorProtocol = record - { request = Calculator +CalculateProtocol : ChannelInitiation +CalculateProtocol = record + { request = Calculate ; response = record { - channel-shape = AddReply + channel-shape = ℕ-Reply ; all-tagged = (HasTag _) ∷ [] } ; request-tagged = [ HasTag+Ref _ ]ᵃ } -TestBox : InboxShape -TestBox = AddReply - -calculator-ci : ChannelInitiation -calculator-ci = record { - request = Calculator - ; response = record { channel-shape = AddReply ; all-tagged = (HasTag _) ∷ [] } +ℕ×ℕ→ℕ-ci : ChannelInitiation +ℕ×ℕ→ℕ-ci = record { + request = Calculate + ; response = record { channel-shape = ℕ-Reply ; all-tagged = (HasTag _) ∷ [] } ; request-tagged = (HasTag+Ref _) ∷ [] } -add-method-header = ResponseMethod calculator-ci -multiply-method-header = ResponseMethod calculator-ci +add-method-header = ResponseMethod ℕ×ℕ→ℕ-ci +multiply-method-header = ResponseMethod ℕ×ℕ→ℕ-ci calculator-methods : List ActiveMethod calculator-methods = add-method-header ∷ multiply-method-header ∷ [] @@ -70,15 +66,23 @@ calculator = record { calculator-actor = run-active-object calculator _ + +TestBox : InboxShape +TestBox = ℕ-Reply + + +-- import Selective.Examples.CalculatorProtocol as CP +-- calculator-test-actor = CP.calculator-test-actor calculator-actor + calculator-test-actor : ∀{i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → []) calculator-test-actor = do spawn∞ calculator-actor - Msg Z (_ ∷ n ∷ []) ← call CalculatorProtocol (record { + Msg Z (_ ∷ n ∷ []) ← call CalculateProtocol (record { var = Z ; chosen-field = Z ; fields = lift 32 ∷ [ lift 10 ]ᵃ ; session = record { - can-request = [ Z ]ᵐ + can-request = [ Z ]ᵐ -- Pick add method ; response-session = record { can-receive = [ Z ]ᵐ ; tag = 0 @@ -87,12 +91,12 @@ calculator-test-actor = do }) where Msg (S ()) _ - Msg Z (_ ∷ m ∷ []) ← debug (show n) (call CalculatorProtocol (record { + Msg Z (_ ∷ m ∷ []) ← debug (show n) (call CalculateProtocol (record { var = Z ; chosen-field = Z - ; fields = lift 32 ∷ [ lift 10 ]ᵃ + ; fields = lift n ∷ [ lift 10 ]ᵃ ; session = record { - can-request = [ S Z ]ᵐ + can-request = [ S Z ]ᵐ -- Pick multiply method ; response-session = record { can-receive = [ Z ]ᵐ ; tag = 1 diff --git a/src/Selective/Examples/TestCall2.agda b/src/Selective/Examples/TestCall2.agda index fd039a9..b6d68d2 100644 --- a/src/Selective/Examples/TestCall2.agda +++ b/src/Selective/Examples/TestCall2.agda @@ -3,49 +3,68 @@ module Selective.Examples.TestCall2 where open import Selective.Libraries.Call2 open import Prelude -AddReplyMessage : MessageType -AddReplyMessage = ValueType UniqueTag ∷ [ ValueType ℕ ]ˡ +open import Debug +open import Data.Nat.Show using (show) -AddReply : InboxShape -AddReply = [ AddReplyMessage ]ˡ +ℕ-ReplyMessage : MessageType +ℕ-ReplyMessage = ValueType UniqueTag ∷ [ ValueType ℕ ]ˡ -AddMessage : MessageType -AddMessage = ValueType UniqueTag ∷ ReferenceType AddReply ∷ ValueType ℕ ∷ [ ValueType ℕ ]ˡ +ℕ-Reply : InboxShape +ℕ-Reply = [ ℕ-ReplyMessage ]ˡ -Calculator : InboxShape -Calculator = [ AddMessage ]ˡ +ℕ×ℕ→ℕ-Message : MessageType +ℕ×ℕ→ℕ-Message = ValueType UniqueTag ∷ ReferenceType ℕ-Reply ∷ ValueType ℕ ∷ [ ValueType ℕ ]ˡ + +Calculate : InboxShape +Calculate = [ ℕ×ℕ→ℕ-Message ]ˡ -CalculatorProtocol : ChannelInitiation -CalculatorProtocol = record - { request = Calculator +CalculateProtocol : ChannelInitiation +CalculateProtocol = record + { request = Calculate ; response = record { - channel-shape = AddReply + channel-shape = ℕ-Reply ; all-tagged = (HasTag _) ∷ [] } ; request-tagged = [ HasTag+Ref _ ]ᵃ } -calculatorActor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift ⊤) [] (λ _ → []) -calculatorActor .force = receive ∞>>= λ { +ℕ×ℕ→ℕ-ci : ChannelInitiation +ℕ×ℕ→ℕ-ci = record { + request = Calculate + ; response = record { channel-shape = ℕ-Reply ; all-tagged = (HasTag _) ∷ [] } + ; request-tagged = (HasTag+Ref _) ∷ [] } + +Calculator : InboxShape +Calculator = ℕ×ℕ→ℕ-Message ∷ [ ℕ×ℕ→ℕ-Message ]ˡ + +calculator-actor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift ⊤) [] (λ _ → []) +calculator-actor .force = receive ∞>>= λ { (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) .force → Z ![t: Z ] (lift tag ∷ [ lift (n + m) ]ᵃ) ∞>> (do strengthen [] - calculatorActor) - ; (Msg (S ()) _) + calculator-actor) + ; (Msg (S Z) (tag ∷ _ ∷ n ∷ m ∷ [])) .force → + (Z ![t: Z ] (lift tag ∷ ([ lift (n * m) ]ᵃ))) ∞>> (do + (strengthen []) + calculator-actor) + ; (Msg (S (S ())) _) } TestBox : InboxShape -TestBox = AddReply +TestBox = ℕ-Reply + +-- import Selective.Examples.CalculatorProtocol as CP +-- calculator-test-actor = CP.calculator-test-actor calculator-actor -calltestActor : ∀{i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → []) -calltestActor = do - (spawn∞ calculatorActor) - Msg Z (tag ∷ n ∷ []) ← call CalculatorProtocol (record { +calculator-test-actor : ∀{i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → []) +calculator-test-actor = do + spawn∞ calculator-actor + Msg Z (_ ∷ n ∷ []) ← call CalculateProtocol (record { var = Z ; chosen-field = Z - ; fields = (lift 32) ∷ [ lift 10 ]ᵃ + ; fields = lift 32 ∷ [ lift 10 ]ᵃ ; session = record { - can-request = ⊆-refl + can-request = [ Z ]ᵐ -- Pick add method ; response-session = record { can-receive = [ Z ]ᵐ ; tag = 0 @@ -54,6 +73,19 @@ calltestActor = do }) where Msg (S ()) _ - (strengthen []) - (return n) - + Msg Z (_ ∷ m ∷ []) ← debug (show n) (call CalculateProtocol (record { + var = Z + ; chosen-field = Z + ; fields = lift n ∷ [ lift 10 ]ᵃ + ; session = record { + can-request = [ S Z ]ᵐ -- Pick multiply method + ; response-session = record { + can-receive = [ Z ]ᵐ + ; tag = 1 + } + } + })) + where + Msg (S ()) _ + debug (show m) (strengthen []) + return m diff --git a/src/Selective/Examples/TestChannel.agda b/src/Selective/Examples/TestChannel.agda new file mode 100644 index 0000000..fa9e651 --- /dev/null +++ b/src/Selective/Examples/TestChannel.agda @@ -0,0 +1,93 @@ +module Selective.Examples.TestChannel where + +open import Selective.Libraries.Channel +open import Prelude + +open import Debug +open import Data.Nat.Show using (show) + +ℕ-ReplyMessage : MessageType +ℕ-ReplyMessage = ValueType UniqueTag ∷ [ ValueType ℕ ]ˡ + +ℕ-Reply : InboxShape +ℕ-Reply = [ ℕ-ReplyMessage ]ˡ + +ℕ×ℕ→ℕ-Message : MessageType +ℕ×ℕ→ℕ-Message = ValueType UniqueTag ∷ ReferenceType ℕ-Reply ∷ ValueType ℕ ∷ [ ValueType ℕ ]ˡ + +Calculate : InboxShape +Calculate = [ ℕ×ℕ→ℕ-Message ]ˡ + +CalculateProtocol : ChannelInitiation +CalculateProtocol = record + { request = Calculate + ; response = record { + channel-shape = ℕ-Reply + ; all-tagged = (HasTag _) ∷ [] + } + ; request-tagged = [ HasTag+Ref _ ]ᵃ + } + +ℕ×ℕ→ℕ-ci : ChannelInitiation +ℕ×ℕ→ℕ-ci = record { + request = Calculate + ; response = record { channel-shape = ℕ-Reply ; all-tagged = (HasTag _) ∷ [] } + ; request-tagged = (HasTag+Ref _) ∷ [] } + +Calculator : InboxShape +Calculator = ℕ×ℕ→ℕ-Message ∷ [ ℕ×ℕ→ℕ-Message ]ˡ + +calculator-actor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift ⊤) [] (λ _ → []) +calculator-actor .force = receive ∞>>= λ { + (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) .force → + Z ![t: Z ] (lift tag ∷ [ lift (n + m) ]ᵃ) ∞>> (do + strengthen [] + calculator-actor) + ; (Msg (S Z) (tag ∷ _ ∷ n ∷ m ∷ [])) .force → + (Z ![t: Z ] (lift tag ∷ ([ lift (n * m) ]ᵃ))) ∞>> (do + (strengthen []) + calculator-actor) + ; (Msg (S (S ())) _) + } + +TestBox : InboxShape +TestBox = ℕ-Reply + +calculator-test-actor : ∀{i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → []) +calculator-test-actor = do + spawn∞ calculator-actor + let add-request = (record { + var = Z + ; chosen-field = Z + ; fields = lift 32 ∷ [ lift 10 ]ᵃ + ; session = record { + can-request = [ Z ]ᵐ -- Pick add method + ; response-session = record { + can-receive = [ Z ]ᵐ + ; tag = 0 + } + } + }) + add-rs = add-request .session .response-session + initiate-channel _ add-request + Msg Z (_ ∷ n ∷ []) ← from-channel (CalculateProtocol .response) add-rs + where + Msg (S ()) _ + let mult-request = (record { + var = Z + ; chosen-field = Z + ; fields = lift n ∷ [ lift 10 ]ᵃ + ; session = record { + can-request = [ S Z ]ᵐ -- Pick multiply method + ; response-session = record { + can-receive = [ Z ]ᵐ + ; tag = 1 + } + } + }) + mult-rs = add-rs = mult-request .session .response-session + Msg Z (_ ∷ m ∷ []) ← from-channel (CalculateProtocol .response) mult-rs + where + Msg (S ()) _ + debug (show m) (strengthen []) + return m diff --git a/src/Selective/Examples/TestSelectiveReceive-calc.agda b/src/Selective/Examples/TestSelectiveReceive-calc.agda new file mode 100644 index 0000000..a2f15b5 --- /dev/null +++ b/src/Selective/Examples/TestSelectiveReceive-calc.agda @@ -0,0 +1,63 @@ +module Selective.Examples.TestSelectiveReceive-calc where + +open import Selective.ActorMonad +open import Prelude + +open import Debug +open import Data.Nat.Show using (show) + +UniqueTag = ℕ +TagField = ValueType UniqueTag + +ℕ-ReplyMessage : MessageType +ℕ-ReplyMessage = ValueType UniqueTag ∷ [ ValueType ℕ ]ˡ + +ℕ-Reply : InboxShape +ℕ-Reply = [ ℕ-ReplyMessage ]ˡ + +ℕ×ℕ→ℕ-Message : MessageType +ℕ×ℕ→ℕ-Message = ValueType UniqueTag ∷ ReferenceType ℕ-Reply ∷ ValueType ℕ ∷ [ ValueType ℕ ]ˡ + +Calculate : InboxShape +Calculate = [ ℕ×ℕ→ℕ-Message ]ˡ + +Calculator : InboxShape +Calculator = ℕ×ℕ→ℕ-Message ∷ [ ℕ×ℕ→ℕ-Message ]ˡ + +calculator-actor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift ⊤) [] (λ _ → []) +calculator-actor .force = receive ∞>>= λ { + (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) .force → + Z ![t: Z ] (lift tag ∷ [ lift (n + m) ]ᵃ) ∞>> (do + strengthen [] + calculator-actor) + ; (Msg (S Z) (tag ∷ _ ∷ n ∷ m ∷ [])) .force → + (Z ![t: Z ] (lift tag ∷ ([ lift (n * m) ]ᵃ))) ∞>> (do + (strengthen []) + calculator-actor) + ; (Msg (S (S ())) _) + } + +TestBox : InboxShape +TestBox = ℕ-Reply + +accept-tagged-ℕ : UniqueTag → MessageFilter TestBox +accept-tagged-ℕ tag (Msg Z (tag' ∷ _)) = ⌊ tag ≟ tag' ⌋ +accept-tagged-ℕ tag (Msg (S ()) _) + +calculator-test-actor : ∀{i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → []) +calculator-test-actor = do + spawn∞ calculator-actor + self + (S Z ![t: Z ] ((lift 0) ∷ (([ Z ]>: ⊆-refl) ∷ lift 32 ∷ [ lift 10 ]ᵃ))) + (strengthen (⊆-suc ⊆-refl)) + sm: Msg Z (_ ∷ n ∷ []) [ _ ] ← (selective-receive (accept-tagged-ℕ 0)) + where + sm: Msg (S ()) _ [ _ ] + self + (S Z ![t: S Z ] ((lift 0) ∷ (([ Z ]>: ⊆-refl) ∷ lift 32 ∷ [ lift 10 ]ᵃ))) + strengthen (⊆-suc ⊆-refl) + sm: Msg Z (_ ∷ m ∷ []) [ _ ] ← (selective-receive (accept-tagged-ℕ 0)) + where + sm: Msg (S ()) _ [ _ ] + strengthen [] + return m