From 81ca18206da14bd73c65d1a5b49905608e304216 Mon Sep 17 00:00:00 2001 From: Pierre Krafft Date: Thu, 17 May 2018 22:10:29 +0200 Subject: [PATCH] Writing + improve found in list --- src/Examples/SelectiveReceive.lagda.tex | 23 +++++--- src/Selective/ActorMonad.lagda.tex | 19 +++---- src/Selective/Simulate.agda | 14 ++--- ...t.agda => SimulationEnvironment.lagda.tex} | 52 +++++++++++++++---- 4 files changed, 74 insertions(+), 34 deletions(-) rename src/Selective/{SimulationEnvironment.agda => SimulationEnvironment.lagda.tex} (94%) diff --git a/src/Examples/SelectiveReceive.lagda.tex b/src/Examples/SelectiveReceive.lagda.tex index f3187df..4f0db24 100644 --- a/src/Examples/SelectiveReceive.lagda.tex +++ b/src/Examples/SelectiveReceive.lagda.tex @@ -17,19 +17,28 @@ tails : List A is-ls : (heads) ++ (el ∷ tails) ≡ ls +matches-filter : ∀{a} {A : Set a} → (f : A → Bool) → A → Set +matches-filter f v = f v ≡ true + +misses-filter : ∀{a} {A : Set a} → (f : A → Bool) → A → Set +misses-filter f v = f v ≡ false + data FoundInList {a : Level} {A : Set a} - (ls : List A) (f : A → Bool) : Set (lsuc a) where + (ls : List A) + (f : A → Bool) : + Set (lsuc a) where Found : (split : SplitList ls) → - (f (SplitList.el split) ≡ true) → + (matches-filter f (SplitList.el split)) → FoundInList ls f - Nothing : FoundInList ls f + Nothing : All (misses-filter f) ls → + FoundInList ls f find-split : {a : Level} {A : Set a} (ls : List A) (f : A → Bool) → FoundInList ls f -find-split [] f = Nothing +find-split [] f = Nothing [] find-split (x ∷ ls) f with (f x) | (inspect f x) -... | false | p = add-x (find-split ls f) +... | false | [ neq ] = add-x (find-split ls f) where add-x : FoundInList ls f → FoundInList (x ∷ ls) f add-x (Found split el-is-ok) = Found (record { @@ -39,7 +48,7 @@ ; is-ls = cong (_∷_ x) (is-ls split) }) el-is-ok where open SplitList - add-x Nothing = Nothing + add-x (Nothing ps) = Nothing (neq ∷ ps) ... | true | [ eq ] = Found (record { heads = [] ; el = x @@ -199,7 +208,7 @@ ; msg-ok = x ; waiting = (heads split) ++ (tails split) }) - case-of-find Nothing .force = + case-of-find (Nothing ps) .force = receive ∞>>= handle-receive where diff --git a/src/Selective/ActorMonad.lagda.tex b/src/Selective/ActorMonad.lagda.tex index 550456a..eb91dfb 100644 --- a/src/Selective/ActorMonad.lagda.tex +++ b/src/Selective/ActorMonad.lagda.tex @@ -48,6 +48,8 @@ received-message-type : MT ∈ To received-fields : All receive-field-content MT +open Message + extract-references : MessageType → ReferenceTypes extract-references [] = [] extract-references (ValueType x ∷ mt) = extract-references mt @@ -57,9 +59,7 @@ add-references-static Γ MT = extract-references MT ++ Γ add-references : ∀ {To} → TypingContext → Message To → TypingContext -add-references Γ msg = - let open Message - in add-references-static Γ (msg .MT) +add-references Γ msg = add-references-static Γ (msg .MT) \end{code} %<*MessageFilter> @@ -73,6 +73,7 @@ \begin{code} record SelectedMessage {IS : InboxShape} (f : MessageFilter IS) : Set₁ where + constructor sm:_[_] field msg : Message IS msg-ok : f msg ≡ true @@ -81,14 +82,10 @@ %<*SelectedMessageAddReferences> \begin{code} - -selected-type : ∀ {IS} - {filter : MessageFilter IS} → - SelectedMessage filter → - MessageType -selected-type record {msg = msg } = - let open Message - in msg .MT +selected-type : ∀ {IS} {filter : MessageFilter IS} → + SelectedMessage filter → + MessageType +selected-type sm: msg [ msg-ok ] = msg .MT add-selected-references : TypingContext → ∀ {IS} {filter : MessageFilter IS} → diff --git a/src/Selective/Simulate.agda b/src/Selective/Simulate.agda index 3cf6d18..a9b4a95 100644 --- a/src/Selective/Simulate.agda +++ b/src/Selective/Simulate.agda @@ -242,17 +242,18 @@ reduce-selective-with-message : {act : Actor} → (env : Env) → Focus act env reduce-selective-with-message env@record { acts = actor@record { computation = SelectiveReceive filter ⟶ cont } ∷ rest ; actors-valid = actor-valid ∷ rest-valid - } Focused AtSelective point inb amv ifa (HasMessage {split = split} {ok}) = + } Focused AtSelective point inb amv ifa (HasMessage split ok) = let updated = update-inbox (env .store) (env .env-inboxes) (env .messages-valid) (actor-valid .actor-has-inbox) (remove-found-message filter) unblock-split = unblock-actors updated (env .blocked) (env .blocked-valid) (env .blocked-no-progress) - received-nm = SplitList.el split + open SplitList + received-nm = split .el added-references = named-inboxes received-nm received-message = unname-message received-nm received-valid : message-valid (env .store) received-nm received-valid = split-all-el inb amv split adds-correct-references : map shape added-references ++ (actor .pre) ≡ add-references (actor .pre) received-message adds-correct-references = add-references++ received-nm received-valid (actor .pre) - new-continuation = Return (record { msg = received-message ; msg-ok = ok }) ⟶ cont + new-continuation = Return sm: received-message [ ok ] ⟶ cont act' : Actor act' = add-references-rewrite actor added-references {received-message} adds-correct-references new-continuation act-valid' : ValidActor (env .store) act' @@ -277,8 +278,9 @@ reduce-selective-without-message : {act : Actor} → (env : Env) → Focus act e (aac : ActorAtConstructor Selective act) → (point : has-inbox (env .store) act) → ∀ inbox → + {ps : All (misses-filter (filter-named (selected-filter act aac))) inbox} → inbox-for-actor (env .env-inboxes) act point inbox → - InboxInFilterState {filter = filter-named (selected-filter act aac)} inbox Nothing → + InboxInFilterState inbox (Nothing ps) → Env reduce-selective-without-message env Focused AtSelective point inbox ifa iifs = block-focused env Focused (BlockedSelective AtSelective point inbox ifa iifs) @@ -295,8 +297,8 @@ reduce-selective env@record { where open GetInbox choose-reduction : (gi : GetInbox (env .store) (env .env-inboxes) (actor-valid .actor-has-inbox)) → FoundInList (gi .messages) (filter-named filter) → Env - choose-reduction gi (Found split x) = reduce-selective-with-message env Focused AtSelective _ (gi .messages) (gi .valid) (gi .right-inbox) (HasMessage {split = split} {x}) - choose-reduction gi Nothing = reduce-selective-without-message env Focused AtSelective _ (gi .messages) (gi .right-inbox) IsEmpty + choose-reduction gi (Found split x) = reduce-selective-with-message env Focused AtSelective _ (gi .messages) (gi .valid) (gi .right-inbox) (HasMessage split x) + choose-reduction gi (Nothing ps) = reduce-selective-without-message env Focused AtSelective _ (gi .messages) (gi .right-inbox) (IsEmpty ps) reduce-strengthen : {act : Actor} → (env : Env) → Focus act env → ActorAtConstructor Strengthen act → diff --git a/src/Selective/SimulationEnvironment.agda b/src/Selective/SimulationEnvironment.lagda.tex similarity index 94% rename from src/Selective/SimulationEnvironment.agda rename to src/Selective/SimulationEnvironment.lagda.tex index a4d853d..03286bf 100644 --- a/src/Selective/SimulationEnvironment.agda +++ b/src/Selective/SimulationEnvironment.lagda.tex @@ -1,3 +1,4 @@ +\begin{code} module Selective.SimulationEnvironment where open import Selective.ActorMonad open import Prelude @@ -441,26 +442,47 @@ ; name = name }) +\end{code} +%<*SplitList> +\begin{code} record SplitList {a : Level} {A : Set a} (ls : List A) : Set (lsuc a) where field heads : List A el : A tails : List A is-ls : (heads) ++ (el ∷ tails) ≡ ls - -data FoundInList {a : Level} {A : Set a} (ls : List A) (f : A → Bool) : Set (lsuc a) where - Found : (split : SplitList ls) → (f (SplitList.el split) ≡ true) → FoundInList ls f - Nothing : FoundInList ls f +\end{code} +% +%<*FoundInList> +\begin{code} +matches-filter : ∀{a} {A : Set a} → (f : A → Bool) → A → Set +matches-filter f v = f v ≡ true + +misses-filter : ∀{a} {A : Set a} → (f : A → Bool) → A → Set +misses-filter f v = f v ≡ false + +data FoundInList {a : Level} {A : Set a} + (ls : List A) + (f : A → Bool) : + Set (lsuc a) where + Found : (split : SplitList ls) → + (matches-filter f (SplitList.el split)) → + FoundInList ls f + Nothing : All (misses-filter f) ls → + FoundInList ls f +\end{code} +% +\begin{code} find-split : {a : Level} {A : Set a} (ls : List A) (f : A → Bool) → FoundInList ls f -find-split [] f = Nothing +find-split [] f = Nothing [] find-split (x ∷ ls) f with (f x) | (inspect f x) -... | false | p = add-x (find-split ls f) +... | false | [ neq ] = add-x (find-split ls f) where add-x : FoundInList ls f → FoundInList (x ∷ ls) f add-x (Found split x₁) = Found (record { heads = x ∷ heads split ; el = el split ; tails = tails split ; is-ls = cong (_∷_ x) (is-ls split) }) x₁ where open SplitList - add-x Nothing = Nothing + add-x (Nothing ps) = Nothing (neq ∷ ps) ... | true | [ eq ] = Found (record { heads = [] ; el = x ; tails = ls ; is-ls = refl }) eq split-all-el : ∀ {a p} {A : Set a} {P : A → Set p} (ls : List A) → All P ls → (sl : SplitList ls) → (P (SplitList.el sl)) @@ -478,8 +500,8 @@ HasMessage : {nm : NamedMessage S} {rest : Inbox S} → InboxInState NonEmpty (nm ∷ rest) data InboxInFilterState {S : InboxShape} {filter : NamedMessage S → Bool} (inbox : Inbox S) : FoundInList inbox filter → Set₁ where - IsEmpty : InboxInFilterState inbox Nothing - HasMessage : {split : SplitList inbox} {p : filter (SplitList.el split) ≡ true} → InboxInFilterState inbox (Found split p) + IsEmpty : ∀ ps → InboxInFilterState inbox (Nothing ps) + HasMessage : (split : SplitList inbox) (p : filter (SplitList.el split) ≡ true) → InboxInFilterState inbox (Found split p) selected-filter : ∀ actor → ActorAtConstructor Selective actor → MessageFilter (Actor.inbox-shape actor) selected-filter record { computation = SelectiveReceive filter ⟶ _ } AtSelective = filter @@ -494,13 +516,22 @@ (p : has-inbox store actor) → InboxForPointer [] store inbs p → IsBlocked store inbs actor +\end{code} +%<*BlockedSelective> +\begin{code} BlockedSelective : (aac : ActorAtConstructor Selective actor) → (point : has-inbox store actor) → ∀ inbox → + {ps : All + (misses-filter (filter-named (selected-filter actor aac))) + inbox} → InboxForPointer inbox store inbs point → - InboxInFilterState {filter = filter-named (selected-filter actor aac)} inbox Nothing → + InboxInFilterState inbox (Nothing ps) → IsBlocked store inbs actor +\end{code} +% +\begin{code} -- The environment is a list of actors and inboxes, -- with a proof that every ector is valid in the context of said list of inboxes @@ -602,3 +633,4 @@ ; messages-valid = mv ; blocked-no-progress = bib }) +\end{code}