content: {-# LANGUAGE CPP, FlexibleContexts #-}
  -----------------------------------------------------------------------------
  -- |
  -- Module      :  CDT
  -- Copyright   :  (c) Masahiro Sakai 2004,2009
  -- License     :  BSD-style
  -- 
  -- Maintainer  :  masahiro.sakai@gmail.com
  -- Stability   :  provisional
  -- Portability :  non-portable (CPP, FlexibleContexts)
  --
  -- Categorical Data Type
  --
  -----------------------------------------------------------------------------
  
  module CDT
    ( ObjectType (..)
    , CDT
    , mkCDT
    , objectType
    , nats
    , nNats
    , isUnconditioned
  
    , functName
    , functVariance
    , functArity
  
    , Nat
    , natName
    , natNTypeParams
    , natType
    , natCDT
    , natIndex
    , natDeclType
    , natDeclDom
    , natDeclCod
    {- for optimization -}
    , natProjectionSequence
    , natIsUnconditioned
  
    , factName
    , factParams
    , factDestType
    , factNTypeParams
  
    , _eqCDT -- XXX
  
    , isComputable
    , isProductiveIn
    , showFunctNameWithVariance
  
    , isTerminalObject
    ) where
  
  import Variance
  import Funct
  import FE
  import Type
  import Subst (tv, apply)
  
  #if __GLASGOW_HASKELL__ >= 706
  import Prelude hiding (join)
  #endif
  import Data.List (findIndices, transpose, find, findIndex, intercalate)
  
  
  data ObjectType
    = LeftObject
    | RightObject
    deriving (Show, Read, Eq)
  
  data CDT
    = CDT
    { objectType      :: !ObjectType
    , nats            :: ![Nat]
    , nNats           :: !Int -- = length of nats
    , isUnconditioned :: !Bool
  
    , functName       :: !String
    , functVariance   :: ![Variance]
    , functArity      :: !Int -- = length of functVariance
  
    , factName        :: !String
    , factParams      :: ![Type]
    , factDestType    :: Type -- $B%k!<%W$rHr$1$k$?$a$K@53J%U%i%0$rIU$1$J$$(B
    }
  
  instance Funct CDT where
    variance CDT{ functVariance = vs } = vs
  
  instance Eq CDT where
    a==b = objectType a == objectType b &&
           nNats a      == nNats b &&
           functName a  == functName b &&
           functArity a == functArity b &&
           all (\(n1,n2) -> natName n1 == natName n2 &&
                            natDeclType n1 == natDeclType n2)
               (zip (nats a) (nats b))
  
  _eqCDT :: CDT -> CDT -> Bool
  _eqCDT a b = a==b
  
  data Nat
    = Nat
    { natName     :: !String
    , natType     :: !Type
    , natCDT      :: !CDT
    , natIndex    :: !Int
    , natDeclType :: !Type
  
    {- for optimization -}
  
    -- right object $B$G$7$+0UL#$,L5$$$N$G(B!$B$rIU$1$J$$(B
    , natProjectionSequence :: [Int]
  
    , natIsUnconditioned :: !Bool
      {- LeftObject$B$J$i(BnatDecl$B$N(Bdom$B$K!"(B
       - RightObject$B$J$i(BnatDecl$B$N(Bcod$B$K(B
       - $B$=$N%*%V%8%'%/%H(B(Var 0)$B$,8=$o$l$F$$$J$$>l9g$K??!#(B
       -}
    }
  
  instance Eq Nat where
    a==b = natCDT a == natCDT b && natIndex a == natIndex b
  
  {-# INLINE natNTypeParams #-}
  natNTypeParams :: Nat -> Int
  natNTypeParams = functArity . natCDT
  
  {-# INLINE natDeclDom #-}
  natDeclDom :: Nat -> FE
  natDeclDom = dom . natDeclType
  
  {-# INLINE natDeclCod #-}
  natDeclCod :: Nat -> FE
  natDeclCod = cod . natDeclType
  
  {-# INLINE factNTypeParams #-}
  factNTypeParams :: CDT -> Int
  factNTypeParams factObj = functArity factObj + 1
  
  
  mkCDT :: ObjectType -> String -> Int -> String -> [(String,Type)] -> CDT
  mkCDT t functName functArity factName natDecls = object
    where
      object =
        CDT
        { objectType      = t
        , nats            = nats
        , nNats           = length (natDecls)
        , isUnconditioned = isUnconditioned
  
        , functName       = functName
        , functVariance   = vs
        , functArity      = functArity
  
        , factName     = factName
        , factParams   = map snd natDecls
        , factDestType = factDestType
        }
  
      vs = map joinL . transpose . map f $ natDecls
        where
          f (_,dom:->cod) =
            zipWith g (tail (variance (CFE (1+functArity) dom)))
                      (tail (variance (CFE (1+functArity) cod)))
          g = case t of
                LeftObject  ->
                  \a b -> a `join` (Contravariance `mult` b)
                RightObject ->
                  \a b -> (Contravariance `mult` a) `join` b
  
      factDestType =
        case t of
          LeftObject  -> a :-> b
          RightObject -> b :-> a
        where a = Ap object [Var x | x <- [1..functArity]]
              b = Var 0
  
      nats = zipWith f natDecls [0..]
        where
          f (name, declType@(dom :-> cod)) idx = nat
            where
              nat = Nat{ natName     = name
                       , natType     = apply s declType
                       , natCDT      = object
                       , natIndex    = idx
                       , natDeclType = declType
                       , natProjectionSequence =
                           case t of
                             LeftObject -> error "not a right object"
                             RightObject -> makeProjectionSequence dom
                       , natIsUnconditioned =
                           case t of
                             LeftObject  -> not (0 `elem` tv dom)
                             RightObject -> not (0 `elem` tv cod)
                       }
              s = [(x, h x) | x <- [0..functArity]]
                where
                  h 0 = Ap object [Var x | x <- [0..(functArity-1)]]
                  h n = Var (n-1)
  
      isUnconditioned = all f natDecls
        where
          f (_, dom :-> cod) =
            case t of
              LeftObject  -> 0 `notElem` tv dom
              RightObject -> 0 `notElem` tv cod
  
  ----------------------------------------------------------------------------
  
  isComputable :: CDT -> Bool
  isComputable obj =
    case objectType obj of
      LeftObject -> all f (nats obj)
        where
          f nat = case natDeclCod nat of
                    Var 0 -> True
                    _     -> False
      RightObject -> all f (nats obj)
        where
          f nat = feIsProductiveIn (natDeclDom nat) 0
  
  isProductiveIn :: CDT -> Int -> Bool
  isProductiveIn obj i =
    objectType obj == RightObject &&
    isUnconditioned obj &&
    all (\(dom :-> _) -> i+1 `notElem` tv dom) natDecls &&
    case filter (\(_ :-> cod) -> i+1 `elem` tv cod) natDecls of
      [Var 0 :-> cod] -> feIsProductiveIn cod (i+1)
      _ -> False
    where natDecls = map natDeclType (nats obj)
  
  feIsProductiveIn :: FE -> Int -> Bool
  feIsProductiveIn (Var m) n = m==n
  feIsProductiveIn (Ap functObj args) n =
    case findIndices (\arg -> n `elem` tv arg) args of
      [i] -> isProductiveIn functObj i
      _   -> False
  
  ----------------------------------------------------------------------------
  
  makeProjectionSequence :: FE -> [Int]
  makeProjectionSequence fe = 
    case fe of
      FE.Var 0 -> []
      FE.Var _ ->
        error "BUG: not a natural transformation of a computable right object"
      FE.Ap functObj args ->
        case findIndex (\arg -> 0 `elem` tv arg) args of
          Just i -> getProjection functObj i
          _      -> error "BUG"
  
  getProjection :: CDT -> Int -> [Int]
  getProjection obj i =
    case find f (nats obj) of
      Just nat -> natIndex nat : makeProjectionSequence (natDeclDom nat)
      _        -> error "BUG"
    where
      f nat = i+1 `elem` tv (natDeclCod nat) && 
              case natDeclDom nat of
                FE.Var 0 -> True
                _        -> False
  
  ----------------------------------------------------------------------------
  
  showFunctNameWithVariance :: CDT -> String
  showFunctNameWithVariance funct =
    functName funct ++
      case variance funct of
        [] -> ""
        vs -> "(" ++ intercalate "," (map Variance.mnemonic vs) ++ ")"
  
  ----------------------------------------------------------------------------
  
  isTerminalObject :: CDT -> Bool
  isTerminalObject obj = objectType obj == RightObject && null (nats obj)
  