Make contexts great again

diff --git a/src/Type.agda b/src/Type.agda
index f5c31303ce8056aaba6d49ea725f8d703dad25a5..153acd398f44d385fceea12a40bebe6e9d0a5429 100644 (file)
--- a/src/Type.agda
+++ b/src/Type.agda
@@ -28,18 +28,15 @@ Ctx = Vec TypeDecl
 
 data Context : Set where
   ◆ : ∀ {n} → Ctx n → Context
-  ■ : ∀ {n m} → Ctx n → Ctx m → Context
+  ■ : Context → Context → Context
 
 infix 4 _∈_
 
 data _∈_ : TypeDecl → Context → Set where
   here-◆ : ∀ {n} {x} {xs : Ctx n} → x ∈ ◆ (x ∷-Vec xs)
   there-◆ : ∀ {n} {x y} {xs : Ctx n} (x∈xs : x ∈ ◆ xs) → x ∈ ◆ (y ∷-Vec xs)
-  here-left-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ ■ (x ∷-Vec xs) ys
-  here-right-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ ■ xs (x ∷-Vec ys)
-  there-left-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ ■ xs ys) → x ∈ ■ (x ∷-Vec xs) ys
-  there-right-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ ■ xs ys) → x ∈ ■ xs (x ∷-Vec ys)
-
-_∷_ : TypeDecl → Context → Context
-t ∷ ◆ xs = ◆ (t ∷-Vec xs)
-x ∷ ■ xs ys = ■ (x ∷-Vec xs) ys
+  here-left-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ ■  (◆ (x ∷-Vec xs)) (◆ ys)
+  here-right-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ ■ (◆ xs) (◆ (x ∷-Vec ys))
+  there-left-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ ■ (◆ xs) (◆ ys)) → x ∈ ■ (◆ (x ∷-Vec xs)) (◆ ys)
+  there-right-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ ■ (◆ xs) (◆ ys)) → x ∈ ■ (◆ xs) (◆ (x ∷-Vec ys))
+

diff --git a/src/TypingBehaviour.agda b/src/TypingBehaviour.agda
index 7d82a792cc914652ba161e233bae4562a2fdca3a..80afd960d1c6dcd621601fb9d6b45fcda5f2c640 100644 (file)
--- a/src/TypingBehaviour.agda
+++ b/src/TypingBehaviour.agda
@@ -5,7 +5,7 @@ open import Relation.Nullary using (¬_)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 open import Data.Nat using (ℕ)
 open import Data.List using (List)
-open import Data.Vec using ([]; _++_)
+open import Data.Vec using ([]; _++_; _∷_)
 open import Data.Product using (_,_; _×_)
 open import Function
 open import Expr
@@ -49,9 +49,9 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
            -----------------------------------
            → Γ ⊢B inputchoice choices ▹ Γ₁
 
-  t-par : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b1 b2 : Behaviour}
-        → ◆ Γ₁ ⊢B b1 ▹ ◆ Γ₁'
-        → ◆ Γ₂ ⊢B b2 ▹ ◆ Γ₂'
+  t-par : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b1 b2 : Behaviour}
+        → Γ₁ ⊢B b1 ▹ Γ₁'
+        → Γ₂ ⊢B b2 ▹ Γ₂'
         ------------------------------------
         → (■ Γ₁ Γ₂) ⊢B b1 ∥ b2 ▹ (■ Γ₁' Γ₂')
 
@@ -68,11 +68,11 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
                  ------------------------------------------------
                  → Γ ⊢B output (o at l [ var e ]) ▹ Γ
 
-  t-assign-new : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
-               → Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
-               → ¬ (var x Tₓ ∈ Γ) -- x ∉ Γ
+  t-assign-new : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
+               → ◆ Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
+               → ¬ (var x Tₓ ∈ ◆ Γ) -- x ∉ Γ
                --------------------------------------
-               → Γ ⊢B x ≃ e ▹ (var x Tₑ ∷ Γ)
+               → ◆ Γ ⊢B x ≃ e ▹ ◆ (var x Tₑ ∷ Γ)
 
   t-assign-exists : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
                   → Γ ⊢ₑ e ∶ Tₑ
@@ -81,11 +81,11 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
                   -------------------------
                   → Γ ⊢B x ≃ e ▹ Γ
 
