...

diff --git a/src/Typecheck.agda b/src/Typecheck.agda
index 68c8a393a70112f010726697bd10b5d276f34f72..eb5122b142d94c40632c6ce4a80c541ec7012fb4 100644 (file)
--- a/src/Typecheck.agda
+++ b/src/Typecheck.agda
@@ -26,30 +26,30 @@ data _⊢ₑ_∶_ {n : ℕ} (Γ : Ctx n) : Expr → Type → Set where
   expr-t : {s : Expr} {b : Type}
          → Γ ⊢ₑ s ∶ b
 
-data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
-  t-nil : {Γ₁ : Ctx m} {Γ≡Γ₁ : Γ CtxPropEq.≈ Γ₁}
+data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
+  t-nil : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Γ≡Γ₁ : Γ CtxPropEq.≈ Γ₁}
         ---------------------------
         → Γ ⊢B nil ▹ Γ₁
           
-  t-if : {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Expr}
+  t-if : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {b1 b2 : Behaviour} {e : Expr}
        → Γ ⊢ₑ e ∶ bool -- Γ ⊢ e : bool
        → Γ ⊢B b1 ▹ Γ₁
        → Γ ⊢B b2 ▹ Γ₁
        ---------------------------
        → Γ ⊢B if e b1 b2 ▹ Γ₁
           
-  t-while : {Γ₁ : Ctx m} {Γ≡Γ₁ : Γ CtxPropEq.≈ Γ₁} {b : Behaviour} {e : Expr} 
+  t-while : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Γ≡Γ₁ : Γ CtxPropEq.≈ Γ₁} {b : Behaviour} {e : Expr} 
           → Γ ⊢ₑ e ∶ bool
           → Γ ⊢B b ▹ Γ₁
           --------------------------
           → Γ ⊢B while e b ▹ Γ₁
           
-  t-choice : {Γ₁ : Ctx m} {choices : List (Input_ex × Behaviour)}
+  t-choice : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {choices : List (Input_ex × Behaviour)}
            → All (λ { (η , b) → Γ ⊢B seq (input η) b ▹ Γ₁ }) choices
            -----------------------------------------------
            → Γ ⊢B inputchoice choices ▹ Γ₁
 
-  t-par : {k k₁ p p₁ : ℕ} {b1 b2 : Behaviour}
+  t-par : ∀ {n m} {Γ : Ctx n} {k k₁ p p₁ : ℕ} {b1 b2 : Behaviour}
           {Γ₁ : Ctx k} {Γ₁' : Ctx k₁} {Γ₂ : Ctx p} {Γ₂' : Ctx p₁} {Γ' : Ctx m}
         → Γ₁ ⊢B b1 ▹ Γ₁'
         → Γ₂ ⊢B b2 ▹ Γ₂'
@@ -57,48 +57,48 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
         --------------------
         → Γ ⊢B par b1 b2 ▹ Γ'
 
-  t-seq : {k : ℕ} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour}
+  t-seq : ∀ {n m} {Γ : Ctx n} {k : ℕ} {Γ₁ : Ctx k} {Γ₂ : Ctx m} {b1 b2 : Behaviour}
         → Γ ⊢B b1 ▹ Γ₁
         → Γ₁ ⊢B b2 ▹ Γ₂
         --------------------
         → Γ ⊢B seq b1 b2 ▹ Γ₂
 
-  t-notification : {n≡m : n ≡ m} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
+  t-notification : ∀ {n m} {Γ : Ctx n} {n≡m : n ≡ m} {o : Operation} {l : Location} {e : Variable} {T₀ Tₑ : Type}
                  → (outNotify o l T₀) ∈ Γ
                  → Γ ⊢ e ∶ Tₑ
                  → Tₑ ⊆ T₀
                  -------------------------------------------
                  → Γ ⊢B output (notification o l (var e)) ▹ subst Ctx n≡m Γ
 
