{-# LANGUAGE CPP #-}
{-# OPTIONS_GHC -Wunused-imports #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

module Agda.TypeChecking.Reduce.Monad
  ( constructorForm
  , enterClosure
  , getConstInfo
  , askR, applyWhenVerboseS
  ) where

import Prelude hiding (null)

import Control.Monad         ( liftM2 )

import qualified Data.Map as Map
import Data.Maybe

import System.IO.Unsafe

import Agda.Syntax.Internal
import Agda.TypeChecking.Monad hiding (enterClosure, constructorForm)
import Agda.TypeChecking.Substitute

import Agda.Utils.Lens
import Agda.Utils.Maybe
#ifdef DEBUG
import Agda.Utils.Monad
#endif
import Agda.Syntax.Common.Pretty () --instance only


instance HasBuiltins ReduceM where
  getBuiltinThing :: SomeBuiltin -> ReduceM (Maybe (Builtin PrimFun))
getBuiltinThing SomeBuiltin
b =
    (Maybe (Builtin PrimFun)
 -> Maybe (Builtin PrimFun) -> Maybe (Builtin PrimFun))
-> ReduceM (Maybe (Builtin PrimFun))
-> ReduceM (Maybe (Builtin PrimFun))
-> ReduceM (Maybe (Builtin PrimFun))
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 ((Builtin PrimFun -> Builtin PrimFun -> Builtin PrimFun)
-> Maybe (Builtin PrimFun)
-> Maybe (Builtin PrimFun)
-> Maybe (Builtin PrimFun)
forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionMaybeWith Builtin PrimFun -> Builtin PrimFun -> Builtin PrimFun
forall a. Builtin a -> Builtin a -> Builtin a
unionBuiltin)
      (SomeBuiltin
-> Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SomeBuiltin
b (Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun))
-> ReduceM (Map SomeBuiltin (Builtin PrimFun))
-> ReduceM (Maybe (Builtin PrimFun))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
-> ReduceM (Map SomeBuiltin (Builtin PrimFun))
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Map SomeBuiltin (Builtin PrimFun)
 -> f (Map SomeBuiltin (Builtin PrimFun)))
-> TCState -> f TCState
Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
stLocalBuiltins)
      (SomeBuiltin
-> Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SomeBuiltin
b (Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun))
-> ReduceM (Map SomeBuiltin (Builtin PrimFun))
-> ReduceM (Maybe (Builtin PrimFun))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
-> ReduceM (Map SomeBuiltin (Builtin PrimFun))
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Map SomeBuiltin (Builtin PrimFun)
 -> f (Map SomeBuiltin (Builtin PrimFun)))
-> TCState -> f TCState
Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
stImportedBuiltins)

constructorForm :: HasBuiltins m => Term -> m Term
constructorForm :: forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm Term
v = do
  mz <- BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinZero
  ms <- getBuiltin' builtinSuc
  return $ fromMaybe v $ constructorForm' mz ms v

enterClosure :: LensClosure c a => c -> (a -> ReduceM b) -> ReduceM b
enterClosure :: forall c a b. LensClosure c a => c -> (a -> ReduceM b) -> ReduceM b
enterClosure c
c | Closure Signature
_sig TCEnv
env ScopeInfo
scope Map ModuleName CheckpointId
cps a
x <- c
c c -> Lens' c (Closure a) -> Closure a
forall o i. o -> Lens' o i -> i
^. (Closure a -> f (Closure a)) -> c -> f c
forall b a. LensClosure b a => Lens' b (Closure a)
Lens' c (Closure a)
lensClosure = \case
  -- The \case is a hack to correctly associate the where block to the rhs
  -- rather than to the expression in the pattern guard.
  a -> ReduceM b
f -> (ReduceEnv -> ReduceEnv) -> ReduceM b -> ReduceM b
forall a. (ReduceEnv -> ReduceEnv) -> ReduceM a -> ReduceM a
localR ((TCEnv -> TCEnv) -> (TCState -> TCState) -> ReduceEnv -> ReduceEnv
mapRedEnvSt TCEnv -> TCEnv
inEnv TCState -> TCState
inState) (a -> ReduceM b
f a
x)
    where
    inEnv :: TCEnv -> TCEnv
inEnv   TCEnv
e = TCEnv
env
    inState :: TCState -> TCState
inState TCState
s =
      -- TODO: use the signature here? would that fix parts of issue 118?
      Lens' TCState ScopeInfo -> LensSet TCState ScopeInfo
forall o i. Lens' o i -> LensSet o i
set (ScopeInfo -> f ScopeInfo) -> TCState -> f TCState
Lens' TCState ScopeInfo
stScope ScopeInfo
scope (TCState -> TCState) -> TCState -> TCState
forall a b. (a -> b) -> a -> b
$ Lens' TCState (Map ModuleName CheckpointId)
-> LensSet TCState (Map ModuleName CheckpointId)
forall o i. Lens' o i -> LensSet o i
set (Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId))
-> TCState -> f TCState
Lens' TCState (Map ModuleName CheckpointId)
stModuleCheckpoints Map ModuleName CheckpointId
cps TCState
s

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

