- commit
- 82040fe
- parent
- a9f1698
- author
- Eugene Akentyev
- date
- 2017-01-18 16:52:02 +0400 +04
Make contexts great again
4 files changed,
+44,
-47
+6,
-9
1@@ -28,18 +28,15 @@ Ctx = Vec TypeDecl
2
3 data Context : Set where
4 ◆ : ∀ {n} → Ctx n → Context
5- ■ : ∀ {n m} → Ctx n → Ctx m → Context
6+ ■ : Context → Context → Context
7
8 infix 4 _∈_
9
10 data _∈_ : TypeDecl → Context → Set where
11 here-◆ : ∀ {n} {x} {xs : Ctx n} → x ∈ ◆ (x ∷-Vec xs)
12 there-◆ : ∀ {n} {x y} {xs : Ctx n} (x∈xs : x ∈ ◆ xs) → x ∈ ◆ (y ∷-Vec xs)
13- here-left-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ ■ (x ∷-Vec xs) ys
14- here-right-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ ■ xs (x ∷-Vec ys)
15- there-left-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ ■ xs ys) → x ∈ ■ (x ∷-Vec xs) ys
16- there-right-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ ■ xs ys) → x ∈ ■ xs (x ∷-Vec ys)
17-
18-_∷_ : TypeDecl → Context → Context
19-t ∷ ◆ xs = ◆ (t ∷-Vec xs)
20-x ∷ ■ xs ys = ■ (x ∷-Vec xs) ys
21+ here-left-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ ■ (◆ (x ∷-Vec xs)) (◆ ys)
22+ here-right-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ ■ (◆ xs) (◆ (x ∷-Vec ys))
23+ there-left-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ ■ (◆ xs) (◆ ys)) → x ∈ ■ (◆ (x ∷-Vec xs)) (◆ ys)
24+ there-right-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ ■ (◆ xs) (◆ ys)) → x ∈ ■ (◆ xs) (◆ (x ∷-Vec ys))
25+
+31,
-31
1@@ -5,7 +5,7 @@ open import Relation.Nullary using (¬_)
2 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
3 open import Data.Nat using (ℕ)
4 open import Data.List using (List)
5-open import Data.Vec using ([]; _++_)
6+open import Data.Vec using ([]; _++_; _∷_)
7 open import Data.Product using (_,_; _×_)
8 open import Function
9 open import Expr
10@@ -49,9 +49,9 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
11 -----------------------------------
12 → Γ ⊢B inputchoice choices ▹ Γ₁
13
14- t-par : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b1 b2 : Behaviour}
15- → ◆ Γ₁ ⊢B b1 ▹ ◆ Γ₁'
16- → ◆ Γ₂ ⊢B b2 ▹ ◆ Γ₂'
17+ t-par : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b1 b2 : Behaviour}
18+ → Γ₁ ⊢B b1 ▹ Γ₁'
19+ → Γ₂ ⊢B b2 ▹ Γ₂'
20 ------------------------------------
21 → (■ Γ₁ Γ₂) ⊢B b1 ∥ b2 ▹ (■ Γ₁' Γ₂')
22
23@@ -68,11 +68,11 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
24 ------------------------------------------------
25 → Γ ⊢B output (o at l [ var e ]) ▹ Γ
26
27- t-assign-new : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
28- → Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
29- → ¬ (var x Tₓ ∈ Γ) -- x ∉ Γ
30+ t-assign-new : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
31+ → ◆ Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
32+ → ¬ (var x Tₓ ∈ ◆ Γ) -- x ∉ Γ
33 --------------------------------------
34- → Γ ⊢B x ≃ e ▹ (var x Tₑ ∷ Γ)
35+ → ◆ Γ ⊢B x ≃ e ▹ ◆ (var x Tₑ ∷ Γ)
36
37 t-assign-exists : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
38 → Γ ⊢ₑ e ∶ Tₑ
39@@ -81,11 +81,11 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
40 -------------------------
41 → Γ ⊢B x ≃ e ▹ Γ
42
43- t-oneway-new : {Γ : Context} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
44- → inOneWay o Tᵢ ∈ Γ
45- → ¬ (var x Tₓ ∈ Γ)
46+ t-oneway-new : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
47+ → inOneWay o Tᵢ ∈ ◆ Γ
48+ → ¬ (var x Tₓ ∈ ◆ Γ)
49 ---------------------------------------
50- → Γ ⊢B input (o [ x ]) ▹ (var x Tᵢ ∷ Γ)
51+ → ◆ Γ ⊢B input (o [ x ]) ▹ ◆ (var x Tᵢ ∷ Γ)
52
53 t-oneway-exists : {Γ : Context} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
54 → inOneWay o Tᵢ ∈ Γ
55@@ -94,12 +94,12 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
56 --------------------------
57 → Γ ⊢B input (o [ x ]) ▹ Γ
58
59- t-solresp-new : {Γ : Context} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
60- → outSolRes o l Tₒ Tᵢ ∈ Γ
61+ t-solresp-new : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
62+ → outSolRes o l Tₒ Tᵢ ∈ ◆ Γ
63 → Tₑ ⊆ Tₒ
64- → ¬ (var x Tₓ ∈ Γ)
65+ → ¬ (var x Tₓ ∈ ◆ Γ)
66 --------------------------------------------------
67- → Γ ⊢B output (o at l [ e ][ x ]) ▹ (var x Tᵢ ∷ Γ)
68+ → ◆ Γ ⊢B output (o at l [ e ][ x ]) ▹ ◆ (var x Tᵢ ∷ Γ)
69
70 t-solresp-exists : {Γ : Context} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
71 → outSolRes o l Tₒ Tᵢ ∈ Γ
72@@ -109,14 +109,14 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
73 -------------------------------------
74 → Γ ⊢B output (o at l [ e ][ x ]) ▹ Γ
75
76- t-reqresp-new : {Γ Γ₁ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
77- → inReqRes o Tᵢ Tₒ ∈ Γ
78- → ¬ (var x Tₓ ∈ Γ)
79- → (var x Tₓ ∷ Γ) ⊢B b ▹ Γ₁
80- → var a Tₐ ∈ Γ₁
81+ t-reqresp-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
82+ → inReqRes o Tᵢ Tₒ ∈ ◆ Γ
83+ → ¬ (var x Tₓ ∈ ◆ Γ)
84+ → ◆ (var x Tₓ ∷ Γ) ⊢B b ▹ ◆ Γ₁
85+ → var a Tₐ ∈ ◆ Γ₁
86 → Tₐ ⊆ Tₒ
87 ----------------------------------
88- → Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₁
89+ → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ ◆ Γ₁
90
91 t-reqresp-exists : {Γ Γ₁ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable}
92 → (inReqRes o Tᵢ Tₒ) ∈ Γ
93@@ -128,11 +128,11 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
94 ----------------------------------
95 → Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₁
96
97- t-wait-new : {Γ : Context} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
98- → outSolRes o l Tₒ Tᵢ ∈ Γ
99- → ¬ (var x Tₓ ∈ Γ)
100+ t-wait-new : ∀ {n} {Γ : Ctx n} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
101+ → outSolRes o l Tₒ Tᵢ ∈ ◆ Γ
102+ → ¬ (var x Tₓ ∈ ◆ Γ)
103 ------------------------------------
104- → Γ ⊢B wait r o l x ▹ (var x Tᵢ ∷ Γ)
105+ → ◆ Γ ⊢B wait r o l x ▹ ◆ (var x Tᵢ ∷ Γ)
106
107 t-wait-exists : {Γ : Context} {Tₒ Tᵢ Tₓ : Type} {o : Operation} {l : Location} {r : Channel} {x : Variable}
108 → outSolRes o l Tₒ Tᵢ ∈ Γ
109@@ -156,11 +156,11 @@ struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b₁ b₂ : Behaviou
110 struct-congruence t refl = t
111
112 struct-cong-par-nil : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b : Behaviour}
113- → ■ Γ₁ Γ₂ ⊢B (b ∥ nil) ▹ ■ Γ₁' Γ₂'
114+ → ■ (◆ Γ₁) (◆ Γ₂) ⊢B (b ∥ nil) ▹ ■ (◆ Γ₁') (◆ Γ₂')
115 → ◆ Γ₁ ⊢B b ▹ ◆ Γ₁'
116 struct-cong-par-nil (t-par x _) = x
117
118---struct-cong-par-sym : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b₁ b₂ : Behaviour}
119--- → Γ₁ ++ Γ₂ ⊢B (b₁ ∥ b₂) ▹ Γ₁' ++ Γ₂'
120--- → Γ₂ ++ Γ₁ ⊢B (b₂ ∥ b₁) ▹ Γ₂' ++ Γ₁'
121---struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁
122+struct-cong-par-sym : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b₁ b₂ : Behaviour}
123+ → ■ Γ₁ Γ₂ ⊢B (b₁ ∥ b₂) ▹ ■ Γ₁' Γ₂'
124+ → ■ Γ₂ Γ₁ ⊢B (b₂ ∥ b₁) ▹ ■ Γ₂' Γ₁'
125+struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁
+4,
-4
1@@ -1,7 +1,7 @@
2 module TypingNetwork where
3
4 open import Relation.Nullary using (¬_)
5-open import Data.Vec using (_∈_; fromList)
6+open import Data.Vec using (fromList) renaming (_∈_ to _∈-Vec_)
7 open import Data.Product using (_,_)
8 open import TypingService
9 open import Service
10@@ -17,7 +17,7 @@ data _⊢N_ : Context → Network → Set where
11
12 t-deployment : ∀ {n m} {Γ : Ctx n} {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
19@@ -25,9 +25,9 @@ data _⊢N_ : Context → Network → Set where
20 → ◆ Γ₁ ⊢N N₁
21 → ◆ Γ₂ ⊢N N₂
22 -- → , ¬ (l ∈ fromList (locs N₁))
23- → ¬ (l ∈ fromList (locs N₂))
24+ → ¬ (l ∈-Vec fromList (locs N₂))
25 ----------------------
26- → ■ Γ₁ Γ₂ ⊢N (N₁ ∥ N₂)
27+ → ■ (◆ Γ₁) (◆ Γ₂) ⊢N (N₁ ∥ N₂)
28
29 t-restriction : ∀ {n} {Γ : Ctx n} {n : Network}
30 → ◆ Γ ⊢N n
+3,
-3
1@@ -3,7 +3,7 @@ module TypingService where
2 open import Relation.Binary.PropositionalEquality using (_≢_)
3 open import Relation.Nullary using (¬_)
4 open import Data.List.All using (All)
5-open import Data.Vec using (Vec; toList; concat; _∈_)
6+open import Data.Vec using (Vec; toList; concat) renaming (_∈_ to _∈-Vec)
7 open import Data.List using (List; zip)
8 open import Data.Product using (_×_; _,_)
9 open import TypingBehaviour using (_⊢B_▹_)
10@@ -20,8 +20,8 @@ data _⊢BSL_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
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- → ¬ (var x Tₓ ∈ concat contexts)
15- → ¬ (var x Tₐ ∈ concat contexts)
16+ → ¬ (var x Tₓ ∈ ◆ (concat contexts))
17+ → ¬ (var x Tₐ ∈ ◆ (concat contexts))
18 → Tₓ ≢ Tₐ
19 ----------------------------------------------
20 → Γ ⊢BSL inputchoice choices ▹ concat contexts