Skip to content

Commit

Permalink
Writing
Browse files Browse the repository at this point in the history
  • Loading branch information
@Zalastax
Zalastax committed May 24, 2018
1 parent 8a7b685 commit 8528e93
Show file tree
Hide file tree
Showing 4 changed files with 185 additions and 59 deletions.
8 changes: 5 additions & 3 deletions src/ActorMonad.lagda.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
24 changes: 15 additions & 9 deletions src/Selective/Examples/ChatAO.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -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 = [] }))
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions src/Selective/Examples/TestAO.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down
204 changes: 161 additions & 43 deletions src/Selective/Libraries/ActiveObjects.lagda.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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}
%</ActiveMethod>
\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}
%</ResponseInput>
\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}
%</state-vars>
\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}
%</ActiveReply>
\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}
%</active-method-VoidMethod>
\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}
%</active-method-ResponseMethod>
\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}
%</method-handler>
\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
Expand All @@ -69,14 +167,26 @@
let rec = methods-shape lci
am-shape = active-method-request am
in am-shape ++ rec

\end{code}
%</methods-shape>
%<*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}
%</ActiveObject>
\begin{code}

active-inbox-shape : ActiveObject → InboxShape
active-inbox-shape ac =
Expand Down Expand Up @@ -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)

Expand All @@ -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} →
Expand Down Expand Up @@ -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}
%</run-active-object>

0 comments on commit 8528e93

Please sign in to comment.