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

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

import Prelude hiding (null)

import Control.Monad.Reader

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

import System.IO.Unsafe

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad hiding
  ( enterClosure, isInstantiatedMeta, verboseS, typeOfConst, lookupMeta, lookupMeta', constructorForm )
import Agda.TypeChecking.Substitute

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

import Agda.Utils.Impossible

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 :: 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 :: 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
forall p. p -> TCEnv
inEnv TCState -> TCState
inState) (a -> ReduceM b
f a
x)
    where
    inEnv :: p -> TCEnv
inEnv   p
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 :: (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 :: 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 :: 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' :: Name -> Term -> Dom Type -> ReduceM a -> ReduceM a
addLetBinding' = Name -> Term -> Dom Type -> ReduceM a -> ReduceM a
forall (m :: * -> *) a.
MonadTCEnv m =>
Name -> Term -> Dom Type -> m a -> m a
defaultAddLetBinding'

  updateContext :: 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 -> Substitution -> Substitution
forall t a. Subst t a => Substitution' t -> a -> a
applySubst 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 :: 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 :: 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)

instance HasConstInfo ReduceM where
  getRewriteRulesFor :: QName -> ReduceM RewriteRules
getRewriteRulesFor = ReduceM TCState -> QName -> ReduceM RewriteRules
forall (m :: * -> *).
Monad m =>
m TCState -> QName -> m RewriteRules
defaultGetRewriteRulesFor ReduceM TCState
forall (m :: * -> *). ReadTCState m => m TCState
getTCState
  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