- commit
- 25ab3d5
- parent
- 1d23c47
- author
- Eugene Akentyev
- date
- 2017-01-07 23:18:07 +0400 +04
Clean up
6 files changed,
+33,
-181
+4,
-3
1@@ -1,14 +1,15 @@
2 module Expr where
3
4-open import Data.Maybe using (Maybe; just; nothing)
5 open import Variable
6
7
8--- TODO: add logic operations and, or
9 data BinOp : Set where
10+ -- Arithmetics
11 plus minus mult div power : BinOp
12+ -- Logical operations
13+ and or : BinOp
14
15 data Expr : Set where
16 var : Variable → Expr
17 binary : BinOp → Expr → Expr → Expr
18- constant : Variable.Value → Expr
19+ constant : Value → Expr
+1,
-0
1@@ -8,6 +8,7 @@ open import Type
2 open import Behaviour
3 open import Variable
4
5+
6 Queue : (A : Set) → Set
7 Queue A = List A
8
+3,
-155
1@@ -1,18 +1,8 @@
2 module Type where
3
4-import Data.Vec.Equality as VecEq
5-open import Level
6-open import Relation.Nullary
7-open import Relation.Binary
8-open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl; cong; cong₂)
9-open import Relation.Nullary.Decidable using (⌊_⌋)
10-open import Function
11-open import Data.Nat using (ℕ) renaming (_≟_ to _≟-Nat_)
12-open import Data.Empty
13-open import Data.String using (String) renaming (_≟_ to _≟-String_)
14-open import Data.List using (List; filter)
15-open import Data.Vec using (Vec; toList)
16-open import Expr
17+open import Data.Nat using (ℕ)
18+open import Data.String using (String)
19+open import Data.Vec using (Vec)
20 open import Variable
21
22
23@@ -28,157 +18,15 @@ Channel = String
24 data Type : Set where
25 bool int double long string raw void : Type
26
27-module TypeEq where
28- _≟_ : Decidable {A = Type} _≡_
29- bool ≟ bool = yes refl
30- int ≟ int = yes refl
31- double ≟ double = yes refl
32- long ≟ long = yes refl
33- string ≟ string = yes refl
34- raw ≟ raw = yes refl
35- void ≟ void = yes refl
36- bool ≟ int = no λ()
37- bool ≟ double = no λ()
38- bool ≟ long = no λ()
39- bool ≟ string = no λ()
40- bool ≟ raw = no λ()
41- bool ≟ void = no λ()
42- int ≟ bool = no λ()
43- int ≟ double = no λ()
44- int ≟ long = no λ()
45- int ≟ string = no λ()
46- int ≟ raw = no λ()
47- int ≟ void = no λ()
48- double ≟ bool = no λ()
49- double ≟ int = no λ()
50- double ≟ long = no λ()
51- double ≟ string = no λ()
52- double ≟ raw = no λ()
53- double ≟ void = no λ()
54- long ≟ bool = no λ()
55- long ≟ int = no λ()
56- long ≟ double = no λ()
57- long ≟ string = no λ()
58- long ≟ raw = no λ()
59- long ≟ void = no λ()
60- string ≟ bool = no λ()
61- string ≟ int = no λ()
62- string ≟ double = no λ()
63- string ≟ long = no λ()
64- string ≟ raw = no λ()
65- string ≟ void = no λ()
66- raw ≟ bool = no λ()
67- raw ≟ int = no λ()
68- raw ≟ double = no λ()
69- raw ≟ long = no λ()
70- raw ≟ string = no λ()
71- raw ≟ void = no λ()
72- void ≟ bool = no λ()
73- void ≟ int = no λ()
74- void ≟ double = no λ()
75- void ≟ long = no λ()
76- void ≟ string = no λ()
77- void ≟ raw = no λ()
78-
79 data TypeDecl : Set where
80 outNotify : Operation → Location → Type → TypeDecl
81 outSolRes : Operation → Location → Type → Type → TypeDecl
82 inOneWay : Operation → Type → TypeDecl
83 inReqRes : Operation → Type → Type → TypeDecl
84 var : Variable → Type → TypeDecl
85- empty : TypeDecl
86- pair : TypeDecl → TypeDecl → TypeDecl
87-
88-cong₃ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
89- (f : A → B → C → D) {x y u v m n} → x ≡ y → u ≡ v → m ≡ n → f x u m ≡ f y v n
90-cong₃ f refl refl refl = refl
91-
92-cong₄ : ∀ {a b c d e} {A : Set a} {B : Set b} {C : Set c} {D : Set d} {E : Set e}
93- (f : A → B → C → D → E) {x y u v m n k l} → x ≡ y → u ≡ v → m ≡ n → k ≡ l → f x u m k ≡ f y v n l
94-cong₄ f refl refl refl refl = refl
95-
96-module TypeDeclEq where
97- _≟_ : Decidable {A = TypeDecl} _≡_
98- (outNotify o1 l1 t1) ≟ (outNotify o2 l2 t2) with o1 ≟-String o2 | l1 ≟-String l2 | t1 TypeEq.≟ t2
99- ... | yes o | yes l | yes t = yes (cong₃ outNotify o l t)
100- ... | no ¬p | _ | _ = no (λ { refl → ¬p refl})
101- ... | _ | no ¬p | _ = no (λ { refl → ¬p refl})
102- ... | _ | _ | no ¬p = no (λ { refl → ¬p refl})
103- (outSolRes o1 l1 t1 t1') ≟ (outSolRes o2 l2 t2 t2') with o1 ≟-String o2 | l1 ≟-String l2 | t1 TypeEq.≟ t2 | t1' TypeEq.≟ t2'
104- ... | yes o | yes l | yes t | yes t' = yes (cong₄ outSolRes o l t t')
105- ... | no ¬p | _ | _ | _ = no (λ { refl → ¬p refl})
106- ... | _ | no ¬p | _ | _ = no (λ { refl → ¬p refl})
107- ... | _ | _ | no ¬p | _ = no (λ { refl → ¬p refl})
108- ... | _ | _ | _ | no ¬p = no (λ { refl → ¬p refl})
109- (inOneWay o1 t1) ≟ (inOneWay o2 t2) with o1 ≟-String o2 | t1 TypeEq.≟ t2
110- ... | yes o | yes t = yes (cong₂ inOneWay o t)
111- ... | no ¬p | _ = no (λ { refl → ¬p refl})
112- ... | _ | no ¬p = no (λ { refl → ¬p refl})
113- (inReqRes o1 t1 t1') ≟ (inReqRes o2 t2 t2') with o1 ≟-String o2 | t1 TypeEq.≟ t2 | t1' TypeEq.≟ t2'
114- ... | yes o | yes l | yes t = yes (cong₃ inReqRes o l t)
115- ... | no ¬p | _ | _ = no (λ { refl → ¬p refl})
116- ... | _ | no ¬p | _ = no (λ { refl → ¬p refl})
117- ... | _ | _ | no ¬p = no (λ { refl → ¬p refl})
118- (var v1 t1) ≟ (var v2 t2) with v1 ≟-Nat v2 | t1 TypeEq.≟ t2
119- ... | yes v | yes t = yes (cong₂ var v t)
120- ... | no ¬p | _ = no (λ { refl → ¬p refl})
121- ... | _ | no ¬p = no (λ { refl → ¬p refl})
122- (pair t1 t1') ≟ (pair t2 t2') with t1 ≟ t2 | t1' ≟ t2'
123- ... | yes t | yes t' = yes (cong₂ pair t t')
124- ... | no ¬p | _ = no (λ { refl → ¬p refl})
125- ... | _ | no ¬p = no (λ { refl → ¬p refl})
126- empty ≟ empty = yes refl
127- empty ≟ (outNotify _ _ _) = no λ()
128- empty ≟ (outSolRes _ _ _ _) = no λ()
129- empty ≟ (inOneWay _ _) = no λ()
130- empty ≟ (inReqRes _ _ _) = no λ()
131- empty ≟ (var _ _) = no λ()
132- empty ≟ (pair _ _) = no λ()
133- (outNotify _ _ _) ≟ (outSolRes _ _ _ _) = no λ()
134- (outNotify _ _ _) ≟ (inOneWay _ _) = no λ()
135- (outNotify _ _ _) ≟ (inReqRes _ _ _) = no λ()
136- (outNotify _ _ _) ≟ (var _ _) = no λ()
137- (outNotify _ _ _) ≟ empty = no λ()
138- (outNotify _ _ _) ≟ (pair _ _) = no λ()
139- (outSolRes _ _ _ _) ≟ (outNotify _ _ _) = no λ()
140- (outSolRes _ _ _ _) ≟ (inOneWay _ _) = no λ()
141- (outSolRes _ _ _ _) ≟ (inReqRes _ _ _) = no λ()
142- (outSolRes _ _ _ _) ≟ (var _ _) = no λ()
143- (outSolRes _ _ _ _) ≟ empty = no λ()
144- (outSolRes _ _ _ _) ≟ (pair _ _) = no λ()
145- (inOneWay _ _) ≟ (outNotify _ _ _) = no λ()
146- (inOneWay _ _) ≟ (outSolRes _ _ _ _) = no λ()
147- (inOneWay _ _) ≟ (inReqRes _ _ _) = no λ()
148- (inOneWay _ _) ≟ (var _ _) = no λ()
149- (inOneWay _ _) ≟ empty = no λ()
150- (inOneWay _ _) ≟ (pair _ _) = no λ()
151- (inReqRes _ _ _) ≟ (outNotify _ _ _) = no λ()
152- (inReqRes _ _ _) ≟ (outSolRes _ _ _ _) = no λ()
153- (inReqRes _ _ _) ≟ (inOneWay _ _) = no λ()
154- (inReqRes _ _ _) ≟ (var _ _) = no λ()
155- (inReqRes _ _ _) ≟ empty = no λ()
156- (inReqRes _ _ _) ≟ (pair _ _) = no λ()
157- (var _ _) ≟ (outNotify _ _ _) = no λ()
158- (var _ _) ≟ (outSolRes _ _ _ _) = no λ()
159- (var _ _) ≟ (inOneWay _ _) = no λ()
160- (var _ _) ≟ (inReqRes _ _ _) = no λ()
161- (var _ _) ≟ empty = no λ()
162- (var _ _) ≟ (pair _ _) = no λ()
163- (pair _ _) ≟ (outNotify _ _ _) = no λ()
164- (pair _ _) ≟ (outSolRes _ _ _ _) = no λ()
165- (pair _ _) ≟ (inOneWay _ _) = no λ()
166- (pair _ _) ≟ (inReqRes _ _ _) = no λ()
167- (pair _ _) ≟ (var _ _) = no λ()
168- (pair _ _) ≟ empty = no λ()
169-
170- decSetoid : DecSetoid _ _
171- decSetoid = PropEq.decSetoid _≟_
172
173 data _⊆_ : Type → Type → Set where
174 sub : {T₁ T₂ : Type} → T₁ ⊆ T₂
175
176 Ctx : ℕ → Set
177 Ctx = Vec TypeDecl
178-
179-module CtxEq = VecEq.DecidableEquality TypeDeclEq.decSetoid
180-module CtxPropEq = VecEq.PropositionalEquality
+24,
-21
1@@ -30,25 +30,25 @@ data Context : Set where
2
3 data _⊢B_▹_ : Context → Behaviour → Context → Set where
4 t-nil : ∀ {n} {Γ : Ctx n}
5- --------------
6+ ------------------
7 → ◆ Γ ⊢B nil ▹ ◆ Γ
8
9 t-if : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Expr}
10 → Γ ⊢ₑ e ∶ bool -- Γ ⊢ e : bool
11 → ◆ Γ ⊢B b1 ▹ ◆ Γ₁
12 → ◆ Γ ⊢B b2 ▹ ◆ Γ₁
13- ----------------------
14+ --------------------------
15 → ◆ Γ ⊢B if e b1 b2 ▹ ◆ Γ₁
16
17 t-while : ∀ {n} {Γ : Ctx n} {b : Behaviour} {e : Expr}
18 → Γ ⊢ₑ e ∶ bool
19 → ◆ Γ ⊢B b ▹ ◆ Γ
20- ---------------------
21+ ------------------------
22 → ◆ Γ ⊢B while e b ▹ ◆ Γ
23
24 t-choice : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {choices : List (Input_ex × Behaviour)}
25 → All (λ { (η , b) → ◆ Γ ⊢B seq (input η) b ▹ ◆ Γ₁ }) choices
26- -------------------------------
27+ -----------------------------------
28 → ◆ Γ ⊢B inputchoice choices ▹ ◆ Γ₁
29
30 t-par : ∀ {k k₁ p p₁} {Γ₁ : Ctx k} {Γ₂ : Ctx p} {Γ₁' : Ctx k₁} {Γ₂' : Ctx p₁}
31@@ -61,47 +61,47 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
32 t-seq : ∀ {n m k} {Γ : Ctx n} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour}
33 → ◆ Γ ⊢B b1 ▹ ◆ Γ₁
34 → ◆ Γ₁ ⊢B b2 ▹ ◆ Γ₂
35- ---------------------
36+ -------------------------
37 → ◆ Γ ⊢B seq b1 b2 ▹ ◆ Γ₂
38
39 t-notification : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
40 → (outNotify o l T₀) ∈ Γ
41 → Γ ⊢ e ∶ Tₑ
42 → Tₑ ⊆ T₀
43- ---------------------------------------------
44+ ------------------------------------------------
45 → ◆ Γ ⊢B output (notification o l (var e)) ▹ ◆ Γ
46
47 t-assign-new : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
48 → Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
49 → ¬ (var x Tₓ ∈ Γ) -- x ∉ Γ
50- -----------------------------------
51+ --------------------------------------
52 → ◆ Γ ⊢B assign x e ▹ ◆ (var x Tₑ ∷ Γ)
53
54 t-assign-exists : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
55 → Γ ⊢ₑ e ∶ Tₑ
56 → var x Tₓ ∈ Γ
57 → Tₑ ≡ Tₓ
58- ----------------------
59+ -------------------------
60 → ◆ Γ ⊢B assign x e ▹ ◆ Γ
61
62 t-oneway-new : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
63 → inOneWay o Tᵢ ∈ Γ
64 → ¬ (var x Tₓ ∈ Γ)
65- ------------------------------------------
66+ ----------------------------------------------
67 → ◆ Γ ⊢B input (oneway o x) ▹ ◆ (var x Tᵢ ∷ Γ)
68
69 t-oneway-exists : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
70 → inOneWay o Tᵢ ∈ Γ
71 → var x Tₓ ∈ Γ
72 → Tᵢ ⊆ Tₓ
73- ------------------------------
74+ ---------------------------------
75 → ◆ Γ ⊢B input (oneway o x) ▹ ◆ Γ
76
77 t-solresp-new : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
78 → outSolRes o l Tₒ Tᵢ ∈ Γ
79 → Tₑ ⊆ Tₒ
80 → ¬ (var x Tₓ ∈ Γ)
81- --------------------------------------------------
82+ -------------------------------------------------------
83 → ◆ Γ ⊢B output (solicitres o l e x) ▹ ◆ (var x Tᵢ ∷ Γ)
84
85 t-solresp-exists : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
86@@ -109,7 +109,7 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
87 → Tₑ ⊆ Tₒ
88 → var x Tₓ ∈ Γ
89 → Tᵢ ⊆ Tₓ
90- ---------------------------------------
91+ ------------------------------------------
92 → ◆ Γ ⊢B output (solicitres o l e x) ▹ ◆ Γ
93
94 t-reqresp-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
95@@ -118,7 +118,7 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
96 → ◆ (var x Tₓ ∷ Γ) ⊢B b ▹ ◆ Γ₁
97 → var a Tₐ ∈ Γ₁
98 → Tₐ ⊆ Tₒ
99- ----------------------------------
100+ --------------------------------------
101 → ◆ Γ ⊢B input (reqres o x a b) ▹ ◆ Γ₁
102
103 t-reqresp-exists : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable}
104@@ -128,20 +128,20 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
105 → ◆ Γ ⊢B b ▹ ◆ Γ₁
106 → var a Tₐ ∈ Γ₁
107 → Tₐ ⊆ Tₒ
108- ----------------------------------
109+ --------------------------------------
110 → ◆ Γ ⊢B input (reqres o x a b) ▹ ◆ Γ₁
111
112 t-wait-new : ∀ {n} {Γ : Ctx n} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
113 → outSolRes o l Tₒ Tᵢ ∈ Γ
114 → ¬ (var x Tₓ ∈ Γ)
115- ------------------------------------
116+ ----------------------------------------
117 → ◆ Γ ⊢B wait r o l x ▹ ◆ (var x Tᵢ ∷ Γ)
118
119 t-wait-exists : ∀ {n} {Γ : Ctx n} {Tₒ Tᵢ Tₓ : Type} {o : Operation} {l : Location} {r : Channel} {x : Variable}
120 → outSolRes o l Tₒ Tᵢ ∈ Γ
121 → var x Tₓ ∈ Γ
122 → Tᵢ ⊆ Tₓ
123- ------------------------
124+ ---------------------------
125 → ◆ Γ ⊢B wait r o l x ▹ ◆ Γ
126
127 t-exec : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₒ Tᵢ Tₓ : Type} {b : Behaviour} {r : Channel} {o : Operation} {x : Variable}
128@@ -149,7 +149,7 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
129 → ◆ Γ ⊢B b ▹ ◆ Γ₁
130 → var x Tₓ ∈ Γ
131 → Tₓ ⊆ Tₒ
132- ------------------------
133+ ----------------------------
134 → ◆ Γ ⊢B exec r o x b ▹ ◆ Γ₁
135
136 struct-congruence : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} → ◆ Γ ⊢B b1 ▹ ◆ Γ₁ → b1 ≡ b2 → ◆ Γ ⊢B b2 ▹ ◆ Γ₁
137@@ -164,13 +164,16 @@ struct-cong-par-nil (t-par t t-nil) = t
138 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) ▹ ■ Γ₂' Γ₁'
139 struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁
140
141+data Label : Set where
142+ x=e readt νr r:o r,o r,ol : Label
143+
144 data SideEffect : ∀ {n m} → Ctx n → Ctx m → Set where
145 updated : ∀ {n m} → (Γ : Ctx n) → (Γ₁ : Ctx m) → SideEffect Γ Γ₁
146 identity : ∀ {n} → (Γ : Ctx n) → SideEffect Γ Γ
147 undefined : SideEffect [] []
148
149-preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B b ▹ ◆ Γ₁ → SideEffect Γ Γₐ → ◆ Γₐ ⊢B b ▹ ◆ Γ₁
150-preservation t undefined = t
151-preservation t (identity γ) = t
152+--preservation : ∀ {n m k} {Γ : Ctx n} {Γₐ : Ctx k} {Γ₁ : Ctx m} {b : Behaviour} → ◆ Γ ⊢B b ▹ ◆ Γ₁ → SideEffect Γ Γₐ → ◆ Γₐ ⊢B b ▹ ◆ Γ₁
153+--preservation t undefined = t
154+--preservation t (identity γ) = t
155 --preservation t-nil (updated {_} {k} Γ Γₐ) = {!!}
156-preservation = {!!}
157+--preservation = {!!}
+1,
-0
1@@ -8,6 +8,7 @@ open import Type
2 open import Service
3 open import Behaviour
4
5+
6 data _⊢BSL_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
7 t-bsl-nil : ∀ {n} {Γ : Ctx n}
8 ----------------
+0,
-2
1@@ -3,8 +3,6 @@ module Variable where
2 open import Data.Integer using (ℤ)
3 open import Data.String using (String)
4 open import Data.Product using (_×_)
5-open import Data.Maybe using (Maybe)
6-open import Data.List using (List)
7 open import Data.Bool using (Bool)
8 open import Data.Nat using (ℕ)
9