From 837b8c029d1faab7de5aab15066ca7d2f4a5afb5 Mon Sep 17 00:00:00 2001
From: Pierre Krafft <kpierre@outlook.com>
Date: Tue, 3 Apr 2018 19:05:12 +0200
Subject: [PATCH] Make FieldsHavePointer more list-like

---
 src/EnvironmentOperations.agda | 12 ++++++------
 src/SimulationEnvironment.agda | 13 +++++++------
 2 files changed, 13 insertions(+), 12 deletions(-)

diff --git a/src/EnvironmentOperations.agda b/src/EnvironmentOperations.agda
index 72fd0b1..d56a5c6 100644
--- a/src/EnvironmentOperations.agda
+++ b/src/EnvironmentOperations.agda
@@ -240,8 +240,8 @@ messages-valid-suc {store} {IS} {n} {x} {nx ∷ _} frsh (px ∷ vi) = message-va
       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)
+    fields-valid-suc (FhpV ∷ valid) = FhpV ∷ fields-valid-suc valid
+    fields-valid-suc (FhpR x ∷ valid) = FhpR (suc-p (suc-helper (actual-has-pointer x) frsh) x) ∷ (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 px
 
@@ -501,8 +501,8 @@ valid++ (NamedM x x₁) v = valid-fields v
                    All (reference-has-pointer store) p →
                    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)
+    valid-fields (FhpV ∷ fhp) ps = valid-fields fhp ps
+    valid-fields (FhpR px ∷ fhp) ps = px ∷ (valid-fields fhp ps)
 
 open _⊢>:_
 
@@ -528,8 +528,8 @@ make-pointers-compatible : ∀ {MT} store pre refs (eq : map shape refs ≡ pre)
                            (rhp : All (reference-has-pointer store) refs) →
                          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)
+make-pointers-compatible store _ refs refl (_∷_ {ValueType x} px fields) rhp = FhpV ∷ make-pointers-compatible store _ refs refl fields rhp
+make-pointers-compatible store _ refs refl (_∷_ {ReferenceType x} px fields) rhp = FhpR (make-pointer-compatible store x refs px rhp foundFw) ∷ (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/SimulationEnvironment.agda b/src/SimulationEnvironment.agda
index 277c98b..15a52db 100644
--- a/src/SimulationEnvironment.agda
+++ b/src/SimulationEnvironment.agda
@@ -143,15 +143,16 @@ 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
 
+data FieldHasPointer (store : Store) : ∀ {f} → named-field-content f → Set₁ where
+  FhpV : ∀ {A} {v : A} → FieldHasPointer store {ValueType A} v
+  FhpR : ∀ {name Fw} → name comp↦ Fw ∈ store → FieldHasPointer store {ReferenceType Fw} name
+
 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 →
+  _∷_ : ∀ {F p MT} {nfc : All named-field-content MT} →
+    FieldHasPointer store {F} p →
     FieldsHavePointer store nfc →
-    FieldsHavePointer store {ReferenceType Fw ∷ MT} (name ∷ nfc)
+    FieldsHavePointer store {F ∷ MT} (p ∷ 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