Prelude and singleton

Makefile

@@ -1,6 +1,6 @@
 include .rc.make
 
-subdirs := src/ src/Examples/ unused/
+subdirs := src/ src/Examples/ unused/ src/Selective/ src/Selective/Examples/
 agda-objects := $(wildcard $(subdirs:%=%*.agdai))
 executables := $(wildcard $(subdirs:%=%*.exe))
 malonzo := $(wildcard $(subdirs:%=%MAlonzo/))

src/ActorMonad.lagda.tex

@@ -1,13 +1,7 @@
 \begin{code}
 module ActorMonad where
-open import Membership using (_∈_ ; _⊆_ ; ⊆-refl ; Z ; S ; find-∈)
+open import Prelude
 
-open import Data.List using (List ; [] ; _∷_ ; _++_)
-open import Data.List.All using (All ; [] ; _∷_)
-open import Data.Unit using (⊤ ; tt)
-
-open import Level using (Lift ; lift ; suc ; zero)
-open import Size using (Size ; Size<_ ; ↑_)
 \end{code}
 
 An Actor is indexed by the shape of its inbox.
@@ -492,7 +486,7 @@
 open ∞ActorM public
 
 -- coinduction helper for Value
-return₁ : {A : Set (suc zero)} → ∀ {i IS post} → (val : A) →
+return₁ : {A : Set (lsuc lzero)} → ∀ {i IS post} → (val : A) →
           ∞ActorM i IS A (post val) post
 return₁ val .force = Return val
 
@@ -559,8 +553,11 @@
 strengthen : ∀ {i IS xs ys} → ys ⊆ xs → ∞ActorM (↑ i) IS ⊤₁ xs (λ _ → ys)
 strengthen inc .force = Strengthen inc
 
+begin : ∀ {i IS A pre post} → ∞ActorM i IS A pre post → ActorM i IS A pre post
+begin = _∞>>_ (return tt)
+
 ⊠-of-values : List Set → InboxShape
 ⊠-of-values [] = []
-⊠-of-values (x ∷ vs) = (ValueType x ∷ []) ∷ ⊠-of-values vs
+⊠-of-values (x ∷ vs) = ([ ValueType x ]ˡ) ∷ ⊠-of-values vs
 \end{code}
 %</ActorMonadHelpers>

src/EnvironmentOperations.agda

@@ -1,24 +1,12 @@
 module EnvironmentOperations where
 open import ActorMonad
 open import SimulationEnvironment
-open import Membership using (_∈_ ; _⊆_ ; [] ; _∷_ ; Z ; S ; lookup-parallel ; lookup-parallel-≡ ; translate-∈ ; x∈[]-⊥ ; translate-⊆ ; ⊆-trans ; find-∈ ; All-⊆)
+open import Prelude
 
-open import Data.List using (List ; _∷_ ; [] ; map ; _++_ ; drop)
-open import Data.List.All using (All ; _∷_ ; []; lookup) renaming (map to ∀map)
 open import Data.List.All.Properties using (++⁺ ; drop⁺)
 open import Data.List.Properties using (map-++-commute)
-open import Data.List.Any using (Any ; here ; there)
-open import Data.Nat using (ℕ ; zero ; suc ; _≟_ ; _<_)
 open import Data.Nat.Properties using (≤-reflexive)
 open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax)
-open import Data.Unit using (⊤ ; tt)
-open import Data.Empty using (⊥ ; ⊥-elim)
-
-open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; cong ; cong₂ ; trans)
-open import Relation.Nullary using (Dec ; yes ; no ; ¬_)
-
-open import Level using (Lift ; lift)
-open import Size using (∞)
 
 open Actor
 open ValidActor
@@ -247,11 +235,11 @@ top-actor-to-back : Env → Env
 top-actor-to-back env with (acts env) | (actors-valid env)
 top-actor-to-back env | [] | _ = env
 top-actor-to-back env | x ∷ acts | (y ∷ prfs) = record
