    {-# 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, isInstantiatedMeta, verboseS, typeOfConst, lookupMeta, lookupMeta', constructorForm )
    import Agda.TypeChecking.Substitute

    import Agda.Utils.Lens
    import Agda.Utils.Monad
    import Agda.Utils.Pretty () --instance only

    instance HasBuiltins ReduceM where
      getBuiltinThing :: String -> ReduceM (Maybe (Builtin PrimFun))
    getBuiltinThing String
    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 Maybe (Builtin PrimFun)
    -> Maybe (Builtin PrimFun) -> Maybe (Builtin PrimFun)
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    mplus (String -> Map String (Builtin PrimFun) -> Maybe (Builtin PrimFun)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup String
    b (Map String (Builtin PrimFun) -> Maybe (Builtin PrimFun))
    -> ReduceM (Map String (Builtin PrimFun))
    -> ReduceM (Maybe (Builtin PrimFun))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' (Map String (Builtin PrimFun)) TCState
    -> ReduceM (Map String (Builtin PrimFun))
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' (Map String (Builtin PrimFun)) TCState
    stLocalBuiltins)
                                       (String -> Map String (Builtin PrimFun) -> Maybe (Builtin PrimFun)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup String
    b (Map String (Builtin PrimFun) -> Maybe (Builtin PrimFun))
    -> ReduceM (Map String (Builtin PrimFun))
    -> ReduceM (Maybe (Builtin PrimFun))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' (Map String (Builtin PrimFun)) TCState
    -> ReduceM (Map String (Builtin PrimFun))
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useR Lens' (Map String (Builtin PrimFun)) TCState
    stImportedBuiltins)

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

    enterClosure :: LensClosure a c => c -> (a -> ReduceM b) -> ReduceM b
    enterClosure :: forall a c b. LensClosure a c => 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' (Closure a) c -> Closure a
    forall o i. o -> Lens' i o -> i
    ^. forall a b. LensClosure a b => Lens' (Closure a) b
    Lens' (Closure a) c
    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' ScopeInfo TCState -> LensSet ScopeInfo TCState
    forall i o. Lens' i o -> LensSet i o
    set Lens' ScopeInfo TCState
    stScope ScopeInfo
    scope (TCState -> TCState) -> TCState -> TCState
    forall a b. (a -> b) -> a -> b
    $ Lens' (Map ModuleName CheckpointId) TCState
    -> LensSet (Map ModuleName CheckpointId) TCState
    forall i o. Lens' i o -> LensSet i o
    set Lens' (Map ModuleName CheckpointId) TCState
    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
      TCState
    s <- m TCState
    forall (m :: * -> *). ReadTCState m => m TCState
    getTCState
      let (i
    i, TCState
    s') = TCState -> (i, TCState)
    forall i. HasFresh i => TCState -> (i, TCState)
    nextFresh TCState
    s
      (TCState -> TCState) -> m a -> m a
    forall (m :: * -> *) a.
    ReadTCState m =>
    (TCState -> TCState) -> m a -> m a
    withTCState (TCState -> TCState -> TCState
    forall a b. a -> b -> a
    const TCState
    s') (i -> m a
    f i
    i)

    instance MonadAddContext ReduceM where
      withFreshName :: forall a. Range -> String -> (Name -> ReduceM a) -> ReduceM a
    withFreshName Range
    r String
    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 -> String -> Name
    forall a. MkName a => Range -> NameId -> a -> Name
    mkName Range
    r NameId
    i String
    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. Name -> Term -> Dom Type -> ReduceM a -> ReduceM a
    addLetBinding' = Name -> Term -> Dom Type -> ReduceM a -> ReduceM a
    forall (m :: * -> *) a.
    (ReadTCState m, MonadTCEnv m) =>
    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 (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\TCEnv
    e -> TCEnv
    e { envContext :: Context
    envContext = Context -> Context
    f (Context -> Context) -> Context -> Context
    forall a b. (a -> b) -> a -> b
    $ TCEnv -> Context
    envContext TCEnv
    e
                         , envCurrentCheckpoint :: CheckpointId
    envCurrentCheckpoint = CheckpointId
    chkpt
                         , envCheckpoints :: Map CheckpointId Substitution
    envCheckpoints = CheckpointId
    -> Substitution
    -> Map CheckpointId Substitution
    -> Map CheckpointId Substitution
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert CheckpointId
    chkpt Substitution
    forall a. Substitution' a
    IdS (Map CheckpointId Substitution -> Map CheckpointId Substitution)
    -> Map CheckpointId Substitution -> Map CheckpointId Substitution
    forall a b. (a -> b) -> a -> b
    $
                                              (Substitution -> Substitution)
    -> Map CheckpointId Substitution -> Map CheckpointId Substitution
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Substitution' (SubstArg Substitution)
    -> Substitution -> Substitution
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution
    Substitution' (SubstArg Substitution)
    rho) (TCEnv -> Map CheckpointId Substitution
    envCheckpoints TCEnv
    e)
                         }) ReduceM a
    ret
            -- let-bindings keep track of own their context

    instance MonadDebug ReduceM where

      traceDebugMessage :: forall a.
    String -> VerboseLevel -> String -> ReduceM a -> ReduceM a
    traceDebugMessage String
    k VerboseLevel
    n String
    s ReduceM a
    cont = do
        ReduceEnv TCEnv
    env TCState
    st <- ReduceM ReduceEnv
    askR
        IO (ReduceM a) -> ReduceM a
    forall a. IO a -> a
    unsafePerformIO (IO (ReduceM a) -> ReduceM a) -> IO (ReduceM a) -> ReduceM a
    forall a b. (a -> b) -> a -> b
    $ do
          ((), TCState)
    _ <- TCEnv -> TCState -> TCMT IO () -> IO ((), TCState)
    forall (m :: * -> *) a.
    MonadIO m =>
    TCEnv -> TCState -> TCMT m a -> m (a, TCState)
    runTCM TCEnv
    env TCState
    st (TCMT IO () -> IO ((), TCState)) -> TCMT IO () -> IO ((), TCState)
    forall a b. (a -> b) -> a -> b
    $ String -> VerboseLevel -> String -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> VerboseLevel -> String -> m ()
    displayDebugMessage String
    k VerboseLevel
    n String
    s
          ReduceM a -> IO (ReduceM a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ReduceM a -> IO (ReduceM a)) -> ReduceM a -> IO (ReduceM a)
    forall a b. (a -> b) -> a -> b
    $ ReduceM a
    cont

      formatDebugMessage :: String -> VerboseLevel -> TCM Doc -> ReduceM String
    formatDebugMessage String
    k VerboseLevel
    n TCM Doc
    d = do
        ReduceEnv TCEnv
    env TCState
    st <- ReduceM ReduceEnv
    askR
        IO (ReduceM String) -> ReduceM String
    forall a. IO a -> a
    unsafePerformIO (IO (ReduceM String) -> ReduceM String)
    -> IO (ReduceM String) -> ReduceM String
    forall a b. (a -> b) -> a -> b
    $ do
          (String
    s , TCState
    _) <- TCEnv -> TCState -> TCMT IO String -> IO (String, TCState)
    forall (m :: * -> *) a.
    MonadIO m =>
    TCEnv -> TCState -> TCMT m a -> m (a, TCState)
    runTCM TCEnv
    env TCState
    st (TCMT IO String -> IO (String, TCState))
    -> TCMT IO String -> IO (String, TCState)
    forall a b. (a -> b) -> a -> b
    $ String -> VerboseLevel -> TCM Doc -> TCMT IO String
    forall (m :: * -> *).
    MonadDebug m =>
    String -> VerboseLevel -> TCM Doc -> m String
    formatDebugMessage String
    k VerboseLevel
    n TCM Doc
    d
          ReduceM String -> IO (ReduceM String)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ReduceM String -> IO (ReduceM String))
    -> ReduceM String -> IO (ReduceM String)
    forall a b. (a -> b) -> a -> b
    $ String -> ReduceM String
    forall (m :: * -> *) a. Monad m => a -> m a
    return String
    s

      verboseBracket :: forall a.
    String -> VerboseLevel -> String -> ReduceM a -> ReduceM a
    verboseBracket String
    k VerboseLevel
    n String
    s = String
    -> VerboseLevel
    -> (ReduceM a -> ReduceM a)
    -> ReduceM a
    -> ReduceM a
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> VerboseLevel -> (m a -> m a) -> m a -> m a
    applyWhenVerboseS String
    k VerboseLevel
    n ((ReduceM a -> ReduceM a) -> ReduceM a -> ReduceM a)
    -> (ReduceM a -> ReduceM a) -> ReduceM a -> ReduceM a
    forall a b. (a -> b) -> a -> b
    $
        ReduceM () -> (() -> ReduceM ()) -> ReduceM a -> ReduceM a
    forall (m :: * -> *) a b.
    Monad m =>
    m a -> (a -> m ()) -> m b -> m b
    bracket_ (String -> VerboseLevel -> String -> ReduceM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> VerboseLevel -> String -> m ()
    openVerboseBracket String
    k VerboseLevel
    n String
    s) (ReduceM () -> () -> ReduceM ()
    forall a b. a -> b -> a
    const (ReduceM () -> () -> ReduceM ()) -> ReduceM () -> () -> ReduceM ()
    forall a b. (a -> b) -> a -> b
    $ String -> VerboseLevel -> ReduceM ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> VerboseLevel -> m ()
    closeVerboseBracket String
    k VerboseLevel
    n)

      getVerbosity :: ReduceM Verbosity
    getVerbosity     = ReduceM Verbosity
    forall (m :: * -> *). HasOptions m => m Verbosity
    defaultGetVerbosity
      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 TCEnv
    env TCState
    st <- ReduceM ReduceEnv
    askR
        TCState -> TCEnv -> QName -> ReduceM (Either SigError Definition)
    forall (m :: * -> *).
    (HasOptions m, MonadDebug m, MonadTCEnv m) =>
    TCState -> TCEnv -> QName -> m (Either SigError Definition)
    defaultGetConstInfo TCState
    st TCEnv
    env QName
    q

    instance PureTCM ReduceM where