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

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

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

typesModule :: String
typesModule = typeCheckerBase ++ ".Types"

type T = Maybe TcType -- Used for annotated AST
notAppl :: Functor f => f a -> f T
notAppl = fmap (const Nothing)


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

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

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

data TcTypeArg
    = TcActualType TcRefType
    | TcActualPolicy ActorPolicy
    | 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 TcNullT
voidT    = TcVoidT

actorIdT :: ActorId -> TcType
actorIdT = TcActorIdT

policyPolT :: ActorPolicy -> TcType
policyPolT = TcPolicyPolT

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

{-
clsTypeWArg :: Name () -> [TcTypeArg] -> TcType
clsTypeWArg n = TcClassT n
-}

clsType :: Ident () -> TcClassType
clsType = qualClsType . return

qualClsType :: [Ident ()] -> TcClassType
qualClsType is = TcClassT (mkName_ TName PName is) []

--nameToClsType :: Name () -> TcClassType
--nameToClsType (Name _ is) = TcClassT $ map (\i -> (i,[])) is
--nameToClsType _ = panic (typesModule ++ ".nameToClsType")
--                  "AntiQName should never appear in an AST being type-checked"

stringT, objectT :: TcClassType
stringT = qualClsType $ map (Ident ()) $ ["java","lang","String"]
objectT = qualClsType $ map (Ident ()) $ ["java","lang","Object"]


-- promoting

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

arrayType :: TcType -> ActorPolicy -> TcType
arrayType = (TcRefT .) . TcArrayT

mkArrayType :: TcType -> [ActorPolicy] -> TcType
mkArrayType = foldr (flip arrayType)


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

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

typeName_ :: TcType -> Name ()
typeName_ (TcRefT (TcClsRefT (TcClassT n _tas))) = mkUniformName_ AmbName $ flattenName n
--    let (is, _) = unzip pn in mkUniformName_ AmbName 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

mNameRefType :: TcRefType -> Maybe (Name ())
mNameRefType (TcClsRefT (TcClassT n as)) =
    if null as then Just (mkUniformName_ AmbName $ flattenName n) else Nothing
mNameRefType _ = Nothing

isNullType (TcRefT 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 ActorPolicy
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

mArrayType :: TcType -> Maybe (TcType, [ActorPolicy])
mArrayType (TcRefT (TcArrayT ty p)) = Just $
    case mArrayType ty of
      Nothing -> (ty, [p])
      Just (t, ps) -> (t, p:ps)
mArrayType _ = Nothing

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

widenConvert :: PrimType () -> [PrimType ()]
widenConvert pt = case pt of
   FloatT  _ -> map ($()) [DoubleT]
   LongT   _ -> map ($()) [DoubleT, FloatT]
   IntT    _ -> map ($()) [DoubleT, FloatT, LongT]
   ShortT  _ -> map ($()) [DoubleT, FloatT, LongT, IntT]
   CharT   _ -> map ($()) [DoubleT, FloatT, LongT, IntT]
   ByteT   _ -> map ($()) [DoubleT, FloatT, LongT, IntT, ShortT]
   _         -> []

narrowConvert :: PrimType () -> [PrimType ()]
narrowConvert pt = case pt of
   DoubleT _ -> map ($()) [ByteT, ShortT, CharT, IntT, LongT, FloatT]
   FloatT  _ -> map ($()) [ByteT, ShortT, CharT, IntT, LongT]
   LongT   _ -> map ($()) [ByteT, ShortT, CharT, IntT]
   IntT    _ -> map ($()) [ByteT, ShortT, CharT]
   CharT   _ -> map ($()) [ByteT, ShortT]
   ShortT  _ -> map ($()) [ByteT, CharT]
   _         -> []

widenNarrowConvert :: PrimType () -> [PrimType ()]
widenNarrowConvert (ByteT _) = [CharT ()]
widenNarrowConvert _ = []


box :: PrimType () -> Maybe (TcClassType)
box pt = case pt of
   BooleanT () -> 
       Just $
            TcClassT 
            (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Boolean"])
            []
   ByteT () -> 
       Just $
            TcClassT 
            (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Byte"])
            []
   ShortT () -> 
       Just $
            TcClassT 
            (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Short"])
            []
   CharT () -> 
       Just $
            TcClassT 
            (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Character"])
            []
   IntT () -> 
       Just $
            TcClassT 
            (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Integer"])
            []
   LongT () -> 
       Just $
            TcClassT 
            (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Long"])
            []
   FloatT () -> 
       Just $
            TcClassT 
            (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Float"])
            []
   DoubleT () -> 
       Just $
            TcClassT 
            (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Double"])
            []
   _ -> Nothing

unbox :: TcClassType -> Maybe (PrimType ())
unbox (TcClassT n _) =
    case map unIdent $ flattenName n 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
--unbox TcNullT = Nothing


unboxType :: TcType -> Maybe (PrimType ())
unboxType (TcRefT (TcClsRefT ct)) = unbox ct
unboxType _ = Nothing


unIdent :: Ident a -> String
unIdent (Ident _ x) = x
unIdent _ = panic (typesModule ++ ".unIdent")
            "AntiQIdent should not appear in AST being typechecked"

isNumConvertible :: TcType -> Bool
isNumConvertible ty = 
    ty `elem` [byteT, shortT, intT, longT, charT, floatT, doubleT] ||
    case unboxType ty of
      Just t | t `elem` (map ($()) [ByteT, ShortT, IntT, LongT, CharT, FloatT, DoubleT]) -> True
      _ -> False

isIntConvertible :: TcType -> Bool
isIntConvertible ty =
    ty `elem` [byteT, shortT, intT, longT, charT] ||
    case unboxType ty of
      Just t | t `elem` (map ($()) [ByteT, ShortT, IntT, LongT, CharT]) -> True
      _ -> False

isBoolConvertible :: TcType -> Bool
isBoolConvertible t = t == booleanT 
                      || unboxType t == Just (BooleanT ())
                      || isLockType t


unaryNumPromote :: TcType -> Maybe (PrimType ())
unaryNumPromote ty
    | TcPrimT pt <- ty            = numPromote pt
    | Just    pt <- unboxType ty  = numPromote pt
    | otherwise = Nothing

    where numPromote :: PrimType () -> Maybe (PrimType ())
          numPromote pt
              | pt `elem` map ($()) [LongT, FloatT, DoubleT] = Just pt
              | pt `elem` map ($()) [ByteT, ShortT, IntT, CharT] = Just $ IntT ()
              | otherwise = Nothing

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

binaryNumPromote :: TcType -> TcType -> Maybe (PrimType ())
binaryNumPromote t1 t2 = do
    pt1 <- unaryNumPromote t1
    pt2 <- unaryNumPromote t2
    return $ max pt1 pt2
      
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 {} -> let (bt, suff) = ppArrayType (TcRefT tcrt) in bt <> suff
        TcTypeVar i -> pretty i
        TcNullT -> text "<null>"

ppArrayType :: TcType -> (Doc, Doc)
ppArrayType (TcRefT (TcArrayT ty pol)) =
    let (bt, suff) = ppArrayType ty
    in (bt, text "[]" <> char '<' <> pretty pol <> char '>' <> suff)
ppArrayType ty = (pretty ty, empty)


instance Pretty TcClassType where
  pretty (TcClassT n tas) =
      pretty n <> ppTypeParams tas
--      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


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

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