Writing + improve found in list

Zalastax · May 17, 2018 · 81ca182 · 81ca182
1 parent 97b2219
commit 81ca182
Show file tree

Hide file tree

Showing 4 changed files with 74 additions and 34 deletions.
diff --git 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
@@ -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
@@ -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 → ...Selective/SimulationEnvironment.lagda.tex b/src/Selective/SimulationEnvironment.agda → ...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}
+%</SplitList>
+%<*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}
+%</FoundInList>
+\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}
+%</BlockedSelective>
+\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}