Add t-bsl-choice

diff --git a/src/TypingBehaviour.agda b/src/TypingBehaviour.agda
index ee808692b2509b4349fb5f60c6222b00af6e7b17..642c23f60ecad267e6bf3212c2e792c2453b482e 100644 (file)
--- a/src/TypingBehaviour.agda
+++ b/src/TypingBehaviour.agda
@@ -14,8 +14,12 @@ open import Behaviour
 open import Variable
 
 
+-- Side effect
 data _⊢_↦_⊢_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Behaviour → Set where
+  -- Updated
   upd : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b₁ b₂ : Behaviour} → Γ ⊢ b₁ ↦ Γ₁ ⊢ b₂
+
+  -- Identity
   idn : ∀ {n} {Γ : Ctx n} {b : Behaviour} → Γ ⊢ b ↦ Γ ⊢ b
 
 data _⊢ₑ_∶_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where
@@ -49,12 +53,11 @@ 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 ▹ ◆ Γ₂'
-       --------------------------------------
-       → (■ Γ₁ Γ₂) ⊢B b1 ∥ b2 ▹ (■ Γ₁' Γ₂')
+  t-par : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b1 b2 : Behaviour}
+        → ◆ Γ₁ ⊢B b1 ▹ ◆ Γ₁'
+        → ◆ Γ₂ ⊢B b2 ▹ ◆ Γ₂'
+        --------------------------------------
+        → (■ Γ₁ Γ₂) ⊢B b1 ∥ b2 ▹ (■ Γ₁' Γ₂')
 
   t-seq : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b₁ b₂ : Behaviour}
         → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁

diff --git a/src/TypingService.agda b/src/TypingService.agda
index 9da969e27e9f8744081e2ba4ca010103d2a1731a..7e2dc36295f46c5a33126f71bc38a660ce6b1500 100644 (file)
--- a/src/TypingService.agda
+++ b/src/TypingService.agda
@@ -1,12 +1,16 @@
 module TypingService where
 
+open import Relation.Binary.PropositionalEquality using (_≢_)
+open import Relation.Nullary using (¬_)
 open import Data.List.All using (All)
-open import Data.List using (List)
+open import Data.Vec using (Vec; toList; concat; _∈_)
+open import Data.List using (List; zip)
 open import Data.Product using (_×_; _,_)
-open import TypingBehaviour using (_⊢B_▹_)
+open import TypingBehaviour using (_⊢B_▹_; ◆)
 open import Type
 open import Service
 open import Behaviour
+open import Variable
 
 
 data _⊢BSL_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
@@ -14,10 +18,13 @@ data _⊢BSL_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
             ----------------
             → Γ ⊢BSL nil ▹ Γ
 
--- TODO: finish
---  t-bsl-choice : ∀ {n} {Γ : Ctx n} {Γ₁ : Ctx n} {choices : List (Input_ex × Behaviour)}
---               → All (λ { (η , b) → Γ ⊢B seq (input η) b ▹ Γ₁ }) choices
---               → Γ ⊢BSL 
+  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)
+               → Tₓ ≢ Tₐ
+               ----------------------------------------------
+               → Γ ⊢BSL inputchoice choices ▹ concat contexts
 
 data _⊢state_ : ∀ {n} → Ctx n → Process → Set where
 
@@ -30,7 +37,7 @@ data _⊢P_ : ∀ {n} → Ctx n → Process → Set where
                 → Γ ⊢P p₁
                 → Γ ⊢P p₂
                 ----------------
-                → Γ ⊢P par p₁ p₂
+                → Γ ⊢P (p₁ ∥ p₂)
 
 
 data _⊢S_ : ∀ {n} → Ctx n → Service → Set where