-                             { acts = acts Data.List.++ x ∷ []
+                             { acts = acts ++  [ x ]ˡ
                              ; blocked = blocked env
                              ; env-inboxes = env-inboxes env
                              ; store = store env
-                             ; actors-valid = ++⁺ prfs (y ∷ [])
+                             ; actors-valid = ++⁺ prfs [ y ]ᵃ
                              ; blocked-valid = blocked-valid env
                              ; messages-valid = messages-valid env
                              ; name-supply = name-supply env
@@ -577,7 +565,10 @@ block-focused env@record {
 -- Takes a named message and a proof that the named message is valid for the store.
 -- Values are valid for any store and references need a proof that the pointer is valid.
 add-message : {S : InboxShape} → {store : Store} → (message : NamedMessage S) → message-valid store message → (ValidMessageList store S → ValidMessageList store S)
-add-message message valid vml = record { inbox = inbox vml ++ (message ∷ []) ; valid = ++⁺ (ValidMessageList.valid vml) (valid ∷ []) }
+add-message message valid vml = record {
+  inbox = inbox vml ++ [ message ]ˡ
+  ; valid = ++⁺ (ValidMessageList.valid vml) [ valid ]ᵃ
+  }
 
 -- Removes the next message from an inbox.
 -- This is a no-op if there are no messages in the inbox.

src/Examples/Call.lagda.tex

@@ -2,27 +2,10 @@
 module Examples.Call where
 
 open import ActorMonad public
-open import Data.List using (List ; _∷_ ; [] ; _++_)
-open import Data.List.All using (All ; _∷_ ; [])
-open import Data.Bool using (Bool ; if_then_else_ ; false ; true)
-open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; _≟_)
-open import Coinduction
-open import Level using (Lift ; lift) renaming (zero to lzero ; suc to lsuc)
-open import Data.List.Any using (here ; there)
-open import Relation.Binary.PropositionalEquality
-            using (_≡_ ; refl ; cong ; sym ; inspect ; [_] ; trans)
-open import Membership using (
-            _∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] ; ⊆-refl
-            ; ⊆-trans ; ⊆-suc ; translate-⊆
-            ; ∈-inc ; ⊆++-refl)
-open import Data.Unit using (⊤ ; tt)
+open import Prelude
 open import Examples.SelectiveReceive using (
             selective-receive ; SelRec ; waiting-refs
             ; add-references++)
-open import Relation.Nullary using (yes ; no)
-
-open import Size
-
 open SelRec
 
 UniqueTag = ℕ
@@ -77,42 +60,41 @@
     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 = (
-  ValueType UniqueTag ∷
-  ReferenceType ((
-    ValueType UniqueTag ∷
-    ValueType ℕ ∷ []) ∷ []
-  ) ∷
-  ValueType ℕ ∷
-  ValueType ℕ ∷ []
-  ) ∷ []
+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)) ∷ [])
+        Z ![t: Z ] ((lift tag) ∷ [ lift (n + m) ]ᵃ )
         strengthen []
         loop
       ; (Msg (S ()) _) }
 
 TestBox : InboxShape
-TestBox = ((ValueType UniqueTag ∷ ValueType ℕ ∷ [])) ∷ [] ∷ []
+TestBox = AddReply
 
 calltestActor : ∀ {i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
-calltestActor .force = spawn∞ calculatorActor ∞>>
-                       [mid: (λ m → add-references (Calculator ∷ []) (msg m) ++
-                                    waiting-refs (waiting m)) ]
-                         call [] Z Z 0
-                           ((lift 10) ∷ ((lift 32) ∷ []))
-                           (Z ∷ []) Z >>=
-                       λ x → strengthen [] >>
-                       return-result x
+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 (Z ∷ []) Z) →
+    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 = () }

src/Examples/InfiniteBind.agda

@@ -1,12 +1,7 @@
 module Examples.InfiniteBind where
 
-open import ActorMonad public
-open import Data.List using (List ; _∷_ ; [])
-open import Coinduction
-open import Level using (Lift ; lift) renaming (zero to lzero ; suc to lsuc)
-open import Data.List.Any using (here ; there)
-open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
-open import Data.Unit using (⊤ ; tt)
+open import ActorMonad
+open import Prelude
 
 Box : InboxShape
 Box = []

src/Examples/Monad.lagda.tex

@@ -1,17 +1,14 @@
 \begin{code}
 module Examples.Monad where
-open import Data.Bool using (Bool ; false ; true)
-open import Data.Nat using (ℕ ; zero ; suc)
-open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
-
+open import Prelude
 infixl 1 _>>=_
 \end{code}
 
 %<*Monad>
 \begin{code}
-data Monad : Set → Set₁ where
-  return : ∀ {A} → A → Monad A
-  _>>=_ : ∀ {A B} → Monad A → (A → Monad B) → Monad B
+data Monad (B : Set) : Set₁ where
+  return : B → Monad B
+  _>>=_ : ∀ {A} → Monad A → (A → Monad B) → Monad B
 \end{code}
 %</Monad>
 

src/Examples/MonadID.lagda.tex

@@ -1,19 +1,17 @@
 \begin{code}
 module Examples.MonadID where
-open import Data.Bool using (Bool ; false ; true)
-open import Data.Nat using (ℕ ; zero ; suc)
-open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
+open import Prelude
 
 infixl 1 _>>=_
 \end{code}
 
 %<*Monad>
 \begin{code}
