Added disjoint union

diff --git a/src/TypingBehaviour.agda b/src/TypingBehaviour.agda
index efef10ef3ff108003b362d434e820f60e732256a..73fea3695f2f9e33391a06234a6efe7193c4d2d7 100644 (file)
--- a/src/TypingBehaviour.agda
+++ b/src/TypingBehaviour.agda
@@ -24,82 +24,85 @@ data _⊢ₑ_∶_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where
   expr-t : {s : Expr} {b : Type}
          → Γ ⊢ₑ s ∶ b
 
-data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
+data Context : Set where
+  ◆ : ∀ {n} → Ctx n → Context
+  ■ : ∀ {n m} → Ctx n → Ctx m → Context
+
+data _⊢B_▹_ : Context → Behaviour → Context → Set where
   t-nil : ∀ {n} {Γ : Ctx n}
         --------------
-        → Γ ⊢B nil ▹ Γ
+        → ◆ Γ ⊢B nil ▹ ◆ Γ
           
   t-if : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Expr}
        → Γ ⊢ₑ e ∶ bool -- Γ ⊢ e : bool
-       → Γ ⊢B b1 ▹ Γ₁
-       → Γ ⊢B b2 ▹ Γ₁
+       → ◆ Γ ⊢B b1 ▹ ◆ Γ₁
+       → ◆ Γ ⊢B b2 ▹ ◆ Γ₁
        ----------------------
-       → Γ ⊢B if e b1 b2 ▹ Γ₁
+       → ◆ Γ ⊢B if e b1 b2 ▹ ◆ Γ₁
           
   t-while : ∀ {n} {Γ : Ctx n} {b : Behaviour} {e : Expr} 
           → Γ ⊢ₑ e ∶ bool
-          → Γ ⊢B b ▹ Γ
+          → ◆ Γ ⊢B b ▹ ◆ Γ
           ---------------------
-          → Γ ⊢B while e b ▹ Γ
+          → ◆ Γ ⊢B while e b ▹ ◆ Γ
           
   t-choice : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {choices : List (Input_ex × Behaviour)}
-           → All (λ { (η , b) → Γ ⊢B seq (input η) b ▹ Γ₁ }) choices
+           → All (λ { (η , b) → ◆ Γ ⊢B seq (input η) b ▹ ◆ Γ₁ }) choices
            -------------------------------
-           → Γ ⊢B inputchoice choices ▹ Γ₁
+           → ◆ Γ ⊢B inputchoice choices ▹ ◆ Γ₁
 
-  t-par : ∀ {n m} {Γ : Ctx n} {k k₁ p p₁ : ℕ} {b1 b2 : Behaviour}
-          {Γ₁ : Ctx k} {Γ₁' : Ctx k₁} {Γ₂ : Ctx p} {Γ₂' : Ctx p₁} {Γ' : Ctx m}
-        → Γ₁ ⊢B b1 ▹ Γ₁'
-        → Γ₂ ⊢B b2 ▹ Γ₂'
-        -- TODO: maybe it's not enough to express that Γ = Γ₁, Γ₂ and Γ' = Γ₁', Γ₂' - disjoint unions
-        ----------------------------------------
-        → (Γ₁ ++ Γ₂) ⊢B par b1 b2 ▹ (Γ₁' ++ Γ₂')
+  t-par : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁}
+          {b1 b2 : Behaviour}
+       → ◆ Γ₁ ⊢B b1 ▹ ◆ Γ₁'
+       → ◆ Γ₂ ⊢B b2 ▹ ◆ Γ₂'
+       --------------------------------------
+       → (■ Γ₁ Γ₂) ⊢B par b1 b2 ▹ (■ Γ₁' Γ₂')
 
   t-seq : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour}
-        → Γ ⊢B b1 ▹ Γ₁
-        → Γ₁ ⊢B b2 ▹ Γ₂
+        → ◆ Γ ⊢B b1 ▹ ◆ Γ₁
+        → ◆ Γ₁ ⊢B b2 ▹ ◆ Γ₂
         ---------------------
-        → Γ ⊢B seq b1 b2 ▹ Γ₂
+        → ◆ Γ ⊢B seq b1 b2 ▹ ◆ Γ₂
 
   t-notification : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
                  → (outNotify o l T₀) ∈ Γ
                  → Γ ⊢ e ∶ Tₑ
                  → Tₑ ⊆ T₀
                  ---------------------------------------------
