Eugene Akentyev
·
2017-01-19
TypingService.agda
1module TypingService where
2
3open import Relation.Binary.PropositionalEquality using (_≢_)
4open import Relation.Nullary using (¬_)
5open import Data.List.All using (All)
6open import Data.Vec using (Vec; toList; concat) renaming (_∈_ to _∈-Vec)
7open import Data.List using (List; zip)
8open import Data.Product using (_×_; _,_)
9open import TypingBehaviour using (_⊢B_▹_)
10open import Type
11open import Service
12open import Behaviour
13open import Variable
14
15
16data _⊢BSL_▹_ : Context → Behaviour → Context → Set where
17 t-bsl-nil : {Γ : Context}
18 ----------------
19 → Γ ⊢BSL nil ▹ Γ
20
21 -- TODO
22 t-bsl-choice : ∀ {m k} {Γ : Context} {contexts : Vec (Ctx m) k} {choices : List (η × Behaviour)} {Tₐ Tₓ : Type} {x : Variable}
23 → All (λ { (Γ₁ , (η , b)) → Γ ⊢B input η ∶ b ▹ ⋆ Γ₁ }) (zip (toList contexts) choices)
24 → ¬ (var x Tₓ ∈ ⋆ (concat contexts))
25 → ¬ (var x Tₐ ∈ ⋆ (concat contexts))
26 → Tₓ ≢ Tₐ
27 ----------------------------------------------
28 → Γ ⊢BSL inputchoice choices ▹ ⋆ (concat contexts)
29
30data _⊢state_ : Context → Process → Set where
31
32data _⊢P_ : Context → Process → Set where
33 t-process-nil : {Γ : Context}
34 ----------
35 → Γ ⊢P nil
36
37 t-process-par : {Γ : Context} {p₁ p₂ : Process}
38 → Γ ⊢P p₁
39 → Γ ⊢P p₂
40 ----------------
41 → Γ ⊢P (p₁ ∥ p₂)
42
43data _⊢S_ : Context → Service → Set where
44 t-service : ∀ {m} {Γ Γ₁ : Context} {b : Behaviour} {d : Deployment m} {p : Process}
45 → Γ ⊢BSL b ▹ Γ₁
46 → Γ ⊢P p
47 ------------------
48 → Γ ⊢S (b ▹ d - p)