From 97b22190df841c071852f3e30e856bf6b48ba335 Mon Sep 17 00:00:00 2001 From: Pierre Krafft Date: Wed, 16 May 2018 23:36:21 +0200 Subject: [PATCH] Writing --- ...s.agda => EnvironmentOperations.lagda.tex} | 34 +++++++++---- src/Examples/SimpleActor.lagda.tex | 50 +++++++++++++++++++ src/Examples/SizedStream.lagda.tex | 20 ++++---- src/Prelude.agda | 2 +- src/{Simulate.agda => Simulate.lagda.tex} | 17 +++++-- src/SimulationEnvironment.lagda.tex | 20 +++++--- 6 files changed, 113 insertions(+), 30 deletions(-) rename src/{EnvironmentOperations.agda => EnvironmentOperations.lagda.tex} (98%) create mode 100644 src/Examples/SimpleActor.lagda.tex rename src/{Simulate.agda => Simulate.lagda.tex} (94%) diff --git a/src/EnvironmentOperations.agda b/src/EnvironmentOperations.lagda.tex similarity index 98% rename from src/EnvironmentOperations.agda rename to src/EnvironmentOperations.lagda.tex index d24291a..402f195 100644 --- a/src/EnvironmentOperations.agda +++ b/src/EnvironmentOperations.lagda.tex @@ -1,3 +1,4 @@ +\begin{code} module EnvironmentOperations where open import ActorMonad open import SimulationEnvironment @@ -463,18 +464,20 @@ ; contained-eq-inboxes = refl } lift-references (_∷_ {y} {xs} x₁ subs) refs refl with (lift-references subs refs refl) -... | q = record { +... | q = + let + contained-el : NamedInbox + contained-el = lookup-parallel x₁ refs shape refl + contained-el-shape = shape contained-el + contained-el-ok : y ≡ contained-el-shape + contained-el-ok = lookup-parallel-≡ x₁ refs shape refl + in record { subset-inbox = x₁ ∷ subs ; contained = contained-el ∷ contained q ; subset = (translate-∈ x₁ refs shape refl) ∷ (subset q) ; contained-eq-inboxes = combine contained-el-shape y (map shape (contained q)) xs (sym contained-el-ok) (contained-eq-inboxes q) } where - contained-el : NamedInbox - contained-el = lookup-parallel x₁ refs shape refl - contained-el-shape = shape contained-el - contained-el-ok : y ≡ contained-el-shape - contained-el-ok = lookup-parallel-≡ x₁ refs shape refl combine : (a b : InboxShape) → (as bs : TypingContext) → (a ≡ b) → (as ≡ bs) → (a ∷ as ≡ b ∷ bs) combine a .a as .as refl refl = refl @@ -594,13 +597,24 @@ unname-field {ValueType x₁} nfc = nfc unname-field {ReferenceType x₁} nfc = _ +\end{code} +%<*named-inboxes> +\begin{code} extract-inboxes : ∀ {MT} → All named-field-content MT → List NamedInbox extract-inboxes [] = [] -extract-inboxes (_∷_ {ValueType _} _ ps) = extract-inboxes ps -extract-inboxes (_∷_ {ReferenceType x} name ps) = inbox# name [ x ] ∷ extract-inboxes ps +extract-inboxes (_∷_ {ValueType _} _ ps) = + let rec = extract-inboxes ps + in rec +extract-inboxes (_∷_ {ReferenceType x} name ps) = + let rec = extract-inboxes ps + in inbox# name [ x ] ∷ rec named-inboxes : ∀ {S} → (nm : NamedMessage S) → List NamedInbox -named-inboxes (NamedM x x₁) = extract-inboxes x₁ +named-inboxes (NamedM tag fields) = extract-inboxes fields +\end{code} +% +\begin{code} + reference-names : {MT : MessageType} → All named-field-content MT → List Name reference-names [] = [] @@ -664,3 +678,5 @@ make-pointers-compatible store _ refs refl (_∷_ {ReferenceType x} px fields) rhp = let foundFw = lookup-reference _ refs rhp refl (actual-is-sendable px) in FhpR (make-pointer-compatible store x refs px rhp foundFw) ∷ (make-pointers-compatible store _ refs refl fields rhp) + +\end{code} diff --git a/src/Examples/SimpleActor.lagda.tex b/src/Examples/SimpleActor.lagda.tex new file mode 100644 index 0000000..0761978 --- /dev/null +++ b/src/Examples/SimpleActor.lagda.tex @@ -0,0 +1,50 @@ +\begin{code} +module Examples.SimpleActor where + +open import ActorMonad public +open import Prelude + +ℕ₁ : Set₁ +ℕ₁ = Lift ℕ + +\end{code} +%<*All> +\begin{code} +TickTock : MessageType +TickTock = [ ValueType Bool ]ˡ + +TickTocker : InboxShape +TickTocker = [ TickTock ]ˡ + +tick-tocker : ∀ {i} → ∞ActorM (↑ i) TickTocker ⊤₁ [] (λ _ → []) +tick-tocker .force = (do + self + Msg Z (b ∷ []) ← receive + where Msg (S ()) _ + let + Γ = [ TickTocker ]ˡ + to : Γ ⊢ TickTocker + to = Z + tag : TickTock ∈ TickTocker + tag = Z + fields : All (send-field-content Γ) TickTock + fields = lift (not b) ∷ [] + to ![t: tag ] fields + strengthen []) ∞>>= + λ _ → tick-tocker + +spawner : ∀ {i} → ∞ActorM i [] ℕ₁ [] (λ _ → [ TickTocker ]ˡ) +spawner = do + spawn∞ tick-tocker + let + Γ = [ TickTocker ]ˡ + to : Γ ⊢ TickTocker + to = Z + tag : TickTock ∈ TickTocker + tag = Z + fields : All (send-field-content Γ) TickTock + fields = lift true ∷ [] + to ![t: tag ] fields + return 42 +\end{code} +% diff --git a/src/Examples/SizedStream.lagda.tex b/src/Examples/SizedStream.lagda.tex index 884270e..e956b47 100644 --- a/src/Examples/SizedStream.lagda.tex +++ b/src/Examples/SizedStream.lagda.tex @@ -9,7 +9,7 @@ coinductive field head : A - tail : ∀ {j : Size< i} → Stream j A + tail : (j : Size< i) → Stream j A \end{code} % \begin{code} @@ -17,20 +17,20 @@ \end{code} %<*SkipTwice> \begin{code} -skip-twice : {i : Size} → Stream (↑ (↑ i)) ℕ → Stream i ℕ -skip-twice s = s .tail .tail +skip-twice : (i : Size) → Stream (↑ (↑ i)) ℕ → Stream i ℕ +skip-twice i s = s .tail (↑ i) .tail i \end{code} % %<*Fib> \begin{code} -zipWith : {i : Size} {A B C : Set} → (A → B → C) → +zipWith : (i : Size) {A B C : Set} → (A → B → C) → Stream i A → Stream i B → Stream i C -(zipWith f xs ys) .head = f (xs .head) (ys .head) -(zipWith f xs ys) .tail = zipWith f (xs .tail) (ys .tail) +(zipWith i f xs ys) .head = f (xs .head) (ys .head) +(zipWith i f xs ys) .tail j = zipWith j f (xs .tail j) (ys .tail j) -fib : {i : Size} → Stream i ℕ -fib .head = 0 -fib .tail .head = 1 -fib .tail .tail = zipWith _+_ fib (fib .tail) +fib : (i : Size) → Stream i ℕ +fib i .head = 0 +fib i .tail j .head = 1 +fib i .tail j .tail k = zipWith k _+_ (fib k) (fib j .tail k) \end{code} % diff --git a/src/Prelude.agda b/src/Prelude.agda index 9c6a523..dae94ab 100644 --- a/src/Prelude.agda +++ b/src/Prelude.agda @@ -2,7 +2,7 @@ module Prelude where -- Simple data open import Data.Bool public - using (Bool ; false ; true) + using (Bool ; false ; true ; not) open import Data.Empty public using (⊥ ; ⊥-elim) open import Data.Nat public diff --git a/src/Simulate.agda b/src/Simulate.lagda.tex similarity index 94% rename from src/Simulate.agda rename to src/Simulate.lagda.tex index bb1ecd2..6a545e8 100644 --- a/src/Simulate.agda +++ b/src/Simulate.lagda.tex @@ -1,3 +1,4 @@ +\begin{code} module Simulate where open import ActorMonad public @@ -94,7 +95,7 @@ env'' : Env env'' = top-actor-to-back env' actor' : Actor - actor' = add-reference actor new-store-entry (Return _ ⟶ cont) + actor' = add-reference actor new-store-entry (Return (lift tt) ⟶ cont) valid'' : ValidActor (env'' .store) actor' valid'' = add-reference-valid RefAdded valid' [p: zero ][handles: ⊆-refl ] env''' : Env @@ -105,12 +106,12 @@ ActorAtConstructor Send act → Env reduce-send env@record { - acts = actor@record { computation = Send {ToIS = ToIS} canSendTo (SendM tag fields) ⟶ cont } ∷ rest + acts = actor@record { computation = Send {ToIS = ToIS} Γ⊢ToIS (SendM tag fields) ⟶ cont } ∷ rest ; actors-valid = actor-valid ∷ rest-valid } Focused AtSend = let to-reference : FoundReference (store env) ToIS - to-reference = lookup-reference-act actor-valid canSendTo + to-reference = lookup-reference-act actor-valid Γ⊢ToIS namedFields = name-fields-act (store env) actor fields actor-valid actor' : Actor actor' = replace-actorM actor (Return _ ⟶ cont) @@ -253,7 +254,13 @@ actor-valid' in env' -reduce : {act : Actor} → (env : Env) → Focus act env → Env +\end{code} +%<*reduceHeader> +\begin{code} +reduce : {actor : Actor} → (env : Env) → Focus actor env → Env +\end{code} +% +\begin{code} reduce env@record { acts = record { computation = (Return val ⟶ []) } ∷ _ } Focused = reduce-unbound-return env Focused AtReturn (NoContinuation {v = val}) reduce env@record { acts = record { computation = (Return val ⟶ (_ ∷ _)) } ∷ _ } Focused = @@ -278,3 +285,5 @@ open ∞Trace keep-stepping : Env → ∞Trace ∞ keep-stepping env .force = env ∷ simulate env + +\end{code} diff --git a/src/SimulationEnvironment.lagda.tex b/src/SimulationEnvironment.lagda.tex index 96427ff..c20f5c8 100644 --- a/src/SimulationEnvironment.lagda.tex +++ b/src/SimulationEnvironment.lagda.tex @@ -25,7 +25,7 @@ -- and can prove that it is unused by proving that every -- previously used name is < than the new name. --- See definition of Name below +-- See definition of Name below -- Named inboxes are just an inbox shape and a name. -- We use this representation to separate the shape of the store and @@ -50,7 +50,7 @@ \end{code} %<*Store> \begin{code} - + Name = ℕ record NamedInbox : Set₁ where @@ -455,16 +455,24 @@ ; name = name }) -data IsBlocked (store : Store) (inbs : Inboxes store) (actor : Actor) : Set₂ where +\end{code} +%<*IsBlocked> +\begin{code} +data IsBlocked (store : Store) + (inboxes : Inboxes store) + (actor : Actor) : Set₂ where BlockedReturn : ActorAtConstructor Return actor → ActorHasNoContinuation actor → - IsBlocked store inbs actor + IsBlocked store inboxes actor BlockedReceive : ActorAtConstructor Receive actor → (p : has-inbox store actor) → - InboxForPointer [] store inbs p → - IsBlocked store inbs actor + InboxForPointer [] store inboxes p → + IsBlocked store inboxes actor +\end{code} +% +\begin{code} -- The environment is a list of actors and inboxes, -- with a proof that every ector is valid in the context of said list of inboxes