{-# 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