Writing

src/EnvironmentOperations.agda → 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}
+%</named-inboxes>
+\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}

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}
+%</All>

src/Examples/SizedStream.lagda.tex

@@ -9,28 +9,28 @@
   coinductive
   field
     head : A
-    tail : ∀ {j : Size< i} → Stream j A
+    tail : (j : Size< i) → Stream j A
 \end{code}
 %</Stream>
 \begin{code}
 open Stream
 \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}
 %</SkipTwice>
 %<*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}
 %</Fib>

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

src/Simulate.agda → 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}
+%</reduceHeader>
+\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}

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}
+%</IsBlocked>
+\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