Improve active objects, restructure project

Zalastax · May 21, 2018 · 62bd54c · 62bd54c
1 parent 81ca182
commit 62bd54c
Show file tree

Hide file tree

Showing 22 changed files with 1,250 additions and 452 deletions.
diff --git a/Makefile b/Makefile
@@ -1,6 +1,6 @@
 include .rc.make
 
-subdirs := src/ src/Examples/ unused/ src/Selective/ src/Selective/Examples/
+subdirs := src/ src/Examples/ src/Libraries/ src/Selective/ src/Selective/Libraries/ src/Selective/Examples/
 agda-objects := $(wildcard $(subdirs:%=%*.agdai))
 executables := $(wildcard $(subdirs:%=%*.exe))
 malonzo := $(wildcard $(subdirs:%=%MAlonzo/))

diff --git a/latex.make b/latex.make
@@ -1,6 +1,6 @@
 include .rc.make
 
-subdirs := src/ src/Examples/ src/Selective/ src/Selective/Examples/
+subdirs := src/ src/Examples/ src/Libraries/ src/Selective/ src/Selective/Libraries/ src/Selective/Examples/
 sources := $(wildcard $(subdirs:%=%*.lagda.tex))
 renamed := $(sources:%.lagda.tex=%.tex)
 moved   := $(renamed:src/%=$(LATEX-OUTPUT-DIR)%)

diff --git a/src/Examples/Main-template.agda b/src/Examples/Main-template.agda
@@ -1,8 +1,8 @@
 module Examples.Main-generated 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/TestCall.agda b/src/Examples/TestCall.agda
