diff --git a/Makefile b/Makefile index 43d336a..77c9d80 100644 --- a/Makefile +++ b/Makefile @@ -23,7 +23,7 @@ selective-generated-main: sed 's/__ENTRY__/$(ENTRY)/' src/Selective/Examples/Main-template.agda > src/Selective/Examples/Main-generated.agda stack exec agda -- -c src/Selective/Examples/Main-generated.agda -test-that-all-compliles: +test-that-all-compiles: $(MAKE) latex-clean $(MAKE) latex stack exec agda -- --no-main -c src/Selective/Examples/Main-generated.agda diff --git a/src/ActorMonad.lagda.tex b/src/ActorMonad.lagda.tex index b0bc567..f0d7b64 100644 --- a/src/ActorMonad.lagda.tex +++ b/src/ActorMonad.lagda.tex @@ -321,17 +321,6 @@ % %<*ActorMonad> -This thesis started out with the goal of formalizing the λ-calculus for actors that -\textcite{DBLP:conf/ecoop/FowlerLW17} call $λ_{act}$. -When investigating $λ_{act}$ we noticed that the language had a structure that made it suitable -for being directly embedded in Agda, -as opposed to the external λ-calculus we originally envisioned. -What we had found was that the processes of $λ_{act}$ were instances of the monad pattern. -Furthermore, -\textcite{DBLP:conf/ecoop/FowlerLW17} show that if the host language is sufficiently advanced -selective receive can be implemented as a library, in contrast to having it as a built in primitive. -This led us to implement \ourlang as an embedded DSL in the form of a monad. - The goal when translating $λ_{act}$ to an Agda embedding was to make the actors correct by construction, and to make it possible to type-check each actor separately. The pattern we found suitable is a monad parameterized by the type of the actor's diff --git a/src/Selective/Libraries/ActiveObjects.lagda.tex b/src/Selective/Libraries/ActiveObjects.lagda.tex index f5a8fab..40dba9c 100644 --- a/src/Selective/Libraries/ActiveObjects.lagda.tex +++ b/src/Selective/Libraries/ActiveObjects.lagda.tex @@ -2,6 +2,7 @@ module Selective.Libraries.ActiveObjects where open import Selective.Libraries.Channel public +open import Selective.Libraries.ReceiveSublist open import Prelude open ChannelType @@ -293,39 +294,11 @@ forget-message input return₁ state' -accept-sublist-unwrapped : (xs ys zs : InboxShape) → ∀{MT} → MT ∈ (xs ++ ys ++ zs) → Bool -accept-sublist-unwrapped [] [] zs p = false -accept-sublist-unwrapped [] (y ∷ ys) zs Z = true -accept-sublist-unwrapped [] (y ∷ ys) zs (S p) = accept-sublist-unwrapped [] ys zs p -accept-sublist-unwrapped (x ∷ xs) ys zs Z = false -accept-sublist-unwrapped (x ∷ xs) ys zs (S p) = accept-sublist-unwrapped xs ys zs p - - -accept-sublist : (xs ys zs : InboxShape) → MessageFilter (xs ++ ys ++ zs) -accept-sublist xs ys zs (Msg received-message-type received-fields) = accept-sublist-unwrapped xs ys zs received-message-type - -record AcceptSublistDependent (IS : InboxShape) (accepted-type : MessageType) : Set₁ where - field - accepted-which : accepted-type ∈ IS - fields : All receive-field-content accepted-type - receive-active-method : {i : Size} → {Γ : TypingContext} → (ac : ActiveObject) → ∞ActorM i (active-inbox-shape ac) (Message (methods-shape (ac .methods))) Γ (add-references Γ) -receive-active-method ac = do - record { msg = Msg {MT} p f ; msg-ok = msg-ok } ← selective-receive (accept-sublist [] (methods-shape (ac .methods)) (ac .extra-messages)) - let record {accepted-which = aw ; fields = fields } = rewrap-message (methods-shape (ac .methods)) (ac .extra-messages) p f msg-ok - return₁ (Msg {MT = MT} aw fields) - where - rewrap-message : ∀{MT} → (ys zs : InboxShape) → (p : MT ∈ (ys ++ zs)) → All receive-field-content MT → (accept-sublist-unwrapped [] ys zs p) ≡ true → AcceptSublistDependent ys MT - rewrap-message [] zs which f () - rewrap-message (x ∷ ys) zs Z f p = record { accepted-which = Z ; fields = f } - rewrap-message (x ∷ ys) zs (S which) f p = - let - rec = rewrap-message ys zs which f p - open AcceptSublistDependent - in record { accepted-which = S (rec .accepted-which) ; fields = rec .fields } +receive-active-method ac = receive-sublist [] (methods-shape (ac .methods)) (ac .extra-messages) \end{code} %<*run-active-object> diff --git a/src/Selective/Libraries/CallNoComments.lagda.tex b/src/Selective/Libraries/CallNoComments.lagda.tex deleted file mode 100644 index 7915d78..0000000 --- a/src/Selective/Libraries/CallNoComments.lagda.tex +++ /dev/null @@ -1,95 +0,0 @@ -\begin{code} -module Selective.Libraries.CallNoComments where - -open import Selective.ActorMonad -open import Prelude - -open SelectedMessage - -UniqueTag = ℕ - -call-select-unwrap : ∀ {MtIn MT} {IS : InboxShape} → - UniqueTag → - MT ∈ IS → - All receive-field-content MT → - (ValueType UniqueTag ∷ MtIn) ∈ IS → - Bool -call-select-unwrap tag Z (tag' ∷ fs) Z = ⌊ tag ≟ tag' ⌋ -call-select-unwrap _ Z _ (S p) = false -call-select-unwrap _ (S x) _ Z = false -call-select-unwrap tag (S x) fs (S p) = call-select-unwrap tag x fs p - -call-select : ∀ {IS IS' MtIn} → - UniqueTag → - IS' <: IS → - (ValueType UniqueTag ∷ MtIn) ∈ IS' → - MessageFilter IS -call-select {IS} tag sub which (Msg x fs) = - call-select-unwrap tag x fs (translate-⊆ sub which) - -call : {Γ : TypingContext} {i : Size} - {MtTo MtIn : MessageType} - {To IS IS' : InboxShape} → - (Γ ⊢ To) → - ((ValueType UniqueTag ∷ ReferenceType IS' ∷ MtTo) ∈ To) → - (tag : UniqueTag) → - All (send-field-content Γ) MtTo → - (ISsubs : IS' <: IS) → - (whichIn : (ValueType UniqueTag ∷ MtIn) ∈ IS') → - ∞ActorM i IS - (SelectedMessage (call-select tag ISsubs whichIn)) - Γ (add-selected-references Γ) -call {Γ} {IS = IS} var toFi tag vals sub whichIn = - do - self - S var ![t: toFi ] ((lift tag) ∷ ([ Z ]>: sub) ∷ (translate-fields vals)) - strengthen (⊆-suc ⊆-refl) - selective-receive (call-select tag sub whichIn) - where - translate-fields : ∀ {MT} → - All (send-field-content Γ) MT → - All (send-field-content (IS ∷ Γ)) MT - translate-fields [] = [] - translate-fields {ValueType x ∷ MT} (px ∷ vals) = - px ∷ (translate-fields vals) - translate-fields {ReferenceType x ∷ MT} (([ p ]>: v) ∷ vals) = - ([ (S p) ]>: v) ∷ (translate-fields vals) - -AddReplyMessage : MessageType -AddReplyMessage = ValueType UniqueTag ∷ [ ValueType ℕ ]ˡ - -AddReply : InboxShape -AddReply = [ AddReplyMessage ]ˡ - -AddMessage : MessageType -AddMessage = ValueType UniqueTag ∷ ReferenceType AddReply ∷ ValueType ℕ ∷ [ ValueType ℕ ]ˡ - -Calculator : InboxShape -Calculator = [ AddMessage ]ˡ - -calculatorActor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift ⊤) [] (λ _ → []) -calculatorActor .force = receive ∞>>= λ { - (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) .force → - (Z ![t: Z ] (lift tag ∷ [ lift (n + m) ]ᵃ)) ∞>> (do - strengthen [] - calculatorActor) - ; (Msg (S ()) _) - } - -TestBox : InboxShape -TestBox = AddReply - -calltestActor : ∀{i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → []) -calltestActor .force = spawn∞ calculatorActor ∞>> do - x ← call Z Z 0 - ((lift 10) ∷ [ lift 32 ]ᵃ) - ⊆-refl Z - strengthen [] - return-result x - where - return-result : SelectedMessage {TestBox} (call-select 0 [ Z ]ᵐ Z) → - ∀ {i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → []) - 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/Libraries/ReceiveSublist.agda b/src/Selective/Libraries/ReceiveSublist.agda new file mode 100644 index 0000000..4fb9e61 --- /dev/null +++ b/src/Selective/Libraries/ReceiveSublist.agda @@ -0,0 +1,48 @@ +module Selective.Libraries.ReceiveSublist where + +open import Selective.ActorMonad public +open import Prelude + +accept-sublist-unwrapped : (xs ys zs : InboxShape) → ∀{MT} → MT ∈ (xs ++ ys ++ zs) → Bool +accept-sublist-unwrapped [] [] zs p = false +accept-sublist-unwrapped [] (y ∷ ys) zs Z = true +accept-sublist-unwrapped [] (y ∷ ys) zs (S p) = accept-sublist-unwrapped [] ys zs p +accept-sublist-unwrapped (x ∷ xs) ys zs Z = false +accept-sublist-unwrapped (x ∷ xs) ys zs (S p) = accept-sublist-unwrapped xs ys zs p + + +accept-sublist : (xs ys zs : InboxShape) → MessageFilter (xs ++ ys ++ zs) +accept-sublist xs ys zs (Msg received-message-type received-fields) = accept-sublist-unwrapped xs ys zs received-message-type + +record AcceptSublistDependent (IS : InboxShape) (accepted-type : MessageType) : Set₁ where + field + accepted-which : accepted-type ∈ IS + fields : All receive-field-content accepted-type + +receive-sublist : {i : Size} → + {Γ : TypingContext} → + (xs ys zs : InboxShape) → + ∞ActorM i (xs ++ ys ++ zs) + (Message ys) + Γ + (add-references Γ) +receive-sublist xs ys zs = do + record { msg = Msg {MT} p f ; msg-ok = msg-ok } ← selective-receive (accept-sublist xs ys zs) + let record {accepted-which = aw ; fields = fields } = rewrap-message xs ys zs p f msg-ok + return₁ (Msg {MT = MT} aw fields) + where + rewrap-message : ∀{MT} → + (xs ys zs : InboxShape) → + (p : MT ∈ (xs ++ ys ++ zs)) → + All receive-field-content MT → + (accept-sublist-unwrapped xs ys zs p) ≡ true → + AcceptSublistDependent ys MT + rewrap-message [] [] zs p f () + rewrap-message [] (x ∷ ys) zs Z f q = record { accepted-which = Z ; fields = f } + rewrap-message [] (x ∷ ys) zs (S p) f q = + let + rec = rewrap-message [] ys zs p f q + open AcceptSublistDependent + in record { accepted-which = S (rec .accepted-which) ; fields = rec .fields } + rewrap-message (x ∷ xs) ys zs Z f () + rewrap-message (x ∷ xs) ys zs (S p) f q = rewrap-message xs ys zs p f q