-                 → Γ ⊢B output (notification o l (var e)) ▹ Γ
+                 → ◆ Γ ⊢B output (notification o 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 assign x e ▹ (var x Tₑ ∷ Γ)
+               → ◆ Γ ⊢B assign x e ▹ ◆ (var x Tₑ ∷ Γ)
 
   t-assign-exists : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
                   → Γ ⊢ₑ e ∶ Tₑ
                   → var x Tₓ ∈ Γ
                   → Tₑ ≡ Tₓ
                   ----------------------
-                  → Γ ⊢B assign x e ▹ Γ
+                  → ◆ Γ ⊢B assign x e ▹ ◆ Γ
 
   t-oneway-new : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
                → inOneWay o Tᵢ ∈ Γ
                → ¬ (var x Tₓ ∈ Γ)
                ------------------------------------------
-               → Γ ⊢B input (oneway o x) ▹ (var x Tᵢ ∷ Γ)
+               → ◆ Γ ⊢B input (oneway o x) ▹ ◆ (var x Tᵢ ∷ Γ)
 
   t-oneway-exists : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
                   → inOneWay o Tᵢ ∈ Γ
                   → var x Tₓ ∈ Γ
                   → Tᵢ ⊆ Tₓ
                   ------------------------------
-                  → Γ ⊢B input (oneway o x) ▹ Γ
+                  → ◆ Γ ⊢B input (oneway o x) ▹ ◆ Γ
 
   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ₓ ∈ Γ)
                 --------------------------------------------------
-                → Γ ⊢B output (solicitres o l e x) ▹ (var x Tᵢ ∷ Γ)
+                → ◆ Γ ⊢B output (solicitres o l e x) ▹ ◆ (var x Tᵢ ∷ Γ)
 
   t-solresp-exists : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
                    → outSolRes o l Tₒ Tᵢ ∈ Γ
@@ -107,70 +110,67 @@ data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
                    → var x Tₓ ∈ Γ
                    → Tᵢ ⊆ Tₓ
                    ---------------------------------------
-                   → Γ ⊢B output (solicitres o l e x) ▹ Γ
+                   → ◆ Γ ⊢B output (solicitres o l e x) ▹ ◆ Γ
 
   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 x Tₓ ∷ Γ) ⊢B b ▹ ◆ Γ₁
                 → var a Tₐ ∈ Γ₁
                 → Tₐ ⊆ Tₒ
                 ----------------------------------
-                → Γ ⊢B input (reqres o x a b) ▹ Γ₁
+                → ◆ Γ ⊢B input (reqres o x a b) ▹ ◆ Γ₁
 
   t-reqresp-exists : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable}
                    → (inReqRes o Tᵢ Tₒ) ∈ Γ
                    → var x Tₓ ∈ Γ
                    → Tᵢ ⊆ Tₓ
-                   → Γ ⊢B b ▹ Γ₁
+                   → ◆ Γ ⊢B b ▹ ◆ Γ₁
                    → var a Tₐ ∈ Γ₁
                    → Tₐ ⊆ Tₒ
                    ----------------------------------
-                   → Γ ⊢B input (reqres o x a b) ▹ Γ₁
+                   → ◆ Γ ⊢B input (reqres o x a b) ▹ ◆ Γ₁
 
   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 : ∀ {n} {Γ : Ctx n} {Tₒ Tᵢ Tₓ : Type} {o : Operation} {l : Location} {r : Channel} {x : Variable}
                 → outSolRes o l Tₒ Tᵢ ∈ Γ
                 → var x Tₓ ∈ Γ
                 → Tᵢ ⊆ Tₓ
                 ------------------------
-                → Γ ⊢B wait r o l x ▹ Γ
+                → ◆ Γ ⊢B wait r o l x ▹ ◆ Γ
 
   t-exec : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₒ Tᵢ Tₓ : Type} {b : Behaviour} {r : Channel} {o : Operation} {x : Variable}
          → inReqRes o Tᵢ Tₒ ∈ Γ
-         → Γ ⊢B b ▹ Γ₁
+         → ◆ Γ ⊢B b ▹ ◆ Γ₁
          → var x Tₓ ∈ Γ
          → Tₓ ⊆ Tₒ
          ------------------------
-         → Γ ⊢B exec r o x b ▹ Γ₁
+         → ◆ Γ ⊢B exec r o x b ▹ ◆ Γ₁
 
-struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → Γ ⊢B b1 ▹ Γ₁ → b1 ≡ b2 → Γ ⊢B b2 ▹ Γ₁
+struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → ◆ Γ ⊢B b1 ▹ ◆ Γ₁ → b1 ≡ b2 → ◆ Γ ⊢B b2 ▹ ◆ Γ₁
 struct-congruence t refl = t
 
-struct-cong-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B (seq nil b) ▹ Γ₁ → Γ ⊢B b ▹ Γ₁
+struct-cong-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B (seq nil b) ▹ ◆ Γ₁ → ◆ Γ ⊢B b ▹ ◆ Γ₁
 struct-cong-nil (t-seq t-nil t) = t
 
---struct-cong-par-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B (par b nil) ▹ Γ₁ → Γ ⊢B b ▹ Γ₁
---struct-cong-par-nil (t-par t t-nil) = {!!}
-
---struct-cong-par-sym : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → Γ ⊢B (par b1 b2) ▹ Γ₁ → Γ ⊢B (par b2 b1) ▹ Γ₁
---struct-cong-par-sym (t-par t₁ t₂) = {!!}
+struct-cong-par-nil : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b : Behaviour} → ■ Γ₁ Γ₂ ⊢B (par b nil) ▹ ■ Γ₁' Γ₂' → ◆ Γ₁ ⊢B b ▹ ◆ Γ₁'
+struct-cong-par-nil (t-par t t-nil) = t
 
---struct-cong-par-assoc : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 b3 : Behaviour} → Γ ⊢B par (par b1 b2) b3 ▹ Γ₁ → Γ ⊢B par b1 (par b2 b3) ▹ Γ₁
---struct-cong-par-assoc (t-par (t-par t₁ t₂) t₃) = {!!}
+struct-cong-par-sym : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b1 b2 : Behaviour} → ■ Γ₁ Γ₂ ⊢B (par b1 b2) ▹ ■ Γ₁' Γ₂' → ■ Γ₂ Γ₁ ⊢B (par b2 b1) ▹ ■ Γ₂' Γ₁'
+struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁
 
 data SideEffect : ∀ {n m} → Ctx n → Ctx m → Set where
   updated : ∀ {n m} → (Γ : Ctx n) → (Γ₁ : Ctx m) → SideEffect Γ Γ₁
   identity : ∀ {n} → (Γ : Ctx n) → SideEffect Γ Γ
   undefined : SideEffect [] []
 
---preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B b ▹ Γ₁ → SideEffect Γ Γₐ → Γₐ ⊢B b ▹ Γ₁
---preservation t undefined = t
---preservation t (identity γ) = t
---preservation t-nil (updated {_} {k} Γ Γₐ) = t-nil {k} {Γₐ}
---preservation = {!!}
+preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B b ▹ ◆ Γ₁ → SideEffect Γ Γₐ → ◆ Γₐ ⊢B b ▹ ◆ Γ₁
+preservation t undefined = t
+preservation t (identity γ) = t
+--preservation t-nil (updated {_} {k} Γ Γₐ) = {!!}
+preservation = {!!}

diff --git a/src/TypingService.agda b/src/TypingService.agda
index 1eb1d4eb44bc135bbb0cd361baa71bfb3b87f92e..0006a18490b42fd5c1df20b75fb239ce822bc2ff 100644 (file)
--- a/src/TypingService.agda
+++ b/src/TypingService.agda
@@ -18,6 +18,8 @@ data _⊢BSL_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
 --               → All (λ { (η , b) → Γ ⊢B seq (input η) b ▹ Γ₁ }) choices
 --               → Γ ⊢BSL 
 
+data _⊢state_ : ∀ {n} → Ctx n → Process → Set where
+
 data _⊢P_ : ∀ {n} → Ctx n → Process → Set where
   t-process-nil : ∀ {n} {Γ : Ctx n}
                 ----------
@@ -29,6 +31,7 @@ data _⊢P_ : ∀ {n} → Ctx n → Process → Set where
                 ----------------
                 → Γ ⊢P par p₁ p₂
 
+
 data _⊢S_ : ∀ {n} → Ctx n → Service → Set where
   t-service : ∀ {n m} {Γ : Ctx n} {b : Behaviour} {d : Deployment m} {p : Process}
             ------------------