Skip to content

Commit

Permalink
Writing
Browse files Browse the repository at this point in the history
  • Loading branch information
@Zalastax
Zalastax committed Jun 12, 2018
1 parent 057202d commit 542a6b7
Show file tree
Hide file tree
Showing 4 changed files with 38 additions and 38 deletions.
18 changes: 9 additions & 9 deletions src/EnvironmentOperations.lagda.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -189,7 +189,7 @@
field
updated-inboxes : Inboxes store'
inboxes-valid : InboxesValid store updated-inboxes
others-unaffected : ∀ {name' IS' inb} → ¬ name ≡ name' → {p' : name' ↦ IS' ∈e store'} → InboxForPointer inb store' original p' → InboxForPointer inb store' updated-inboxes p'
others-unaffected : ∀ {name' IS' inb} → ¬ name ≡ name' → {p' : name' ↦ IS' ∈ store'} → InboxForPointer inb store' original p' → InboxForPointer inb store' updated-inboxes p'


open ValidMessageList
Expand All @@ -209,22 +209,22 @@
{store' : Store} →
(inboxes : Inboxes store') →
(InboxesValid store inboxes) →
(name ↦ IS ∈e store') →
(name ↦ IS ∈ store') →
(f : InboxUpdater store IS) →
UpdatedInbox store inboxes name
update-inbox _ _ [] () _
update-inbox {name} store {store'} (x ∷ inboxes) (px ∷ proofs) zero f =
record { updated-inboxes = inbox updated ∷ inboxes ; inboxes-valid = (valid updated) ∷ proofs ; others-unaffected = unaffected }
where
updated = (f (record { inbox = x ; valid = px }))
unaffected : ∀ {name' IS' inb} → ¬ name ≡ name' → {p' : name' ↦ IS' ∈e store'} → InboxForPointer inb store' (x ∷ inboxes) p' → InboxForPointer inb store' (inbox updated ∷ inboxes) p'
unaffected : ∀ {name' IS' inb} → ¬ name ≡ name' → {p' : name' ↦ IS' ∈ store'} → InboxForPointer inb store' (x ∷ inboxes) p' → InboxForPointer inb store' (inbox updated ∷ inboxes) p'
unaffected pr zero = ⊥-elim (pr refl)
unaffected pr (suc ifp) = suc ifp
update-inbox {name} store {store'} (x ∷ inboxes) (px ∷ proofs) (suc p) f =
record { updated-inboxes = x ∷ updated-inboxes updated ; inboxes-valid = px ∷ inboxes-valid updated ; others-unaffected = unaffected }
where
updated = (update-inbox store inboxes proofs p f)
unaffected : ∀ {name' IS' inb} → ¬ name ≡ name' → {p' : name' ↦ IS' ∈e store'} → InboxForPointer inb store' (x ∷ inboxes) p' → InboxForPointer inb store' (x ∷ updated-inboxes updated) p'
unaffected : ∀ {name' IS' inb} → ¬ name ≡ name' → {p' : name' ↦ IS' ∈ store'} → InboxForPointer inb store' (x ∷ inboxes) p' → InboxForPointer inb store' (x ∷ updated-inboxes updated) p'
unaffected pr zero = zero
unaffected pr (suc ifp) = suc (others-unaffected updated pr ifp)

Expand Down Expand Up @@ -315,7 +315,7 @@



record GetInbox (store : Store) {store' : Store} (inboxes : Inboxes store') {name : Name} {S : InboxShape} (p : name ↦ S ∈e store') : Set₂ where
record GetInbox (store : Store) {store' : Store} (inboxes : Inboxes store') {name : Name} {S : InboxShape} (p : name ↦ S ∈ store') : Set₂ where
field
messages : Inbox S
valid : all-messages-valid store messages
Expand All @@ -330,10 +330,10 @@

-- Get the messages of an inbox pointed to in the environment.
-- This is just a simple lookup into the list of inboxes.
get-inbox : ∀ {name IS} → (env : Env) → (p : name ↦ IS ∈e (store env)) → GetInbox (env .store) (env .env-inboxes) p
get-inbox : ∀ {name IS} → (env : Env) → (p : name ↦ IS ∈ (store env)) → GetInbox (env .store) (env .env-inboxes) p
get-inbox env point = loop (env-inboxes env) (messages-valid env) point
where
loop : {store store' : Store} → (inbs : Inboxes store') → InboxesValid store inbs → ∀ {name IS} → (p : name ↦ IS ∈e store') → GetInbox store inbs p
loop : {store store' : Store} → (inbs : Inboxes store') → InboxesValid store inbs → ∀ {name IS} → (p : name ↦ IS ∈ store') → GetInbox store inbs p
loop _ [] ()
loop (x ∷ _) (px ∷ _) zero = record { messages = x ; valid = px ; right-inbox = zero }
loop (_ ∷ inbs) (_ ∷ inb-valid) (suc point) =
Expand Down Expand Up @@ -397,7 +397,7 @@
blocked-unaffected (BlockedReturn x y) = BlockedReturn x y
blocked-unaffected (BlockedReceive x p y) = BlockedReceive x p (others-unaffected updated ¬p y)

update-inbox-env : ∀ {name IS} → (env : Env) → name ↦ IS ∈e (store env) →
update-inbox-env : ∀ {name IS} → (env : Env) → name ↦ IS ∈ (store env) →
(f : ValidMessageList (store env) IS → ValidMessageList (store env) IS) → Env
update-inbox-env {name} {IS} env p f =
let
Expand Down Expand Up @@ -437,7 +437,7 @@
open FoundReference

-- Extract the found pointer
underlying-pointer : ∀ {IS store} → (ref : FoundReference store IS) → (name ref ↦ actual (reference ref) ∈e store )
underlying-pointer : ∀ {IS store} → (ref : FoundReference store IS) → (name ref ↦ actual (reference ref) ∈ store )
underlying-pointer ref = actual-has-pointer (reference ref)

translate-message-pointer : ∀ {ToIS A store} →
Expand Down
18 changes: 9 additions & 9 deletions src/Selective/EnvironmentOperations.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -189,7 +189,7 @@ record UpdatedInbox (store : Store) {store' : Store} (original : Inboxes store')
field
updated-inboxes : Inboxes store'
inboxes-valid : InboxesValid store updated-inboxes
others-unaffected : ∀ {name' IS' inb} → ¬ name ≡ name' → {p' : name' ↦ IS' ∈e store'} → InboxForPointer inb store' original p' → InboxForPointer inb store' updated-inboxes p'
others-unaffected : ∀ {name' IS' inb} → ¬ name ≡ name' → {p' : name' ↦ IS' ∈ store'} → InboxForPointer inb store' original p' → InboxForPointer inb store' updated-inboxes p'


open ValidMessageList
Expand All @@ -209,22 +209,22 @@ update-inbox : {name : Name} → {IS : InboxShape} →
{store' : Store} →
(inboxes : Inboxes store') →
(InboxesValid store inboxes) →
(name ↦ IS ∈e store') →
(name ↦ IS ∈ store') →
(f : InboxUpdater store IS) →
UpdatedInbox store inboxes name
update-inbox _ _ [] () _
update-inbox {name} store {store'} (x ∷ inboxes) (px ∷ proofs) zero f =
record { updated-inboxes = inbox updated ∷ inboxes ; inboxes-valid = (valid updated) ∷ proofs ; others-unaffected = unaffected }
where
updated = (f (record { inbox = x ; valid = px }))
unaffected : ∀ {name' IS' inb} → ¬ name ≡ name' → {p' : name' ↦ IS' ∈e store'} → InboxForPointer inb store' (x ∷ inboxes) p' → InboxForPointer inb store' (inbox updated ∷ inboxes) p'
unaffected : ∀ {name' IS' inb} → ¬ name ≡ name' → {p' : name' ↦ IS' ∈ store'} → InboxForPointer inb store' (x ∷ inboxes) p' → InboxForPointer inb store' (inbox updated ∷ inboxes) p'
unaffected pr zero = ⊥-elim (pr refl)
unaffected pr (suc ifp) = suc ifp
update-inbox {name} store {store'} (x ∷ inboxes) (px ∷ proofs) (suc p) f =
record { updated-inboxes = x ∷ updated-inboxes updated ; inboxes-valid = px ∷ inboxes-valid updated ; others-unaffected = unaffected }
where
updated = (update-inbox store inboxes proofs p f)
unaffected : ∀ {name' IS' inb} → ¬ name ≡ name' → {p' : name' ↦ IS' ∈e store'} → InboxForPointer inb store' (x ∷ inboxes) p' → InboxForPointer inb store' (x ∷ updated-inboxes updated) p'
unaffected : ∀ {name' IS' inb} → ¬ name ≡ name' → {p' : name' ↦ IS' ∈ store'} → InboxForPointer inb store' (x ∷ inboxes) p' → InboxForPointer inb store' (x ∷ updated-inboxes updated) p'
unaffected pr zero = zero
unaffected pr (suc ifp) = suc (others-unaffected updated pr ifp)

Expand Down Expand Up @@ -316,18 +316,18 @@ add-top {IS} {A} {post} m env = record



record GetInbox (store : Store) {store' : Store} (inboxes : Inboxes store') {name : Name} {S : InboxShape} (p : name ↦ S ∈e store') : Set₂ where
record GetInbox (store : Store) {store' : Store} (inboxes : Inboxes store') {name : Name} {S : InboxShape} (p : name ↦ S ∈ store') : Set₂ where
field
messages : Inbox S
valid : all-messages-valid store messages
right-inbox : InboxForPointer messages store' inboxes p

-- Get the messages of an inbox pointed to in the environment.
-- This is just a simple lookup into the list of inboxes.
get-inbox : ∀ {name IS} → (env : Env) → (p : name ↦ IS ∈e (store env)) → GetInbox (env .store) (env .env-inboxes) p
get-inbox : ∀ {name IS} → (env : Env) → (p : name ↦ IS ∈ (store env)) → GetInbox (env .store) (env .env-inboxes) p
get-inbox env point = loop (env-inboxes env) (messages-valid env) point
where
loop : {store store' : Store} → (inbs : Inboxes store') → InboxesValid store inbs → ∀ {name IS} → (p : name ↦ IS ∈e store') → GetInbox store inbs p
loop : {store store' : Store} → (inbs : Inboxes store') → InboxesValid store inbs → ∀ {name IS} → (p : name ↦ IS ∈ store') → GetInbox store inbs p
loop _ [] ()
loop (x ∷ _) (px ∷ _) zero = record { messages = x ; valid = px ; right-inbox = zero }
loop (_ ∷ inbs) (_ ∷ inb-valid) (suc point) =
Expand Down Expand Up @@ -392,7 +392,7 @@ unblock-actors {store} {original} {n} updated (x ∷ blckd) (v ∷ blckd-valid)
blocked-unaffected (BlockedReceive x p y) = BlockedReceive x p (others-unaffected updated ¬p y)
blocked-unaffected (BlockedSelective x p a b c) = BlockedSelective x p a (others-unaffected updated ¬p b) c

update-inbox-env : ∀ {name IS} → (env : Env) → name ↦ IS ∈e (store env) →
update-inbox-env : ∀ {name IS} → (env : Env) → name ↦ IS ∈ (store env) →
(f : ValidMessageList (store env) IS → ValidMessageList (store env) IS) → Env
update-inbox-env {name} {IS} env p f =
let
Expand Down Expand Up @@ -432,7 +432,7 @@ open _comp↦_∈_
open FoundReference

-- Extract the found pointer
underlying-pointer : ∀ {IS store} → (ref : FoundReference store IS) → (name ref ↦ actual (reference ref) ∈e store )
underlying-pointer : ∀ {IS store} → (ref : FoundReference store IS) → (name ref ↦ actual (reference ref) ∈ store )
underlying-pointer ref = actual-has-pointer (reference ref)

translate-message-pointer : ∀ {ToIS A store} →
Expand Down
20 changes: 10 additions & 10 deletions src/Selective/SimulationEnvironment.lagda.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,19 +52,19 @@
-- Indexing into the store is done by building the peano-number to the index of the element.
-- To create the successor you have to provide a proof that you're not going past the name
-- you're looking for.
data _↦_∈e_ (n : Name) (S : InboxShape) : Store → Set where
data _↦_∈_ (n : Name) (S : InboxShape) : Store → Set where
zero : ∀ {xs}
→ n ↦ S ∈e (inbox# n [ S ] ∷ xs)
→ n ↦ S ∈ (inbox# n [ S ] ∷ xs)
suc : ∀ {n' : Name} { S' xs} {pr : ¬ n ≡ n'}
→ n ↦ S ∈e xs
→ n ↦ S ∈e (inbox# n' [ S' ] ∷ xs)
→ n ↦ S ∈ xs
→ n ↦ S ∈ (inbox# n' [ S' ] ∷ xs)


record _comp↦_∈_ (n : Name) (wanted : InboxShape) (store : Store) : Set₁ where
constructor [p:_][handles:_]
field
{actual} : InboxShape
actual-has-pointer : n ↦ actual ∈e store
actual-has-pointer : n ↦ actual ∈ store
actual-handles-wanted : wanted <: actual

Cont : ∀ (i : Size) (IS : InboxShape) {A B : Set₁}
Expand Down Expand Up @@ -144,10 +144,10 @@
_∷_ : ∀ {store name inbox-shape} → Inbox inbox-shape →
(inboxes : Inboxes store) → Inboxes (inbox# name [ inbox-shape ] ∷ store)

data InboxForPointer {inbox-shape : InboxShape} (inbox : Inbox inbox-shape) {name : Name} : (store : Store) → (Inboxes store) → (name ↦ inbox-shape ∈e store) → Set₁ where
data InboxForPointer {inbox-shape : InboxShape} (inbox : Inbox inbox-shape) {name : Name} : (store : Store) → (Inboxes store) → (name ↦ inbox-shape ∈ store) → Set₁ where
zero : ∀ {store} {inbs : Inboxes store} →
InboxForPointer inbox (inbox# name [ inbox-shape ] ∷ store) (inbox ∷ inbs) zero
suc : ∀ {n' : Name} {S' inb' store} {p : name ↦ inbox-shape ∈e store} {inbs : Inboxes store} {pr : ¬ name ≡ n'} →
suc : ∀ {n' : Name} {S' inb' store} {p : name ↦ inbox-shape ∈ store} {inbs : Inboxes store} {pr : ¬ name ≡ n'} →
InboxForPointer inbox store inbs p →
InboxForPointer inbox (inbox# n' [ S' ] ∷ store) (inb' ∷ inbs) (suc {pr = pr} p)

Expand All @@ -157,7 +157,7 @@
has-inbox : Store → Actor → Set
has-inbox store actor =
let open Actor
in actor .name ↦ actor .inbox-shape ∈e store
in actor .name ↦ actor .inbox-shape ∈ store

inbox-for-actor : ∀ {store} (inbs : Inboxes store) (actor : Actor) (p : has-inbox store actor) (inb : Inbox (Actor.inbox-shape actor)) → Set₁
inbox-for-actor {store} inbs actor p inb = InboxForPointer inb store inbs p
Expand Down Expand Up @@ -225,7 +225,7 @@
field
name : Name
freshness-carrier : All (λ v → NamedInbox.name v < name) store
name-is-fresh : {n : Name} {IS : InboxShape} → n ↦ IS ∈e store → ¬ n ≡ name
name-is-fresh : {n : Name} {IS : InboxShape} → n ↦ IS ∈ store → ¬ n ≡ name

open NameSupply

Expand All @@ -239,7 +239,7 @@
-- helps show that all the names in the store are still valid if we add a new name on top,
-- if the new name is > than all the names already in the store.
suc-helper : ∀ {store name IS n} →
name ↦ IS ∈e store →
name ↦ IS ∈ store →
All (λ v → suc (NamedInbox.name v) ≤ n) store →
¬ name ≡ n
suc-helper zero (px ∷ p) = <-¬≡ px
Expand Down
20 changes: 10 additions & 10 deletions src/SimulationEnvironment.lagda.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -70,19 +70,19 @@
-- Indexing into the store is done by building the peano-number to the index of the element.
-- To create the successor you have to provide a proof that you're not going past the name
-- you're looking for.
data _↦_∈e_ (n : Name) (S : InboxShape) : Store → Set where
data _↦_∈_ (n : Name) (S : InboxShape) : Store → Set where
zero : ∀ {xs}
→ n ↦ S ∈e (inbox# n [ S ] ∷ xs)
→ n ↦ S ∈ (inbox# n [ S ] ∷ xs)
suc : ∀ {n' : Name} { S' xs} {pr : ¬ n ≡ n'}
→ n ↦ S ∈e xs
→ n ↦ S ∈e (inbox# n' [ S' ] ∷ xs)
→ n ↦ S ∈ xs
→ n ↦ S ∈ (inbox# n' [ S' ] ∷ xs)


record _comp↦_∈_ (n : Name) (wanted : InboxShape) (store : Store) : Set₁ where
constructor [p:_][handles:_]
field
{actual} : InboxShape
actual-has-pointer : n ↦ actual ∈e store
actual-has-pointer : n ↦ actual ∈ store
actual-handles-wanted : wanted <: actual

Cont : ∀ (i : Size) (IS : InboxShape) {A B : Set₁}
Expand Down Expand Up @@ -172,10 +172,10 @@
do-the-work {ValueType x₁ ∷ MT} (px ∷ nfc) = px ∷ (do-the-work nfc)
do-the-work {ReferenceType x₁ ∷ MT} (px ∷ nfc) = _ ∷ do-the-work nfc

data InboxForPointer {inbox-shape : InboxShape} (inbox : Inbox inbox-shape) {name : Name} : (store : Store) → (Inboxes store) → (name ↦ inbox-shape ∈e store) → Set₁ where
data InboxForPointer {inbox-shape : InboxShape} (inbox : Inbox inbox-shape) {name : Name} : (store : Store) → (Inboxes store) → (name ↦ inbox-shape ∈ store) → Set₁ where
zero : ∀ {store} {inbs : Inboxes store} →
InboxForPointer inbox (inbox# name [ inbox-shape ] ∷ store) (inbox ∷ inbs) zero
suc : ∀ {n' : Name} {S' inb' store} {p : name ↦ inbox-shape ∈e store} {inbs : Inboxes store} {pr : ¬ name ≡ n'} →
suc : ∀ {n' : Name} {S' inb' store} {p : name ↦ inbox-shape ∈ store} {inbs : Inboxes store} {pr : ¬ name ≡ n'} →
InboxForPointer inbox store inbs p →
InboxForPointer inbox (inbox# n' [ S' ] ∷ store) (inb' ∷ inbs) (suc {pr = pr} p)

Expand All @@ -185,7 +185,7 @@
has-inbox : Store → Actor → Set
has-inbox store actor =
let open Actor
in actor .name ↦ actor .inbox-shape ∈e store
in actor .name ↦ actor .inbox-shape ∈ store


inbox-for-actor : ∀ {store} (inbs : Inboxes store) (actor : Actor) (p : has-inbox store actor) (inb : Inbox (Actor.inbox-shape actor)) → Set₁
Expand Down Expand Up @@ -254,7 +254,7 @@
field
name : Name
freshness-carrier : All (λ v → NamedInbox.name v < name) store
name-is-fresh : {n : Name} {IS : InboxShape} → n ↦ IS ∈e store → ¬ n ≡ name
name-is-fresh : {n : Name} {IS : InboxShape} → n ↦ IS ∈ store → ¬ n ≡ name

open NameSupply

Expand All @@ -270,7 +270,7 @@
-- helps show that all the names in the store are still valid if we add a new name on top,
-- if the new name is > than all the names already in the store.
suc-helper : ∀ {store name IS n} →
name ↦ IS ∈e store →
name ↦ IS ∈ store →
All (λ v → suc (NamedInbox.name v) ≤ n) store →
¬ name ≡ n
suc-helper zero (px ∷ p) = <-¬≡ px
Expand Down

0 comments on commit 542a6b7

Please sign in to comment.