Update versions

Due to changes in standard-library

README.md

@@ -9,14 +9,14 @@ in a style inspired by Effects from Idris and Koen Claessen's Poor Man's Concurr
 
 
 | Dependency       | Version                                  |
-|------------------|------------------------------------------|
-| Agda             | 2.5.4 |
-| standard-library | 2ff655cc3b6632ee0e3a52319360177b65ef59ce |
+|------------------|---------|
+| Agda             | 2.5.4.2 |
+| standard-library | v0.17   |
 
 ## How to build?
 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
+My preferred way is to to clone the repo, checkout the release-2.5.4.2 branch and run
 `stack install --stack-yaml stack-8.2.2.yaml`.
 
 The project itself can be built with make or using agda-mode in emacs.

src/ActorMonad.lagda.tex

@@ -265,7 +265,7 @@
 \begin{minipage}{\textwidth}
 \begin{code}
 send-field-content : TypingContext → MessageField → Set₁
-send-field-content Γ (ValueType A) = Lift A
+send-field-content Γ (ValueType A) = Lift (lsuc lzero) A
 send-field-content Γ (ReferenceType requested) = Γ ⊢>: requested
 \end{code}
 \end{minipage}
@@ -336,7 +336,7 @@
 \begin{code}
 infixl 1 _∞>>=_ _>>=_ _∞>>_ _>>_
 ⊤₁ : Set₁
-⊤₁ = Lift ⊤
+⊤₁ = Lift (lsuc lzero) ⊤
 \end{code}
 %<*ActorMonadHeader>
 \begin{code}
@@ -418,7 +418,7 @@
 
 -- universe lifting for return₁
 return : {A : Set} → ∀ {i IS post} → (val : A) →
-         ∞ActorM i IS (Lift A) (post (lift val)) post
+         ∞ActorM i IS (Lift (lsuc lzero) A) (post (lift val)) post
 return val = return₁ (lift val)
 
 _>>=_ : ∀ {i IS A B pre mid post} → (m : ∞ActorM i IS A pre mid) →

src/Examples/PingPong.agda

@@ -54,12 +54,12 @@ pingMainActor : (i : Size) (A : Set₁) → Set₂
 pingMainActor i A = ∞ActorM i Pingbox A PingRefs constPingrefs
 
 mutual
-  pingReceive : ∀ {i} (msg : Message Pingbox) → ∞ActorM i Pingbox (Lift Bool) (add-references PingRefs msg) constPingrefs
+  pingReceive : ∀ {i} (msg : Message Pingbox) → ∞ActorM i Pingbox (Lift (lsuc lzero) Bool) (add-references PingRefs msg) constPingrefs
   pingReceive (Msg Z (b ∷ [])) = return b
   pingReceive (Msg (S Z) _) = strengthen [ S Z ]ᵐ >> loopTillPingValue
   pingReceive (Msg (S (S ())) x₁)
 
-  loopTillPingValue : ∀ {i} → pingMainActor i (Lift Bool)
+  loopTillPingValue : ∀ {i} → pingMainActor i (Lift (lsuc lzero) Bool)
   loopTillPingValue .force = receive ∞>>= pingReceive
 
 pinger : ∀ {i} → ∞ActorM (↑ i) Pingbox ⊤₁ [] constPingrefs
@@ -83,11 +83,11 @@ pongMainActor : (i : Size) (A : Set₁) → Set₂
 pongMainActor i A = ∞ActorM i Pongbox A PongRefs constPongrefs
 
 mutual
-  pongReceive : ∀ {i} (msg : Message Pongbox) → ∞ActorM i Pongbox (Lift ℕ) (add-references PongRefs msg) constPongrefs
+  pongReceive : ∀ {i} (msg : Message Pongbox) → ∞ActorM i Pongbox (Lift (lsuc lzero) ℕ) (add-references PongRefs msg) constPongrefs
   pongReceive (Msg Z (n ∷ [])) = return n
   pongReceive (Msg (S Z) _) = strengthen [ S Z ]ᵐ >> loopTillPongValue
   pongReceive (Msg (S (S ())) _)
