- commit
- 2d07c59
- parent
- a27ccbf
- author
- Eugene Akentyev
- date
- 2016-11-05 18:58:34 +0400 +04
Add t-notification
2 files changed,
+20,
-4
+3,
-0
1@@ -51,5 +51,8 @@ data TypeDecl : Set where
2 empty : TypeDecl
3 pair : TypeDecl → TypeDecl → TypeDecl
4
5+data _⊆_ : TypeTree → TypeTree → Set where
6+ sub : {T₁ T₂ : TypeTree} → T₁ ⊆ T₂
7+
8 Ctx : ℕ → Set
9 Ctx = Vec TypeDecl
+17,
-4
1@@ -2,7 +2,7 @@ module Typecheck where
2
3 import Data.Vec.Equality as VecEq
4 open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
5-open import Data.Nat using (ℕ)
6+open import Data.Nat using (ℕ; _+_)
7 open import Data.Vec using (Vec; _∈_; zip)
8 open import Expr
9 open import Type
10@@ -33,14 +33,21 @@ data _⊢_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set
11 ----------------------
12 → Γ ⊢ while (var e) b ▹ Γ₁
13
14- t-choice : {Γ₁ : Ctx m} {k n : ℕ} {η : Input_ex} {inputs : Vec Input_ex n} {b : Behaviour} {behaviours : Vec Behaviour n}
15+ t-choice : {Γ₁ : Ctx m} {k n : ℕ} {η : Input_ex} {inputs : Vec Input_ex n}
16+ {b : Behaviour} {behaviours : Vec Behaviour n}
17 → η ∈ inputs
18 → b ∈ behaviours
19 → Γ ⊢ seq (input η) b ▹ Γ₁
20 --------------------------
21 → Γ ⊢ inputchoice (zip inputs behaviours) ▹ Γ₁
22
23- --t-par
24+ t-par : {k k₁ p p₁ : ℕ} {b1 b2 : Behaviour}
25+ {Γ₁ : Ctx k} {Γ₁' : Ctx k₁} {Γ₂ : Ctx p} {Γ₂' : Ctx p₁} {Γ' : Ctx m}
26+ → Γ₁ ⊢ b1 ▹ Γ₁'
27+ → Γ₂ ⊢ b2 ▹ Γ₂'
28+ -- TODO: Express that Γ = Γ₁, Γ₂ and Γ' = Γ₁', Γ₂' - disjoint unions
29+ ---------------
30+ → Γ ⊢ par b1 b2 ▹ Γ'
31
32 t-seq : {k : ℕ} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour}
33 → Γ ⊢ b1 ▹ Γ₁
34@@ -48,4 +55,10 @@ data _⊢_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set
35 --------------
36 → Γ ⊢ seq b1 b2 ▹ Γ₂
37
38-
39+ t-notification : {k : ℕ} {Γ₁ : Ctx m} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : TypeTree}
40+ → (outNotify o l T₀) ∈ Γ
41+ → Γ ⊢ e of Tₑ
42+ → Tₑ ⊆ T₀
43+ -------------
44+ → n ≡ m
45+ → Γ ⊢ output (notification o l (var e)) ▹ Γ₁