- commit
- a9f1698
- parent
- eacd202
- author
- Eugene Akentyev
- date
- 2017-01-18 09:06:25 +0400 +04
Expand behaviour's typing rules. Add network and service typing rules.
5 files changed,
+119,
-100
+7,
-0
1@@ -1,5 +1,6 @@
2 module Network where
3
4+open import Data.List using (List; []; [_]; _++_)
5 open import Type
6 open import Service
7
8@@ -9,3 +10,9 @@ data Network : Set where
9 νr : Network → Network
10 _∥_ : Network → Network → Network
11 nil : Network
12+
13+locs : Network → List Location
14+locs (νr n) = locs n
15+locs (n₁ ∥ n₂) = locs n₁ ++ locs n₂
16+locs nil = []
17+locs ([ s ] l) = [ l ]
+22,
-9
1@@ -2,18 +2,13 @@ module Type where
2
3 open import Data.Nat using (ℕ)
4 open import Data.String using (String)
5-open import Data.Vec using (Vec)
6+open import Data.Vec using (Vec) renaming (_∷_ to _∷-Vec_)
7 open import Variable
8
9
10-Operation : Set
11-Operation = String
12-
13-Location : Set
14-Location = String
15-
16-Channel : Set
17-Channel = String
18+data Operation : Set where
19+data Location : Set where
20+data Channel : Set where
21
22 data Type : Set where
23 bool int double long string raw void : Type
24@@ -30,3 +25,21 @@ data _⊆_ : Type → Type → Set where
25
26 Ctx : ℕ → Set
27 Ctx = Vec TypeDecl
28+
29+data Context : Set where
30+ ◆ : ∀ {n} → Ctx n → Context
31+ ■ : ∀ {n m} → Ctx n → Ctx m → Context
32+
33+infix 4 _∈_
34+
35+data _∈_ : TypeDecl → Context → Set where
36+ here-◆ : ∀ {n} {x} {xs : Ctx n} → x ∈ ◆ (x ∷-Vec xs)
37+ there-◆ : ∀ {n} {x y} {xs : Ctx n} (x∈xs : x ∈ ◆ xs) → x ∈ ◆ (y ∷-Vec xs)
38+ here-left-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ ■ (x ∷-Vec xs) ys
39+ here-right-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ ■ xs (x ∷-Vec ys)
40+ there-left-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ ■ xs ys) → x ∈ ■ (x ∷-Vec xs) ys
41+ there-right-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ ■ xs ys) → x ∈ ■ xs (x ∷-Vec ys)
42+
43+_∷_ : TypeDecl → Context → Context
44+t ∷ ◆ xs = ◆ (t ∷-Vec xs)
45+x ∷ ■ xs ys = ■ (x ∷-Vec xs) ys
+60,
-82
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 (_∈_; []; _++_; _∷_; here; there)
6+open import Data.Vec using ([]; _++_)
7 open import Data.Product using (_,_; _×_)
8 open import Function
9 open import Expr
10@@ -22,143 +22,132 @@ data _⊢_↦_⊢_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Behaviour
11 -- Identity
12 idn : ∀ {n} {Γ : Ctx n} {b : Behaviour} → Γ ⊢ b ↦ Γ ⊢ b
13
14-data _⊢ₑ_∶_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where
15+data _⊢ₑ_∶_ (Γ : Context) : Expr → Type → Set where
16 expr-t : {s : Expr} {b : Type}
17 → Γ ⊢ₑ s ∶ b
18
19-data Context : Set where
20- ◆ : ∀ {n} → Ctx n → Context
21- ■ : ∀ {n m} → Ctx n → Ctx m → Context
22-
23 data _⊢B_▹_ : Context → Behaviour → Context → Set where
24- t-nil : ∀ {n} {Γ : Ctx n}
25+ t-nil : {Γ : Context}
26 ------------------
27- → ◆ Γ ⊢B nil ▹ ◆ Γ
28+ → Γ ⊢B nil ▹ Γ
29
30- t-if : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b₁ b₂ : Behaviour} {e : Expr}
31+ t-if : {Γ Γ₁ : Context} {b₁ b₂ : Behaviour} {e : Expr}
32 → Γ ⊢ₑ e ∶ bool -- Γ ⊢ e : bool
33- → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁
34- → ◆ Γ ⊢B b₂ ▹ ◆ Γ₁
35+ → Γ ⊢B b₁ ▹ Γ₁
36+ → Γ ⊢B b₂ ▹ Γ₁
37 --------------------------
38- → ◆ Γ ⊢B if e then b₁ else b₂ ▹ ◆ Γ₁
39+ → Γ ⊢B if e then b₁ else b₂ ▹ Γ₁
40
41- t-while : ∀ {n} {Γ : Ctx n} {b : Behaviour} {e : Expr}
42+ t-while : {Γ : Context} {b : Behaviour} {e : Expr}
43 → Γ ⊢ₑ e ∶ bool
44- → ◆ Γ ⊢B b ▹ ◆ Γ
45+ → Γ ⊢B b ▹ Γ
46 ------------------------
47- → ◆ Γ ⊢B while[ e ] b ▹ ◆ Γ
48+ → Γ ⊢B while[ e ] b ▹ Γ
49
50- t-choice : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {choices : List (η × Behaviour)}
51- → All (λ { (η , b) → ◆ Γ ⊢B (input η) ∶ b ▹ ◆ Γ₁ }) choices
52+ t-choice : {Γ Γ₁ : Context} {choices : List (η × Behaviour)}
53+ → All (λ { (η , b) → Γ ⊢B (input η) ∶ b ▹ Γ₁ }) choices
54 -----------------------------------
55- → ◆ Γ ⊢B inputchoice choices ▹ ◆ Γ₁
56+ → Γ ⊢B inputchoice choices ▹ Γ₁
57
58 t-par : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b1 b2 : Behaviour}
59 → ◆ Γ₁ ⊢B b1 ▹ ◆ Γ₁'
60 → ◆ Γ₂ ⊢B b2 ▹ ◆ Γ₂'
61- --------------------------------------
62+ ------------------------------------
63 → (■ Γ₁ Γ₂) ⊢B b1 ∥ b2 ▹ (■ Γ₁' Γ₂')
64
65- t-seq : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b₁ b₂ : Behaviour}
66- → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁
67- → ◆ Γ₁ ⊢B b₂ ▹ ◆ Γ₂
68- -------------------------
69- → ◆ Γ ⊢B b₁ ∶ b₂ ▹ ◆ Γ₂
70+ t-seq : {Γ Γ₁ Γ₂ : Context} {b₁ b₂ : Behaviour}
71+ → Γ ⊢B b₁ ▹ Γ₁
72+ → Γ₁ ⊢B b₂ ▹ Γ₂
73+ -----------------------
74+ → Γ ⊢B b₁ ∶ b₂ ▹ Γ₂
75
76- t-notification : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
77+ t-notification : {Γ : Context} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
78 → (outNotify o l T₀) ∈ Γ
79 → var e Tₑ ∈ Γ
80 → Tₑ ⊆ T₀
81 ------------------------------------------------
82- → ◆ Γ ⊢B output (o at l [ var e ]) ▹ ◆ Γ
83+ → Γ ⊢B output (o at l [ var e ]) ▹ Γ
84
85- t-assign-new : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
86+ t-assign-new : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
87 → Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
88 → ¬ (var x Tₓ ∈ Γ) -- x ∉ Γ
89 --------------------------------------
90- → ◆ Γ ⊢B x ≃ e ▹ ◆ (var x Tₑ ∷ Γ)
91+ → Γ ⊢B x ≃ e ▹ (var x Tₑ ∷ Γ)
92
93- t-assign-exists : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
94+ t-assign-exists : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
95 → Γ ⊢ₑ e ∶ Tₑ
96 → var x Tₓ ∈ Γ
97 → Tₑ ≡ Tₓ
98 -------------------------
99- → ◆ Γ ⊢B x ≃ e ▹ ◆ Γ
100+ → Γ ⊢B x ≃ e ▹ Γ
101
102- t-oneway-new : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
103+ t-oneway-new : {Γ : Context} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
104 → inOneWay o Tᵢ ∈ Γ
105 → ¬ (var x Tₓ ∈ Γ)
106- ----------------------------------------------
107- → ◆ Γ ⊢B input (o [ x ]) ▹ ◆ (var x Tᵢ ∷ Γ)
108+ ---------------------------------------
109+ → Γ ⊢B input (o [ x ]) ▹ (var x Tᵢ ∷ Γ)
110
111- t-oneway-exists : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
112+ t-oneway-exists : {Γ : Context} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
113 → inOneWay o Tᵢ ∈ Γ
114 → var x Tₓ ∈ Γ
115 → Tᵢ ⊆ Tₓ
116- ---------------------------------
117- → ◆ Γ ⊢B input (o [ x ]) ▹ ◆ Γ
118+ --------------------------
119+ → Γ ⊢B input (o [ x ]) ▹ Γ
120
121- t-solresp-new : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
122+ t-solresp-new : {Γ : Context} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
123 → outSolRes o l Tₒ Tᵢ ∈ Γ
124 → Tₑ ⊆ Tₒ
125 → ¬ (var x Tₓ ∈ Γ)
126- -------------------------------------------------------
127- → ◆ Γ ⊢B output (o at l [ e ][ x ]) ▹ ◆ (var x Tᵢ ∷ Γ)
128+ --------------------------------------------------
129+ → Γ ⊢B output (o at l [ e ][ x ]) ▹ (var x Tᵢ ∷ Γ)
130
131- t-solresp-exists : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
132+ t-solresp-exists : {Γ : Context} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
133 → outSolRes o l Tₒ Tᵢ ∈ Γ
134 → Tₑ ⊆ Tₒ
135 → var x Tₓ ∈ Γ
136 → Tᵢ ⊆ Tₓ
137- ------------------------------------------
138- → ◆ Γ ⊢B output (o at l [ e ][ x ]) ▹ ◆ Γ
139+ -------------------------------------
140+ → Γ ⊢B output (o at l [ e ][ x ]) ▹ Γ
141
142- t-reqresp-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
143+ t-reqresp-new : {Γ Γ₁ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
144 → inReqRes o Tᵢ Tₒ ∈ Γ
145 → ¬ (var x Tₓ ∈ Γ)
146- → ◆ (var x Tₓ ∷ Γ) ⊢B b ▹ ◆ Γ₁
147+ → (var x Tₓ ∷ Γ) ⊢B b ▹ Γ₁
148 → var a Tₐ ∈ Γ₁
149 → Tₐ ⊆ Tₒ
150- --------------------------------------
151- → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ ◆ Γ₁
152+ ----------------------------------
153+ → Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₁
154
155- t-reqresp-exists : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable}
156+ t-reqresp-exists : {Γ Γ₁ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable}
157 → (inReqRes o Tᵢ Tₒ) ∈ Γ
158 → var x Tₓ ∈ Γ
159 → Tᵢ ⊆ Tₓ
160- → ◆ Γ ⊢B b ▹ ◆ Γ₁
161+ → Γ ⊢B b ▹ Γ₁
162 → var a Tₐ ∈ Γ₁
163 → Tₐ ⊆ Tₒ
164- --------------------------------------
165- → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ ◆ Γ₁
166+ ----------------------------------
167+ → Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₁
168
169- t-wait-new : ∀ {n} {Γ : Ctx n} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
170+ t-wait-new : {Γ : Context} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
171 → outSolRes o l Tₒ Tᵢ ∈ Γ
172 → ¬ (var x Tₓ ∈ Γ)
173- ----------------------------------------
174- → ◆ Γ ⊢B wait r o l x ▹ ◆ (var x Tᵢ ∷ Γ)
175+ ------------------------------------
176+ → Γ ⊢B wait r o l x ▹ (var x Tᵢ ∷ Γ)
177
178- t-wait-exists : ∀ {n} {Γ : Ctx n} {Tₒ Tᵢ Tₓ : Type} {o : Operation} {l : Location} {r : Channel} {x : Variable}
179+ t-wait-exists : {Γ : Context} {Tₒ Tᵢ Tₓ : Type} {o : Operation} {l : Location} {r : Channel} {x : Variable}
180 → outSolRes o l Tₒ Tᵢ ∈ Γ
181 → var x Tₓ ∈ Γ
182 → Tᵢ ⊆ Tₓ
183- ---------------------------
184- → ◆ Γ ⊢B wait r o l x ▹ ◆ Γ
185+ -----------------------
186+ → Γ ⊢B wait r o l x ▹ Γ
187
188- t-exec : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₒ Tᵢ Tₓ : Type} {b : Behaviour} {r : Channel} {o : Operation} {x : Variable}
189+ t-exec : {Γ Γ₁ : Context} {Tₒ Tᵢ Tₓ : Type} {b : Behaviour} {r : Channel} {o : Operation} {x : Variable}
190 → inReqRes o Tᵢ Tₒ ∈ Γ
191- → ◆ Γ ⊢B b ▹ ◆ Γ₁
192+ → Γ ⊢B b ▹ Γ₁
193 → var x Tₓ ∈ Γ
194 → Tₓ ⊆ Tₒ
195- ----------------------------
196- → ◆ Γ ⊢B exec r o x b ▹ ◆ Γ₁
197-
198- t-mutate : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx m} {Γₐ : Ctx k} {b₁ b₂ : Behaviour}
199- → Γ ⊢ b₁ ↦ Γₐ ⊢ b₂
200- → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁
201- ------------------
202- → ◆ Γₐ ⊢B b₂ ▹ ◆ Γ₁
203-
204+ ------------------------
205+ → Γ ⊢B exec r o x b ▹ Γ₁
206
207 struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b₁ b₂ : Behaviour}
208 → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁
209@@ -171,18 +160,7 @@ struct-cong-par-nil : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁
210 → ◆ Γ₁ ⊢B b ▹ ◆ Γ₁'
211 struct-cong-par-nil (t-par x _) = x
212
213-struct-cong-par-sym : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b₁ b₂ : Behaviour}
214- → ■ Γ₁ Γ₂ ⊢B (b₁ ∥ b₂) ▹ ■ Γ₁' Γ₂'
215- → ■ Γ₂ Γ₁ ⊢B (b₂ ∥ b₁) ▹ ■ Γ₂' Γ₁'
216-struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁
217-
218-struct-cong-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour}
219- → ◆ Γ ⊢B (nil ∶ b) ▹ ◆ Γ₁
220- → ◆ Γ ⊢B b ▹ ◆ Γ₁
221-struct-cong-nil = t-mutate upd
222-
223-preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b₁ b₂ : Behaviour}
224- → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁
225- → Γ ⊢ b₁ ↦ Γₐ ⊢ b₂
226- → ◆ Γₐ ⊢B b₂ ▹ ◆ Γ₁
227-preservation x s = t-mutate s x
228+--struct-cong-par-sym : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b₁ b₂ : Behaviour}
229+-- → Γ₁ ++ Γ₂ ⊢B (b₁ ∥ b₂) ▹ Γ₁' ++ Γ₂'
230+-- → Γ₂ ++ Γ₁ ⊢B (b₂ ∥ b₁) ▹ Γ₂' ++ Γ₁'
231+--struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁
+26,
-7
1@@ -1,16 +1,35 @@
2 module TypingNetwork where
3
4+open import Relation.Nullary using (¬_)
5+open import Data.Vec using (_∈_; fromList)
6+open import Data.Product using (_,_)
7+open import TypingService
8+open import Service
9 open import Network
10 open import Type
11+open import Behaviour
12
13-data _⊢N_ : ∀ {n} → Ctx n → Network → Set where
14+
15+data _⊢N_ : Context → Network → Set where
16 t-network-nil : ∀ {n} {Γ : Ctx n}
17- ----------
18- → Γ ⊢N nil
19+ ------------
20+ → ◆ Γ ⊢N nil
21+
22+ t-deployment : ∀ {n m} {Γ : Ctx n} {b : Behaviour} {l : Location} {o : Operation} {p : Process} {d : Deployment m} {Tₒ : Type}
23+ → Γ ⊢S (b ▹ d - p)
24+ → ¬ (outNotify o l Tₒ ∈ Γ)
25+ --------------------------
26+ → ◆ Γ ⊢N ([ b ▹ d - p ] l)
27
28- -- TODO: implement t-network and t-deployment
29+ t-network : ∀ {n} {m} {Γ₁ : Ctx n} {Γ₂ : Ctx m} {N₁ N₂ : Network} {l : Location}
30+ → ◆ Γ₁ ⊢N N₁
31+ → ◆ Γ₂ ⊢N N₂
32+-- → , ¬ (l ∈ fromList (locs N₁))
33+ → ¬ (l ∈ fromList (locs N₂))
34+ ----------------------
35+ → ■ Γ₁ Γ₂ ⊢N (N₁ ∥ N₂)
36
37 t-restriction : ∀ {n} {Γ : Ctx n} {n : Network}
38- → Γ ⊢N n
39- -----------
40- → Γ ⊢N νr n
41+ → ◆ Γ ⊢N n
42+ -------------
43+ → ◆ Γ ⊢N νr n
+4,
-2
1@@ -6,7 +6,7 @@ open import Data.List.All using (All)
2 open import Data.Vec using (Vec; toList; concat; _∈_)
3 open import Data.List using (List; zip)
4 open import Data.Product using (_×_; _,_)
5-open import TypingBehaviour using (_⊢B_▹_; ◆)
6+open import TypingBehaviour using (_⊢B_▹_)
7 open import Type
8 open import Service
9 open import Behaviour
10@@ -41,6 +41,8 @@ data _⊢P_ : ∀ {n} → Ctx n → Process → Set where
11
12
13 data _⊢S_ : ∀ {n} → Ctx n → Service → Set where
14- t-service : ∀ {n m} {Γ : Ctx n} {b : Behaviour} {d : Deployment m} {p : Process}
15+ t-service : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx k} {b : Behaviour} {d : Deployment m} {p : Process}
16+ → Γ ⊢BSL b ▹ Γ₁
17+ → Γ ⊢P p
18 ------------------
19 → Γ ⊢S (b ▹ d - p)