{-# 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` (map ($()) [ByteT, ShortT, IntT, LongT, CharT, FloatT, DoubleT]) -> True
      _ -> False

isIntConvertible :: TcType -> Bool
isIntConvertible t =
    case unboxConvert t of
      Just t | t `elem` (map ($()) [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