-  t-oneway-new : {Γ : Context} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
-               → inOneWay o Tᵢ ∈ Γ
-               → ¬ (var x Tₓ ∈ Γ)
+  t-oneway-new : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
+               → inOneWay o Tᵢ ∈ ◆ Γ
+               → ¬ (var x Tₓ ∈ ◆ Γ)
                ---------------------------------------
-               → Γ ⊢B input (o [ x ]) ▹ (var x Tᵢ ∷ Γ)
+               → ◆ Γ ⊢B input (o [ x ]) ▹ ◆ (var x Tᵢ ∷ Γ)
 
   t-oneway-exists : {Γ : Context} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
                   → inOneWay o Tᵢ ∈ Γ
@@ -94,12 +94,12 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
                   --------------------------
                   → Γ ⊢B input (o [ x ]) ▹ Γ
 
-  t-solresp-new : {Γ : Context} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
-                → outSolRes o l Tₒ Tᵢ ∈ Γ
+  t-solresp-new : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
+                → outSolRes o l Tₒ Tᵢ ∈ ◆ Γ
                 → Tₑ ⊆ Tₒ
-                → ¬ (var x Tₓ ∈ Γ)
+                → ¬ (var x Tₓ ∈ ◆ Γ)
                 --------------------------------------------------
-                → Γ ⊢B output (o at l [ e ][ x ]) ▹ (var x Tᵢ ∷ Γ)
+                → ◆ Γ ⊢B output (o at l [ e ][ x ]) ▹ ◆ (var x Tᵢ ∷ Γ)
 
   t-solresp-exists : {Γ : Context} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
                    → outSolRes o l Tₒ Tᵢ ∈ Γ
@@ -109,14 +109,14 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
                    -------------------------------------
                    → Γ ⊢B output (o at l [ e ][ x ]) ▹ Γ
 
-  t-reqresp-new : {Γ Γ₁ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
-                → inReqRes o Tᵢ Tₒ ∈ Γ
-                → ¬ (var x Tₓ ∈ Γ)
-                → (var x Tₓ ∷ Γ) ⊢B b ▹ Γ₁
-                → var a Tₐ ∈ Γ₁
+  t-reqresp-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
+                → inReqRes o Tᵢ Tₒ ∈ ◆ Γ
+                → ¬ (var x Tₓ ∈ ◆ Γ)
+                → ◆ (var x Tₓ ∷ Γ) ⊢B b ▹ ◆ Γ₁
+                → var a Tₐ ∈ ◆ Γ₁
                 → Tₐ ⊆ Tₒ
                 ----------------------------------
-                → Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₁
+                → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ ◆ Γ₁
 
   t-reqresp-exists : {Γ Γ₁ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable}
                    → (inReqRes o Tᵢ Tₒ) ∈ Γ
@@ -128,11 +128,11 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
                    ----------------------------------
                    → Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₁
 
-  t-wait-new : {Γ : Context} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
-             → outSolRes o l Tₒ Tᵢ ∈ Γ
-             → ¬ (var x Tₓ ∈ Γ)
+  t-wait-new : ∀ {n} {Γ : Ctx n} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
+             → outSolRes o l Tₒ Tᵢ ∈ ◆ Γ
+             → ¬ (var x Tₓ ∈ ◆ Γ)
              ------------------------------------
-             → Γ ⊢B wait r o l x ▹ (var x Tᵢ ∷ Γ)
+             → ◆ Γ ⊢B wait r o l x ▹ ◆ (var x Tᵢ ∷ Γ)
 
   t-wait-exists : {Γ : Context} {Tₒ Tᵢ Tₓ : Type} {o : Operation} {l : Location} {r : Channel} {x : Variable}
                 → outSolRes o l Tₒ Tᵢ ∈ Γ
@@ -156,11 +156,11 @@ struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b₁ b₂ : Behaviou
 struct-congruence t refl = t
 
 struct-cong-par-nil : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b : Behaviour}
-                    → ■ Γ₁ Γ₂ ⊢B (b ∥ nil) ▹ ■ Γ₁' Γ₂'
+                    → ■ (◆ Γ₁) (◆ Γ₂) ⊢B (b ∥ nil) ▹ ■ (◆ Γ₁') (◆ Γ₂')
                     → ◆ Γ₁ ⊢B b ▹ ◆ Γ₁'
 struct-cong-par-nil (t-par x _) = x
 
