From 8528e93ee32c6e378e603c896a1b88078109cf9f Mon Sep 17 00:00:00 2001 From: Pierre Krafft Date: Thu, 24 May 2018 14:20:01 +0200 Subject: [PATCH] Writing --- src/ActorMonad.lagda.tex | 8 +- src/Selective/Examples/ChatAO.agda | 24 ++- src/Selective/Examples/TestAO.agda | 8 +- .../Libraries/ActiveObjects.lagda.tex | 204 ++++++++++++++---- 4 files changed, 185 insertions(+), 59 deletions(-) diff --git a/src/ActorMonad.lagda.tex b/src/ActorMonad.lagda.tex index 4cecef2..b0bc567 100644 --- a/src/ActorMonad.lagda.tex +++ b/src/ActorMonad.lagda.tex @@ -144,7 +144,7 @@ S <: T \quad inbox : \overrightarrow{T} \quad name \mapsto inbox \\ \hline \operatorname{Reference}(name) : S -\end{array} +\end{array} \] The desire to statically check that references are well-typed has affected the design of \ourlang a lot. @@ -223,7 +223,8 @@ where $Γ ⊢>: T$ says that T is a subtype of some type in Γ. \begin{code} -record _⊢>:_ (Γ : TypingContext) (requested : InboxShape) : Set₁ where +record _⊢>:_ (Γ : TypingContext) + (requested : InboxShape) : Set₁ where constructor [_]>:_ field {actual} : InboxShape @@ -265,7 +266,8 @@ send-field-content Γ (ValueType A) = Lift A send-field-content Γ (ReferenceType requested) = Γ ⊢>: requested -record SendMessage (To : InboxShape) (Γ : TypingContext) : Set₁ where +record SendMessage (To : InboxShape) + (Γ : TypingContext) : Set₁ where constructor SendM field {MT} : MessageType diff --git a/src/Selective/Examples/ChatAO.agda b/src/Selective/Examples/ChatAO.agda index cbf599b..baaf77f 100644 --- a/src/Selective/Examples/ChatAO.agda +++ b/src/Selective/Examples/ChatAO.agda @@ -294,7 +294,7 @@ room-manager-methods = join-room-header ∷ create-room-header ∷ [ list-rooms- room-manager-inbox = methods-shape room-manager-methods list-rooms : active-method room-manager-inbox RoomManagerState rms-to-context list-rooms-header -list-rooms _ _ msg state = +list-rooms _ msg state = let open RoomManagerState in return₁ (record { @@ -320,14 +320,20 @@ lookup-room rms name = loop (x ∷ Γ) rl = RawMonad._>>=_ Maybe.monad (loop Γ rl) (λ p → just (S p)) create-room : active-method room-manager-inbox RoomManagerState rms-to-context create-room-header -create-room _ _ (Msg Z (room-name ∷ [])) state = do +create-room _ input@(_ sent Msg Z (room-name ∷ [])) state = do p ← lookup-room state room-name handle-create-room p where - handle-create-room : ∀ {i IS} → Maybe ( (IS ∷ rms-to-context state) ⊢ room-inbox) → - ∞ActorM i room-manager-inbox (ActiveReply create-room-ci RoomManagerState rms-to-context (Msg Z (room-name ∷ [])) IS) - (IS ∷ rms-to-context state) - (reply-vars rms-to-context (Msg Z (room-name ∷ [])) IS) + open ResponseInput + return-type = ActiveReply create-room-ci RoomManagerState rms-to-context input + precondition = reply-state-vars rms-to-context input state + postcondition = reply-vars rms-to-context input + handle-create-room : ∀ {i} → Maybe (precondition ⊢ room-inbox) → + ∞ActorM i + room-manager-inbox + return-type + precondition + postcondition handle-create-room (just x) = return₁ (record { new-state = state ; reply = SendM Z ((lift (CR-EXISTS room-name)) ∷ []) }) handle-create-room nothing = do spawn∞ (run-active-object room (record { clients = [] })) @@ -337,7 +343,7 @@ create-room _ _ (Msg Z (room-name ∷ [])) state = do state' = record { rooms = room-name ∷ state .rooms} strengthen ((S Z) ∷ (Z ∷ (⊆-suc (⊆-suc ⊆-refl)))) return₁ (record { new-state = state' ; reply = SendM Z ((lift (CR-SUCCESS room-name)) ∷ []) }) -create-room _ _ (Msg (S ()) _) _ +create-room _ (_ sent Msg (S ()) _) _ join-room : active-method room-manager-inbox RoomManagerState rms-to-context join-room-header join-room _ (Msg Z (tag ∷ _ ∷ room-name ∷ client-name ∷ [])) state = do @@ -377,8 +383,8 @@ room-supervisor-methods = [ get-room-manager-header ]ˡ rs-inbox = methods-shape room-supervisor-methods get-room-manager-handler : active-method rs-inbox ⊤₁ rs-vars get-room-manager-header -get-room-manager-handler _ _ (Msg Z received-fields) _ = return₁ (record { new-state = _ ; reply = SendM Z [ [ (S Z) ]>: ⊆-refl ]ᵃ }) -get-room-manager-handler _ _ (Msg (S ()) _) _ +get-room-manager-handler _ (_ sent Msg Z received-fields) _ = return₁ (record { new-state = _ ; reply = SendM Z [ [ (S Z) ]>: ⊆-refl ]ᵃ }) +get-room-manager-handler _ (_ sent Msg (S ()) _) _ room-supervisor-ao : ActiveObject room-supervisor-ao = record diff --git a/src/Selective/Examples/TestAO.agda b/src/Selective/Examples/TestAO.agda index defa9d6..75e2473 100644 --- a/src/Selective/Examples/TestAO.agda +++ b/src/Selective/Examples/TestAO.agda @@ -52,12 +52,12 @@ calculator-state-vars : ⊤₁ → TypingContext calculator-state-vars _ = [] add : (active-method calculator-inbox ⊤₁ calculator-state-vars add-method-header) -add _ _ (Msg Z (n ∷ m ∷ [])) v = return₁ (record { new-state = _ ; reply = SendM Z [ lift (n + m)]ᵃ }) -add _ _ (Msg (S ()) _) _ +add _ (_ sent Msg Z (n ∷ m ∷ [])) v = return₁ (record { new-state = _ ; reply = SendM Z [ lift (n + m)]ᵃ }) +add _ (_ sent Msg (S ()) _) _ multiply : (active-method calculator-inbox ⊤₁ (λ _ → []) multiply-method-header) -multiply _ _ (Msg Z (n ∷ m ∷ [])) v = return₁ (record { new-state = _ ; reply = SendM Z [ lift (n * m)]ᵃ }) -multiply _ _ (Msg (S ()) _) _ +multiply _ (_ sent Msg Z (n ∷ m ∷ [])) v = return₁ (record { new-state = _ ; reply = SendM Z [ lift (n * m)]ᵃ }) +multiply _ (_ sent Msg (S ()) _) _ calculator : ActiveObject calculator = record { diff --git a/src/Selective/Libraries/ActiveObjects.lagda.tex b/src/Selective/Libraries/ActiveObjects.lagda.tex index fcf9e97..f5a8fab 100644 --- a/src/Selective/Libraries/ActiveObjects.lagda.tex +++ b/src/Selective/Libraries/ActiveObjects.lagda.tex @@ -7,58 +7,156 @@ open ChannelType open ChannelInitiation +\end{code} +%<*ActiveMethod> +\begin{code} data ActiveMethod : Set₁ where VoidMethod : InboxShape → ActiveMethod ResponseMethod : ChannelInitiation → ActiveMethod +\end{code} +% +\begin{code} active-request-type : ChannelInitiation → InboxShape -active-request-type record { request = .[] ; response = response ; request-tagged = [] } = [] -active-request-type record { request = .(_ ∷ _) ; response = response ; request-tagged = (px ∷ pxs) } = - let rec = active-request-type (record { request = _ ; response = response ; request-tagged = pxs }) - in extra-fields-shape px ∷ rec +active-request-type ci = loop (ci .request-tagged) + where + open ChannelInitiation + loop : ∀ {IS} → {request : InboxShape} → All (IsRequestMessage IS) request → InboxShape + loop [] = [] + loop (px ∷ airm) = + let rec = loop airm + in extra-fields-shape px ∷ rec -state-vars : ∀ {ci} {st : Set₁} → (st → TypingContext) → Message ci → InboxShape → st → TypingContext -state-vars f input caller state = caller ∷ add-references (f state) input +\end{code} +%<*ResponseInput> +\begin{code} +record ResponseInput (ci : ChannelInitiation) : Set₁ where + constructor _sent_ + field + caller : InboxShape + msg : Message (active-request-type ci) +\end{code} +% +\begin{code} +\end{code} +%<*state-vars> +\begin{code} +state-vars : ∀ {IS} {state-type : Set₁} → + (state-type → TypingContext) → + Message IS → state-type → + TypingContext +state-vars vars input state = add-references (vars state) input +\end{code} +% +\begin{code} +reply-state-vars : ∀ {ci} {state-type : Set₁} → + (state-type → TypingContext) → + ResponseInput ci → + state-type → + TypingContext +reply-state-vars vars input state = + let open ResponseInput + in (input .caller) ∷ state-vars vars (input .msg) state active-reply-needed-fields : ∀ mt → IsChannelMessage mt → MessageType active-reply-needed-fields _ (HasTag MT) = MT active-reply-type : ChannelType → InboxShape -active-reply-type record { channel-shape = [] } = [] -active-reply-type record { channel-shape = (x ∷ xs) ; all-tagged = (px ∷ pxs) } = - let rec = active-reply-type (record { channel-shape = xs ; all-tagged = pxs }) - in active-reply-needed-fields x px ∷ rec +active-reply-type ci = loop (ci .all-tagged) + where + open ChannelType + loop : {channel-shape : InboxShape} → All IsChannelMessage channel-shape → InboxShape + loop [] = [] + loop (px ∷ aim) = + let rec = loop aim + in active-reply-needed-fields _ px ∷ rec -record ActiveReply (ci : ChannelInitiation) (state-type : Set₁) (var-f : state-type → TypingContext) (input : Message (active-request-type ci)) (caller : InboxShape) : Set₁ where +\end{code} +%<*ActiveReply> +\begin{code} +record ActiveReply (ci : ChannelInitiation) + (state-type : Set₁) + (vars : state-type → TypingContext) + (input : ResponseInput ci) : Set₁ where field new-state : state-type - reply : SendMessage (active-reply-type (ci .response)) (state-vars var-f input caller new-state) + reply : SendMessage + (active-reply-type (ci .response)) + (reply-state-vars vars input new-state) +\end{code} +% +\begin{code} -reply-vars : ∀ {st ci var-f input} → (st → TypingContext) → Message (active-request-type ci) → (caller : InboxShape) → ActiveReply ci st var-f input caller → TypingContext -reply-vars f input caller ar = state-vars f input caller (ActiveReply.new-state ar) +reply-vars : ∀ {st ci var-f input} → (st → TypingContext) → ResponseInput ci → ActiveReply ci st var-f input → TypingContext +reply-vars f input ar = reply-state-vars f input (ActiveReply.new-state ar) active-method : InboxShape → (state-type : Set₁) → (state-type → TypingContext) → ActiveMethod → Set₂ -active-method IS st var-f (VoidMethod IS') = - let input-type = Message IS' - in (i : Size) → - (input : input-type) → - (state : st) → - ∞ActorM i IS - st - (add-references (var-f state) input) - (λ state' → add-references (var-f state') input) -active-method IS st var-f (ResponseMethod ci) = - let input-type = Message (active-request-type ci) - in (i : Size) → - (caller : InboxShape) → - (input : input-type) → - (state : st) → - ∞ActorM i IS - (ActiveReply ci st var-f input caller) - (caller ∷ add-references (var-f state) input) - (reply-vars var-f input caller) +active-method IS state-type var-f (VoidMethod IS') = + let +\end{code} +%<*active-method-VoidMethod> +\begin{code} + input-type = Message IS' + + return-type : input-type → Set₁ + return-type _ = state-type + + precondition : input-type → state-type → TypingContext + precondition input state = state-vars var-f input state + postcondition : (input : input-type) → + return-type input → TypingContext + postcondition input state = state-vars var-f input state +\end{code} +% +\begin{code} + in + (i : Size) → + (input : input-type) → + (state : state-type) → + ∞ActorM i IS + (return-type input) + (precondition input state) + (postcondition input) +active-method IS state-type var-f (ResponseMethod ci) = + let + open ResponseInput +\end{code} +%<*active-method-ResponseMethod> +\begin{code} + input-type = ResponseInput ci + + return-type : input-type → Set₁ + return-type input = ActiveReply ci state-type var-f input + + precondition : input-type → state-type → TypingContext + precondition input state = reply-state-vars var-f input state + + postcondition : (input : input-type) → + return-type input → TypingContext + postcondition input = reply-vars var-f input +\end{code} +% +\begin{code} + in +\end{code} +%<*method-handler> +\begin{code} + (i : Size) → + (input : input-type) → + (state : state-type) → + ∞ActorM i IS + (return-type input) + (precondition input state) + (postcondition input) +\end{code} +% +\begin{code} + +\end{code} +%<*methods-shape> +\begin{code} active-method-request : ActiveMethod → InboxShape active-method-request (VoidMethod x) = x active-method-request (ResponseMethod x) = x .request @@ -69,14 +167,26 @@ let rec = methods-shape lci am-shape = active-method-request am in am-shape ++ rec - +\end{code} +% +%<*ActiveObject> +\begin{code} record ActiveObject : Set₂ where field state-type : Set₁ vars : state-type → TypingContext methods : List ActiveMethod extra-messages : InboxShape - handlers : All (active-method (methods-shape methods ++ extra-messages) state-type vars) methods + handlers : All + (active-method + (methods-shape methods ++ extra-messages) + state-type + vars + ) + methods +\end{code} +% +\begin{code} active-inbox-shape : ActiveObject → InboxShape active-inbox-shape ac = @@ -110,18 +220,18 @@ (ac .state-type) (add-references (ac .vars state) input) (λ x → add-references (ac .vars x) input) invoke-active-method ac (Msg x f) state = invoke f (ac .methods) (ac .handlers) x where - translate-invoke-pointer : {ci : ChannelInitiation} → + translate-invoke-pointer : (ci : ChannelInitiation) → {MT : MessageType} → (ValueType UniqueTag ∷ ReferenceType (ci .response .channel-shape) ∷ MT) ∈ ci .request → MT ∈ active-request-type ci - translate-invoke-pointer {record { request-tagged = HasTag+Ref MT ∷ _ }} Z = Z - translate-invoke-pointer {record { response = response ; request-tagged = _ ∷ rt }} (S p) = - let rec = translate-invoke-pointer {record { request = _ ; response = response ; request-tagged = rt }} p + translate-invoke-pointer record { request-tagged = HasTag+Ref MT ∷ _ } Z = Z + translate-invoke-pointer record { response = response ; request-tagged = _ ∷ rt } (S p) = + let rec = translate-invoke-pointer record { request = _ ; response = response ; request-tagged = rt } p in S rec translate-send-pointer : ∀ {ct MT} → MT ∈ active-reply-type ct → (TagField ∷ MT) ∈ ct .channel-shape - translate-send-pointer {record { channel-shape = [] }} () + translate-send-pointer {record { all-tagged = [] }} () translate-send-pointer {record { all-tagged = HasTag MT ∷ _ }} Z = Z translate-send-pointer {record { channel-shape = x ∷ xs ; all-tagged = px ∷ pxs }} (S p) = S (translate-send-pointer p) @@ -148,9 +258,9 @@ invoke-reply-method (tag ∷ _ ∷ f) ci handler p (HasTag+Ref MT) = let active-message : Message (active-request-type ci) - active-message = Msg (translate-invoke-pointer p) f + active-message = Msg (translate-invoke-pointer ci p) f in do - record { new-state = new-state ; reply = SendM which fields } ← handler _ _ active-message state + record { new-state = new-state ; reply = SendM which fields } ← handler _ (_ sent active-message) state send Z (SendM (translate-send-pointer which) (lift tag ∷ fields)) return₁ new-state invoke : {i : Size} {MT : MessageType} → @@ -217,13 +327,21 @@ open AcceptSublistDependent in record { accepted-which = S (rec .accepted-which) ; fields = rec .fields } +\end{code} +%<*run-active-object> +\begin{code} run-active-object : {i : Size} → (ac : ActiveObject) → (state : ac .state-type) → - ∞ActorM (↑ i) (active-inbox-shape ac) (ac .state-type) ((ac .vars) state) (ac .vars) + ∞ActorM (↑ i) + (active-inbox-shape ac) + (ac .state-type) + ((ac .vars) state) + (ac .vars) run-active-object ac state .force = receive-active-method ac ∞>>= λ { m .force → handle-active-method ac m state ∞>>= λ state' → run-active-object ac state' } \end{code} +%