implementation module Sil.Types

from StdFunc import const
import StdList
import StdOverloaded
import StdString

import Control.Applicative
import Control.Monad
import Data.Error
from Data.Func import $
import Data.Maybe
from Text import <+

import GenEq

import Sil.Syntax

derive gEq Type
instance == Type where == a b = gEq{|*|} a b

instance toString Type
where
	toString TBool = "Bool"
	toString TInt  = "Int"
	toString TVoid = "Void"
	toString (at --> rt) = "(" <+ at <+ " -> " <+ rt <+ ")"

instance toString TypeError
where
	toString (IllegalApplication ft et) = "Cannot apply a " <+ et <+ " to a " <+ ft <+ "."

typeSize :: Type -> Int
typeSize TVoid = 0
typeSize TBool = 1
typeSize TInt  = 1

instance zero TypeResolver where zero = const Nothing

instance type Function
where
	type res f = Just $ Ok $ foldr (-->) f.f_type [a.arg_type \\ a <- f.f_args]

instance type Expression
where
	type res (Name n) = type res n
	type res (Literal lit) = case lit of
		BLit _ -> Just $ Ok TBool
		ILit _ -> Just $ Ok TInt
	type res (App n args) =
		mapM (type res) args >>= \ats ->
		res n >>= \ft -> pure
		( sequence ats >>= \ats ->
		  ft           >>= \ft  -> foldM tryApply ft ats)
	type res (BuiltinApp op e) =
		type res e  >>= \te  ->
		type res op >>= \top -> pure
		( top >>= \top ->
		  te  >>= \te  -> tryApply top te)
	type res (BuiltinApp2 e1 op e2) =
		type res e1 >>= \te1 ->
		type res e2 >>= \te2 ->
		type res op >>= \top -> pure
		( top >>= \top ->
		  te1 >>= \te1 ->
		  te2 >>= \te2 -> foldM tryApply top [te1,te2])

tryApply :: Type Type -> MaybeError TypeError Type
tryApply ft=:(at --> rt) et
| et == at     = Ok rt
| otherwise    = Error $ IllegalApplication ft et
tryApply ft et = Error $ IllegalApplication ft et

instance type Name where type res n = res n

instance type Op1
where
	type _ Neg = Just $ Ok $ TInt  --> TInt
	type _ Not = Just $ Ok $ TBool --> TBool

instance type Op2
where
	type _ Add    = Just $ Ok $ TInt  --> TInt  --> TInt
	type _ Sub    = Just $ Ok $ TInt  --> TInt  --> TInt
	type _ Mul    = Just $ Ok $ TInt  --> TInt  --> TInt
	type _ Div    = Just $ Ok $ TInt  --> TInt  --> TInt
	type _ Rem    = Just $ Ok $ TInt  --> TInt  --> TInt
	type _ Equals = Just $ Ok $ TInt  --> TInt  --> TBool
	type _ LogOr  = Just $ Ok $ TBool --> TBool --> TBool
	type _ LogAnd = Just $ Ok $ TBool --> TBool --> TBool