in work

diff --git a/src/Type.agda b/src/Type.agda
index 75be9df3513bfce7ffb7cab9495f4415b5cac9bb..421eba6d1762e57a8700b56d3ac0b223bfbd0cf8 100644 (file)
--- a/src/Type.agda
+++ b/src/Type.agda
@@ -181,3 +181,4 @@ Ctx : ℕ → Set
 Ctx = Vec TypeDecl
 
 module CtxEq = VecEq.DecidableEquality TypeDeclEq.decSetoid
+module CtxPropEq = VecEq.PropositionalEquality

diff --git a/src/Typecheck.agda b/src/Typecheck.agda
index c556b537862fa4b6091a2d12db45496a6b8badf8..1dfca7728abaee70fc14f574631a6a9e8f226365 100644 (file)
--- a/src/Typecheck.agda
+++ b/src/Typecheck.agda
@@ -7,6 +7,7 @@ open import Relation.Nullary
 open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; subst; refl)
 open import Data.Nat using (ℕ; _+_; suc; _≟_)
 open import Data.Vec using (Vec; _∈_; zip; _∷_; here)
+open import Function
 open import Expr
 open import Type
 open import Behaviour
@@ -24,9 +25,9 @@ data _⊢ₑ_∶_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where
          → Γ ⊢ₑ s ∶ b
 
 data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
-  t-nil : (n≡m : n ≡ m)
+  t-nil : {Γ₁ : Ctx m} {Γ≡Γ₁ : Γ CtxPropEq.≈ Γ₁}
         ---------------------------
-        → Γ ⊢B nil ▹ subst Ctx n≡m Γ
+        → Γ ⊢B nil ▹ Γ₁
           
   t-if : {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Expr}
        → Γ ⊢ₑ e ∶ bool -- Γ ⊢ e : bool
@@ -35,11 +36,11 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
        ---------------------------
        → Γ ⊢B if e b1 b2 ▹ Γ₁
           
-  t-while : {n≡m : n ≡ m} {b : Behaviour} {e : Variable}
-          → Γ ⊢ e ∶ bool
-          → Γ ⊢B b ▹ Γ
+  t-while : {Γ₁ : Ctx m} {Γ≡Γ₁ : Γ CtxPropEq.≈ Γ₁} {b : Behaviour} {e : Expr} 
+          → Γ ⊢ₑ e ∶ bool
+          → Γ ⊢B b ▹ Γ₁
           --------------------------
-          → Γ ⊢B while (var e) b ▹ subst Ctx n≡m Γ
+          → Γ ⊢B while e b ▹ Γ₁
           
   t-choice : {Γ₁ : Ctx m} {k n : ℕ}  {η : Input_ex} {inputs : Vec Input_ex n}
              {b : Behaviour} {behaviours : Vec Behaviour n}
@@ -134,10 +135,19 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
                    ------------------------------------
                    → Γ ⊢B (input (reqres o x a b)) ▹ Γ₁
 
-check-B : {n m : ℕ} {Γ₁ : Ctx m} → (Γ : Ctx n) → (b : Behaviour) → Dec (Γ ⊢B b ▹ Γ₁)
+check-B : {n m : ℕ} {Γ₁ : Ctx m} → (Γ : Ctx n) → (b : Behaviour) → Dec (_⊢B_▹_ {n} {m} Γ b Γ₁)
+check-B {n} {m} {Γ₁} Γ nil with Γ CtxEq.≟ Γ₁
+... | yes Γ≡Γ₁ = yes (t-nil {n} {m} {Γ} {Γ₁} {Γ≡Γ₁})
+... | no ¬p = no (λ {(t-nil {Γ₁} {Γ≡Γ₁}) → ¬p Γ≡Γ₁})
 check-B {n} {m} {Γ₁} Γ (if e b1 b2) with check-B Γ b1 | check-B Γ b2
 ... | yes ctx₁ | yes ctx₂ = yes (t-if expr-t ctx₁ ctx₂)
 ... | yes _ | no ¬p = no (λ {(t-if _ _ c₂) → ¬p c₂})
 ... | no ¬p | yes _ = no (λ {(t-if _ c₁ _) → ¬p c₁})
 ... | no _ | no ¬p = no (λ {(t-if _ _ c₂) → ¬p c₂})
+check-B {n} {m} {Γ₁} Γ (while e b) with Γ CtxEq.≟ Γ₁
+... | yes Γ≡Γ₁ = case (check-B {n} {m} {Γ₁} Γ b) of λ
+  { (yes ctx) → yes (t-while {n} {m} {Γ} {Γ₁} {Γ≡Γ₁} expr-t ctx)
+  ; (no ¬p) → no (λ {(t-while _ ctx) → ¬p ctx})
+  }
+... | no ¬p = no {!!}
 check-B Γ b = {!!}