From 2d07c5919997f17757af7e77acaca77d8771973a Mon Sep 17 00:00:00 2001
From: Eugene Akentyev <ak3ntev@gmail.com>
Date: Sat, 5 Nov 2016 17:58:34 +0300
Subject: [PATCH] Add t-notification

---
 src/Type.agda      |  3 +++
 src/Typecheck.agda | 21 +++++++++++++++++----
 2 files changed, 20 insertions(+), 4 deletions(-)

diff --git a/src/Type.agda b/src/Type.agda
index 20c4d8c..0490a32 100644
--- a/src/Type.agda
+++ b/src/Type.agda
@@ -51,5 +51,8 @@ data TypeDecl : Set where
   empty : TypeDecl
   pair : TypeDecl → TypeDecl → TypeDecl
 
+data _⊆_ : TypeTree → TypeTree → Set where
+  sub : {T₁ T₂ : TypeTree} → T₁ ⊆ T₂
+
 Ctx : ℕ → Set
 Ctx = Vec TypeDecl
diff --git a/src/Typecheck.agda b/src/Typecheck.agda
index 9dbd535..72e98b3 100644
--- a/src/Typecheck.agda
+++ b/src/Typecheck.agda
@@ -2,7 +2,7 @@ module Typecheck where
 
 import Data.Vec.Equality as VecEq
 open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
-open import Data.Nat using (ℕ)
+open import Data.Nat using (ℕ; _+_)
 open import Data.Vec using (Vec; _∈_; zip)
 open import Expr
 open import Type
@@ -33,14 +33,21 @@ data _⊢_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set
           ----------------------
           → Γ ⊢ while (var e) b ▹ Γ₁
           
-  t-choice : {Γ₁ : Ctx m} {k n : ℕ}  {η : Input_ex} {inputs : Vec Input_ex n} {b : Behaviour} {behaviours : Vec Behaviour n}
+  t-choice : {Γ₁ : Ctx m} {k n : ℕ}  {η : Input_ex} {inputs : Vec Input_ex n}
+             {b : Behaviour} {behaviours : Vec Behaviour n}
            → η ∈ inputs
            → b ∈ behaviours
            → Γ ⊢ seq (input η) b ▹ Γ₁
            --------------------------
            → Γ ⊢ inputchoice (zip inputs behaviours) ▹ Γ₁
 
-  --t-par
+  t-par : {k k₁ p p₁ : ℕ} {b1 b2 : Behaviour}
+          {Γ₁ : Ctx k} {Γ₁' : Ctx k₁} {Γ₂ : Ctx p} {Γ₂' : Ctx p₁} {Γ' : Ctx m}
+        → Γ₁ ⊢ b1 ▹ Γ₁'
+        → Γ₂ ⊢ b2 ▹ Γ₂'
+        -- TODO: Express that Γ = Γ₁, Γ₂ and Γ' = Γ₁', Γ₂' - disjoint unions
+        ---------------
+        → Γ ⊢ par b1 b2 ▹ Γ'
 
   t-seq : {k : ℕ} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour}
         → Γ ⊢ b1 ▹ Γ₁
@@ -48,4 +55,10 @@ data _⊢_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set
         --------------
         → Γ ⊢ seq b1 b2 ▹ Γ₂
 
-  
+  t-notification : {k : ℕ} {Γ₁ : Ctx m} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : TypeTree}
+                 → (outNotify o l T₀) ∈ Γ
+                 → Γ ⊢ e of Tₑ
+                 → Tₑ ⊆ T₀
+                 -------------
+                 → n ≡ m
+                 → Γ ⊢ output (notification o l (var e)) ▹ Γ₁
-- 
2.50.1