Eugene Akentyev
·
2017-01-19
TypingNetwork.agda
1module TypingNetwork where
2
3open import Relation.Nullary using (¬_)
4open import Data.Vec using (fromList) renaming (_∈_ to _∈-Vec_)
5open import Data.Product using (_,_)
6open import TypingService
7open import Service
8open import Network
9open import Type
10open import Behaviour
11
12
13data _⊢N_ : Context → Network → Set where
14 t-network-nil : {Γ : Context}
15 ------------
16 → Γ ⊢N nil
17
18 t-deployment : ∀ {m} {Γ : Context} {b : Behaviour} {l : Location} {o : Operation} {p : Process} {d : Deployment m} {Tₒ : Type}
19 → Γ ⊢S (b ▹ d - p)
20 → ¬ (outNotify o l Tₒ ∈ Γ)
21 --------------------------
22 → Γ ⊢N ([ b ▹ d - p ] l)
23
24 t-network : {Γ₁ Γ₂ : Context} {N₁ N₂ : Network} {l : Location}
25 → Γ₁ ⊢N N₁
26 → Γ₂ ⊢N N₂
27-- → , ¬ (l ∈ fromList (locs N₁))
28 → ¬ (l ∈-Vec fromList (locs N₂))
29 ----------------------
30 → & Γ₁ Γ₂ ⊢N (N₁ ∥ N₂)
31
32 t-restriction : {Γ : Context} {n : Network}
33 → Γ ⊢N n
34 -------------
35 → Γ ⊢N νr n