- commit
- 91d804c
- parent
- dd77c46
- author
- Eugene Akentyev
- date
- 2017-01-16 16:13:26 +0400 +04
Rename side effect. Add comments.
3 files changed,
+56,
-29
+20,
-3
1@@ -7,15 +7,22 @@ open import Variable
2 open import Expr
3 open import Type
4
5-
6-data η̂ : Set where
7+-- Output
8+data η̂ : Set where
9+ -- o@l(e) -- Notification
10 _at_[_] : Operation → Location → Expr → η̂
11+
12+ -- o@l(e)(x) -- Solicit-response
13 _at_[_][_] : Operation → Location → Expr → Variable → η̂
14
15 data Behaviour : Set
16
17+-- Input
18 data η : Set where
19+ -- o(x) -- One-way
20 _[_] : Operation → Variable → η
21+
22+ -- o(x)(x'){B} -- Request-response
23 _[_][_]_ : Operation → Variable → Variable → Behaviour → η
24
25 data Behaviour where
26@@ -23,11 +30,21 @@ data Behaviour where
27 output : η̂ → Behaviour
28 if_then_else_ : Expr → Behaviour → Behaviour → Behaviour
29 while[_]_ : Expr → Behaviour → Behaviour
30+
31+ -- Sequence
32 _∶_ : Behaviour → Behaviour → Behaviour
33- _∣_ : Behaviour → Behaviour → Behaviour
34+
35+ -- Parallel
36+ _∥_ : Behaviour → Behaviour → Behaviour
37+
38+ -- Assign
39 _≃_ : Variable → Expr → Behaviour
40+
41 nil : Behaviour
42+
43+ -- [η₁]{B₁}⋯[ηₐ]{Bₐ} -- Input choice
44 inputchoice : List (η × Behaviour) → Behaviour
45+
46 wait : Channel → Operation → Location → Variable → Behaviour
47 exec : Channel → Operation → Variable → Behaviour → Behaviour
48
+1,
-1
1@@ -7,5 +7,5 @@ open import Service
2 data Network : Set where
3 [_]_ : Service → Location → Network
4 νr : Network → Network
5- _||_ : Network → Network → Network
6+ _∥_ : Network → Network → Network
7 nil : Network
+35,
-25
1@@ -14,10 +14,9 @@ open import Behaviour
2 open import Variable
3
4
5-data SideEffect : ∀ {n m} → Ctx n → Ctx m → Set where
6- updated : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} → SideEffect Γ Γ₁
7- identity : ∀ {n} → (Γ : Ctx n) → SideEffect Γ Γ
8- undefined : SideEffect [] []
9+data _⊢_↦_⊢_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Behaviour → Set where
10+ upd : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b₁ b₂ : Behaviour} → Γ ⊢ b₁ ↦ Γ₁ ⊢ b₂
11+ idn : ∀ {n} {Γ : Ctx n} {b : Behaviour} → Γ ⊢ b ↦ Γ ⊢ b
12
13 data _⊢ₑ_∶_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where
14 expr-t : {s : Expr} {b : Type}
15@@ -32,12 +31,12 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
16 ------------------
17 → ◆ Γ ⊢B nil ▹ ◆ Γ
18
19- t-if : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Expr}
20+ t-if : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b₁ b₂ : Behaviour} {e : Expr}
21 → Γ ⊢ₑ e ∶ bool -- Γ ⊢ e : bool
22- → ◆ Γ ⊢B b1 ▹ ◆ Γ₁
23- → ◆ Γ ⊢B b2 ▹ ◆ Γ₁
24+ → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁
25+ → ◆ Γ ⊢B b₂ ▹ ◆ Γ₁
26 --------------------------
27- → ◆ Γ ⊢B if e then b1 else b2 ▹ ◆ Γ₁
28+ → ◆ Γ ⊢B if e then b₁ else b₂ ▹ ◆ Γ₁
29
30 t-while : ∀ {n} {Γ : Ctx n} {b : Behaviour} {e : Expr}
31 → Γ ⊢ₑ e ∶ bool
32@@ -55,13 +54,13 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
33 → ◆ Γ₁ ⊢B b1 ▹ ◆ Γ₁'
34 → ◆ Γ₂ ⊢B b2 ▹ ◆ Γ₂'
35 --------------------------------------
36- → (■ Γ₁ Γ₂) ⊢B b1 ∣ b2 ▹ (■ Γ₁' Γ₂')
37+ → (■ Γ₁ Γ₂) ⊢B b1 ∥ b2 ▹ (■ Γ₁' Γ₂')
38
39- t-seq : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour}
40- → ◆ Γ ⊢B b1 ▹ ◆ Γ₁
41- → ◆ Γ₁ ⊢B b2 ▹ ◆ Γ₂
42+ t-seq : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b₁ b₂ : Behaviour}
43+ → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁
44+ → ◆ Γ₁ ⊢B b₂ ▹ ◆ Γ₂
45 -------------------------
46- → ◆ Γ ⊢B b1 ∶ b2 ▹ ◆ Γ₂
47+ → ◆ Γ ⊢B b₁ ∶ b₂ ▹ ◆ Γ₂
48
49 t-notification : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
50 → (outNotify o l T₀) ∈ Γ
51@@ -151,25 +150,36 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
52 ----------------------------
53 → ◆ Γ ⊢B exec r o x b ▹ ◆ Γ₁
54
55- t-mutate : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx m} {Γₐ : Ctx k} {b : Behaviour}
56- → SideEffect Γ Γₐ
57- → ◆ Γ ⊢B b ▹ ◆ Γ₁
58+ t-mutate : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx m} {Γₐ : Ctx k} {b₁ b₂ : Behaviour}
59+ → Γ ⊢ b₁ ↦ Γₐ ⊢ b₂
60+ → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁
61 ------------------
62- → ◆ Γₐ ⊢B b ▹ ◆ Γ₁
63+ → ◆ Γₐ ⊢B b₂ ▹ ◆ Γ₁
64
65
66-struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → ◆ Γ ⊢B b1 ▹ ◆ Γ₁ → b1 ≡ b2 → ◆ Γ ⊢B b2 ▹ ◆ Γ₁
67+struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b₁ b₂ : Behaviour}
68+ → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁
69+ → b₁ ≡ b₂
70+ → ◆ Γ ⊢B b₂ ▹ ◆ Γ₁
71 struct-congruence t refl = t
72
73-struct-cong-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B (nil ∶ b) ▹ ◆ Γ₁ → ◆ Γ ⊢B b ▹ ◆ Γ₁
74-struct-cong-nil (t-seq x x₁) = t-mutate updated x₁
75-struct-cong-nil (t-mutate x x₁) = t-mutate updated (struct-cong-nil x₁)
76-
77-struct-cong-par-nil : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b : Behaviour} → ■ Γ₁ Γ₂ ⊢B (b ∣ nil) ▹ ■ Γ₁' Γ₂' → ◆ Γ₁ ⊢B b ▹ ◆ Γ₁'
78+struct-cong-par-nil : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b : Behaviour}
79+ → ■ Γ₁ Γ₂ ⊢B (b ∥ nil) ▹ ■ Γ₁' Γ₂'
80+ → ◆ Γ₁ ⊢B b ▹ ◆ Γ₁'
81 struct-cong-par-nil (t-par x _) = x
82
83-struct-cong-par-sym : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b1 b2 : Behaviour} → ■ Γ₁ Γ₂ ⊢B (b1 ∣ b2) ▹ ■ Γ₁' Γ₂' → ■ Γ₂ Γ₁ ⊢B (b2 ∣ b1) ▹ ■ Γ₂' Γ₁'
84+struct-cong-par-sym : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b₁ b₂ : Behaviour}
85+ → ■ Γ₁ Γ₂ ⊢B (b₁ ∥ b₂) ▹ ■ Γ₁' Γ₂'
86+ → ■ Γ₂ Γ₁ ⊢B (b₂ ∥ b₁) ▹ ■ Γ₂' Γ₁'
87 struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁
88
89-preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B b ▹ ◆ Γ₁ → SideEffect Γ Γₐ → ◆ Γₐ ⊢B b ▹ ◆ Γ₁
90+struct-cong-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour}
91+ → ◆ Γ ⊢B (nil ∶ b) ▹ ◆ Γ₁
92+ → ◆ Γ ⊢B b ▹ ◆ Γ₁
93+struct-cong-nil = t-mutate upd
94+
95+preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b₁ b₂ : Behaviour}
96+ → ◆ Γ ⊢B b₁ ▹ ◆ Γ₁
97+ → Γ ⊢ b₁ ↦ Γₐ ⊢ b₂
98+ → ◆ Γₐ ⊢B b₂ ▹ ◆ Γ₁
99 preservation x s = t-mutate s x