Writing

Zalastax · May 22, 2018 · 8a7b685 · 8a7b685
1 parent 62bd54c
commit 8a7b685
Show file tree

Hide file tree

Showing 4 changed files with 126 additions and 23 deletions.
diff --git a/src/Membership.lagda.tex b/src/Membership.lagda.tex
@@ -46,10 +46,19 @@
 -- find-∈ {ls = x ∷ xs} Z = x
 -- find-∈ (S px) = find-∈ px
 
-translate-⊆ : ∀ {a} {A : Set a} {ls ks : List A} {x : A} → (ls ⊆ ks) → (x ∈ ls) → (x ∈ ks)
+\end{code}
+%<*translate-sub>
+\begin{code}
+translate-⊆ : ∀ {a} {A : Set a} {ls ks : List A} {x : A} →
+              (ls ⊆ ks) →
+              (x ∈ ls) →
+              (x ∈ ks)
 translate-⊆ [] ()
 translate-⊆ (x₂ ∷ subs) Z = x₂
 translate-⊆ (x₂ ∷ subs) (S px) = translate-⊆ subs px
+\end{code}
+%</translate-sub>
+\begin{code}
 
 lookup-parallel : ∀ {a b} {A : Set a} {B : Set b} {x : A} {gss : List A} → x ∈ gss → (refs : List B) → (f : B → A) → map f refs ≡ gss → B
 lookup-parallel Z [] f ()
@@ -69,9 +78,17 @@
 translate-∈ Z (x ∷ refs) f refl = Z
 translate-∈ (S px) (x ∷ refs) f refl = S (translate-∈ px refs f refl)
 
-lookup-all : ∀ {a p} {A : Set a} {P : A → Set p} {ls : List A} {x : A} → x ∈ ls → All P ls → P x
+\end{code}
+%<*lookup-all>
+\begin{code}
+lookup-all : ∀ {a p} {A : Set a} {P : A → Set p} {ls : List A} {x : A} →
+              x ∈ ls →
+              All P ls → P x
 lookup-all Z (px ∷ pxs) = px
 lookup-all (S px) (px₁ ∷ pxs) = lookup-all px pxs
+\end{code}
+%</lookup-all>
+\begin{code}
 
 All-⊆ : ∀ {a p} {A : Set a} {P : A → Set p} {xs ys} → xs ⊆ ys → All P ys → All P xs
 All-⊆ {xs = []} {ys} subs pys = []

diff --git a/src/Selective/Libraries/ActiveObjects.agda → ...lective/Libraries/ActiveObjects.lagda.tex b/src/Selective/Libraries/ActiveObjects.agda → ...lective/Libraries/ActiveObjects.lagda.tex
@@ -1,3 +1,4 @@
+\begin{code}
 module Selective.Libraries.ActiveObjects where
 
 open import Selective.Libraries.Channel public
@@ -225,3 +226,4 @@
   handle-active-method ac m state ∞>>= λ state' →
   run-active-object ac state'
   }
+\end{code}
diff --git a/src/Selective/Libraries/Call2.agda → src/Selective/Libraries/Call2.lagda.tex b/src/Selective/Libraries/Call2.agda → src/Selective/Libraries/Call2.lagda.tex
@@ -1,3 +1,5 @@
+\begin{code}
+
 module Selective.Libraries.Call2 where
 
 open import Selective.Libraries.Channel public
@@ -6,10 +8,18 @@
 open ChannelType
 open ChannelInitiation
 
+\end{code}
+%<*call>
+\begin{code}
 call : ∀ {Γ i caller} →
-        ∀ protocol →
+        (protocol : ChannelInitiation) →
         Request Γ caller protocol →
-        ∞ActorM i caller (Message (protocol .response .channel-shape)) Γ (add-references Γ)
+        ∞ActorM
+          i
+          caller
+          (Message (protocol .response .channel-shape))
+          Γ
+          (add-references Γ)
 call protocol request =
   let
     open ChannelInitiationSession
@@ -19,3 +29,5 @@
     initiate-channel _ request
     let rs = request .session .response-session
     from-channel (protocol .response) rs
+\end{code}
+%</call>
diff --git a/src/Selective/Libraries/Channel.agda → src/Selective/Libraries/Channel.lagda.tex b/src/Selective/Libraries/Channel.agda → src/Selective/Libraries/Channel.lagda.tex
@@ -1,8 +1,12 @@
+\begin{code}
 module Selective.Libraries.Channel where
 
 open import Selective.ActorMonad public
 open import Prelude
 
+\end{code}
+%<*ChannelType>
+\begin{code}
 UniqueTag = ℕ
 TagField = ValueType UniqueTag
 
@@ -13,13 +17,24 @@
   field
     channel-shape : InboxShape
     all-tagged : All IsChannelMessage channel-shape
+\end{code}
+%</ChannelType>
+\begin{code}
 
 open ChannelType
 
-record ChannelSession (channel : ChannelType) (receiver : InboxShape): Set₁ where
+\end{code}
+%<*ChannelSession>
+\begin{code}
+record ChannelSession
+        (channel : ChannelType)
+        (receiver : InboxShape): Set₁ where
   field
     can-receive : (channel .channel-shape) <: receiver
     tag : UniqueTag
+\end{code}
+%</ChannelSession>
+\begin{code}
 
 record ChannelCandidate (channel-shape receiver : InboxShape) : Set₁ where
   field
@@ -136,10 +151,20 @@
   candidates = channel-candidates (ct .all-tagged) (session .can-receive)
     in convert-response-unwrapped (session .tag) x fields candidates msg-ok
 
+\end{code}
+%<*from-channel>
+\begin{code}
 from-channel : ∀ {Γ i receiver} →
                ∀ ct →
                ChannelSession ct receiver →
