Make call literal

Zalastax · Apr 3, 2018 · bfc7225 · bfc7225
1 parent 3e722b4
commit bfc7225
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 1 deletion.
diff --git a/src/Examples/Call.agda → src/Examples/Call.lagda.tex b/src/Examples/Call.agda → src/Examples/Call.lagda.tex
@@ -1,3 +1,4 @@
+\begin{code}
 module Examples.Call where
 
 open import ActorMonad public
@@ -115,3 +116,4 @@
     return-result record { msg = (Msg Z (tag ∷ n ∷ [])) } = return n
     return-result record { msg = (Msg (S x) x₁) ; msg-ok = () }
 
+\end{code}
diff --git a/src/Selective/Examples/Call.agda → src/Selective/Examples/Call.lagda.tex b/src/Selective/Examples/Call.agda → src/Selective/Examples/Call.lagda.tex
@@ -1,3 +1,4 @@
+\begin{code}
 module Selective.Examples.Call where
 
 open import Selective.ActorMonad public
@@ -52,11 +53,18 @@
        ∞ActorM i IS
          (SelectedMessage (call-select tag ISsubs whichIn))
          Γ (add-selected-references Γ)
-call {Γ} {IS = IS} var toFi tag vals sub whichIn = do
+call {Γ} {IS = IS} var toFi tag vals sub whichIn =
+\end{code}
+%<*CallComputation>
+\begin{code}
+  do
      self
      S var ![t: toFi ] ((lift tag) ∷ ([ Z ]>: sub) ∷ (translate-fields vals))
      strengthen (⊆-suc ⊆-refl)
      selective-receive (call-select tag sub whichIn)
+\end{code}
+%</CallComputation>
+\begin{code}
   where
     translate-fields : ∀ {MT} →
                        All (send-field-content Γ) MT →
@@ -104,3 +112,4 @@
     return-result record { msg = (Msg Z (tag ∷ n ∷ [])) } = return n
     return-result record { msg = (Msg (S x) x₁) ; msg-ok = () }
 
+\end{code}