From ee50b2e53c936c96cbb85f35fa30a447fc5137c9 Mon Sep 17 00:00:00 2001 From: Pierre Krafft Date: Fri, 11 May 2018 12:14:18 +0200 Subject: [PATCH] Prelude and singleton --- Makefile | 2 +- src/ActorMonad.lagda.tex | 15 +-- src/EnvironmentOperations.agda | 23 ++-- src/Examples/ArbitraryBind.agda | 20 --- src/Examples/Call.lagda.tex | 58 +++------ src/Examples/InfiniteBind.agda | 9 +- src/Examples/Monad.lagda.tex | 11 +- src/Examples/MonadID.lagda.tex | 14 +-- src/Examples/MonadMaybe.lagda.tex | 6 +- src/Examples/MonadParameterized.lagda.tex | 14 +-- src/Examples/NeedsFrameRule.lagda.tex | 21 ++-- src/Examples/Peano.lagda.tex | 4 +- src/Examples/PingPong.agda | 58 ++++----- src/Examples/SelectiveReceive.lagda.tex | 32 ++--- src/Examples/SizedStream.lagda.tex | 4 +- src/Examples/Stream.lagda.tex | 3 +- src/Examples/Types.lagda.tex | 44 ++----- src/NatProps.agda | 2 - src/Prelude.agda | 69 +++++++++++ src/Runtime.agda | 14 +-- src/Selective/ActorMonad.lagda.tex | 15 +-- src/Selective/ActorMonadNoText.lagda.tex | 15 +-- src/Selective/EnvironmentOperations.agda | 23 ++-- src/Selective/Examples/ActiveObjects.agda | 23 ++-- src/Selective/Examples/Bookstore.agda | 91 ++++++-------- src/Selective/Examples/Call.lagda.tex | 57 ++++----- src/Selective/Examples/Call2.agda | 56 +++------ .../Examples/CallNoComments.lagda.tex | 106 +++++++--------- src/Selective/Examples/Channel.agda | 20 +-- src/Selective/Examples/Chat.agda | 117 ++++++++---------- src/Selective/Examples/Fibonacci.agda | 47 +++---- src/Selective/Examples/PingPong.agda | 62 +++++----- src/Selective/Examples/TestAC.agda | 46 +++---- src/Selective/Runtime.agda | 14 +-- src/Selective/Simulate.agda | 12 +- src/Selective/SimulationEnvironment.agda | 39 +++--- src/Simulate.agda | 20 ++- src/SimulationEnvironment.agda | 38 +++--- src/Singleton.agda | 17 +++ 39 files changed, 522 insertions(+), 719 deletions(-) delete mode 100644 src/Examples/ArbitraryBind.agda create mode 100644 src/Prelude.agda create mode 100644 src/Singleton.agda diff --git a/Makefile b/Makefile index be07352..af9de9a 100644 --- a/Makefile +++ b/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/)) diff --git a/src/ActorMonad.lagda.tex b/src/ActorMonad.lagda.tex index 3c3fb9b..4e99fa0 100644 --- a/src/ActorMonad.lagda.tex +++ b/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} % diff --git a/src/EnvironmentOperations.agda b/src/EnvironmentOperations.agda index 68698f0..d24291a 100644 --- a/src/EnvironmentOperations.agda +++ b/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. diff --git a/src/Examples/ArbitraryBind.agda b/src/Examples/ArbitraryBind.agda deleted file mode 100644 index 1f998c4..0000000 --- a/src/Examples/ArbitraryBind.agda +++ /dev/null @@ -1,20 +0,0 @@ -module Examples.ArbitraryBind where - -open import ActorMonad public -open import Data.List using (List ; _∷_ ; []) -open import Data.Bool using (Bool ; if_then_else_ ; false ; true) -open import Coinduction -open import Level using (Lift ; lift) renaming (zero to lzero ; suc to lsuc) -open import Relation.Binary.PropositionalEquality using (_≡_ ; refl) -open import Membership using (_∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] ; ⊆-refl) - -ArbitraryBox : InboxShape -ArbitraryBox = [] - -ifSelf : (Lift {lzero} {lsuc lzero} Bool) → TypingContext -ifSelf (lift false) = [] -ifSelf (lift true) = ArbitraryBox ∷ [] - -arbitraryActor : Bool → ActorM ArbitraryBox (Lift Bool) [] ifSelf -arbitraryActor false = return false >>= return₁ -arbitraryActor true = ♯ Self >>= λ _ → return true diff --git a/src/Examples/Call.lagda.tex b/src/Examples/Call.lagda.tex index 782b477..b6d4abf 100644 --- a/src/Examples/Call.lagda.tex +++ b/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,16 +60,17 @@ 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 @@ -94,25 +78,23 @@ 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 = () } diff --git a/src/Examples/InfiniteBind.agda b/src/Examples/InfiniteBind.agda index f0c7d95..53b32b2 100644 --- a/src/Examples/InfiniteBind.agda +++ b/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 = [] diff --git a/src/Examples/Monad.lagda.tex b/src/Examples/Monad.lagda.tex index ba79bfb..c4607b1 100644 --- a/src/Examples/Monad.lagda.tex +++ b/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} % diff --git a/src/Examples/MonadID.lagda.tex b/src/Examples/MonadID.lagda.tex index 0bfd760..b667415 100644 --- a/src/Examples/MonadID.lagda.tex +++ b/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} % diff --git a/src/Examples/MonadMaybe.lagda.tex b/src/Examples/MonadMaybe.lagda.tex index a7526dd..483435e 100644 --- a/src/Examples/MonadMaybe.lagda.tex +++ b/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 diff --git a/src/Examples/MonadParameterized.lagda.tex b/src/Examples/MonadParameterized.lagda.tex index ec551c9..d3ec816 100644 --- a/src/Examples/MonadParameterized.lagda.tex +++ b/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 diff --git a/src/Examples/NeedsFrameRule.lagda.tex b/src/Examples/NeedsFrameRule.lagda.tex index 6ea8b0d..b1b9aa9 100644 --- a/src/Examples/NeedsFrameRule.lagda.tex +++ b/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} % diff --git a/src/Examples/Peano.lagda.tex b/src/Examples/Peano.lagda.tex index 65ab698..fad7e82 100644 --- a/src/Examples/Peano.lagda.tex +++ b/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} -% \ No newline at end of file +% diff --git a/src/Examples/PingPong.agda b/src/Examples/PingPong.agda index 9c077ad..d2dfb24 100644 --- a/src/Examples/PingPong.agda +++ b/src/Examples/PingPong.agda @@ -1,16 +1,7 @@ module Examples.PingPong 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 Size -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 Membership using (_∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] ; ⊆-refl) -open import Data.Unit using (⊤ ; tt) +open import Prelude -- An example including three actors: spawner, pinger, ponger -- @@ -29,19 +20,31 @@ Spawnbox : InboxShape Spawnbox = [] mutual - PingValues = Bool ∷ [] - PongValues = ℕ ∷ [] + PingValues = [ Bool ]ˡ + PongValues = [ ℕ ]ˡ - PingRefs : ReferenceTypes - PingRefs = (⊠-of-values PongValues) ∷ [] - PongRefs : ReferenceTypes - PongRefs = ⊠-of-values PingValues ∷ [] + PingRefs : TypingContext + PingRefs = [ ⊠-of-values PongValues ]ˡ + PongRefs : TypingContext + PongRefs = [ ⊠-of-values PingValues ]ˡ + + PongReferenceMessage : MessageType + PongReferenceMessage = [ ReferenceType (⊠-of-values PongValues) ]ˡ + + BoolMessage : MessageType + BoolMessage = [ ValueType Bool ]ˡ Pingbox : InboxShape - Pingbox = (ValueType Bool ∷ []) ∷ (ReferenceType (⊠-of-values PongValues) ∷ []) ∷ [] + Pingbox = BoolMessage ∷ [ PongReferenceMessage ]ˡ + + PingReferenceMessage : MessageType + PingReferenceMessage = [ ReferenceType (⊠-of-values PingValues) ]ˡ + + NatMessage : MessageType + NatMessage = [ ValueType ℕ ]ˡ Pongbox : InboxShape - Pongbox = (ValueType ℕ ∷ []) ∷ (ReferenceType (⊠-of-values PingValues) ∷ []) ∷ [] + Pongbox = NatMessage ∷ [ PingReferenceMessage ]ˡ constPingrefs : {A : Set₁} → (A → TypingContext) @@ -53,7 +56,7 @@ 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 (Msg Z (b ∷ [])) = return b - pingReceive (Msg (S Z) _) = strengthen (S Z ∷ []) >> loopTillPingValue + pingReceive (Msg (S Z) _) = strengthen [ S Z ]ᵐ >> loopTillPingValue pingReceive (Msg (S (S ())) x₁) loopTillPingValue : ∀ {i} → pingMainActor i (Lift Bool) @@ -70,7 +73,7 @@ pinger .force = loopTillPong ∞>> pingMain 0 })) pingMain : ∀ {i} → ℕ → pingMainActor i ⊤₁ pingMain n .force = loopTillPingValue ∞>>= λ - { (lift false) → (Z ![t: Z ] (lift n ∷ [])) >> pingMain (suc n) + { (lift false) → (Z ![t: Z ] ( [ lift n ]ᵃ)) >> pingMain (suc n) ; (lift true) → return _} constPongrefs : {A : Set₁} → (A → TypingContext) @@ -82,13 +85,13 @@ 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 (Msg Z (n ∷ [])) = return n - pongReceive (Msg (S Z) _) = strengthen (S Z ∷ []) >> loopTillPongValue + pongReceive (Msg (S Z) _) = strengthen [ S Z ]ᵐ >> loopTillPongValue pongReceive (Msg (S (S ())) _) loopTillPongValue : ∀ {i} → pongMainActor i (Lift ℕ) loopTillPongValue .force = receive ∞>>= pongReceive ponger : ∀ {i} → ∞ActorM (↑ i) Pongbox ⊤₁ [] constPongrefs -ponger .force = loopTillPing ∞>> ((Z ![t: Z ] ((lift false) ∷ [])) >> pongMain) +ponger .force = loopTillPing ∞>> ((Z ![t: Z ] ([ lift false ]ᵃ)) >> pongMain) where loopTillPing : ∀ {i} → ∞ActorM i Pongbox ⊤₁ [] constPongrefs loopTillPing .force = receive ∞>>= λ { @@ -98,14 +101,13 @@ ponger .force = loopTillPing ∞>> ((Z ![t: Z ] ((lift false) ∷ [])) >> pongMa } pongMain : ∀ {i} → pongMainActor i ⊤₁ pongMain .force = loopTillPongValue ∞>>= λ { - (lift 10) → Z ![t: Z ] ((lift true) ∷ []) - ; (lift n) → (Z ![t: Z ] ((lift false) ∷ [])) >> pongMain + (lift 10) → Z ![t: Z ] [ lift true ]ᵃ + ; (lift n) → Z ![t: Z ] [ lift false ]ᵃ >> pongMain } --- TODO: this needs to look prettier -spawner : ∀ {i} → ∞ActorM i Spawnbox ⊤₁ [] (λ _ → Pingbox ∷ Pongbox ∷ []) +spawner : ∀ {i} → ∞ActorM i Spawnbox ⊤₁ [] (λ _ → Pingbox ∷ [ Pongbox ]ˡ) spawner = do spawn∞ ponger spawn∞ pinger - Z ![t: S Z ] (([ (S Z) ]>: (Z ∷ [])) ∷ []) - S Z ![t: S Z ] (([ Z ]>: (Z ∷ [])) ∷ []) + Z ![t: S Z ] [ [ S Z ]>: [ Z ]ᵐ ]ᵃ + S Z ![t: S Z ] [ [ Z ]>: [ Z ]ᵐ ]ᵃ diff --git a/src/Examples/SelectiveReceive.lagda.tex b/src/Examples/SelectiveReceive.lagda.tex index c92c736..f3187df 100644 --- a/src/Examples/SelectiveReceive.lagda.tex +++ b/src/Examples/SelectiveReceive.lagda.tex @@ -3,20 +3,8 @@ module Examples.SelectiveReceive where open import ActorMonad public -open import Data.List using (List ; _∷_ ; [] ; _++_) -open import Data.List.All using (All ; _∷_ ; []) +open import Prelude open import Data.List.Properties using (++-assoc ; ++-identityʳ) -open import Data.Bool using (Bool ; false ; true) -open import Data.Nat using (ℕ ; zero ; suc) -open import Level using (Level ; Lift ; lift) - renaming (zero to lzero ; suc to lsuc) -open import Size using (Size ; ↑_) -open import Data.List.Any using (here ; there) -open import Relation.Binary.PropositionalEquality - using (_≡_ ; refl ; cong ; sym ; inspect ; [_] ; trans) -open import Membership -open import Data.Unit using (⊤ ; tt) - waiting-refs : ∀ {IS} → (q : List (Message IS)) → ReferenceTypes waiting-refs [] = [] @@ -82,10 +70,10 @@ move-received : ∀ {IS} → ∀ pre → (q : List (Message IS)) → (x : Message IS) → - (pre ++ (waiting-refs (q ++ (x ∷ [])))) ⊆ + (pre ++ (waiting-refs (q ++ [ x ]ˡ))) ⊆ (add-references (pre ++ waiting-refs q) x) move-received pre q (Msg {MT} x x₁) rewrite - (waiting-refs++ q (Msg x x₁ ∷ [])) | + (waiting-refs++ q [ Msg x x₁ ]ˡ) | (++-identityʳ (extract-references MT)) = ⊆-trans move-1 move-2 where @@ -225,7 +213,7 @@ handle-receive x with (f x) | (inspect f x) handle-receive {i} x | false | p = strengthen (move-received Γ q x) >> - selective-receive (q ++ (x ∷ [])) f + selective-receive (q ++ [ x ]ˡ) f handle-receive x | true | [ p ] = strengthen (accept-received Γ q x) >> return₁ ret-v @@ -235,8 +223,10 @@ \end{code} \begin{code} + +BoolMessage = [ ValueType Bool ]ˡ SelectiveTestBox : InboxShape -SelectiveTestBox = (ValueType Bool ∷ []) ∷ [] +SelectiveTestBox = [ BoolMessage ]ˡ testActor : ∀ {i} → ActorM i SelectiveTestBox (Lift Bool) [] (λ _ → []) testActor = selective-receive [] only-true ∞>>= after-receive @@ -255,8 +245,8 @@ after-receive record { msg = (Msg (S ()) _) } spawner : ∀ {i} → ActorM i [] ⊤₁ [] (λ _ → []) -spawner = - spawn testActor ∞>> - ((Z ![t: Z ] ((lift true) ∷ [])) >> - strengthen []) +spawner = begin do + spawn testActor + Z ![t: Z ] [ lift true ]ᵃ + strengthen [] \end{code} diff --git a/src/Examples/SizedStream.lagda.tex b/src/Examples/SizedStream.lagda.tex index 1f8a87b..884270e 100644 --- a/src/Examples/SizedStream.lagda.tex +++ b/src/Examples/SizedStream.lagda.tex @@ -1,8 +1,6 @@ \begin{code} module Examples.SizedStream where -open import Data.Nat -open import Relation.Binary.PropositionalEquality using (_≡_ ; refl) -open import Size using (Size ; Size<_ ; ↑_) +open import Prelude \end{code} %<*Stream> diff --git a/src/Examples/Stream.lagda.tex b/src/Examples/Stream.lagda.tex index 45d2c5d..dde3fe3 100644 --- a/src/Examples/Stream.lagda.tex +++ b/src/Examples/Stream.lagda.tex @@ -1,7 +1,6 @@ \begin{code} module Examples.Stream where -open import Data.Nat -open import Relation.Binary.PropositionalEquality using (_≡_ ; refl) +open import Prelude \end{code} %<*Stream> diff --git a/src/Examples/Types.lagda.tex b/src/Examples/Types.lagda.tex index b0418ea..efd79f4 100644 --- a/src/Examples/Types.lagda.tex +++ b/src/Examples/Types.lagda.tex @@ -6,33 +6,12 @@ open import Data.Unit using (⊤ ; tt) open import Data.Bool using (Bool ; false ; true) open import Data.Nat using (ℕ ; zero ; suc ; _+_) -open import Data.Vec using (Vec ; [] ; _∷_) open import Data.List using (List ; [] ; _∷_) open import Data.List.All using (All ; [] ; _∷_) open import Data.String using (String) open import ActorMonad open import Membership using (_∈_; _⊆_ ; _∷_ ; [] ; S ; Z) - -record Singleton {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where - field - [_] : A → B -open Singleton {{...}} - -instance - singletonList : ∀{a}{A : Set a} → Singleton A (List A) - singletonList .Singleton.[_] a = a ∷ [] - - singletonAll : ∀{a p} {A : Set a} {P : A → Set p} {x : A} → Singleton (P x) (All P (x ∷ [])) - singletonAll .Singleton.[_] p = p ∷ [] - - singletonMem : ∀{a} {A : Set a} {x : A} {ys : List A} → Singleton (x ∈ ys) ((x ∷ []) ⊆ ys) - singletonMem .Singleton.[_] p = p ∷ [] - -[_]ˡ : ∀{a}{A : Set a} → A → List A -[ a ]ˡ = a ∷ [] - -[_]ᵐ : ∀{a} {A : Set a} {x : A} {ys : List A} → (x ∈ ys) → ((x ∷ []) ⊆ ys) -[ p ]ᵐ = p ∷ [] +open import Singleton \end{code} %<*PropositionalEquality> @@ -49,7 +28,7 @@ %<*Cong> \begin{code} -cong : ∀ {a} {A B : Set a} {m n : A} → (f : A → B) → m ≡ n → f m ≡ f n +cong : {A B : Set} {m n : A} → (f : A → B) → m ≡ n → f m ≡ f n cong f refl = refl @@ -78,22 +57,23 @@ %<*ExampleInbox> \begin{code} +BoolMessage = [ ValueType Bool ]ˡ +StringMessage = [ ValueType String ]ˡ + +OtherInbox : InboxShape +OtherInbox = StringMessage ∷ [ BoolMessage ]ˡ +RefNatMessage : MessageType +RefNatMessage = ReferenceType OtherInbox ∷ [ ValueType ℕ ]ˡ + TestInbox : InboxShape -TestInbox = ( ReferenceType ( - [ ValueType String ]ˡ - ∷ [ ValueType Bool ]ˡ - ∷ []) - ∷ ValueType ℕ - ∷ []) - ∷ [ ValueType Bool ]ˡ - ∷ [] +TestInbox = RefNatMessage ∷ [ BoolMessage ]ˡ \end{code} % %<*Subtyping> \begin{code} Boolbox : InboxShape -Boolbox = [ [ ValueType Bool ]ˡ ]ˡ +Boolbox = [ BoolMessage ]ˡ test-subtyping : Boolbox <: TestInbox test-subtyping = [ S Z ]ᵐ diff --git a/src/NatProps.agda b/src/NatProps.agda index ab84cbc..dbadc11 100644 --- a/src/NatProps.agda +++ b/src/NatProps.agda @@ -1,9 +1,7 @@ module NatProps where open import Data.Nat using (ℕ ; _≟_ ; _<_ ; zero ; suc ; s≤s) -open import Data.Nat.Properties using (s≤s-injective) open import Relation.Nullary using (Dec ; yes ; no ; ¬_) open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym) -open import Data.Empty using (⊥) <-¬≡ : ∀ {n m} → n < m → ¬ n ≡ m <-¬≡ {zero} {zero} () diff --git a/src/Prelude.agda b/src/Prelude.agda new file mode 100644 index 0000000..9c6a523 --- /dev/null +++ b/src/Prelude.agda @@ -0,0 +1,69 @@ +module Prelude where + +-- Simple data +open import Data.Bool public + using (Bool ; false ; true) +open import Data.Empty public + using (⊥ ; ⊥-elim) +open import Data.Nat public + using ( + ℕ ; zero ; suc + ; _+_ ; _*_ + ; _≤_ ; z≤n ; s≤s + ; _<_ ; _≟_ ; pred + ) +open import Data.Maybe public + using (Maybe ; just ; nothing) +open import Data.Unit public + using (⊤ ; tt) +open import Data.String public + using (String) + renaming (_++_ to _||_) + +-- List-like modules + +open import Data.List public + using ( + List ; [] ; _∷_ + ; _++_ ; map ; drop + ; reverse ; _∷ʳ_ ; length + ) +open import Data.List.All public + using (All ; [] ; _∷_ ; lookup) + renaming (map to ∀map) +open import Membership public + using ( + _∈_ ; S ; Z + ; _⊆_ ; _∷_ ; [] + ; ⊆-refl ; ⊆-suc ; find-∈ + ; lookup-parallel ; lookup-parallel-≡ ; translate-∈ + ; translate-⊆ ; ⊆-trans ; All-⊆ + ; ⊆++-l-refl ; lookup-all + ; ∈-inc ; ⊆++-refl ; ⊆++comm' + ; ⊆++comm ; ⊆-move ; ⊆-inc + ; ⊆-skip + ) +open import Data.List.Any public + using (Any ; here ; there) + +open import Singleton public + using ([_]ˡ ; [_]ᵃ ; [_]ᵐ) + +-- Propositions and properties +open import Relation.Binary.PropositionalEquality public + using ( + _≡_ ; refl ; sym + ; cong ; cong₂ ; trans + ; inspect ; [_] + ) +open import Relation.Nullary public + using (Dec ; yes ; no ; ¬_) +open import Relation.Nullary.Decidable public + using (⌊_⌋) + +-- Other +open import Level public + using (Level; _⊔_ ; Lift ; lift) + renaming (zero to lzero; suc to lsuc) +open import Size public + using (Size ; Size<_ ; ↑_ ; ∞) diff --git a/src/Runtime.agda b/src/Runtime.agda index 01762f5..3fc71c5 100644 --- a/src/Runtime.agda +++ b/src/Runtime.agda @@ -1,16 +1,10 @@ module Runtime where open import Simulate open import SimulationEnvironment +open import Prelude -open import Data.List using (List ; _∷_ ; [] ; map ; length) -open import Data.List.All using (All ; _∷_ ; []) -open import Data.Nat using (ℕ ; zero ; suc) open import Data.Nat.Show using (show) -open import Data.String using (String ; _++_) -open import Data.Unit using (⊤ ; tt) - open import Coinduction using ( ♯_ ; ♭) -open import Size using (∞) import IO open ∞Trace @@ -36,10 +30,10 @@ show-env : Env → String show-env env = let count = count-blocked env open BlockedCount - in "There are " ++ show (count .return-count) ++ " finished actors and " ++ show (count .receive-count) ++ " blocked actors" + in "There are " || show (count .return-count) || " finished actors and " || show (count .receive-count) || " blocked actors" show-final-step : ℕ → String -show-final-step n = "Done after " ++ (show n) ++ " steps." +show-final-step n = "Done after " || (show n) || " steps." -- run-env continously runs the simulation of an environment -- and transforms the steps taken into output to the console. @@ -48,7 +42,7 @@ run-env env = loop 1 ((simulate env) .force) where loop : ℕ → Trace ∞ → IO.IO ⊤ loop n (TraceStop env _) = ♯ IO.putStrLn (show-final-step n) IO.>> ♯ IO.putStrLn (show-env env) - loop n (x ∷ xs) = ♯ IO.putStrLn ("Step " ++ show n ) IO.>> ♯ loop (suc n) (xs .force) + loop n (x ∷ xs) = ♯ IO.putStrLn ("Step " || show n ) IO.>> ♯ loop (suc n) (xs .force) run-env-silent : Env → IO.IO ⊤ run-env-silent env = loop 1 ((simulate env) .force) diff --git a/src/Selective/ActorMonad.lagda.tex b/src/Selective/ActorMonad.lagda.tex index 35312b0..550456a 100644 --- a/src/Selective/ActorMonad.lagda.tex +++ b/src/Selective/ActorMonad.lagda.tex @@ -1,15 +1,6 @@ \begin{code} module Selective.ActorMonad where -open import Membership using (_∈_ ; _⊆_ ; ⊆-refl ; Z ; S ; find-∈) - -open import Data.List using (List ; [] ; _∷_ ; _++_) -open import Data.List.All using (All ; [] ; _∷_) -open import Data.Unit using (⊤ ; tt) -open import Data.Bool using (Bool ; true ; false) -open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; cong ; cong₂ ; trans) - -open import Level using (Lift ; lift ; suc ; zero) -open import Size using (Size ; Size<_ ; ↑_) +open import Prelude mutual data MessageField : Set₁ where @@ -159,7 +150,7 @@ open ∞ActorM public -- coinduction helper for Value -return₁ : {A : Set (suc zero)} → ∀ {i IS post} → (val : A) → ∞ActorM i IS A (post val) post +return₁ : {A : Set (lsuc lzero)} → ∀ {i IS post} → (val : A) → ∞ActorM i IS A (post val) post return₁ val .force = Return val -- universe lifting for return₁ @@ -240,5 +231,5 @@ ⊠-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} diff --git a/src/Selective/ActorMonadNoText.lagda.tex b/src/Selective/ActorMonadNoText.lagda.tex index 399067a..05a685d 100644 --- a/src/Selective/ActorMonadNoText.lagda.tex +++ b/src/Selective/ActorMonadNoText.lagda.tex @@ -1,15 +1,6 @@ \begin{code} module Selective.ActorMonadNoText where -open import Membership using (_∈_ ; _⊆_ ; ⊆-refl ; Z ; S ; find-∈) - -open import Data.List using (List ; [] ; _∷_ ; _++_) -open import Data.List.All using (All ; [] ; _∷_) -open import Data.Unit using (⊤ ; tt) -open import Data.Bool using (Bool ; true ; false) -open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; cong ; cong₂ ; trans) - -open import Level using (Lift ; lift ; suc ; zero) -open import Size using (Size ; Size<_ ; ↑_) +open import Prelude mutual data MessageField : Set₁ where @@ -137,7 +128,7 @@ open ∞ActorM public -- coinduction helper for Value -return₁ : {A : Set (suc zero)} → ∀ {i IS post} → (val : A) → ∞ActorM i IS A (post val) post +return₁ : {A : Set (lsuc lzero)} → ∀ {i IS post} → (val : A) → ∞ActorM i IS A (post val) post return₁ val .force = Return val -- universe lifting for return₁ @@ -204,5 +195,5 @@ ⊠-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} diff --git a/src/Selective/EnvironmentOperations.agda b/src/Selective/EnvironmentOperations.agda index f99d3a7..bfb6c34 100644 --- a/src/Selective/EnvironmentOperations.agda +++ b/src/Selective/EnvironmentOperations.agda @@ -1,25 +1,13 @@ module Selective.EnvironmentOperations where open import Selective.ActorMonad open import Selective.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 Data.Bool using (Bool ; true ; false) -open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; cong ; cong₂ ; trans ; inspect ; [_]) -open import Relation.Nullary using (Dec ; yes ; no ; ¬_) - -open import Level using (Lift ; lift) -open import Size using (∞) open Actor open ValidActor @@ -248,11 +236,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 @@ -573,7 +561,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. diff --git a/src/Selective/Examples/ActiveObjects.agda b/src/Selective/Examples/ActiveObjects.agda index 5c0d84c..d32e211 100644 --- a/src/Selective/Examples/ActiveObjects.agda +++ b/src/Selective/Examples/ActiveObjects.agda @@ -1,19 +1,10 @@ module Selective.Examples.ActiveObjects where -open import Selective.ActorMonad public -open import Selective.Examples.Channel public -open import Selective.Examples.Call2 public -open import Membership using ( - _∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] - ; ⊆-refl ; ⊆-trans ; ⊆-suc ; translate-⊆ - ; lookup-all ; ⊆++-l-refl - ) -open import Data.List using (List ; _∷_ ; [] ; _++_ ; map) -open import Data.List.All using (All ; _∷_ ; []) renaming (map to ∀map) -open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; _≟_ ) +open import Selective.ActorMonad +open import Selective.Examples.Channel +open import Selective.Examples.Call2 +open import Prelude open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax) -open import Level using (Lift ; lift) renaming (zero to lzero ; suc to lsuc) -open import Size open ChannelType open ChannelInitiation @@ -119,7 +110,7 @@ invoke-active-method ac (Msg x f) state = invoke f (ac .methods) (ac .handlers) MT ∈ active-request-type ci translate-invoke-pointer {record { request-tagged = HasTag+Ref MT ∷ _ }} Z = Z translate-invoke-pointer {record { response = response ; request-tagged = _ ∷ rt }} (S p) = - let rec = translate-invoke-pointer {record { request = _ ; response = response ; request-tagged = rt }} p + let rec = translate-invoke-pointer {record { request = _ ; response = response ; request-tagged = rt }} p in S rec translate-send-pointer : ∀ {ct MT} → MT ∈ active-reply-type ct → @@ -147,11 +138,11 @@ invoke-active-method ac (Msg x f) state = invoke f (ac .methods) (ac .handlers) (cis : List ChannelInitiation) → All (active-method (active-inbox-shape (ac .methods)) (ac .state-type) (ac .vars)) cis → MT ∈ active-inbox-shape cis → - ∞ActorM i (active-inbox-shape (ac .methods)) (ac .state-type) (add-references-static (ac .vars state) MT) (λ st → add-references-static (ac .vars st) MT) + ∞ActorM i (active-inbox-shape (ac .methods)) (ac .state-type) (add-references-static (ac .vars state) MT) (λ st → add-references-static (ac .vars st) MT) invoke _ _ [] () invoke f (ci ∷ _) (_ ∷ _) x with (∈++ (ci .request) _ x) invoke f (ci ∷ _) (handler ∷ _) x | Left q = - let irm = lookup-all q (ci .request-tagged) + let irm = lookup-all q (ci .request-tagged) in invoke' f ci handler q irm invoke f (_ ∷ cis) (_ ∷ handlers) x | Right q = invoke f cis handlers q diff --git a/src/Selective/Examples/Bookstore.agda b/src/Selective/Examples/Bookstore.agda index 6c7b49c..842f543 100644 --- a/src/Selective/Examples/Bookstore.agda +++ b/src/Selective/Examples/Bookstore.agda @@ -1,29 +1,19 @@ module Selective.Examples.Bookstore where -open import Selective.ActorMonad public +open import Selective.ActorMonad open import Selective.Examples.Call using (UniqueTag ; call) -open import Data.List using (List ; _∷_ ; [] ; map ; _++_ ; reverse ; _∷ʳ_ ; length) -open import Data.List.All using (All ; _∷_ ; []) -open import Data.Bool using (Bool ; false ; true) -open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; _≟_ ; pred ; ⌈_/2⌉ ; _≤?_ ; _∸_ ; _≤_ ; z≤n ; s≤s ; _<_ ; _≰_ ) -open import Data.Nat.Properties using (≤-antisym ; ≰⇒>) -open import Data.Maybe as Maybe using (Maybe ; just ; nothing) -open import Data.String using (String ; primStringEquality) renaming (_++_ to _||_) -open import Size -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) -open import Relation.Nullary using (yes ; no) -open import Relation.Nullary.Decidable using (⌊_⌋) -open import Membership using (_∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] ; ⊆-refl ; ⊆-suc ; ⊆++-refl ; translate-⊆) -open import Data.Unit using (⊤ ; tt) - -open import Data.List.Properties - -open import Category.Monad +open import Prelude + +open import Data.Nat + using ( _≟_ ; pred ; ⌈_/2⌉ ; _≤?_ ; _∸_ ; _≤_ ; z≤n ; s≤s ; _<_ ; _≰_ ) +open import Data.Nat.Properties + using (≤-antisym ; ≰⇒>) +open import Data.Nat.Show + using (show) +open import Data.String + using (primStringEquality) open import Debug -open import Data.Nat.Show using (show) BookTitle = String Money = ℕ @@ -41,13 +31,13 @@ record Book : Set where -- =========== GetQuoteReply : MessageType -GetQuoteReply = ValueType UniqueTag ∷ ValueType (Maybe Book) ∷ [] +GetQuoteReply = ValueType UniqueTag ∷ [ ValueType (Maybe Book) ]ˡ GetQuoteReplyInterface : InboxShape -GetQuoteReplyInterface = GetQuoteReply ∷ [] +GetQuoteReplyInterface = [ GetQuoteReply ]ˡ GetQuote : MessageType -GetQuote = ValueType UniqueTag ∷ ReferenceType GetQuoteReplyInterface ∷ ValueType BookTitle ∷ [] +GetQuote = ValueType UniqueTag ∷ ReferenceType GetQuoteReplyInterface ∷ [ ValueType BookTitle ]ˡ -- ====================== -- PROPOSE CONTRIBUTION @@ -59,7 +49,7 @@ record Contribution : Set where money : Money ContributionMessage : MessageType -ContributionMessage = ValueType Contribution ∷ [] +ContributionMessage = [ ValueType Contribution ]ˡ -- =============== -- AGREE OR QUIT @@ -69,39 +59,39 @@ data AgreeChoice : Set where AGREE QUIT : AgreeChoice AgreeDecision : MessageType -AgreeDecision = ValueType AgreeChoice ∷ [] +AgreeDecision = [ ValueType AgreeChoice ]ˡ -- ================ -- TRANSFER MONEY -- ================ Transfer : MessageType -Transfer = ValueType BuyerRole ∷ ValueType Contribution ∷ [] +Transfer = ValueType BuyerRole ∷ [ ValueType Contribution ]ˡ -- ============ -- INTERFACES -- ============ Buyer1-to-Seller : InboxShape -Buyer1-to-Seller = GetQuote ∷ Transfer ∷ [] +Buyer1-to-Seller = GetQuote ∷ [ Transfer ]ˡ Buyer2-to-Seller : InboxShape -Buyer2-to-Seller = AgreeDecision ∷ Transfer ∷ [] +Buyer2-to-Seller = AgreeDecision ∷ [ Transfer ]ˡ Buyer1-to-Buyer2 : InboxShape -Buyer1-to-Buyer2 = ContributionMessage ∷ [] +Buyer1-to-Buyer2 = [ ContributionMessage ]ˡ Buyer2-to-Buyer1 : InboxShape -Buyer2-to-Buyer1 = AgreeDecision ∷ [] +Buyer2-to-Buyer1 = [ AgreeDecision ]ˡ SellerInterface : InboxShape -SellerInterface = GetQuote ∷ AgreeDecision ∷ Transfer ∷ [] +SellerInterface = GetQuote ∷ AgreeDecision ∷ [ Transfer ]ˡ Buyer1Interface : InboxShape -Buyer1Interface = (ReferenceType Buyer1-to-Seller ∷ []) ∷ (ReferenceType Buyer1-to-Buyer2 ∷ []) ∷ GetQuoteReply ∷ AgreeDecision ∷ [] +Buyer1Interface = [ ReferenceType Buyer1-to-Seller ]ˡ ∷ [ ReferenceType Buyer1-to-Buyer2 ]ˡ ∷ GetQuoteReply ∷ [ AgreeDecision ]ˡ Buyer2Interface : InboxShape -Buyer2Interface = (ReferenceType Buyer2-to-Seller ∷ []) ∷ (ReferenceType Buyer2-to-Buyer1 ∷ []) ∷ ContributionMessage ∷ [] +Buyer2Interface = [ ReferenceType Buyer2-to-Seller ]ˡ ∷ [ ReferenceType Buyer2-to-Buyer1 ]ˡ ∷ [ ContributionMessage ]ˡ -- ======== -- COMMON @@ -112,12 +102,13 @@ book1 = "Crime and Punishment" transfer-money : ∀ {i IS Seller Γ} → Γ ⊢ Seller → - (Transfer ∷ []) <: Seller → + [ Transfer ]ˡ <: Seller → BuyerRole → Book → Money → ∞ActorM i IS ⊤₁ Γ (λ _ → Γ) -transfer-money p sub role book money = p ![t: translate-⊆ sub Z ] ((lift role) ∷ (lift (record { book = book ; money = money })) ∷ []) +transfer-money p sub role book money = p ![t: translate-⊆ sub Z ] ((lift role) ∷ [ lift record { book = book ; money = money } ]ᵃ) + -- ======== -- SELLER -- ======== @@ -145,14 +136,14 @@ seller = begin do where record { msg = (Msg (S _) _) ; msg-ok = () } let maybe-book = find-book known-books title - (Z ![t: Z ] (lift tag ∷ (lift maybe-book ∷ []))) + (Z ![t: Z ] (lift tag ∷ [ lift maybe-book ]ᵃ)) after-book-quote maybe-book where select-quote : MessageFilter SellerInterface select-quote (Msg Z _) = true select-quote _ = false known-books : List Book - known-books = record { title = book1 ; price = 37 } ∷ [] + known-books = [ record { title = book1 ; price = 37 } ]ˡ find-book : List Book → BookTitle → Maybe Book find-book [] title = nothing find-book (book ∷ books) title with (primStringEquality (Book.title book) title) @@ -189,7 +180,7 @@ seller = begin do ... | TooMuchMoney p = "Received too much money for " || Book.title book || ". $" || show (Book.price book) || " - $" || show (Contribution.money c1) || " - $" || show (Contribution.money c2) || " = -$" || show ((Contribution.money c1 + Contribution.money c2) ∸ Book.price book) after-book-quote : ∀ {i} → Maybe Book → - ∞ActorM i SellerInterface ⊤₁ (GetQuoteReplyInterface ∷ []) (λ _ → []) + ∞ActorM i SellerInterface ⊤₁ [ GetQuoteReplyInterface ]ˡ (λ _ → []) after-book-quote (just book) = do lift AGREE ← wait-for-decision where @@ -243,7 +234,7 @@ buyer1 = begin do BookTitle → ∞ActorM i Buyer1Interface (Lift (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) + record { msg = Msg (S (S Z)) (_ ∷ book ∷ []) ; msg-ok = msg-ok } ← call p Z tag [ lift title ]ᵃ [ S (S Z) ]ᵐ Z where record { msg = (Msg Z (_ ∷ _)) ; msg-ok = () } record { msg = (Msg (S Z) (_ ∷ _)) ; msg-ok = () } @@ -255,7 +246,7 @@ buyer1 = begin do Book → Money → ∞ActorM i Buyer1Interface ⊤₁ Γ (λ _ → Γ) - send-contribution p book money = p ![t: Z ] ((lift (record { book = book ; money = money })) ∷ []) + send-contribution p book money = p ![t: Z ] [ lift record { book = book ; money = money } ]ᵃ select-decision : MessageFilter Buyer1Interface select-decision (Msg (S (S (S Z))) _) = true select-decision _ = false @@ -322,12 +313,12 @@ buyer2 = begin do ∞ActorM i Buyer2Interface ⊤₁ Γ (λ _ → Γ) handle-contribution seller buyer1 record { book = book ; money = money } with (contribution-is-fair (Book.price book) money) ... | true = do - (buyer1 ![t: Z ] ((lift AGREE) ∷ [])) - (seller ![t: Z ] ((lift AGREE) ∷ [])) - (transfer-money seller (⊆-suc ⊆-refl) Buyer2 book ((Book.price book) ∸ money)) + buyer1 ![t: Z ] [ lift AGREE ]ᵃ + seller ![t: Z ] [ lift AGREE ]ᵃ + transfer-money seller (⊆-suc ⊆-refl) Buyer2 book ((Book.price book) ∸ money) ... | false = do - (buyer1 ![t: Z ] ((lift QUIT) ∷ [])) - (seller ![t: Z ] ((lift QUIT) ∷ [])) + buyer1 ![t: Z ] [ lift QUIT ]ᵃ + seller ![t: Z ] [ lift QUIT ]ᵃ -- ============ -- SUPERVISOR @@ -338,9 +329,9 @@ bookstore-supervisor = do spawn seller spawn buyer1 spawn buyer2 - Z ![t: Z ] (([ (S (S Z)) ]>: ((S Z) ∷ ((S (S Z)) ∷ []))) ∷ []) - Z ![t: S Z ] (([ (S Z) ]>: ((S (S (S Z))) ∷ [])) ∷ []) - (S Z) ![t: Z ] (([ (S (S Z)) ]>: (Z ∷ (S (S Z) ∷ []))) ∷ []) - (S Z) ![t: S Z ] (([ Z ]>: ((S (S Z)) ∷ [])) ∷ []) + Z ![t: Z ] [ [ (S (S Z)) ]>: ( S Z ∷ [ S (S Z) ]ᵐ)]ᵃ + Z ![t: S Z ] [ [ S Z ]>: [ S (S (S Z)) ]ᵐ ]ᵃ + (S Z) ![t: Z ] [ [ S (S Z) ]>: (Z ∷ [ S (S Z) ]ᵐ) ]ᵃ + (S Z) ![t: S Z ] [ [ Z ]>: [ S (S Z) ]ᵐ ]ᵃ (strengthen []) diff --git a/src/Selective/Examples/Call.lagda.tex b/src/Selective/Examples/Call.lagda.tex index b92c039..e79368f 100644 --- a/src/Selective/Examples/Call.lagda.tex +++ b/src/Selective/Examples/Call.lagda.tex @@ -1,23 +1,8 @@ \begin{code} module Selective.Examples.Call where -open import Selective.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 Size -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-⊆ - ) -open import Data.Unit using (⊤ ; tt) -open import Relation.Nullary using (yes ; no) -open import Relation.Nullary.Decidable using (⌊_⌋) +open import Selective.ActorMonad +open import Prelude open SelectedMessage @@ -109,39 +94,39 @@ translate-fields {ReferenceType x ∷ MT} (([ p ]>: v) ∷ vals) = ([ (S p) ]>: v) ∷ (translate-fields vals) +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 .force = receive ∞>>= λ { (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) .force → - (Z ![t: Z ] ((lift tag) ∷ (lift (n + m)) ∷ [])) ∞>> (do + (Z ![t: Z ] (lift tag ∷ [ lift (n + m) ]ᵃ)) ∞>> (do strengthen [] calculatorActor) ; (Msg (S ()) _) } TestBox : InboxShape -TestBox = ( - ValueType UniqueTag ∷ - ValueType ℕ ∷ []) ∷ - [] ∷ [] +TestBox = AddReply calltestActor : ∀{i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → []) -calltestActor .force = spawn∞ calculatorActor ∞>> (do - x ← call Z Z 0 ((lift 10) ∷ ((lift 32) ∷ [])) (Z ∷ []) Z - 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 : SelectedMessage {TestBox} (call-select 0 (Z ∷ []) Z) → + return-result : SelectedMessage {TestBox} (call-select 0 [ Z ]ᵐ 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/Selective/Examples/Call2.agda b/src/Selective/Examples/Call2.agda index 254c0c2..7d809e8 100644 --- a/src/Selective/Examples/Call2.agda +++ b/src/Selective/Examples/Call2.agda @@ -1,24 +1,8 @@ module Selective.Examples.Call2 where -open import Selective.ActorMonad public -open import Selective.Examples.Channel public -open import Data.List using (List ; _∷_ ; [] ; _++_ ; map) -open import Data.List.All using (All ; _∷_ ; []) renaming (map to ∀map) -open import Data.Bool using (Bool ; if_then_else_ ; false ; true) -open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; _≟_ ) -open import Size -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-⊆ - ; lookup-all - ) -open import Data.Unit using (⊤ ; tt) -open import Relation.Nullary using (yes ; no) -open import Relation.Nullary.Decidable using (⌊_⌋) +open import Selective.ActorMonad +open import Selective.Examples.Channel +open import Prelude open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax) open ChannelType @@ -38,43 +22,39 @@ call protocol request = let rs = request .session .response-session from-channel (protocol .response) rs -CalculatorResponse : InboxShape -CalculatorResponse = ( - ValueType UniqueTag ∷ - ValueType ℕ ∷ []) ∷ [] +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 CalculatorResponse ∷ - ValueType ℕ ∷ - ValueType ℕ ∷ [] - ) ∷ [] +Calculator = [ AddMessage ]ˡ CalculatorProtocol : ChannelInitiation CalculatorProtocol = record { request = Calculator ; response = record { - channel-shape = CalculatorResponse + channel-shape = AddReply ; all-tagged = (HasTag _) ∷ [] } - ; request-tagged = (HasTag+Ref (ValueType ℕ ∷ ValueType ℕ ∷ [])) ∷ [] + ; request-tagged = [ HasTag+Ref _ ]ᵃ } calculatorActor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift ⊤) [] (λ _ → []) calculatorActor .force = receive ∞>>= λ { (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) .force → - (Z ![t: Z ] ((lift tag) ∷ (lift (n + m)) ∷ [])) ∞>> (do + Z ![t: Z ] (lift tag ∷ [ lift (n + m) ]ᵃ) ∞>> (do strengthen [] calculatorActor) ; (Msg (S ()) _) } TestBox : InboxShape -TestBox = ( - ValueType UniqueTag ∷ - ValueType ℕ ∷ []) ∷ - [] ∷ [] +TestBox = AddReply calltestActor : ∀{i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → []) calltestActor = do @@ -82,11 +62,11 @@ calltestActor = do Msg Z (tag ∷ n ∷ []) ← call CalculatorProtocol (record { var = Z ; chosen-field = Z - ; fields = (lift 32) ∷ ((lift 10) ∷ []) + ; fields = (lift 32) ∷ [ lift 10 ]ᵃ ; session = record { can-request = ⊆-refl ; response-session = record { - can-receive = Z ∷ [] + can-receive = [ Z ]ᵐ ; tag = 0 } } diff --git a/src/Selective/Examples/CallNoComments.lagda.tex b/src/Selective/Examples/CallNoComments.lagda.tex index e7c92cc..dc9ead3 100644 --- a/src/Selective/Examples/CallNoComments.lagda.tex +++ b/src/Selective/Examples/CallNoComments.lagda.tex @@ -1,36 +1,20 @@ \begin{code} -module Selective.Examples.CallNoComments where +module Selective.Examples.Call where -open import Selective.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 Size -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-⊆ - ) -open import Data.Unit using (⊤ ; tt) -open import Relation.Nullary using (yes ; no) +open import Selective.ActorMonad +open import Prelude open SelectedMessage UniqueTag = ℕ call-select-unwrap : ∀ {MtIn MT} {IS : InboxShape} → - UniqueTag → - MT ∈ IS → - All receive-field-content MT → - (ValueType UniqueTag ∷ MtIn) ∈ IS → - Bool -call-select-unwrap tag Z (tag' ∷ fs) Z with (tag ≟ tag') -... | yes p = true -... | no p = false + UniqueTag → + MT ∈ IS → + All receive-field-content MT → + (ValueType UniqueTag ∷ MtIn) ∈ IS → + Bool +call-select-unwrap tag Z (tag' ∷ fs) Z = ⌊ tag ≟ tag' ⌋ call-select-unwrap _ Z _ (S p) = false call-select-unwrap _ (S x) _ Z = false call-select-unwrap tag (S x) fs (S p) = call-select-unwrap tag x fs p @@ -44,66 +28,66 @@ call-select-unwrap tag x fs (translate-⊆ sub which) call : {Γ : TypingContext} {i : Size} - {MtTo MtIn : MessageType} - {To IS IS' : InboxShape} → - (Γ ⊢ To) → - ((ValueType UniqueTag ∷ ReferenceType IS' ∷ MtTo) ∈ To) → - (tag : UniqueTag) → - All (send-field-content Γ) MtTo → - (ISsubs : IS' <: IS) → - (whichIn : (ValueType UniqueTag ∷ MtIn) ∈ IS') → - ∞ActorM i IS - (SelectedMessage (call-select tag ISsubs whichIn)) - Γ (add-selected-references Γ) + {MtTo MtIn : MessageType} + {To IS IS' : InboxShape} → + (Γ ⊢ To) → + ((ValueType UniqueTag ∷ ReferenceType IS' ∷ MtTo) ∈ To) → + (tag : UniqueTag) → + All (send-field-content Γ) MtTo → + (ISsubs : IS' <: IS) → + (whichIn : (ValueType UniqueTag ∷ MtIn) ∈ IS') → + ∞ActorM i IS + (SelectedMessage (call-select tag ISsubs whichIn)) + Γ (add-selected-references Γ) call {Γ} {IS = IS} var toFi tag vals sub whichIn = do - self - S var ![t: toFi ] ((lift tag) ∷ ([ Z ]>: sub) ∷ (translate-fields vals)) - strengthen (⊆-suc ⊆-refl) - selective-receive (call-select tag sub whichIn) + self + S var ![t: toFi ] ((lift tag) ∷ ([ Z ]>: sub) ∷ (translate-fields vals)) + strengthen (⊆-suc ⊆-refl) + selective-receive (call-select tag sub whichIn) where translate-fields : ∀ {MT} → - All (send-field-content Γ) MT → - All (send-field-content (IS ∷ Γ)) MT + All (send-field-content Γ) MT → + All (send-field-content (IS ∷ Γ)) MT translate-fields [] = [] translate-fields {ValueType x ∷ MT} (px ∷ vals) = px ∷ (translate-fields vals) translate-fields {ReferenceType x ∷ MT} (([ p ]>: v) ∷ vals) = ([ (S p) ]>: v) ∷ (translate-fields vals) +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 .force = receive ∞>>= λ { (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) .force → - (Z ![t: Z ] ((lift tag) ∷ (lift (n + m)) ∷ [])) ∞>> (do + (Z ![t: Z ] (lift tag ∷ [ lift (n + m) ]ᵃ)) ∞>> (do strengthen [] calculatorActor) ; (Msg (S ()) _) } TestBox : InboxShape -TestBox = ( - ValueType UniqueTag ∷ - ValueType ℕ ∷ []) ∷ - [] ∷ [] +TestBox = AddReply calltestActor : ∀{i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → []) -calltestActor .force = spawn∞ calculatorActor ∞>> (do - x ← call Z Z 0 ((lift 10) ∷ ((lift 32) ∷ [])) (Z ∷ []) Z - 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 : SelectedMessage {TestBox} (call-select 0 (Z ∷ []) Z) → + return-result : SelectedMessage {TestBox} (call-select 0 [ Z ]ᵐ 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/Selective/Examples/Channel.agda b/src/Selective/Examples/Channel.agda index a3010ad..9762457 100644 --- a/src/Selective/Examples/Channel.agda +++ b/src/Selective/Examples/Channel.agda @@ -1,23 +1,7 @@ module Selective.Examples.Channel where -open import Selective.ActorMonad public -open import Data.List using (List ; _∷_ ; [] ; _++_ ; map) -open import Data.List.All using (All ; _∷_ ; []) renaming (map to ∀map) -open import Data.Bool using (Bool ; if_then_else_ ; false ; true) -open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; _≟_ ) -open import Size -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-⊆ - ; lookup-all - ) -open import Data.Unit using (⊤ ; tt) -open import Relation.Nullary using (yes ; no) -open import Relation.Nullary.Decidable using (⌊_⌋) +open import Selective.ActorMonad +open import Prelude open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax) UniqueTag = ℕ diff --git a/src/Selective/Examples/Chat.agda b/src/Selective/Examples/Chat.agda index b428a13..c5ce5c9 100644 --- a/src/Selective/Examples/Chat.agda +++ b/src/Selective/Examples/Chat.agda @@ -1,24 +1,13 @@ module Selective.Examples.Chat where -open import Selective.ActorMonad public +open import Selective.ActorMonad open import Selective.Examples.Call using (UniqueTag ; call) -open import Data.List using (List ; _∷_ ; [] ; map ; _++_ ; reverse ; _∷ʳ_ ; length) -open import Data.List.All using (All ; _∷_ ; []) -open import Data.Bool using (Bool ; false ; true) -open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; _≟_ ; pred) -open import Data.Maybe as Maybe using (Maybe ; just ; nothing) -open import Data.String using (String) renaming (_++_ to _||_) -open import Size -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) -open import Relation.Nullary using (yes ; no) -open import Relation.Nullary.Decidable using (⌊_⌋) -open import Membership using (_∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] ; ⊆-refl ; ⊆-suc ; ⊆++-refl) -open import Data.Unit using (⊤ ; tt) +open import Prelude + hiding (Maybe) +open import Data.Maybe as Maybe + hiding (map) open import Data.List.Properties - open import Category.Monad open import Debug @@ -45,16 +34,16 @@ data JoinRoomStatus : Set where JRS-SUCCESS JRS-FAIL : RoomName → JoinRoomStatus JoinRoomSuccessReply : MessageType -JoinRoomSuccessReply = ValueType UniqueTag ∷ ValueType JoinRoomSuccess ∷ ReferenceType Client-to-Room ∷ [] +JoinRoomSuccessReply = ValueType UniqueTag ∷ ValueType JoinRoomSuccess ∷ [ ReferenceType Client-to-Room ]ˡ JoinRoomFailReply : MessageType -JoinRoomFailReply = ValueType UniqueTag ∷ ValueType JoinRoomFail ∷ [] +JoinRoomFailReply = ValueType UniqueTag ∷ [ ValueType JoinRoomFail ]ˡ JoinRoomReplyInterface : InboxShape -JoinRoomReplyInterface = (JoinRoomSuccessReply ∷ JoinRoomFailReply ∷ []) ++ Room-to-Client +JoinRoomReplyInterface = JoinRoomSuccessReply ∷ JoinRoomFailReply ∷ Room-to-Client JoinRoom : MessageType -JoinRoom = ValueType UniqueTag ∷ ReferenceType JoinRoomReplyInterface ∷ ValueType RoomName ∷ ValueType ClientName ∷ [] +JoinRoom = ValueType UniqueTag ∷ ReferenceType JoinRoomReplyInterface ∷ ValueType RoomName ∷ [ ValueType ClientName ]ˡ -- ============= -- CREATE ROOM @@ -64,10 +53,10 @@ data CreateRoomResult : Set where CR-SUCCESS CR-EXISTS : RoomName → CreateRoomResult CreateRoomReply : MessageType -CreateRoomReply = ValueType UniqueTag ∷ ValueType CreateRoomResult ∷ [] +CreateRoomReply = ValueType UniqueTag ∷ [ ValueType CreateRoomResult ]ˡ CreateRoom : MessageType -CreateRoom = ValueType UniqueTag ∷ ReferenceType (CreateRoomReply ∷ []) ∷ ValueType RoomName ∷ [] +CreateRoom = ValueType UniqueTag ∷ ReferenceType [ CreateRoomReply ]ˡ ∷ [ ValueType RoomName ]ˡ -- ============ -- LIST ROOMS @@ -77,35 +66,33 @@ RoomList : Set RoomList = List RoomName ListRoomsReply : MessageType -ListRoomsReply = ValueType UniqueTag ∷ ValueType RoomList ∷ [] +ListRoomsReply = ValueType UniqueTag ∷ [ ValueType RoomList ]ˡ ListRooms : MessageType -ListRooms = ValueType UniqueTag ∷ ReferenceType (ListRoomsReply ∷ []) ∷ [] +ListRooms = ValueType UniqueTag ∷ [ ReferenceType [ ListRoomsReply ]ˡ ]ˡ -- === -- -- === Client-to-RoomManager : InboxShape -Client-to-RoomManager = JoinRoom ∷ CreateRoom ∷ ListRooms ∷ [] +Client-to-RoomManager = JoinRoom ∷ CreateRoom ∷ [ ListRooms ]ˡ RoomManagerInterface : InboxShape RoomManagerInterface = Client-to-RoomManager GetRoomManagerReply : MessageType -GetRoomManagerReply = ValueType UniqueTag ∷ ReferenceType RoomManagerInterface ∷ [] +GetRoomManagerReply = ValueType UniqueTag ∷ [ ReferenceType RoomManagerInterface ]ˡ GetRoomManager : MessageType -GetRoomManager = ValueType UniqueTag ∷ ReferenceType (GetRoomManagerReply ∷ []) ∷ [] +GetRoomManager = ValueType UniqueTag ∷ [ ReferenceType [ GetRoomManagerReply ]ˡ ]ˡ RoomSupervisorInterface : InboxShape -RoomSupervisorInterface = GetRoomManager ∷ [] +RoomSupervisorInterface = [ GetRoomManager ]ˡ ClientSupervisorInterface : InboxShape ClientSupervisorInterface = - (ReferenceType RoomSupervisorInterface ∷ []) - ∷ GetRoomManagerReply - ∷ [] + [ ReferenceType RoomSupervisorInterface ]ˡ ∷ [ GetRoomManagerReply ]ˡ -- @@ -119,25 +106,25 @@ record ChatMessageContent : Set where message : String ChatMessage : MessageType -ChatMessage = ValueType ChatMessageContent ∷ [] +ChatMessage = [ ValueType ChatMessageContent ]ˡ LeaveRoom : MessageType -LeaveRoom = ValueType ClientName ∷ [] +LeaveRoom = [ ValueType ClientName ]ˡ -Client-to-Room = ChatMessage ∷ LeaveRoom ∷ [] +Client-to-Room = ChatMessage ∷ [ LeaveRoom ]ˡ -Room-to-Client = ChatMessage ∷ [] +Room-to-Client = [ ChatMessage ]ˡ AddToRoom : MessageType -AddToRoom = ValueType ClientName ∷ ReferenceType Room-to-Client ∷ [] +AddToRoom = ValueType ClientName ∷ [ ReferenceType Room-to-Client ]ˡ RoomManager-to-Room : InboxShape -RoomManager-to-Room = AddToRoom ∷ [] +RoomManager-to-Room = [ AddToRoom ]ˡ RoomInstanceInterface : InboxShape RoomInstanceInterface = Client-to-Room ++ RoomManager-to-Room -ClientInterface = (ReferenceType RoomManagerInterface ∷ []) ∷ CreateRoomReply ∷ ListRoomsReply ∷ JoinRoomReplyInterface +ClientInterface = [ ReferenceType RoomManagerInterface ]ˡ ∷ CreateRoomReply ∷ ListRoomsReply ∷ JoinRoomReplyInterface -- ====== -- ROOM @@ -199,7 +186,7 @@ room-instance = begin (loop (record { clients = [] })) send-loop l (x ∷ r) with (x ≟ name) ... | (yes _) = recurse l r x ... | (no _) = let p = build-pointer l (x ∷ r) Z - in debug ("Sending to " || show x || ": " || message) (p ![t: Z ] (((lift (chat-from name message: message)) ∷ []))) >> recurse l r x + in debug ("Sending to " || show x || ": " || message) (p ![t: Z ] [ lift (chat-from name message: message) ]ᵃ ) >> recurse l r x recurse l r x rewrite ++-temp-fix l r x = send-loop (l ∷ʳ x) r handle-message : ∀ {i} → (rs : RoomState) → (m : Message RoomInstanceInterface) → @@ -273,23 +260,23 @@ room-manager = begin (loop (record { rooms = [] })) (Maybe (Γ ⊢ RoomInstanceInterface)) → ∞ActorM i RoomManagerInterface ⊤₁ Γ (λ _ → Γ) handle-room-join tag room-name client-name cp (just rp) = do - cp ![t: Z ] ((lift tag) ∷ ((lift (JR-SUCCESS room-name)) ∷ (([ rp ]>: (Z ∷ ((S Z) ∷ []))) ∷ []))) - rp ![t: S (S Z) ] (lift client-name ∷ ([ cp ]>: ((S (S Z)) ∷ [])) ∷ []) + cp ![t: Z ] ((lift tag) ∷ (lift (JR-SUCCESS room-name)) ∷ [ [ rp ]>: (Z ∷ [ S Z ]ᵐ) ]ᵃ) + rp ![t: S (S Z) ] ((lift client-name) ∷ [ [ cp ]>: [ S (S Z) ]ᵐ ]ᵃ) handle-room-join tag room-name client-name p nothing = - p ![t: S Z ] (lift tag ∷ (lift (JR-FAIL room-name) ∷ [])) + p ![t: S Z ] (lift tag ∷ [ lift (JR-FAIL room-name) ]ᵃ) handle-create-room : ∀ {i} → (rms : RoomManagerState) → UniqueTag → RoomName → - Maybe (((CreateRoomReply ∷ []) ∷ rms-to-context rms) ⊢ RoomInstanceInterface) → - ∞ActorM i RoomManagerInterface RoomManagerState ((CreateRoomReply ∷ []) ∷ rms-to-context rms) rms-to-context + Maybe (([ CreateRoomReply ]ˡ ∷ rms-to-context rms) ⊢ RoomInstanceInterface) → + ∞ActorM i RoomManagerInterface RoomManagerState ([ CreateRoomReply ]ˡ ∷ rms-to-context rms) rms-to-context handle-create-room rms tag name (just x) = do - (Z ![t: Z ] ((lift tag) ∷ ((lift (CR-EXISTS name)) ∷ []))) - (strengthen (⊆-suc ⊆-refl)) - (return₁ rms) + Z ![t: Z ] ((lift tag) ∷ [ lift (CR-EXISTS name) ]ᵃ) + strengthen (⊆-suc ⊆-refl) + return₁ rms handle-create-room rms tag name nothing = do - (Z ![t: Z ] ((lift tag) ∷ ((lift (CR-SUCCESS name)) ∷ []))) - (strengthen (⊆-suc ⊆-refl)) + Z ![t: Z ] ((lift tag) ∷ [ lift (CR-SUCCESS name) ]ᵃ) + strengthen (⊆-suc ⊆-refl) spawn room-instance let rms' : RoomManagerState @@ -310,7 +297,7 @@ room-manager = begin (loop (record { rooms = [] })) handle-create-room state tag name p -- List rooms handle-message state (Msg (S (S Z)) (tag ∷ _ ∷ [])) = do - (Z ![t: Z ] ((lift tag) ∷ (lift (RoomManagerState.rooms state) ∷ []))) + (Z ![t: Z ] ((lift tag) ∷ [(lift (RoomManagerState.rooms state) )]ᵃ)) (strengthen (⊆-suc ⊆-refl)) (return₁ state) handle-message state (Msg (S (S (S ()))) _) @@ -327,7 +314,7 @@ room-manager = begin (loop (record { rooms = [] })) -- ================= rs-context : TypingContext -rs-context = RoomManagerInterface ∷ [] +rs-context = [ RoomManagerInterface ]ˡ -- room-supervisor spawns the room-manager -- and provides an interface for getting a reference to the current room-manager @@ -341,7 +328,7 @@ room-supervisor = begin do provide-manager-instance .force = begin do (Msg Z (tag ∷ _ ∷ [])) ← receive where (Msg (S ()) _) - (Z ![t: Z ] (lift tag ∷ (([ (S Z) ]>: ⊆-refl) ∷ []))) + Z ![t: Z ] (lift tag ∷ [ [ S Z ]>: ⊆-refl ]ᵃ) (strengthen (⊆-suc ⊆-refl)) provide-manager-instance @@ -353,7 +340,7 @@ busy-wait : ∀ {i IS Γ} → ℕ → ∞ActorM i IS ⊤₁ Γ (λ _ → Γ) busy-wait zero = return _ busy-wait (suc n) = return tt >> busy-wait n -client-get-room-manager : ∀ {i} → ∞ActorM i ClientInterface ⊤₁ [] (λ _ → RoomManagerInterface ∷ []) +client-get-room-manager : ∀ {i} → ∞ActorM i ClientInterface ⊤₁ [] (λ _ → [ RoomManagerInterface ]ˡ) client-get-room-manager = do record { msg = Msg Z _} ← (selective-receive (λ { (Msg Z x₁) → true @@ -370,7 +357,7 @@ client-create-room : ∀ {i } → RoomName → ∞ActorM i ClientInterface (Lift CreateRoomResult) Γ (λ _ → Γ) client-create-room p tag name = do - record { msg = (Msg (S Z) (_ ∷ cr ∷ [])) } ← (call p (S Z) tag ((lift name) ∷ []) ((S Z) ∷ []) Z) + record { msg = (Msg (S Z) (_ ∷ cr ∷ [])) } ← (call p (S Z) tag [ lift name ]ᵃ [ S Z ]ᵐ Z) where record { msg = (Msg Z (_ ∷ _)) ; msg-ok = () } record { msg = (Msg (S (S _)) _) ; msg-ok = () } @@ -390,7 +377,7 @@ client-join-room : ∀ {i Γ} → ∞ActorM i ClientInterface (Lift 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) ∷ []))) + S p ![t: Z ] (lift tag ∷ (([ Z ]>: ⊆-suc (⊆-suc (⊆-suc ⊆-refl))) ∷ (lift room-name) ∷ [ lift client-name ]ᵃ)) (strengthen (⊆-suc ⊆-refl)) m ← (selective-receive (select-join-reply tag)) handle-message m @@ -419,7 +406,7 @@ client-send-message : ∀ {i Γ} → ClientName → String → ∞ActorM i ClientInterface ⊤₁ Γ (λ _ → Γ) -client-send-message p client-name message = p ![t: Z ] ((lift (chat-from client-name message: message)) ∷ []) +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) Γ (λ _ → Γ) @@ -444,7 +431,7 @@ client-leave-room : ∀ {i Γ} → Γ ⊢ Client-to-Room → ClientName → ∞ActorM i ClientInterface ⊤₁ Γ (λ _ → Γ) -client-leave-room p name = p ![t: S Z ] ((lift name) ∷ []) +client-leave-room p name = p ![t: S Z ] [ lift name ]ᵃ debug-chat : {a : Level} {A : Set a} → ClientName → ChatMessageContent → A → A debug-chat client-name content = let open ChatMessageContent @@ -588,21 +575,21 @@ client-supervisor = begin do return _ spawn-clients : ∀ {i} → ∞ActorM i ClientSupervisorInterface ⊤₁ cs-context (λ _ → cs-context) spawn-clients = do - (spawn client1) - Z ![t: Z ] (([ S Z ]>: ⊆-refl) ∷ []) + spawn client1 + Z ![t: Z ] [ [ S Z ]>: ⊆-refl ]ᵃ (strengthen (⊆-suc ⊆-refl)) (spawn client2) - Z ![t: Z ] (([ S Z ]>: ⊆-refl) ∷ []) + Z ![t: Z ] [ [ S Z ]>: ⊆-refl ]ᵃ (strengthen (⊆-suc ⊆-refl)) (spawn client3) - Z ![t: Z ] (([ S Z ]>: ⊆-refl) ∷ []) + Z ![t: Z ] [ [ S Z ]>: ⊆-refl ]ᵃ (strengthen (⊆-suc ⊆-refl)) -- chat-supervisor is the top-most actor -- it spawns and connects the ClientRegistry to the RoomRegistry chat-supervisor : ∀ {i} → ∞ActorM i [] ⊤₁ [] (λ _ → []) chat-supervisor = do - (spawn room-supervisor) - (spawn client-supervisor) - (Z ![t: Z ] (([ (S Z) ]>: ⊆-refl) ∷ [])) - (strengthen []) + spawn room-supervisor + spawn client-supervisor + Z ![t: Z ] [ [ S Z ]>: ⊆-refl ]ᵃ + strengthen [] diff --git a/src/Selective/Examples/Fibonacci.agda b/src/Selective/Examples/Fibonacci.agda index 65587c7..5dc880b 100644 --- a/src/Selective/Examples/Fibonacci.agda +++ b/src/Selective/Examples/Fibonacci.agda @@ -1,16 +1,7 @@ module Selective.Examples.Fibonacci where -open import Selective.ActorMonad public -open import Data.List using (List ; _∷_ ; []) -open import Data.List.All using (All ; _∷_ ; []) -open import Data.Bool using (Bool ; false ; true) -open import Data.Nat using (ℕ ; zero ; suc ; _+_) -open import Size -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 Membership using (_∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] ; ⊆-refl ; ⊆-suc) -open import Data.Unit using (⊤ ; tt) +open import Selective.ActorMonad +open import Prelude open import Debug open import Data.Nat.Show using (show) @@ -19,30 +10,26 @@ data End : Set where END : End ℕ-message : MessageType -ℕ-message = ValueType ℕ ∷ [] +ℕ-message = [ ValueType ℕ ]ˡ End-message : MessageType -End-message = ValueType End ∷ [] +End-message = [ ValueType End ]ˡ Client-to-Server : InboxShape -Client-to-Server = ℕ-message ∷ End-message ∷ [] +Client-to-Server = ℕ-message ∷ [ End-message ]ˡ Server-to-Client : InboxShape -Server-to-Client = ℕ-message ∷ [] +Server-to-Client = [ ℕ-message ]ˡ ServerInterface : InboxShape -ServerInterface = - (ReferenceType Server-to-Client ∷ []) - ∷ Client-to-Server +ServerInterface = [ ReferenceType Server-to-Client ]ˡ ∷ Client-to-Server ClientInterface : InboxShape -ClientInterface = - (ReferenceType Client-to-Server ∷ []) - ∷ Server-to-Client +ClientInterface = [ ReferenceType Client-to-Server ]ˡ ∷ Server-to-Client ServerRefs : TypingContext -ServerRefs = Server-to-Client ∷ [] +ServerRefs = [ Server-to-Client ]ˡ constServerRefs : {A : Set₁} → (A → TypingContext) constServerRefs _ = ServerRefs @@ -75,11 +62,11 @@ server = wait-for-client ∞>> run-fibonacci 1 Next n ← wait-for-value where Done → return _ let next = x + n - (Z ![t: Z ] (lift next ∷ [])) + Z ![t: Z ] [ lift next ]ᵃ (run-fibonacci next) ClientRefs : TypingContext -ClientRefs = Client-to-Server ∷ [] +ClientRefs = [ Client-to-Server ]ˡ constClientRefs : {A : Set₁} → (A → TypingContext) constClientRefs _ = ClientRefs @@ -105,16 +92,16 @@ client = wait-for-server ∞>> run 10 0 record { msg = (Msg (S (S ())) x₁) } return n run : ℕ → ℕ → ∀ {i} → ∞ActorM i ClientInterface ⊤₁ ClientRefs constClientRefs - run zero x = Z ![t: S Z ] ((lift END) ∷ []) + run zero x = Z ![t: S Z ] [ lift END ]ᵃ run (suc todo) x .force = begin do (Z ![t: Z ] ((lift x) ∷ [])) (lift n) ← wait-for-value let next = x + n run (debug (show next) todo) next -spawner : ∀ {i} → ∞ActorM i [] ⊤₁ [] (λ _ → ClientInterface ∷ ServerInterface ∷ []) +spawner : ∀ {i} → ∞ActorM i [] ⊤₁ [] (λ _ → ClientInterface ∷ [ ServerInterface ]ˡ) spawner = do - (spawn server) - (spawn client) - (S Z ![t: Z ] (([ Z ]>: ⊆-suc ⊆-refl) ∷ [])) - (Z ![t: Z ] (([ S Z ]>: ⊆-suc ⊆-refl) ∷ [])) + spawn server + spawn client + S Z ![t: Z ] [ [ Z ]>: ⊆-suc ⊆-refl ]ᵃ + Z ![t: Z ] [ [ S Z ]>: ⊆-suc ⊆-refl ]ᵃ diff --git a/src/Selective/Examples/PingPong.agda b/src/Selective/Examples/PingPong.agda index d133793..39f4393 100644 --- a/src/Selective/Examples/PingPong.agda +++ b/src/Selective/Examples/PingPong.agda @@ -1,16 +1,7 @@ module Selective.Examples.PingPong where open import Selective.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 Size -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 Membership using (_∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] ; ⊆-refl) -open import Data.Unit using (⊤ ; tt) +open import Prelude -- An example including three actors: spawner, pinger, ponger -- @@ -29,19 +20,31 @@ Spawnbox : InboxShape Spawnbox = [] mutual - PingValues = Bool ∷ [] - PongValues = ℕ ∷ [] + PingValues = [ Bool ]ˡ + PongValues = [ ℕ ]ˡ - PingRefs : ReferenceTypes - PingRefs = (⊠-of-values PongValues) ∷ [] - PongRefs : ReferenceTypes - PongRefs = ⊠-of-values PingValues ∷ [] + PingRefs : TypingContext + PingRefs = [ ⊠-of-values PongValues ]ˡ + PongRefs : TypingContext + PongRefs = [ ⊠-of-values PingValues ]ˡ + + PongReferenceMessage : MessageType + PongReferenceMessage = [ ReferenceType (⊠-of-values PongValues) ]ˡ + + BoolMessage : MessageType + BoolMessage = [ ValueType Bool ]ˡ Pingbox : InboxShape - Pingbox = (ValueType Bool ∷ []) ∷ (ReferenceType (⊠-of-values PongValues) ∷ []) ∷ [] + Pingbox = BoolMessage ∷ [ PongReferenceMessage ]ˡ + + PingReferenceMessage : MessageType + PingReferenceMessage = [ ReferenceType (⊠-of-values PingValues) ]ˡ + + NatMessage : MessageType + NatMessage = [ ValueType ℕ ]ˡ Pongbox : InboxShape - Pongbox = (ValueType ℕ ∷ []) ∷ (ReferenceType (⊠-of-values PingValues) ∷ []) ∷ [] + Pongbox = NatMessage ∷ [ PingReferenceMessage ]ˡ constPingrefs : {A : Set₁} → (A → TypingContext) @@ -53,7 +56,7 @@ 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 (Msg Z (b ∷ [])) = return b - pingReceive (Msg (S Z) _) = strengthen (S Z ∷ []) >> loopTillPingValue + pingReceive (Msg (S Z) _) = strengthen [ S Z ]ᵐ >> loopTillPingValue pingReceive (Msg (S (S ())) x₁) loopTillPingValue : ∀ {i} → pingMainActor i (Lift Bool) @@ -75,7 +78,7 @@ pinger .force = waitForPong ∞>> pingMain 0 } pingMain : ∀ {i} → ℕ → pingMainActor i ⊤₁ pingMain n .force = loopTillPingValue ∞>>= λ - { (lift false) → (Z ![t: Z ] (lift n ∷ [])) >> pingMain (suc n) + { (lift false) → (Z ![t: Z ] ([ lift n ]ᵃ)) >> pingMain (suc n) ; (lift true) → return _} constPongrefs : {A : Set₁} → (A → TypingContext) @@ -87,13 +90,13 @@ 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 (Msg Z (n ∷ [])) = return n - pongReceive (Msg (S Z) _) = strengthen (S Z ∷ []) >> loopTillPongValue + pongReceive (Msg (S Z) _) = strengthen [ S Z ]ᵐ >> loopTillPongValue pongReceive (Msg (S (S ())) _) loopTillPongValue : ∀ {i} → pongMainActor i (Lift ℕ) loopTillPongValue .force = receive ∞>>= pongReceive ponger : ∀ {i} → ∞ActorM (↑ i) Pongbox ⊤₁ [] constPongrefs -ponger .force = waitForPing ∞>> ((Z ![t: Z ] ((lift false) ∷ [])) >> pongMain) +ponger .force = waitForPing ∞>> ((Z ![t: Z ] ([ lift false ]ᵃ)) >> pongMain) where waitForPing : ∀ {i} → ∞ActorM i Pongbox ⊤₁ [] constPongrefs waitForPing = selective-receive (λ { @@ -107,12 +110,13 @@ ponger .force = waitForPing ∞>> ((Z ![t: Z ] ((lift false) ∷ [])) >> pongMai } pongMain : ∀ {i} → pongMainActor i ⊤₁ pongMain .force = loopTillPongValue ∞>>= λ { - (lift 10) → Z ![t: Z ] ((lift true) ∷ []) - ; (lift n) → (Z ![t: Z ] ((lift false) ∷ [])) >> pongMain + (lift 10) → Z ![t: Z ] [ lift true ]ᵃ + ; (lift n) → Z ![t: Z ] [ lift false ]ᵃ >> pongMain } -spawner : ∀ {i} → ∞ActorM i Spawnbox ⊤₁ [] (λ _ → Pingbox ∷ Pongbox ∷ []) -spawner = spawn∞ ponger >> - (spawn∞ pinger >> - (Z ![t: S Z ] (([ (S Z) ]>: (Z ∷ [])) ∷ []) >> - (S Z ![t: S Z ] (([ Z ]>: (Z ∷ [])) ∷ [])))) +spawner : ∀ {i} → ∞ActorM i Spawnbox ⊤₁ [] (λ _ → Pingbox ∷ [ Pongbox ]ˡ) +spawner = do + spawn∞ ponger + spawn∞ pinger + Z ![t: S Z ] [ [ S Z ]>: [ Z ]ᵐ ]ᵃ + S Z ![t: S Z ] [ [ Z ]>: [ Z ]ᵐ ]ᵃ diff --git a/src/Selective/Examples/TestAC.agda b/src/Selective/Examples/TestAC.agda index f5fa8e0..8066723 100644 --- a/src/Selective/Examples/TestAC.agda +++ b/src/Selective/Examples/TestAC.agda @@ -1,29 +1,11 @@ module Selective.Examples.TestAC where -open import Selective.ActorMonad public -open import Selective.Examples.Channel public -open import Selective.Examples.Call2 public -open import Selective.Examples.ActiveObjects public +open import Selective.ActorMonad +open import Prelude +open import Selective.Examples.Channel +open import Selective.Examples.Call2 +open import Selective.Examples.ActiveObjects -open import Data.List using (List ; _∷_ ; [] ; _++_ ; map) -open import Data.List.All using (All ; _∷_ ; []) renaming (map to ∀map) -open import Data.Bool using (Bool ; if_then_else_ ; false ; true) -open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; _*_ ; _≟_ ) -open import Size -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-⊆ - ; lookup-all - ) -open import Data.Unit using (⊤ ; tt) -open import Relation.Nullary using (yes ; no) -open import Relation.Nullary.Decidable using (⌊_⌋) -open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax) -open import Level using (Lift ; lift) renaming (zero to lzero ; suc to lsuc) open import Debug open import Data.Nat.Show using (show) @@ -31,7 +13,7 @@ open import Data.Nat.Show using (show) calculator-ci : ChannelInitiation calculator-ci = record { request = Calculator - ; response = record { channel-shape = CalculatorResponse ; all-tagged = (HasTag _) ∷ [] } + ; response = record { channel-shape = AddReply ; all-tagged = (HasTag _) ∷ [] } ; request-tagged = (HasTag+Ref _) ∷ [] } calculator-methods : List ChannelInitiation @@ -40,11 +22,11 @@ calculator-methods = calculator-ci ∷ calculator-ci ∷ [] calculator-inbox = active-inbox-shape calculator-methods add : (active-method calculator-inbox ⊤₁ (λ _ → []) calculator-ci) -add (Msg Z (n ∷ m ∷ [])) v = return₁ (record { new-state = _ ; reply = SendM Z ((lift (n + m)) ∷ []) }) +add (Msg Z (n ∷ m ∷ [])) v = return₁ (record { new-state = _ ; reply = SendM Z [ lift (n + m)]ᵃ }) add (Msg (S ()) _) _ multiply : (active-method calculator-inbox ⊤₁ (λ _ → []) calculator-ci) -multiply (Msg Z (n ∷ m ∷ [])) v = return₁ (record { new-state = _ ; reply = SendM Z ((lift (n * m)) ∷ []) }) +multiply (Msg Z (n ∷ m ∷ [])) v = return₁ (record { new-state = _ ; reply = SendM Z [ lift (n * m)]ᵃ }) multiply (Msg (S ()) _) _ calculator : ActiveObject @@ -63,11 +45,11 @@ calculator-test-actor = do Msg Z (_ ∷ n ∷ []) ← call CalculatorProtocol (record { var = Z ; chosen-field = Z - ; fields = (lift 32) ∷ ((lift 10) ∷ []) + ; fields = lift 32 ∷ [ lift 10 ]ᵃ ; session = record { - can-request = Z ∷ [] + can-request = [ Z ]ᵐ ; response-session = record { - can-receive = Z ∷ [] + can-receive = [ Z ]ᵐ ; tag = 0 } } @@ -77,11 +59,11 @@ calculator-test-actor = do Msg Z (_ ∷ m ∷ []) ← debug (show n) (call CalculatorProtocol (record { var = Z ; chosen-field = Z - ; fields = (lift 32) ∷ ((lift 10) ∷ []) + ; fields = lift 32 ∷ [ lift 10 ]ᵃ ; session = record { - can-request = (S Z) ∷ [] + can-request = [ S Z ]ᵐ ; response-session = record { - can-receive = Z ∷ [] + can-receive = [ Z ]ᵐ ; tag = 1 } } diff --git a/src/Selective/Runtime.agda b/src/Selective/Runtime.agda index 5610808..24861ec 100644 --- a/src/Selective/Runtime.agda +++ b/src/Selective/Runtime.agda @@ -1,16 +1,10 @@ module Selective.Runtime where open import Selective.Simulate open import Selective.SimulationEnvironment +open import Prelude -open import Data.List using (List ; _∷_ ; [] ; map ; length) -open import Data.List.All using (All ; _∷_ ; []) -open import Data.Nat using (ℕ ; zero ; suc) open import Data.Nat.Show using (show) -open import Data.String using (String ; _++_) -open import Data.Unit using (⊤ ; tt) - open import Coinduction using ( ♯_ ; ♭) -open import Size using (∞) import IO open ∞Trace @@ -40,10 +34,10 @@ show-env : Env → String show-env env = let count = count-blocked env open BlockedCount - in "There are " ++ show (count .return-count) ++ " finished actors, " ++ show (count .receive-count) ++ " receiving actors, and " ++ show (count .selective-count) ++ " selecting actors" + in "There are " || show (count .return-count) || " finished actors, " || show (count .receive-count) || " receiving actors, and " || show (count .selective-count) || " selecting actors" show-final-step : ℕ → String -show-final-step n = "Done after " ++ (show n) ++ " steps." +show-final-step n = "Done after " || (show n) || " steps." -- run-env continously runs the simulation of an environment -- and transforms the steps taken into output to the console. @@ -52,7 +46,7 @@ run-env env = loop 1 ((simulate env) .force) where loop : ℕ → Trace ∞ → IO.IO ⊤ loop n (TraceStop env _) = ♯ IO.putStrLn (show-final-step n) IO.>> ♯ IO.putStrLn (show-env env) - loop n (x ∷ xs) = ♯ IO.putStrLn ("Step " ++ show n ) IO.>> ♯ loop (suc n) (xs .force) + loop n (x ∷ xs) = ♯ IO.putStrLn ("Step " || show n ) IO.>> ♯ loop (suc n) (xs .force) run-env-silent : Env → IO.IO ⊤ run-env-silent env = loop 1 ((simulate env) .force) diff --git a/src/Selective/Simulate.agda b/src/Selective/Simulate.agda index a8e95f9..3cf6d18 100644 --- a/src/Selective/Simulate.agda +++ b/src/Selective/Simulate.agda @@ -1,23 +1,13 @@ module Selective.Simulate where -open import Membership using (_∈_ ; _⊆_ ; All-⊆ ; translate-⊆ ; ⊆-refl) open import Selective.ActorMonad public open import Selective.SimulationEnvironment open import Selective.EnvironmentOperations +open import Prelude -open import Data.List using (List ; _∷_ ; [] ; map ; _++_) -open import Data.List.All using (All ; _∷_ ; [] ; lookup) renaming (map to ∀map) open import Data.List.All.Properties using (++⁺) -open import Data.Nat using (ℕ ; zero ; suc ; _≟_ ; _<_ ; s≤s) open import Data.Nat.Properties using (≤-reflexive ; ≤-step) -open import Data.Unit using (⊤ ; tt) open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax) -open import Data.Bool using (Bool ; true ; false) - -open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; cong ; trans ; inspect ; [_]) - -open import Level using (Lift ; lift) renaming (suc to lsuc ; zero to lzero) -open import Size using (∞ ; Size ; Size<_) open Actor open ValidActor diff --git a/src/Selective/SimulationEnvironment.agda b/src/Selective/SimulationEnvironment.agda index f0c257a..de0d406 100644 --- a/src/Selective/SimulationEnvironment.agda +++ b/src/Selective/SimulationEnvironment.agda @@ -1,23 +1,18 @@ module Selective.SimulationEnvironment where -open import Membership using (_∈_ ; find-∈ ; _⊆_) open import Selective.ActorMonad -open import NatProps +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.Product using (Σ ; _,_ ; _×_ ; Σ-syntax) -open import Data.Nat using (ℕ ; _≟_ ; _<_ ; zero ; suc ; s≤s) -open import Data.Nat.Properties using (≤-reflexive ; ≤-step) -open import Data.Unit using (⊤ ; tt) -open import Data.Bool using (Bool ; true ; false) +open import NatProps + using (<-¬≡) +open import Data.Nat.Properties + using (≤-reflexive ; ≤-step) -open import Level using (Level ; Lift ; lift) renaming (suc to lsuc) -open import Size using (Size ; Size<_ ; ↑_ ; ∞) +open import Data.Product + using (Σ ; _,_ ; _×_ ; Σ-syntax) -open import Data.Empty using (⊥) -open import Relation.Nullary using (Dec ; yes ; no ; ¬_) -open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; cong ; cong₂ ; trans ; inspect ; [_]) -open import Relation.Unary using (Decidable) renaming (_⊆_ to _⋐_) +open import Relation.Unary + using (Decidable) + renaming (_⊆_ to _⋐_) -- We give every actor and inbox a name. -- The internal type of an actor is not important, @@ -216,7 +211,7 @@ data InboxesValid (store : Store) : ∀ {store'} → Inboxes store' → Set₁ w -- A name is unused in a store if every inbox has a name that is < than the name NameFresh : Store → ℕ → Set₁ -NameFresh store n = All (λ v → name v Data.Nat.< n) store +NameFresh store n = All (λ v → name v < n) store where open NamedInbox -- If a name is fresh for a store (i.e. all names in the store are < than the name), @@ -243,7 +238,7 @@ record NameSupplyStream (i : Size) (store : Store) : Set₁ where -- if the new name is > than all the names already in the store. suc-helper : ∀ {store name IS n} → name ↦ IS ∈e store → - All (λ v → suc (NamedInbox.name v) Data.Nat.≤ n) store → + All (λ v → suc (NamedInbox.name v) ≤ n) store → ¬ name ≡ n suc-helper zero (px ∷ p) = <-¬≡ px suc-helper (suc q) (px ∷ p) = suc-helper q p @@ -541,7 +536,7 @@ empty-env = record -- The actor can't have any known references singleton-env : ∀ {IS A post} → ActorM ∞ IS A [] post → Env singleton-env {IS} {A} {post} actor = record - { acts = record + { acts = [ record { inbox-shape = IS ; A = A ; references = [] @@ -550,13 +545,13 @@ singleton-env {IS} {A} {post} actor = record ; post = post ; computation = record { act = actor ; cont = [] } ; name = name-supply-singleton .supply .name - } ∷ [] + } ]ˡ ; blocked = [] ; env-inboxes = [] ∷ [] - ; store = inbox# 0 [ IS ] ∷ [] - ; actors-valid = (record { actor-has-inbox = zero ; references-have-pointer = [] }) ∷ [] + ; store = [ inbox# 0 [ IS ] ]ˡ + ; actors-valid = [ record { actor-has-inbox = zero ; references-have-pointer = [] }]ᵃ ; blocked-valid = [] - ; messages-valid = [] ∷ [] + ; messages-valid = [] ∷ [] ; name-supply = name-supply-singleton .next IS ; blocked-no-progress = [] } diff --git a/src/Simulate.agda b/src/Simulate.agda index 8448819..bb1ecd2 100644 --- a/src/Simulate.agda +++ b/src/Simulate.agda @@ -1,22 +1,16 @@ module Simulate where -open import Membership using (_∈_ ; _⊆_ ; All-⊆ ; translate-⊆ ; ⊆-refl) open import ActorMonad public open import SimulationEnvironment open import EnvironmentOperations +open import Prelude -open import Data.List using (List ; _∷_ ; [] ; map ; _++_) -open import Data.List.All using (All ; _∷_ ; [] ; lookup) renaming (map to ∀map) -open import Data.List.All.Properties using (++⁺) -open import Data.Nat using (ℕ ; zero ; suc ; _≟_ ; _<_ ; s≤s) -open import Data.Nat.Properties using (≤-reflexive ; ≤-step) -open import Data.Unit using (⊤ ; tt) -open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax) - -open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; cong ; trans ; inspect ; [_]) - -open import Level using (Lift ; lift) renaming (suc to lsuc ; zero to lzero) -open import Size using (∞ ; Size ; Size<_) +open import Data.List.All.Properties + using (++⁺) +open import Data.Nat.Properties + using (≤-reflexive ; ≤-step) +open import Data.Product + using (Σ ; _,_ ; _×_ ; Σ-syntax) open Actor open ValidActor diff --git a/src/SimulationEnvironment.agda b/src/SimulationEnvironment.agda index b08c11b..4cb8d3a 100644 --- a/src/SimulationEnvironment.agda +++ b/src/SimulationEnvironment.agda @@ -1,22 +1,18 @@ module SimulationEnvironment where -open import Membership using (_∈_ ; find-∈ ; _⊆_) open import ActorMonad -open import NatProps +open import Prelude -open import Data.List using (List ; _∷_ ; [] ; map) -open import Data.List.All using (All ; _∷_ ; [] ; lookup) renaming (map to ∀map) -open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax) -open import Data.Nat using (ℕ ; _≟_ ; _<_ ; zero ; suc ; s≤s) -open import Data.Nat.Properties using (≤-reflexive ; ≤-step) -open import Data.Unit using (⊤ ; tt) +open import NatProps + using (<-¬≡) +open import Data.Nat.Properties + using (≤-reflexive ; ≤-step) -open import Level using (Lift ; lift) -open import Size using (Size ; Size<_ ; ↑_ ; ∞) +open import Data.Product + using (Σ ; _,_ ; _×_ ; Σ-syntax) -open import Data.Empty using (⊥) -open import Relation.Nullary using (Dec ; yes ; no ; ¬_) -open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym) -open import Relation.Unary using (Decidable) renaming (_⊆_ to _⋐_) +open import Relation.Unary + using (Decidable) + renaming (_⊆_ to _⋐_) -- We give every actor and inbox a name. @@ -213,7 +209,7 @@ data InboxesValid (store : Store) : ∀ {store'} → Inboxes store' → Set₁ w -- A name is unused in a store if every inbox has a name that is < than the name NameFresh : Store → ℕ → Set₁ -NameFresh store n = All (λ v → name v Data.Nat.< n) store +NameFresh store n = All (λ v → name v < n) store where open NamedInbox -- If a name is fresh for a store (i.e. all names in the store are < than the name), @@ -240,7 +236,7 @@ record NameSupplyStream (i : Size) (store : Store) : Set₁ where -- if the new name is > than all the names already in the store. suc-helper : ∀ {store name IS n} → name ↦ IS ∈e store → - All (λ v → suc (NamedInbox.name v) Data.Nat.≤ n) store → + All (λ v → suc (NamedInbox.name v) ≤ n) store → ¬ name ≡ n suc-helper zero (px ∷ p) = <-¬≡ px suc-helper (suc q) (px ∷ p) = suc-helper q p @@ -472,7 +468,7 @@ empty-env = record -- The actor can't have any known references singleton-env : ∀ {IS A post} → ActorM ∞ IS A [] post → Env singleton-env {IS} {A} {post} actor = record - { acts = record + { acts = [ record { inbox-shape = IS ; A = A ; references = [] @@ -481,13 +477,13 @@ singleton-env {IS} {A} {post} actor = record ; post = post ; computation = record { act = actor ; cont = [] } ; name = name-supply-singleton .supply .name - } ∷ [] + } ]ˡ ; blocked = [] ; env-inboxes = [] ∷ [] - ; store = inbox# 0 [ IS ] ∷ [] - ; actors-valid = (record { actor-has-inbox = zero ; references-have-pointer = [] }) ∷ [] + ; store = [ inbox# 0 [ IS ] ]ˡ + ; actors-valid = [ record { actor-has-inbox = zero ; references-have-pointer = [] }]ᵃ ; blocked-valid = [] - ; messages-valid = [] ∷ [] + ; messages-valid = [] ∷ [] ; name-supply = name-supply-singleton .next IS ; blocked-no-progress = [] } diff --git a/src/Singleton.agda b/src/Singleton.agda new file mode 100644 index 0000000..2e01160 --- /dev/null +++ b/src/Singleton.agda @@ -0,0 +1,17 @@ +module Singleton where + +open import Data.List + using (List ; [] ; _∷_) +open import Data.List.All + using (All ; [] ; _∷_) +open import Membership + using (_∈_; _⊆_ ; _∷_ ; []) + +[_]ˡ : ∀{a}{A : Set a} → A → List A +[ a ]ˡ = a ∷ [] + +[_]ᵃ : ∀{a p} {A : Set a} {P : A → Set p} {x : A} → P x → All P (x ∷ []) +[ p ]ᵃ = p ∷ [] + +[_]ᵐ : ∀{a} {A : Set a} {x : A} {ys : List A} → (x ∈ ys) → ((x ∷ []) ⊆ ys) +[ p ]ᵐ = p ∷ []