- commit
- 1d23c47
- parent
- 7b68f9a
- author
- Eugene Akentyev
- date
- 2017-01-03 02:49:52 +0400 +04
Added disjoint union
2 files changed,
+51,
-48
+48,
-48
1@@ -24,82 +24,85 @@ data _⊢ₑ_∶_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where
2 expr-t : {s : Expr} {b : Type}
3 → Γ ⊢ₑ s ∶ b
4
5-data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
6+data Context : Set where
7+ ◆ : ∀ {n} → Ctx n → Context
8+ ■ : ∀ {n m} → Ctx n → Ctx m → Context
9+
10+data _⊢B_▹_ : Context → Behaviour → Context → Set where
11 t-nil : ∀ {n} {Γ : Ctx n}
12 --------------
13- → Γ ⊢B nil ▹ Γ
14+ → ◆ Γ ⊢B nil ▹ ◆ Γ
15
16 t-if : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Expr}
17 → Γ ⊢ₑ e ∶ bool -- Γ ⊢ e : bool
18- → Γ ⊢B b1 ▹ Γ₁
19- → Γ ⊢B b2 ▹ Γ₁
20+ → ◆ Γ ⊢B b1 ▹ ◆ Γ₁
21+ → ◆ Γ ⊢B b2 ▹ ◆ Γ₁
22 ----------------------
23- → Γ ⊢B if e b1 b2 ▹ Γ₁
24+ → ◆ Γ ⊢B if e b1 b2 ▹ ◆ Γ₁
25
26 t-while : ∀ {n} {Γ : Ctx n} {b : Behaviour} {e : Expr}
27 → Γ ⊢ₑ e ∶ bool
28- → Γ ⊢B b ▹ Γ
29+ → ◆ Γ ⊢B b ▹ ◆ Γ
30 ---------------------
31- → Γ ⊢B while e b ▹ Γ
32+ → ◆ Γ ⊢B while e b ▹ ◆ Γ
33
34 t-choice : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {choices : List (Input_ex × Behaviour)}
35- → All (λ { (η , b) → Γ ⊢B seq (input η) b ▹ Γ₁ }) choices
36+ → All (λ { (η , b) → ◆ Γ ⊢B seq (input η) b ▹ ◆ Γ₁ }) choices
37 -------------------------------
38- → Γ ⊢B inputchoice choices ▹ Γ₁
39+ → ◆ Γ ⊢B inputchoice choices ▹ ◆ Γ₁
40
41- t-par : ∀ {n m} {Γ : Ctx n} {k k₁ p p₁ : ℕ} {b1 b2 : Behaviour}
42- {Γ₁ : Ctx k} {Γ₁' : Ctx k₁} {Γ₂ : Ctx p} {Γ₂' : Ctx p₁} {Γ' : Ctx m}
43- → Γ₁ ⊢B b1 ▹ Γ₁'
44- → Γ₂ ⊢B b2 ▹ Γ₂'
45- -- TODO: maybe it's not enough to express that Γ = Γ₁, Γ₂ and Γ' = Γ₁', Γ₂' - disjoint unions
46- ----------------------------------------
47- → (Γ₁ ++ Γ₂) ⊢B par b1 b2 ▹ (Γ₁' ++ Γ₂')
48+ t-par : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁}
49+ {b1 b2 : Behaviour}
50+ → ◆ Γ₁ ⊢B b1 ▹ ◆ Γ₁'
51+ → ◆ Γ₂ ⊢B b2 ▹ ◆ Γ₂'
52+ --------------------------------------
53+ → (■ Γ₁ Γ₂) ⊢B par b1 b2 ▹ (■ Γ₁' Γ₂')
54
55 t-seq : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour}
56- → Γ ⊢B b1 ▹ Γ₁
57- → Γ₁ ⊢B b2 ▹ Γ₂
58+ → ◆ Γ ⊢B b1 ▹ ◆ Γ₁
59+ → ◆ Γ₁ ⊢B b2 ▹ ◆ Γ₂
60 ---------------------
61- → Γ ⊢B seq b1 b2 ▹ Γ₂
62+ → ◆ Γ ⊢B seq b1 b2 ▹ ◆ Γ₂
63
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)) ▹ Γ
70+ → ◆ Γ ⊢B output (notification o l (var e)) ▹ ◆ Γ
71
72 t-assign-new : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
73 → Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
74 → ¬ (var x Tₓ ∈ Γ) -- x ∉ Γ
75 -----------------------------------
76- → Γ ⊢B assign x e ▹ (var x Tₑ ∷ Γ)
77+ → ◆ Γ ⊢B assign x e ▹ ◆ (var x Tₑ ∷ Γ)
78
79 t-assign-exists : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
80 → Γ ⊢ₑ e ∶ Tₑ
81 → var x Tₓ ∈ Γ
82 → Tₑ ≡ Tₓ
83 ----------------------
84- → Γ ⊢B assign x e ▹ Γ
85+ → ◆ Γ ⊢B assign x e ▹ ◆ Γ
86
87 t-oneway-new : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
88 → inOneWay o Tᵢ ∈ Γ
89 → ¬ (var x Tₓ ∈ Γ)
90 ------------------------------------------
91- → Γ ⊢B input (oneway o x) ▹ (var x Tᵢ ∷ Γ)
92+ → ◆ Γ ⊢B input (oneway o x) ▹ ◆ (var x Tᵢ ∷ Γ)
93
94 t-oneway-exists : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
95 → inOneWay o Tᵢ ∈ Γ
96 → var x Tₓ ∈ Γ
97 → Tᵢ ⊆ Tₓ
98 ------------------------------
99- → Γ ⊢B input (oneway o x) ▹ Γ
100+ → ◆ Γ ⊢B input (oneway o x) ▹ ◆ Γ
101
102 t-solresp-new : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
103 → outSolRes o l Tₒ Tᵢ ∈ Γ
104 → Tₑ ⊆ Tₒ
105 → ¬ (var x Tₓ ∈ Γ)
106 --------------------------------------------------
107- → Γ ⊢B output (solicitres o l e x) ▹ (var x Tᵢ ∷ Γ)
108+ → ◆ Γ ⊢B output (solicitres o l e x) ▹ ◆ (var x Tᵢ ∷ Γ)
109
110 t-solresp-exists : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
111 → outSolRes o l Tₒ Tᵢ ∈ Γ
112@@ -107,70 +110,67 @@ data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
113 → var x Tₓ ∈ Γ
114 → Tᵢ ⊆ Tₓ
115 ---------------------------------------
116- → Γ ⊢B output (solicitres o l e x) ▹ Γ
117+ → ◆ Γ ⊢B output (solicitres o l e x) ▹ ◆ Γ
118
119 t-reqresp-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
120 → inReqRes o Tᵢ Tₒ ∈ Γ
121 → ¬ (var x Tₓ ∈ Γ)
122- → (var x Tₓ ∷ Γ) ⊢B b ▹ Γ₁
123+ → ◆ (var x Tₓ ∷ Γ) ⊢B b ▹ ◆ Γ₁
124 → var a Tₐ ∈ Γ₁
125 → Tₐ ⊆ Tₒ
126 ----------------------------------
127- → Γ ⊢B input (reqres o x a b) ▹ Γ₁
128+ → ◆ Γ ⊢B input (reqres o x a b) ▹ ◆ Γ₁
129
130 t-reqresp-exists : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable}
131 → (inReqRes o Tᵢ Tₒ) ∈ Γ
132 → var x Tₓ ∈ Γ
133 → Tᵢ ⊆ Tₓ
134- → Γ ⊢B b ▹ Γ₁
135+ → ◆ Γ ⊢B b ▹ ◆ Γ₁
136 → var a Tₐ ∈ Γ₁
137 → Tₐ ⊆ Tₒ
138 ----------------------------------
139- → Γ ⊢B input (reqres o x a b) ▹ Γ₁
140+ → ◆ Γ ⊢B input (reqres o x a b) ▹ ◆ Γ₁
141
142 t-wait-new : ∀ {n} {Γ : Ctx n} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
143 → outSolRes o l Tₒ Tᵢ ∈ Γ
144 → ¬ (var x Tₓ ∈ Γ)
145 ------------------------------------
146- → Γ ⊢B wait r o l x ▹ (var x Tᵢ ∷ Γ)
147+ → ◆ Γ ⊢B wait r o l x ▹ ◆ (var x Tᵢ ∷ Γ)
148
149 t-wait-exists : ∀ {n} {Γ : Ctx n} {Tₒ Tᵢ Tₓ : Type} {o : Operation} {l : Location} {r : Channel} {x : Variable}
150 → outSolRes o l Tₒ Tᵢ ∈ Γ
151 → var x Tₓ ∈ Γ
152 → Tᵢ ⊆ Tₓ
153 ------------------------
154- → Γ ⊢B wait r o l x ▹ Γ
155+ → ◆ Γ ⊢B wait r o l x ▹ ◆ Γ
156
157 t-exec : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₒ Tᵢ Tₓ : Type} {b : Behaviour} {r : Channel} {o : Operation} {x : Variable}
158 → inReqRes o Tᵢ Tₒ ∈ Γ
159- → Γ ⊢B b ▹ Γ₁
160+ → ◆ Γ ⊢B b ▹ ◆ Γ₁
161 → var x Tₓ ∈ Γ
162 → Tₓ ⊆ Tₒ
163 ------------------------
164- → Γ ⊢B exec r o x b ▹ Γ₁
165+ → ◆ Γ ⊢B exec r o x b ▹ ◆ Γ₁
166
167-struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → Γ ⊢B b1 ▹ Γ₁ → b1 ≡ b2 → Γ ⊢B b2 ▹ Γ₁
168+struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → ◆ Γ ⊢B b1 ▹ ◆ Γ₁ → b1 ≡ b2 → ◆ Γ ⊢B b2 ▹ ◆ Γ₁
169 struct-congruence t refl = t
170
171-struct-cong-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B (seq nil b) ▹ Γ₁ → Γ ⊢B b ▹ Γ₁
172+struct-cong-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B (seq nil b) ▹ ◆ Γ₁ → ◆ Γ ⊢B b ▹ ◆ Γ₁
173 struct-cong-nil (t-seq t-nil t) = t
174
175---struct-cong-par-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B (par b nil) ▹ Γ₁ → Γ ⊢B b ▹ Γ₁
176---struct-cong-par-nil (t-par t t-nil) = {!!}
177-
178---struct-cong-par-sym : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → Γ ⊢B (par b1 b2) ▹ Γ₁ → Γ ⊢B (par b2 b1) ▹ Γ₁
179---struct-cong-par-sym (t-par t₁ t₂) = {!!}
180+struct-cong-par-nil : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b : Behaviour} → ■ Γ₁ Γ₂ ⊢B (par b nil) ▹ ■ Γ₁' Γ₂' → ◆ Γ₁ ⊢B b ▹ ◆ Γ₁'
181+struct-cong-par-nil (t-par t t-nil) = t
182
183---struct-cong-par-assoc : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 b3 : Behaviour} → Γ ⊢B par (par b1 b2) b3 ▹ Γ₁ → Γ ⊢B par b1 (par b2 b3) ▹ Γ₁
184---struct-cong-par-assoc (t-par (t-par t₁ t₂) t₃) = {!!}
185+struct-cong-par-sym : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b1 b2 : Behaviour} → ■ Γ₁ Γ₂ ⊢B (par b1 b2) ▹ ■ Γ₁' Γ₂' → ■ Γ₂ Γ₁ ⊢B (par b2 b1) ▹ ■ Γ₂' Γ₁'
186+struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁
187
188 data SideEffect : ∀ {n m} → Ctx n → Ctx m → Set where
189 updated : ∀ {n m} → (Γ : Ctx n) → (Γ₁ : Ctx m) → SideEffect Γ Γ₁
190 identity : ∀ {n} → (Γ : Ctx n) → SideEffect Γ Γ
191 undefined : SideEffect [] []
192
193---preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b : Behaviour} → Γ ⊢B b ▹ Γ₁ → SideEffect Γ Γₐ → Γₐ ⊢B b ▹ Γ₁
194---preservation t undefined = t
195---preservation t (identity γ) = t
196---preservation t-nil (updated {_} {k} Γ Γₐ) = t-nil {k} {Γₐ}
197---preservation = {!!}
198+preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B b ▹ ◆ Γ₁ → SideEffect Γ Γₐ → ◆ Γₐ ⊢B b ▹ ◆ Γ₁
199+preservation t undefined = t
200+preservation t (identity γ) = t
201+--preservation t-nil (updated {_} {k} Γ Γₐ) = {!!}
202+preservation = {!!}
+3,
-0
1@@ -18,6 +18,8 @@ data _⊢BSL_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
2 -- → All (λ { (η , b) → Γ ⊢B seq (input η) b ▹ Γ₁ }) choices
3 -- → Γ ⊢BSL
4
5+data _⊢state_ : ∀ {n} → Ctx n → Process → Set where
6+
7 data _⊢P_ : ∀ {n} → Ctx n → Process → Set where
8 t-process-nil : ∀ {n} {Γ : Ctx n}
9 ----------
10@@ -29,6 +31,7 @@ data _⊢P_ : ∀ {n} → Ctx n → Process → Set where
11 ----------------
12 → Γ ⊢P par p₁ p₂
13
14+
15 data _⊢S_ : ∀ {n} → Ctx n → Service → Set where
16 t-service : ∀ {n m} {Γ : Ctx n} {b : Behaviour} {d : Deployment m} {p : Process}
17 ------------------