diff --git a/src/Membership.lagda.tex b/src/Membership.lagda.tex index 74012a7..6325353 100644 --- 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} +% +\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} +% +\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 b/src/Selective/Libraries/ActiveObjects.lagda.tex similarity index 99% rename from src/Selective/Libraries/ActiveObjects.agda rename to src/Selective/Libraries/ActiveObjects.lagda.tex index dc4fd4c..fcf9e97 100644 --- a/src/Selective/Libraries/ActiveObjects.agda +++ b/src/Selective/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 b/src/Selective/Libraries/Call2.lagda.tex similarity index 60% rename from src/Selective/Libraries/Call2.agda rename to src/Selective/Libraries/Call2.lagda.tex index 96bb9e7..82f6987 100644 --- a/src/Selective/Libraries/Call2.agda +++ b/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} +% diff --git a/src/Selective/Libraries/Channel.agda b/src/Selective/Libraries/Channel.lagda.tex similarity index 75% rename from src/Selective/Libraries/Channel.agda rename to src/Selective/Libraries/Channel.lagda.tex index a31bbf4..cb7e18c 100644 --- a/src/Selective/Libraries/Channel.agda +++ b/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} +% +\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} +% +\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} +% +\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} +% +\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} +% +%<*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} +% +%<*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> +\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} +% +\begin{code}