Change direction to theorems. Add t-wait and t-exec.

diff --git a/src/Typecheck.agda b/src/Typecheck.agda
index eb5122b142d94c40632c6ce4a80c541ec7012fb4..be6629817eebe23e4b68d4ec737d6384f0f04246 100644 (file)
--- a/src/Typecheck.agda
+++ b/src/Typecheck.agda
@@ -1,13 +1,11 @@
 module Typecheck where
 
-open import Data.List.All using (All; all) renaming ([] to []-All; _∷_ to _∷-All_)
-import Data.Vec.Equality as VecEq
+open import Data.List.All using (All)
 open import Relation.Nullary using (¬_)
-open import Relation.Nullary
 open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; subst; refl)
 open import Data.Nat using (ℕ; _+_; suc; _≟_)
-open import Data.List using (List; []; _∷_; foldl)
-open import Data.Vec using (Vec; _∈_; zip; _∷_; here; fromList; toList) renaming ([] to []-Vec)
+open import Data.List using (List)
+open import Data.Vec using (_∈_)
 open import Data.Product using (_,_; _×_)
 open import Function
 open import Expr
@@ -89,14 +87,14 @@ data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
                → ¬ ((var x Tₓ) ∈ Γ)
                → (var x Tᵢ) ∈ Γ₁
                -------------------------------
-               → Γ ⊢B (input (oneway o x)) ▹ Γ₁
+               → Γ ⊢B input (oneway o x) ▹ Γ₁
 
   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 Γ
+                  → Γ ⊢B input (oneway o x) ▹ subst Ctx n≡m Γ
 
   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ᵢ) ∈ Γ
@@ -104,7 +102,7 @@ data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
                 → ¬ (var x Tₓ ∈ Γ)
                 → (var x Tᵢ) ∈ Γ₁
                 -----------------------------------------
-                → Γ ⊢B (output (solicitres o l e x)) ▹ Γ₁
+                → Γ ⊢B output (solicitres o l e x) ▹ Γ₁
 
   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ᵢ) ∈ Γ
@@ -112,7 +110,7 @@ data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
                    → (var x Tₓ) ∈ Γ
                    → Tᵢ ⊆ Tₓ
                    -----------------------------------------
-                   → Γ ⊢B (output (solicitres o l e x)) ▹ subst Ctx n≡m Γ
+                   → Γ ⊢B output (solicitres o l e x) ▹ subst Ctx n≡m Γ
 
   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ₒ) ∈ Γ
@@ -122,7 +120,7 @@ data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
                 → (var a Tₐ) ∈ Γ₁
                 → Tₐ ⊆ Tₒ
                 -----------------------------------
-                → Γ ⊢B (input (reqres o x a b)) ▹ Γ₁
+                → Γ ⊢B input (reqres o x a b) ▹ Γ₁
 
   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ₒ) ∈ Γ
@@ -132,26 +130,26 @@ data _⊢B_▹_ : ∀ {n m} → Ctx n → Behaviour → Ctx m → Set where
                    → (var a Tₐ) ∈ Γ₁
                    → Tₐ ⊆ Tₒ
                    ------------------------------------
-                   → Γ ⊢B (input (reqres o x a b)) ▹ Γ₁
-
-
-{-# NON_TERMINATING #-}
-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 Γ₁
-... | 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 (λ {(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 Γ₁ = {!!}
+                   → Γ ⊢B input (reqres o x a b) ▹ Γ₁
+
+  t-wait-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
+             → (outSolRes o l Tₒ Tᵢ) ∈ Γ
+             → ¬ ((var x Tₓ) ∈ Γ)
+             → (var x Tᵢ) ∈ Γ₁
+             ------------------------
+             → Γ ⊢B wait r o l x ▹ Γ₁
+
+  t-wait-exists : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₒ Tᵢ Tₓ : Type} {o : Operation} {l : Location} {r : Channel} {x : Variable}
+                → (outSolRes o l Tₒ Tᵢ) ∈ Γ
+                → ((var x Tₓ) ∈ Γ)
+                → Tᵢ ⊆ Tₓ
+                ------------------------
+                → Γ ⊢B wait r o l x ▹ Γ₁
+
+  t-exec : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₒ Tᵢ Tₓ : Type} {b : Behaviour} {r : Channel} {o : Operation} {x : Variable}
+         → (inReqRes o Tᵢ Tₒ) ∈ Γ
+         → Γ ⊢B b ▹ Γ₁
+         → (var x Tₓ) ∈ Γ
+         → Tₓ ⊆ Tₒ
+         ------------------------
+         → Γ ⊢B exec r o x b ▹ Γ₁