{-# 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
import Agda.Utils.Monad
import Agda.Syntax.Common.Pretty ()
instance HasBuiltins ReduceM where
getBuiltinThing :: SomeBuiltin -> ReduceM (Maybe (Builtin PrimFun))
getBuiltinThing SomeBuiltin
b =
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionMaybeWith forall a. Builtin a -> Builtin a -> Builtin a
unionBuiltin)
(forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SomeBuiltin
b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR Lens' TCState (BuiltinThings PrimFun)
stLocalBuiltins)
(forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SomeBuiltin
b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR Lens' TCState (BuiltinThings PrimFun)
stImportedBuiltins)
constructorForm :: HasBuiltins m => Term -> m Term
constructorForm :: forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm Term
v = do
Maybe Term
mz <- forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinZero
Maybe Term
ms <- forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinSuc
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe Term
v forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
Applicative m =>
m Term -> m Term -> Term -> m Term
constructorForm' Maybe Term
mz Maybe Term
ms Term
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 forall o i. o -> Lens' o i -> i
^. forall b a. LensClosure b a => Lens' b (Closure a)
lensClosure = \case
a -> ReduceM b
f -> 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 =
forall o i. Lens' o i -> LensSet o i
set Lens' TCState ScopeInfo
stScope ScopeInfo
scope forall a b. (a -> b) -> a -> b
$ forall o i. Lens' o i -> LensSet o i
set 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
TCState
s <- forall (m :: * -> *). ReadTCState m => m TCState
getTCState
let (i
i, TCState
s') = forall i. HasFresh i => TCState -> (i, TCState)
nextFresh TCState
s
forall (m :: * -> *) a.
ReadTCState m =>
(TCState -> TCState) -> m a -> m a
withTCState (forall a b. a -> b -> a
const TCState
s') (i -> m a
f i
i)
instance MonadAddContext ReduceM where
withFreshName :: forall a. Range -> ArgName -> (Name -> ReduceM a) -> ReduceM a
withFreshName Range
r ArgName
s Name -> ReduceM a
k = forall (m :: * -> *) i a.
(ReadTCState m, HasFresh i) =>
(i -> m a) -> m a
withFreshR forall a b. (a -> b) -> a -> b
$ \NameId
i -> Name -> ReduceM a
k (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 = 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' = 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 = forall (m :: * -> *) i a.
(ReadTCState m, HasFresh i) =>
(i -> m a) -> m a
withFreshR forall a b. (a -> b) -> a -> b
$ \ CheckpointId
chkpt ->
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\TCEnv
e -> TCEnv
e { envContext :: Context
envContext = Context -> Context
f forall a b. (a -> b) -> a -> b
$ TCEnv -> Context
envContext TCEnv
e
, envCurrentCheckpoint :: CheckpointId
envCurrentCheckpoint = CheckpointId
chkpt
, envCheckpoints :: Map CheckpointId Substitution
envCheckpoints = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert CheckpointId
chkpt forall a. Substitution' a
IdS forall a b. (a -> b) -> a -> b
$
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
rho) (TCEnv -> Map CheckpointId Substitution
envCheckpoints TCEnv
e)
}) ReduceM a
ret
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 TCEnv
env TCState
st Maybe (MetaId -> ReduceM Bool)
_ <- ReduceM ReduceEnv
askR
forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ do
((), TCState)
_ <- forall (m :: * -> *) a.
MonadIO m =>
TCEnv -> TCState -> TCMT m a -> m (a, TCState)
runTCM TCEnv
env TCState
st forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> ArgName -> m ()
displayDebugMessage ArgName
k VerboseLevel
n ArgName
s
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ReduceM a
cont
formatDebugMessage :: ArgName -> VerboseLevel -> TCM Doc -> ReduceM ArgName
formatDebugMessage ArgName
k VerboseLevel
n TCM Doc
d = do
ReduceEnv TCEnv
env TCState
st Maybe (MetaId -> ReduceM Bool)
_ <- ReduceM ReduceEnv
askR
forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ do
(ArgName
s , TCState
_) <- forall (m :: * -> *) a.
MonadIO m =>
TCEnv -> TCState -> TCMT m a -> m (a, TCState)
runTCM TCEnv
env TCState
st forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCM Doc -> m ArgName
formatDebugMessage ArgName
k VerboseLevel
n TCM Doc
d
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ArgName
s
verboseBracket :: forall a.
ArgName -> VerboseLevel -> ArgName -> ReduceM a -> ReduceM a
verboseBracket ArgName
k VerboseLevel
n ArgName
s = forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> VerboseLevel -> (m a -> m a) -> m a -> m a
applyWhenVerboseS ArgName
k VerboseLevel
n forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ (forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> ArgName -> m ()
openVerboseBracket ArgName
k VerboseLevel
n ArgName
s) (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> m ()
closeVerboseBracket ArgName
k VerboseLevel
n)
getVerbosity :: ReduceM Verbosity
getVerbosity = forall (m :: * -> *). HasOptions m => m Verbosity
defaultGetVerbosity
getProfileOptions :: ReduceM ProfileOptions
getProfileOptions = forall (m :: * -> *). HasOptions m => m ProfileOptions
defaultGetProfileOptions
isDebugPrinting :: ReduceM Bool
isDebugPrinting = forall (m :: * -> *). MonadTCEnv m => m Bool
defaultIsDebugPrinting
nowDebugPrinting :: forall a. ReduceM a -> ReduceM a
nowDebugPrinting = forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
defaultNowDebugPrinting
instance HasConstInfo ReduceM where
getRewriteRulesFor :: QName -> ReduceM RewriteRules
getRewriteRulesFor = 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 Maybe (MetaId -> ReduceM Bool)
_ <- ReduceM ReduceEnv
askR
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