- commit
- 912e12b
- parent
- 9fbadb5
- author
- Eugene Akentyev
- date
- 2016-12-16 00:50:22 +0400 +04
in work
2 files changed,
+18,
-7
+1,
-0
1@@ -181,3 +181,4 @@ Ctx : ℕ → Set
2 Ctx = Vec TypeDecl
3
4 module CtxEq = VecEq.DecidableEquality TypeDeclEq.decSetoid
5+module CtxPropEq = VecEq.PropositionalEquality
+17,
-7
1@@ -7,6 +7,7 @@ open import Relation.Nullary
2 open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; subst; refl)
3 open import Data.Nat using (ℕ; _+_; suc; _≟_)
4 open import Data.Vec using (Vec; _∈_; zip; _∷_; here)
5+open import Function
6 open import Expr
7 open import Type
8 open import Behaviour
9@@ -24,9 +25,9 @@ data _⊢ₑ_∶_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where
10 → Γ ⊢ₑ s ∶ b
11
12 data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
13- t-nil : (n≡m : n ≡ m)
14+ t-nil : {Γ₁ : Ctx m} {Γ≡Γ₁ : Γ CtxPropEq.≈ Γ₁}
15 ---------------------------
16- → Γ ⊢B nil ▹ subst Ctx n≡m Γ
17+ → Γ ⊢B nil ▹ Γ₁
18
19 t-if : {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Expr}
20 → Γ ⊢ₑ e ∶ bool -- Γ ⊢ e : bool
21@@ -35,11 +36,11 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
22 ---------------------------
23 → Γ ⊢B if e b1 b2 ▹ Γ₁
24
25- t-while : {n≡m : n ≡ m} {b : Behaviour} {e : Variable}
26- → Γ ⊢ e ∶ bool
27- → Γ ⊢B b ▹ Γ
28+ t-while : {Γ₁ : Ctx m} {Γ≡Γ₁ : Γ CtxPropEq.≈ Γ₁} {b : Behaviour} {e : Expr}
29+ → Γ ⊢ₑ e ∶ bool
30+ → Γ ⊢B b ▹ Γ₁
31 --------------------------
32- → Γ ⊢B while (var e) b ▹ subst Ctx n≡m Γ
33+ → Γ ⊢B while e b ▹ Γ₁
34
35 t-choice : {Γ₁ : Ctx m} {k n : ℕ} {η : Input_ex} {inputs : Vec Input_ex n}
36 {b : Behaviour} {behaviours : Vec Behaviour n}
37@@ -134,10 +135,19 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
38 ------------------------------------
39 → Γ ⊢B (input (reqres o x a b)) ▹ Γ₁
40
41-check-B : {n m : ℕ} {Γ₁ : Ctx m} → (Γ : Ctx n) → (b : Behaviour) → Dec (Γ ⊢B b ▹ Γ₁)
42+check-B : {n m : ℕ} {Γ₁ : Ctx m} → (Γ : Ctx n) → (b : Behaviour) → Dec (_⊢B_▹_ {n} {m} Γ b Γ₁)
43+check-B {n} {m} {Γ₁} Γ nil with Γ CtxEq.≟ Γ₁
44+... | yes Γ≡Γ₁ = yes (t-nil {n} {m} {Γ} {Γ₁} {Γ≡Γ₁})
45+... | no ¬p = no (λ {(t-nil {Γ₁} {Γ≡Γ₁}) → ¬p Γ≡Γ₁})
46 check-B {n} {m} {Γ₁} Γ (if e b1 b2) with check-B Γ b1 | check-B Γ b2
47 ... | yes ctx₁ | yes ctx₂ = yes (t-if expr-t ctx₁ ctx₂)
48 ... | yes _ | no ¬p = no (λ {(t-if _ _ c₂) → ¬p c₂})
49 ... | no ¬p | yes _ = no (λ {(t-if _ c₁ _) → ¬p c₁})
50 ... | no _ | no ¬p = no (λ {(t-if _ _ c₂) → ¬p c₂})
51+check-B {n} {m} {Γ₁} Γ (while e b) with Γ CtxEq.≟ Γ₁
52+... | yes Γ≡Γ₁ = case (check-B {n} {m} {Γ₁} Γ b) of λ
53+ { (yes ctx) → yes (t-while {n} {m} {Γ} {Γ₁} {Γ≡Γ₁} expr-t ctx)
54+ ; (no ¬p) → no (λ {(t-while _ ctx) → ¬p ctx})
55+ }
56+... | no ¬p = no {!!}
57 check-B Γ b = {!!}