Clean up selective receive

Zalastax · Apr 2, 2018 · f3797ff · f3797ff
1 parent 5625644
commit f3797ff
Show file tree

Hide file tree

Showing 4 changed files with 359 additions and 181 deletions.
diff --git a/src/Examples/Call.agda b/src/Examples/Call.agda
@@ -65,6 +65,6 @@ calltestActor .force = spawn∞ calculatorActor ∞>>
                        return-result x
   where
     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 = () }
+    return-result record { msg = (Msg Z (px ∷ x₁)) } = return px
+    return-result record { msg = (Msg (S x) x₁) ; msg-ok = () }
 
diff --git a/src/Examples/SelectiveReceive.agda b/src/Examples/SelectiveReceive.agda