repos / jolie.agda.git

commit

30b45bc

parent

a20278c

author

Eugene Akentyev

date

2016-11-02 02:50:56 +0400 +04

Add type_of_value and type_of_var. Remove maybe from if-then-else behaviour.

 1@@ -1,6 +1,5 @@
 2 module Behaviour where
 3 
 4-open import Data.Maybe using (Maybe)
 5 open import Data.String using (String)
 6 open import Data.List using (List)
 7 open import Data.Product using (_×_)
 8@@ -22,7 +21,7 @@ data Input_ex : Set where
 9 data Behaviour where
10   input : Input_ex → Behaviour
11   output : Output_ex → Behaviour
12-  if : Expr → Behaviour → Maybe Behaviour → Behaviour
13+  if : Expr → Behaviour → Behaviour → Behaviour
14   while : Expr → Behaviour → Behaviour
15   seq : Behaviour → Behaviour → Behaviour
16   par : Behaviour → Behaviour → Behaviour

 1@@ -1,8 +1,10 @@
 2 module Expr where
 3 
 4+open import Data.Maybe using (Maybe; just; nothing)
 5 open import Variable
 6 
 7 
 8+-- TODO: add logic operations and, or
 9 data BinOp : Set where
10   plus : BinOp
11   minus : BinOp

 1@@ -1,5 +1,9 @@
 2 module Typecheck where
 3 
 4+import Relation.Binary.PropositionalEquality as PropEq
 5+open import Data.Maybe using (Maybe; just; nothing)
 6+open import Data.Bool using (if_then_else_)
 7+open import Data.Product using (_,_)
 8 open import Function
 9 open import Expr
10 open import Type
11@@ -7,19 +11,37 @@ open import Behaviour
12 open import Variable
13 
14 
15+type_of_value : Value → BasicType
16+type_of_value (Value.string _) = Type.string
17+type_of_value (Value.int _) = Type.int
18+type_of_value (Value.bool _) = Type.bool
19+type_of_value (Value.double _) = Type.double
20+type_of_value (Value.long _) = Type.long
21+
22+type_of_var : Variable → Maybe BasicType
23+type_of_var (leaf _ v) = just $ type_of_value v
24+type_of_var _ = nothing
25+
26 data Check (Γ : Ctx) : Behaviour → Set where
27   yes : {b : Behaviour} → Check Γ b
28   no : {b : Behaviour} → Check Γ b
29 
30 typecheck_behaviour : (Γ : Ctx) → (b : Behaviour) → Check Γ b
31-typecheck_behaviour env nil = yes
32-typecheck_behaviour env (if e b1 maybe_b2) =
33+typecheck_behaviour ctx nil = yes
34+typecheck_behaviour ctx (if e b1 b2) =
35   case e of λ
36   {
37     -- If conditional expression is variable
38     (var v) →
39-      let ctx1 = typecheck_behaviour env b1 in
40-      {!!}
41+      let ctx1 = typecheck_behaviour ctx b1 in
42+      case (type_of_var v) of λ
43+      -- If e : bool
44+      { (just bool) →
45+        let ctx2 = typecheck_behaviour ctx b2 in
46+        {!!}
47+      ; _ → no
48+      }
49+      --case ()
50   ; _ → no
51   }
52 typecheck_behaviour _ _ = no