Prepare for presentation

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                 |

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

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}
-%</SkipTwice>
 %<*Fib>
 \begin{minipage}{\textwidth}
 \begin{code}

src/Examples/TestSelectiveReceive.lagda.tex

@@ -59,3 +59,10 @@
   after-receive
 \end{code}
 %</Body>
+\begin{code}
+spawner : ∀ {i} → ActorM i SR-inbox
+                    (List (Message SR-inbox))
+                    []
+                    (λ q' → OtherInbox ∷ (waiting-refs q'))
+spawner = receive-42-with-reference []
+\end{code}

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

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)

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__)

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