    {-# 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 qualified Data.Map as Map
    import Data.Maybe

    import System.IO.Unsafe

    import Agda.Syntax.Common.Pretty () --instance only
    import Agda.Syntax.Internal

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

    import Agda.Utils.Lens
    import Agda.Utils.Maybe
    import Agda.Utils.Monad

    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