Eugene Akentyev
·
2017-02-22
TypingBehaviour.agda
1module TypingBehaviour where
2
3open import Data.List.All using (All)
4open import Relation.Nullary using (¬_)
5open import Relation.Binary.PropositionalEquality using (_≡_; refl)
6open import Data.Nat using (ℕ)
7open import Data.List using (List)
8open import Data.Vec using ([]; _++_; _∷_)
9open import Data.Product using (_,_; _×_)
10open import BehaviouralSemantics
11open import Function
12open import Expr
13open import Type
14open import Behaviour
15open import Variable
16
17
18data _⊢ₑ_∶_ (Γ : Context) : Expr → Type → Set where
19 expr-t : {s : Expr} {b : Type}
20 → Γ ⊢ₑ s ∶ b
21
22-- Side effect
23data _↦⟨_⟩_ : Context → Label → Context → Set where
24 s-assign : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
25 → Γ ⊢ₑ e ∶ Tₑ
26 → var x Tₓ ∈ Γ
27 → Tₓ ≡ Tₑ
28 ---------------------------------
29 → Γ ↦⟨ lb-assign x e ⟩ Γ
30
31 s-assign-upd : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
32 → Γ ⊢ₑ e ∶ Tₑ
33 → ¬ (var x Tₓ ∈ Γ)
34 → Γ ↦⟨ lb-assign x e ⟩ (appendContext (var x Tₓ) Γ)
35
36data _⊢B_▹_ : Context → Behaviour → Context → Set where
37 t-nil : {Γ : Context}
38 --------------
39 → Γ ⊢B nil ▹ Γ
40
41 t-if : {Γ Γ₁ : Context} {b₁ b₂ : Behaviour} {e : Expr}
42 → Γ ⊢ₑ e ∶ bool -- Γ ⊢ e : bool
43 → Γ ⊢B b₁ ▹ Γ₁
44 → Γ ⊢B b₂ ▹ Γ₁
45 --------------------------------
46 → Γ ⊢B if e then b₁ else b₂ ▹ Γ₁
47
48 t-while : {Γ : Context} {b : Behaviour} {e : Expr}
49 → Γ ⊢ₑ e ∶ bool
50 → Γ ⊢B b ▹ Γ
51 -----------------------
52 → Γ ⊢B while[ e ] b ▹ Γ
53
54 t-choice : {Γ Γ₁ : Context} {choices : List (η × Behaviour)}
55 → All (λ { (η , b) → Γ ⊢B (input η) ∶ b ▹ Γ₁ }) choices
56 -------------------------------
57 → Γ ⊢B inputchoice choices ▹ Γ₁
58
59 t-par : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b1 b2 : Behaviour}
60 → Γ₁ ⊢B b1 ▹ Γ₁'
61 → Γ₂ ⊢B b2 ▹ Γ₂'
62 ------------------------------------
63 → (& Γ₁ Γ₂) ⊢B b1 ∥ b2 ▹ (& Γ₁' Γ₂')
64
65 t-seq : {Γ Γ₁ Γ₂ : Context} {b₁ b₂ : Behaviour}
66 → Γ ⊢B b₁ ▹ Γ₁
67 → Γ₁ ⊢B b₂ ▹ Γ₂
68 -------------------
69 → Γ ⊢B b₁ ∶ b₂ ▹ Γ₂
70
71 t-notification : {Γ : Context} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
72 → (outNotify o l T₀) ∈ Γ
73 → var e Tₑ ∈ Γ
74 → Tₑ ⊆ T₀
75 ------------------------------------
76 → Γ ⊢B output (o at l [ var e ]) ▹ Γ
77
78 t-assign-new : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
79 → ⋆ Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
80 → ¬ (var x Tₓ ∈ ⋆ Γ) -- x ∉ Γ
81 ---------------------------------
82 → ⋆ Γ ⊢B x ≃ e ▹ ⋆ (var x Tₑ ∷ Γ)
83
84 t-assign-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
85 → & (⋆ Γ) (⋆ Γ₁) ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
86 → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁)) -- x ∉ Γ
87 -------------------------------------------------------
88 → & (⋆ Γ) (⋆ Γ₁) ⊢B x ≃ e ▹ & (⋆ (var x Tₑ ∷ Γ)) (⋆ Γ₁)
89
90 t-assign-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
91 → & (⋆ Γ) (⋆ Γ₁) ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
92 → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁)) -- x ∉ Γ
93 ------------------------------------------------------
94 → & (⋆ Γ) (⋆ Γ₁) ⊢B x ≃ e ▹ & (⋆ Γ) (⋆ (var x Tₑ ∷ Γ₁))
95
96 t-assign-exists : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
97 → Γ ⊢ₑ e ∶ Tₑ
98 → var x Tₓ ∈ Γ
99 → Tₑ ≡ Tₓ
100 ----------------
101 → Γ ⊢B x ≃ e ▹ Γ
102
103 t-oneway-new : ∀ {n} {Γ : Ctx n} {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 t-oneway-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
110 → inOneWay o Tᵢ ∈ & (⋆ Γ) (⋆ Γ₁)
111 → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
112 -----------------------------------------------------------------
113 → & (⋆ Γ) (⋆ Γ₁) ⊢B input (o [ x ]) ▹ & (⋆ (var x Tᵢ ∷ Γ)) (⋆ Γ₁)
114
115 t-oneway-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
116 → inOneWay o Tᵢ ∈ & (⋆ Γ) (⋆ Γ₁)
117 → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
118 -----------------------------------------------------------------
119 → & (⋆ Γ) (⋆ Γ₁) ⊢B input (o [ x ]) ▹ & (⋆ Γ) (⋆ (var x Tᵢ ∷ Γ₁))
120
121 t-oneway-exists : {Γ : Context} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
122 → inOneWay o Tᵢ ∈ Γ
123 → var x Tₓ ∈ Γ
124 → Tᵢ ⊆ Tₓ
125 --------------------------
126 → Γ ⊢B input (o [ x ]) ▹ Γ
127
128 t-solresp-new : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
129 → outSolRes o l Tₒ Tᵢ ∈ ⋆ Γ
130 → Tₑ ⊆ Tₒ
131 → ¬ (var x Tₓ ∈ ⋆ Γ)
132 ------------------------------------------------------
133 → ⋆ Γ ⊢B output (o at l [ e ][ x ]) ▹ ⋆ (var x Tᵢ ∷ Γ)
134
135 t-solresp-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
136 → outSolRes o l Tₒ Tᵢ ∈ & (⋆ Γ) (⋆ Γ₁)
137 → Tₑ ⊆ Tₒ
138 → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
139 ----------------------------------------------------------------------------
140 → & (⋆ Γ) (⋆ Γ₁) ⊢B output (o at l [ e ][ x ]) ▹ & (⋆ (var x Tᵢ ∷ Γ)) (⋆ Γ₁)
141
142 t-solresp-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
143 → outSolRes o l Tₒ Tᵢ ∈ & (⋆ Γ) (⋆ Γ₁)
144 → Tₑ ⊆ Tₒ
145 → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
146 ----------------------------------------------------------------------------
147 → & (⋆ Γ) (⋆ Γ₁) ⊢B output (o at l [ e ][ x ]) ▹ & (⋆ Γ) (⋆ (var x Tᵢ ∷ Γ₁))
148
149 t-solresp-exists : {Γ : Context} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
150 → outSolRes o l Tₒ Tᵢ ∈ Γ
151 → Tₑ ⊆ Tₒ
152 → var x Tₓ ∈ Γ
153 → Tᵢ ⊆ Tₓ
154 -------------------------------------
155 → Γ ⊢B output (o at l [ e ][ x ]) ▹ Γ
156
157 t-reqresp-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
158 → inReqRes o Tᵢ Tₒ ∈ ⋆ Γ
159 → ¬ (var x Tₓ ∈ ⋆ Γ)
160 → ⋆ (var x Tₓ ∷ Γ) ⊢B b ▹ ⋆ Γ₁
161 → var a Tₐ ∈ ⋆ Γ₁
162 → Tₐ ⊆ Tₒ
163 --------------------------------------
164 → ⋆ Γ ⊢B input (o [ x ][ a ] b) ▹ ⋆ Γ₁
165
166 t-reqresp-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Γ₂ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
167 → inReqRes o Tᵢ Tₒ ∈ & (⋆ Γ) (⋆ Γ₁)
168 → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
169 → & (⋆ (var x Tₓ ∷ Γ)) (⋆ Γ₁) ⊢B b ▹ Γ₂
170 → var a Tₐ ∈ Γ₂
171 → Tₐ ⊆ Tₒ
172 ------------------------------------
173 → ⋆ Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₂
174
175 t-reqresp-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Γ₂ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
176 → inReqRes o Tᵢ Tₒ ∈ & (⋆ Γ) (⋆ Γ₁)
177 → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
178 → & (⋆ Γ) (⋆ (var x Tₓ ∷ Γ₁)) ⊢B b ▹ Γ₂
179 → var a Tₐ ∈ Γ₂
180 → Tₐ ⊆ Tₒ
181 ------------------------------------
182 → ⋆ Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₂
183
184 t-reqresp-exists : {Γ Γ₁ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable}
185 → (inReqRes o Tᵢ Tₒ) ∈ Γ
186 → var x Tₓ ∈ Γ
187 → Tᵢ ⊆ Tₓ
188 → Γ ⊢B b ▹ Γ₁
189 → var a Tₐ ∈ Γ₁
190 → Tₐ ⊆ Tₒ
191 ----------------------------------
192 → Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₁
193
194 t-wait-new : ∀ {n} {Γ : Ctx n} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
195 → outSolRes o l Tₒ Tᵢ ∈ ⋆ Γ
196 → ¬ (var x Tₓ ∈ ⋆ Γ)
197 ----------------------------------------
198 → ⋆ Γ ⊢B wait r o l x ▹ ⋆ (var x Tᵢ ∷ Γ)
199
200 t-wait-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
201 → outSolRes o l Tₒ Tᵢ ∈ & (⋆ Γ) (⋆ Γ₁)
202 → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
203 --------------------------------------------------------------
204 → & (⋆ Γ) (⋆ Γ₁) ⊢B wait r o l x ▹ & (⋆ (var x Tᵢ ∷ Γ)) (⋆ Γ₁)
205
206 t-wait-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
207 → outSolRes o l Tₒ Tᵢ ∈ & (⋆ Γ) (⋆ Γ₁)
208 → ¬ (var x Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
209 --------------------------------------------------------------
210 → & (⋆ Γ) (⋆ Γ₁) ⊢B wait r o l x ▹ & (⋆ Γ) (⋆ (var x Tᵢ ∷ Γ₁))
211
212 t-wait-exists : {Γ : Context} {Tₒ Tᵢ Tₓ : Type} {o : Operation} {l : Location} {r : Channel} {x : Variable}
213 → outSolRes o l Tₒ Tᵢ ∈ Γ
214 → var x Tₓ ∈ Γ
215 → Tᵢ ⊆ Tₓ
216 -----------------------
217 → Γ ⊢B wait r o l x ▹ Γ
218
219 t-exec : {Γ Γ₁ : Context} {Tₒ Tᵢ Tₓ : Type} {b : Behaviour} {r : Channel} {o : Operation} {x : Variable}
220 → inReqRes o Tᵢ Tₒ ∈ Γ
221 → Γ ⊢B b ▹ Γ₁
222 → var x Tₓ ∈ Γ
223 → Tₓ ⊆ Tₒ
224 ------------------------
225 → Γ ⊢B exec r o x b ▹ Γ₁
226
227struct-congruence : {Γ Γ₁ : Context} {b₁ b₂ : Behaviour}
228 → Γ ⊢B b₁ ▹ Γ₁
229 → b₁ ≡ b₂
230 → Γ ⊢B b₂ ▹ Γ₁
231struct-congruence t refl = t
232
233struct-cong-seq-nil : {Γ Γ₁ : Context} {b : Behaviour}
234 → Γ ⊢B nil ∶ b ▹ Γ₁
235 → Γ ⊢B b ▹ Γ₁
236struct-cong-seq-nil (t-seq t-nil x) = x
237
238struct-cong-par-nil : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b : Behaviour}
239 → & Γ₁ Γ₂ ⊢B (b ∥ nil) ▹ & Γ₁' Γ₂'
240 → Γ₁ ⊢B b ▹ Γ₁'
241struct-cong-par-nil (t-par x _) = x
242
243struct-cong-par-sym : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b₁ b₂ : Behaviour}
244 → & Γ₁ Γ₂ ⊢B (b₁ ∥ b₂) ▹ & Γ₁' Γ₂'
245 → & Γ₂ Γ₁ ⊢B (b₂ ∥ b₁) ▹ & Γ₂' Γ₁'
246struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁
247
248struct-cong-par-assoc : {Γ₁ Γ₂ Γ₃ Γ₁' Γ₂' Γ₃' : Context} {b₁ b₂ b₃ : Behaviour}
249 → & (& Γ₁ Γ₂) Γ₃ ⊢B (b₁ ∥ b₂) ∥ b₃ ▹ & (& Γ₁' Γ₂') Γ₃'
250 → & Γ₁ (& Γ₂ Γ₃) ⊢B b₁ ∥ (b₂ ∥ b₃) ▹ & Γ₁' (& Γ₂' Γ₃')
251struct-cong-par-assoc (t-par (t-par t1 t2) t3) = t-par t1 (t-par t2 t3)
252
253--type-preservation : {Γ Γ′ Γ′′ : Context} {b b′ : Behaviour} {η : Label}
254-- → Γ ⊢B b ▹ Γ′
255-- → b ↝ b′ ∶ η
256-- → Γ ↦⟨ η ⟩ Γ′′
257-- → Γ′′ ⊢B b′ ▹ Γ′
258--type-preservation _ = {!-c -t 30!}
259
260type-preservation-if-then : {Γ Γ′ : Context} {b₁ b₂ : Behaviour} {t : State} {e : Expr}
261 → Γ ⊢B if e then b₁ else b₂ ▹ Γ′
262 → (if e then b₁ else b₂) ↝ b₁ ∶ (lb-read t)
263 → Γ ↦⟨ lb-read t ⟩ Γ
264 → Γ ⊢B b₁ ▹ Γ′
265type-preservation-if-then (t-if et t1 t2) _ _ = t1
266
267type-preservation-if-else : {Γ Γ′ : Context} {b₁ b₂ : Behaviour} {t : State} {e : Expr}
268 → Γ ⊢B if e then b₁ else b₂ ▹ Γ′
269 → (if e then b₁ else b₂) ↝ b₂ ∶ (lb-read t)
270 → Γ ↦⟨ lb-read t ⟩ Γ
271 → Γ ⊢B b₂ ▹ Γ′
272type-preservation-if-else (t-if et t1 t2) _ _ = t2
273
274type-preservation-iter : {Γ Γ′ : Context} {b : Behaviour} {t : State} {e : Expr}
275 → Γ ⊢B while[ e ] b ▹ Γ′
276 → (while[ e ] b) ↝ (b ∶ (while[ e ] b)) ∶ (lb-read t)
277 → Γ ↦⟨ lb-read t ⟩ Γ
278 → Γ ⊢B (b ∶ (while[ e ] b)) ▹ Γ′
279type-preservation-iter (t-while te t) _ _ = t-seq t (t-while te t)
280
281type-preservation-no-iter : {Γ Γ′ : Context} {b : Behaviour} {t : State} {e : Expr}
282 → Γ ⊢B while[ e ] b ▹ Γ′
283 → (while[ e ] b) ↝ nil ∶ (lb-read t)
284 → Γ ↦⟨ lb-read t ⟩ Γ
285 → Γ ⊢B (nil ∶ (while[ e ] b)) ▹ Γ
286type-preservation-no-iter (t-while te t) _ _ = t-seq t-nil (t-while te t)
287
288type-preservation-assign : {Γ Γ′ Γ′′ : Context} {x : Variable} {t : State} {e : Expr} {Tₑ : Type}
289 → Γ ⊢B x ≃ e ▹ Γ′
290 → (x ≃ e) ↝ nil ∶ (lb-assign x e)
291 → Γ ↦⟨ lb-assign x e ⟩ Γ′′
292 → Γ′′ ⊢B x ≃ e ▹ Γ′
293type-preservation-assign (t-assign-new x₁ x₂) _ _ = {!!}
294type-preservation-assign (t-assign-new-left x₁ x₂) _ _ = {!!}
295type-preservation-assign (t-assign-new-right x₁ x₂) _ _ = {!!}
296type-preservation-assign (t-assign-exists x₁ x₂ x₃) _ _ = {!!}