- commit
- a867bc4
- parent
- bba29dc
- author
- Eugene Akentyev
- date
- 2016-12-08 00:32:24 +0400 +04
Fix equality of contexts
1 files changed,
+27,
-29
+27,
-29
1@@ -1,11 +1,10 @@
2-
3 module Typecheck where
4
5 import Data.List as List
6 import Data.Vec.Equality as VecEq
7 open import Relation.Nullary using (¬_)
8 open import Relation.Nullary
9-open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
10+open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; subst)
11 open import Data.Nat using (ℕ; _+_; suc)
12 open import Data.Vec using (Vec; _∈_; zip; _∷_)
13 open import Expr
14@@ -14,32 +13,36 @@ open import Behaviour
15 open import Variable
16
17
18-data _⊢_of_ {n : ℕ} (Γ : Ctx n) : Variable → Type → Set where
19+substCtx : {n m : ℕ} → n ≡ m → Ctx n → Ctx m
20+substCtx n≡m Γ = subst (λ x → Vec TypeDecl x) n≡m Γ
21+
22+data _⊢_∶_ {n : ℕ} (Γ : Ctx n) : Variable → Type → Set where
23 var-t : {s : Variable} {b : Type}
24- → Γ ⊢ s of b
25+ → (var s b) ∈ Γ
26+ ------------
27+ → Γ ⊢ s ∶ b
28
29 data _⊢ₑ_of_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where
30 expr-t : {s : Expr} {b : Type}
31 → Γ ⊢ₑ s of b
32
33-data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set where
34- t-nil : {Γ₁ : Ctx m}
35- → n ≡ m
36- --------------
37- → Γ ⊢B nil ▹ Γ₁
38+data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
39+ t-nil : {n≡m : n ≡ m}
40+ ---------------------------
41+ → Γ ⊢B nil ▹ substCtx n≡m Γ
42
43 t-if : {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Variable}
44- → Γ ⊢ e of bool -- Γ ⊢ e : bool
45+ → Γ ⊢ e ∶ bool -- Γ ⊢ e : bool
46 → Γ ⊢B b1 ▹ Γ₁
47 → Γ ⊢B b2 ▹ Γ₁
48 ---------------------------
49 → Γ ⊢B if (var e) b1 b2 ▹ Γ₁
50
51- t-while : {Γ₁ : Ctx m} {b : Behaviour} {e : Variable}
52- → Γ ⊢ e of bool
53- → Γ ⊢B b ▹ Γ₁
54+ t-while : {n≡m : n ≡ m} {b : Behaviour} {e : Variable}
55+ → Γ ⊢ e ∶ bool
56+ → Γ ⊢B b ▹ Γ
57 --------------------------
58- → Γ ⊢B while (var e) b ▹ Γ₁
59+ → Γ ⊢B while (var e) b ▹ substCtx n≡m Γ
60
61 t-choice : {Γ₁ : Ctx m} {k n : ℕ} {η : Input_ex} {inputs : Vec Input_ex n}
62 {b : Behaviour} {behaviours : Vec Behaviour n}
63@@ -63,13 +66,12 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set
64 --------------------
65 → Γ ⊢B seq b1 b2 ▹ Γ₂
66
67- t-notification : {k : ℕ} {Γ₁ : Ctx m} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
68+ t-notification : {n≡m : n ≡ m} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
69 → (outNotify o l T₀) ∈ Γ
70- → Γ ⊢ e of Tₑ
71+ → Γ ⊢ e ∶ Tₑ
72 → Tₑ ⊆ T₀
73- → n ≡ m
74 -------------------------------------------
75- → Γ ⊢B output (notification o l (var e)) ▹ Γ₁
76+ → Γ ⊢B output (notification o l (var e)) ▹ substCtx n≡m Γ
77
78 t-assign-new : {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
79 → Γ ⊢ₑ e of Tₑ -- Γ ⊢ e : bool
80@@ -78,13 +80,12 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set
81 ---------------------
82 → Γ ⊢B assign x e ▹ Γ₁
83
84- t-assign-exists : {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
85+ t-assign-exists : {n≡m : n ≡ m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
86 → Γ ⊢ₑ e of Tₑ
87 → (var x Tₓ) ∈ Γ
88 → Tₑ ≡ Tₓ
89- → n ≡ m -- TODO Γ ≡ Γ₁
90 ---------------------
91- → Γ ⊢B assign x e ▹ Γ₁
92+ → Γ ⊢B assign x e ▹ substCtx n≡m Γ
93
94 t-oneway-new : {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
95 → (inOneWay o Tᵢ) ∈ Γ
96@@ -93,13 +94,12 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set
97 -------------------------------
98 → Γ ⊢B (input (oneway o x)) ▹ Γ₁
99
100- t-oneway-exists : {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
101+ t-oneway-exists : {n≡m : n ≡ m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
102 → (inOneWay o Tᵢ) ∈ Γ
103 → ((var x Tₓ) ∈ Γ)
104 → Tᵢ ⊆ Tₓ
105- → n ≡ m -- TODO Γ ≡ Γ₁
106 --------------------------------
107- → Γ ⊢B (input (oneway o x)) ▹ Γ₁
108+ → Γ ⊢B (input (oneway o x)) ▹ substCtx n≡m Γ
109
110 t-solresp-new : {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
111 → (outSolRes o l Tₒ Tᵢ) ∈ Γ
112@@ -109,14 +109,13 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set
113 -----------------------------------------
114 → Γ ⊢B (output (solicitres o l e x)) ▹ Γ₁
115
116- t-solresp-exists : {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
117+ t-solresp-exists : {n≡m : n ≡ m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
118 → (outSolRes o l Tₒ Tᵢ) ∈ Γ
119 → Tₑ ⊆ Tₒ
120 → (var x Tₓ) ∈ Γ
121 → Tᵢ ⊆ Tₓ
122- → n ≡ m -- TODO Γ ≡ Γ₁
123 -----------------------------------------
124- → Γ ⊢B (output (solicitres o l e x)) ▹ Γ₁
125+ → Γ ⊢B (output (solicitres o l e x)) ▹ substCtx n≡m Γ
126
127 t-reqresp-new : {p : ℕ} {Γₓ : Ctx p} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
128 → (inReqRes o Tᵢ Tₒ) ∈ Γ
129@@ -138,6 +137,5 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set
130 ------------------------------------
131 → Γ ⊢B (input (reqres o x a b)) ▹ Γ₁
132
133-
134-check-B : {n m : ℕ} {Γ₁ : Ctx m} → (Γ : Ctx n) → (B : Behaviour) → Dec (Γ ⊢B B ▹ Γ₁)
135+check-B : {n m : ℕ} {Γ₁ : Ctx m} → (Γ : Ctx n) → (b : Behaviour) → Dec (Γ ⊢B b ▹ Γ₁)
136 check-B = {!!}