Add check type for behaviour

diff --git a/src/Type.agda b/src/Type.agda
index a2ac4d4a1cbdc78ee6762e4a4b5ed217124ca58d..2d8cf33659cb8d79e83b93d0f6227883d73adf55 100644 (file)
--- 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 7b75c27d479a7a4a072b78826beefd652ff7ec7b..5de57a91fd986ef8e9898c5497b8a8b9f432ab8f 100644 (file)
--- 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