-data MonadID : Set → Set₁ where
-  return : ∀ {A} → A → MonadID A
-  _>>=_ : ∀ {A B} → MonadID A →
-                    (A → MonadID B) →
-                    MonadID B
+data MonadID (B : Set) : Set₁ where
+  return : B → MonadID B
+  _>>=_ : ∀ {A} → MonadID A →
+            (A → MonadID B) →
+            MonadID B
 \end{code}
 %</Monad>
 

src/Examples/MonadMaybe.lagda.tex

@@ -10,9 +10,9 @@
 
 %<*Monad>
 \begin{code}
-data Maybe : Set → Set₁ where
-  nothing : ∀ {A}  → Maybe A
-  just : ∀ {A} → A → Maybe A
+data Maybe (A : Set) : Set₁ where
+  nothing : Maybe A
+  just    : A → Maybe A
 
 return : ∀ {A} → A → Maybe A
 return = just

src/Examples/MonadParameterized.lagda.tex

@@ -11,9 +11,9 @@
 
 %<*Monad'>
 \begin{code}
-data MonadParam' : {p q : Set} → Set → p → q → Set₁ where
-    return : ∀ {A B} → {pre : B} → A → MonadParam' A pre pre
-    _>>=_ : ∀ {A B X Y Z} → {pre : X} → {mid : Y} → {post : Z} →
+data MonadParam' (B : Set) : {p q : Set} → p → q → Set₁ where
+    return : ∀ {p} → {pre : p} → B → MonadParam' B pre pre
+    _>>=_ : ∀ {A X Y Z} → {pre : X} → {mid : Y} → {post : Z} →
             MonadParam' A pre mid →
             (A → MonadParam' B mid post) →
             MonadParam' B pre post
@@ -22,10 +22,10 @@
 
 %<*Monad>
 \begin{code}
-data MonadParam : {p q : Set} → (A : Set) → p → (A → q) → Set₁ where
-    return : {A S : Set} → {post : A → S} → (val : A) →
-                MonadParam A (post val) post
-    _>>=_ : ∀ {A B X Y Z} → {pre : X} → {mid : A → Y} → {post : B → Z} →
+data MonadParam (B : Set) : {p q : Set} → p → (B → q) → Set₁ where
+    return : {S : Set} → {post : B → S} → (val : B) →
+                MonadParam B (post val) post
+    _>>=_ : ∀ {A X Y Z} → {pre : X} → {mid : A → Y} → {post : B → Z} →
                 MonadParam A pre mid →
                 ((x : A) → MonadParam B (mid x) post) →
                 MonadParam B pre post

src/Examples/NeedsFrameRule.lagda.tex

@@ -1,25 +1,24 @@
 \begin{code}
 module Examples.NeedsFrameRule where
 open import ActorMonad
-open import Data.Nat using (ℕ)
-open import Membership using (_∈_ ; Z)
-open import Data.List using (List ; [] ; _∷_ ; _++_)
-open import Data.List.All using (All ; [] ; _∷_)
-open import Size using (Size ; Size<_ ; ↑_)
-open import Level using (Lift ; lift)
+open import Prelude
 
 \end{code}
 %<*send-nat>
 \begin{code}
+
+NatMessage : MessageType
+NatMessage = [ ValueType ℕ ]ˡ
+
 send-nat : ∀ {i IS ToIS pre} →
                (canSendTo : ToIS ∈ pre) →
-               ((ValueType ℕ ∷ []) ∈ ToIS) →
+               (NatMessage ∈ ToIS) →
                ∞ActorM (↑ i) IS ⊤₁ pre (λ _ → pre)
-send-nat canSendTo p = canSendTo ![t: p ] (lift 42 ∷ [])
+send-nat canSendTo p = canSendTo ![t: p ] [ lift 42 ]ᵃ
 
 send-nat-frame : ∀ {i IS ToIS} →
-                 ((ValueType ℕ ∷ []) ∈ ToIS) →
-                 ∞ActorM (↑ i) IS ⊤₁ (ToIS ∷ []) (λ _ → ToIS ∷ [])
-send-nat-frame p = Z ![t: p ] (lift 42 ∷ [])
+                 (NatMessage ∈ ToIS) →
+                 ∞ActorM (↑ i) IS ⊤₁ [ ToIS ]ˡ (λ _ → [ ToIS ]ˡ)
+send-nat-frame p = Z ![t: p ] ([ lift 42 ]ᵃ)
 \end{code}
 %</send-nat>

src/Examples/Peano.lagda.tex

@@ -6,10 +6,10 @@
 \begin{code}
 data ℕ : Set where
     zero : ℕ
-    suc : ℕ → ℕ    
+    suc : ℕ → ℕ
 
 data _≤_ : ℕ → ℕ → Set where
     z≤n : {n : ℕ} → zero ≤ n
     s≤s : {n m : ℕ} → n ≤ m → suc n ≤ suc m
 \end{code}
-%</Peano>
+%</Peano>