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

diff --git a/src/Behaviour.agda b/src/Behaviour.agda
index 5f2a8930804a3ad49ca02788c871c612ae6e439e..09091ac9e96b6c13a265163ff291bc16118b051e 100644 (file)
--- a/src/Behaviour.agda
+++ b/src/Behaviour.agda
@@ -1,6 +1,5 @@
 module Behaviour where
 
-open import Data.Maybe using (Maybe)
 open import Data.String using (String)
 open import Data.List using (List)
 open import Data.Product using (_×_)
@@ -22,7 +21,7 @@ data Input_ex : Set where
 data Behaviour where
   input : Input_ex → Behaviour
   output : Output_ex → Behaviour
-  if : Expr → Behaviour → Maybe Behaviour → Behaviour
+  if : Expr → Behaviour → Behaviour → Behaviour
   while : Expr → Behaviour → Behaviour
   seq : Behaviour → Behaviour → Behaviour
   par : Behaviour → Behaviour → Behaviour

diff --git a/src/Expr.agda b/src/Expr.agda
index a2990645795fa9a4f2e02145580c2d29e448ca95..b6360f32703d35136d83d507a92731b6ef4b354d 100644 (file)
--- a/src/Expr.agda
+++ b/src/Expr.agda
@@ -1,8 +1,10 @@
 module Expr where
 
+open import Data.Maybe using (Maybe; just; nothing)
 open import Variable
 
 
+-- TODO: add logic operations and, or
 data BinOp : Set where
   plus : BinOp
   minus : BinOp

diff --git a/src/Typecheck.agda b/src/Typecheck.agda
index 5de57a91fd986ef8e9898c5497b8a8b9f432ab8f..26b280047071660ba4e671e3bf69900648ec67fb 100644 (file)
--- a/src/Typecheck.agda
+++ b/src/Typecheck.agda
@@ -1,5 +1,9 @@
 module Typecheck where
 
+import Relation.Binary.PropositionalEquality as PropEq
+open import Data.Maybe using (Maybe; just; nothing)
+open import Data.Bool using (if_then_else_)
+open import Data.Product using (_,_)
 open import Function
 open import Expr
 open import Type
@@ -7,19 +11,37 @@ open import Behaviour
 open import Variable
 
 
+type_of_value : Value → BasicType
+type_of_value (Value.string _) = Type.string
+type_of_value (Value.int _) = Type.int
+type_of_value (Value.bool _) = Type.bool
+type_of_value (Value.double _) = Type.double
+type_of_value (Value.long _) = Type.long
+
+type_of_var : Variable → Maybe BasicType
+type_of_var (leaf _ v) = just $ type_of_value v
+type_of_var _ = nothing
+
 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) =
+typecheck_behaviour ctx nil = yes
+typecheck_behaviour ctx (if e b1 b2) =
   case e of λ
   {
     -- If conditional expression is variable
     (var v) →
-      let ctx1 = typecheck_behaviour env b1 in
-      {!!}
+      let ctx1 = typecheck_behaviour ctx b1 in
+      case (type_of_var v) of λ
+      -- If e : bool
+      { (just bool) →
+        let ctx2 = typecheck_behaviour ctx b2 in
+        {!!}
+      ; _ → no
+      }
+      --case ()
   ; _ → no
   }
 typecheck_behaviour _ _ = no