Writing

Makefile

@@ -23,7 +23,7 @@ selective-generated-main:
 	sed 's/__ENTRY__/$(ENTRY)/' src/Selective/Examples/Main-template.agda > src/Selective/Examples/Main-generated.agda
 	stack exec agda -- -c src/Selective/Examples/Main-generated.agda
 
-test-that-all-compliles:
+test-that-all-compiles:
 	$(MAKE) latex-clean
 	$(MAKE) latex
 	stack exec agda -- --no-main -c src/Selective/Examples/Main-generated.agda

src/ActorMonad.lagda.tex

@@ -321,17 +321,6 @@
 %</LiftTop>
 
 %<*ActorMonad>
-This thesis started out with the goal of formalizing the λ-calculus for actors that
-\textcite{DBLP:conf/ecoop/FowlerLW17} call $λ_{act}$.
-When investigating $λ_{act}$ we noticed that the language had a structure that made it suitable
-for being directly embedded in Agda,
-as opposed to the external λ-calculus we originally envisioned.
-What we had found was that the processes of $λ_{act}$ were instances of the monad pattern.
-Furthermore,
-\textcite{DBLP:conf/ecoop/FowlerLW17} show that if the host language is sufficiently advanced
-selective receive can be implemented as a library, in contrast to having it as a built in primitive.
-This led us to implement \ourlang as an embedded DSL in the form of a monad.
-
 The goal when translating $λ_{act}$ to an Agda embedding was to make the actors correct by construction,
 and to make it possible to type-check each actor separately.
 The pattern we found suitable is a monad parameterized by the type of the actor's

src/Selective/Libraries/ActiveObjects.lagda.tex

@@ -2,6 +2,7 @@
 module Selective.Libraries.ActiveObjects where
 
 open import Selective.Libraries.Channel public
+open import Selective.Libraries.ReceiveSublist
 open import Prelude
 
 open ChannelType
@@ -293,39 +294,11 @@
     forget-message input
     return₁ state'
 
-accept-sublist-unwrapped : (xs ys zs : InboxShape) → ∀{MT} → MT ∈ (xs ++ ys ++ zs) → Bool
-accept-sublist-unwrapped [] [] zs p = false
-accept-sublist-unwrapped [] (y ∷ ys) zs Z = true
-accept-sublist-unwrapped [] (y ∷ ys) zs (S p) = accept-sublist-unwrapped [] ys zs p
-accept-sublist-unwrapped (x ∷ xs) ys zs Z = false
-accept-sublist-unwrapped (x ∷ xs) ys zs (S p) = accept-sublist-unwrapped xs ys zs p
-
-
-accept-sublist : (xs ys zs : InboxShape) → MessageFilter (xs ++ ys ++ zs)
-accept-sublist xs ys zs (Msg received-message-type received-fields) = accept-sublist-unwrapped xs ys zs received-message-type
-
-record AcceptSublistDependent (IS : InboxShape) (accepted-type : MessageType) : Set₁ where
-  field
-    accepted-which : accepted-type ∈ IS
-    fields : All receive-field-content accepted-type
-
 receive-active-method : {i : Size} →
                         {Γ : TypingContext} →
                         (ac : ActiveObject) →
                         ∞ActorM i (active-inbox-shape ac) (Message (methods-shape (ac .methods))) Γ (add-references Γ)
-receive-active-method ac = do
-    record { msg = Msg {MT} p f ; msg-ok = msg-ok } ← selective-receive (accept-sublist [] (methods-shape (ac .methods)) (ac .extra-messages))
-    let record {accepted-which = aw ; fields = fields } = rewrap-message (methods-shape (ac .methods)) (ac .extra-messages) p f msg-ok
-    return₁ (Msg {MT = MT} aw fields)
-  where
-    rewrap-message : ∀{MT} → (ys zs : InboxShape) → (p : MT ∈ (ys ++ zs)) → All receive-field-content MT → (accept-sublist-unwrapped [] ys zs p) ≡ true → AcceptSublistDependent ys MT
-    rewrap-message [] zs which f ()
-    rewrap-message (x ∷ ys) zs Z f p = record { accepted-which = Z ; fields = f }
-    rewrap-message (x ∷ ys) zs (S which) f p =
-      let
-        rec = rewrap-message ys zs which f p
-        open AcceptSublistDependent
-      in record { accepted-which = S (rec .accepted-which) ; fields = rec .fields }
+receive-active-method ac = receive-sublist [] (methods-shape (ac .methods)) (ac .extra-messages)
 
 \end{code}
 %<*run-active-object>

src/Selective/Libraries/ReceiveSublist.agda

@@ -0,0 +1,48 @@
+module Selective.Libraries.ReceiveSublist where
+
+open import Selective.ActorMonad public
+open import Prelude
+
+accept-sublist-unwrapped : (xs ys zs : InboxShape) → ∀{MT} → MT ∈ (xs ++ ys ++ zs) → Bool
+accept-sublist-unwrapped [] [] zs p = false
+accept-sublist-unwrapped [] (y ∷ ys) zs Z = true
+accept-sublist-unwrapped [] (y ∷ ys) zs (S p) = accept-sublist-unwrapped [] ys zs p
+accept-sublist-unwrapped (x ∷ xs) ys zs Z = false
+accept-sublist-unwrapped (x ∷ xs) ys zs (S p) = accept-sublist-unwrapped xs ys zs p
+
+
+accept-sublist : (xs ys zs : InboxShape) → MessageFilter (xs ++ ys ++ zs)
+accept-sublist xs ys zs (Msg received-message-type received-fields) = accept-sublist-unwrapped xs ys zs received-message-type
+
+record AcceptSublistDependent (IS : InboxShape) (accepted-type : MessageType) : Set₁ where
+  field
+    accepted-which : accepted-type ∈ IS
+    fields : All receive-field-content accepted-type
+
+receive-sublist : {i : Size} →
+                  {Γ : TypingContext} →
+                  (xs ys zs : InboxShape) →
+                  ∞ActorM i (xs ++ ys ++ zs)
+                            (Message ys)
+                            Γ
+                            (add-references Γ)
+receive-sublist xs ys zs = do
+    record { msg = Msg {MT} p f ; msg-ok = msg-ok } ← selective-receive (accept-sublist xs ys zs)
+    let record {accepted-which = aw ; fields = fields } = rewrap-message xs ys zs p f msg-ok
+    return₁ (Msg {MT = MT} aw fields)
+  where
+    rewrap-message : ∀{MT} →
+                     (xs ys zs : InboxShape) →
+                     (p : MT ∈ (xs ++ ys ++ zs)) →
+                     All receive-field-content MT →
+                     (accept-sublist-unwrapped xs ys zs p) ≡ true →
+                     AcceptSublistDependent ys MT
+    rewrap-message [] [] zs p f ()
+    rewrap-message [] (x ∷ ys) zs Z f q = record { accepted-which = Z ; fields = f }
+    rewrap-message [] (x ∷ ys) zs (S p) f q =
+      let
+        rec = rewrap-message [] ys zs p f q
+        open AcceptSublistDependent
+      in record { accepted-which = S (rec .accepted-which) ; fields = rec .fields }
+    rewrap-message (x ∷ xs) ys zs Z f ()
+    rewrap-message (x ∷ xs) ys zs (S p) f q = rewrap-message xs ys zs p f q