Better use of dependent types

Zalastax · Mar 22, 2018 · 2db0975 · 2db0975
1 parent c30d8e5
commit 2db0975
Show file tree

Hide file tree

Showing 5 changed files with 75 additions and 103 deletions.
diff --git a/src/.#Simulate.agda b/src/.#Simulate.agda
diff --git a/src/EnvironmentOperations.agda b/src/EnvironmentOperations.agda
@@ -121,14 +121,13 @@ rewrap-valid-actor va refl refl refl = record { actor-has-inbox = actor-has-inbo
 
 record ValidMessageList (store : Store) (S : InboxShape) : Set₁ where
   field
-    inbox : List (NamedMessage S)
+    inbox : Inbox S
     valid : All (message-valid store) inbox
 
-record UpdatedInboxes (store : Store) (original : Inboxes) : Set₂ where
+record UpdatedInboxes (store : Store)  {store' : Store} (original : Inboxes store') : Set₂ where
   field
-    updated-inboxes : Inboxes
-    inboxes-valid : All (all-messages-valid store) updated-inboxes
-    same-store : inboxes-to-store original ≡ inboxes-to-store updated-inboxes
+    updated-inboxes : Inboxes store'
+    inboxes-valid : InboxesValid store updated-inboxes
 
 open ValidMessageList
 open UpdatedInboxes
@@ -143,25 +142,16 @@ open UpdatedInboxes
 -- and has to provide a proof that this list is also valid for the store
 update-inboxes : {name : Name} → {IS : InboxShape} →
   (store : Store) →
-  (inboxes : Inboxes) →
-  (All (all-messages-valid store) inboxes) →
-  (name ↦ IS ∈e (inboxes-to-store inboxes)) →
+  {store' : Store} → (inboxes : Inboxes store') →
+  (InboxesValid store inboxes) →
+  (name ↦ IS ∈e store') →
   (f : ValidMessageList store IS → ValidMessageList store IS) →
   UpdatedInboxes store inboxes
-update-inboxes store [] [] () f
-update-inboxes store (x ∷ inboxes) (px ∷ proofs) zero f with (f (record { inbox = Inbox.inbox-messages x ; valid = px }))
-... | updated = record {
-  updated-inboxes = updatedInbox ∷ inboxes
-  ; inboxes-valid = (valid updated) ∷ proofs
-  ; same-store = refl }
-  where
-    updatedInbox : Inbox
-    updatedInbox = record { inbox-shape = Inbox.inbox-shape x ; inbox-messages = inbox updated ; name = Inbox.name x }
-update-inboxes store (x ∷ inboxes) (px ∷ proofs) (suc reference) f with (update-inboxes store inboxes proofs reference f)
-... | updatedInboxes = record {
-  updated-inboxes = x ∷ updated-inboxes updatedInboxes
-  ; inboxes-valid = px ∷ inboxes-valid updatedInboxes
-  ; same-store = cong (_∷_ inbox# (Inbox.name x) [ Inbox.inbox-shape x ]) (same-store updatedInboxes) }
+update-inboxes _ _ [] () _
+update-inboxes store (x ∷ inboxes) (px ∷ proofs) zero f with (f (record { inbox = x ; valid = px }))
+... | updated = record { updated-inboxes = (inbox updated) ∷ inboxes ; inboxes-valid = (valid updated) ∷ proofs }
+update-inboxes store (x ∷ inboxes) (px ∷ proofs) (suc p) f with (update-inboxes store inboxes proofs p f)
+... | updated = record { updated-inboxes = x ∷ updated-inboxes updated ; inboxes-valid = px ∷ (inboxes-valid updated) }
 
 -- Move the actor that is at the top of the list, to the back of the list
 -- This is done to create a round-robin system for the actors, since run-env always picks the actor at the top
@@ -175,7 +165,6 @@ top-actor-to-back env | x ∷ acts | (y ∷ prfs) = record
                              ; blocked = blocked env
                              ; env-inboxes = env-inboxes env
                              ; store = store env
-                             ; inbs=store = inbs=store env
                              ; fresh-name = fresh-name env
                              ; actors-valid = ++⁺ prfs (y ∷ [])
                              ; blocked-valid = blocked-valid env
@@ -194,7 +183,6 @@ drop-top-actor env | _ ∷ rest | _ ∷ prfs = record
                                   ; blocked = blocked env
                                   ; env-inboxes = env-inboxes env
                                   ; store = store env
-                                  ; inbs=store = inbs=store env
                                   ; fresh-name = fresh-name env
                                   ; actors-valid = prfs
                                   ; blocked-valid = blocked-valid env
@@ -239,26 +227,19 @@ valid-actor-suc frsh va = record {
     open _comp↦_∈_
 
 -- All the messages in an inbox are still valid if we add a new inbox to the store, as long as that name is not used in the store before
-messages-valid-suc : ∀ {store inb n x} → (NameFresh store n) → all-messages-valid store inb → all-messages-valid (inbox# n [ x ] ∷ store) inb
-messages-valid-suc {store} {inb} {n} {x} frsh vi = do-the-work n x (Inbox.inbox-shape inb) (Inbox.inbox-messages inb) vi frsh
+messages-valid-suc : ∀ {store IS n x} {inb : Inbox IS} → (NameFresh store n) → all-messages-valid store inb → all-messages-valid (inbox# n [ x ] ∷ store) inb
+messages-valid-suc {store} {IS} {n} {x} frsh [] = []
+messages-valid-suc {store} {IS} {n} {x} {nx ∷ _} frsh (px ∷ vi) = message-valid-suc nx px ∷ (messages-valid-suc frsh vi)
   where
     open _comp↦_∈_
-    fields-valid-suc : ∀ {MT} (x₂ : All named-field-content MT) →
-      all-fields-have-pointer store x₂ → all-fields-have-pointer (inbox# n [ x ] ∷ store) x₂
-    fields-valid-suc {[]} [] p = p
-    fields-valid-suc {ValueType x₁ ∷ MT} (_ ∷ x₂) (_ , ps) = _ , fields-valid-suc x₂ ps
-    fields-valid-suc {ReferenceType x₁ ∷ MT} (px ∷ x₂) (p , ps) = suc-p (suc-helper (actual-has-pointer p) frsh) p , fields-valid-suc x₂ ps
-    msgValidSuc : (x₁ : NamedMessage (Inbox.inbox-shape inb)) →
-                  message-valid store x₁ → message-valid (inbox# n [ x ] ∷ store) x₁
-    msgValidSuc (NamedM x₁ x₂) mv = fields-valid-suc x₂ mv
-    message-valid-suc : ∀ {MT} (x₂ : All named-field-content MT) → all-fields-have-pointer store x₂ → ∀ n x → (NameFresh store n) → all-fields-have-pointer (inbox# n [ x ] ∷ store) x₂
-    message-valid-suc {[]} [] hj n x frsh = _
-    message-valid-suc {ValueType x₁ ∷ MT} (px ∷ x₂) (_ , hj) n x frsh = _ , message-valid-suc x₂ hj n x frsh
-    message-valid-suc {ReferenceType x₁ ∷ MT} (name ∷ x₂) (px , hj) n x frsh = (suc-p (suc-helper (actual-has-pointer px) frsh) px) , message-valid-suc x₂ hj n x frsh
-    do-the-work : ∀ n x w (w₁ : List (NamedMessage w)) → All (message-valid store) w₁ → NameFresh store n →
-                  All (message-valid (inbox# n [ x ] ∷ store)) w₁
-    do-the-work n x w [] prfs frsh = []
-    do-the-work n x w (NamedM x₁ x₂ ∷ w₁) (px ∷ prfs) frsh = message-valid-suc x₂ px n x frsh ∷ (do-the-work n x w w₁ prfs frsh)
+    fields-valid-suc : ∀ {MT} → (fields : All named-field-content MT) →
+      all-fields-have-pointer store fields →
+      all-fields-have-pointer (inbox# n [ x ] ∷ store) fields
+    fields-valid-suc [] _ = _
+    fields-valid-suc {ValueType x ∷ _} (px ∷ fields) (_ , valid) = _ , (fields-valid-suc fields valid)
+    fields-valid-suc {ReferenceType x ∷ _} (px ∷ fields) (p , valid) = suc-p (suc-helper (actual-has-pointer p) frsh) p , (fields-valid-suc fields valid)
+    message-valid-suc : (nx : NamedMessage IS) → message-valid store nx → message-valid (inbox# n [ x ] ∷ store) nx
+    message-valid-suc (NamedM x₁ x₂) px = fields-valid-suc x₂ px
 
 -- Add a new actor to the environment.
 -- The actor is added to the top of the list of actors.
@@ -275,32 +256,33 @@ add-top {IS} {A} {post} actor-m env = record
                                             ; name = fresh-name env
                                             } ∷ acts env
                                  ; blocked = blocked env
-                                 ; env-inboxes = record { inbox-shape = IS ; inbox-messages = [] ; name = fresh-name env } ∷ env-inboxes env
+                                 ; env-inboxes = [] ∷ env-inboxes env
                                  ; store = inbox# fresh-name env [ IS ] ∷ store env
-                                 ; inbs=store = cong (_∷_ inbox# fresh-name env [ IS ]) (inbs=store env)
                                  ; fresh-name = suc (fresh-name env)
                                  ; actors-valid = record { actor-has-inbox = zero ; references-have-pointer = [] } ∷ ∀map (valid-actor-suc (name-is-fresh env)) (actors-valid env)
                                  ; blocked-valid = ∀map (valid-actor-suc (name-is-fresh env)) (blocked-valid env)
-                                 ; messages-valid = [] ∷ ∀map (λ {x} vi → messages-valid-suc {_} {x} (name-is-fresh env) vi) (messages-valid env)
+                                 ; messages-valid = [] ∷ map-suc (store env) (messages-valid env) (name-is-fresh env)
                                  ; name-is-fresh = Data.Nat.s≤s (≤-reflexive refl) ∷ ∀map  Data.Nat.Properties.≤-step (name-is-fresh env)
                                  }
+  where
+    map-suc : (store : Store) → {store' : Store} → {inbs : Inboxes store'} → InboxesValid store inbs → ∀ {n} → (NameFresh store n) → InboxesValid (inbox# n [ IS ] ∷ store) inbs
+    map-suc store [] frsh = []
+    map-suc store (x ∷ valid) frsh = messages-valid-suc frsh x ∷ (map-suc store valid frsh)
 
 record GetInbox (store : Store) (S : InboxShape) : Set₂ where
   field
-    messages : List (NamedMessage S)
-    valid : All (message-valid store) messages
+    messages : Inbox S
+    valid : all-messages-valid store messages
 
 -- 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) → name ↦ IS ∈e (store env) → GetInbox (store env) IS
-get-inbox env point = loop (env-inboxes env) (messages-valid env) (fix-the-point point (inbs=store env))
+get-inbox env point = loop (env-inboxes env) (messages-valid env) point
   where
-    fix-the-point : ∀ {name IS} → name ↦ IS ∈e store env → store env ≡ inboxes-to-store (env-inboxes env) → name ↦ IS ∈e inboxes-to-store (env-inboxes env)
-    fix-the-point p refl = p
-    loop : ∀ {name IS} → (inboxes : Inboxes) → All (all-messages-valid (store env)) inboxes → name ↦ IS ∈e (inboxes-to-store inboxes) → GetInbox (store env) IS
-    loop [] [] ()
-    loop (x ∷ _) (px ∷ prfs) zero = record { messages = Inbox.inbox-messages x ; valid = px }
-    loop (_ ∷ inboxes) (_ ∷ prfs) (suc point) = loop inboxes prfs point
+    loop : {store store' : Store} → (inbs : Inboxes store') → InboxesValid store inbs → ∀ {name IS} → name ↦ IS ∈e store' → GetInbox store IS
+    loop _ [] ()
+    loop (x ∷ _) (px ∷ _) zero = record { messages = x ; valid = px }
+    loop (_ ∷ inbs) (_ ∷ valid) (suc point) = loop inbs valid point
 
 -- Updates an inbox in the environment
 -- Just a wrapper arround 'updateInboxes'
@@ -309,20 +291,16 @@ update-inbox-env : ∀ {name IS} → (env : Env) → name ↦ IS ∈e (store env
 update-inbox-env {name} {IS} env p f = record
                            { acts = acts env
                            ; blocked = blocked env
-                           ; env-inboxes = updated-inboxes updatedInboxes
+                           ; env-inboxes = updated-inboxes updated
                            ; store = store env
-                           ; inbs=store = trans (inbs=store env) (same-store updatedInboxes)
                            ; fresh-name = fresh-name env
                            ; actors-valid = actors-valid env
                            ; blocked-valid = blocked-valid env
-                           ; messages-valid = inboxes-valid updatedInboxes
+                           ; messages-valid = inboxes-valid updated
                            ; name-is-fresh = name-is-fresh env
                            }
   where
-    -- Just some helpers to align the types
-    pp : name ↦ IS ∈e (inboxes-to-store (env-inboxes env))
-    pp rewrite (inbs=store env) = p
-    updatedInboxes = update-inboxes (store env) (env-inboxes env) (messages-valid env) pp f
+    updated = update-inboxes (store env) (env-inboxes env) (messages-valid env) p f
 
 -- Move an actor from the blocked list to the actors list.
 -- Simply looks through the names of all blocked actors and moves those (should be just 1 or 0) with the same name.
@@ -345,7 +323,6 @@ unblock-actor env name = newEnv (loop (blocked env) (blocked-valid env))
                                                              ; blocked = ba
                                                              ; env-inboxes = env-inboxes env
                                                              ; store = store env
-                                                             ; inbs=store = inbs=store env
                                                              ; fresh-name = fresh-name env
                                                              ; actors-valid = ++⁺ (actors-valid env) unblockedValid
                                                              ; blocked-valid = baValid
@@ -422,7 +399,6 @@ replace-actors env actors actorsValid = record {
   ; blocked = blocked env
   ; env-inboxes = env-inboxes env
   ; store = store env
-  ; inbs=store = inbs=store env
   ; fresh-name = fresh-name env
   ; actors-valid = actorsValid
   ; blocked-valid = blocked-valid env
@@ -439,7 +415,6 @@ replace-actors+blocked env actors actorsValid blocked blockedValid = record {
   ; blocked = blocked
   ; env-inboxes = env-inboxes env
   ; store = store env
-  ; inbs=store = inbs=store env
   ; fresh-name = fresh-name env
   ; actors-valid = actorsValid
   ; blocked-valid = blockedValid
@@ -457,7 +432,6 @@ add-message message valid vml = record { inbox = inbox vml ++ (message ∷ []) ;
 remove-message : {S : InboxShape} → {store : Store} → (ValidMessageList store S → ValidMessageList store S)
 remove-message vml = record { inbox = drop 1 (inbox vml) ; valid = drop⁺ 1 (ValidMessageList.valid vml) }
 
-
 name-fields : ∀ {MT store} → (pre : TypingContext) →
                (refs : List NamedInbox) →
                All (reference-has-pointer store) refs →

diff --git a/src/Runtime.agda b/src/Runtime.agda
@@ -50,16 +50,16 @@ log-trace : Trace → IO.IO ⊤
 log-trace trace = IO.putStrLn (show-trace trace ++ ".")
 
 -- Output the number of inboxes in the environment.
-log-inbox-count : Inboxes → IO.IO ⊤
-log-inbox-count inboxes = IO.putStrLn ("There are " ++ (show (Data.List.length inboxes)) ++ " inboxes.")
+log-inbox-count : ∀ {store} → Inboxes store → IO.IO ⊤
+log-inbox-count {store} inboxes = IO.putStrLn ("There are " ++ (show (Data.List.length store)) ++ " inboxes.")
 
 -- Output the number of messages in an inbox
-log-message-counts : Inboxes → IO.IO ⊤
+log-message-counts : ∀ {store} → Inboxes store → IO.IO ⊤
 log-message-counts [] = IO.return _
-log-message-counts (x ∷ xs) = ♯ IO.putStrLn ("Inbox #" ++ show (Inbox.name x) ++ " has " ++ (show (Data.List.length (Inbox.inbox-messages x))) ++ " messages.") IO.>> ♯ log-message-counts xs
+log-message-counts {inbox# name [ _ ] ∷ store} (x ∷ xs) = ♯ IO.putStrLn ("Inbox #" ++ show name ++ " has " ++ (show (Data.List.length x)) ++ " messages.") IO.>> ♯ log-message-counts xs
 
 -- Output the nunmber of inboxes and how many messages are in each inbox.
-log-inboxes : Inboxes → IO.IO ⊤
+log-inboxes : ∀ {store} → Inboxes store → IO.IO ⊤
 log-inboxes inboxes = ♯ log-inbox-count inboxes IO.>> ♯ log-message-counts inboxes
 
 -- Output how many actors are currently running and how many actors are blocked.

diff --git a/src/Simulate.agda b/src/Simulate.agda
@@ -119,16 +119,12 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f |
     newStoreEntry = inbox# fresh-name env [ NewIS ]
     newStore : Store
     newStore = newStoreEntry ∷ store env
-    newInb : Inbox
-    newInb = record { inbox-shape = NewIS ; inbox-messages = [] ; name = fresh-name env }
     newAct : Actor
     newAct = new-actor bm (fresh-name env)
     newActValid : ValidActor newStore newAct
     newActValid = record { actor-has-inbox = zero ; references-have-pointer = [] }
     newIsFresh : NameFresh newStore (suc (fresh-name env))
     newIsFresh = s≤s (≤-reflexive refl) ∷ ∀map ≤-step (name-is-fresh env)
-    newInbs=newStore : store env ≡ inboxes-to-store (env-inboxes env) → newStore ≡ inboxes-to-store (newInb ∷ env-inboxes env)
-    newInbs=newStore refl = refl
     bindAct : Actor
     bindAct = add-reference actor newStoreEntry (♭ (f _))
     bindActValid : ValidActor newStore bindAct
@@ -143,15 +139,18 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f |
     env' = record
              { acts = newAct ∷ bindAct ∷ rest
              ; blocked = blocked env
-             ; env-inboxes = newInb ∷ env-inboxes env
+             ; env-inboxes = [] ∷ env-inboxes env
              ; store = newStore
-             ; inbs=store = newInbs=newStore (inbs=store env)
              ; fresh-name = suc (fresh-name env)
              ; actors-valid = newActValid ∷ bindActValid ∷ ∀map (valid-actor-suc (name-is-fresh env)) restValid
              ; blocked-valid = ∀map (valid-actor-suc (name-is-fresh env)) (blocked-valid env)
-             ; messages-valid = [] ∷ ∀map (λ {inb} mv → messages-valid-suc {_} {inb} (name-is-fresh env) mv) (messages-valid env)
+             ; messages-valid = [] ∷ map-suc (store env) (messages-valid env) (name-is-fresh env)
              ; name-is-fresh = newIsFresh
              }
+         where
+           map-suc : (store : Store) → {store' : Store} → {inbs : Inboxes store'} → InboxesValid store inbs → ∀ {n} → (NameFresh store n) → InboxesValid (inbox# n [ NewIS ] ∷ store) inbs
+           map-suc store [] frsh = []
+           map-suc store (x ∷ valid) frsh = (messages-valid-suc frsh x) ∷ (map-suc store valid frsh)
 -- ===== Bind send reference =====
 -- Spawns a reference message and continues with (f tt).
 --
@@ -204,9 +203,7 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f |
   where
     actorsInbox : GetInbox (store env) (inbox-shape actor)
     actorsInbox = get-inbox env (actor-has-inbox valid)
-    actorsPointer : (inboxes-to-store (env-inboxes env) ≡ store env) → (name actor) ↦ (inbox-shape actor) ∈e inboxes-to-store (env-inboxes env)
-    actorsPointer refl = actor-has-inbox valid
-    inboxesAfter = update-inboxes (store env) (env-inboxes env) (messages-valid env) (actorsPointer (sym (inbs=store env))) remove-message
+    inboxesAfter = update-inboxes (store env) (env-inboxes env) (messages-valid env) (actor-has-inbox valid) remove-message
     receiveKind : List (NamedMessage (inbox-shape actor)) → ReceiveKind
     receiveKind [] = Nothing
     receiveKind (NamedM _ ps ∷ xs) = Value (reference-names ps)
@@ -219,7 +216,6 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f |
                                                                    ; blocked = blocked env
                                                                    ; env-inboxes = updated-inboxes inboxesAfter
                                                                    ; store = store env
-                                                                   ; inbs=store = trans (inbs=store env) (same-store inboxesAfter)
                                                                    ; actors-valid = record {
                                                                      actor-has-inbox = actor-has-inbox valid
                                                                      ; references-have-pointer = valid++ nm nmv (references actor) (references-have-pointer valid) } ∷ restValid