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