-  loopTillPongValue : ∀ {i} → pongMainActor i (Lift ℕ)
+  loopTillPongValue : ∀ {i} → pongMainActor i (Lift (lsuc lzero) ℕ)
   loopTillPongValue .force = receive ∞>>= pongReceive
 
 ponger : ∀ {i} → ∞ActorM (↑ i) Pongbox ⊤₁ [] constPongrefs

src/Examples/SimpleActor.lagda.tex

@@ -5,7 +5,7 @@
 open import Prelude
 
 ℕ₁ : Set₁
-ℕ₁ = Lift ℕ
+ℕ₁ = Lift (lsuc lzero) ℕ
 
 \end{code}
 %<*Interfaces>

src/Examples/TestCall.agda

@@ -18,10 +18,10 @@ AddMessage = ValueType UniqueTag ∷ ReferenceType AddReply ∷ ValueType ℕ 
 Calculator : InboxShape
 Calculator = [ AddMessage ]ˡ
 
-calculatorActor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift ⊤) [] (λ _ → [])
+calculatorActor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift (lsuc lzero) ⊤) [] (λ _ → [])
 calculatorActor = loop
   where
-    loop : ∀ {i} → ∞ActorM i Calculator (Lift ⊤) [] (λ _ → [])
+    loop : ∀ {i} → ∞ActorM i Calculator (Lift (lsuc lzero) ⊤) [] (λ _ → [])
     loop .force = receive ∞>>= λ {
       (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) → do
         Z ![t: Z ] ((lift tag) ∷ [ lift (n + m) ]ᵃ )
@@ -32,7 +32,7 @@ calculatorActor = loop
 TestBox : InboxShape
 TestBox = AddReply
 
-calltestActor : ∀ {i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
+calltestActor : ∀ {i} → ∞ActorM i TestBox (Lift (lsuc lzero) ℕ) [] (λ _ → [])
 calltestActor .force = spawn∞ calculatorActor ∞>> do
     x ← call [] Z Z 0
          ((lift 10) ∷ [ lift 32 ]ᵃ)
@@ -41,6 +41,6 @@ calltestActor .force = spawn∞ calculatorActor ∞>> do
     return-result x
   where
     return-result : SelRec TestBox (call-select 0 ⊆-refl Z) →
-                    ∀ {i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
+                    ∀ {i} → ∞ActorM i TestBox (Lift (lsuc lzero) ℕ) [] (λ _ → [])
     return-result record { msg = (Msg Z (tag ∷ n ∷ [])) } = return n
     return-result record { msg = (Msg (S x) x₁) ; msg-ok = () }

src/Examples/Types.lagda.tex

@@ -116,13 +116,13 @@
 %</ImplicitIdentity>
 %<*Lift>
 \begin{code}
-record Lift {a ℓ} (A : Set a) : Set (a ⊔ ℓ) where
+record Lift {a} ℓ (A : Set a) : Set (a ⊔ ℓ) where
   constructor lift
   field lower : A
 \end{code}
 %</Lift>
 %<*LiftBool>
 \begin{code}
-Bool₁ = Lift {lzero} {lsuc lzero} Bool
+Bool₁ = Lift (lsuc lzero) Bool
 \end{code}
 %</LiftBool>

src/Runtime.agda

@@ -4,7 +4,7 @@ open import SimulationEnvironment
 open import Prelude
 
 open import Data.Nat.Show using (show)
-open import Coinduction using ( ♯_ ; ♭)
+open import Codata.Musical.Notation using ( ♯_ ; ♭)
 import IO
 open ∞Trace
 

src/Selective/ActorMonad.lagda.tex

@@ -27,7 +27,7 @@
       actual-handles-requested : requested <: actual
 
 send-field-content : TypingContext → MessageField → Set₁
-send-field-content Γ (ValueType A) = Lift A
+send-field-content Γ (ValueType A) = Lift (lsuc lzero) A
 send-field-content Γ (ReferenceType requested) = Γ ⊢>: requested
 
 record SendMessage (To : InboxShape) (Γ : TypingContext) : Set₁ where
@@ -99,7 +99,7 @@
 
 
 ⊤₁ : Set₁
-⊤₁ = Lift ⊤
+⊤₁ = Lift (lsuc lzero) ⊤
 
 infixl 1 _∞>>=_ _>>=_ _∞>>_ _>>_
 
@@ -157,7 +157,7 @@
 return₁ val .force = Return val
 
 -- universe lifting for return₁
-return : {A : Set} → ∀ {i IS post} → (val : A) → ∞ActorM i IS (Lift A) (post (lift val)) post
+return : {A : Set} → ∀ {i IS post} → (val : A) → ∞ActorM i IS (Lift (lsuc lzero) A) (post (lift val)) post
 return val = return₁ (lift val)
 
 _>>=_ : ∀ {i IS A B pre mid post} → (m : ∞ActorM i IS A pre mid) →

src/Selective/ActorMonadNoText.lagda.tex

@@ -27,7 +27,7 @@
       actual-handles-requested : requested <: actual
 
 send-field-content : TypingContext → MessageField → Set₁
-send-field-content Γ (ValueType A) = Lift A
+send-field-content Γ (ValueType A) = Lift (lsuc lzero) A
 send-field-content Γ (ReferenceType requested) = Γ ⊢>: requested
 
 data SendMessage (To : InboxShape) (Γ : TypingContext) : Set₁ where
@@ -76,7 +76,7 @@
 
 
 ⊤₁ : Set₁
-⊤₁ = Lift ⊤
+⊤₁ = Lift (lsuc lzero) ⊤
 
 infixl 1 _∞>>=_ _>>=_ _∞>>_ _>>_
 
@@ -132,7 +132,7 @@
 return₁ val .force = Return val
 
 -- universe lifting for return₁
-return : {A : Set} → ∀ {i IS post} → (val : A) → ∞ActorM i IS (Lift A) (post (lift val)) post
+return : {A : Set} → ∀ {i IS post} → (val : A) → ∞ActorM i IS (Lift (lsuc lzero) A) (post (lift val)) post
 return val = return₁ (lift val)
 
 _>>=_ : ∀ {i IS A B pre mid post} → (m : ∞ActorM i IS A pre mid) →

src/Selective/Examples/Bookstore.agda

@@ -153,7 +153,7 @@ seller = begin do
     select-decision (Msg (S Z) _) = true
     select-decision _ = false
     wait-for-decision : ∀ {i Γ} →
-                        ∞ActorM i SellerInterface (Lift AgreeChoice) Γ (λ _ → Γ)
+                        ∞ActorM i SellerInterface (Lift (lsuc lzero) AgreeChoice) Γ (λ _ → Γ)
     wait-for-decision = do
       record { msg = Msg (S Z) (ac ∷ []) } ← (selective-receive select-decision)
         where
@@ -165,7 +165,7 @@ seller = begin do
     select-contribution-from _ _ = false
     wait-for-money-from : ∀ {i Γ} →
                           BuyerRole →
-                          ∞ActorM i SellerInterface (Lift Contribution) Γ (λ _ → Γ)
+                          ∞ActorM i SellerInterface (Lift (lsuc lzero) Contribution) Γ (λ _ → Γ)
     wait-for-money-from br = do
       record { msg = Msg (S (S Z)) (_ ∷ contribution ∷ []) } ← (selective-receive (select-contribution-from br))
         where
@@ -232,7 +232,7 @@ buyer1 = begin do
                Γ ⊢ Buyer1-to-Seller →
                UniqueTag →
                BookTitle →
-               ∞ActorM i Buyer1Interface (Lift (Maybe Book)) Γ (λ _ → Γ)
+               ∞ActorM i Buyer1Interface (Lift (lsuc lzero) (Maybe Book)) Γ (λ _ → Γ)
     get-quote p tag title = do
       record { msg = Msg (S (S Z)) (_ ∷ book ∷ []) ; msg-ok = msg-ok } ← call p Z tag [ lift title ]ᵃ [ S (S Z) ]ᵐ Z
         where
@@ -251,7 +251,7 @@ buyer1 = begin do
     select-decision (Msg (S (S (S Z))) _) = true
     select-decision _ = false
     wait-for-decision : ∀ {i Γ} →
-                        ∞ActorM i Buyer1Interface (Lift AgreeChoice) Γ (λ _ → Γ)
+                        ∞ActorM i Buyer1Interface (Lift (lsuc lzero) AgreeChoice) Γ (λ _ → Γ)
     wait-for-decision = do
       record {msg = Msg (S (S (S Z))) (ac ∷ []) } ← (selective-receive select-decision)
         where
@@ -296,7 +296,7 @@ buyer2 = begin do
     select-contribution : MessageFilter Buyer2Interface
     select-contribution (Msg (S (S Z)) _) = true
     select-contribution _ = false
-    wait-for-contribution : ∀ {i Γ} → ∞ActorM i Buyer2Interface (Lift Contribution) Γ (λ _ → Γ)
+    wait-for-contribution : ∀ {i Γ} → ∞ActorM i Buyer2Interface (Lift (lsuc lzero) Contribution) Γ (λ _ → Γ)
     wait-for-contribution = do
       record { msg = Msg (S (S Z)) (cc ∷ []) } ← (selective-receive select-contribution)
         where

src/Selective/Examples/CalculatorProtocol.agda

@@ -41,8 +41,8 @@ TestBox : InboxShape
 TestBox = ℕ-Reply
 
 calculator-test-actor : ∀{i} →
-  ∞ActorM (↑ i) Calculator (Lift ⊤) [] (λ _ → []) →
-  ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
+  ∞ActorM (↑ i) Calculator (Lift (lsuc lzero) ⊤) [] (λ _ → []) →
+  ∞ActorM i TestBox (Lift (lsuc lzero) ℕ) [] (λ _ → [])
 calculator-test-actor calculator-actor = do
   spawn∞ calculator-actor
   Msg Z (_ ∷ n ∷ []) ← call CalculateProtocol (record {

src/Selective/Examples/Chat.agda

@@ -6,6 +6,7 @@ open import Prelude
   hiding (Maybe)
 open import Data.Maybe as Maybe
   hiding (map)
+open import Data.Maybe.Categorical as CMaybe
 
 open import Data.List.Properties
 open import Category.Monad
@@ -246,8 +247,8 @@ lookup-room rms name =
     loop [] [] = nothing
     loop [] (x ∷ xs) with (x ≟ name)
     ... | (yes p) = just Z
-    ... | (no _) = RawMonad._>>=_ Maybe.monad (loop [] xs) λ p → just (S p)
-    loop (x ∷ Γ) rl = RawMonad._>>=_ Maybe.monad (loop Γ rl) (λ p → just (S p))
+    ... | (no _) = RawMonad._>>=_ CMaybe.monad (loop [] xs) λ p → just (S p)
+    loop (x ∷ Γ) rl = RawMonad._>>=_ CMaybe.monad (loop Γ rl) (λ p → just (S p))
 
 room-manager : ∀ {i} → ActorM i RoomManagerInterface RoomManagerState [] rms-to-context
 room-manager = begin (loop (record { rooms = [] }))
@@ -355,7 +356,7 @@ client-create-room : ∀ {i } →
                      Γ ⊢ RoomManagerInterface →
                      UniqueTag →
                      RoomName →
-                     ∞ActorM i ClientInterface (Lift CreateRoomResult) Γ (λ _ → Γ)
+                     ∞ActorM i ClientInterface (Lift (lsuc lzero) CreateRoomResult) Γ (λ _ → Γ)
 client-create-room p tag name = do
   record { msg = (Msg (S Z) (_ ∷ cr ∷ [])) } ← (call p (S Z) tag [ lift name ]ᵃ [ S Z ]ᵐ Z)
     where
@@ -364,7 +365,7 @@ client-create-room p tag name = do
   return cr
 
 add-if-join-success : TypingContext →
-                      Lift {lzero} {lsuc lzero} JoinRoomStatus →
+                      Lift (lsuc lzero) JoinRoomStatus →
                       TypingContext
 add-if-join-success Γ (lift (JRS-SUCCESS x)) = Client-to-Room ∷ Γ
 add-if-join-success Γ (lift (JRS-FAIL x)) = Γ
@@ -374,7 +375,7 @@ client-join-room : ∀ {i Γ} →
                    UniqueTag →
                    RoomName →
                    ClientName →
-                   ∞ActorM i ClientInterface (Lift JoinRoomStatus) Γ (add-if-join-success Γ)
+                   ∞ActorM i ClientInterface (Lift (lsuc lzero) JoinRoomStatus) Γ (add-if-join-success Γ)
 client-join-room p tag room-name client-name = do
     self
     S p ![t: Z ] (lift tag ∷ (([ Z ]>: ⊆-suc (⊆-suc (⊆-suc ⊆-refl))) ∷ (lift room-name) ∷ [ lift client-name ]ᵃ))
@@ -391,7 +392,7 @@ client-join-room p tag room-name client-name = do
     select-join-reply tag (Msg (S (S (S (S (S Z))))) x₁) = false
     select-join-reply tag (Msg (S (S (S (S (S (S ())))))) _)
     handle-message : ∀ {tag i Γ} → (m : SelectedMessage (select-join-reply tag)) →
-                     ∞ActorM i ClientInterface (Lift JoinRoomStatus)
+                     ∞ActorM i ClientInterface (Lift (lsuc lzero) JoinRoomStatus)
                        (add-selected-references Γ m) (add-if-join-success Γ)
     handle-message record { msg = (Msg Z _) ; msg-ok = () }
     handle-message record { msg = (Msg (S Z) _) ; msg-ok = () }
@@ -409,7 +410,7 @@ client-send-message : ∀ {i  Γ} →
 client-send-message p client-name message = p ![t: Z ] [ lift (chat-from client-name message: message) ]ᵃ
 
 client-receive-message : ∀ {i Γ} →
-                         ∞ActorM i ClientInterface (Lift ChatMessageContent) Γ (λ _ → Γ)
+                         ∞ActorM i ClientInterface (Lift (lsuc lzero) ChatMessageContent) Γ (λ _ → Γ)
 client-receive-message = do
     m ← (selective-receive select-message)
     handle-message m
@@ -418,7 +419,7 @@ client-receive-message = do
     select-message (Msg (S (S (S (S (S Z))))) _) = true
     select-message (Msg _ _) = false
     handle-message : ∀ {i Γ} → (m : SelectedMessage select-message) →
-                     ∞ActorM i ClientInterface (Lift ChatMessageContent) (add-selected-references Γ m) (λ _ → Γ)
+                     ∞ActorM i ClientInterface (Lift (lsuc lzero) ChatMessageContent) (add-selected-references Γ m) (λ _ → Γ)
     handle-message record { msg = (Msg Z _) ; msg-ok = () }
     handle-message record { msg = (Msg (S Z) _) ; msg-ok = () }
     handle-message record { msg = (Msg (S (S Z)) _) ; msg-ok = () }

src/Selective/Examples/ChatAO.agda

@@ -428,7 +428,7 @@ client-create-room : ∀ {i } →
                      Γ ⊢ RoomManagerInterface →
                      UniqueTag →
                      RoomName →
-                     ∞ActorM i ClientInterface (Lift CreateRoomResult) Γ (λ _ → Γ)
+                     ∞ActorM i ClientInterface (Lift (lsuc lzero) CreateRoomResult) Γ (λ _ → Γ)
 client-create-room p tag name = do
   Msg Z (_ ∷ cr ∷ []) ← (call create-room-ci (record {
     var = p
@@ -447,7 +447,7 @@ client-create-room p tag name = do
   return cr
 
 add-if-join-success : TypingContext →
-                      Lift {lzero} {lsuc lzero} JoinRoomStatus →
+                      Lift (lsuc lzero) JoinRoomStatus →
                       TypingContext
 add-if-join-success Γ (lift (JRS-SUCCESS x)) = Client-to-Room ∷ Γ
 add-if-join-success Γ (lift (JRS-FAIL x)) = Γ
@@ -457,7 +457,7 @@ client-join-room : ∀ {i Γ} →
                    UniqueTag →
                    RoomName →
                    ClientName →
-                   ∞ActorM i ClientInterface (Lift JoinRoomStatus) Γ (add-if-join-success Γ)
+                   ∞ActorM i ClientInterface (Lift (lsuc lzero) JoinRoomStatus) Γ (add-if-join-success Γ)
 client-join-room p tag room-name client-name = do
     self
     S p ![t: Z ] (lift tag ∷ (([ Z ]>: ⊆-suc (⊆-suc (⊆-suc ⊆-refl))) ∷ (lift room-name) ∷ [ lift client-name ]ᵃ))
@@ -474,7 +474,7 @@ client-join-room p tag room-name client-name = do
     select-join-reply tag (Msg (S (S (S (S (S Z))))) x₁) = false
     select-join-reply tag (Msg (S (S (S (S (S (S ())))))) _)
     handle-message : ∀ {tag i Γ} → (m : SelectedMessage (select-join-reply tag)) →
-                     ∞ActorM i ClientInterface (Lift JoinRoomStatus)
+                     ∞ActorM i ClientInterface (Lift (lsuc lzero) JoinRoomStatus)
                        (add-selected-references Γ m) (add-if-join-success Γ)
     handle-message record { msg = (Msg Z _) ; msg-ok = () }
     handle-message record { msg = (Msg (S Z) _) ; msg-ok = () }
@@ -492,7 +492,7 @@ client-send-message : ∀ {i  Γ} →
 client-send-message p client-name message = p ![t: Z ] ([ lift (chat-from client-name message: message) ]ᵃ)
 
 client-receive-message : ∀ {i Γ} →
-                         ∞ActorM i ClientInterface (Lift ChatMessageContent) Γ (λ _ → Γ)
+                         ∞ActorM i ClientInterface (Lift (lsuc lzero) ChatMessageContent) Γ (λ _ → Γ)
 client-receive-message = do
     m ← (selective-receive select-message)
     handle-message m
@@ -501,7 +501,7 @@ client-receive-message = do
     select-message (Msg (S (S (S (S (S Z))))) _) = true
     select-message (Msg _ _) = false
     handle-message : ∀ {i Γ} → (m : SelectedMessage select-message) →
-                     ∞ActorM i ClientInterface (Lift ChatMessageContent) (add-selected-references Γ m) (λ _ → Γ)
+                     ∞ActorM i ClientInterface (Lift (lsuc lzero) ChatMessageContent) (add-selected-references Γ m) (λ _ → Γ)
     handle-message record { msg = (Msg Z _) ; msg-ok = () }
     handle-message record { msg = (Msg (S Z) _) ; msg-ok = () }
     handle-message record { msg = (Msg (S (S Z)) _) ; msg-ok = () }

src/Selective/Examples/Fibonacci.agda

@@ -81,7 +81,7 @@ client = wait-for-server ∞>> run 10 0
         record { msg = (Msg Z _) ; msg-ok = msg-ok } → return tt
         ; record { msg = (Msg (S _) _) ; msg-ok = () }
         }
-    wait-for-value : ∀ {i} → ∞ActorM i ClientInterface (Lift ℕ) ClientRefs constClientRefs
+    wait-for-value : ∀ {i} → ∞ActorM i ClientInterface (Lift (lsuc lzero) ℕ) ClientRefs constClientRefs
     wait-for-value = do
       record { msg = Msg (S Z) (n ∷ []) } ← selective-receive (λ {
         (Msg Z _) → false

src/Selective/Examples/PingPong.agda

@@ -20,10 +20,10 @@ Spawnbox : InboxShape
 Spawnbox = []
 
 ℕ₁ : Set₁
-ℕ₁ = Lift ℕ
+ℕ₁ = Lift (lsuc lzero) ℕ
 
 Bool₁ : Set₁
-Bool₁ = Lift Bool
+Bool₁ = Lift (lsuc lzero) Bool
 
 mutual
   PingValues = [ Bool ]ˡ