---struct-cong-par-sym : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b₁ b₂ : Behaviour}
---                    → Γ₁ ++ Γ₂ ⊢B (b₁ ∥ b₂) ▹ Γ₁' ++ Γ₂'
---                    → Γ₂ ++ Γ₁ ⊢B (b₂ ∥ b₁) ▹ Γ₂' ++ Γ₁'
---struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁
+struct-cong-par-sym : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b₁ b₂ : Behaviour}
+                    → ■ Γ₁ Γ₂ ⊢B (b₁ ∥ b₂) ▹ ■ Γ₁' Γ₂'
+                    → ■ Γ₂ Γ₁ ⊢B (b₂ ∥ b₁) ▹ ■ Γ₂' Γ₁'
+struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁

diff --git a/src/TypingNetwork.agda b/src/TypingNetwork.agda
index be79b1ab7d917b5cb024df27cc88fa94a4c5fc7b..2313f3dd1b156c5db0574b7f22103282b4ef9228 100644 (file)
--- a/src/TypingNetwork.agda
+++ b/src/TypingNetwork.agda
@@ -1,7 +1,7 @@
 module TypingNetwork where
 
 open import Relation.Nullary using (¬_)
-open import Data.Vec using (_∈_; fromList)
+open import Data.Vec using (fromList) renaming (_∈_ to _∈-Vec_)
 open import Data.Product using (_,_)
 open import TypingService
 open import Service
@@ -17,7 +17,7 @@ data _⊢N_ : Context → Network → Set where
 
   t-deployment : ∀ {n m} {Γ : Ctx n} {b : Behaviour} {l : Location} {o : Operation} {p : Process} {d : Deployment m} {Tₒ : Type}
                → Γ ⊢S (b ▹ d - p)
-               → ¬ (outNotify o l Tₒ ∈ Γ)
+               → ¬ (outNotify o l Tₒ ∈ ◆ Γ)
                --------------------------
                → ◆ Γ ⊢N ([ b ▹ d - p ] l)
 
@@ -25,9 +25,9 @@ data _⊢N_ : Context → Network → Set where
             → ◆ Γ₁ ⊢N N₁
             → ◆ Γ₂ ⊢N N₂
 --            →  , ¬ (l ∈ fromList (locs N₁))
-            → ¬ (l ∈ fromList (locs N₂))
+            → ¬ (l ∈-Vec fromList (locs N₂))
             ----------------------
-            → ■ Γ₁ Γ₂ ⊢N (N₁ ∥ N₂)
+            → ■ (◆ Γ₁) (◆ Γ₂) ⊢N (N₁ ∥ N₂)
 
   t-restriction : ∀ {n} {Γ : Ctx n} {n : Network}
                 → ◆ Γ ⊢N n

diff --git a/src/TypingService.agda b/src/TypingService.agda
index eeefc58f5935c725c2c5034f392fab5e5d638623..ed364bc05dae3b0b697e5a185e121d83ea77ef3b 100644 (file)
--- a/src/TypingService.agda
+++ b/src/TypingService.agda
@@ -3,7 +3,7 @@ module TypingService where
 open import Relation.Binary.PropositionalEquality using (_≢_)
 open import Relation.Nullary using (¬_)
 open import Data.List.All using (All)
-open import Data.Vec using (Vec; toList; concat; _∈_)
+open import Data.Vec using (Vec; toList; concat) renaming (_∈_ to _∈-Vec)
 open import Data.List using (List; zip)
 open import Data.Product using (_×_; _,_)
 open import TypingBehaviour using (_⊢B_▹_)
@@ -20,8 +20,8 @@ data _⊢BSL_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
 
   t-bsl-choice : ∀ {n m k} {Γ : Ctx n} {contexts : Vec (Ctx m) k} {choices : List (η × Behaviour)} {Tₐ Tₓ : Type} {x : Variable}
                → All (λ { (Γ₁ , (η , b)) → ◆ Γ ⊢B input η ∶ b ▹ ◆ Γ₁ }) (zip (toList contexts) choices)
-               → ¬ (var x Tₓ ∈ concat contexts)
-               → ¬ (var x Tₐ ∈ concat contexts)
+               → ¬ (var x Tₓ ∈ ◆ (concat contexts))
+               → ¬ (var x Tₐ ∈ ◆ (concat contexts))
                → Tₓ ≢ Tₐ
                ----------------------------------------------
                → Γ ⊢BSL inputchoice choices ▹ concat contexts