    {-# LANGUAGE CPP #-}
    module Agda.TypeChecking.Level where

    import Control.Monad.Error
    import Control.Applicative
    import Data.List as List

    import Agda.Syntax.Position
    import Agda.Syntax.Common
    import Agda.Syntax.Literal
    import Agda.Syntax.Internal
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Monad.Builtin

    import Agda.Utils.Impossible
    #include "../undefined.h"

    newtype LevelView = Max [PlusView]
      deriving (Show)

    data PlusView = ClosedLevel Integer
                  | Plus Integer LevelAtom
      deriving (Show, Eq)

    data LevelAtom = MetaLevel MetaId Args
                 | BlockedLevel Term
                 | NeutralLevel Term
      deriving (Show, Eq, Ord)

    instance Ord PlusView where
      compare ClosedLevel{} Plus{}            = LT
      compare Plus{} ClosedLevel{}            = GT
      compare (ClosedLevel n) (ClosedLevel m) = compare n m
      compare (Plus n a) (Plus m b)           = compare (a,n) (b,m)

    data LevelKit = LevelKit
      { levelSuc   :: Term -> Term
      , levelMax   :: Term -> Term -> Term
      , levelZero  :: Term
      , sucName  :: QName
      , maxName  :: QName
      , zeroName :: QName
      }

    levelSucFunction :: MonadTCM tcm => tcm (Term -> Term)
    levelSucFunction = do
      suc <- primLevelSuc
      return $ \a -> suc `apply` [Arg NotHidden a]

    builtinLevelKit :: MonadTCM tcm => tcm (Maybe LevelKit)
    builtinLevelKit = liftTCM $ do
        zero@(Con z []) <- primLevelZero
        suc@(Con s []) <- primLevelSuc
        max@(Def m []) <- primLevelMax
        let a @@ b = a `apply` [Arg NotHidden b]
        return $ Just $ LevelKit
          { levelSuc = \a -> suc @@ a
          , levelMax = \a b -> max @@ a @@ b
          , levelZero = zero
          , sucName = s
          , maxName = m
          , zeroName = z
          }
      `catchError` \_ -> return Nothing

    unLevelAtom :: LevelAtom -> Term
    unLevelAtom (MetaLevel x as) = MetaV x as
    unLevelAtom (BlockedLevel a) = a
    unLevelAtom (NeutralLevel a) = a

    unLevelView :: MonadTCM tcm => LevelView -> tcm Term
    unLevelView nv = case nv of
        Max []            -> return $ Lit $ LitLevel noRange 0
        Max [ClosedLevel n] -> return $ Lit $ LitLevel noRange n
        Max [Plus 0 a]    -> return $ unLevelAtom a
        Max [a]           -> do
          suc <- primLevelSuc
          return $ unPlusV (\n -> suc `apply` [Arg NotHidden n]) a
        Max as -> do
          Just LevelKit{ levelSuc = suc, levelMax = max } <- builtinLevelKit
          return $ case map (unPlusV suc) as of
            [a] -> a
            []  -> __IMPOSSIBLE__
            as  -> foldr1 max as
      where
        unPlusV suc (ClosedLevel n) = Lit (LitLevel noRange n)
        unPlusV suc (Plus n a)    = foldr (.) id (genericReplicate n suc) (unLevelAtom a)

    maybePrimCon :: MonadTCM tcm => TCM Term -> tcm (Maybe QName)
    maybePrimCon prim = liftTCM $ do
        Con c [] <- prim
        return (Just c)
      `catchError` \_ -> return Nothing

    maybePrimDef :: MonadTCM tcm => TCM Term -> tcm (Maybe QName)
    maybePrimDef prim = liftTCM $ do
        Def f [] <- prim
        return (Just f)
      `catchError` \_ -> return Nothing

    levelView :: MonadTCM tcm => Term -> tcm LevelView
    levelView a = do
      msuc <- maybePrimCon primLevelSuc
      mzer <- maybePrimCon primLevelZero
      mmax <- maybePrimDef primLevelMax
      let view a =
            case a of
              Con s [Arg NotHidden a]
                | Just s == msuc -> inc <$> view a
              Con z []
                | Just z == mzer -> return $ closed 0
              Lit (LitLevel _ n)   -> return $ closed n
              Def m [Arg NotHidden a, Arg NotHidden b]
                | Just m == mmax -> lub <$> view a <*> view b
              _                  -> mkAtom a
      view =<< normalise a
      where
        mkAtom a = do
          b <- reduceB a
          return $ case b of
            NotBlocked (MetaV m as) -> atom $ MetaLevel m as
            NotBlocked a            -> atom $ NeutralLevel a
            Blocked _ a             -> atom $ BlockedLevel a

        atom a = Max [Plus 0 a]

        closed n = maxim [ClosedLevel n]

        inc (Max as) = Max $ map inc' as
          where
            inc' (ClosedLevel n) = ClosedLevel $ n + 1
            inc' (Plus n a)    = Plus (n + 1) a

        maxim as = Max $ ns ++ List.sort bs
          where
            ns = case [ n | ClosedLevel n <- as, n > 0 ] of
              []  -> []
              ns  -> [ClosedLevel $ maximum ns]
            bs = subsume [ b | b@Plus{} <- as ]

            subsume (ClosedLevel{} : _) = __IMPOSSIBLE__
            subsume [] = []
            subsume (Plus n a : bs)
              | not $ null ns = subsume bs
              | otherwise     = Plus n a : subsume [ b | b@(Plus _ a') <- bs, a /= a' ]
              where
                ns = [ m | Plus m a'  <- bs, a == a', m > n ]

        lub (Max as) (Max bs) = maxim $ as ++ bs