From cc67ec1eccd6cdcf49658be50420f49a2315db0e Mon Sep 17 00:00:00 2001
From: Eugene Akentyev <ak3ntev@gmail.com>
Date: Sat, 17 Dec 2016 18:58:21 +0300
Subject: [PATCH] Add t-choice case.

---
 src/Behaviour.agda |  5 ++---
 src/Typecheck.agda | 26 +++++++++++++++-----------
 2 files changed, 17 insertions(+), 14 deletions(-)

diff --git a/src/Behaviour.agda b/src/Behaviour.agda
index 8c78720..c60c3e1 100644
--- a/src/Behaviour.agda
+++ b/src/Behaviour.agda
@@ -1,8 +1,7 @@
 module Behaviour where
 
-open import Data.Nat using (ℕ)
 open import Data.String using (String)
-open import Data.Vec using (Vec)
+open import Data.List using (List)
 open import Data.Product using (_×_)
 open import Variable
 open import Expr
@@ -28,7 +27,7 @@ data Behaviour where
   par : Behaviour → Behaviour → Behaviour
   assign : Variable → Expr → Behaviour
   nil : Behaviour
-  inputchoice : {n : ℕ} → Vec (Input_ex × Behaviour) n → Behaviour
+  inputchoice : List (Input_ex × Behaviour) → Behaviour
   wait : Channel → Operation → Location → Variable → Behaviour
   exec : Channel → Operation → Variable → Behaviour → Behaviour
 
diff --git a/src/Typecheck.agda b/src/Typecheck.agda
index 1dfca77..68c8a39 100644
--- a/src/Typecheck.agda
+++ b/src/Typecheck.agda
@@ -1,12 +1,14 @@
 module Typecheck where
 
-import Data.List as List
+open import Data.List.All using (All; all) renaming ([] to []-All; _∷_ to _∷-All_)
 import Data.Vec.Equality as VecEq
 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.Vec using (Vec; _∈_; zip; _∷_; here)
+open import Data.List using (List; []; _∷_; foldl)
+open import Data.Vec using (Vec; _∈_; zip; _∷_; here; fromList; toList) renaming ([] to []-Vec)
+open import Data.Product using (_,_; _×_)
 open import Function
 open import Expr
 open import Type
@@ -42,13 +44,10 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
           --------------------------
           → Γ ⊢B while e b ▹ Γ₁
           
-  t-choice : {Γ₁ : Ctx m} {k n : ℕ}  {η : Input_ex} {inputs : Vec Input_ex n}
-             {b : Behaviour} {behaviours : Vec Behaviour n}
-           → η ∈ inputs
-           → b ∈ behaviours
-           → Γ ⊢B seq (input η) b ▹ Γ₁
-           ----------------------------------------------
-           → Γ ⊢B inputchoice (zip inputs behaviours) ▹ Γ₁
+  t-choice : {Γ₁ : 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}
           {Γ₁ : Ctx k} {Γ₁' : Ctx k₁} {Γ₂ : Ctx p} {Γ₂' : Ctx p₁} {Γ' : Ctx m}
@@ -135,10 +134,12 @@ data _⊢B_▹_ {n m : ℕ} (Γ : Ctx n) : Behaviour → Ctx m → Set where
                    ------------------------------------
                    → Γ ⊢B (input (reqres o x a b)) ▹ Γ₁
 
+
+{-# NON_TERMINATING #-}
 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 Γ≡Γ₁})
+... | 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₂})
@@ -149,5 +150,8 @@ check-B {n} {m} {Γ₁} Γ (while e b) with Γ CtxEq.≟ Γ₁
   { (yes ctx) → yes (t-while {n} {m} {Γ} {Γ₁} {Γ≡Γ₁} expr-t ctx)
   ; (no ¬p) → no (λ {(t-while _ ctx) → ¬p ctx})
   }
-... | no ¬p = no {!!}
+... | 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 = {!!}
-- 
2.50.1