- commit
- d26f7fc
- parent
- cc67ec1
- author
- Eugene Akentyev
- date
- 2016-12-19 23:50:32 +0400 +04
...
1 files changed,
+25,
-25
+25,
-25
1@@ -26,30 +26,30 @@ data _⊢ₑ_∶_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where
2 expr-t : {s : Expr} {b : Type}
3 → Γ ⊢ₑ s ∶ b
4
5-data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
6- t-nil : {Γ₁ : Ctx m} {Γ≡Γ₁ : Γ CtxPropEq.≈ Γ₁}
7+data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
8+ t-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Γ≡Γ₁ : Γ CtxPropEq.≈ Γ₁}
9 ---------------------------
10 → Γ ⊢B nil ▹ Γ₁
11
12- t-if : {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Expr}
13+ t-if : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Expr}
14 → Γ ⊢ₑ e ∶ bool -- Γ ⊢ e : bool
15 → Γ ⊢B b1 ▹ Γ₁
16 → Γ ⊢B b2 ▹ Γ₁
17 ---------------------------
18 → Γ ⊢B if e b1 b2 ▹ Γ₁
19
20- t-while : {Γ₁ : Ctx m} {Γ≡Γ₁ : Γ CtxPropEq.≈ Γ₁} {b : Behaviour} {e : Expr}
21+ t-while : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Γ≡Γ₁ : Γ CtxPropEq.≈ Γ₁} {b : Behaviour} {e : Expr}
22 → Γ ⊢ₑ e ∶ bool
23 → Γ ⊢B b ▹ Γ₁
24 --------------------------
25 → Γ ⊢B while e b ▹ Γ₁
26
27- t-choice : {Γ₁ : Ctx m} {choices : List (Input_ex × Behaviour)}
28+ t-choice : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {choices : List (Input_ex × Behaviour)}
29 → All (λ { (η , b) → Γ ⊢B seq (input η) b ▹ Γ₁ }) choices
30 -----------------------------------------------
31 → Γ ⊢B inputchoice choices ▹ Γ₁
32
33- t-par : {k k₁ p p₁ : ℕ} {b1 b2 : Behaviour}
34+ t-par : ∀ {n m} {Γ : Ctx n} {k k₁ p p₁ : ℕ} {b1 b2 : Behaviour}
35 {Γ₁ : Ctx k} {Γ₁' : Ctx k₁} {Γ₂ : Ctx p} {Γ₂' : Ctx p₁} {Γ' : Ctx m}
36 → Γ₁ ⊢B b1 ▹ Γ₁'
37 → Γ₂ ⊢B b2 ▹ Γ₂'
38@@ -57,48 +57,48 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
39 --------------------
40 → Γ ⊢B par b1 b2 ▹ Γ'
41
42- t-seq : {k : ℕ} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour}
43+ t-seq : ∀ {n m} {Γ : Ctx n} {k : ℕ} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour}
44 → Γ ⊢B b1 ▹ Γ₁
45 → Γ₁ ⊢B b2 ▹ Γ₂
46 --------------------
47 → Γ ⊢B seq b1 b2 ▹ Γ₂
48
49- t-notification : {n≡m : n ≡ m} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
50+ t-notification : ∀ {n m} {Γ : Ctx n} {n≡m : n ≡ m} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
51 → (outNotify o l T₀) ∈ Γ
52 → Γ ⊢ e ∶ Tₑ
53 → Tₑ ⊆ T₀
54 -------------------------------------------
55 → Γ ⊢B output (notification o l (var e)) ▹ subst Ctx n≡m Γ
56
57- t-assign-new : {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
58+ t-assign-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
59 → Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
60 → ¬ (var x Tₓ ∈ Γ) -- x ∉ Γ
61 → (var x Tₑ) ∈ Γ₁
62 ---------------------
63 → Γ ⊢B assign x e ▹ Γ₁
64
65- t-assign-exists : {n≡m : n ≡ m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
66+ t-assign-exists : ∀ {n m} {Γ : Ctx n} {n≡m : n ≡ m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
67 → Γ ⊢ₑ e ∶ Tₑ
68 → (var x Tₓ) ∈ Γ
69 → Tₑ ≡ Tₓ
70 ---------------------
71 → Γ ⊢B assign x e ▹ subst Ctx n≡m Γ
72
73- t-oneway-new : {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
74+ t-oneway-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
75 → (inOneWay o Tᵢ) ∈ Γ
76 → ¬ ((var x Tₓ) ∈ Γ)
77 → (var x Tᵢ) ∈ Γ₁
78 -------------------------------
79 → Γ ⊢B (input (oneway o x)) ▹ Γ₁
80
81- t-oneway-exists : {n≡m : n ≡ m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
82+ t-oneway-exists : ∀ {n m} {Γ : Ctx n} {n≡m : n ≡ m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
83 → (inOneWay o Tᵢ) ∈ Γ
84 → ((var x Tₓ) ∈ Γ)
85 → Tᵢ ⊆ Tₓ
86 --------------------------------
87 → Γ ⊢B (input (oneway o x)) ▹ subst Ctx n≡m Γ
88
89- t-solresp-new : {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
90+ t-solresp-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
91 → (outSolRes o l Tₒ Tᵢ) ∈ Γ
92 → Tₑ ⊆ Tₒ
93 → ¬ (var x Tₓ ∈ Γ)
94@@ -106,7 +106,7 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
95 -----------------------------------------
96 → Γ ⊢B (output (solicitres o l e x)) ▹ Γ₁
97
98- t-solresp-exists : {n≡m : n ≡ m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
99+ t-solresp-exists : ∀ {n m} {Γ : Ctx n} {n≡m : n ≡ m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
100 → (outSolRes o l Tₒ Tᵢ) ∈ Γ
101 → Tₑ ⊆ Tₒ
102 → (var x Tₓ) ∈ Γ
103@@ -114,7 +114,7 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
104 -----------------------------------------
105 → Γ ⊢B (output (solicitres o l e x)) ▹ subst Ctx n≡m Γ
106
107- t-reqresp-new : {p : ℕ} {Γₓ : Ctx p} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
108+ t-reqresp-new : ∀ {n m} {Γ : Ctx n} {p : ℕ} {Γₓ : Ctx p} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
109 → (inReqRes o Tᵢ Tₒ) ∈ Γ
110 → ¬ (var x Tₓ ∈ Γ)
111 → (var x Tₓ) ∈ Γₓ
112@@ -124,7 +124,7 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
113 -----------------------------------
114 → Γ ⊢B (input (reqres o x a b)) ▹ Γ₁
115
116- t-reqresp-exists : {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable}
117+ t-reqresp-exists : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable}
118 → (inReqRes o Tᵢ Tₒ) ∈ Γ
119 → (var x Tₓ) ∈ Γ
120 → Tᵢ ⊆ Tₓ
121@@ -136,22 +136,22 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
122
123
124 {-# NON_TERMINATING #-}
125-check-B : {n m : ℕ} {Γ₁ : Ctx m} → (Γ : Ctx n) → (b : Behaviour) → Dec (_⊢B_▹_ {n} {m} Γ b Γ₁)
126-check-B {n} {m} {Γ₁} Γ nil with Γ CtxEq.≟ Γ₁
127+check-B : ∀ {n m} → (Γ : Ctx n) → (b : Behaviour) → (Γ₁ : Ctx m) → Dec (Γ ⊢B b ▹ Γ₁)
128+check-B {n} {m} Γ nil Γ₁ with Γ CtxEq.≟ Γ₁
129 ... | yes Γ≡Γ₁ = yes (t-nil {n} {m} {Γ} {Γ₁} {Γ≡Γ₁})
130-... | no ¬p = no (λ {(t-nil {_} {Γ≡Γ₁}) → ¬p Γ≡Γ₁})
131-check-B {n} {m} {Γ₁} Γ (if e b1 b2) with check-B Γ b1 | check-B Γ b2
132+... | no ¬p = no (λ {(t-nil {_} {_} {_} {_} {Γ≡Γ₁}) → ¬p Γ≡Γ₁})
133+check-B {n} {m} Γ (if e b1 b2) Γ₁ with check-B Γ b1 Γ₁ | check-B Γ b2 Γ₁
134 ... | yes ctx₁ | yes ctx₂ = yes (t-if expr-t ctx₁ ctx₂)
135 ... | yes _ | no ¬p = no (λ {(t-if _ _ c₂) → ¬p c₂})
136 ... | no ¬p | yes _ = no (λ {(t-if _ c₁ _) → ¬p c₁})
137 ... | no _ | no ¬p = no (λ {(t-if _ _ c₂) → ¬p c₂})
138-check-B {n} {m} {Γ₁} Γ (while e b) with Γ CtxEq.≟ Γ₁
139-... | yes Γ≡Γ₁ = case (check-B {n} {m} {Γ₁} Γ b) of λ
140+check-B {n} {m} Γ (while e b) Γ₁ with Γ CtxEq.≟ Γ₁
141+... | yes Γ≡Γ₁ = case (check-B {n} {m} Γ b Γ₁) of λ
142 { (yes ctx) → yes (t-while {n} {m} {Γ} {Γ₁} {Γ≡Γ₁} expr-t ctx)
143 ; (no ¬p) → no (λ {(t-while _ ctx) → ¬p ctx})
144 }
145-... | no ¬p = no (λ {(t-while {_} {Γ≡Γ₁} _ _) → ¬p Γ≡Γ₁})
146-check-B {n} {m} {Γ₁} Γ (inputchoice pairs) with all (λ { (η , b) → check-B {n} {m} {Γ₁} Γ (seq (input η) b) }) pairs
147+... | no ¬p = no (λ {(t-while {_} {_} {_} {_} {Γ≡Γ₁} _ _) → ¬p Γ≡Γ₁})
148+check-B {n} {m} Γ (inputchoice pairs) Γ₁ with all (λ { (η , b) → check-B {n} {m} Γ (seq (input η) b) Γ₁ }) pairs
149 ... | yes checked = yes (t-choice checked)
150 ... | no ¬p = no (λ { (t-choice checked) → ¬p checked })
151-check-B Γ b = {!!}
152+check-B Γ b Γ₁ = {!!}