repos / jolie.agda.git

commit

aace256

parent

0fd4be2

author

Eugene Akentyev

date

2016-12-08 16:34:57 +0400 +04

Add 'if case' to check-B

 1@@ -4,9 +4,9 @@ import Data.List as List
 2 import Data.Vec.Equality as VecEq
 3 open import Relation.Nullary using (¬_)
 4 open import Relation.Nullary
 5-open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; subst)
 6-open import Data.Nat using (ℕ; _+_; suc)
 7-open import Data.Vec using (Vec; _∈_; zip; _∷_)
 8+open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; subst; refl)
 9+open import Data.Nat using (ℕ; _+_; suc; _≟_)
10+open import Data.Vec using (Vec; _∈_; zip; _∷_; here)
11 open import Expr
12 open import Type
13 open import Behaviour
14@@ -19,21 +19,21 @@ data _⊢_∶_ {n : ℕ} (Γ : Ctx n) : Variable → Type → Set where
15         ------------
16         → Γ ⊢ s ∶ b
17 
18-data _⊢ₑ_of_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where
19+data _⊢ₑ_∶_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where
20   expr-t : {s : Expr} {b : Type}
21-         → Γ ⊢ₑ s of b
22+         → Γ ⊢ₑ s ∶ b
23 
24-data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour →  Ctx m → Set where
25-  t-nil : {n≡m : n ≡ m}
26+data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
27+  t-nil : (n≡m : n ≡ m)
28         ---------------------------
29         → Γ ⊢B nil ▹ subst Ctx n≡m Γ
30           
31-  t-if : {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Variable}
32-       → Γ ⊢ e ∶ bool -- Γ ⊢ e : bool
33+  t-if : {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Expr}
34+       → Γ ⊢ₑ e ∶ bool -- Γ ⊢ e : bool
35        → Γ ⊢B b1 ▹ Γ₁
36        → Γ ⊢B b2 ▹ Γ₁
37        ---------------------------
38-       → Γ ⊢B if (var e) b1 b2 ▹ Γ₁
39+       → Γ ⊢B if e b1 b2 ▹ Γ₁
40           
41   t-while : {n≡m : n ≡ m} {b : Behaviour} {e : Variable}
42           → Γ ⊢ e ∶ bool
43@@ -71,14 +71,14 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour →  Ctx m → Set where
44                  → Γ ⊢B output (notification o l (var e)) ▹ subst Ctx n≡m Γ
45 
46   t-assign-new : {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
47-               → Γ ⊢ₑ e of Tₑ -- Γ ⊢ e : bool
48+               → Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
49                → ¬ (var x Tₓ ∈ Γ) -- x ∉ Γ
50                → (var x Tₑ) ∈ Γ₁
51                ---------------------
52                → Γ ⊢B assign x e ▹ Γ₁
53 
54   t-assign-exists : {n≡m : n ≡ m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
55-                  → Γ ⊢ₑ e of Tₑ
56+                  → Γ ⊢ₑ e ∶ Tₑ
57                   → (var x Tₓ) ∈ Γ
58                   → Tₑ ≡ Tₓ
59                   ---------------------
60@@ -135,4 +135,18 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour →  Ctx m → Set where
61                    → Γ ⊢B (input (reqres o x a b)) ▹ Γ₁
62 
63 check-B : {n m : ℕ} {Γ₁ : Ctx m} → (Γ : Ctx n) → (b : Behaviour) → Dec (Γ ⊢B b ▹ Γ₁)
64-check-B = {!!}
65+check-B {n} {m} {Γ₁} Γ (if e b1 b2) with check-B Γ b1 | check-B Γ b2
66+... | yes ctx₁ | yes ctx₂ = yes (t-if expr-t ctx₁ ctx₂)
67+... | yes _ | no ¬p = no lem
68+  where
69+    lem : ¬ Γ ⊢B if e b1 b2 ▹ Γ₁
70+    lem (t-if _ _ c₂) = ¬p c₂
71+... | no ¬p | yes _ = no lem
72+  where
73+    lem : ¬ Γ ⊢B if e b1 b2 ▹ Γ₁
74+    lem (t-if _ c₁ _) = ¬p c₁
75+... | no _ | no ¬2 = no lem
76+  where
77+    lem : ¬ Γ ⊢B if e b1 b2 ▹ Γ₁
78+    lem (t-if _ _ c₂) = ¬2 c₂
79+check-B Γ b = {!!}