{-# LANGUAGE CPP, DeriveDataTypeable #-}
module Language.Java.Paragon.TypeCheck.Types where

import Language.Java.Paragon.Syntax
import Language.Java.Paragon.Pretty

import Language.Java.Paragon.TypeCheck.Policy
import Language.Java.Paragon.TypeCheck.Locks
import Language.Java.Paragon.TypeCheck.Actors

import Data.Maybe (isJust, fromJust)
import Text.PrettyPrint

#ifdef BASE4
import Data.Data
#else
import Data.Generics (Data(..),Typeable(..))
#endif

data TcType
    = TcPrimT PrimType | TcRefT TcRefType | TcVoidT
    | TcActorIdT ActorId | TcPolicyPolT TcPolicy | TcLockT [TcLock]
  deriving (Eq, Ord, Show, Data, Typeable)

data TcRefType
    = TcClsRefT TcClassType
    | TcArrayT TcType (Maybe TcPolicy)
    | TcTypeVar Ident
  deriving (Eq, Ord, Show, Data, Typeable)

data TcClassType
    = TcClassT [(Ident, [TcTypeArg])] | TcNullT -- Ignore wildcards for now
  deriving (Eq, Ord, Show, Data, Typeable)

data TcTypeArg
    = TcActualType TcRefType
    | TcActualPolicy TcPolicy
    | TcActualActor ActorId
    | TcActualLockState [TcLock]
  deriving (Eq, Ord, Show, Data, Typeable)

-- type TcTypeArg = TcTypeArgRaw ActorId TcPolicy TcLock

------------------------------------
-- Constructors

booleanT, byteT, shortT, intT, longT, 
 charT, floatT, doubleT, actorT, policyT :: TcType
booleanT = TcPrimT BooleanT
byteT    = TcPrimT ByteT
shortT   = TcPrimT ShortT
intT     = TcPrimT IntT
longT    = TcPrimT LongT
charT    = TcPrimT CharT
floatT   = TcPrimT FloatT
doubleT  = TcPrimT DoubleT
actorT   = TcPrimT ActorT
policyT  = TcPrimT PolicyT

nullT, voidT :: TcType
nullT    = TcRefT (TcClsRefT TcNullT)
voidT    = TcVoidT

actorIdT :: ActorId -> TcType
actorIdT = TcActorIdT

policyPolT :: TcPolicy -> TcType
policyPolT = TcPolicyPolT

lockT :: [TcLock] -> TcType
lockT = TcLockT

clsTypeWArg :: [(Ident, [TcTypeArg])] -> TcType
clsTypeWArg = TcRefT . TcClsRefT . TcClassT

clsType :: Ident -> TcType
clsType = qualClsType . return

qualClsType :: [Ident] -> TcType
qualClsType = clsTypeWArg . map (\i -> (i, []))

stringT :: TcType
stringT = clsType (Ident "String")

-- promoting

clsTypeToType :: TcClassType -> TcType
clsTypeToType = TcRefT . TcClsRefT



-----------------------------------
-- Destructors

-- Invariant: First argument is a class type
typeName :: TcType -> Maybe Name
typeName (TcRefT (TcClsRefT (TcClassT pn))) =
         let (is, args) = unzip pn
         in if all null args then Just (Name is) else Nothing
typeName _ = Nothing

typeName_ :: TcType -> Name
typeName_ (TcRefT (TcClsRefT (TcClassT pn))) =
    let (is, _) = unzip pn in Name is
typeName_ t = error $ "typeName_: Not a class type: " ++ show t

--typeName_ typ = case typeName typ of
--                  Just n -> n
--                  Nothing -> error $ "typeName_: " ++ show typ

isClassType, isRefType, isNullType :: TcType -> Bool
isClassType (TcRefT (TcClsRefT (TcClassT _))) = True
isClassType _ = False

isRefType (TcRefT _) = True
isRefType _ = False

isNullType (TcRefT (TcClsRefT TcNullT)) = True
isNullType _ = False

mActorId :: TcType -> Maybe ActorId
mActorId (TcActorIdT aid) = Just aid
mActorId _ = Nothing

mLocks :: TcType -> Maybe [TcLock]
mLocks (TcLockT ls) = Just ls
mLocks _ = Nothing

mPolicyPol :: TcType -> Maybe TcPolicy
mPolicyPol (TcPolicyPolT p) = Just p
mPolicyPol _ = Nothing

isLockType :: TcType -> Bool
isLockType = isJust . mLocks

isActorType :: TcType -> Bool
isActorType = isJust . mActorId

isPolicyType :: TcType -> Bool
isPolicyType = isJust . mPolicyPol


-------------------------------------------
-- Type operations


unboxConvert :: TcType -> Maybe PrimType
unboxConvert (TcPrimT t) = Just t
unboxConvert (TcRefT (TcClsRefT (TcClassT is))) =
    case map ((\(Ident x) -> x) . fst) is of
      ["java", "lang", "Boolean"  ] -> Just BooleanT
      ["java", "lang", "Byte"     ] -> Just ByteT
      ["java", "lang", "Character"] -> Just CharT
      ["java", "lang", "Short"    ] -> Just ShortT
      ["java", "lang", "Integer"  ] -> Just IntT
      ["java", "lang", "Long"     ] -> Just LongT
      ["java", "lang", "Float"    ] -> Just FloatT
      ["java", "lang", "Double"   ] -> Just DoubleT
      _ -> Nothing

isNumConvertible :: TcType -> Bool
isNumConvertible t =
    case unboxConvert t of
      Just t | t `elem` [ByteT, ShortT, IntT, LongT, CharT, FloatT, DoubleT] -> True
      _ -> False

isIntConvertible :: TcType -> Bool
isIntConvertible t =
    case unboxConvert t of
      Just t | t `elem` [ByteT, ShortT, IntT, LongT, CharT] -> True
      _ -> False

isBoolConvertible :: TcType -> Bool
isBoolConvertible t = unboxConvert t == Just BooleanT

unaryNumPromote :: TcType -> Maybe PrimType
unaryNumPromote t =
    case unboxConvert t of
      Just t | t `elem` [ByteT, ShortT, IntT, CharT] -> Just IntT
      Just t | t `elem` [LongT, FloatT, DoubleT] -> Just t
      _ -> Nothing

unaryNumPromote_ :: TcType -> TcType
unaryNumPromote_ = TcPrimT . fromJust . unaryNumPromote

binaryNumPromote :: TcType -> TcType -> Maybe PrimType
binaryNumPromote t1 t2 = 
    case (unboxConvert t1, unboxConvert t2) of
      (Just tc1, Just tc2) -> Just $ 
          let tcs = [tc1, tc2]
              pts = [DoubleT, FloatT, LongT, IntT]
           in case break (`elem` tcs) pts of
                (_, []) -> IntT
                (_, t:_) -> t
      _ -> Nothing

binaryNumPromote_ :: TcType -> TcType -> TcType
binaryNumPromote_ t1 t2 = TcPrimT . fromJust $ binaryNumPromote t1 t2

---------------------------------------------
-- Pretty printing

instance Pretty TcType where
  pretty tct =
      case tct of
        TcPrimT pt -> pretty pt
        TcRefT rt -> pretty rt
        TcVoidT -> text "void"
        TcActorIdT aid -> text "actor[" <> pretty aid <> text "]"
        TcPolicyPolT p -> text "policy[" <> pretty p <> text "]"
        TcLockT ls -> (hsep $ text "lock[" : punctuate (text ",") (map pretty ls)) <> text "]"

instance Pretty TcRefType where
  pretty tcrt =
      case tcrt of
        TcClsRefT ct -> pretty ct
        TcArrayT t mp -> pretty t <> text "[]" <> maybe empty pretty mp
        TcTypeVar i -> pretty i

instance Pretty TcClassType where
  pretty (TcClassT iargs) =
      hcat . punctuate (char '.') $ map (\(i,tas) -> pretty i <> ppTypeParams tas) iargs

instance Pretty TcTypeArg where
  pretty (TcActualType t) = pretty t
  pretty (TcActualPolicy p) = text "policy" <+> pretty p
  pretty (TcActualActor aid) = text "actor" <+> pretty aid
  pretty (TcActualLockState ls) = text "lock[]" <+> ppArgs ls

instance Pretty TcPolicy where
  pretty (TcPolicy cs) = braces $ hcat (punctuate (char ';') $ map pretty cs)
  pretty (TcPolicyVar mv) = pretty mv
  pretty (TcRigidVar i) = text "policyof" <> parens (pretty i)
  pretty (TcJoin p1 p2) = pretty p1 <+> char '*' <+> pretty p2
  pretty (TcMeet p1 p2) = pretty p1 <+> char '+' <+> pretty p2

instance Pretty TcMetaVar where
  pretty (TcMetaVar i _) = text ("$$" ++ show i)

instance Pretty a => Pretty (TcClause a) where
  pretty (TcClause h b) = pretty h <> char ':' <+> hcat (punctuate (char ',') $ map pretty b)

instance Pretty TcAtom where
  pretty (TcAtom n as) = pretty n <> opt (not $ null as) (parens (hcat (punctuate (char ',') $ map pretty as)))

instance Pretty TcActor where
  pretty (TcActor aid) = pretty aid
  pretty (TcVar i) = char '\'' <> pretty i

instance Pretty ActorId where
  pretty (Fresh k) = text ('#':show k)
  pretty (Alias k) = text ('@':show k)
  pretty (ActorTPVar i) = pretty i

instance Pretty TcLock where
  pretty (TcLock n aids) = pretty n <> 
    opt (not $ null aids) (parens (hcat (punctuate (char ',') $ map pretty aids)))
  pretty (TcLockVar i) = pretty i



ppTypeParams :: Pretty a => [a] -> Doc
ppTypeParams [] = empty
ppTypeParams tps = char '<' 
    <> hsep (punctuate comma (map pretty tps))
    <> char '>'

opt :: Bool -> Doc -> Doc
opt x a = if x then a else empty

ppArgs :: Pretty a => [a] -> Doc
ppArgs = parens . hsep . punctuate comma . map pretty