Prettier property for fields having pointer

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

Hide file tree

Showing 3 changed files with 33 additions and 35 deletions.
diff --git a/src/EnvironmentOperations.agda b/src/EnvironmentOperations.agda
@@ -232,14 +232,14 @@ 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} → (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)
+    fields-valid-suc : ∀ {MT} {fields : All named-field-content MT} →
+      FieldsHavePointer store fields →
+      FieldsHavePointer (inbox# n [ x ] ∷ store) fields
+    fields-valid-suc [] = []
+    fields-valid-suc (v+ valid) = v+ fields-valid-suc valid
+    fields-valid-suc (x ∷r valid) = (suc-p (suc-helper (actual-has-pointer x) frsh) x) ∷r (fields-valid-suc 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
+    message-valid-suc (NamedM x₁ x₂) px = fields-valid-suc px
 
 -- Add a new actor to the environment.
 -- The actor is added to the top of the list of actors.
@@ -452,7 +452,7 @@ unname-field {ValueType x₁} nfc = nfc
 unname-field {ReferenceType x₁} nfc = _
 
 unname-message : ∀ {S} → NamedMessage S → Message S
-unname-message (NamedM x fields) = Msg x (do-the-work fields) -- (∀map unname-field fields)
+unname-message (NamedM x fields) = Msg x (do-the-work fields)
   where
     do-the-work : ∀ {MT} → All named-field-content MT → All receive-field-content MT
     do-the-work {[]} nfc = []
@@ -486,19 +486,19 @@ add-references++ msg@(NamedM {MT} x x₁) p w = halp (add-fields++ MT x₁)
     add-fields++ (ValueType x ∷ MT) (px ∷ x₁) = add-fields++ MT x₁
     add-fields++ (ReferenceType x ∷ MT) (px ∷ x₁) = cong (_∷_ x) (add-fields++ MT x₁)
 
-valid++ : ∀ {S store} → (nm : NamedMessage S) → message-valid store nm → ∀ w →
+valid++ : ∀ {S store} → (nm : NamedMessage S) → message-valid store nm → ∀ {w} →
         All (reference-has-pointer store) w →
         All (reference-has-pointer store) (named-inboxes nm ++ w)
-valid++ (NamedM x x₁) v p = valid-fields x₁ v p
+valid++ (NamedM x x₁) v = valid-fields v
   where
     valid-fields : ∀ {MT store} →
-                   (x₁ : All named-field-content MT) →
-                   all-fields-have-pointer store x₁ → ∀ p →
+                   {fields : All named-field-content MT} →
+                   FieldsHavePointer store fields → ∀ {p} →
                    All (reference-has-pointer store) p →
-                   All (reference-has-pointer store) (extract-inboxes x₁ ++ p)
-    valid-fields [] h p ps = ps
-    valid-fields (_∷_ {ValueType x} px x₁) (_ , h) p ps = valid-fields x₁ h p ps
-    valid-fields (_∷_ {ReferenceType x} px x₁) (hj , h) p ps = hj ∷ (valid-fields x₁ h p ps)
+                   All (reference-has-pointer store) (extract-inboxes fields ++ p)
+    valid-fields [] ps = ps
+    valid-fields (v+ fhp) ps = valid-fields fhp ps
+    valid-fields (px ∷r fhp) ps = px ∷ (valid-fields fhp ps)
 
 open _⊢>:_
 
@@ -517,13 +517,15 @@ make-pointer-compatible : ∀ store x refs
                        name w comp↦ x ∈ store
 make-pointer-compatible store x refs px rhp w = [p: actual-has-pointer (reference w) ][handles: compatible-handles store x refs px w ]
 
+open FieldsHavePointer
+
 make-pointers-compatible : ∀ {MT} store pre refs (eq : map shape refs ≡ pre)
                            (fields : All (send-field-content pre) MT)
                            (rhp : All (reference-has-pointer store) refs) →
-                         all-fields-have-pointer store (name-fields pre refs rhp fields eq)
-make-pointers-compatible store pre refs eq [] rhp = _
-make-pointers-compatible store _ refs refl (_∷_ {ValueType x} px fields) rhp = _ , (make-pointers-compatible store _ refs refl fields rhp)
-make-pointers-compatible store _ refs refl (_∷_ {ReferenceType x} px fields) rhp = make-pointer-compatible store x refs px rhp foundFw , (make-pointers-compatible store _ refs refl fields rhp)
+                         FieldsHavePointer store (name-fields pre refs rhp fields eq)
+make-pointers-compatible store pre refs eq [] rhp = []
+make-pointers-compatible store _ refs refl (_∷_ {ValueType x} px fields) rhp = v+ make-pointers-compatible store _ refs refl fields rhp
+make-pointers-compatible store _ refs refl (_∷_ {ReferenceType x} px fields) rhp = (make-pointer-compatible store x refs px rhp foundFw) ∷r (make-pointers-compatible store _ refs refl fields rhp)
   where
     foundFw : FoundReference store (actual px)
     foundFw = lookup-reference _ refs rhp refl (actual-is-sendable px)
diff --git a/src/Simulate.agda b/src/Simulate.agda
@@ -218,7 +218,7 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m >>= f |
                                                                    ; store = store env
                                                                    ; actors-valid = record {
                                                                      actor-has-inbox = actor-has-inbox valid
-                                                                     ; references-have-pointer = valid++ nm nmv (references actor) (references-have-pointer valid) } ∷ restValid
+                                                                     ; references-have-pointer = valid++ nm nmv (references-have-pointer valid) } ∷ restValid
                                                                    ; blocked-valid = blocked-valid env
                                                                    ; messages-valid = inboxes-valid inboxesAfter
                                                                    ; fresh-name = fresh-name env

diff --git a/src/SimulationEnvironment.agda b/src/SimulationEnvironment.agda
@@ -142,17 +142,22 @@ record ValidActor (store : Store) (actor : Actor) : Set₂ where
     actor-has-inbox : has-inbox store actor
     references-have-pointer : all-references-have-a-pointer store actor
 
-all-fields-have-pointer : ∀ {MT} → Store → All named-field-content MT → Set₁
-all-fields-have-pointer st [] = Lift ⊤
-all-fields-have-pointer st (_∷_ {ValueType _} _ xs) = ⊤ × all-fields-have-pointer st xs
-all-fields-have-pointer st (_∷_ {ReferenceType Fw} name xs) = (name comp↦ Fw ∈ st) × all-fields-have-pointer st xs
+data FieldsHavePointer (store : Store) : ∀ {MT} → All named-field-content MT → Set₁ where
+  [] : FieldsHavePointer store []
+  v+_ : ∀ {MT A} {v : A} {nfc : All named-field-content MT} →
+    FieldsHavePointer store nfc →
+    FieldsHavePointer store {ValueType A ∷ MT} (v ∷ nfc)
+  _∷r_ : ∀ {name Fw MT} {nfc : All named-field-content MT} →
+    name comp↦ Fw ∈ store →
+    FieldsHavePointer store nfc →
+    FieldsHavePointer store {ReferenceType Fw ∷ MT} (name ∷ nfc)
 
 -- To limit references to only those that are valid for the current store,
 -- we have to prove that name in the message points to an inbox of the same
 -- type as the reference.
 -- Value messages are not context sensitive.
 message-valid : ∀ {IS} → Store → NamedMessage IS → Set₁
-message-valid store (NamedM x x₁) = all-fields-have-pointer store x₁
+message-valid store (NamedM x x₁) = FieldsHavePointer store x₁
 
 -- An inbox is valid in a store if all its messages are valid
 all-messages-valid : ∀ {IS} → Store → Inbox IS → Set₁
@@ -167,15 +172,6 @@ data InboxesValid (store : Store) : ∀ {store'} → Inboxes store' → Set₁ w
     InboxesValid store inboxes →
     InboxesValid store {inbox# name [ IS ] ∷ store'} (inbox ∷ inboxes)
 
--- A store entry is just an inbox without its messages.
--- We make this distinction so that updating the messages of a store
--- does not invalidate every pointer into the store.
--- inbox-to-store-entry : Inbox → NamedInbox
--- inbox-to-store-entry inb = inbox# (Inbox.name inb) [ Inbox.inbox-shape inb ]
-
--- inboxes-to-store : Inboxes → Store
--- inboxes-to-store = map inbox-to-store-entry
-
 -- A name is unused in a store if every inbox has a name that is < than the name
 NameFresh : Store → ℕ → Set₁
 NameFresh store n = All (λ v → name v Data.Nat.< n) store