diff --git a/README.md b/README.md index 8e8ec27..4c59c10 100644 --- a/README.md +++ b/README.md @@ -10,8 +10,19 @@ in a style inspired by Effects from Idris and Koen Claessen's Poor Man's Concurr | Dependency | Version | |------------------|------------------------------------------| -| Agda | 2.5.3 | -| standard-library | 27182f8b24f0493a184e5ee82b285d18c61d6a37 | +| Agda | 8a7ad7f79c09d3a55110b6f92ab07267564601f0 | +| standard-library | 2a40a031e40042e72e245cce17956e5df49fcdd5 | + +## How to build? +Agda and the standard library are nightlies for Agda 2.5.4. +The simplest way to build Agda is to clone the repo and run +`stack install --stack-yaml stack-8.2.2.yaml`. +The nightlies are used to get do-notation and solve some bugs with codata. + +The project itself can be built with make or using agda-mode in emacs. +Latex files can be generated with `make latex`, but most of the thesis is kept in ShareLatex. + +## Project structure | File | Description | |-----------------------|----------------------------------------------------------| @@ -20,4 +31,6 @@ in a style inspired by Effects from Idris and Koen Claessen's Poor Man's Concurr | ActorMonad | The embedding you use to create different actor programs | | SimulationEnvironment | The datastructures and proofs used in the simulation | | EnvironmentOperations | Functions modifying the simulation environment | +| Examples | Showcases patterns and code used in the thesis | +| Selective | Selective receive as a primary operation | | unused | Old code I didn't want to throw away yet | diff --git a/latex.make b/latex.make index 87162c3..e95b6fe 100644 --- a/latex.make +++ b/latex.make @@ -4,6 +4,8 @@ subdirs := src/ src/Examples/ src/Selective/ src/Selective/Examples/ sources := $(wildcard $(subdirs:%=%*.lagda.tex)) renamed := $(sources:%.lagda.tex=%.tex) moved := $(renamed:src/%=$(LATEX-OUTPUT-DIR)%) +out-subdirs := $(subdirs:src/%=$(LATEX-OUTPUT-DIR)%) +generated := $(wildcard $(out-subdirs:%=%*.tex)) $(moved): $(LATEX-OUTPUT-DIR)%.tex: src/%.lagda.tex stack exec agda -- --latex-dir=$(LATEX-OUTPUT-DIR) --latex $< @@ -12,4 +14,5 @@ $(moved): $(LATEX-OUTPUT-DIR)%.tex: src/%.lagda.tex .PHONY: all clean all: $(moved) -clean: rm -rf $(LATEX-OUTPUT-DIR) \ No newline at end of file +clean: + rm $(wildcard $(wildcard $(generated))) \ No newline at end of file diff --git a/src/.#ActorMonad.lagda.tex b/src/.#ActorMonad.lagda.tex deleted file mode 100644 index 8da5454..0000000 --- a/src/.#ActorMonad.lagda.tex +++ /dev/null @@ -1 +0,0 @@ -kpier@BALMUNG.16712:1515698921 \ No newline at end of file diff --git a/src/ActorMonad.lagda.tex b/src/ActorMonad.lagda.tex index 43afa8a..dbda55c 100644 --- a/src/ActorMonad.lagda.tex +++ b/src/ActorMonad.lagda.tex @@ -6,8 +6,8 @@ open import Data.List.All using (All ; [] ; _∷_) open import Data.Unit using (⊤ ; tt) -open import Coinduction using (∞ ; ♯_ ; ♭) 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. @@ -177,13 +177,13 @@ Following are some examples comparing a λ-calculus with names and a λ-calculus using de Bruijn indices. -\begin{table}[] +\begin{table}[h] \centering \begin{tabular}{ll} Named & de Bruijn \\ $ λ\ x → x $ & $ λ\ 1 $ \\ $ λ\ x → λ\ y → x $ & $ λ\ λ\ 2 $ \\ -$ λ\ x → λ\ y → λ\ z → x\ z\ (y\ z) $ & $ λ\ λ\ λ\ 3\ 1\ (2\ 1) $ \\ +$ λ\ x → λ\ y → λ\ z → x\ z\ (y\ z) $ & $ λ\ λ\ λ\ 3\ 1\ (2\ 1) $ \\ \end{tabular} \end{table} @@ -255,7 +255,10 @@ send-field-content Γ (ReferenceType requested) = Γ ⊢>: requested data SendMessage (To : InboxShape) (Γ : TypingContext) : Set₁ where - SendM : {MT : MessageType} → MT ∈ To → All (send-field-content Γ) MT → SendMessage To Γ + SendM : {MT : MessageType} → + MT ∈ To → + All (send-field-content Γ) MT → + SendMessage To Γ \end{code} Somewhat surprisingly, @@ -275,7 +278,10 @@ receive-field-content (ReferenceType Fw) = ⊤ data Message (To : InboxShape) : Set₁ where - Msg : {MT : MessageType} → MT ∈ To → All receive-field-content MT → Message To + Msg : {MT : MessageType} → + MT ∈ To → + All receive-field-content MT → + Message To extract-references : MessageType → ReferenceTypes extract-references [] = [] @@ -287,7 +293,7 @@ \end{code} % \begin{code} -infixl 1 _>>=_ +infixl 1 _∞>>=_ _>>=_ _∞>>_ _>>_ \end{code} %<*LiftTop> \AgdaTarget{⊤₁} @@ -322,10 +328,20 @@ \AgdaTarget{ActorM} \begin{code} -data ActorM (IS : InboxShape) : (A : Set₁) → +data ActorM (i : Size) (IS : InboxShape) : (A : Set₁) → (pre : TypingContext) → (post : A → TypingContext) → - Set₂ where + Set₂ + +record ∞ActorM (i : Size) (IS : InboxShape) (A : Set₁) + (pre : TypingContext) + (post : A → TypingContext) : + Set₂ where + coinductive + constructor delay_ + field force : ∀ {j : Size< i} → ActorM j IS A pre post + +data ActorM (i : Size) (IS : InboxShape) where \end{code} % %<*ActorMonadBindReturn> @@ -344,10 +360,10 @@ \AgdaTarget{Return} \begin{code} - Return : ∀ {A post} → (val : A) → ActorM IS A (post val) post - _>>=_ : ∀ {A B pre mid post} → (m : ∞ (ActorM IS A pre mid)) → - (f : (x : A) → ∞ (ActorM IS B (mid x) (post))) → - ActorM IS B pre post + Return : ∀ {A post} → (val : A) → ActorM i IS A (post val) post + _∞>>=_ : ∀ {A B pre mid post} → (m : ∞ActorM i IS A pre mid) → + (f : (x : A) → ∞ActorM i IS B (mid x) (post)) → + ActorM i IS B pre post \end{code} % %<*ActorMonadSpawn> @@ -359,13 +375,13 @@ \AgdaTarget{Spawn} \begin{code} Spawn : {NewIS : InboxShape} → {A : Set₁} → ∀ {pre postN} → - ActorM NewIS A [] postN → - ActorM IS ⊤₁ pre λ _ → NewIS ∷ pre + ActorM i NewIS A [] postN → + ActorM i IS ⊤₁ pre λ _ → NewIS ∷ pre \end{code} % %<*ActorMonadSend> An actor can send messages to any actor it has a reference to. -It is not explicit in the monad what happens to a sent message, but we will see in (SECTION) +It is not explicit in the monad what happens to a sent message, but we will see in (SECTION) that evaluating Send will append the message to the actor being referenced. The reference variable might be a subtype to the underlying actor it references, but this fact is completely opaque to the \AgdaRef[ActorMonad]{Send} construct. @@ -377,7 +393,7 @@ Send : ∀ {pre} → {ToIS : InboxShape} → (canSendTo : pre ⊢ ToIS) → (msg : SendMessage ToIS pre) → - ActorM IS ⊤₁ pre (λ _ → pre) + ActorM i IS ⊤₁ pre (λ _ → pre) \end{code} % %<*ActorMonadReceive> @@ -392,7 +408,7 @@ actors to be implemented as non-parameterized monads. \AgdaTarget{Receive} \begin{code} - Receive : ∀ {pre} → ActorM IS (Message IS) pre (add-references pre) + Receive : ∀ {pre} → ActorM i IS (Message IS) pre (add-references pre) \end{code} % %<*ActorMonadSelf> @@ -402,7 +418,7 @@ In \AgdaRef[ActorMonad]{ActorM}, this need is fulfilled by the \AgdaRef[ActorMonad]{Self} construct, which adds a reference to the actor itself to the variable context. \begin{code} - Self : ∀ {pre} → ActorM IS ⊤₁ pre (λ _ → IS ∷ pre) + Self : ∀ {pre} → ActorM i IS ⊤₁ pre (λ _ → IS ∷ pre) \end{code} % %<*ActorMonadStrengthen> @@ -423,7 +439,7 @@ \AgdaTarget{Strengthen} \begin{code} Strengthen : ∀ {ys xs} → (inc : ys ⊆ xs) → - ActorM IS ⊤₁ xs (λ _ → ys) + ActorM i IS ⊤₁ xs (λ _ → ys) \end{code} % @@ -434,44 +450,79 @@ -- ========== Helpers for ActorM ========== -- +open ∞ActorM public + -- coinduction helper for Value -return₁ : {A : Set (suc zero)} → ∀ {IS post} → (val : A) → ∞ (ActorM IS A (post val) post) -return₁ val = ♯ Return val +return₁ : {A : Set (suc zero)} → ∀ {i IS post} → (val : A) → + ∞ActorM i IS A (post val) post +return₁ val .force = Return val -- universe lifting for return₁ -return : {A : Set} → ∀ {IS post} → (val : A) → ∞ (ActorM IS (Lift A) (post (lift val)) post) +return : {A : Set} → ∀ {i IS post} → (val : A) → + ∞ActorM i IS (Lift A) (post (lift val)) post return val = return₁ (lift val) +_>>=_ : ∀ {i IS A B pre mid post} → (m : ∞ActorM i IS A pre mid) → + (f : (x : A) → ∞ActorM i IS B (mid x) (post)) → + ∞ActorM i IS B pre post +(m >>= f) .force = m ∞>>= f + +_∞>>_ : ∀ {i IS A B pre mid post} → (m : ∞ActorM i IS A pre (λ _ → mid)) → + (n : ∞ActorM i IS B mid post) → + ActorM i IS B pre post +m ∞>> n = m ∞>>= λ _ → n + +[mid:_]_>>=_ : ∀ {i IS A B pre post} → ∀ mid → + (m : ∞ActorM i IS A pre mid) → + (f : (x : A) → ∞ActorM i IS B (mid x) (post)) → + ∞ActorM i IS B pre post +[mid: mid ] m >>= f = _>>=_ {mid = mid} m f + +_>>_ : ∀ {i IS A B pre mid post} → (m : ∞ActorM i IS A pre (λ _ → mid)) → + (n : ∞ActorM i IS B mid post) → + ∞ActorM i IS B pre post +(m >> n) .force = m ∞>> n + +[mid:_]_>>_ : ∀ {i IS A B pre post} → ∀ mid → + (m : ∞ActorM i IS A pre (λ _ → mid)) → + (n : ∞ActorM i IS B mid (post)) → + ∞ActorM i IS B pre post +[mid: mid ] m >> f = _>>_ {mid = mid} m f + -- coinduction helper for spawn -spawn : ∀ {IS NewIS A pre postN} → - ActorM NewIS A [] postN → - ∞ (ActorM IS ⊤₁ pre λ _ → NewIS ∷ pre) -spawn newAct = ♯ Spawn newAct +spawn : ∀ {i IS NewIS A pre postN} → + ActorM i NewIS A [] postN → + ∞ActorM (↑ i) IS ⊤₁ pre λ _ → NewIS ∷ pre +spawn newAct .force = Spawn newAct -- spawn potentially infinite actors -spawn∞ : ∀ {IS NewIS A pre postN} → - ∞ (ActorM NewIS A [] postN) → - ∞ (ActorM IS ⊤₁ pre λ _ → NewIS ∷ pre) -spawn∞ newAct = spawn (♭ newAct) +spawn∞ : ∀ {i IS NewIS A pre postN} → + ∞ActorM (↑ i) NewIS A [] postN → + ∞ActorM (↑ i) IS ⊤₁ pre λ _ → NewIS ∷ pre +spawn∞ newAct = spawn (newAct .force) -- coinduction helper and neater syntax for message sending -_![t:_]_ : ∀ {IS ToIS pre MT} → +_![t:_]_ : ∀ {i IS ToIS pre MT} → (canSendTo : ToIS ∈ pre) → (MT ∈ ToIS) → All (send-field-content pre) MT → - ∞ (ActorM IS ⊤₁ pre (λ _ → pre)) -canSendTo ![t: p ] fields = ♯ Send canSendTo (SendM p fields) + ∞ActorM i IS ⊤₁ pre (λ _ → pre) +(canSendTo ![t: p ] fields) .force = Send canSendTo (SendM p fields) -- coinduction helper for Receive -receive : ∀ {IS pre} → ∞ (ActorM IS (Message IS) pre (add-references pre)) -receive = ♯ Receive +receive : ∀ {i IS pre} → ∞ActorM i IS (Message IS) pre (add-references pre) +receive .force = Receive + +self : ∀ {i IS pre} → ∞ActorM i IS ⊤₁ pre (λ _ → IS ∷ pre) +self .force = Self -- coinduction helper for Strengthen -strengthen : ∀ {IS xs ys} → ys ⊆ xs → ∞ (ActorM IS ⊤₁ xs (λ _ → ys)) -strengthen inc = ♯ Strengthen inc +strengthen : ∀ {i IS xs ys} → ys ⊆ xs → ∞ActorM i IS ⊤₁ xs (λ _ → ys) +strengthen inc .force = Strengthen inc ⊠-of-values : List Set → InboxShape ⊠-of-values [] = [] ⊠-of-values (x ∷ vs) = (ValueType x ∷ []) ∷ ⊠-of-values vs \end{code} -% \ No newline at end of file +% + diff --git a/src/Colist.agda b/src/Colist.agda new file mode 100644 index 0000000..c40e64b --- /dev/null +++ b/src/Colist.agda @@ -0,0 +1,14 @@ +module Colist where + +open import Size using (Size ; Size<_) + +data Colist (i : Size) {a} (A : Set a) : Set a + +record ∞Colist (i : Size) {a} (A : Set a) : Set a where + coinductive + constructor delay_ + field force : ∀ {j : Size< i} → Colist i A + +data Colist (i : Size) {a} (A : Set a) where + [] : Colist i A + _∷_ : (x : A) (xs : ∞Colist i A) → Colist i A diff --git a/src/EnvironmentOperations.agda b/src/EnvironmentOperations.agda index 1d56c24..72fd0b1 100644 --- a/src/EnvironmentOperations.agda +++ b/src/EnvironmentOperations.agda @@ -18,6 +18,7 @@ open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; co open import Relation.Nullary using (Dec ; yes ; no) open import Level using (Lift ; lift) +open import Size using (∞) open Actor open ValidActor @@ -26,7 +27,7 @@ open NamedInbox -- We can create a new Actor from an ActorM if we know its name. -- This is used when spawning an actor. -new-actor : ∀ {IS A post} → ActorM IS A [] post → Name → Actor +new-actor : ∀ {IS A post} → ActorM ∞ IS A [] post → Name → Actor new-actor {IS} {A} {post} m name = record { inbox-shape = IS ; A = A @@ -41,7 +42,7 @@ new-actor {IS} {A} {post} m name = record -- An actor can be lifted to run sub-programs that need less references lift-actor : (actor : Actor) → {pre : TypingContext} → (references : Store) → (pre-eq-refs : (map shape references) ≡ pre) → - ActorM (inbox-shape actor) (A actor) pre (post actor) → Actor + ActorM ∞ (inbox-shape actor) (A actor) pre (post actor) → Actor lift-actor actor {pre} references pre-eq-refs m = record { inbox-shape = inbox-shape actor ; A = A actor @@ -55,7 +56,7 @@ lift-actor actor {pre} references pre-eq-refs m = record -- Replace the monadic part of an actor -- Many of the bind-operations don't change anything except what the next step should be. -replace-actorM : (actor : Actor) → ActorM (inbox-shape actor) (A actor) (pre actor) (post actor) → Actor +replace-actorM : (actor : Actor) → ActorM ∞ (inbox-shape actor) (A actor) (pre actor) (post actor) → Actor replace-actorM actor m = record { inbox-shape = inbox-shape actor ; A = A actor @@ -70,7 +71,7 @@ replace-actorM actor m = record -- Add one reference to an actor. -- Used when receiving a reference, spawn, or self. -- The precondition and references are equal via the congruence relation on consing the shape of the reference. -add-reference : (actor : Actor) → (nm : NamedInbox) → ActorM (inbox-shape actor) (A actor) (shape nm ∷ pre actor) (post actor) → Actor +add-reference : (actor : Actor) → (nm : NamedInbox) → ActorM ∞ (inbox-shape actor) (A actor) (shape nm ∷ pre actor) (post actor) → Actor add-reference actor nm m = record { inbox-shape = inbox-shape actor ; A = A actor @@ -82,7 +83,7 @@ add-reference actor nm m = record ; name = name actor } -add-references-to-actor : (actor : Actor) → (nms : List NamedInbox) → ActorM (inbox-shape actor) (A actor) ((map shape nms) ++ pre actor) (post actor) → Actor +add-references-to-actor : (actor : Actor) → (nms : List NamedInbox) → ActorM ∞ (inbox-shape actor) (A actor) ((map shape nms) ++ pre actor) (post actor) → Actor add-references-to-actor actor nms m = record { inbox-shape = inbox-shape actor ; A = A actor @@ -94,7 +95,10 @@ add-references-to-actor actor nms m = record ; name = name actor } -add-references-rewrite : (actor : Actor) → (nms : List NamedInbox) → {x : Message (inbox-shape actor)} → map shape nms ++ pre actor ≡ add-references (pre actor) x → ActorM (inbox-shape actor) (A actor) (add-references (pre actor) x) (post actor) → Actor +add-references-rewrite : (actor : Actor) → (nms : List NamedInbox) → {x : Message (inbox-shape actor)} → + map shape nms ++ pre actor ≡ add-references (pre actor) x → + ActorM ∞ (inbox-shape actor) (A actor) (add-references (pre actor) x) (post actor) → + Actor add-references-rewrite actor nms {x} p m = record { inbox-shape = inbox-shape actor ; A = A actor @@ -243,7 +247,7 @@ messages-valid-suc {store} {IS} {n} {x} {nx ∷ _} frsh (px ∷ vi) = message-va -- Add a new actor to the environment. -- The actor is added to the top of the list of actors. -add-top : ∀ {IS A post} → ActorM IS A [] post → Env → Env +add-top : ∀ {IS A post} → ActorM ∞ IS A [] post → Env → Env add-top {IS} {A} {post} actor-m env = record { acts = record { inbox-shape = IS diff --git a/src/Examples/Call.agda b/src/Examples/Call.agda index 026fc97..fa8416f 100644 --- a/src/Examples/Call.agda +++ b/src/Examples/Call.agda @@ -11,7 +11,9 @@ 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 Examples.SelectiveReceive -- using (selective-receive ; SelRec ; waiting-refs ; add-references++) +open import Examples.SelectiveReceive using (selective-receive ; SelRec ; waiting-refs ; add-references++ ; ∈-inc ; ⊆++-refl) + +open import Size open SelRec @@ -24,14 +26,15 @@ call-select-unwrap (S x) (S p) = call-select-unwrap x p call-select : ∀ {IS IS' MtIn} → IS' <: IS → MtIn ∈ IS' → Message IS → Bool call-select sub which (Msg x x₁) = call-select-unwrap x (translate-⊆ sub which) -call : ∀ {Γ MtTo MtIn} {To IS IS' : InboxShape} → (q : List (Message IS)) → (Γ ⊢ To) → +call : ∀ {Γ MtTo MtIn i} {To IS IS' : InboxShape} → (q : List (Message IS)) → (Γ ⊢ To) → ((ReferenceType IS' ∷ MtTo) ∈ To) → All (send-field-content Γ) MtTo → (ISsubs : IS' <: IS) → (whichIn : MtIn ∈ IS') → - (ActorM IS (SelRec IS (call-select ISsubs whichIn)) (Γ ++ (waiting-refs q)) (λ m → (add-references Γ (msg m)) ++ (waiting-refs (waiting m)))) -call {Γ} {IS = IS} q var toFi vals sub whichIn = ♯ Self >>= λ _ → - ♯ ((S (translate-⊆ (⊆++-refl Γ (waiting-refs q)) var) ![t: toFi ] (([ Z ]>: sub) ∷ translate-fields vals)) >>= λ _ → - ♯ (strengthen (⊆-suc ⊆-refl) >>= λ _ → - ♯ selective-receive q (call-select sub whichIn))) + ∞ActorM i IS (SelRec IS (call-select ISsubs whichIn)) (Γ ++ (waiting-refs q)) (λ m → (add-references Γ (msg m)) ++ (waiting-refs (waiting m))) +call {Γ} {IS = IS} q var toFi vals sub whichIn = do + self + S (translate-⊆ (⊆++-refl Γ (waiting-refs q)) var) ![t: toFi ] (([ Z ]>: sub) ∷ (translate-fields vals)) + strengthen (⊆-suc ⊆-refl) + selective-receive q (call-select sub whichIn) where translate-fields : ∀ {MT} → All (send-field-content Γ) MT → All (send-field-content (IS ∷ Γ ++ waiting-refs q)) MT translate-fields {[]} [] = [] @@ -41,26 +44,27 @@ call {Γ} {IS = IS} q var toFi vals sub whichIn = ♯ Self >>= λ _ → Calculator : InboxShape Calculator = (ReferenceType ((ValueType ℕ ∷ []) ∷ []) ∷ ValueType ℕ ∷ ValueType ℕ ∷ []) ∷ [] -calculatorActor : ActorM Calculator (Lift ⊤) [] (λ _ → []) -calculatorActor = loop >>= return₁ +calculatorActor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift ⊤) [] (λ _ → []) +calculatorActor = loop where - loop : ∞ (ActorM Calculator (Lift ⊤) [] (λ _ → [])) - loop = ♯ (receive >>= λ { - (Msg Z (_ ∷ n ∷ m ∷ [])) → ♯ ((Z ![t: Z ] ((lift (n + m)) ∷ [])) >>= λ _ → ♯ (strengthen [] >>= λ _ → loop)) - ; (Msg (S ()) x₁) - }) + loop : ∀ {i} → ∞ActorM i Calculator (Lift ⊤) [] (λ _ → []) + loop .force = receive ∞>>= λ { + (Msg Z (_ ∷ n ∷ m ∷ [])) → do + Z ![t: Z ] ((lift (n + m)) ∷ []) + strengthen [] + loop + ; (Msg (S ()) _) } TestBox : InboxShape TestBox = ((ValueType ℕ ∷ [])) ∷ [] ∷ [] -calltestActor : ActorM TestBox (Lift ℕ) [] (λ _ → []) -calltestActor = spawn calculatorActor >>= (λ _ → - ♯ (_>>=_ { mid = λ m → add-references (Calculator ∷ []) (msg m) ++ waiting-refs (waiting m)} - (♯ (call [] Z Z ((lift 10) ∷ ((lift 32) ∷ []))) (Z ∷ []) Z) λ x → - ♯ ( strengthen [] >>= λ _ → - return-result x))) +calltestActor : ∀ {i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → []) +calltestActor .force = spawn∞ calculatorActor ∞>> + [mid: (λ m → add-references (Calculator ∷ []) (msg m) ++ waiting-refs (waiting m)) ] call [] Z Z ((lift 10) ∷ ((lift 32) ∷ [])) (Z ∷ []) Z >>= + λ x → strengthen [] >> + return-result x where - return-result : SelRec TestBox (call-select (Z ∷ []) Z) → ∞ (ActorM TestBox (Lift ℕ) [] (λ _ → [])) + return-result : SelRec TestBox (call-select (Z ∷ []) Z) → ∀ {i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → []) return-result record { msg = (Msg Z (px ∷ x₁)) ; right-msg = right-msg ; waiting = waiting } = return px return-result record { msg = (Msg (S x) x₁) ; right-msg = () } diff --git a/src/Examples/InfiniteBind.agda b/src/Examples/InfiniteBind.agda index c771aee..f0c7d95 100644 --- a/src/Examples/InfiniteBind.agda +++ b/src/Examples/InfiniteBind.agda @@ -11,6 +11,6 @@ open import Data.Unit using (⊤ ; tt) Box : InboxShape Box = [] -binder : ActorM Box ⊤₁ [] (λ _ → []) -binder = ♯ binder >>= λ _ → ♯ binder +binder : ∀ {i} → ∞ActorM i Box ⊤₁ [] (λ _ → []) +binder .force = binder ∞>> binder diff --git a/src/Examples/Main-template.agda b/src/Examples/Main-template.agda index 5d3a735..e9b752c 100644 --- a/src/Examples/Main-template.agda +++ b/src/Examples/Main-template.agda @@ -5,11 +5,13 @@ import Examples.SelectiveReceive as SelectiveReceive import Examples.Call as Call open import Runtime open import SimulationEnvironment +open import ActorMonad import IO +open ∞ActorM -pingpongEntry = singleton-env PingPong.spawner -infinitebindEntry = singleton-env InfiniteBind.binder +pingpongEntry = singleton-env (PingPong.spawner .force) +infinitebindEntry = singleton-env (InfiniteBind.binder .force) selectiveReceiveEntry = singleton-env SelectiveReceive.spawner -callEntry = singleton-env Call.calltestActor +callEntry = singleton-env (Call.calltestActor .force) main = IO.run (run-env trace+actors-logger __ENTRY__) diff --git a/src/Examples/Main.agda b/src/Examples/Main.agda index 2ea1be9..11a55fa 100644 --- a/src/Examples/Main.agda +++ b/src/Examples/Main.agda @@ -5,11 +5,13 @@ import Examples.SelectiveReceive as SelectiveReceive import Examples.Call as Call open import Runtime open import SimulationEnvironment +open import ActorMonad import IO +open ∞ActorM -pingpongEntry = singleton-env PingPong.spawner -infinitebindEntry = singleton-env InfiniteBind.binder +pingpongEntry = singleton-env (PingPong.spawner .force) +infinitebindEntry = singleton-env (InfiniteBind.binder .force) selectiveReceiveEntry = singleton-env SelectiveReceive.spawner -callEntry = singleton-env Call.calltestActor +callEntry = singleton-env (Call.calltestActor .force) main = IO.run (run-env trace+actors-logger pingpongEntry) diff --git a/src/Examples/NonTermination.lagda.tex b/src/Examples/NonTermination.lagda.tex new file mode 100644 index 0000000..1a619cd --- /dev/null +++ b/src/Examples/NonTermination.lagda.tex @@ -0,0 +1,16 @@ +\begin{code} +module Examples.NonTermination where +\end{code} + +%<*ProveAnything> +\begin{code} +{-# NON_TERMINATING #-} +anything : ∀ {a} {A : Set a} → A +anything = anything + +data ⊥ : Set where + +can-prove-⊥ : ⊥ +can-prove-⊥ = anything +\end{code} +% diff --git a/src/Examples/Peano.lagda.tex b/src/Examples/Peano.lagda.tex new file mode 100644 index 0000000..65ab698 --- /dev/null +++ b/src/Examples/Peano.lagda.tex @@ -0,0 +1,15 @@ +\begin{code} +module Examples.Peano where +\end{code} + +%<*Peano> +\begin{code} +data ℕ : Set where + zero : ℕ + 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 203f52c..9c077ad 100644 --- a/src/Examples/PingPong.agda +++ b/src/Examples/PingPong.agda @@ -5,7 +5,7 @@ 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 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) @@ -47,62 +47,65 @@ mutual constPingrefs : {A : Set₁} → (A → TypingContext) constPingrefs _ = PingRefs -pingMainActor : (A : Set₁) → Set₂ -pingMainActor A = ActorM Pingbox A PingRefs constPingrefs +pingMainActor : (i : Size) (A : Set₁) → Set₂ +pingMainActor i A = ∞ActorM i Pingbox A PingRefs constPingrefs mutual - pingReceive : (msg : Message Pingbox) → ∞ (ActorM Pingbox (Lift Bool) (add-references PingRefs msg) constPingrefs) + 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 : ∞ (pingMainActor (Lift Bool)) - loopTillPingValue = ♯ (receive >>= pingReceive) + loopTillPingValue : ∀ {i} → pingMainActor i (Lift Bool) + loopTillPingValue .force = receive ∞>>= pingReceive -pinger : ActorM Pingbox ⊤₁ [] constPingrefs -pinger = loopTillPong >>= (λ _ → pingMain 0) +pinger : ∀ {i} → ∞ActorM (↑ i) Pingbox ⊤₁ [] constPingrefs +pinger .force = loopTillPong ∞>> pingMain 0 where - loopTillPong : ∞ (ActorM Pingbox ⊤₁ [] constPingrefs) - loopTillPong = ♯ (receive >>= ((λ + loopTillPong : ∀ {i} → ∞ActorM i Pingbox ⊤₁ [] constPingrefs + loopTillPong .force = receive ∞>>= ((λ { (Msg Z x₁) → loopTillPong ; (Msg (S Z) x₁) → return _ ; (Msg (S (S ())) x₁) - }))) - pingMain : ℕ → ∞ (pingMainActor ⊤₁) - pingMain n = ♯ ((loopTillPingValue >>= λ - { (lift false) → ♯ ( (Z ![t: Z ] (lift n ∷ [])) >>= λ _ → pingMain (suc n)) - ; (lift true) → return _})) + })) + pingMain : ∀ {i} → ℕ → pingMainActor i ⊤₁ + pingMain n .force = loopTillPingValue ∞>>= λ + { (lift false) → (Z ![t: Z ] (lift n ∷ [])) >> pingMain (suc n) + ; (lift true) → return _} constPongrefs : {A : Set₁} → (A → TypingContext) constPongrefs _ = PongRefs -pongMainActor : (A : Set₁) → Set₂ -pongMainActor A = ActorM Pongbox A PongRefs constPongrefs +pongMainActor : (i : Size) (A : Set₁) → Set₂ +pongMainActor i A = ∞ActorM i Pongbox A PongRefs constPongrefs mutual - pongReceive : (msg : Message Pongbox) → ∞ (ActorM Pongbox (Lift ℕ) (add-references PongRefs msg) constPongrefs) + 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 : ∞ (pongMainActor (Lift ℕ)) - loopTillPongValue = ♯ (receive >>= pongReceive) + loopTillPongValue : ∀ {i} → pongMainActor i (Lift ℕ) + loopTillPongValue .force = receive ∞>>= pongReceive -ponger : ActorM Pongbox ⊤₁ [] constPongrefs -ponger = loopTillPing >>= λ _ → ♯ ((Z ![t: Z ] ((lift false) ∷ [])) >>= λ _ → pongMain) +ponger : ∀ {i} → ∞ActorM (↑ i) Pongbox ⊤₁ [] constPongrefs +ponger .force = loopTillPing ∞>> ((Z ![t: Z ] ((lift false) ∷ [])) >> pongMain) where - loopTillPing : ∞ (ActorM Pongbox ⊤₁ [] constPongrefs) - loopTillPing = ♯ (receive >>= λ { + loopTillPing : ∀ {i} → ∞ActorM i Pongbox ⊤₁ [] constPongrefs + loopTillPing .force = receive ∞>>= λ { (Msg Z _) → loopTillPing ; (Msg (S Z) _) → return _ ; (Msg (S (S ())) _) - }) - pongMain : ∞ (pongMainActor ⊤₁) - pongMain = ♯ (loopTillPongValue >>= λ - { (lift 10) → ♯ (Z ![t: Z ] ((lift true) ∷ []) >>= λ _ → return _) - ; (lift n) → ♯ (Z ![t: Z ] ((lift false) ∷ []) >>= λ _ → pongMain)}) + } + pongMain : ∀ {i} → pongMainActor i ⊤₁ + pongMain .force = loopTillPongValue ∞>>= λ { + (lift 10) → Z ![t: Z ] ((lift true) ∷ []) + ; (lift n) → (Z ![t: Z ] ((lift false) ∷ [])) >> pongMain + } -- TODO: this needs to look prettier -spawner : ActorM 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/Examples/SelectiveReceive.agda b/src/Examples/SelectiveReceive.agda index 41dd5a4..680de32 100644 --- a/src/Examples/SelectiveReceive.agda +++ b/src/Examples/SelectiveReceive.agda @@ -6,8 +6,8 @@ open import Data.List.All using (All ; _∷_ ; []) open import Data.List.Properties using (++-assoc ; ++-identityʳ) 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 (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 using (_∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] ; ⊆-refl ; ⊆-trans ; ⊆-suc) @@ -142,17 +142,17 @@ record SelRec (IS : InboxShape) (f : Message IS → Bool) : Set₁ where open SelRec -selective-receive : ∀ {IS pre} → (q : List (Message IS)) → (f : Message IS → Bool) → ActorM IS (SelRec IS f) (pre ++ (waiting-refs q)) (λ m → (add-references pre (msg m)) ++ (waiting-refs (waiting m))) -selective-receive {IS} {pre} q f = case-of-find (find-split q f) +selective-receive : ∀ {i IS pre} → (q : List (Message IS)) → (f : Message IS → Bool) → ∞ActorM i IS (SelRec IS f) (pre ++ (waiting-refs q)) (λ m → (add-references pre (msg m)) ++ (waiting-refs (waiting m))) +selective-receive {IS = IS} {pre} q f = case-of-find (find-split q f) where - case-of-find : FoundInList q f → ActorM IS (SelRec IS f) (pre ++ waiting-refs q) (λ m → add-references pre (msg m) ++ waiting-refs (waiting m)) - case-of-find (Found split x) = strengthen (accept-found pre q split) >>= λ _ → (return₁ (record { msg = el split ; right-msg = x ; waiting = (heads split) ++ (tails split) })) - case-of-find Nothing = receive >>= handle-receive + case-of-find : ∀ {i} → FoundInList q f → ∞ActorM i IS (SelRec IS f) (pre ++ waiting-refs q) (λ m → add-references pre (msg m) ++ waiting-refs (waiting m)) + case-of-find (Found split x) .force = strengthen (accept-found pre q split) ∞>> return₁ (record { msg = el split ; right-msg = x ; waiting = (heads split) ++ (tails split) }) + case-of-find Nothing .force = receive ∞>>= handle-receive where - handle-receive : (x : Message IS) → ∞ (ActorM IS (SelRec IS f) (add-references (pre ++ waiting-refs q) x) (λ m → (add-references pre (msg m) ++ waiting-refs (waiting m)))) + handle-receive : ∀ {i} (x : Message IS) → ∞ActorM i IS (SelRec IS f) (add-references (pre ++ waiting-refs q) x) (λ m → (add-references pre (msg m) ++ waiting-refs (waiting m))) handle-receive x with (f x) | (inspect f x) - handle-receive x | false | p = ♯ (strengthen (move-received pre q x) >>= λ _ → (♯ selective-receive (q ++ (x ∷ [])) f)) - handle-receive x | true | [ p ] = ♯ ( strengthen (accept-received pre q x) >>= λ _ → (return₁ ret-v)) + handle-receive {i} x | false | p = strengthen (move-received pre q x) >> selective-receive (q ++ (x ∷ [])) f + handle-receive x | true | [ p ] = strengthen (accept-received pre q x) >> return₁ ret-v where ret-v : SelRec IS f ret-v = record { msg = x ; right-msg = p ; waiting = q } @@ -160,15 +160,15 @@ selective-receive {IS} {pre} q f = case-of-find (find-split q f) SelectiveTestBox : InboxShape SelectiveTestBox = (ValueType Bool ∷ []) ∷ [] -testActor : ActorM SelectiveTestBox (Lift Bool) [] (λ _ → []) -testActor = _>>=_ {SelectiveTestBox} {SelRec SelectiveTestBox only-true} {Lift Bool} {[]} {λ m → add-references [] (msg m) ++ waiting-refs (waiting m)} (♯ selective-receive [] only-true) after-receive +testActor : ∀ {i} → ActorM i SelectiveTestBox (Lift Bool) [] (λ _ → []) +testActor = selective-receive [] only-true ∞>>= after-receive where only-true : Message SelectiveTestBox → Bool only-true (Msg Z (b ∷ [])) = b only-true (Msg (S ()) x₁) - after-receive : (x : SelRec SelectiveTestBox only-true) → ∞ (ActorM SelectiveTestBox (Lift Bool) (add-references [] (msg x) ++ waiting-refs (waiting x)) (λ _ → [])) - after-receive record { msg = (Msg Z (.true ∷ [])) ; right-msg = refl ; waiting = waiting } = ♯ (strengthen [] >>= λ _ → (return true)) + after-receive : ∀ {i} (x : SelRec SelectiveTestBox only-true) → ∞ActorM i SelectiveTestBox (Lift Bool) (add-references [] (msg x) ++ waiting-refs (waiting x)) (λ _ → []) + after-receive record { msg = (Msg Z (.true ∷ [])) ; right-msg = refl ; waiting = waiting } = strengthen [] >> return true after-receive record { msg = (Msg (S ()) x₁) ; right-msg = right-msg ; waiting = waiting } -spawner : ActorM [] ⊤₁ [] (λ _ → []) -spawner = spawn testActor >>= λ _ → ♯ ((Z ![t: Z ] ((lift false) ∷ [])) >>= λ _ → strengthen [] ) +spawner : ∀ {i} → ActorM i [] ⊤₁ [] (λ _ → []) +spawner = spawn testActor ∞>> ((Z ![t: Z ] ((lift false) ∷ [])) >> strengthen []) diff --git a/src/Examples/SizedStream.lagda.tex b/src/Examples/SizedStream.lagda.tex new file mode 100644 index 0000000..1f8a87b --- /dev/null +++ b/src/Examples/SizedStream.lagda.tex @@ -0,0 +1,38 @@ +\begin{code} +module Examples.SizedStream where +open import Data.Nat +open import Relation.Binary.PropositionalEquality using (_≡_ ; refl) +open import Size using (Size ; Size<_ ; ↑_) + +\end{code} +%<*Stream> +\begin{code} +record Stream (i : Size) (A : Set) : Set where + coinductive + field + head : A + tail : ∀ {j : Size< i} → Stream j A +\end{code} +% +\begin{code} +open Stream +\end{code} +%<*SkipTwice> +\begin{code} +skip-twice : {i : Size} → Stream (↑ (↑ i)) ℕ → Stream i ℕ +skip-twice s = s .tail .tail +\end{code} +% +%<*Fib> +\begin{code} +zipWith : {i : Size} {A B C : Set} → (A → B → C) → + Stream i A → Stream i B → Stream i C +(zipWith f xs ys) .head = f (xs .head) (ys .head) +(zipWith f xs ys) .tail = zipWith f (xs .tail) (ys .tail) + +fib : {i : Size} → Stream i ℕ +fib .head = 0 +fib .tail .head = 1 +fib .tail .tail = zipWith _+_ fib (fib .tail) +\end{code} +% diff --git a/src/Examples/Stream.lagda.tex b/src/Examples/Stream.lagda.tex new file mode 100644 index 0000000..45d2c5d --- /dev/null +++ b/src/Examples/Stream.lagda.tex @@ -0,0 +1,40 @@ +\begin{code} +module Examples.Stream where +open import Data.Nat +open import Relation.Binary.PropositionalEquality using (_≡_ ; refl) + +\end{code} +%<*Stream> +\begin{code} +record Stream (A : Set) : Set where + coinductive + field + head : A + tail : Stream A +\end{code} +% +\begin{code} +open Stream +\end{code} +%<*AllNats> +\begin{code} +nats : ℕ → Stream ℕ +nats n .head = n +nats n .tail = nats (suc n) + +all-nats = nats 0 + +third-tail : (all-nats .tail .tail .tail .head) ≡ 3 +third-tail = refl +\end{code} +% + +\begin{code} +{-# NON_TERMINATING #-} +\end{code} +%<*NatsAlternative> +\begin{code} +nats' : ℕ → Stream ℕ +nats' n = record { head = n ; tail = nats' (suc n) } +\end{code} +% diff --git a/src/Examples/Types.lagda.tex b/src/Examples/Types.lagda.tex index 1a13c5f..cae822e 100644 --- a/src/Examples/Types.lagda.tex +++ b/src/Examples/Types.lagda.tex @@ -3,15 +3,36 @@ open import Data.Unit using (⊤ ; tt) open import Data.Bool using (Bool ; false ; true) -open import Data.Nat using (ℕ ; zero ; suc) +open import Data.Nat using (ℕ ; zero ; suc ; _+_) open import Data.Vec using (Vec ; [] ; _∷_) open import Data.List using (List ; [] ; _∷_) open import Data.String using (String) -open import Relation.Binary.PropositionalEquality using (_≡_ ; refl) open import ActorMonad \end{code} +%<*PropositionalEquality> +\begin{code} +data _≡_ {a} {A : Set a} (x : A) : A → Set a where + refl : x ≡ x + +trivial = 4 ≡ 4 +definitional = (2 + 2) ≡ 4 +\end{code} +% + +%<*Cong> +\begin{code} +cong : ∀ {a} {A B : Set a} {m n : A} → (f : A → B) → m ≡ n → f m ≡ f n +cong f refl = refl + + +id-0 : (n : ℕ) → (n + 0) ≡ (0 + n) +id-0 zero = refl +id-0 (suc n) = cong suc (id-0 n) +\end{code} +% + %<*unfortunate> \begin{code} unfortunate : Set @@ -53,3 +74,22 @@ partial (suc (suc (suc n))) () \end{code} % + +%<*Identity> +\begin{code} +identity : (A : Set) → A → A +identity A x = x +\end{code} +% + +%<*ImplicitIdentity> +\begin{code} +identity' : {A : Set} → A → A +identity' x = x + +f : ℕ → ℕ +f = identity' +g = identity' {Bool} +h = identity' 2 +\end{code} +% diff --git a/src/Membership.lagda.tex b/src/Membership.lagda.tex index af54f66..ed4baf0 100644 --- a/src/Membership.lagda.tex +++ b/src/Membership.lagda.tex @@ -10,18 +10,18 @@ \end{code} %<*ElementIn> \begin{code} -data _∈_ {a} {A : Set a} : A → (List A) -> Set a where +data _∈_ {a} {A : Set a} : A → (List A) → Set a where Z : ∀ {x xs} → x ∈ (x ∷ xs) - S : ∀ {x y xs} → x ∈ xs -> x ∈ (y ∷ xs) + S : ∀ {x y xs} → x ∈ xs → x ∈ (y ∷ xs) \end{code} % \begin{code} x∈[]-⊥ : ∀ {a} {A : Set a} {x : A} → x ∈ [] → ⊥ x∈[]-⊥ () -data _⊆_ {a} {A : Set a} : List A -> List A -> Set a where +data _⊆_ {a} {A : Set a} : List A → List A → Set a where [] : ∀ {xs} → [] ⊆ xs - _∷_ : ∀ {x xs ys} → x ∈ ys -> xs ⊆ ys -> (x ∷ xs) ⊆ ys + _∷_ : ∀ {x xs ys} → x ∈ ys → xs ⊆ ys → (x ∷ xs) ⊆ ys ⊆-suc : ∀ {a} {A : Set a} {y : A} {xs ys : List A} → xs ⊆ ys → xs ⊆ (y ∷ ys) ⊆-suc [] = [] diff --git a/src/Runtime.agda b/src/Runtime.agda index 5c6bb9c..259873c 100644 --- a/src/Runtime.agda +++ b/src/Runtime.agda @@ -2,15 +2,17 @@ module Runtime where open import Simulate open import SimulationEnvironment -open import Data.Colist using (Colist ; [] ; _∷_) +open import Colist using (Colist ; ∞Colist ; [] ; _∷_) open import Data.List using (List ; _∷_ ; [] ; map ; length) 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 Coinduction using ( ♯_ ; ♭) +open import Size using (∞) import IO +open ∞Colist Logger = (ℕ → EnvStep → IO.IO ⊤) @@ -18,11 +20,11 @@ Logger = (ℕ → EnvStep → IO.IO ⊤) -- and transforms the steps taken into output to the console. -- The output can be configured by prodiving different loggers. run-env : Logger → Env → IO.IO ⊤ -run-env logger env = loop 1 (simulate env) +run-env logger env = loop 1 ((simulate env) .force) where - loop : ℕ → Colist EnvStep → IO.IO ⊤ + loop : ℕ → Colist ∞ EnvStep → IO.IO ⊤ loop n [] = IO.putStrLn ("Done after " ++ (show n) ++ " steps.") - loop n (x ∷ xs) = ♯ logger n x IO.>> ♯ loop (suc n) (♭ xs) + loop n (x ∷ xs) = ♯ logger n x IO.>> ♯ loop (suc n) (xs .force) open EnvStep open Env @@ -38,7 +40,7 @@ show-trace (Return name) = show name ++ " returned" show-trace (Bind trace) = "Bind [ " ++ show-trace trace ++ " ]" show-trace (BindDouble name) = "Bind " ++ (show name) show-trace (Spawn spawner spawned) = (show spawner) ++ " spawned " ++ (show spawned) -show-trace (Send sender receiver references) = (show sender) ++ " sent a reference to " ++ (show receiver) ++ " forwarding [" ++ showNames references ++ "]" +show-trace (Send sender receiver references) = (show sender) ++ " sent a message to " ++ (show receiver) ++ " forwarding [" ++ showNames references ++ "]" show-trace (Receive name Nothing) = (show name) ++ " received nothing. It was put in the blocked list" show-trace (Receive name (Value references)) = (show name) ++ " received a message forwarding [" ++ showNames references ++ "]" show-trace (Receive name Dropped) = (show name) ++ " received something, but had no bind. It was dropped" diff --git a/src/Selective/ActorMonad.lagda.tex b/src/Selective/ActorMonad.lagda.tex index 7b1bba3..06b7dc0 100644 --- a/src/Selective/ActorMonad.lagda.tex +++ b/src/Selective/ActorMonad.lagda.tex @@ -8,8 +8,8 @@ open import Data.Bool using (Bool ; true ; false) open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; cong ; cong₂ ; trans) -open import Coinduction using (∞ ; ♯_ ; ♭) open import Level using (Lift ; lift ; suc ; zero) +open import Size using (Size ; Size<_ ; ↑_) mutual data MessageField : Set₁ where @@ -40,14 +40,14 @@ send-field-content Γ (ReferenceType requested) = Γ ⊢>: requested data SendMessage (To : InboxShape) (Γ : TypingContext) : Set₁ where - SendM : {MT : MessageType} → MT ∈ To → All (send-field-content Γ) MT → SendMessage To Γ + SendM : {MT : MessageType} → MT ∈ To → All (send-field-content Γ) MT → SendMessage To Γ receive-field-content : MessageField → Set receive-field-content (ValueType A) = A receive-field-content (ReferenceType Fw) = ⊤ data Message (To : InboxShape) : Set₁ where - Msg : {MT : MessageType} → MT ∈ To → All receive-field-content MT → Message To + Msg : {MT : MessageType} → MT ∈ To → All receive-field-content MT → Message To extract-references : MessageType → ReferenceTypes extract-references [] = [] @@ -83,79 +83,125 @@ % \begin{code} - + ⊤₁ : Set₁ ⊤₁ = Lift ⊤ -infixl 1 _>>=_ +infixl 1 _∞>>=_ _>>=_ _∞>>_ _>>_ -data ActorM (IS : InboxShape) : (A : Set₁) → +data ActorM (i : Size) (IS : InboxShape) : (A : Set₁) → (pre : TypingContext) → (post : A → TypingContext) → + Set₂ + +record ∞ActorM (i : Size) (IS : InboxShape) (A : Set₁) + (pre : TypingContext) + (post : A → TypingContext) : Set₂ where - Return : ∀ {A post} → (val : A) → ActorM IS A (post val) post - _>>=_ : ∀ {A B pre mid post} → (m : ∞ (ActorM IS A pre mid)) → - (f : (x : A) → ∞ (ActorM IS B (mid x) (post))) → - ActorM IS B pre post + coinductive + constructor delay_ + field force : ∀ {j : Size< i} → ActorM j IS A pre post + +data ActorM (i : Size) (IS : InboxShape) where + Return : ∀ {A post} → (val : A) → ActorM i IS A (post val) post + _∞>>=_ : ∀ {A B pre mid post} → (m : ∞ActorM i IS A pre mid) → + (f : (x : A) → ∞ActorM i IS B (mid x) (post)) → + ActorM i IS B pre post Spawn : {NewIS : InboxShape} → {A : Set₁} → ∀ {pre postN} → - ActorM NewIS A [] postN → - ActorM IS ⊤₁ pre λ _ → NewIS ∷ pre + ActorM i NewIS A [] postN → + ActorM i IS ⊤₁ pre λ _ → NewIS ∷ pre Send : ∀ {pre} → {ToIS : InboxShape} → (canSendTo : pre ⊢ ToIS) → (msg : SendMessage ToIS pre) → - ActorM IS ⊤₁ pre (λ _ → pre) - Receive : ∀ {pre} → ActorM IS (Message IS) pre (add-references pre) + ActorM i IS ⊤₁ pre (λ _ → pre) + Receive : ∀ {pre} → ActorM i IS (Message IS) pre (add-references pre) \end{code} %<*SelectiveReceiveConstruct> \begin{code} SelectiveReceive : ∀ {pre} → (filter : MessageFilter IS) → - ActorM IS (SelectedMessage filter) pre (add-selected-references pre) + ActorM i IS (SelectedMessage filter) pre (add-selected-references pre) \end{code} % \begin{code} - Self : ∀ {pre} → ActorM IS ⊤₁ pre (λ _ → IS ∷ pre) + Self : ∀ {pre} → ActorM i IS ⊤₁ pre (λ _ → IS ∷ pre) Strengthen : ∀ {ys xs} → (inc : ys ⊆ xs) → - ActorM IS ⊤₁ xs (λ _ → ys) + ActorM i IS ⊤₁ xs (λ _ → ys) -- -- ========== Helpers for ActorM ========== -- +open ∞ActorM public + -- coinduction helper for Value -return₁ : {A : Set (suc zero)} → ∀ {IS post} → (val : A) → ∞ (ActorM IS A (post val) post) -return₁ val = ♯ Return val +return₁ : {A : Set (suc zero)} → ∀ {i IS post} → (val : A) → ∞ActorM i IS A (post val) post +return₁ val .force = Return val -- universe lifting for return₁ -return : {A : Set} → ∀ {IS post} → (val : A) → ∞ (ActorM IS (Lift A) (post (lift val)) post) +return : {A : Set} → ∀ {i IS post} → (val : A) → ∞ActorM i IS (Lift A) (post (lift val)) post return val = return₁ (lift val) +_>>=_ : ∀ {i IS A B pre mid post} → (m : ∞ActorM i IS A pre mid) → + (f : (x : A) → ∞ActorM i IS B (mid x) (post)) → + ∞ActorM i IS B pre post +(m >>= f) .force = m ∞>>= f + +_∞>>_ : ∀ {i IS A B pre mid post} → (m : ∞ActorM i IS A pre (λ _ → mid)) → + (n : ∞ActorM i IS B mid post) → + ActorM i IS B pre post +m ∞>> n = m ∞>>= λ _ → n + +[mid:_]_>>=_ : ∀ {i IS A B pre post} → ∀ mid → + (m : ∞ActorM i IS A pre mid) → + (f : (x : A) → ∞ActorM i IS B (mid x) (post)) → + ∞ActorM i IS B pre post +[mid: mid ] m >>= f = _>>=_ {mid = mid} m f + +_>>_ : ∀ {i IS A B pre mid post} → (m : ∞ActorM i IS A pre (λ _ → mid)) → + (n : ∞ActorM i IS B mid post) → + ∞ActorM i IS B pre post +(m >> n) .force = m ∞>> n + +[mid:_]_>>_ : ∀ {i IS A B pre post} → ∀ mid → + (m : ∞ActorM i IS A pre (λ _ → mid)) → + (n : ∞ActorM i IS B mid (post)) → + ∞ActorM i IS B pre post +[mid: mid ] m >> f = _>>_ {mid = mid} m f + -- coinduction helper for spawn -spawn : ∀ {IS NewIS A pre postN} → - ActorM NewIS A [] postN → - ∞ (ActorM IS ⊤₁ pre λ _ → NewIS ∷ pre) -spawn newAct = ♯ Spawn newAct +spawn : ∀ {i IS NewIS A pre postN} → + ActorM i NewIS A [] postN → + ∞ActorM (↑ i) IS ⊤₁ pre λ _ → NewIS ∷ pre +spawn newAct .force = Spawn newAct -- spawn potentially infinite actors -spawn∞ : ∀ {IS NewIS A pre postN} → - ∞ (ActorM NewIS A [] postN) → - ∞ (ActorM IS ⊤₁ pre λ _ → NewIS ∷ pre) -spawn∞ newAct = spawn (♭ newAct) +spawn∞ : ∀ {i IS NewIS A pre postN} → + ∞ActorM (↑ i) NewIS A [] postN → + ∞ActorM (↑ i) IS ⊤₁ pre λ _ → NewIS ∷ pre +spawn∞ newAct = spawn (newAct .force) -- coinduction helper and neater syntax for message sending -_![t:_]_ : ∀ {IS ToIS pre MT} → +_![t:_]_ : ∀ {i IS ToIS pre MT} → (canSendTo : ToIS ∈ pre) → (MT ∈ ToIS) → All (send-field-content pre) MT → - ∞ (ActorM IS ⊤₁ pre (λ _ → pre)) -canSendTo ![t: p ] fields = ♯ Send canSendTo (SendM p fields) + ∞ActorM i IS ⊤₁ pre (λ _ → pre) +(canSendTo ![t: p ] fields) .force = Send canSendTo (SendM p fields) -- coinduction helper for Receive -receive : ∀ {IS pre} → ∞ (ActorM IS (Message IS) pre (add-references pre)) -receive = ♯ Receive +receive : ∀ {i IS pre} → ∞ActorM i IS (Message IS) pre (add-references pre) +receive .force = Receive + +selective-receive : ∀ {i IS pre} → (filter : MessageFilter IS) → + ∞ActorM i IS (SelectedMessage filter) pre (add-selected-references pre) +selective-receive filter .force = SelectiveReceive filter + +self : ∀ {i IS pre} → ∞ActorM i IS ⊤₁ pre (λ _ → IS ∷ pre) +self .force = Self -- coinduction helper for Strengthen -strengthen : ∀ {IS xs ys} → ys ⊆ xs → ∞ (ActorM IS ⊤₁ xs (λ _ → ys)) -strengthen inc = ♯ Strengthen inc +strengthen : ∀ {i IS xs ys} → ys ⊆ xs → ∞ActorM i IS ⊤₁ xs (λ _ → ys) +strengthen inc .force = Strengthen inc ⊠-of-values : List Set → InboxShape ⊠-of-values [] = [] diff --git a/src/Selective/EnvironmentOperations.agda b/src/Selective/EnvironmentOperations.agda index baf088a..189f59b 100644 --- a/src/Selective/EnvironmentOperations.agda +++ b/src/Selective/EnvironmentOperations.agda @@ -19,6 +19,7 @@ open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; co open import Relation.Nullary using (Dec ; yes ; no) open import Level using (Lift ; lift ; Level) renaming (suc to lsuc) +open import Size using (∞) open Actor open ValidActor @@ -27,7 +28,7 @@ open NamedInbox -- We can create a new Actor from an ActorM if we know its name. -- This is used when spawning an actor. -new-actor : ∀ {IS A post} → ActorM IS A [] post → Name → Actor +new-actor : ∀ {IS A post} → ActorM ∞ IS A [] post → Name → Actor new-actor {IS} {A} {post} m name = record { inbox-shape = IS ; A = A @@ -42,7 +43,7 @@ new-actor {IS} {A} {post} m name = record -- An actor can be lifted to run sub-programs that need less references lift-actor : (actor : Actor) → {pre : TypingContext} → (references : Store) → (pre-eq-refs : (map shape references) ≡ pre) → - ActorM (inbox-shape actor) (A actor) pre (post actor) → Actor + ActorM ∞ (inbox-shape actor) (A actor) pre (post actor) → Actor lift-actor actor {pre} references pre-eq-refs m = record { inbox-shape = inbox-shape actor ; A = A actor @@ -56,7 +57,7 @@ lift-actor actor {pre} references pre-eq-refs m = record -- Replace the monadic part of an actor -- Many of the bind-operations don't change anything except what the next step should be. -replace-actorM : (actor : Actor) → ActorM (inbox-shape actor) (A actor) (pre actor) (post actor) → Actor +replace-actorM : (actor : Actor) → ActorM ∞ (inbox-shape actor) (A actor) (pre actor) (post actor) → Actor replace-actorM actor m = record { inbox-shape = inbox-shape actor ; A = A actor @@ -71,7 +72,7 @@ replace-actorM actor m = record -- Add one reference to an actor. -- Used when receiving a reference, spawn, or self. -- The precondition and references are equal via the congruence relation on consing the shape of the reference. -add-reference : (actor : Actor) → (nm : NamedInbox) → ActorM (inbox-shape actor) (A actor) (shape nm ∷ pre actor) (post actor) → Actor +add-reference : (actor : Actor) → (nm : NamedInbox) → ActorM ∞ (inbox-shape actor) (A actor) (shape nm ∷ pre actor) (post actor) → Actor add-reference actor nm m = record { inbox-shape = inbox-shape actor ; A = A actor @@ -83,7 +84,7 @@ add-reference actor nm m = record ; name = name actor } -add-references-to-actor : (actor : Actor) → (nms : List NamedInbox) → ActorM (inbox-shape actor) (A actor) ((map shape nms) ++ pre actor) (post actor) → Actor +add-references-to-actor : (actor : Actor) → (nms : List NamedInbox) → ActorM ∞ (inbox-shape actor) (A actor) ((map shape nms) ++ pre actor) (post actor) → Actor add-references-to-actor actor nms m = record { inbox-shape = inbox-shape actor ; A = A actor @@ -95,7 +96,10 @@ add-references-to-actor actor nms m = record ; name = name actor } -add-references-rewrite : (actor : Actor) → (nms : List NamedInbox) → {x : Message (inbox-shape actor)} → map shape nms ++ pre actor ≡ add-references (pre actor) x → ActorM (inbox-shape actor) (A actor) (add-references (pre actor) x) (post actor) → Actor +add-references-rewrite : (actor : Actor) → (nms : List NamedInbox) → {x : Message (inbox-shape actor)} → + map shape nms ++ pre actor ≡ add-references (pre actor) x → + ActorM ∞ (inbox-shape actor) (A actor) (add-references (pre actor) x) (post actor) → + Actor add-references-rewrite actor nms {x} p m = record { inbox-shape = inbox-shape actor ; A = A actor @@ -122,14 +126,13 @@ rewrap-valid-actor va refl refl refl = record { actor-has-inbox = actor-has-inbo record ValidMessageList (store : Store) (S : InboxShape) : Set₁ where field - inbox : List (NamedMessage S) + inbox : Inbox S valid : All (message-valid store) inbox -record UpdatedInboxes (store : Store) (original : Inboxes) : Set₂ where +record UpdatedInboxes (store : Store) {store' : Store} (original : Inboxes store') : Set₂ where field - updated-inboxes : Inboxes - inboxes-valid : All (all-messages-valid store) updated-inboxes - same-store : inboxes-to-store original ≡ inboxes-to-store updated-inboxes + updated-inboxes : Inboxes store' + inboxes-valid : InboxesValid store updated-inboxes open ValidMessageList open UpdatedInboxes @@ -144,25 +147,16 @@ open UpdatedInboxes -- and has to provide a proof that this list is also valid for the store update-inboxes : {name : Name} → {IS : InboxShape} → (store : Store) → - (inboxes : Inboxes) → - (All (all-messages-valid store) inboxes) → - (name ↦ IS ∈e (inboxes-to-store inboxes)) → + {store' : Store} → (inboxes : Inboxes store') → + (InboxesValid store inboxes) → + (name ↦ IS ∈e store') → (f : ValidMessageList store IS → ValidMessageList store IS) → UpdatedInboxes store inboxes -update-inboxes store [] [] () f -update-inboxes store (x ∷ inboxes) (px ∷ proofs) zero f with (f (record { inbox = Inbox.inbox-messages x ; valid = px })) -... | updated = record { - updated-inboxes = updatedInbox ∷ inboxes - ; inboxes-valid = (valid updated) ∷ proofs - ; same-store = refl } - where - updatedInbox : Inbox - updatedInbox = record { inbox-shape = Inbox.inbox-shape x ; inbox-messages = inbox updated ; name = Inbox.name x } -update-inboxes store (x ∷ inboxes) (px ∷ proofs) (suc reference) f with (update-inboxes store inboxes proofs reference f) -... | updatedInboxes = record { - updated-inboxes = x ∷ updated-inboxes updatedInboxes - ; inboxes-valid = px ∷ inboxes-valid updatedInboxes - ; same-store = cong (_∷_ inbox# (Inbox.name x) [ Inbox.inbox-shape x ]) (same-store updatedInboxes) } +update-inboxes _ _ [] () _ +update-inboxes store (x ∷ inboxes) (px ∷ proofs) zero f with (f (record { inbox = x ; valid = px })) +... | updated = record { updated-inboxes = (inbox updated) ∷ inboxes ; inboxes-valid = (valid updated) ∷ proofs } +update-inboxes store (x ∷ inboxes) (px ∷ proofs) (suc p) f with (update-inboxes store inboxes proofs p f) +... | updated = record { updated-inboxes = x ∷ updated-inboxes updated ; inboxes-valid = px ∷ (inboxes-valid updated) } -- Move the actor that is at the top of the list, to the back of the list -- This is done to create a round-robin system for the actors, since run-env always picks the actor at the top @@ -176,7 +170,6 @@ top-actor-to-back env | x ∷ acts | (y ∷ prfs) = record ; blocked = blocked env ; env-inboxes = env-inboxes env ; store = store env - ; inbs=store = inbs=store env ; fresh-name = fresh-name env ; actors-valid = ++⁺ prfs (y ∷ []) ; blocked-valid = blocked-valid env @@ -195,7 +188,6 @@ drop-top-actor env | _ ∷ rest | _ ∷ prfs = record ; blocked = blocked env ; env-inboxes = env-inboxes env ; store = store env - ; inbs=store = inbs=store env ; fresh-name = fresh-name env ; actors-valid = prfs ; blocked-valid = blocked-valid env @@ -240,30 +232,23 @@ valid-actor-suc frsh va = record { open _comp↦_∈_ -- All the messages in an inbox are still valid if we add a new inbox to the store, as long as that name is not used in the store before -messages-valid-suc : ∀ {store inb n x} → (NameFresh store n) → all-messages-valid store inb → all-messages-valid (inbox# n [ x ] ∷ store) inb -messages-valid-suc {store} {inb} {n} {x} frsh vi = do-the-work n x (Inbox.inbox-shape inb) (Inbox.inbox-messages inb) vi frsh +messages-valid-suc : ∀ {store IS n x} {inb : Inbox IS} → (NameFresh store n) → all-messages-valid store inb → all-messages-valid (inbox# n [ x ] ∷ store) inb +messages-valid-suc {store} {IS} {n} {x} frsh [] = [] +messages-valid-suc {store} {IS} {n} {x} {nx ∷ _} frsh (px ∷ vi) = message-valid-suc nx px ∷ (messages-valid-suc frsh vi) where open _comp↦_∈_ - fields-valid-suc : ∀ {MT} (x₂ : All named-field-content MT) → - all-fields-have-pointer store x₂ → all-fields-have-pointer (inbox# n [ x ] ∷ store) x₂ - fields-valid-suc {[]} [] p = p - fields-valid-suc {ValueType x₁ ∷ MT} (_ ∷ x₂) (_ , ps) = _ , fields-valid-suc x₂ ps - fields-valid-suc {ReferenceType x₁ ∷ MT} (px ∷ x₂) (p , ps) = suc-p (suc-helper (actual-has-pointer p) frsh) p , fields-valid-suc x₂ ps - msgValidSuc : (x₁ : NamedMessage (Inbox.inbox-shape inb)) → - message-valid store x₁ → message-valid (inbox# n [ x ] ∷ store) x₁ - msgValidSuc (NamedM x₁ x₂) mv = fields-valid-suc x₂ mv - message-valid-suc : ∀ {MT} (x₂ : All named-field-content MT) → all-fields-have-pointer store x₂ → ∀ n x → (NameFresh store n) → all-fields-have-pointer (inbox# n [ x ] ∷ store) x₂ - message-valid-suc {[]} [] hj n x frsh = _ - message-valid-suc {ValueType x₁ ∷ MT} (px ∷ x₂) (_ , hj) n x frsh = _ , message-valid-suc x₂ hj n x frsh - message-valid-suc {ReferenceType x₁ ∷ MT} (name ∷ x₂) (px , hj) n x frsh = (suc-p (suc-helper (actual-has-pointer px) frsh) px) , message-valid-suc x₂ hj n x frsh - do-the-work : ∀ n x w (w₁ : List (NamedMessage w)) → All (message-valid store) w₁ → NameFresh store n → - All (message-valid (inbox# n [ x ] ∷ store)) w₁ - do-the-work n x w [] prfs frsh = [] - do-the-work n x w (NamedM x₁ x₂ ∷ w₁) (px ∷ prfs) frsh = message-valid-suc x₂ px n x frsh ∷ (do-the-work n x w w₁ prfs frsh) + fields-valid-suc : ∀ {MT} {fields : All named-field-content MT} → + FieldsHavePointer store fields → + FieldsHavePointer (inbox# n [ x ] ∷ store) fields + fields-valid-suc [] = [] + fields-valid-suc (v+ valid) = v+ fields-valid-suc valid + fields-valid-suc (x ∷r valid) = (suc-p (suc-helper (actual-has-pointer x) frsh) x) ∷r (fields-valid-suc valid) + message-valid-suc : (nx : NamedMessage IS) → message-valid store nx → message-valid (inbox# n [ x ] ∷ store) nx + message-valid-suc (NamedM x₁ x₂) px = fields-valid-suc px -- Add a new actor to the environment. -- The actor is added to the top of the list of actors. -add-top : ∀ {IS A post} → ActorM IS A [] post → Env → Env +add-top : ∀ {IS A post} → ActorM ∞ IS A [] post → Env → Env add-top {IS} {A} {post} actor-m env = record { acts = record { inbox-shape = IS @@ -276,32 +261,33 @@ add-top {IS} {A} {post} actor-m env = record ; name = fresh-name env } ∷ acts env ; blocked = blocked env - ; env-inboxes = record { inbox-shape = IS ; inbox-messages = [] ; name = fresh-name env } ∷ env-inboxes env + ; env-inboxes = [] ∷ env-inboxes env ; store = inbox# fresh-name env [ IS ] ∷ store env - ; inbs=store = cong (_∷_ inbox# fresh-name env [ IS ]) (inbs=store env) ; fresh-name = suc (fresh-name env) ; actors-valid = record { actor-has-inbox = zero ; references-have-pointer = [] } ∷ ∀map (valid-actor-suc (name-is-fresh env)) (actors-valid env) ; blocked-valid = ∀map (valid-actor-suc (name-is-fresh env)) (blocked-valid env) - ; messages-valid = [] ∷ ∀map (λ {x} vi → messages-valid-suc {_} {x} (name-is-fresh env) vi) (messages-valid env) + ; messages-valid = [] ∷ map-suc (store env) (messages-valid env) (name-is-fresh env) ; name-is-fresh = Data.Nat.s≤s (≤-reflexive refl) ∷ ∀map Data.Nat.Properties.≤-step (name-is-fresh env) } + where + map-suc : (store : Store) → {store' : Store} → {inbs : Inboxes store'} → InboxesValid store inbs → ∀ {n} → (NameFresh store n) → InboxesValid (inbox# n [ IS ] ∷ store) inbs + map-suc store [] frsh = [] + map-suc store (x ∷ valid) frsh = messages-valid-suc frsh x ∷ (map-suc store valid frsh) record GetInbox (store : Store) (S : InboxShape) : Set₂ where field - messages : List (NamedMessage S) - valid : All (message-valid store) messages + messages : Inbox S + valid : all-messages-valid store messages -- Get the messages of an inbox pointed to in the environment. -- This is just a simple lookup into the list of inboxes. get-inbox : ∀ {name IS} → (env : Env) → name ↦ IS ∈e (store env) → GetInbox (store env) IS -get-inbox env point = loop (env-inboxes env) (messages-valid env) (fix-the-point point (inbs=store env)) +get-inbox env point = loop (env-inboxes env) (messages-valid env) point where - fix-the-point : ∀ {name IS} → name ↦ IS ∈e store env → store env ≡ inboxes-to-store (env-inboxes env) → name ↦ IS ∈e inboxes-to-store (env-inboxes env) - fix-the-point p refl = p - loop : ∀ {name IS} → (inboxes : Inboxes) → All (all-messages-valid (store env)) inboxes → name ↦ IS ∈e (inboxes-to-store inboxes) → GetInbox (store env) IS - loop [] [] () - loop (x ∷ _) (px ∷ prfs) zero = record { messages = Inbox.inbox-messages x ; valid = px } - loop (_ ∷ inboxes) (_ ∷ prfs) (suc point) = loop inboxes prfs point + loop : {store store' : Store} → (inbs : Inboxes store') → InboxesValid store inbs → ∀ {name IS} → name ↦ IS ∈e store' → GetInbox store IS + loop _ [] () + loop (x ∷ _) (px ∷ _) zero = record { messages = x ; valid = px } + loop (_ ∷ inbs) (_ ∷ valid) (suc point) = loop inbs valid point -- Updates an inbox in the environment -- Just a wrapper arround 'updateInboxes' @@ -310,20 +296,16 @@ update-inbox-env : ∀ {name IS} → (env : Env) → name ↦ IS ∈e (store env update-inbox-env {name} {IS} env p f = record { acts = acts env ; blocked = blocked env - ; env-inboxes = updated-inboxes updatedInboxes + ; env-inboxes = updated-inboxes updated ; store = store env - ; inbs=store = trans (inbs=store env) (same-store updatedInboxes) ; fresh-name = fresh-name env ; actors-valid = actors-valid env ; blocked-valid = blocked-valid env - ; messages-valid = inboxes-valid updatedInboxes + ; messages-valid = inboxes-valid updated ; name-is-fresh = name-is-fresh env } where - -- Just some helpers to align the types - pp : name ↦ IS ∈e (inboxes-to-store (env-inboxes env)) - pp rewrite (inbs=store env) = p - updatedInboxes = update-inboxes (store env) (env-inboxes env) (messages-valid env) pp f + updated = update-inboxes (store env) (env-inboxes env) (messages-valid env) p f -- Move an actor from the blocked list to the actors list. -- Simply looks through the names of all blocked actors and moves those (should be just 1 or 0) with the same name. @@ -346,7 +328,6 @@ unblock-actor env name = newEnv (loop (blocked env) (blocked-valid env)) ; blocked = ba ; env-inboxes = env-inboxes env ; store = store env - ; inbs=store = inbs=store env ; fresh-name = fresh-name env ; actors-valid = ++⁺ (actors-valid env) unblockedValid ; blocked-valid = baValid @@ -423,7 +404,6 @@ replace-actors env actors actorsValid = record { ; blocked = blocked env ; env-inboxes = env-inboxes env ; store = store env - ; inbs=store = inbs=store env ; fresh-name = fresh-name env ; actors-valid = actorsValid ; blocked-valid = blocked-valid env @@ -440,7 +420,6 @@ replace-actors+blocked env actors actorsValid blocked blockedValid = record { ; blocked = blocked ; env-inboxes = env-inboxes env ; store = store env - ; inbs=store = inbs=store env ; fresh-name = fresh-name env ; actors-valid = actorsValid ; blocked-valid = blockedValid @@ -458,7 +437,6 @@ add-message message valid vml = record { inbox = inbox vml ++ (message ∷ []) ; remove-message : {S : InboxShape} → {store : Store} → (ValidMessageList store S → ValidMessageList store S) remove-message vml = record { inbox = drop 1 (inbox vml) ; valid = drop⁺ 1 (ValidMessageList.valid vml) } - name-fields : ∀ {MT store} → (pre : TypingContext) → (refs : List NamedInbox) → All (reference-has-pointer store) refs → @@ -479,7 +457,7 @@ unname-field {ValueType x₁} nfc = nfc unname-field {ReferenceType x₁} nfc = _ unname-message : ∀ {S} → NamedMessage S → Message S -unname-message (NamedM x fields) = Msg x (do-the-work fields) -- (∀map unname-field fields) +unname-message (NamedM x fields) = Msg x (do-the-work fields) where do-the-work : ∀ {MT} → All named-field-content MT → All receive-field-content MT do-the-work {[]} nfc = [] @@ -513,19 +491,19 @@ add-references++ msg@(NamedM {MT} x x₁) p w = halp (add-fields++ MT x₁) add-fields++ (ValueType x ∷ MT) (px ∷ x₁) = add-fields++ MT x₁ add-fields++ (ReferenceType x ∷ MT) (px ∷ x₁) = cong (_∷_ x) (add-fields++ MT x₁) -valid++ : ∀ {S store} → (nm : NamedMessage S) → message-valid store nm → ∀ w → +valid++ : ∀ {S store} → (nm : NamedMessage S) → message-valid store nm → ∀ {w} → All (reference-has-pointer store) w → All (reference-has-pointer store) (named-inboxes nm ++ w) -valid++ (NamedM x x₁) v p = valid-fields x₁ v p +valid++ (NamedM x x₁) v = valid-fields v where valid-fields : ∀ {MT store} → - (x₁ : All named-field-content MT) → - all-fields-have-pointer store x₁ → ∀ p → + {fields : All named-field-content MT} → + FieldsHavePointer store fields → ∀ {p} → All (reference-has-pointer store) p → - All (reference-has-pointer store) (extract-inboxes x₁ ++ p) - valid-fields [] h p ps = ps - valid-fields (_∷_ {ValueType x} px x₁) (_ , h) p ps = valid-fields x₁ h p ps - valid-fields (_∷_ {ReferenceType x} px x₁) (hj , h) p ps = hj ∷ (valid-fields x₁ h p ps) + All (reference-has-pointer store) (extract-inboxes fields ++ p) + valid-fields [] ps = ps + valid-fields (v+ fhp) ps = valid-fields fhp ps + valid-fields (px ∷r fhp) ps = px ∷ (valid-fields fhp ps) open _⊢>:_ @@ -544,13 +522,15 @@ make-pointer-compatible : ∀ store x refs name w comp↦ x ∈ store make-pointer-compatible store x refs px rhp w = [p: actual-has-pointer (reference w) ][handles: compatible-handles store x refs px w ] +open FieldsHavePointer + make-pointers-compatible : ∀ {MT} store pre refs (eq : map shape refs ≡ pre) (fields : All (send-field-content pre) MT) (rhp : All (reference-has-pointer store) refs) → - all-fields-have-pointer store (name-fields pre refs rhp fields eq) -make-pointers-compatible store pre refs eq [] rhp = _ -make-pointers-compatible store _ refs refl (_∷_ {ValueType x} px fields) rhp = _ , (make-pointers-compatible store _ refs refl fields rhp) -make-pointers-compatible store _ refs refl (_∷_ {ReferenceType x} px fields) rhp = make-pointer-compatible store x refs px rhp foundFw , (make-pointers-compatible store _ refs refl fields rhp) + FieldsHavePointer store (name-fields pre refs rhp fields eq) +make-pointers-compatible store pre refs eq [] rhp = [] +make-pointers-compatible store _ refs refl (_∷_ {ValueType x} px fields) rhp = v+ make-pointers-compatible store _ refs refl fields rhp +make-pointers-compatible store _ refs refl (_∷_ {ReferenceType x} px fields) rhp = (make-pointer-compatible store x refs px rhp foundFw) ∷r (make-pointers-compatible store _ refs refl fields rhp) where foundFw : FoundReference store (actual px) foundFw = lookup-reference _ refs rhp refl (actual-is-sendable px) diff --git a/src/Selective/Examples/Call.agda b/src/Selective/Examples/Call.agda index 0d08c99..2286a20 100644 --- a/src/Selective/Examples/Call.agda +++ b/src/Selective/Examples/Call.agda @@ -5,7 +5,7 @@ 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 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) @@ -26,15 +26,15 @@ call-select {IS} sub which = filter filter : MessageFilter IS filter (Msg x x₁) = call-select-unwrap x (translate-⊆ sub which) -call : ∀ {Γ MtTo MtIn} {To IS IS' : InboxShape} → (Γ ⊢ To) → +call : ∀ {Γ MtTo MtIn i} {To IS IS' : InboxShape} → (Γ ⊢ To) → ((ReferenceType IS' ∷ MtTo) ∈ To) → All (send-field-content Γ) MtTo → (ISsubs : IS' <: IS) → (whichIn : MtIn ∈ IS') → - (ActorM IS (SelectedMessage (call-select ISsubs whichIn)) Γ) (add-selected-references Γ) + ∞ActorM i IS (SelectedMessage (call-select ISsubs whichIn)) Γ (add-selected-references Γ) call {Γ} {IS = IS} var toFi vals sub whichIn = - ♯ Self >>= λ _ → - ♯ ((S var ![t: toFi ] (([ Z ]>: sub) ∷ translate-fields vals)) >>= λ _ → - ♯ ( strengthen (⊆-suc ⊆-refl) >>= λ _ → - ♯ SelectiveReceive (call-select sub whichIn))) + self >> + ((S var ![t: toFi ] (([ Z ]>: sub) ∷ (translate-fields vals))) >> + (strengthen (⊆-suc ⊆-refl) >> + selective-receive (call-select sub whichIn))) where translate-fields : ∀ {MT} → All (send-field-content Γ) MT → All (send-field-content (IS ∷ Γ)) MT translate-fields [] = [] @@ -44,24 +44,24 @@ call {Γ} {IS = IS} var toFi vals sub whichIn = Calculator : InboxShape Calculator = (ReferenceType ((ValueType ℕ ∷ []) ∷ []) ∷ ValueType ℕ ∷ ValueType ℕ ∷ []) ∷ [] -calculatorActor : ActorM Calculator (Lift ⊤) [] (λ _ → []) -calculatorActor = loop >>= return₁ - where - loop : ∞ (ActorM Calculator (Lift ⊤) [] (λ _ → [])) - loop = ♯ (receive >>= λ { - (Msg Z (_ ∷ n ∷ m ∷ [])) → ♯ ((Z ![t: Z ] ((lift (n + m)) ∷ [])) >>= λ _ → ♯ (strengthen [] >>= λ _ → loop)) - ; (Msg (S ()) x₁) - }) +calculatorActor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift ⊤) [] (λ _ → []) +calculatorActor .force = receive ∞>>= λ { + (Msg Z (_ ∷ n ∷ m ∷ [])) .force → (Z ![t: Z ] ((lift (n + m)) ∷ [])) ∞>> + (strengthen [] >> + calculatorActor) + ; (Msg (S ()) _) + } TestBox : InboxShape TestBox = ((ValueType ℕ ∷ [])) ∷ [] ∷ [] -calltestActor : ActorM TestBox (Lift ℕ) [] (λ _ → []) -calltestActor = spawn calculatorActor >>= (λ _ → - ♯ ( - (♯ (call Z Z ((lift 10) ∷ ((lift 32) ∷ []))) (Z ∷ []) Z) >>= λ x → ♯ ( strengthen [] >>= λ _ → (return-result x)))) +calltestActor : ∀{i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → []) +calltestActor .force = spawn∞ calculatorActor ∞>> + (call Z Z ((lift 10) ∷ ((lift 32) ∷ [])) (Z ∷ []) Z >>= λ x → + strengthen [] >> + return-result x) where - return-result : SelectedMessage {TestBox} (call-select (Z ∷ []) Z) → ∞ (ActorM TestBox (Lift ℕ) [] (λ _ → [])) + return-result : SelectedMessage {TestBox} (call-select (Z ∷ []) Z) → ∀ {i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → []) return-result record { msg = (Msg Z (px ∷ x₁)) } = return px return-result record { msg = (Msg (S x) x₁) ; msg-ok = () } diff --git a/src/Selective/Examples/Main-generated.agda b/src/Selective/Examples/Main-generated.agda index 11390f9..7fbd208 100644 --- a/src/Selective/Examples/Main-generated.agda +++ b/src/Selective/Examples/Main-generated.agda @@ -1,9 +1,13 @@ module Selective.Examples.Main-generated where import Selective.Examples.PingPong as PingPong +import Selective.Examples.Call as Call open import Selective.Runtime open import Selective.SimulationEnvironment +open import Selective.ActorMonad import IO +open ∞ActorM -pingpongEntry = singleton-env PingPong.spawner +pingpongEntry = singleton-env (PingPong.spawner .force) +callEntry = singleton-env (Call.calltestActor .force) -main = IO.run (run-env trace+actors-logger pingpongEntry) +main = IO.run (run-env trace+actors-logger callEntry) diff --git a/src/Selective/Examples/Main-template.agda b/src/Selective/Examples/Main-template.agda index 22fae53..ca42615 100644 --- a/src/Selective/Examples/Main-template.agda +++ b/src/Selective/Examples/Main-template.agda @@ -1,9 +1,13 @@ module Selective.Examples.Main-generated where import Selective.Examples.PingPong as PingPong +import Selective.Examples.Call as Call open import Selective.Runtime open import Selective.SimulationEnvironment +open import Selective.ActorMonad import IO +open ∞ActorM -pingpongEntry = singleton-env PingPong.spawner +pingpongEntry = singleton-env (PingPong.spawner .force) +callEntry = singleton-env (Call.calltestActor .force) main = IO.run (run-env trace+actors-logger __ENTRY__) diff --git a/src/Selective/Examples/PingPong.agda b/src/Selective/Examples/PingPong.agda index 2099257..d133793 100644 --- a/src/Selective/Examples/PingPong.agda +++ b/src/Selective/Examples/PingPong.agda @@ -5,13 +5,12 @@ 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 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 Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax) -- An example including three actors: spawner, pinger, ponger -- @@ -48,65 +47,72 @@ mutual constPingrefs : {A : Set₁} → (A → TypingContext) constPingrefs _ = PingRefs -pingMainActor : (A : Set₁) → Set₂ -pingMainActor A = ActorM Pingbox A PingRefs constPingrefs +pingMainActor : (i : Size) (A : Set₁) → Set₂ +pingMainActor i A = ∞ActorM i Pingbox A PingRefs constPingrefs mutual - pingReceive : (msg : Message Pingbox) → ∞ (ActorM Pingbox (Lift Bool) (add-references PingRefs msg) constPingrefs) + 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 : ∞ (pingMainActor (Lift Bool)) - loopTillPingValue = ♯ (receive >>= pingReceive) + loopTillPingValue : ∀ {i} → pingMainActor i (Lift Bool) + loopTillPingValue .force = receive ∞>>= pingReceive -pinger : ActorM Pingbox ⊤₁ [] constPingrefs -pinger = loopTillPong >>= (λ _ → pingMain 0) +pinger : ∀ {i} → ∞ActorM (↑ i) Pingbox ⊤₁ [] constPingrefs +pinger .force = waitForPong ∞>> pingMain 0 where - loopTillPong : ∞ (ActorM Pingbox ⊤₁ [] constPingrefs) - loopTillPong = ♯ (receive >>= ((λ - { (Msg Z x₁) → loopTillPong - ; (Msg (S Z) x₁) → return _ - ; (Msg (S (S ())) x₁) - }))) - pingMain : ℕ → ∞ (pingMainActor ⊤₁) - pingMain n = ♯ ((loopTillPingValue >>= λ - { (lift false) → ♯ ( (Z ![t: Z ] (lift n ∷ [])) >>= λ _ → pingMain (suc n)) - ; (lift true) → return _})) + waitForPong : ∀ {i} → ∞ActorM i Pingbox ⊤₁ [] constPingrefs + waitForPong = selective-receive (λ { + (Msg Z _) → false + ; (Msg (S Z) _) → true + ; (Msg (S (S ())) _) + }) >>= λ { + record { msg = (Msg Z _) ; msg-ok = () } + ; record { msg = (Msg (S Z) _) ; msg-ok = refl } → return _ + ; record { msg = (Msg (S (S ())) x₁) } + + } + pingMain : ∀ {i} → ℕ → pingMainActor i ⊤₁ + pingMain n .force = loopTillPingValue ∞>>= λ + { (lift false) → (Z ![t: Z ] (lift n ∷ [])) >> pingMain (suc n) + ; (lift true) → return _} constPongrefs : {A : Set₁} → (A → TypingContext) constPongrefs _ = PongRefs -pongMainActor : (A : Set₁) → Set₂ -pongMainActor A = ActorM Pongbox A PongRefs constPongrefs +pongMainActor : (i : Size) (A : Set₁) → Set₂ +pongMainActor i A = ∞ActorM i Pongbox A PongRefs constPongrefs mutual - pongReceive : (msg : Message Pongbox) → ∞ (ActorM Pongbox (Lift ℕ) (add-references PongRefs msg) constPongrefs) + 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 : ∞ (pongMainActor (Lift ℕ)) - loopTillPongValue = ♯ (receive >>= pongReceive) + loopTillPongValue : ∀ {i} → pongMainActor i (Lift ℕ) + loopTillPongValue .force = receive ∞>>= pongReceive -ponger : ActorM Pongbox ⊤₁ [] constPongrefs -ponger = loopTillPing >>= λ _ → ♯ ((Z ![t: Z ] ((lift false) ∷ [])) >>= λ _ → pongMain) +ponger : ∀ {i} → ∞ActorM (↑ i) Pongbox ⊤₁ [] constPongrefs +ponger .force = waitForPing ∞>> ((Z ![t: Z ] ((lift false) ∷ [])) >> pongMain) where - loopTillPing : ∞ (ActorM Pongbox ⊤₁ [] constPongrefs) - loopTillPing = ♯ (♯ SelectiveReceive (λ { - (Msg Z x₁) → false + waitForPing : ∀ {i} → ∞ActorM i Pongbox ⊤₁ [] constPongrefs + waitForPing = selective-receive (λ { + (Msg Z _) → false ; (Msg (S Z) _) → true - ; (Msg (S (S ())) _)}) >>= λ { + ; (Msg (S (S ())) _) + }) >>= λ { record { msg = (Msg Z _) ; msg-ok = () } - ; record { msg = (Msg (S Z) _) ; msg-ok = msg-ok } → return₁ _ - ; record { msg = (Msg (S (S ())) x₁) }}) - pongMain : ∞ (pongMainActor ⊤₁) - pongMain = ♯ (loopTillPongValue >>= λ - { (lift 10) → ♯ (Z ![t: Z ] ((lift true) ∷ []) >>= λ _ → return _) - ; (lift n) → ♯ (Z ![t: Z ] ((lift false) ∷ []) >>= λ _ → pongMain) - }) - --- TODO: this needs to look prettier -spawner : ActorM Spawnbox ⊤₁ [] (λ _ → Pingbox ∷ Pongbox ∷ []) -spawner = spawn ponger >>= λ _ → - ♯ (spawn pinger >>= λ _ → ♯ ((Z ![t: S Z ](([ S Z ]>: (Z ∷ [])) ∷ [])) >>= λ _ → - S Z ![t: S Z ] (([ Z ]>: (Z ∷ [])) ∷ []))) + ; record { msg = (Msg (S Z) x₁) ; msg-ok = refl } → return _ + ; record { msg = (Msg (S (S ())) x₁) } + } + pongMain : ∀ {i} → pongMainActor i ⊤₁ + pongMain .force = loopTillPongValue ∞>>= λ { + (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 ∷ [])) ∷ [])))) diff --git a/src/Selective/Runtime.agda b/src/Selective/Runtime.agda index 03ec9ad..9f5ec33 100644 --- a/src/Selective/Runtime.agda +++ b/src/Selective/Runtime.agda @@ -2,15 +2,17 @@ module Selective.Runtime where open import Selective.Simulate open import Selective.SimulationEnvironment -open import Data.Colist using (Colist ; [] ; _∷_) +open import Colist using (Colist ; ∞Colist ; [] ; _∷_) open import Data.List using (List ; _∷_ ; [] ; map ; length) 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 Coinduction using ( ♯_ ; ♭) +open import Size using (∞) import IO +open ∞Colist Logger = (ℕ → EnvStep → IO.IO ⊤) @@ -18,11 +20,11 @@ Logger = (ℕ → EnvStep → IO.IO ⊤) -- and transforms the steps taken into output to the console. -- The output can be configured by prodiving different loggers. run-env : Logger → Env → IO.IO ⊤ -run-env logger env = loop 1 (simulate env) +run-env logger env = loop 1 ((simulate env) .force) where - loop : ℕ → Colist EnvStep → IO.IO ⊤ + loop : ℕ → Colist ∞ EnvStep → IO.IO ⊤ loop n [] = IO.putStrLn ("Done after " ++ (show n) ++ " steps.") - loop n (x ∷ xs) = ♯ logger n x IO.>> ♯ loop (suc n) (♭ xs) + loop n (x ∷ xs) = ♯ logger n x IO.>> ♯ loop (suc n) (xs .force) open EnvStep open Env @@ -38,7 +40,7 @@ show-trace (Return name) = show name ++ " returned" show-trace (Bind trace) = "Bind [ " ++ show-trace trace ++ " ]" show-trace (BindDouble name) = "Bind " ++ (show name) show-trace (Spawn spawner spawned) = (show spawner) ++ " spawned " ++ (show spawned) -show-trace (Send sender receiver references) = (show sender) ++ " sent a reference to " ++ (show receiver) ++ " forwarding [" ++ showNames references ++ "]" +show-trace (Send sender receiver references) = (show sender) ++ " sent a message to " ++ (show receiver) ++ " forwarding [" ++ showNames references ++ "]" show-trace (Receive name Nothing) = (show name) ++ " received nothing. It was put in the blocked list" show-trace (Receive name (Value references)) = (show name) ++ " received a message forwarding [" ++ showNames references ++ "]" show-trace (Receive name Dropped) = (show name) ++ " received something, but had no bind. It was dropped" @@ -53,16 +55,16 @@ log-trace : Trace → IO.IO ⊤ log-trace trace = IO.putStrLn (show-trace trace ++ ".") -- Output the number of inboxes in the environment. -log-inbox-count : Inboxes → IO.IO ⊤ -log-inbox-count inboxes = IO.putStrLn ("There are " ++ (show (Data.List.length inboxes)) ++ " inboxes.") +log-inbox-count : ∀ {store} → Inboxes store → IO.IO ⊤ +log-inbox-count {store} inboxes = IO.putStrLn ("There are " ++ (show (Data.List.length store)) ++ " inboxes.") -- Output the number of messages in an inbox -log-message-counts : Inboxes → IO.IO ⊤ +log-message-counts : ∀ {store} → Inboxes store → IO.IO ⊤ log-message-counts [] = IO.return _ -log-message-counts (x ∷ xs) = ♯ IO.putStrLn ("Inbox #" ++ show (Inbox.name x) ++ " has " ++ (show (Data.List.length (Inbox.inbox-messages x))) ++ " messages.") IO.>> ♯ log-message-counts xs +log-message-counts {inbox# name [ _ ] ∷ store} (x ∷ xs) = ♯ IO.putStrLn ("Inbox #" ++ show name ++ " has " ++ (show (Data.List.length x)) ++ " messages.") IO.>> ♯ log-message-counts xs -- Output the nunmber of inboxes and how many messages are in each inbox. -log-inboxes : Inboxes → IO.IO ⊤ +log-inboxes : ∀ {store} → Inboxes store → IO.IO ⊤ log-inboxes inboxes = ♯ log-inbox-count inboxes IO.>> ♯ log-message-counts inboxes -- Output how many actors are currently running and how many actors are blocked. diff --git a/src/Selective/Simulate.agda b/src/Selective/Simulate.agda index 6a06766..2997c89 100644 --- a/src/Selective/Simulate.agda +++ b/src/Selective/Simulate.agda @@ -4,8 +4,8 @@ open import Membership using (_∈_ ; _⊆_ ; All-⊆ ; translate-⊆ ; ⊆-refl open import Selective.ActorMonad public open import Selective.SimulationEnvironment open import Selective.EnvironmentOperations +open import Colist -open import Data.Colist using (Colist ; [] ; _∷_) 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 (++⁺) @@ -17,7 +17,7 @@ open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax) open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; cong ; trans) open import Level using (Lift ; lift) renaming (suc to lsuc ; zero to lzero) -open import Coinduction using (∞ ; ♯_ ; ♭) +open import Size using (∞) data ReceiveKind : Set where Nothing : ReceiveKind @@ -42,7 +42,7 @@ record EnvStep : Set₂ where trace : Trace private - keep-simulating : Trace → Env → Colist EnvStep + keep-simulating : Trace → Env → ∞Colist ∞ EnvStep open Actor open ValidActor @@ -53,6 +53,7 @@ open UpdatedInboxes open ValidMessageList open NamedInbox open _comp↦_∈_ +open ∞Colist -- Simulates the actors running in parallel by making one step of one actor at a time. -- The actor that was run is put in the back of the queue unless it became blocked. @@ -63,10 +64,10 @@ open _comp↦_∈_ -- The behaviour of one step depends on whether there is a step coming after or if this is the -- last step for the actor, so for every constructor we need to handle the case of when the -- constructor is used in a bind or separately. -simulate : Env → Colist EnvStep +simulate : Env → ∞Colist ∞ EnvStep simulate env with (acts env) | (actors-valid env) -- ===== OUT OF ACTORS ===== -simulate env | [] | _ = [] +simulate env | [] | _ = delay [] simulate env | actor ∷ rest | _ with (actor-m actor) -- ===== Return ===== -- If an actor returns a value but there is nothing that follows, @@ -74,17 +75,17 @@ simulate env | actor ∷ rest | _ with (actor-m actor) simulate env | actor ∷ rest | _ | Return val = keep-simulating (Return (name actor)) (drop-top-actor env) -- ===== Bind ===== -simulate env | actor ∷ rest | _ | m >>= f with (♭ m) +simulate env | actor ∷ rest | _ | m ∞>>= f with (m .force) -- ===== Bind Value ===== -- return v >>= f ≡ f v, via the left identity monad law -- We keep simulating, with the monadic part of the actor replaced by the value of f applied to v. -- Recall that the precondition of a return is the same as the postcondition, -- so the available references does not change. -simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | +simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f | Return val = keep-simulating (Bind (Return (name actor))) env' where bindAct : Actor - bindAct = replace-actorM actor (♭ (f val)) + bindAct = replace-actorM actor ((f val) .force) env' : Env env' = replace-actors env (bindAct ∷ rest) (rewrap-valid-actor valid refl refl refl ∷ restValid) -- ===== Bind Bind ===== @@ -93,11 +94,11 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | -- it can be run just one step. -- The simulation will keep shifting parantheses until it eventually reaches -- a part that is not a bind inside a bind. -simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= g | - mm >>= f = keep-simulating (Bind (BindDouble (name actor))) env' +simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= g | + mm ∞>>= f = keep-simulating (Bind (BindDouble (name actor))) env' where bindAct : Actor - bindAct = replace-actorM actor (mm >>= λ x → ♯ (f x >>= g)) + bindAct = replace-actorM actor (mm ∞>>= λ x → f x >>= g) env' : Env env' = replace-actors env (bindAct ∷ rest) (rewrap-valid-actor valid refl refl refl ∷ restValid) -- ===== Bind Spawn ===== @@ -113,25 +114,21 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= g | -- -- In conclusion, the spawned actor is first added to the top of the round-robin queue -- and then moved to the back. -simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | +simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f | Spawn {NewIS} {B} {_} {postN} bm = keep-simulating (Spawn (name actor) (fresh-name env)) (top-actor-to-back env') where newStoreEntry : NamedInbox newStoreEntry = inbox# fresh-name env [ NewIS ] newStore : Store newStore = newStoreEntry ∷ store env - newInb : Inbox - newInb = record { inbox-shape = NewIS ; inbox-messages = [] ; name = fresh-name env } newAct : Actor newAct = new-actor bm (fresh-name env) newActValid : ValidActor newStore newAct newActValid = record { actor-has-inbox = zero ; references-have-pointer = [] } newIsFresh : NameFresh newStore (suc (fresh-name env)) newIsFresh = s≤s (≤-reflexive refl) ∷ ∀map ≤-step (name-is-fresh env) - newInbs=newStore : store env ≡ inboxes-to-store (env-inboxes env) → newStore ≡ inboxes-to-store (newInb ∷ env-inboxes env) - newInbs=newStore refl = refl bindAct : Actor - bindAct = add-reference actor newStoreEntry (♭ (f _)) + bindAct = add-reference actor newStoreEntry ((f _) .force) bindActValid : ValidActor newStore bindAct bindActValid = record { actor-has-inbox = suc {pr = @@ -144,15 +141,18 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | env' = record { acts = newAct ∷ bindAct ∷ rest ; blocked = blocked env - ; env-inboxes = newInb ∷ env-inboxes env + ; env-inboxes = [] ∷ env-inboxes env ; store = newStore - ; inbs=store = newInbs=newStore (inbs=store env) ; fresh-name = suc (fresh-name env) ; actors-valid = newActValid ∷ bindActValid ∷ ∀map (valid-actor-suc (name-is-fresh env)) restValid ; blocked-valid = ∀map (valid-actor-suc (name-is-fresh env)) (blocked-valid env) - ; messages-valid = [] ∷ ∀map (λ {inb} mv → messages-valid-suc {_} {inb} (name-is-fresh env) mv) (messages-valid env) + ; messages-valid = [] ∷ map-suc (store env) (messages-valid env) (name-is-fresh env) ; name-is-fresh = newIsFresh } + where + map-suc : (store : Store) → {store' : Store} → {inbs : Inboxes store'} → InboxesValid store inbs → ∀ {n} → (NameFresh store n) → InboxesValid (inbox# n [ NewIS ] ∷ store) inbs + map-suc store [] frsh = [] + map-suc store (x ∷ valid) frsh = (messages-valid-suc frsh x) ∷ (map-suc store valid frsh) -- ===== Bind send reference ===== -- Spawns a reference message and continues with (f tt). -- @@ -172,14 +172,14 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | -- Sending a message to an actor that is blocked, -- unblocks it and moves it to the actor queue. -- The unblocked actor is put in the back of the round-robin queue. -simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | +simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f | Send {ToIS = ToIS} canSendTo (SendM p fields) = keep-simulating (Bind (Send (name actor) (name foundTo) (reference-names namedFields))) withUnblocked where foundTo : FoundReference (store env) ToIS foundTo = lookup-reference-act valid canSendTo namedFields = name-fields-act (store env) actor fields valid bindAct : Actor - bindAct = replace-actorM actor (♭ (f _)) + bindAct = replace-actorM actor ((f _) .force) withM : Env withM = replace-actors env (bindAct ∷ rest) (rewrap-valid-actor valid refl refl refl ∷ restValid) withUpdatedInbox : Env @@ -200,14 +200,12 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | -- * If the next message is a value, just continue with (f message) -- * If the next message is a reference, -- take the proof that the message is valid and use that to prove that the added reference is valid. -simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | +simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f | Receive = keep-simulating (Bind (Receive (name actor) (receiveKind (GetInbox.messages actorsInbox)))) (env' actorsInbox) where actorsInbox : GetInbox (store env) (inbox-shape actor) actorsInbox = get-inbox env (actor-has-inbox valid) - actorsPointer : (inboxes-to-store (env-inboxes env) ≡ store env) → (name actor) ↦ (inbox-shape actor) ∈e inboxes-to-store (env-inboxes env) - actorsPointer refl = actor-has-inbox valid - inboxesAfter = update-inboxes (store env) (env-inboxes env) (messages-valid env) (actorsPointer (sym (inbs=store env))) remove-message + inboxesAfter = update-inboxes (store env) (env-inboxes env) (messages-valid env) (actor-has-inbox valid) remove-message receiveKind : List (NamedMessage (inbox-shape actor)) → ReceiveKind receiveKind [] = Nothing receiveKind (NamedM _ ps ∷ xs) = Value (reference-names ps) @@ -216,68 +214,75 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | rest restValid (actor ∷ blocked env) (valid ∷ blocked-valid env) env' record { messages = (nm ∷ messages) ; valid = nmv ∷ vmsg } = record - { acts = add-references-rewrite actor (named-inboxes nm) {unname-message nm} (add-references++ nm nmv (pre actor) ) (♭ (f (unname-message nm))) ∷ rest + { acts = add-references-rewrite actor (named-inboxes nm) {unname-message nm} (add-references++ nm nmv (pre actor) ) ((f (unname-message nm) .force)) ∷ rest ; blocked = blocked env ; env-inboxes = updated-inboxes inboxesAfter ; store = store env - ; inbs=store = trans (inbs=store env) (same-store inboxesAfter) ; actors-valid = record { actor-has-inbox = actor-has-inbox valid - ; references-have-pointer = valid++ nm nmv (references actor) (references-have-pointer valid) } ∷ restValid + ; references-have-pointer = valid++ nm nmv (references-have-pointer valid) } ∷ restValid ; blocked-valid = blocked-valid env ; messages-valid = inboxes-valid inboxesAfter ; fresh-name = fresh-name env ; name-is-fresh = name-is-fresh env } -simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | +simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f | SelectiveReceive filter = keep-simulating (Bind (Selective (name actor) (receiveKind selectedMessage))) (env' selectedMessage) where actorsInbox : GetInbox (store env) (inbox-shape actor) actorsInbox = get-inbox env (actor-has-inbox valid) - actorsPointer : (inboxes-to-store (env-inboxes env) ≡ store env) → (name actor) ↦ (inbox-shape actor) ∈e inboxes-to-store (env-inboxes env) - actorsPointer refl = actor-has-inbox valid selectedMessage : FoundInList (GetInbox.messages actorsInbox) (λ x → filter (unname-message x)) selectedMessage = find-split (GetInbox.messages actorsInbox) λ x → filter (unname-message x) - inboxesAfter = update-inboxes (store env) (env-inboxes env) (messages-valid env) (actorsPointer (sym (inbs=store env))) (remove-found-message filter) + inboxesAfter = update-inboxes (store env) (env-inboxes env) + (messages-valid env) (actor-has-inbox valid) + (remove-found-message filter) receiveKind : FoundInList (GetInbox.messages actorsInbox) (λ x → filter (unname-message x)) → ReceiveKind receiveKind (Found split x) = Value (reference-names (Σ.proj₂ (named-message-fields (el split)))) where open SplitList receiveKind Nothing = Nothing env' : FoundInList (GetInbox.messages actorsInbox) (λ x → filter (unname-message x)) → Env env' Nothing = replace-actors+blocked env - rest restValid - (actor ∷ blocked env) (valid ∷ blocked-valid env) - env' (Found split x ) = record - { acts = add-references-rewrite actor (named-inboxes (SplitList.el split)) {unname-message (SplitList.el split)} - (add-references++ (SplitList.el split) (split-all-el (GetInbox.messages actorsInbox) (GetInbox.valid actorsInbox) split) (pre actor)) - (♭ (f (record { msg = unname-message (SplitList.el split) ; msg-ok = x }))) ∷ rest - ; blocked = blocked env - ; env-inboxes = updated-inboxes inboxesAfter - ; store = store env - ; inbs=store = trans (inbs=store env) (same-store inboxesAfter) - ; actors-valid = record { - actor-has-inbox = actor-has-inbox valid - ; references-have-pointer = valid++ (SplitList.el split) - (split-all-el (GetInbox.messages actorsInbox) (GetInbox.valid actorsInbox) split) (references actor) (references-have-pointer valid) - } ∷ restValid - ; blocked-valid = blocked-valid env - ; messages-valid = inboxes-valid inboxesAfter - ; fresh-name = fresh-name env - ; name-is-fresh = name-is-fresh env - } + rest restValid + (actor ∷ blocked env) (valid ∷ blocked-valid env) + env' (Found split x) = record + { acts = add-references-rewrite actor (named-inboxes (SplitList.el split)) + {unname-message (SplitList.el split)} + (add-references++ (SplitList.el split) + (split-all-el + (GetInbox.messages actorsInbox) + (GetInbox.valid actorsInbox) + split) + (pre actor)) + (f (record { msg = unname-message (SplitList.el split) ; msg-ok = x }) .force) ∷ rest + ; blocked = blocked env + ; store = store env + ; env-inboxes = updated-inboxes inboxesAfter + ; actors-valid = (record { + actor-has-inbox = actor-has-inbox valid + ; references-have-pointer = valid++ (SplitList.el split) + (split-all-el (GetInbox.messages actorsInbox) + (GetInbox.valid actorsInbox) + split) + (references-have-pointer valid) + }) ∷ restValid + ; blocked-valid = blocked-valid env + ; messages-valid = inboxes-valid inboxesAfter + ; fresh-name = fresh-name env + ; name-is-fresh = name-is-fresh env + } -- ===== Bind lift ===== -- To bind a lift we just perform the lifting of the actor and rewrap it in the same bind, like so: -- ((Lift x) >>= f) ⇒ liftedX >>= f -simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | +simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f | Strengthen {ys} {xs} inc = keep-simulating (Bind (Strengthen (name actor))) env' where liftedRefs = lift-references inc (references actor) (pre-eq-refs actor) - strengthenedM : ActorM (inbox-shape actor) ⊤₁ (map shape (contained liftedRefs)) (λ _ → ys) - strengthenedM rewrite (sym (contained-eq-inboxes liftedRefs)) = Return _ + strengthenedM : ∞ActorM ∞ (inbox-shape actor) ⊤₁ (map shape (contained liftedRefs)) (λ _ → ys) + strengthenedM rewrite (sym (contained-eq-inboxes liftedRefs)) = return _ -- liftedBx : ActorM (inbox-shape actor) B (map shape (contained liftedRefs)) postX -- liftedBx rewrite (sym (contained-eq-inboxes liftedRefs)) = bx bindAct : Actor - bindAct = lift-actor actor (contained liftedRefs) refl (♯ strengthenedM >>= f) + bindAct = lift-actor actor (contained liftedRefs) refl (strengthenedM ∞>>= f) bindActValid : ValidActor (store env) bindAct bindActValid = record { actor-has-inbox = actor-has-inbox valid ; references-have-pointer = All-⊆ (subset liftedRefs) (references-have-pointer valid) } @@ -287,11 +292,11 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | -- To bind 'self' we just need to add the actors name and type to its references / precondition. -- We get the proof that the added reference is valid via (actor-has-inbox valid). -- countinues with (f tt) -simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | +simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f | Self = keep-simulating (Bind (Self (name actor))) env' where bindAct : Actor - bindAct = add-reference actor (inbox# name actor [ inbox-shape actor ]) (♭ (f _)) + bindAct = add-reference actor (inbox# name actor [ inbox-shape actor ]) ((f _) .force) bindActValid : ValidActor (store env) bindAct bindActValid = record { actor-has-inbox = actor-has-inbox valid ; references-have-pointer = [p: (actor-has-inbox valid) ][handles: ⊆-refl ] ∷ references-have-pointer valid } @@ -343,4 +348,4 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | Self = keep-simulating (Self (name actor)) (drop-top-actor env) -keep-simulating trace env = record { env = env ; trace = trace } ∷ ♯ simulate (top-actor-to-back env) +keep-simulating trace env .force = record { env = env ; trace = trace } ∷ simulate (top-actor-to-back env) diff --git a/src/Selective/SimulationEnvironment.agda b/src/Selective/SimulationEnvironment.agda index dc8e4e5..b115eab 100644 --- a/src/Selective/SimulationEnvironment.agda +++ b/src/Selective/SimulationEnvironment.agda @@ -9,6 +9,7 @@ open import Data.Nat using (ℕ ; _≟_) open import Data.Unit using (⊤ ; tt) open import Level using (Lift ; lift) +open import Size using (∞) open import Data.Empty using (⊥) open import Relation.Nullary using (Dec ; yes ; no ; ¬_) @@ -91,7 +92,7 @@ record Actor : Set₂ where pre : TypingContext pre-eq-refs : (map NamedInbox.shape references) ≡ pre post : A → TypingContext - actor-m : ActorM inbox-shape A pre post + actor-m : ActorM ∞ inbox-shape A pre post name : Name named-field-content : MessageField → Set @@ -113,16 +114,13 @@ data NamedMessage (To : InboxShape): Set₁ where named-message-fields : ∀ {To} → NamedMessage To → Σ[ MT ∈ MessageType ] All named-field-content MT named-message-fields (NamedM {MT} x x₁) = MT , x₁ --- A list of messages, wrapped up with the shape of the messages --- Each inbox is given a name, matching those for actors -record Inbox : Set₂ where - field - inbox-shape : InboxShape - inbox-messages : List (NamedMessage inbox-shape) - name : Name +Inbox : InboxShape → Set₁ +Inbox is = List (NamedMessage is) --- TODO: Naming of Store and Inboxes? -Inboxes = List Inbox +data Inboxes : (store : Store) → Set₁ where + [] : Inboxes [] + _∷_ : ∀ {store name inbox-shape} → List (NamedMessage inbox-shape) → + (inboxes : Inboxes store) → Inboxes (inbox# name [ inbox-shape ] ∷ store) -- Property that there exists an inbox of the right shape in the list of inboxes -- This is used both for proving that every actor has an inbox, @@ -148,30 +146,35 @@ record ValidActor (store : Store) (actor : Actor) : Set₂ where actor-has-inbox : has-inbox store actor references-have-pointer : all-references-have-a-pointer store actor -all-fields-have-pointer : ∀ {MT} → Store → All named-field-content MT → Set₁ -all-fields-have-pointer st [] = Lift ⊤ -all-fields-have-pointer st (_∷_ {ValueType _} _ xs) = ⊤ × all-fields-have-pointer st xs -all-fields-have-pointer st (_∷_ {ReferenceType Fw} name xs) = (name comp↦ Fw ∈ st) × all-fields-have-pointer st xs +data FieldsHavePointer (store : Store) : ∀ {MT} → All named-field-content MT → Set₁ where + [] : FieldsHavePointer store [] + v+_ : ∀ {MT A} {v : A} {nfc : All named-field-content MT} → + FieldsHavePointer store nfc → + FieldsHavePointer store {ValueType A ∷ MT} (v ∷ nfc) + _∷r_ : ∀ {name Fw MT} {nfc : All named-field-content MT} → + name comp↦ Fw ∈ store → + FieldsHavePointer store nfc → + FieldsHavePointer store {ReferenceType Fw ∷ MT} (name ∷ nfc) -- To limit references to only those that are valid for the current store, -- we have to prove that name in the message points to an inbox of the same -- type as the reference. -- Value messages are not context sensitive. message-valid : ∀ {IS} → Store → NamedMessage IS → Set₁ -message-valid store (NamedM x x₁) = all-fields-have-pointer store x₁ +message-valid store (NamedM x x₁) = FieldsHavePointer store x₁ -- An inbox is valid in a store if all its messages are valid -all-messages-valid : Store → Inbox → Set₁ -all-messages-valid store inb = All (message-valid store) (Inbox.inbox-messages inb) +all-messages-valid : ∀ {IS} → Store → Inbox IS → Set₁ +all-messages-valid store = All (message-valid store) --- A store entry is just an inbox without its messages. --- We make this distinction so that updating the messages of a store --- does not invalidate every pointer into the store. -inbox-to-store-entry : Inbox → NamedInbox -inbox-to-store-entry inb = inbox# (Inbox.name inb) [ Inbox.inbox-shape inb ] +infixr 5 _∷_ -inboxes-to-store : Inboxes → Store -inboxes-to-store = map inbox-to-store-entry +data InboxesValid (store : Store) : ∀ {store'} → Inboxes store' → Set₁ where + [] : InboxesValid store [] + _∷_ : ∀ {store' name IS} {inboxes : Inboxes store'} {inbox : Inbox IS} → + all-messages-valid store inbox → + InboxesValid store inboxes → + InboxesValid store {inbox# name [ IS ] ∷ store'} (inbox ∷ inboxes) -- A name is unused in a store if every inbox has a name that is < than the name NameFresh : Store → ℕ → Set₁ @@ -189,14 +192,13 @@ record Env : Set₂ where -- actors that won't succed in taking a step, and we get a clear step-condition when there are no -- non-blocked actors left. blocked : List Actor - env-inboxes : Inboxes store : Store - inbs=store : store ≡ inboxes-to-store env-inboxes + env-inboxes : Inboxes store -- The proofs that an actor and a blocked actor is valid is actually the same proof, -- but kept in a separate list. actors-valid : All (ValidActor store) acts blocked-valid : All (ValidActor store) blocked - messages-valid : All (all-messages-valid store) env-inboxes + messages-valid : InboxesValid store env-inboxes -- In each environment we keep track of the next fresh name, -- and a proof that the name is not already used in the store. fresh-name : Name @@ -209,7 +211,6 @@ empty-env = record ; blocked = [] ; env-inboxes = [] ; store = [] - ; inbs=store = refl ; fresh-name = 0 ; actors-valid = [] ; blocked-valid = [] @@ -219,7 +220,7 @@ empty-env = record -- An environment containing a single actor. -- The actor can't have any known references -singleton-env : ∀ {IS A post} → ActorM IS A [] post → Env +singleton-env : ∀ {IS A post} → ActorM ∞ IS A [] post → Env singleton-env {IS} {A} {post} actor = record { acts = record { inbox-shape = IS @@ -232,9 +233,8 @@ singleton-env {IS} {A} {post} actor = record ; name = 0 } ∷ [] ; blocked = [] - ; env-inboxes = record { inbox-shape = IS ; inbox-messages = [] ; name = 0 } ∷ [] + ; env-inboxes = [] ∷ [] ; store = inbox# 0 [ IS ] ∷ [] - ; inbs=store = refl ; fresh-name = 1 ; actors-valid = (record { actor-has-inbox = zero ; references-have-pointer = [] }) ∷ [] ; blocked-valid = [] diff --git a/src/Simulate.agda b/src/Simulate.agda index 4532b2a..5cb0cf2 100644 --- a/src/Simulate.agda +++ b/src/Simulate.agda @@ -4,8 +4,8 @@ open import Membership using (_∈_ ; _⊆_ ; All-⊆ ; translate-⊆ ; ⊆-refl open import ActorMonad public open import SimulationEnvironment open import EnvironmentOperations +open import Colist -open import Data.Colist using (Colist ; [] ; _∷_) 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 (++⁺) @@ -17,7 +17,7 @@ open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax) open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; cong ; trans) open import Level using (Lift ; lift) renaming (suc to lsuc ; zero to lzero) -open import Coinduction using (∞ ; ♯_ ; ♭) +open import Size using (∞) data ReceiveKind : Set where Nothing : ReceiveKind @@ -41,7 +41,7 @@ record EnvStep : Set₂ where trace : Trace private - keep-simulating : Trace → Env → Colist EnvStep + keep-simulating : Trace → Env → ∞Colist ∞ EnvStep open Actor open ValidActor @@ -52,6 +52,7 @@ open UpdatedInboxes open ValidMessageList open NamedInbox open _comp↦_∈_ +open ∞Colist -- Simulates the actors running in parallel by making one step of one actor at a time. -- The actor that was run is put in the back of the queue unless it became blocked. @@ -62,10 +63,10 @@ open _comp↦_∈_ -- The behaviour of one step depends on whether there is a step coming after or if this is the -- last step for the actor, so for every constructor we need to handle the case of when the -- constructor is used in a bind or separately. -simulate : Env → Colist EnvStep +simulate : Env → ∞Colist ∞ EnvStep simulate env with (acts env) | (actors-valid env) -- ===== OUT OF ACTORS ===== -simulate env | [] | _ = [] +simulate env | [] | _ = delay [] simulate env | actor ∷ rest | _ with (actor-m actor) -- ===== Return ===== -- If an actor returns a value but there is nothing that follows, @@ -73,17 +74,17 @@ simulate env | actor ∷ rest | _ with (actor-m actor) simulate env | actor ∷ rest | _ | Return val = keep-simulating (Return (name actor)) (drop-top-actor env) -- ===== Bind ===== -simulate env | actor ∷ rest | _ | m >>= f with (♭ m) +simulate env | actor ∷ rest | _ | m ∞>>= f with (m .force) -- ===== Bind Value ===== -- return v >>= f ≡ f v, via the left identity monad law -- We keep simulating, with the monadic part of the actor replaced by the value of f applied to v. -- Recall that the precondition of a return is the same as the postcondition, -- so the available references does not change. -simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | +simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f | Return val = keep-simulating (Bind (Return (name actor))) env' where bindAct : Actor - bindAct = replace-actorM actor (♭ (f val)) + bindAct = replace-actorM actor ((f val) .force) env' : Env env' = replace-actors env (bindAct ∷ rest) (rewrap-valid-actor valid refl refl refl ∷ restValid) -- ===== Bind Bind ===== @@ -92,11 +93,11 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | -- it can be run just one step. -- The simulation will keep shifting parantheses until it eventually reaches -- a part that is not a bind inside a bind. -simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= g | - mm >>= f = keep-simulating (Bind (BindDouble (name actor))) env' +simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= g | + mm ∞>>= f = keep-simulating (Bind (BindDouble (name actor))) env' where bindAct : Actor - bindAct = replace-actorM actor (mm >>= λ x → ♯ (f x >>= g)) + bindAct = replace-actorM actor (mm ∞>>= λ x → f x >>= g) env' : Env env' = replace-actors env (bindAct ∷ rest) (rewrap-valid-actor valid refl refl refl ∷ restValid) -- ===== Bind Spawn ===== @@ -112,7 +113,7 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= g | -- -- In conclusion, the spawned actor is first added to the top of the round-robin queue -- and then moved to the back. -simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | +simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f | Spawn {NewIS} {B} {_} {postN} bm = keep-simulating (Spawn (name actor) (fresh-name env)) (top-actor-to-back env') where newStoreEntry : NamedInbox @@ -126,7 +127,7 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | newIsFresh : NameFresh newStore (suc (fresh-name env)) newIsFresh = s≤s (≤-reflexive refl) ∷ ∀map ≤-step (name-is-fresh env) bindAct : Actor - bindAct = add-reference actor newStoreEntry (♭ (f _)) + bindAct = add-reference actor newStoreEntry ((f _) .force) bindActValid : ValidActor newStore bindAct bindActValid = record { actor-has-inbox = suc {pr = @@ -170,14 +171,14 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | -- Sending a message to an actor that is blocked, -- unblocks it and moves it to the actor queue. -- The unblocked actor is put in the back of the round-robin queue. -simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | +simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f | Send {ToIS = ToIS} canSendTo (SendM p fields) = keep-simulating (Bind (Send (name actor) (name foundTo) (reference-names namedFields))) withUnblocked where foundTo : FoundReference (store env) ToIS foundTo = lookup-reference-act valid canSendTo namedFields = name-fields-act (store env) actor fields valid bindAct : Actor - bindAct = replace-actorM actor (♭ (f _)) + bindAct = replace-actorM actor ((f _) .force) withM : Env withM = replace-actors env (bindAct ∷ rest) (rewrap-valid-actor valid refl refl refl ∷ restValid) withUpdatedInbox : Env @@ -198,7 +199,7 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | -- * If the next message is a value, just continue with (f message) -- * If the next message is a reference, -- take the proof that the message is valid and use that to prove that the added reference is valid. -simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | +simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f | Receive = keep-simulating (Bind (Receive (name actor) (receiveKind (GetInbox.messages actorsInbox)))) (env' actorsInbox) where actorsInbox : GetInbox (store env) (inbox-shape actor) @@ -212,7 +213,7 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | rest restValid (actor ∷ blocked env) (valid ∷ blocked-valid env) env' record { messages = (nm ∷ messages) ; valid = nmv ∷ vmsg } = record - { acts = add-references-rewrite actor (named-inboxes nm) {unname-message nm} (add-references++ nm nmv (pre actor) ) (♭ (f (unname-message nm))) ∷ rest + { acts = add-references-rewrite actor (named-inboxes nm) {unname-message nm} (add-references++ nm nmv (pre actor) ) ((f (unname-message nm) .force)) ∷ rest ; blocked = blocked env ; env-inboxes = updated-inboxes inboxesAfter ; store = store env @@ -227,16 +228,16 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | -- ===== Bind lift ===== -- To bind a lift we just perform the lifting of the actor and rewrap it in the same bind, like so: -- ((Lift x) >>= f) ⇒ liftedX >>= f -simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | +simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f | Strengthen {ys} {xs} inc = keep-simulating (Bind (Strengthen (name actor))) env' where liftedRefs = lift-references inc (references actor) (pre-eq-refs actor) - strengthenedM : ActorM (inbox-shape actor) ⊤₁ (map shape (contained liftedRefs)) (λ _ → ys) - strengthenedM rewrite (sym (contained-eq-inboxes liftedRefs)) = Return _ + strengthenedM : ∞ActorM ∞ (inbox-shape actor) ⊤₁ (map shape (contained liftedRefs)) (λ _ → ys) + strengthenedM rewrite (sym (contained-eq-inboxes liftedRefs)) = return _ -- liftedBx : ActorM (inbox-shape actor) B (map shape (contained liftedRefs)) postX -- liftedBx rewrite (sym (contained-eq-inboxes liftedRefs)) = bx bindAct : Actor - bindAct = lift-actor actor (contained liftedRefs) refl (♯ strengthenedM >>= f) + bindAct = lift-actor actor (contained liftedRefs) refl (strengthenedM ∞>>= f) bindActValid : ValidActor (store env) bindAct bindActValid = record { actor-has-inbox = actor-has-inbox valid ; references-have-pointer = All-⊆ (subset liftedRefs) (references-have-pointer valid) } @@ -246,11 +247,11 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | -- To bind 'self' we just need to add the actors name and type to its references / precondition. -- We get the proof that the added reference is valid via (actor-has-inbox valid). -- countinues with (f tt) -simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f | +simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f | Self = keep-simulating (Bind (Self (name actor))) env' where bindAct : Actor - bindAct = add-reference actor (inbox# name actor [ inbox-shape actor ]) (♭ (f _)) + bindAct = add-reference actor (inbox# name actor [ inbox-shape actor ]) ((f _) .force) bindActValid : ValidActor (store env) bindAct bindActValid = record { actor-has-inbox = actor-has-inbox valid ; references-have-pointer = [p: (actor-has-inbox valid) ][handles: ⊆-refl ] ∷ references-have-pointer valid } @@ -300,4 +301,4 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | Self = keep-simulating (Self (name actor)) (drop-top-actor env) -keep-simulating trace env = record { env = env ; trace = trace } ∷ ♯ simulate (top-actor-to-back env) +keep-simulating trace env .force = record { env = env ; trace = trace } ∷ simulate (top-actor-to-back env) diff --git a/src/SimulationEnvironment.agda b/src/SimulationEnvironment.agda index 63a5f9c..277c98b 100644 --- a/src/SimulationEnvironment.agda +++ b/src/SimulationEnvironment.agda @@ -9,6 +9,7 @@ open import Data.Nat using (ℕ ; _≟_) open import Data.Unit using (⊤ ; tt) open import Level using (Lift ; lift) +open import Size using (∞) open import Data.Empty using (⊥) open import Relation.Nullary using (Dec ; yes ; no ; ¬_) @@ -91,7 +92,7 @@ record Actor : Set₂ where pre : TypingContext pre-eq-refs : (map NamedInbox.shape references) ≡ pre post : A → TypingContext - actor-m : ActorM inbox-shape A pre post + actor-m : ActorM ∞ inbox-shape A pre post name : Name named-field-content : MessageField → Set @@ -216,7 +217,7 @@ empty-env = record -- An environment containing a single actor. -- The actor can't have any known references -singleton-env : ∀ {IS A post} → ActorM IS A [] post → Env +singleton-env : ∀ {IS A post} → ActorM ∞ IS A [] post → Env singleton-env {IS} {A} {post} actor = record { acts = record { inbox-shape = IS