Add typing rules for cases with disjoint union

diff --git a/src/TypingBehaviour.agda b/src/TypingBehaviour.agda
index 80afd960d1c6dcd621601fb9d6b45fcda5f2c640..0d2aa3e8bba66e97acba25a2d7fa1810f11de799 100644 (file)
--- a/src/TypingBehaviour.agda
+++ b/src/TypingBehaviour.agda
@@ -28,25 +28,25 @@ data _⊢ₑ_∶_ (Γ : Context) : Expr → Type → Set where
 
 data _⊢B_▹_ : Context → Behaviour → Context → Set where
   t-nil : {Γ : Context}
-        ------------------
+        --------------
         → Γ ⊢B nil ▹ Γ
           
   t-if : {Γ Γ₁ : Context} {b₁ b₂ : Behaviour} {e : Expr}
        → Γ ⊢ₑ e ∶ bool -- Γ ⊢ e : bool
        → Γ ⊢B b₁ ▹ Γ₁
        → Γ ⊢B b₂ ▹ Γ₁
-       --------------------------
+       --------------------------------
        → Γ ⊢B if e then b₁ else b₂ ▹ Γ₁
           
   t-while : {Γ : Context} {b : Behaviour} {e : Expr} 
           → Γ ⊢ₑ e ∶ bool
           → Γ ⊢B b ▹ Γ
-          ------------------------
+          -----------------------
           → Γ ⊢B while[ e ] b ▹ Γ
           
   t-choice : {Γ Γ₁ : Context} {choices : List (η × Behaviour)}
            → All (λ { (η , b) → Γ ⊢B (input η) ∶ b ▹ Γ₁ }) choices
-           -----------------------------------
+           -------------------------------
            → Γ ⊢B inputchoice choices ▹ Γ₁
 
   t-par : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b1 b2 : Behaviour}
@@ -58,35 +58,59 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
   t-seq : {Γ Γ₁ Γ₂ : Context} {b₁ b₂ : Behaviour}
         → Γ ⊢B b₁ ▹ Γ₁
         → Γ₁ ⊢B b₂ ▹ Γ₂
-        -----------------------
+        -------------------
         → Γ ⊢B b₁ ∶ b₂ ▹ Γ₂
 
   t-notification : {Γ : Context} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
                  → (outNotify o l T₀) ∈ Γ
                  → var e Tₑ ∈ Γ
                  → Tₑ ⊆ T₀
-                 ------------------------------------------------
+                 ------------------------------------
                  → Γ ⊢B output (o at l [ var e ]) ▹ Γ
 
   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ₑ ∷ Γ)
 
+  t-assign-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m}  {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
+                    → ■ (◆ Γ) (◆ Γ₁) ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
+                    → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁)) -- x ∉ Γ
+                    -------------------------------------------------------
+                    → ■ (◆ Γ) (◆ Γ₁) ⊢B x ≃ e ▹ ■ (◆ (var x Tₑ ∷ Γ)) (◆ Γ₁)
+
+  t-assign-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m}  {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
+                     → ■ (◆ Γ) (◆ Γ₁) ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
+                     → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁)) -- x ∉ Γ
+                     ------------------------------------------------------
+                     → ■ (◆ Γ) (◆ Γ₁) ⊢B x ≃ e ▹ ■ (◆ Γ) (◆ (var x Tₑ ∷ Γ₁))
+
   t-assign-exists : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
                   → Γ ⊢ₑ e ∶ Tₑ
                   → var x Tₓ ∈ Γ
                   → Tₑ ≡ Tₓ
-                  -------------------------
+                  ----------------
                   → Γ ⊢B x ≃ e ▹ Γ
 
   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ᵢ ∷ Γ)
 
+  t-oneway-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
+                    → inOneWay o Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁)
+                    → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
+                    -----------------------------------------------------------------
+                    → ■ (◆ Γ) (◆ Γ₁) ⊢B input (o [ x ]) ▹ ■ (◆ (var x Tᵢ ∷ Γ)) (◆ Γ₁)
+
+  t-oneway-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
+                     → inOneWay o Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁)
+                     → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
+                     -----------------------------------------------------------------
+                     → ■ (◆ Γ) (◆ Γ₁) ⊢B input (o [ x ]) ▹ ■ (◆ Γ) (◆ (var x Tᵢ ∷ Γ₁))
+
   t-oneway-exists : {Γ : Context} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
                   → inOneWay o Tᵢ ∈ Γ
                   → var x Tₓ ∈ Γ
@@ -98,9 +122,23 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
                 → outSolRes o l Tₒ Tᵢ ∈ ◆ Γ
                 → Tₑ ⊆ Tₒ
                 → ¬ (var x Tₓ ∈ ◆ Γ)
-                --------------------------------------------------
+                ------------------------------------------------------
                 → ◆ Γ ⊢B output (o at l [ e ][ x ]) ▹ ◆ (var x Tᵢ ∷ Γ)
 
+  t-solresp-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
+                     → outSolRes o l Tₒ Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁)
+                     → Tₑ ⊆ Tₒ
+                     → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
+                     ----------------------------------------------------------------------------
+                     → ■ (◆ Γ) (◆ Γ₁) ⊢B output (o at l [ e ][ x ]) ▹ ■ (◆ (var x Tᵢ ∷ Γ)) (◆ Γ₁)
+
+  t-solresp-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
+                      → outSolRes o l Tₒ Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁)
+                      → Tₑ ⊆ Tₒ
+                      → ¬ (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ᵢ ∈ Γ
                    → Tₑ ⊆ Tₒ
@@ -115,9 +153,27 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
                 → ◆ (var x Tₓ ∷ Γ) ⊢B b ▹ ◆ Γ₁
                 → var a Tₐ ∈ ◆ Γ₁
                 → Tₐ ⊆ Tₒ
-                ----------------------------------
+                --------------------------------------
                 → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ ◆ Γ₁
 
+  t-reqresp-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Γ₂ : 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ₐ ⊆ Tₒ
+                     ------------------------------------
+                     → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₂
+
+  t-reqresp-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Γ₂ : 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ₐ ⊆ Tₒ
+                      ------------------------------------
+                      → ◆ Γ ⊢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ₒ) ∈ Γ
                    → var x Tₓ ∈ Γ
@@ -131,9 +187,21 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
   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ᵢ ∷ Γ)
 
+  t-wait-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {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ᵢ ∷ Γ)) (◆ Γ₁)
+
+  t-wait-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {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ᵢ ∷ Γ₁))
+
   t-wait-exists : {Γ : Context} {Tₒ Tᵢ Tₓ : Type} {o : Operation} {l : Location} {r : Channel} {x : Variable}
                 → outSolRes o l Tₒ Tᵢ ∈ Γ
                 → var x Tₓ ∈ Γ