instance MonadAddContext ReduceM where
  withFreshName :: forall a. Range -> ArgName -> (Name -> ReduceM a) -> ReduceM a
withFreshName Range
r ArgName
s Name -> ReduceM a
k = (NameId -> ReduceM a) -> ReduceM a
forall (m :: * -> *) i a.
(ReadTCState m, HasFresh i) =>
(i -> m a) -> m a
withFreshR ((NameId -> ReduceM a) -> ReduceM a)
-> (NameId -> ReduceM a) -> ReduceM a
forall a b. (a -> b) -> a -> b
$ \NameId
i -> Name -> ReduceM a
k (Range -> NameId -> ArgName -> Name
forall a. MkName a => Range -> NameId -> a -> Name
mkName Range
r NameId
i ArgName
s)

  addCtx :: forall a. Name -> Dom Type -> ReduceM a -> ReduceM a
addCtx = Name -> Dom Type -> ReduceM a -> ReduceM a
forall (m :: * -> *) a.
MonadAddContext m =>
Name -> Dom Type -> m a -> m a
defaultAddCtx

  addLetBinding' :: forall a.
Origin -> Name -> Term -> Dom Type -> ReduceM a -> ReduceM a
addLetBinding' = Origin -> Name -> Term -> Dom Type -> ReduceM a -> ReduceM a
forall (m :: * -> *) a.
(ReadTCState m, MonadTCEnv m) =>
Origin -> Name -> Term -> Dom Type -> m a -> m a
defaultAddLetBinding'

  updateContext :: forall a.
Substitution -> (Context -> Context) -> ReduceM a -> ReduceM a
updateContext Substitution
rho Context -> Context
f ReduceM a
ret = (CheckpointId -> ReduceM a) -> ReduceM a
forall (m :: * -> *) i a.
(ReadTCState m, HasFresh i) =>
(i -> m a) -> m a
withFreshR ((CheckpointId -> ReduceM a) -> ReduceM a)
-> (CheckpointId -> ReduceM a) -> ReduceM a
forall a b. (a -> b) -> a -> b
$ \ CheckpointId
chkpt ->
    (TCEnv -> TCEnv) -> ReduceM a -> ReduceM a
forall a. (TCEnv -> TCEnv) -> ReduceM a -> ReduceM a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\TCEnv
e -> TCEnv
e { envContext = f $ envContext e
                     , envCurrentCheckpoint = chkpt
                     , envCheckpoints = Map.insert chkpt IdS $
                                          fmap (applySubst rho) (envCheckpoints e)
                     }) ReduceM a
ret
        -- let-bindings keep track of own their context

instance MonadDebug ReduceM where

  traceDebugMessage :: forall a.
ArgName -> VerboseLevel -> ArgName -> ReduceM a -> ReduceM a
traceDebugMessage ArgName
k VerboseLevel
n ArgName
s ReduceM a
cont = do
    ReduceEnv env st _ <- ReduceM ReduceEnv
askR
    unsafePerformIO $ do
      _ <- runTCM env st $ displayDebugMessage k n s
      return $ cont

  formatDebugMessage :: ArgName -> VerboseLevel -> TCM Doc -> ReduceM ArgName
formatDebugMessage ArgName
k VerboseLevel
n TCM Doc
d = do
    ReduceEnv env st _ <- ReduceM ReduceEnv
askR
    unsafePerformIO $ do
      (s , _) <- runTCM env st $ formatDebugMessage k n d
      return $ return s

#ifdef DEBUG
  verboseBracket k n s = applyWhenVerboseS k n $
    bracket_ (openVerboseBracket k n s) (const $ closeVerboseBracket k n)
#else
  verboseBracket :: forall a.
ArgName -> VerboseLevel -> ArgName -> ReduceM a -> ReduceM a
verboseBracket ArgName
k VerboseLevel
n ArgName
s ReduceM a
ma = ReduceM a
ma
  {-# INLINE verboseBracket #-}
#endif

  getVerbosity :: ReduceM Verbosity
getVerbosity      = ReduceM Verbosity
forall (m :: * -> *). HasOptions m => m Verbosity
defaultGetVerbosity
  getProfileOptions :: ReduceM ProfileOptions
getProfileOptions = ReduceM ProfileOptions
forall (m :: * -> *). HasOptions m => m ProfileOptions
defaultGetProfileOptions
  isDebugPrinting :: ReduceM Bool
isDebugPrinting   = ReduceM Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
defaultIsDebugPrinting
  nowDebugPrinting :: forall a. ReduceM a -> ReduceM a
nowDebugPrinting  = ReduceM a -> ReduceM a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
defaultNowDebugPrinting

instance HasConstInfo ReduceM where
  getRewriteRulesFor :: QName -> ReduceM RewriteRules
getRewriteRulesFor = QName -> ReduceM RewriteRules
forall (m :: * -> *).
(ReadTCState m, MonadTCEnv m) =>
QName -> m RewriteRules
defaultGetRewriteRulesFor
  getConstInfo' :: QName -> ReduceM (Either SigError Definition)
getConstInfo' QName
q = do
    ReduceEnv env st _ <- ReduceM ReduceEnv
askR
    defaultGetConstInfo st env q

instance PureTCM ReduceM where