- commit
- 326ef04
- parent
- e4f03b5
- author
- Eugene Akentyev
- date
- 2017-01-18 17:52:44 +0400 +04
Update struct theorems and typing rules for network and service layers
3 files changed,
+23,
-23
+6,
-6
1@@ -217,15 +217,15 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
2 ------------------------
3 → Γ ⊢B exec r o x b ▹ Γ₁
4
5-struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b₁ b₂ : Behaviour}
6- → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁
7+struct-congruence : {Γ Γ₁ : Context} {b₁ b₂ : Behaviour}
8+ → Γ ⊢B b₁ ▹ Γ₁
9 → b₁ ≡ b₂
10- → ◆ Γ ⊢B b₂ ▹ ◆ Γ₁
11+ → Γ ⊢B b₂ ▹ Γ₁
12 struct-congruence t refl = t
13
14-struct-cong-par-nil : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b : Behaviour}
15- → ■ (◆ Γ₁) (◆ Γ₂) ⊢B (b ∥ nil) ▹ ■ (◆ Γ₁') (◆ Γ₂')
16- → ◆ Γ₁ ⊢B b ▹ ◆ Γ₁'
17+struct-cong-par-nil : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b : Behaviour}
18+ → ■ Γ₁ Γ₂ ⊢B (b ∥ nil) ▹ ■ Γ₁' Γ₂'
19+ → Γ₁ ⊢B b ▹ Γ₁'
20 struct-cong-par-nil (t-par x _) = x
21
22 struct-cong-par-sym : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b₁ b₂ : Behaviour}
+5,
-5
1@@ -11,15 +11,15 @@ open import Behaviour
2
3
4 data _⊢N_ : Context → Network → Set where
5- t-network-nil : ∀ {n} {Γ : Ctx n}
6+ t-network-nil : {Γ : Context}
7 ------------
8- → ◆ Γ ⊢N nil
9+ → Γ ⊢N nil
10
11- t-deployment : ∀ {n m} {Γ : Ctx n} {b : Behaviour} {l : Location} {o : Operation} {p : Process} {d : Deployment m} {Tₒ : Type}
12+ t-deployment : ∀ {m} {Γ : Context} {b : Behaviour} {l : Location} {o : Operation} {p : Process} {d : Deployment m} {Tₒ : Type}
13 → Γ ⊢S (b ▹ d - p)
14- → ¬ (outNotify o l Tₒ ∈ ◆ Γ)
15+ → ¬ (outNotify o l Tₒ ∈ Γ)
16 --------------------------
17- → ◆ Γ ⊢N ([ b ▹ d - p ] l)
18+ → Γ ⊢N ([ b ▹ d - p ] l)
19
20 t-network : ∀ {n} {m} {Γ₁ : Ctx n} {Γ₂ : Ctx m} {N₁ N₂ : Network} {l : Location}
21 → ◆ Γ₁ ⊢N N₁
+12,
-12
1@@ -13,35 +13,35 @@ open import Behaviour
2 open import Variable
3
4
5-data _⊢BSL_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
6- t-bsl-nil : ∀ {n} {Γ : Ctx n}
7+data _⊢BSL_▹_ : Context → Behaviour → Context → Set where
8+ t-bsl-nil : {Γ : Context}
9 ----------------
10 → Γ ⊢BSL nil ▹ Γ
11
12- t-bsl-choice : ∀ {n m k} {Γ : Ctx n} {contexts : Vec (Ctx m) k} {choices : List (η × Behaviour)} {Tₐ Tₓ : Type} {x : Variable}
13- → All (λ { (Γ₁ , (η , b)) → ◆ Γ ⊢B input η ∶ b ▹ ◆ Γ₁ }) (zip (toList contexts) choices)
14+ -- TODO
15+ t-bsl-choice : ∀ {m k} {Γ : Context} {contexts : Vec (Ctx m) k} {choices : List (η × Behaviour)} {Tₐ Tₓ : Type} {x : Variable}
16+ → All (λ { (Γ₁ , (η , b)) → Γ ⊢B input η ∶ b ▹ ◆ Γ₁ }) (zip (toList contexts) choices)
17 → ¬ (var x Tₓ ∈ ◆ (concat contexts))
18 → ¬ (var x Tₐ ∈ ◆ (concat contexts))
19 → Tₓ ≢ Tₐ
20 ----------------------------------------------
21- → Γ ⊢BSL inputchoice choices ▹ concat contexts
22+ → Γ ⊢BSL inputchoice choices ▹ ◆ (concat contexts)
23
24-data _⊢state_ : ∀ {n} → Ctx n → Process → Set where
25+data _⊢state_ : Context → Process → Set where
26
27-data _⊢P_ : ∀ {n} → Ctx n → Process → Set where
28- t-process-nil : ∀ {n} {Γ : Ctx n}
29+data _⊢P_ : Context → Process → Set where
30+ t-process-nil : {Γ : Context}
31 ----------
32 → Γ ⊢P nil
33
34- t-process-par : ∀ {n} {Γ : Ctx n} {p₁ p₂ : Process}
35+ t-process-par : {Γ : Context} {p₁ p₂ : Process}
36 → Γ ⊢P p₁
37 → Γ ⊢P p₂
38 ----------------
39 → Γ ⊢P (p₁ ∥ p₂)
40
41-
42-data _⊢S_ : ∀ {n} → Ctx n → Service → Set where
43- t-service : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx k} {b : Behaviour} {d : Deployment m} {p : Process}
44+data _⊢S_ : Context → Service → Set where
45+ t-service : ∀ {m} {Γ Γ₁ : Context} {b : Behaviour} {d : Deployment m} {p : Process}
46 → Γ ⊢BSL b ▹ Γ₁
47 → Γ ⊢P p
48 ------------------