- commit
- 6abff2b
- parent
- d75b931
- author
- Eugene Akentyev
- date
- 2016-12-27 05:19:31 +0400 +04
Update type rules of behaviour layer.
1 files changed,
+77,
-69
+77,
-69
1@@ -5,7 +5,7 @@ open import Relation.Nullary using (¬_)
2 open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; subst; refl)
3 open import Data.Nat using (ℕ; _+_; suc; _≟_)
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@@ -25,26 +25,26 @@ data _⊢ₑ_∶_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where
11 → Γ ⊢ₑ s ∶ b
12
13 data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
14- t-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Γ≡Γ₁ : Γ CtxPropEq.≈ Γ₁}
15- ---------------------------
16- → Γ ⊢B nil ▹ Γ₁
17+ t-nil : ∀ {n} {Γ : Ctx n}
18+ --------------
19+ → Γ ⊢B nil ▹ Γ
20
21 t-if : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Expr}
22 → Γ ⊢ₑ e ∶ bool -- Γ ⊢ e : bool
23 → Γ ⊢B b1 ▹ Γ₁
24 → Γ ⊢B b2 ▹ Γ₁
25- ---------------------------
26+ ----------------------
27 → Γ ⊢B if e b1 b2 ▹ Γ₁
28
29- t-while : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Γ≡Γ₁ : Γ CtxPropEq.≈ Γ₁} {b : Behaviour} {e : Expr}
30+ t-while : ∀ {n} {Γ : Ctx n} {b : Behaviour} {e : Expr}
31 → Γ ⊢ₑ e ∶ bool
32- → Γ ⊢B b ▹ Γ₁
33- --------------------------
34- → Γ ⊢B while e b ▹ Γ₁
35+ → Γ ⊢B b ▹ Γ
36+ ---------------------
37+ → Γ ⊢B while e b ▹ Γ
38
39 t-choice : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {choices : List (Input_ex × Behaviour)}
40 → All (λ { (η , b) → Γ ⊢B seq (input η) b ▹ Γ₁ }) choices
41- -----------------------------------------------
42+ -------------------------------
43 → Γ ⊢B inputchoice choices ▹ Γ₁
44
45 t-par : ∀ {n m} {Γ : Ctx n} {k k₁ p p₁ : ℕ} {b1 b2 : Behaviour}
46@@ -52,104 +52,112 @@ data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
47 → Γ₁ ⊢B b1 ▹ Γ₁'
48 → Γ₂ ⊢B b2 ▹ Γ₂'
49 -- TODO: maybe it's not enough to express that Γ = Γ₁, Γ₂ and Γ' = Γ₁', Γ₂' - disjoint unions
50- --------------------
51- → Γ ⊢B par b1 b2 ▹ Γ'
52+ ----------------------------------------
53+ → (Γ₁ ++ Γ₂) ⊢B par b1 b2 ▹ (Γ₁' ++ Γ₂')
54
55- t-seq : ∀ {n m} {Γ : Ctx n} {k : ℕ} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour}
56+ t-seq : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour}
57 → Γ ⊢B b1 ▹ Γ₁
58 → Γ₁ ⊢B b2 ▹ Γ₂
59- --------------------
60+ ---------------------
61 → Γ ⊢B seq b1 b2 ▹ Γ₂
62
63- t-notification : ∀ {n m} {Γ : Ctx n} {n≡m : n ≡ m} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
64+ t-notification : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
65 → (outNotify o l T₀) ∈ Γ
66 → Γ ⊢ e ∶ Tₑ
67 → Tₑ ⊆ T₀
68- -------------------------------------------
69- → Γ ⊢B output (notification o l (var e)) ▹ subst Ctx n≡m Γ
70+ ---------------------------------------------
71+ → Γ ⊢B output (notification o l (var e)) ▹ Γ
72
73- t-assign-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
74+ t-assign-new : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
75 → Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
76 → ¬ (var x Tₓ ∈ Γ) -- x ∉ Γ
77- → (var x Tₑ) ∈ Γ₁
78- ---------------------
79- → Γ ⊢B assign x e ▹ Γ₁
80+ -----------------------------------
81+ → Γ ⊢B assign x e ▹ (var x Tₑ ∷ Γ)
82
83- t-assign-exists : ∀ {n m} {Γ : Ctx n} {n≡m : n ≡ m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
84+ t-assign-exists : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
85 → Γ ⊢ₑ e ∶ Tₑ
86- → (var x Tₓ) ∈ Γ
87+ → var x Tₓ ∈ Γ
88 → Tₑ ≡ Tₓ
89- ---------------------
90- → Γ ⊢B assign x e ▹ subst Ctx n≡m Γ
91-
92- t-oneway-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
93- → (inOneWay o Tᵢ) ∈ Γ
94- → ¬ ((var x Tₓ) ∈ Γ)
95- → (var x Tᵢ) ∈ Γ₁
96- -------------------------------
97- → Γ ⊢B input (oneway o x) ▹ Γ₁
98-
99- t-oneway-exists : ∀ {n m} {Γ : Ctx n} {n≡m : n ≡ m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
100- → (inOneWay o Tᵢ) ∈ Γ
101- → ((var x Tₓ) ∈ Γ)
102+ ----------------------
103+ → Γ ⊢B assign x e ▹ Γ
104+
105+ t-oneway-new : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
106+ → inOneWay o Tᵢ ∈ Γ
107+ → ¬ (var x Tₓ ∈ Γ)
108+ ------------------------------------------
109+ → Γ ⊢B input (oneway o x) ▹ (var x Tᵢ ∷ Γ)
110+
111+ t-oneway-exists : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
112+ → inOneWay o Tᵢ ∈ Γ
113+ → var x Tₓ ∈ Γ
114 → Tᵢ ⊆ Tₓ
115- --------------------------------
116- → Γ ⊢B input (oneway o x) ▹ subst Ctx n≡m Γ
117+ ------------------------------
118+ → Γ ⊢B input (oneway o x) ▹ Γ
119
120- t-solresp-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
121- → (outSolRes o l Tₒ Tᵢ) ∈ Γ
122+ t-solresp-new : ∀ {n} {Γ : Ctx n} {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- → (var x Tᵢ) ∈ Γ₁
127- -----------------------------------------
128- → Γ ⊢B output (solicitres o l e x) ▹ Γ₁
129+ --------------------------------------------------
130+ → Γ ⊢B output (solicitres o l e x) ▹ (var x Tᵢ ∷ Γ)
131
132- t-solresp-exists : ∀ {n m} {Γ : Ctx n} {n≡m : n ≡ m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
133- → (outSolRes o l Tₒ Tᵢ) ∈ Γ
134+ t-solresp-exists : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
135+ → outSolRes o l Tₒ Tᵢ ∈ Γ
136 → Tₑ ⊆ Tₒ
137- → (var x Tₓ) ∈ Γ
138+ → var x Tₓ ∈ Γ
139 → Tᵢ ⊆ Tₓ
140- -----------------------------------------
141- → Γ ⊢B output (solicitres o l e x) ▹ subst Ctx n≡m Γ
142+ ---------------------------------------
143+ → Γ ⊢B output (solicitres o l e x) ▹ Γ
144
145- t-reqresp-new : ∀ {n m} {Γ : Ctx n} {p : ℕ} {Γₓ : Ctx p} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
146- → (inReqRes o Tᵢ Tₒ) ∈ Γ
147+ t-reqresp-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
148+ → inReqRes o Tᵢ Tₒ ∈ Γ
149 → ¬ (var x Tₓ ∈ Γ)
150- → (var x Tₓ) ∈ Γₓ
151- → Γₓ ⊢B b ▹ Γ₁
152- → (var a Tₐ) ∈ Γ₁
153+ → (var x Tₓ ∷ Γ) ⊢B b ▹ Γ₁
154+ → var a Tₐ ∈ Γ₁
155 → Tₐ ⊆ Tₒ
156- -----------------------------------
157+ ----------------------------------
158 → Γ ⊢B input (reqres o x a b) ▹ Γ₁
159
160 t-reqresp-exists : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable}
161 → (inReqRes o Tᵢ Tₒ) ∈ Γ
162- → (var x Tₓ) ∈ Γ
163+ → var x Tₓ ∈ Γ
164 → Tᵢ ⊆ Tₓ
165 → Γ ⊢B b ▹ Γ₁
166- → (var a Tₐ) ∈ Γ₁
167+ → var a Tₐ ∈ Γ₁
168 → Tₐ ⊆ Tₒ
169- ------------------------------------
170+ ----------------------------------
171 → Γ ⊢B input (reqres o x a b) ▹ Γ₁
172
173- t-wait-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
174- → (outSolRes o l Tₒ Tᵢ) ∈ Γ
175- → ¬ ((var x Tₓ) ∈ Γ)
176- → (var x Tᵢ) ∈ Γ₁
177- ------------------------
178- → Γ ⊢B wait r o l x ▹ Γ₁
179+ t-wait-new : ∀ {n} {Γ : Ctx n} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
180+ → outSolRes o l Tₒ Tᵢ ∈ Γ
181+ → ¬ (var x Tₓ ∈ Γ)
182+ ------------------------------------
183+ → Γ ⊢B wait r o l x ▹ (var x Tᵢ ∷ Γ)
184
185- t-wait-exists : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₒ Tᵢ Tₓ : Type} {o : Operation} {l : Location} {r : Channel} {x : Variable}
186- → (outSolRes o l Tₒ Tᵢ) ∈ Γ
187- → ((var x Tₓ) ∈ Γ)
188+ t-wait-exists : ∀ {n} {Γ : Ctx n} {Tₒ Tᵢ Tₓ : Type} {o : Operation} {l : Location} {r : Channel} {x : Variable}
189+ → outSolRes o l Tₒ Tᵢ ∈ Γ
190+ → var x Tₓ ∈ Γ
191 → Tᵢ ⊆ Tₓ
192 ------------------------
193- → Γ ⊢B wait r o l x ▹ Γ₁
194+ → Γ ⊢B wait r o l x ▹ Γ
195
196 t-exec : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₒ Tᵢ Tₓ : Type} {b : Behaviour} {r : Channel} {o : Operation} {x : Variable}
197- → (inReqRes o Tᵢ Tₒ) ∈ Γ
198+ → inReqRes o Tᵢ Tₒ ∈ Γ
199 → Γ ⊢B b ▹ Γ₁
200- → (var x Tₓ) ∈ Γ
201+ → var x Tₓ ∈ Γ
202 → Tₓ ⊆ Tₒ
203 ------------------------
204 → Γ ⊢B exec r o x b ▹ Γ₁
205+
206+congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → Γ ⊢B b1 ▹ Γ₁ → b1 ≡ b2 → Γ ⊢B b2 ▹ Γ₁
207+congruence t refl = t
208+
209+data SideEffect : ∀ {n m} → Ctx n → Ctx m → Set where
210+ updated : ∀ {n m} → (Γ : Ctx n) → (Γ₁ : Ctx m) → SideEffect Γ Γ₁
211+ identity : ∀ {n} → (Γ : Ctx n) → SideEffect Γ Γ
212+ undefined : SideEffect [] []
213+
214+preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B b ▹ Γ₁ → SideEffect Γ Γₐ → Γₐ ⊢B b ▹ Γ₁
215+preservation t undefined = t
216+preservation t (identity γ) = t
217+preservation t (updated Γ Γ₁)= {!!}