{-# LANGUAGE CPP              #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

module Agda.TypeChecking.Reduce.Monad
  ( constructorForm
  , enterClosure
  , underAbstraction , underAbstraction_
  , addCtxTel
  , getConstInfo
  , isInstantiatedMeta
  , lookupMeta
  , askR, applyWhenVerboseS
  ) where

import Prelude hiding (null)

import Control.Arrow ((***), first, second)
import Control.Applicative hiding (empty)
import Control.Monad.Reader

import qualified Data.IntMap as IntMap
import qualified Data.Map as Map
import Data.Maybe
import Data.Monoid

import Debug.Trace
import System.IO.Unsafe

import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad hiding
  ( enterClosure, underAbstraction_, underAbstraction, addCtx,
    isInstantiatedMeta, verboseS, typeOfConst, lookupMeta, lookupMeta' )
import Agda.TypeChecking.Monad.Builtin hiding ( constructorForm )
import Agda.TypeChecking.Substitute
import Agda.Interaction.Options

import qualified Agda.Utils.HashMap as HMap
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty

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

instance HasBuiltins ReduceM where
  getBuiltinThing b = liftM2 mplus (Map.lookup b <$> useR stLocalBuiltins)
                                   (Map.lookup b <$> useR stImportedBuiltins)

constructorForm :: HasBuiltins m => Term -> m Term
constructorForm v = do
  mz <- getBuiltin' builtinZero
  ms <- getBuiltin' builtinSuc
  return $ fromMaybe v $ constructorForm' mz ms v

enterClosure :: Closure a -> (a -> ReduceM b) -> ReduceM b
enterClosure (Closure sig env scope cps x) f = localR (mapRedEnvSt inEnv inState) (f x)
  where
    inEnv   e = env
    inState s =
      -- TODO: use the signature here? would that fix parts of issue 118?
      set stScope scope $ set stModuleCheckpoints cps s

withFreshR :: (ReadTCState m, HasFresh i) => (i -> m a) -> m a
withFreshR f = do
  s <- getTCState
  let (i, s') = nextFresh s
  withTCState (const s') (f i)

withFreshName :: (MonadReduce m) => Range -> ArgName -> (Name -> m a) -> m a
withFreshName r s k = withFreshR $ \i -> k (mkName r i s)

withFreshName_ :: (MonadReduce m) => ArgName -> (Name -> m a) -> m a
withFreshName_ = withFreshName noRange

addCtx :: (MonadReduce m) => Name -> Dom Type -> m a -> m a
addCtx x a ret = do
  ctx <- asksTC $ map (fst . unDom) . envContext
  let ce = (x,) <$> a
  oldChkpt <- viewTC eCurrentCheckpoint
  withFreshR $ \ chkpt ->
    localTC (\e -> e { envContext = ce : envContext e
                   , envCurrentCheckpoint = chkpt
                   , envCheckpoints = Map.insert chkpt IdS $
                                        fmap (raise 1) (envCheckpoints e)
                   }) ret
      -- let-bindings keep track of own their context

addCtxTel :: (MonadReduce m) => Telescope -> m a -> m a
addCtxTel EmptyTel          ret = ret
addCtxTel (ExtendTel t tel) ret = underAbstraction t tel $ \tel -> addCtxTel tel ret

underAbstraction :: (MonadReduce m, Subst t a) => Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction _ (NoAbs _ v) f = f v
underAbstraction t a f =
  withFreshName_ (realName $ absName a) $ \x -> addCtx x t $ f (absBody a)
  where
    realName s = if isNoName s then "x" else s

underAbstraction_ :: (MonadReduce m, Subst t a) => Abs a -> (a -> m b) -> m b
underAbstraction_ = underAbstraction __DUMMY_DOM__

lookupMeta' :: MetaId -> ReduceM (Maybe MetaVariable)
lookupMeta' (MetaId i) = IntMap.lookup i <$> useR stMetaStore

lookupMeta :: MetaId -> ReduceM MetaVariable
lookupMeta = fromMaybe __IMPOSSIBLE__ <.> lookupMeta'

isInstantiatedMeta :: MetaId -> ReduceM Bool
isInstantiatedMeta i = do
  mv <- lookupMeta i
  return $ case mvInstantiation mv of
    InstV{} -> True
    _       -> False

-- | Apply a function if a certain verbosity level is activated.
--
--   Precondition: The level must be non-negative.
{-# SPECIALIZE applyWhenVerboseS :: VerboseKey -> Int -> (ReduceM a -> ReduceM a) -> ReduceM a-> ReduceM a #-}
applyWhenVerboseS :: HasOptions m => VerboseKey -> Int -> (m a -> m a) -> m a -> m a
applyWhenVerboseS k n f a = ifM (hasVerbosity k n) (f a) a

instance MonadDebug ReduceM where

  traceDebugMessage n s cont = do
    ReduceEnv env st <- askR
    unsafePerformIO $ do
      _ <- runTCM env st $ displayDebugMessage n s
      return $ cont

  formatDebugMessage k n d = do
    ReduceEnv env st <- askR
    unsafePerformIO $ do
      (s , _) <- runTCM env st $ formatDebugMessage k n d
      return $ return s

instance HasConstInfo ReduceM where
  getRewriteRulesFor = defaultGetRewriteRulesFor getTCState
  getConstInfo' q = do
    ReduceEnv env st <- askR
    defaultGetConstInfo st env q