From a20278cb77ec59f3b1447d77ae4338aa5e0b996a Mon Sep 17 00:00:00 2001
From: Eugene Akentyev <ak3ntev@gmail.com>
Date: Tue, 1 Nov 2016 21:33:22 +0300
Subject: [PATCH] Add check type for behaviour

---
 src/Type.agda      |  5 ++---
 src/Typecheck.agda | 17 ++++++++---------
 2 files changed, 10 insertions(+), 12 deletions(-)

diff --git a/src/Type.agda b/src/Type.agda
index a2ac4d4..2d8cf33 100644
--- a/src/Type.agda
+++ b/src/Type.agda
@@ -47,6 +47,5 @@ data TypeDecl : Set where
   empty : TypeDecl
   pair : TypeDecl → TypeDecl → TypeDecl
 
-Γ : Set
-Γ = List TypeDecl
-
+Ctx : Set
+Ctx = List TypeDecl
diff --git a/src/Typecheck.agda b/src/Typecheck.agda
index 7b75c27..5de57a9 100644
--- a/src/Typecheck.agda
+++ b/src/Typecheck.agda
@@ -1,19 +1,18 @@
 module Typecheck where
 
-open import Data.List using ([])
-open import Data.Maybe using (Maybe; just; nothing)
 open import Function
 open import Expr
 open import Type
 open import Behaviour
 open import Variable
 
-data _⊢_▸_ : Γ → Behaviour → Γ → Set where
-  t-nil : {γ : Γ} → γ ⊢ nil ▸ γ
---  t-if-then : 
 
-typecheck_behaviour : Γ → Behaviour → Maybe Γ
-typecheck_behaviour env nil = just env
+data Check (Γ : Ctx) : Behaviour → Set where
+  yes : {b : Behaviour} → Check Γ b
+  no : {b : Behaviour} → Check Γ b
+
+typecheck_behaviour : (Γ : Ctx) → (b : Behaviour) → Check Γ b
+typecheck_behaviour env nil = yes
 typecheck_behaviour env (if e b1 maybe_b2) =
   case e of λ
   {
@@ -21,6 +20,6 @@ typecheck_behaviour env (if e b1 maybe_b2) =
     (var v) →
       let ctx1 = typecheck_behaviour env b1 in
       {!!}
-  ; _ → nothing
+  ; _ → no
   }
-typecheck_behaviour _ _ = nothing
+typecheck_behaviour _ _ = no
-- 
2.50.1