Add t-notification

diff --git a/src/Type.agda b/src/Type.agda
index 20c4d8c2c431c8364f074002a620d513669422ee..0490a328f3dfc7d640b683c4f93224f97fbd1d34 100644 (file)
--- 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 9dbd535b02d41e3a4c2f3f59de26899b9f2a6a0e..72e98b3f02b6fdb6931ddcf7ea0398e82db63bfb 100644 (file)
--- 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)) ▹ Γ₁