From 326ef04170ef42b0b19c482d6b7ca4a23f87c5a7 Mon Sep 17 00:00:00 2001
From: Eugene Akentyev <ak3ntev@gmail.com>
Date: Wed, 18 Jan 2017 16:52:44 +0300
Subject: [PATCH] Update struct theorems and typing rules for network and
 service layers

---
 src/TypingBehaviour.agda | 12 ++++++------
 src/TypingNetwork.agda   | 10 +++++-----
 src/TypingService.agda   | 24 ++++++++++++------------
 3 files changed, 23 insertions(+), 23 deletions(-)

diff --git a/src/TypingBehaviour.agda b/src/TypingBehaviour.agda
index 0d2aa3e..4cab90f 100644
--- 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 2313f3d..ad77cc3 100644
--- 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 ed364bc..efe748f 100644
--- 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
             ------------------
-- 
2.50.1