Fix equality of contexts

diff --git a/src/Typecheck.agda b/src/Typecheck.agda
index 97d9173f32595a79043eda36e9faf3be5ebf090b..f65c31842f4405b5b38d17429f487cc4e3f85eac 100644 (file)
--- a/src/Typecheck.agda
+++ b/src/Typecheck.agda
@@ -1,11 +1,10 @@
-
 module Typecheck where
 
 import Data.List as List
 import Data.Vec.Equality as VecEq
 open import Relation.Nullary using (¬_)
 open import Relation.Nullary
-open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
+open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; subst)
 open import Data.Nat using (ℕ; _+_; suc)
 open import Data.Vec using (Vec; _∈_; zip; _∷_)
 open import Expr
@@ -14,32 +13,36 @@ open import Behaviour
 open import Variable
 
 
-data _⊢_of_ {n : ℕ} (Γ : Ctx n) : Variable → Type → Set where
+substCtx : {n m : ℕ} → n ≡ m → Ctx n → Ctx m
+substCtx n≡m Γ = subst (λ x → Vec TypeDecl x) n≡m Γ
+
+data _⊢_∶_ {n : ℕ} (Γ : Ctx n) : Variable → Type → Set where
   var-t : {s : Variable} {b : Type}
-        → Γ ⊢ s of b
+        → (var s b) ∈ Γ
+        ------------
+        → Γ ⊢ s ∶ b
 
 data _⊢ₑ_of_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where
   expr-t : {s : Expr} {b : Type}
          → Γ ⊢ₑ s of b
 
-data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set where 
-  t-nil : {Γ₁ : Ctx m}
-        → n ≡ m
-        --------------
-        → Γ ⊢B nil ▹ Γ₁
+data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour →  Ctx m → Set where
+  t-nil : {n≡m : n ≡ m}
+        ---------------------------
+        → Γ ⊢B nil ▹ substCtx n≡m Γ
           
   t-if : {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Variable}
-       → Γ ⊢ e of bool -- Γ ⊢ e : bool
+       → Γ ⊢ e ∶ bool -- Γ ⊢ e : bool
        → Γ ⊢B b1 ▹ Γ₁
        → Γ ⊢B b2 ▹ Γ₁
        ---------------------------
        → Γ ⊢B if (var e) b1 b2 ▹ Γ₁
           
-  t-while : {Γ₁ : Ctx m} {b : Behaviour} {e : Variable}
-          → Γ ⊢ e of bool
-          → Γ ⊢B b ▹ Γ₁
+  t-while : {n≡m : n ≡ m} {b : Behaviour} {e : Variable}
+          → Γ ⊢ e ∶ bool
+          → Γ ⊢B b ▹ Γ
           --------------------------
-          → Γ ⊢B while (var e) b ▹ Γ₁
+          → Γ ⊢B while (var e) b ▹ substCtx n≡m Γ
           
   t-choice : {Γ₁ : Ctx m} {k n : ℕ}  {η : Input_ex} {inputs : Vec Input_ex n}
              {b : Behaviour} {behaviours : Vec Behaviour n}
@@ -63,13 +66,12 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set
         --------------------
         → Γ ⊢B seq b1 b2 ▹ Γ₂
 
-  t-notification : {k : ℕ} {Γ₁ : Ctx m} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
+  t-notification : {n≡m : n ≡ m} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
                  → (outNotify o l T₀) ∈ Γ
-                 → Γ ⊢ e of Tₑ
+                 → Γ ⊢ e ∶ Tₑ
                  → Tₑ ⊆ T₀
-                 → n ≡ m
                  -------------------------------------------
-                 → Γ ⊢B output (notification o l (var e)) ▹ Γ₁
+                 → Γ ⊢B output (notification o l (var e)) ▹ substCtx n≡m Γ
 
   t-assign-new : {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
                → Γ ⊢ₑ e of Tₑ -- Γ ⊢ e : bool
@@ -78,13 +80,12 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set
                ---------------------
                → Γ ⊢B assign x e ▹ Γ₁
 
-  t-assign-exists : {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
+  t-assign-exists : {n≡m : n ≡ m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
                   → Γ ⊢ₑ e of Tₑ
                   → (var x Tₓ) ∈ Γ
                   → Tₑ ≡ Tₓ
-                  → n ≡ m -- TODO Γ ≡ Γ₁
                   ---------------------
-                  → Γ ⊢B assign x e ▹ Γ₁
+                  → Γ ⊢B assign x e ▹ substCtx n≡m Γ
 
   t-oneway-new : {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
                → (inOneWay o Tᵢ) ∈ Γ
@@ -93,13 +94,12 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set
                -------------------------------
                → Γ ⊢B (input (oneway o x)) ▹ Γ₁
 
-  t-oneway-exists : {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
+  t-oneway-exists : {n≡m : n ≡ m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
                   → (inOneWay o Tᵢ) ∈ Γ
                   → ((var x Tₓ) ∈ Γ)
                   → Tᵢ ⊆ Tₓ
-                  → n ≡ m -- TODO Γ ≡ Γ₁
                   --------------------------------
-                  → Γ ⊢B (input (oneway o x)) ▹ Γ₁
+                  → Γ ⊢B (input (oneway o x)) ▹ substCtx n≡m Γ
 
   t-solresp-new : {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
                 → (outSolRes o l Tₒ Tᵢ) ∈ Γ
@@ -109,14 +109,13 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set
                 -----------------------------------------
                 → Γ ⊢B (output (solicitres o l e x)) ▹ Γ₁
 
-  t-solresp-exists : {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
+  t-solresp-exists : {n≡m : n ≡ m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
                    → (outSolRes o l Tₒ Tᵢ) ∈ Γ
                    → Tₑ ⊆ Tₒ
                    → (var x Tₓ) ∈ Γ
                    → Tᵢ ⊆ Tₓ
-                   → n ≡ m -- TODO Γ ≡ Γ₁
                    -----------------------------------------
-                   → Γ ⊢B (output (solicitres o l e x)) ▹ Γ₁
+                   → Γ ⊢B (output (solicitres o l e x)) ▹ substCtx n≡m Γ
 
   t-reqresp-new : {p : ℕ} {Γₓ : Ctx p} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
                 → (inReqRes o Tᵢ Tₒ) ∈ Γ
@@ -138,6 +137,5 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → (Γ₁ : Ctx m) → Set
                    ------------------------------------
                    → Γ ⊢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 b ▹ Γ₁)
 check-B = {!!}