repos / jolie.agda.git

commit

a20278c

parent

626b6f7

author

Eugene Akentyev

date

2016-11-01 22:33:22 +0400 +04

Add check type for behaviour

1@@ -47,6 +47,5 @@ data TypeDecl : Set where
2   empty : TypeDecl
3   pair : TypeDecl → TypeDecl → TypeDecl
4 
5-Γ : Set
6-Γ = List TypeDecl
7-
8+Ctx : Set
9+Ctx = List TypeDecl

 1@@ -1,19 +1,18 @@
 2 module Typecheck where
 3 
 4-open import Data.List using ([])
 5-open import Data.Maybe using (Maybe; just; nothing)
 6 open import Function
 7 open import Expr
 8 open import Type
 9 open import Behaviour
10 open import Variable
11 
12-data _⊢_▸_ : Γ → Behaviour → Γ → Set where
13-  t-nil : {γ : Γ} → γ ⊢ nil ▸ γ
14---  t-if-then : 
15 
16-typecheck_behaviour : Γ → Behaviour → Maybe Γ
17-typecheck_behaviour env nil = just env
18+data Check (Γ : Ctx) : Behaviour → Set where
19+  yes : {b : Behaviour} → Check Γ b
20+  no : {b : Behaviour} → Check Γ b
21+
22+typecheck_behaviour : (Γ : Ctx) → (b : Behaviour) → Check Γ b
23+typecheck_behaviour env nil = yes
24 typecheck_behaviour env (if e b1 maybe_b2) =
25   case e of λ
26   {
27@@ -21,6 +20,6 @@ typecheck_behaviour env (if e b1 maybe_b2) =
28     (var v) →
29       let ctx1 = typecheck_behaviour env b1 in
30       {!!}
31-  ; _ → nothing
32+  ; _ → no
33   }
34-typecheck_behaviour _ _ = nothing
35+typecheck_behaviour _ _ = no