From: Eugene Akentyev Date: Tue, 1 Nov 2016 22:50:56 +0000 (+0300) Subject: Add type_of_value and type_of_var. Remove maybe from if-then-else behaviour. X-Git-Url: https://git.xn--bdkaa.com/?a=commitdiff_plain;h=30b45bc2bb31a894b49d86903b4aff8062b13f73;p=jolie.agda.git 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 5f2a893..09091ac 100644 --- 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 a299064..b6360f3 100644 --- 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 5de57a9..26b2800 100644 --- 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