-  t-assign-new : {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
+  t-assign-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
                → Γ ⊢ₑ e ∶ Tₑ -- Γ ⊢ e : bool
                → ¬ (var x Tₓ ∈ Γ) -- x ∉ Γ
                → (var x Tₑ) ∈ Γ₁
                ---------------------
                → Γ ⊢B assign x e ▹ Γ₁
 
-  t-assign-exists : {n≡m : n ≡ m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
+  t-assign-exists : ∀ {n m} {Γ : Ctx n} {n≡m : n ≡ m} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
                   → Γ ⊢ₑ e ∶ Tₑ
                   → (var x Tₓ) ∈ Γ
                   → Tₑ ≡ Tₓ
                   ---------------------
                   → Γ ⊢B assign x e ▹ subst Ctx n≡m Γ
 
-  t-oneway-new : {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
+  t-oneway-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
                → (inOneWay o Tᵢ) ∈ Γ
                → ¬ ((var x Tₓ) ∈ Γ)
                → (var x Tᵢ) ∈ Γ₁
                -------------------------------
                → Γ ⊢B (input (oneway o x)) ▹ Γ₁
 
-  t-oneway-exists : {n≡m : n ≡ m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
+  t-oneway-exists : ∀ {n m} {Γ : Ctx n} {n≡m : n ≡ m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
                   → (inOneWay o Tᵢ) ∈ Γ
                   → ((var x Tₓ) ∈ Γ)
                   → Tᵢ ⊆ Tₓ
                   --------------------------------
                   → Γ ⊢B (input (oneway o x)) ▹ subst Ctx n≡m Γ
 
-  t-solresp-new : {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
+  t-solresp-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
                 → (outSolRes o l Tₒ Tᵢ) ∈ Γ
                 → Tₑ ⊆ Tₒ
                 → ¬ (var x Tₓ ∈ Γ)
@@ -106,7 +106,7 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
                 -----------------------------------------
                 → Γ ⊢B (output (solicitres o l e x)) ▹ Γ₁
 
-  t-solresp-exists : {n≡m : n ≡ m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
+  t-solresp-exists : ∀ {n m} {Γ : Ctx n} {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ₓ) ∈ Γ
@@ -114,7 +114,7 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
                    -----------------------------------------
                    → Γ ⊢B (output (solicitres o l e x)) ▹ subst Ctx n≡m Γ
 
-  t-reqresp-new : {p : ℕ} {Γₓ : Ctx p} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
+  t-reqresp-new : ∀ {n m} {Γ : Ctx n} {p : ℕ} {Γₓ : Ctx p} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
                 → (inReqRes o Tᵢ Tₒ) ∈ Γ
                 → ¬ (var x Tₓ ∈ Γ)
                 → (var x Tₓ) ∈ Γₓ
@@ -124,7 +124,7 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
                 -----------------------------------
                 → Γ ⊢B (input (reqres o x a b)) ▹ Γ₁
 
-  t-reqresp-exists : {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable}
+  t-reqresp-exists : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable}
                    → (inReqRes o Tᵢ Tₒ) ∈ Γ
                    → (var x Tₓ) ∈ Γ
                    → Tᵢ ⊆ Tₓ
@@ -136,22 +136,22 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
 
 
 {-# NON_TERMINATING #-}
-check-B : {n m : ℕ} {Γ₁ : Ctx m} → (Γ : Ctx n) → (b : Behaviour) → Dec (_⊢B_▹_ {n} {m} Γ b Γ₁)
-check-B {n} {m} {Γ₁} Γ nil with Γ CtxEq.≟ Γ₁
+check-B : ∀ {n m} → (Γ : Ctx n) → (b : Behaviour) → (Γ₁ : Ctx m) → Dec (Γ ⊢B 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
+... | 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 λ
+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 (λ {(t-while {_} {Γ≡Γ₁} _ _) → ¬p Γ≡Γ₁})
-check-B {n} {m} {Γ₁} Γ (inputchoice pairs) with all (λ { (η , b) → check-B {n} {m} {Γ₁} Γ (seq (input η) b) }) pairs
+... | no ¬p = no (λ {(t-while {_} {_} {_} {_} {Γ≡Γ₁} _ _) → ¬p Γ≡Γ₁})
+check-B {n} {m} Γ (inputchoice pairs) Γ₁ with all (λ { (η , b) → check-B {n} {m} Γ (seq (input η) b) Γ₁ }) pairs
 ... | yes checked = yes (t-choice checked)
 ... | no ¬p = no (λ { (t-choice checked) → ¬p checked })
-check-B Γ b = {!!}
+check-B Γ b Γ₁ = {!!}