From 542a6b7c7642230ab9ef7c76bc937177ff7e5dbe Mon Sep 17 00:00:00 2001 From: Pierre Krafft Date: Tue, 12 Jun 2018 16:49:48 +0200 Subject: [PATCH] Writing --- src/EnvironmentOperations.lagda.tex | 18 ++++++++--------- src/Selective/EnvironmentOperations.agda | 18 ++++++++--------- src/Selective/SimulationEnvironment.lagda.tex | 20 +++++++++---------- src/SimulationEnvironment.lagda.tex | 20 +++++++++---------- 4 files changed, 38 insertions(+), 38 deletions(-) diff --git a/src/EnvironmentOperations.lagda.tex b/src/EnvironmentOperations.lagda.tex index 402f195..32fcb5f 100644 --- a/src/EnvironmentOperations.lagda.tex +++ b/src/EnvironmentOperations.lagda.tex @@ -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 @@ -209,7 +209,7 @@ {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 _ _ [] () _ @@ -217,14 +217,14 @@ 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) @@ -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 @@ -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) = @@ -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 @@ -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} → diff --git a/src/Selective/EnvironmentOperations.agda b/src/Selective/EnvironmentOperations.agda index bfb6c34..320e1aa 100644 --- a/src/Selective/EnvironmentOperations.agda +++ b/src/Selective/EnvironmentOperations.agda @@ -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 @@ -209,7 +209,7 @@ 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 _ _ [] () _ @@ -217,14 +217,14 @@ 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) @@ -316,7 +316,7 @@ 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 @@ -324,10 +324,10 @@ record GetInbox (store : Store) {store' : Store} (inboxes : Inboxes store') {nam -- 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) = @@ -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 @@ -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} → diff --git a/src/Selective/SimulationEnvironment.lagda.tex b/src/Selective/SimulationEnvironment.lagda.tex index 35b9f65..7982efe 100644 --- a/src/Selective/SimulationEnvironment.lagda.tex +++ b/src/Selective/SimulationEnvironment.lagda.tex @@ -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₁} @@ -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) @@ -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 @@ -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 @@ -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 diff --git a/src/SimulationEnvironment.lagda.tex b/src/SimulationEnvironment.lagda.tex index 547e33c..24eb067 100644 --- a/src/SimulationEnvironment.lagda.tex +++ b/src/SimulationEnvironment.lagda.tex @@ -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₁} @@ -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) @@ -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₁ @@ -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 @@ -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