-               ∞ActorM i receiver (Message (ct .channel-shape)) Γ (add-references Γ)
+               ∞ActorM i
+                receiver
+                (Message (ct .channel-shape))
+                Γ
+                (add-references Γ)
+\end{code}
+%</from-channel>
+\begin{code}
 from-channel ct cs =
   let
     open ChannelType
@@ -150,41 +175,76 @@
     let record { accepted-which = aw ; fields = fields } = convert-response {session = cs} m
     return₁ (Msg {MT = msg .MT} aw fields)
 
-
+\end{code}
+%<*ChannelInitiation>
+\begin{code}
 data IsRequestMessage (IS : InboxShape) : MessageType → Set₁ where
-  HasTag+Ref : ∀ MT → IsRequestMessage IS (TagField ∷ ReferenceType IS ∷ MT)
+  HasTag+Ref :
+    ∀ MT →
+    IsRequestMessage IS (TagField ∷ ReferenceType IS ∷ MT)
 
 record ChannelInitiation : Set₁ where
   field
     request : InboxShape
     response : ChannelType
-    request-tagged : All (IsRequestMessage (response .channel-shape)) request
-
+    request-tagged : All 
+                      (IsRequestMessage (response .channel-shape))
+                      request
+\end{code}
+%</ChannelInitiation>
+\begin{code}
 open ChannelInitiation
 
-record ChannelInitiationSession (ci : ChannelInitiation) (caller callee : InboxShape): Set₁ where
+\end{code}
+%<*ChannelInitiationSession>
+\begin{code}
+record ChannelInitiationSession
+        (ci : ChannelInitiation)
+        (caller callee : InboxShape): Set₁ where
   field
     can-request : (ci .request) <: callee
     response-session : ChannelSession (ci .response) caller
-
-extra-fields-shape : ∀ {IS Mt} → IsRequestMessage IS Mt → MessageType
+\end{code}
+%</ChannelInitiationSession>
+%<*Request>
+\begin{code}
+extra-fields-shape : ∀ {IS Mt} →
+                      IsRequestMessage IS Mt →
+                      MessageType
 extra-fields-shape (HasTag+Ref Mt) = Mt
 
-extra-fields : ∀ {IS Mt} → (Γ : TypingContext) → IsRequestMessage IS Mt → Set₁
-extra-fields Γ irm = All (send-field-content Γ) (extra-fields-shape irm)
+extra-fields : ∀ {IS Mt} →
+                (Γ : TypingContext) →
+                IsRequestMessage IS Mt →
+                Set₁
+extra-fields Γ irm = All
+                      (send-field-content Γ)
+                      (extra-fields-shape irm)
 
-record Request (Γ : TypingContext) (caller : InboxShape) (ci : ChannelInitiation) : Set₁ where
+record Request (Γ : TypingContext)
+               (caller : InboxShape)
+               (ci : ChannelInitiation) : Set₁ where
   field
     {callee} : InboxShape
     var : Γ ⊢ callee
     {MtTo} : MessageType
     chosen-field : MtTo ∈ (ci .request)
-    fields : extra-fields Γ (lookup-all chosen-field (ci .request-tagged))
+    fields : extra-fields
+              Γ
+              (lookup-all chosen-field (ci .request-tagged))
     session : ChannelInitiationSession ci caller callee
+\end{code}
+%</Request>
+%<*initiate-channel-fields>
+\begin{code}
 
-suc-send-field-content : ∀ {Γ IS F} → send-field-content Γ F → send-field-content (IS ∷ Γ) F
+suc-send-field-content : ∀ {Γ IS F} →
+                          send-field-content Γ F →
+                          send-field-content (IS ∷ Γ) F
 suc-send-field-content {F = ValueType x} sfc = sfc
-suc-send-field-content {F = ReferenceType x} ([ actual-is-sendable ]>: actual-handles-requested) = [ S actual-is-sendable ]>: actual-handles-requested
+suc-send-field-content {F = ReferenceType x}
+  ([   actual-is-sendable ]>: actual-handles-requested) =
+   [ S actual-is-sendable ]>: actual-handles-requested
 
 initiate-channel-fields :
   ∀ {Γ caller ci} →
@@ -199,10 +259,16 @@
   let open ChannelSession
       open ChannelInitiationSession
       channel = session .response-session
-  in (lift (channel .tag)) ∷ (([ Z ]>: (channel .can-receive)) ∷ ∀map suc-send-field-content fields)
+      channel-tag = lift (channel .tag)
+      reference = [ Z ]>: (channel .can-receive)
+  in channel-tag ∷ reference ∷ ∀map suc-send-field-content fields
 
+\end{code}
+%</initiate-channel-fields>
+%<*initiate-channel>
+\begin{code}
 initiate-channel : ∀ {Γ i receiver} →
-                   ∀ ci →
+                   (ci : ChannelInitiation) →
                    Request Γ receiver ci →
                    ∞ActorM i receiver ⊤₁ Γ (λ _ → Γ)
 initiate-channel ci request =
@@ -211,6 +277,12 @@
     open ChannelInitiationSession
   in do
     self
-    let protocol-to-callee = translate-⊆ (request .session .can-request)
-    S (request .var) ![t: protocol-to-callee (request .chosen-field) ] initiate-channel-fields request
+    let
+      protocol-to-callee = translate-⊆ (request .session .can-request)
+      to = S (request .var)
+      which = protocol-to-callee (request .chosen-field)
+    to ![t: which ] initiate-channel-fields request
     strengthen (⊆-suc ⊆-refl)
+\end{code}
+%</initiate-channel>
+\begin{code}