- commit
- 54b8b36
- parent
- 25ab3d5
- author
- Eugene Akentyev
- date
- 2017-01-08 05:22:36 +0400 +04
Change to unicode syntax for behaviour
2 files changed,
+32,
-32
+14,
-14
1@@ -8,26 +8,26 @@ open import Expr
2 open import Type
3
4
5-data Output_ex : Set where
6- notification : Operation → Location → Expr → Output_ex
7- solicitres : Operation → Location → Expr → Variable → Output_ex
8+data η̂ : Set where
9+ _at_[_] : Operation → Location → Expr → η̂
10+ _at_[_][_] : Operation → Location → Expr → Variable → η̂
11
12 data Behaviour : Set
13
14-data Input_ex : Set where
15- oneway : Operation → Variable → Input_ex
16- reqres : Operation → Variable → Variable → Behaviour → Input_ex
17+data η : Set where
18+ _[_] : Operation → Variable → η
19+ _[_][_]_ : Operation → Variable → Variable → Behaviour → η
20
21 data Behaviour where
22- input : Input_ex → Behaviour
23- output : Output_ex → Behaviour
24- if : Expr → Behaviour → Behaviour → Behaviour
25- while : Expr → Behaviour → Behaviour
26- seq : Behaviour → Behaviour → Behaviour
27- par : Behaviour → Behaviour → Behaviour
28- assign : Variable → Expr → Behaviour
29+ input : η → Behaviour
30+ output : η̂ → Behaviour
31+ if_then_else_ : Expr → Behaviour → Behaviour → Behaviour
32+ while[_]_ : Expr → Behaviour → Behaviour
33+ _∶_ : Behaviour → Behaviour → Behaviour
34+ _∣_ : Behaviour → Behaviour → Behaviour
35+ _≃_ : Variable → Expr → Behaviour
36 nil : Behaviour
37- inputchoice : List (Input_ex × Behaviour) → Behaviour
38+ inputchoice : List (η × Behaviour) → Behaviour
39 wait : Channel → Operation → Location → Variable → Behaviour
40 exec : Channel → Operation → Variable → Behaviour → Behaviour
41
+18,
-18
1@@ -38,16 +38,16 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
2 → ◆ Γ ⊢B b1 ▹ ◆ Γ₁
3 → ◆ Γ ⊢B b2 ▹ ◆ Γ₁
4 --------------------------
5- → ◆ Γ ⊢B if e b1 b2 ▹ ◆ Γ₁
6+ → ◆ Γ ⊢B if e then b1 else b2 ▹ ◆ Γ₁
7
8 t-while : ∀ {n} {Γ : Ctx n} {b : Behaviour} {e : Expr}
9 → Γ ⊢ₑ e ∶ bool
10 → ◆ Γ ⊢B b ▹ ◆ Γ
11 ------------------------
12- → ◆ Γ ⊢B while e b ▹ ◆ Γ
13+ → ◆ Γ ⊢B while[ e ] b ▹ ◆ Γ
14
15- t-choice : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {choices : List (Input_ex × Behaviour)}
16- → All (λ { (η , b) → ◆ Γ ⊢B seq (input η) b ▹ ◆ Γ₁ }) choices
17+ t-choice : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {choices : List (η × Behaviour)}
18+ → All (λ { (η , b) → ◆ Γ ⊢B (input η) ∶ b ▹ ◆ Γ₁ }) choices
19 -----------------------------------
20 → ◆ Γ ⊢B inputchoice choices ▹ ◆ Γ₁
21
22@@ -56,53 +56,53 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
23 → ◆ Γ₁ ⊢B b1 ▹ ◆ Γ₁'
24 → ◆ Γ₂ ⊢B b2 ▹ ◆ Γ₂'
25 --------------------------------------
26- → (■ Γ₁ Γ₂) ⊢B par b1 b2 ▹ (■ Γ₁' Γ₂')
27+ → (■ Γ₁ Γ₂) ⊢B b1 ∣ b2 ▹ (■ Γ₁' Γ₂')
28
29 t-seq : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour}
30 → ◆ Γ ⊢B b1 ▹ ◆ Γ₁
31 → ◆ Γ₁ ⊢B b2 ▹ ◆ Γ₂
32 -------------------------
33- → ◆ Γ ⊢B seq b1 b2 ▹ ◆ Γ₂
34+ → ◆ Γ ⊢B b1 ∶ b2 ▹ ◆ Γ₂
35
36 t-notification : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
37 → (outNotify o l T₀) ∈ Γ
38 → Γ ⊢ e ∶ Tₑ
39 → Tₑ ⊆ T₀
40 ------------------------------------------------
41- → ◆ Γ ⊢B output (notification o l (var e)) ▹ ◆ Γ
42+ → ◆ Γ ⊢B output (o at l [ var e ]) ▹ ◆ Γ
43
44 t-assign-new : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
45 → Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
46 → ¬ (var x Tₓ ∈ Γ) -- x ∉ Γ
47 --------------------------------------
48- → ◆ Γ ⊢B assign x e ▹ ◆ (var x Tₑ ∷ Γ)
49+ → ◆ Γ ⊢B x ≃ e ▹ ◆ (var x Tₑ ∷ Γ)
50
51 t-assign-exists : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
52 → Γ ⊢ₑ e ∶ Tₑ
53 → var x Tₓ ∈ Γ
54 → Tₑ ≡ Tₓ
55 -------------------------
56- → ◆ Γ ⊢B assign x e ▹ ◆ Γ
57+ → ◆ Γ ⊢B x ≃ e ▹ ◆ Γ
58
59 t-oneway-new : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
60 → inOneWay o Tᵢ ∈ Γ
61 → ¬ (var x Tₓ ∈ Γ)
62 ----------------------------------------------
63- → ◆ Γ ⊢B input (oneway o x) ▹ ◆ (var x Tᵢ ∷ Γ)
64+ → ◆ Γ ⊢B input (o [ x ]) ▹ ◆ (var x Tᵢ ∷ Γ)
65
66 t-oneway-exists : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
67 → inOneWay o Tᵢ ∈ Γ
68 → var x Tₓ ∈ Γ
69 → Tᵢ ⊆ Tₓ
70 ---------------------------------
71- → ◆ Γ ⊢B input (oneway o x) ▹ ◆ Γ
72+ → ◆ Γ ⊢B input (o [ x ]) ▹ ◆ Γ
73
74 t-solresp-new : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
75 → outSolRes o l Tₒ Tᵢ ∈ Γ
76 → Tₑ ⊆ Tₒ
77 → ¬ (var x Tₓ ∈ Γ)
78 -------------------------------------------------------
79- → ◆ Γ ⊢B output (solicitres o l e x) ▹ ◆ (var x Tᵢ ∷ Γ)
80+ → ◆ Γ ⊢B output (o at l [ e ][ x ]) ▹ ◆ (var x Tᵢ ∷ Γ)
81
82 t-solresp-exists : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
83 → outSolRes o l Tₒ Tᵢ ∈ Γ
84@@ -110,7 +110,7 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
85 → var x Tₓ ∈ Γ
86 → Tᵢ ⊆ Tₓ
87 ------------------------------------------
88- → ◆ Γ ⊢B output (solicitres o l e x) ▹ ◆ Γ
89+ → ◆ Γ ⊢B output (o at l [ e ][ x ]) ▹ ◆ Γ
90
91 t-reqresp-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
92 → inReqRes o Tᵢ Tₒ ∈ Γ
93@@ -119,7 +119,7 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
94 → var a Tₐ ∈ Γ₁
95 → Tₐ ⊆ Tₒ
96 --------------------------------------
97- → ◆ Γ ⊢B input (reqres o x a b) ▹ ◆ Γ₁
98+ → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ ◆ Γ₁
99
100 t-reqresp-exists : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable}
101 → (inReqRes o Tᵢ Tₒ) ∈ Γ
102@@ -129,7 +129,7 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
103 → var a Tₐ ∈ Γ₁
104 → Tₐ ⊆ Tₒ
105 --------------------------------------
106- → ◆ Γ ⊢B input (reqres o x a b) ▹ ◆ Γ₁
107+ → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ ◆ Γ₁
108
109 t-wait-new : ∀ {n} {Γ : Ctx n} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
110 → outSolRes o l Tₒ Tᵢ ∈ Γ
111@@ -155,13 +155,13 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
112 struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → ◆ Γ ⊢B b1 ▹ ◆ Γ₁ → b1 ≡ b2 → ◆ Γ ⊢B b2 ▹ ◆ Γ₁
113 struct-congruence t refl = t
114
115-struct-cong-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B (seq nil b) ▹ ◆ Γ₁ → ◆ Γ ⊢B b ▹ ◆ Γ₁
116+struct-cong-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B (nil ∶ b) ▹ ◆ Γ₁ → ◆ Γ ⊢B b ▹ ◆ Γ₁
117 struct-cong-nil (t-seq t-nil t) = t
118
119-struct-cong-par-nil : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b : Behaviour} → ■ Γ₁ Γ₂ ⊢B (par b nil) ▹ ■ Γ₁' Γ₂' → ◆ Γ₁ ⊢B b ▹ ◆ Γ₁'
120+struct-cong-par-nil : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁} {b : Behaviour} → ■ Γ₁ Γ₂ ⊢B (b ∣ nil) ▹ ■ Γ₁' Γ₂' → ◆ Γ₁ ⊢B b ▹ ◆ Γ₁'
121 struct-cong-par-nil (t-par t t-nil) = t
122
123-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) ▹ ■ Γ₂' Γ₁'
124+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) ▹ ■ Γ₂' Γ₁'
125 struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁
126
127 data Label : Set where