- commit
- e4f03b5
- parent
- 82040fe
- author
- Eugene Akentyev
- date
- 2017-01-18 17:28:00 +0400 +04
Add typing rules for cases with disjoint union
1 files changed,
+80,
-12
+80,
-12
1@@ -28,25 +28,25 @@ data _⊢ₑ_∶_ (Γ : Context) : Expr → Type → Set where
2
3 data _⊢B_▹_ : Context → Behaviour → Context → Set where
4 t-nil : {Γ : Context}
5- ------------------
6+ --------------
7 → Γ ⊢B nil ▹ Γ
8
9 t-if : {Γ Γ₁ : Context} {b₁ b₂ : Behaviour} {e : Expr}
10 → Γ ⊢ₑ e ∶ bool -- Γ ⊢ e : bool
11 → Γ ⊢B b₁ ▹ Γ₁
12 → Γ ⊢B b₂ ▹ Γ₁
13- --------------------------
14+ --------------------------------
15 → Γ ⊢B if e then b₁ else b₂ ▹ Γ₁
16
17 t-while : {Γ : Context} {b : Behaviour} {e : Expr}
18 → Γ ⊢ₑ e ∶ bool
19 → Γ ⊢B b ▹ Γ
20- ------------------------
21+ -----------------------
22 → Γ ⊢B while[ e ] b ▹ Γ
23
24 t-choice : {Γ Γ₁ : Context} {choices : List (η × Behaviour)}
25 → All (λ { (η , b) → Γ ⊢B (input η) ∶ b ▹ Γ₁ }) choices
26- -----------------------------------
27+ -------------------------------
28 → Γ ⊢B inputchoice choices ▹ Γ₁
29
30 t-par : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b1 b2 : Behaviour}
31@@ -58,35 +58,59 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
32 t-seq : {Γ Γ₁ Γ₂ : Context} {b₁ b₂ : Behaviour}
33 → Γ ⊢B b₁ ▹ Γ₁
34 → Γ₁ ⊢B b₂ ▹ Γ₂
35- -----------------------
36+ -------------------
37 → Γ ⊢B b₁ ∶ b₂ ▹ Γ₂
38
39 t-notification : {Γ : Context} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
40 → (outNotify o l T₀) ∈ Γ
41 → var e Tₑ ∈ Γ
42 → Tₑ ⊆ T₀
43- ------------------------------------------------
44+ ------------------------------------
45 → Γ ⊢B output (o at 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 x ≃ e ▹ ◆ (var x Tₑ ∷ Γ)
53
54+ t-assign-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
55+ → ■ (◆ Γ) (◆ Γ₁) ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
56+ → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁)) -- x ∉ Γ
57+ -------------------------------------------------------
58+ → ■ (◆ Γ) (◆ Γ₁) ⊢B x ≃ e ▹ ■ (◆ (var x Tₑ ∷ Γ)) (◆ Γ₁)
59+
60+ t-assign-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
61+ → ■ (◆ Γ) (◆ Γ₁) ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
62+ → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁)) -- x ∉ Γ
63+ ------------------------------------------------------
64+ → ■ (◆ Γ) (◆ Γ₁) ⊢B x ≃ e ▹ ■ (◆ Γ) (◆ (var x Tₑ ∷ Γ₁))
65+
66 t-assign-exists : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
67 → Γ ⊢ₑ e ∶ Tₑ
68 → var x Tₓ ∈ Γ
69 → Tₑ ≡ Tₓ
70- -------------------------
71+ ----------------
72 → Γ ⊢B x ≃ e ▹ Γ
73
74 t-oneway-new : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
75 → inOneWay o Tᵢ ∈ ◆ Γ
76 → ¬ (var x Tₓ ∈ ◆ Γ)
77- ---------------------------------------
78+ -------------------------------------------
79 → ◆ Γ ⊢B input (o [ x ]) ▹ ◆ (var x Tᵢ ∷ Γ)
80
81+ t-oneway-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
82+ → inOneWay o Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁)
83+ → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
84+ -----------------------------------------------------------------
85+ → ■ (◆ Γ) (◆ Γ₁) ⊢B input (o [ x ]) ▹ ■ (◆ (var x Tᵢ ∷ Γ)) (◆ Γ₁)
86+
87+ t-oneway-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
88+ → inOneWay o Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁)
89+ → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
90+ -----------------------------------------------------------------
91+ → ■ (◆ Γ) (◆ Γ₁) ⊢B input (o [ x ]) ▹ ■ (◆ Γ) (◆ (var x Tᵢ ∷ Γ₁))
92+
93 t-oneway-exists : {Γ : Context} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
94 → inOneWay o Tᵢ ∈ Γ
95 → var x Tₓ ∈ Γ
96@@ -98,9 +122,23 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
97 → outSolRes o l Tₒ Tᵢ ∈ ◆ Γ
98 → Tₑ ⊆ Tₒ
99 → ¬ (var x Tₓ ∈ ◆ Γ)
100- --------------------------------------------------
101+ ------------------------------------------------------
102 → ◆ Γ ⊢B output (o at l [ e ][ x ]) ▹ ◆ (var x Tᵢ ∷ Γ)
103
104+ t-solresp-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
105+ → outSolRes o l Tₒ Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁)
106+ → Tₑ ⊆ Tₒ
107+ → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
108+ ----------------------------------------------------------------------------
109+ → ■ (◆ Γ) (◆ Γ₁) ⊢B output (o at l [ e ][ x ]) ▹ ■ (◆ (var x Tᵢ ∷ Γ)) (◆ Γ₁)
110+
111+ t-solresp-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
112+ → outSolRes o l Tₒ Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁)
113+ → Tₑ ⊆ Tₒ
114+ → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
115+ ----------------------------------------------------------------------------
116+ → ■ (◆ Γ) (◆ Γ₁) ⊢B output (o at l [ e ][ x ]) ▹ ■ (◆ Γ) (◆ (var x Tᵢ ∷ Γ₁))
117+
118 t-solresp-exists : {Γ : Context} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
119 → outSolRes o l Tₒ Tᵢ ∈ Γ
120 → Tₑ ⊆ Tₒ
121@@ -115,9 +153,27 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
122 → ◆ (var x Tₓ ∷ Γ) ⊢B b ▹ ◆ Γ₁
123 → var a Tₐ ∈ ◆ Γ₁
124 → Tₐ ⊆ Tₒ
125- ----------------------------------
126+ --------------------------------------
127 → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ ◆ Γ₁
128
129+ t-reqresp-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Γ₂ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
130+ → inReqRes o Tᵢ Tₒ ∈ ■ (◆ Γ) (◆ Γ₁)
131+ → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
132+ → ■ (◆ (var x Tₓ ∷ Γ)) (◆ Γ₁) ⊢B b ▹ Γ₂
133+ → var a Tₐ ∈ Γ₂
134+ → Tₐ ⊆ Tₒ
135+ ------------------------------------
136+ → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₂
137+
138+ t-reqresp-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Γ₂ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
139+ → inReqRes o Tᵢ Tₒ ∈ ■ (◆ Γ) (◆ Γ₁)
140+ → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
141+ → ■ (◆ Γ) (◆ (var x Tₓ ∷ Γ₁)) ⊢B b ▹ Γ₂
142+ → var a Tₐ ∈ Γ₂
143+ → Tₐ ⊆ Tₒ
144+ ------------------------------------
145+ → ◆ Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₂
146+
147 t-reqresp-exists : {Γ Γ₁ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable}
148 → (inReqRes o Tᵢ Tₒ) ∈ Γ
149 → var x Tₓ ∈ Γ
150@@ -131,9 +187,21 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
151 t-wait-new : ∀ {n} {Γ : Ctx n} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
152 → outSolRes o l Tₒ Tᵢ ∈ ◆ Γ
153 → ¬ (var x Tₓ ∈ ◆ Γ)
154- ------------------------------------
155+ ----------------------------------------
156 → ◆ Γ ⊢B wait r o l x ▹ ◆ (var x Tᵢ ∷ Γ)
157
158+ t-wait-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
159+ → outSolRes o l Tₒ Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁)
160+ → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
161+ --------------------------------------------------------------
162+ → ■ (◆ Γ) (◆ Γ₁) ⊢B wait r o l x ▹ ■ (◆ (var x Tᵢ ∷ Γ)) (◆ Γ₁)
163+
164+ t-wait-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
165+ → outSolRes o l Tₒ Tᵢ ∈ ■ (◆ Γ) (◆ Γ₁)
166+ → ¬ (var x Tₓ ∈ ■ (◆ Γ) (◆ Γ₁))
167+ --------------------------------------------------------------
168+ → ■ (◆ Γ) (◆ Γ₁) ⊢B wait r o l x ▹ ■ (◆ Γ) (◆ (var x Tᵢ ∷ Γ₁))
169+
170 t-wait-exists : {Γ : Context} {Tₒ Tᵢ Tₓ : Type} {o : Operation} {l : Location} {r : Channel} {x : Variable}
171 → outSolRes o l Tₒ Tᵢ ∈ Γ
172 → var x Tₓ ∈ Γ