@@ -0,0 +1,46 @@
+module Examples.TestCall where
+
+open import Prelude
+open import Libraries.SelectiveReceive
+open import Libraries.Call
+
+open SelRec
+
+AddReplyMessage : MessageType
+AddReplyMessage = ValueType UniqueTag ∷ [ ValueType ℕ ]ˡ
+
+AddReply : InboxShape
+AddReply = [ AddReplyMessage ]ˡ
+
+AddMessage : MessageType
+AddMessage = ValueType UniqueTag ∷ ReferenceType AddReply ∷ ValueType ℕ ∷ [ ValueType ℕ ]ˡ
+
+Calculator : InboxShape
+Calculator = [ AddMessage ]ˡ
+
+calculatorActor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift ⊤) [] (λ _ → [])
+calculatorActor = loop
+  where
+    loop : ∀ {i} → ∞ActorM i Calculator (Lift ⊤) [] (λ _ → [])
+    loop .force = receive ∞>>= λ {
+      (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) → do
+        Z ![t: Z ] ((lift tag) ∷ [ lift (n + m) ]ᵃ )
+        strengthen []
+        loop
+      ; (Msg (S ()) _) }
+
+TestBox : InboxShape
+TestBox = AddReply
+
+calltestActor : ∀ {i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
+calltestActor .force = spawn∞ calculatorActor ∞>> do
+    x ← call [] Z Z 0
+         ((lift 10) ∷ [ lift 32 ]ᵃ)
+         ⊆-refl Z
+    strengthen []
+    return-result x
+  where
+    return-result : SelRec TestBox (call-select 0 ⊆-refl Z) →
+                    ∀ {i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
+    return-result record { msg = (Msg Z (tag ∷ n ∷ [])) } = return n
+    return-result record { msg = (Msg (S x) x₁) ; msg-ok = () }
diff --git a/src/Examples/TestSelectiveReceive.agda b/src/Examples/TestSelectiveReceive.agda
@@ -0,0 +1,32 @@
+module Examples.TestSelectiveReceive where
+
+open import Prelude
+open import Libraries.SelectiveReceive
+
+open SelRec
+
+BoolMessage = [ ValueType Bool ]ˡ
+SelectiveTestBox : InboxShape
+SelectiveTestBox = [ BoolMessage ]ˡ
+
+testActor : ∀ {i} → ActorM i SelectiveTestBox (Lift Bool) [] (λ _ → [])
+testActor = selective-receive [] only-true ∞>>= after-receive
+  where
+    only-true : Message SelectiveTestBox → Bool
+    only-true (Msg Z (b ∷ [])) = b
+    only-true (Msg (S ()) x₁)
+    after-receive : ∀ {i}
+                    (x : SelRec SelectiveTestBox only-true) →
+                    ∞ActorM i SelectiveTestBox (Lift Bool)
+                      (add-references [] (msg x) ++ waiting-refs (waiting x))
+                      (λ _ → [])
+    after-receive record { msg = (Msg Z (.true ∷ [])) ; msg-ok = refl } =
+      strengthen [] >>
+      return true
+    after-receive record { msg = (Msg (S ()) _) }
+
+spawner : ∀ {i} → ActorM i [] ⊤₁ [] (λ _ → [])
+spawner = begin do
+  spawn testActor
+  Z ![t: Z ] [ lift true ]ᵃ
+  strengthen []
diff --git a/src/Examples/Call.lagda.tex → src/Libraries/Call.lagda.tex b/src/Examples/Call.lagda.tex → src/Libraries/Call.lagda.tex
@@ -1,9 +1,9 @@
 \begin{code}
-module Examples.Call where
+module Libraries.Call where
 
 open import ActorMonad public
 open import Prelude
-open import Examples.SelectiveReceive using (
+open import Libraries.SelectiveReceive using (
             selective-receive ; SelRec ; waiting-refs
             ; add-references++)
 open SelRec
@@ -59,44 +59,4 @@
       px ∷ translate-fields ps
     translate-fields {ReferenceType x ∷ MT} (([ p ]>: v) ∷ ps) =
       ([ (S (∈-inc Γ (waiting-refs q) _ p)) ]>: v) ∷ (translate-fields ps)
-
-AddReplyMessage : MessageType
-AddReplyMessage = ValueType UniqueTag ∷ [ ValueType ℕ ]ˡ
-
-AddReply : InboxShape
-AddReply = [ AddReplyMessage ]ˡ
-
-AddMessage : MessageType
-AddMessage = ValueType UniqueTag ∷ ReferenceType AddReply ∷ ValueType ℕ ∷ [ ValueType ℕ ]ˡ
-
-Calculator : InboxShape
-Calculator = [ AddMessage ]ˡ
-
-calculatorActor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift ⊤) [] (λ _ → [])
-calculatorActor = loop
-  where
-    loop : ∀ {i} → ∞ActorM i Calculator (Lift ⊤) [] (λ _ → [])
-    loop .force = receive ∞>>= λ {
-      (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) → do
-        Z ![t: Z ] ((lift tag) ∷ [ lift (n + m) ]ᵃ )
-        strengthen []
-        loop
-      ; (Msg (S ()) _) }
-
-TestBox : InboxShape
-TestBox = AddReply
-
-calltestActor : ∀ {i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
-calltestActor .force = spawn∞ calculatorActor ∞>> do
-    x ← call [] Z Z 0
-         ((lift 10) ∷ [ lift 32 ]ᵃ)
-         ⊆-refl Z
-    strengthen []
-    return-result x
-  where
-    return-result : SelRec TestBox (call-select 0 ⊆-refl Z) →
-                    ∀ {i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
-    return-result record { msg = (Msg Z (tag ∷ n ∷ [])) } = return n
-    return-result record { msg = (Msg (S x) x₁) ; msg-ok = () }
-
 \end{code}
diff --git a/src/Examples/SelectiveReceive.lagda.tex → src/Libraries/SelectiveReceive.lagda.tex b/src/Examples/SelectiveReceive.lagda.tex → src/Libraries/SelectiveReceive.lagda.tex
@@ -1,6 +1,6 @@
 \begin{code}
 
-module Examples.SelectiveReceive where
+module Libraries.SelectiveReceive where
 
 open import ActorMonad public
 open import Prelude
@@ -230,32 +230,3 @@
             ret-v : SelRec IS f
             ret-v = record { msg = x ; msg-ok = p ; waiting = q }
 \end{code}
-
-\begin{code}
-
-BoolMessage = [ ValueType Bool ]ˡ
-SelectiveTestBox : InboxShape
-SelectiveTestBox = [ BoolMessage ]ˡ
-
-testActor : ∀ {i} → ActorM i SelectiveTestBox (Lift Bool) [] (λ _ → [])
-testActor = selective-receive [] only-true ∞>>= after-receive
-  where
-    only-true : Message SelectiveTestBox → Bool
-    only-true (Msg Z (b ∷ [])) = b
-    only-true (Msg (S ()) x₁)
-    after-receive : ∀ {i}
-                    (x : SelRec SelectiveTestBox only-true) →
-                    ∞ActorM i SelectiveTestBox (Lift Bool)
-                      (add-references [] (msg x) ++ waiting-refs (waiting x))
-                      (λ _ → [])
-    after-receive record { msg = (Msg Z (.true ∷ [])) ; msg-ok = refl } =
-      strengthen [] >>
-      return true
-    after-receive record { msg = (Msg (S ()) _) }
-
-spawner : ∀ {i} → ActorM i [] ⊤₁ [] (λ _ → [])
-spawner = begin do
-  spawn testActor
-  Z ![t: Z ] [ lift true ]ᵃ
-  strengthen []
-\end{code}
diff --git a/src/Selective/Examples/ActiveObjects.agda b/src/Selective/Examples/ActiveObjects.agda
diff --git a/src/Selective/Examples/Bookstore.agda b/src/Selective/Examples/Bookstore.agda
@@ -1,7 +1,7 @@
 module Selective.Examples.Bookstore where
 
 open import Selective.ActorMonad
-open import Selective.Examples.Call using (UniqueTag ; call)
+open import Selective.Libraries.Call using (UniqueTag ; call)
 open import Prelude
 
 open import Data.Nat

diff --git a/src/Selective/Examples/Chat.agda b/src/Selective/Examples/Chat.agda
@@ -1,7 +1,7 @@
 module Selective.Examples.Chat where
 
 open import Selective.ActorMonad
-open import Selective.Examples.Call using (UniqueTag ; call)
+open import Selective.Libraries.Call
 open import Prelude
   hiding (Maybe)
 open import Data.Maybe as Maybe