content: {-# LANGUAGE CPP #-}
  {-# LANGUAGE DeriveDataTypeable #-}
  
  module IType(
    IType(..)
    ,IKind(..)
    ,itArrow
    ,iToCT
    ,iToCK
     )
      where
  
  #if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 804)
  import Prelude hiding ((<>))
  #endif
  
  import ErrorUtil(internalError)
  import Id(Id)
  import PreIds(idArrow)
  import CType(Type(..), CType, TyCon(..), Kind(..),
               TISort, cTApplys, cTVar, cTCon, cTNum, cTStr)
  import StdPrel(tiArrow)
  import Eval(Hyper(..),hyper3, hyper2, hyper)
  import PPrint
  import PFPrint
  import Position(noPosition)
  import Util(itos)
  import FStringCompat(FString)
  import qualified Data.Generics as Generic
  
  -- ==============================
  -- IKind, IType
  
  data IKind
          = IKStar
          | IKNum
          | IKStr
          | IKFun IKind IKind
          deriving (Eq, Ord, Show, Generic.Data, Generic.Typeable)
  
  data IType
          = ITForAll Id IKind IType
          | ITAp IType IType
          | ITVar Id
          | ITCon Id IKind TISort
          | ITNum Integer
          | ITStr FString
          deriving (Show, Generic.Data, Generic.Typeable)
  
  -- --------------------------------
  -- Hyper Instances
  instance Hyper IType where
      hyper (ITForAll i k t) y = hyper3 i k t y
      hyper (ITAp a b) y = hyper2 a b y
      hyper (ITVar i) y = hyper i y
      hyper (ITCon i k s) y = hyper3 i k s y
      hyper (ITNum i) y = hyper i y
      hyper (ITStr s) y = hyper s y
  
  instance Hyper IKind where
      hyper IKStar y = y
      hyper IKNum y = y
      hyper IKStr y = y
      hyper (IKFun a b) y = hyper2 a b y
  
  -- --------------------------------
  -- Eq Instances
  instance Eq IType where
      x == y  =  cmpT x y == EQ
      x /= y  =  cmpT x y /= EQ
  
  instance Ord IType where
      compare x y = cmpT x y
  
  cmpT :: IType -> IType -> Ordering
  cmpT (ITForAll i1 _ t1) (ITForAll i2 _ t2) =  -- kind comparison skipped for speed
          case compare i1 i2 of
          EQ -> cmpT t1 t2
          o  -> o
  cmpT (ITForAll _  _  _ ) _                   = LT
  
  cmpT (ITAp _ _)          (ITForAll _  _  _)  = GT
  cmpT (ITAp f1 a1)        (ITAp f2 a2)        =
          case cmpT f1 f2 of
          EQ -> cmpT a1 a2
          o  -> o
  cmpT (ITAp _  _)         _                   = LT
  
  cmpT (ITVar _)           (ITForAll _  _  _)  = GT
  cmpT (ITVar _)           (ITAp _  _)         = GT
  cmpT (ITVar i1)          (ITVar i2)          = compare i1 i2
  cmpT (ITVar _)           _                   = LT
  
  cmpT (ITCon _  _ _)      (ITForAll _  _  _)  = GT
  cmpT (ITCon _  _ _)      (ITAp _ _)          = GT
  cmpT (ITCon _  _ _)      (ITVar _)           = GT
  cmpT (ITCon i1 _ _)      (ITCon i2 _ _)      = compare i1 i2
  cmpT (ITCon _  _ _)      _                   = LT
  
  cmpT (ITNum _)           (ITForAll _  _  _)  = GT
  cmpT (ITNum _)           (ITAp _ _)          = GT
  cmpT (ITNum _)           (ITVar _)           = GT
  cmpT (ITNum _)           (ITCon _ _ _)       = GT
  cmpT (ITNum n1)          (ITNum n2)          = compare n1 n2
  cmpT (ITNum _)           _                   = LT
  
  cmpT (ITStr s1)          (ITStr s2)          = compare s1 s2
  cmpT (ITStr _)           _                   = GT
  
  -- -----------------------------------------
  -- Pretty Print instances PPrint and PVPrint
  
  instance PPrint IKind where
      pPrint _ _ IKStar = text "*"
      pPrint _ _ IKNum = text "#"
      pPrint _ _ IKStr = text "$"
      pPrint d p (IKFun l r) = pparen (p>9) $ pPrint d 9 l <+> text "->" <+> pPrint d 10 r
  
  instance PPrint IType where
      pPrint d p (ITForAll i k t) = ppQuant "\\/" d p i k t
      pPrint d p (ITAp (ITAp arr a) r) | arr == itArrow =
          pparen (p > 8) (sep [pPrint d 9 a <+> text "->", pPrint d 8 r])
      pPrint d p (ITAp e e') = pparen (p>9) $
          sep [pPrint d 9 e, pPrint d 10 e']
      pPrint d p (ITVar i) = pPrint d 0 i
      pPrint d p (ITCon c _ _) = pPrint d 0 c
      pPrint d p (ITNum n) = text (itos n)
      pPrint d p (ITStr s) = text (show s)
  
  instance PVPrint IType where
      -- convert to CType and use the PVPrint instance for that
      pvPrint d p ity =
          let convITyToCTy (ITForAll _ _ t) = convITyToCTy t
              convITyToCTy (ITAp t1 t2)  = cTApplys (convITyToCTy t1)
                                                    [convITyToCTy t2]
              convITyToCTy (ITVar i)     = cTVar i
              convITyToCTy (ITCon i _ _) = cTCon i
              convITyToCTy (ITNum n)     = cTNum n noPosition
              convITyToCTy (ITStr s)     = cTStr s noPosition
          in  pvPrint d p (convITyToCTy ity)
  
  -- ---------------------------------------------------
  -- Other utility functions
  
  -- Function type (a -> b)
  itArrow :: IType
  itArrow = ITCon (idArrow noPosition) (IKFun IKStar (IKFun IKStar IKStar)) tiArrow
  
  -- Pretty print ITForAll
  ppQuant :: String -> PDetail -> Int -> Id -> IKind -> IType -> Doc
  ppQuant s d p i t e =
      pparen (p>0) (sep [text s <> pparen True (pPrint d 0 i <>text" ::" <+> pPrint d 0 t) <+> text ".", pPrint d 0 e])
  
  -- ---------------------------------------------------
  -- Convert ISyntax kinds/types to CType
  
  iToCT :: IType -> CType
  iToCT (ITForAll _ _ _) = internalError "IConv.iToCT: ITForAll"
  iToCT (ITAp t1 t2) = TAp (iToCT t1) (iToCT t2)
  iToCT (ITVar i) = internalError "IConv.iToCT: ITVar"
  iToCT (ITCon i k s) = TCon (TyCon i (Just (iToCK k)) s)
  iToCT (ITNum n) = TCon (TyNum n noPosition)
  iToCT (ITStr s) = TCon (TyStr s noPosition)
  
  iToCK :: IKind -> Kind
  iToCK (IKStar) = KStar
  iToCK (IKNum) = KNum
  iToCK (IKStr) = KStr
  iToCK (IKFun k1 k2) = Kfun (iToCK k1) (iToCK k2)
  