Update struct theorems and typing rules for network and service layers

diff --git a/src/TypingBehaviour.agda b/src/TypingBehaviour.agda
index 0d2aa3e8bba66e97acba25a2d7fa1810f11de799..4cab90f9e9d9a133599b3de5a4978995e8640e09 100644 (file)
--- a/src/TypingBehaviour.agda
+++ b/src/TypingBehaviour.agda
@@ -217,15 +217,15 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
          ------------------------
          → Γ ⊢B exec r o x b ▹ Γ₁
 
-struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b₁ b₂ : Behaviour}
-                  → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁
+struct-congruence : {Γ Γ₁ : Context} {b₁ b₂ : Behaviour}
+                  → Γ ⊢B b₁ ▹ Γ₁
                   → b₁ ≡ b₂
-                  → ◆ Γ ⊢B b₂ ▹ ◆ Γ₁
+                  → Γ ⊢B b₂ ▹ Γ₁
 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 ▹ ◆ Γ₁'
+struct-cong-par-nil : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b : Behaviour}
+                    → ■ Γ₁ Γ₂ ⊢B (b ∥ nil) ▹ ■ Γ₁' Γ₂'
+                    → Γ₁ ⊢B b ▹ Γ₁'
 struct-cong-par-nil (t-par x _) = x
 
 struct-cong-par-sym : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b₁ b₂ : Behaviour}

diff --git a/src/TypingNetwork.agda b/src/TypingNetwork.agda
index 2313f3dd1b156c5db0574b7f22103282b4ef9228..ad77cc35cb5bb1509481effc3d3c96f328a6bb2f 100644 (file)
--- a/src/TypingNetwork.agda
+++ b/src/TypingNetwork.agda
@@ -11,15 +11,15 @@ open import Behaviour
 
 
 data _⊢N_ : Context → Network → Set where
-  t-network-nil : ∀ {n} {Γ : Ctx n}
+  t-network-nil : {Γ : Context}
                 ------------
-                → ◆ Γ ⊢N nil
+                → Γ ⊢N nil
 
-  t-deployment : ∀ {n m} {Γ : Ctx n} {b : Behaviour} {l : Location} {o : Operation} {p : Process} {d : Deployment m} {Tₒ : Type}
+  t-deployment : ∀ {m} {Γ : Context} {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)
+               → Γ ⊢N ([ b ▹ d - p ] l)
 
   t-network : ∀ {n} {m} {Γ₁ : Ctx n} {Γ₂ : Ctx m} {N₁ N₂ : Network} {l : Location}
             → ◆ Γ₁ ⊢N N₁

diff --git a/src/TypingService.agda b/src/TypingService.agda
index ed364bc05dae3b0b697e5a185e121d83ea77ef3b..efe748ff9dcc0f01409231de56c1b69c9dd42082 100644 (file)
--- a/src/TypingService.agda
+++ b/src/TypingService.agda
@@ -13,35 +13,35 @@ open import Behaviour
 open import Variable
 
 
-data _⊢BSL_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
-  t-bsl-nil : ∀ {n} {Γ : Ctx n}
+data _⊢BSL_▹_ : Context → Behaviour → Context → Set where
+  t-bsl-nil : {Γ : Context}
             ----------------
             → Γ ⊢BSL nil ▹ Γ
 
-  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)
+  -- TODO
+  t-bsl-choice : ∀ {m k} {Γ : Context} {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))
                → Tₓ ≢ Tₐ
                ----------------------------------------------
-               → Γ ⊢BSL inputchoice choices ▹ concat contexts
+               → Γ ⊢BSL inputchoice choices ▹ ◆ (concat contexts)
 
-data _⊢state_ : ∀ {n} → Ctx n → Process → Set where
+data _⊢state_ : Context → Process → Set where
 
-data _⊢P_ : ∀ {n} → Ctx n → Process → Set where
-  t-process-nil : ∀ {n} {Γ : Ctx n}
+data _⊢P_ : Context → Process → Set where
+  t-process-nil : {Γ : Context}
                 ----------
                 → Γ ⊢P nil
 
-  t-process-par : ∀ {n} {Γ : Ctx n} {p₁ p₂ : Process}
+  t-process-par : {Γ : Context} {p₁ p₂ : Process}
                 → Γ ⊢P p₁
                 → Γ ⊢P p₂
                 ----------------
                 → Γ ⊢P (p₁ ∥ p₂)
 
-
-data _⊢S_ : ∀ {n} → Ctx n → Service → Set where
-  t-service : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx k} {b : Behaviour} {d : Deployment m} {p : Process}            
+data _⊢S_ : Context → Service → Set where
+  t-service : ∀ {m} {Γ Γ₁ : Context} {b : Behaviour} {d : Deployment m} {p : Process}            
             → Γ ⊢BSL b ▹ Γ₁
             → Γ ⊢P p
             ------------------