implementation module Sil.Types

import StdBool
from StdFunc import const, o
import StdList
import StdMisc
import StdOverloaded
import StdString

import GenEq

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

from ABC.Assembler import :: BasicType(..)

import Sil.Error
import Sil.Syntax
import Sil.Util.Printer

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 <+ ")"
	toString (TTuple _ ts) = "(" <+ printersperse ", " ts <+ ")"
	toString (TList t)     = "[" <+ t <+ "]"

instance zero TypeSize where zero = {asize=0, bsize=0, btypes=[]}

typeSize :: Type -> TypeSize
typeSize TVoid        = zero
typeSize TBool        = {zero & bsize=1, btypes=[BT_Bool]}
typeSize TInt         = {zero & bsize=1, btypes=[BT_Int]}
typeSize (TTuple _ _) = {zero & asize=1}
typeSize (TList _)    = {zero & asize=1}

(+~) infixl 6 :: TypeSize TypeSize -> TypeSize
(+~) a b =
	{ asize  = a.asize  +  b.asize
	, bsize  = a.bsize  +  b.bsize
	, btypes = a.btypes ++ b.btypes
	}

(-~) infixl 6 :: TypeSize TypeSize -> TypeSize
(-~) a b =
	{ asize  = a.asize  -  b.asize
	, bsize  = a.bsize  -  b.bsize
	, btypes = abort "btypes after -~\r\n"
	}

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 Cons e2) =
		type res e1 >>= \te1 ->
		type res e2 >>= \te2 -> pure
		( te1 >>= \te1 ->
		  te2 >>= \te2 ->
		  let top = te1 --> TList te1 --> TList te1 in
		  foldM tryApply top [te1,te2])
	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])
	type res e=:(List (Just t) es) =
		mapM (type res) es >>= \tes -> pure
		(sequence tes >>= \tes -> case [(e,t`) \\ e <- es & t` <- tes | t <> t`] of
			[(e`,t`):_] -> Error $ C_TypeMisMatch t e` t`
			[]          -> Ok $ TList t)
	type res (List Nothing []) = Nothing
	type res e=:(List Nothing es) =
		mapM (type res) es >>= \tes -> pure
		(sequence tes >>= \tes -> case removeDup tes of
			[t]    -> Ok $ TList t
			[_:_]  -> Error $ C_CouldNotDeduceType e)
	type res (Tuple n es)
	| n > 32 = Just $ Error $ T_TooHighTupleArity n
	| otherwise =
		mapM (type res) es >>= \ats -> pure (sequence ats >>= pure o TTuple n)
	type res (Field f e)
	| isTuple = type res e >>= \te -> pure (te >>= \te -> case te of
		TTuple arity es -> if (0 < tupleEl && tupleEl <= arity)
			(Ok $ es!!(tupleEl - 1))
			(Error $ T_IllegalField f te)
		_ -> Error $ T_IllegalField f te)
	| f == "hd" = type res e >>= \te -> pure (te >>= \te -> case te of
		TList t -> Ok t
		_       -> Error $ T_IllegalField f te)
	| f == "tl" = type res e >>= \te -> pure (te >>= \te -> case te of
		t=:(TList _) -> Ok t
		_            -> Error $ T_IllegalField f te)
	| f == "nil" = type res e >>= \te -> pure (te >>= \te -> case te of
		(TList _) -> Ok TBool
		_         -> Error $ T_IllegalField f te)
	| otherwise = type res e >>= \te -> pure (te >>= Error o T_IllegalField f)
	where
		f` = fromString f

		isTuple = length f` >= 2 && hd f` == '_' && all isDigit (tl f`)
		tupleEl = toInt $ toString $ tl f`

tryApply :: Type Type -> MaybeError Error Type
tryApply ft=:(at --> rt) et
| et == at     = Ok rt
| otherwise    = Error $ T_IllegalApplication ft et
tryApply ft et = Error $ T_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