-- | Lenses for 'TCState' and more.

module Agda.TypeChecking.Monad.State where

import qualified Control.Exception as E

import Control.DeepSeq           (rnf)
import Control.Exception         (evaluate)
import Control.Monad.Trans       (MonadIO, liftIO)
import Control.Monad.Trans.Maybe (MaybeT(MaybeT), runMaybeT)

import Data.Maybe
import qualified Data.HashMap.Strict as HMap
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set

import Agda.Benchmarking

import Agda.Compiler.Backend.Base (pattern Backend, backendName, mayEraseType)

import Agda.Interaction.Response
  (InteractionOutputCallback, Response)

import Agda.Syntax.Common
import Agda.Syntax.Scope.Base
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Abstract (PatternSynDefn, PatternSynDefns)
import Agda.Syntax.Abstract.PatternSynonyms
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Internal
import Agda.Syntax.Position
import Agda.Syntax.TopLevelModuleName

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Warnings

import Agda.TypeChecking.Monad.Debug (reportSDoc, reportSLn, verboseS)
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.CompiledClause

import qualified Agda.Utils.BiMap as BiMap
import Agda.Utils.Lens
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Monad
import Agda.Syntax.Common.Pretty
import Agda.Utils.Tuple

import Agda.Utils.Impossible

-- | Resets the non-persistent part of the type checking state.

resetState :: TCM ()
resetState :: TCM ()
resetState = do
    pers <- (TCState -> PersistentTCState) -> TCMT IO PersistentTCState
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC TCState -> PersistentTCState
stPersistentState
    putTC $ initState { stPersistentState = pers }

-- | Resets all of the type checking state.
--
--   Keep only 'Benchmark' and backend information.

resetAllState :: TCM ()
resetAllState :: TCM ()
resetAllState = do
    b <- TCM Benchmark
getBenchmark
    backends <- useTC stBackends
    putTC $ updatePersistentState (\ PersistentTCState
s -> PersistentTCState
s { stBenchmark = b }) initState
    stBackends `setTCLens` backends
-- resetAllState = putTC initState

-- | Restore 'TCState' after performing subcomputation.
--
--   In contrast to 'Agda.Utils.Monad.localState', the 'Benchmark'
--   info from the subcomputation is saved.
localTCState :: TCM a -> TCM a
localTCState :: forall a. TCM a -> TCM a
localTCState = TCMT IO TCState -> (TCState -> TCM ()) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC (\ TCState
s -> do
   b <- TCM Benchmark
getBenchmark
   putTC s
   modifyBenchmark $ const b)

-- | Same as 'localTCState' but also returns the state in which we were just
--   before reverting it.
localTCStateSaving :: TCM a -> TCM (a, TCState)
localTCStateSaving :: forall a. TCM a -> TCM (a, TCState)
localTCStateSaving TCM a
compute = do
  oldState <- TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
  result <- compute
  newState <- getTC
  do
    b <- getBenchmark
    putTC oldState
    modifyBenchmark $ const b
  return (result, newState)

-- | Same as 'localTCState' but keep all warnings.
localTCStateSavingWarnings :: TCM a -> TCM a
localTCStateSavingWarnings :: forall a. TCM a -> TCM a
localTCStateSavingWarnings TCM a
compute = do
  (result, newState) <- TCM a -> TCM (a, TCState)
forall a. TCM a -> TCM (a, TCState)
localTCStateSaving TCM a
compute
  modifyTC $ over stTCWarnings $ const $ newState ^. stTCWarnings
  return result

data SpeculateResult = SpeculateAbort | SpeculateCommit

-- | Allow rolling back the state changes of a TCM computation.
speculateTCState :: TCM (a, SpeculateResult) -> TCM a
speculateTCState :: forall a. TCM (a, SpeculateResult) -> TCM a
speculateTCState TCM (a, SpeculateResult)
m = do
  ((x, res), newState) <- TCM (a, SpeculateResult) -> TCM ((a, SpeculateResult), TCState)
forall a. TCM a -> TCM (a, TCState)
localTCStateSaving TCM (a, SpeculateResult)
m
  case res of
    SpeculateResult
SpeculateAbort  -> a -> TCMT IO a
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
    SpeculateResult
SpeculateCommit -> a
x a -> TCM () -> TCMT IO a
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
newState

speculateTCState_ :: TCM SpeculateResult -> TCM ()
speculateTCState_ :: TCM SpeculateResult -> TCM ()
speculateTCState_ TCM SpeculateResult
m = TCM () -> TCM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM ((), SpeculateResult) -> TCM ()
forall a. TCM (a, SpeculateResult) -> TCM a
speculateTCState (TCM ((), SpeculateResult) -> TCM ())
-> TCM ((), SpeculateResult) -> TCM ()
forall a b. (a -> b) -> a -> b
$ ((),) (SpeculateResult -> ((), SpeculateResult))
-> TCM SpeculateResult -> TCM ((), SpeculateResult)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM SpeculateResult
m

-- | A fresh TCM instance.
--
-- The computation is run in a fresh state, with the exception that
-- the persistent state is preserved. If the computation changes the
-- state, then these changes are ignored, except for changes to the
-- persistent state. (Changes to the persistent state are also ignored
-- if errors other than type errors or IO exceptions are encountered.)

freshTCM :: TCM a -> TCM (Either TCErr a)
freshTCM :: forall a. TCM a -> TCM (Either TCErr a)
freshTCM TCM a
m = do
  ps <- Lens' TCState PersistentTCState -> TCMT IO PersistentTCState
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (PersistentTCState -> f PersistentTCState) -> TCState -> f TCState
Lens' TCState PersistentTCState
lensPersistentState
  let s = Lens' TCState PersistentTCState
-> LensSet TCState PersistentTCState
forall o i. Lens' o i -> LensSet o i
set (PersistentTCState -> f PersistentTCState) -> TCState -> f TCState
Lens' TCState PersistentTCState
lensPersistentState PersistentTCState
ps TCState
initState
  r <- liftIO $ (Right <$> runTCM initEnv s m) `E.catch` (return . Left)
  case r of
    Right (a
a, TCState
s) -> do
      Lens' TCState PersistentTCState -> PersistentTCState -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
setTCLens (PersistentTCState -> f PersistentTCState) -> TCState -> f TCState
Lens' TCState PersistentTCState
lensPersistentState (PersistentTCState -> TCM ()) -> PersistentTCState -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCState
s TCState -> Lens' TCState PersistentTCState -> PersistentTCState
forall o i. o -> Lens' o i -> i
^. (PersistentTCState -> f PersistentTCState) -> TCState -> f TCState
Lens' TCState PersistentTCState
lensPersistentState
      Either TCErr a -> TCMT IO (Either TCErr a)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either TCErr a -> TCMT IO (Either TCErr a))
-> Either TCErr a -> TCMT IO (Either TCErr a)
forall a b. (a -> b) -> a -> b
$ a -> Either TCErr a
forall a b. b -> Either a b
Right a
a
    Left TCErr
err -> do
      case TCErr
err of
        TypeError { tcErrState :: TCErr -> TCState
tcErrState = TCState
s } ->
          Lens' TCState PersistentTCState -> PersistentTCState -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
setTCLens (PersistentTCState -> f PersistentTCState) -> TCState -> f TCState
Lens' TCState PersistentTCState
lensPersistentState (PersistentTCState -> TCM ()) -> PersistentTCState -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCState
s TCState -> Lens' TCState PersistentTCState -> PersistentTCState
forall o i. o -> Lens' o i -> i
^. (PersistentTCState -> f PersistentTCState) -> TCState -> f TCState
Lens' TCState PersistentTCState
lensPersistentState
        IOException (Just TCState
s) Range
_ IOException
_ ->
          Lens' TCState PersistentTCState -> PersistentTCState -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
setTCLens (PersistentTCState -> f PersistentTCState) -> TCState -> f TCState
Lens' TCState PersistentTCState
lensPersistentState (PersistentTCState -> TCM ()) -> PersistentTCState -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCState
s TCState -> Lens' TCState PersistentTCState -> PersistentTCState
forall o i. o -> Lens' o i -> i
^. (PersistentTCState -> f PersistentTCState) -> TCState -> f TCState
Lens' TCState PersistentTCState
lensPersistentState
        TCErr
_ -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Either TCErr a -> TCMT IO (Either TCErr a)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either TCErr a -> TCMT IO (Either TCErr a))
-> Either TCErr a -> TCMT IO (Either TCErr a)
forall a b. (a -> b) -> a -> b
$ TCErr -> Either TCErr a
forall a b. a -> Either a b
Left TCErr
err

---------------------------------------------------------------------------
-- * Lens for persistent states and its fields
---------------------------------------------------------------------------

updatePersistentState
  :: (PersistentTCState -> PersistentTCState) -> (TCState -> TCState)
updatePersistentState :: (PersistentTCState -> PersistentTCState) -> TCState -> TCState
updatePersistentState PersistentTCState -> PersistentTCState
f TCState
s = TCState
s { stPersistentState = f (stPersistentState s) }

modifyPersistentState :: (PersistentTCState -> PersistentTCState) -> TCM ()
modifyPersistentState :: (PersistentTCState -> PersistentTCState) -> TCM ()
modifyPersistentState = (TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> TCM ())
-> ((PersistentTCState -> PersistentTCState) -> TCState -> TCState)
-> (PersistentTCState -> PersistentTCState)
-> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PersistentTCState -> PersistentTCState) -> TCState -> TCState
updatePersistentState

-- | Lens for 'stAccumStatistics'.

lensAccumStatisticsP :: Lens' PersistentTCState Statistics
lensAccumStatisticsP :: Lens' PersistentTCState Statistics
lensAccumStatisticsP Statistics -> f Statistics
f PersistentTCState
s = Statistics -> f Statistics
f (PersistentTCState -> Statistics
stAccumStatistics PersistentTCState
s) f Statistics
-> (Statistics -> PersistentTCState) -> f PersistentTCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Statistics
a ->
  PersistentTCState
s { stAccumStatistics = a }

lensAccumStatistics :: Lens' TCState Statistics
lensAccumStatistics :: Lens' TCState Statistics
lensAccumStatistics =  (PersistentTCState -> f PersistentTCState) -> TCState -> f TCState
Lens' TCState PersistentTCState
lensPersistentState ((PersistentTCState -> f PersistentTCState)
 -> TCState -> f TCState)
-> ((Statistics -> f Statistics)
    -> PersistentTCState -> f PersistentTCState)
-> (Statistics -> f Statistics)
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Statistics -> f Statistics)
-> PersistentTCState -> f PersistentTCState
Lens' PersistentTCState Statistics
lensAccumStatisticsP

---------------------------------------------------------------------------
-- * Scope
---------------------------------------------------------------------------

{-# INLINE getScope #-}
-- | Get the current scope.
getScope :: ReadTCState m => m ScopeInfo
getScope :: forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope = Lens' TCState ScopeInfo -> m ScopeInfo
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (ScopeInfo -> f ScopeInfo) -> TCState -> f TCState
Lens' TCState ScopeInfo
stScope

{-# INLINE setScope #-}
-- | Set the current scope.
setScope :: ScopeInfo -> TCM ()
setScope :: ScopeInfo -> TCM ()
setScope ScopeInfo
scope = (ScopeInfo -> ScopeInfo) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(ScopeInfo -> ScopeInfo) -> m ()
modifyScope (ScopeInfo -> ScopeInfo -> ScopeInfo
forall a b. a -> b -> a
const ScopeInfo
scope)

{-# INLINE modifyScope_ #-}
-- | Modify the current scope without updating the inverse maps.
modifyScope_ :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m ()
modifyScope_ :: forall (m :: * -> *).
MonadTCState m =>
(ScopeInfo -> ScopeInfo) -> m ()
modifyScope_ ScopeInfo -> ScopeInfo
f = (ScopeInfo -> f ScopeInfo) -> TCState -> f TCState
Lens' TCState ScopeInfo
stScope Lens' TCState ScopeInfo -> (ScopeInfo -> ScopeInfo) -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` ScopeInfo -> ScopeInfo
f

{-# INLINE modifyScope #-}
-- | Modify the current scope.
modifyScope :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m ()
modifyScope :: forall (m :: * -> *).
MonadTCState m =>
(ScopeInfo -> ScopeInfo) -> m ()
modifyScope ScopeInfo -> ScopeInfo
f = (ScopeInfo -> ScopeInfo) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(ScopeInfo -> ScopeInfo) -> m ()
modifyScope_ (ScopeInfo -> ScopeInfo
recomputeInverseScopeMaps (ScopeInfo -> ScopeInfo)
-> (ScopeInfo -> ScopeInfo) -> ScopeInfo -> ScopeInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeInfo -> ScopeInfo
f)

{-# INLINE useScope #-}
-- | Get a part of the current scope.
useScope :: ReadTCState m => Lens' ScopeInfo a -> m a
useScope :: forall (m :: * -> *) a. ReadTCState m => Lens' ScopeInfo a -> m a
useScope Lens' ScopeInfo a
l = Lens' TCState a -> m a
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Lens' TCState a -> m a) -> Lens' TCState a -> m a
forall a b. (a -> b) -> a -> b
$ (ScopeInfo -> f ScopeInfo) -> TCState -> f TCState
Lens' TCState ScopeInfo
stScope ((ScopeInfo -> f ScopeInfo) -> TCState -> f TCState)
-> ((a -> f a) -> ScopeInfo -> f ScopeInfo)
-> (a -> f a)
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f a) -> ScopeInfo -> f ScopeInfo
Lens' ScopeInfo a
l

{-# INLINE locallyScope #-}
-- | Run a computation in a modified scope.
locallyScope :: ReadTCState m => Lens' ScopeInfo a -> (a -> a) -> m b -> m b
locallyScope :: forall (m :: * -> *) a b.
ReadTCState m =>
Lens' ScopeInfo a -> (a -> a) -> m b -> m b
locallyScope Lens' ScopeInfo a
l = Lens' TCState a -> (a -> a) -> m b -> m b
forall a b. Lens' TCState a -> (a -> a) -> m b -> m b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState (Lens' TCState a -> (a -> a) -> m b -> m b)
-> Lens' TCState a -> (a -> a) -> m b -> m b
forall a b. (a -> b) -> a -> b
$ (ScopeInfo -> f ScopeInfo) -> TCState -> f TCState
Lens' TCState ScopeInfo
stScope ((ScopeInfo -> f ScopeInfo) -> TCState -> f TCState)
-> ((a -> f a) -> ScopeInfo -> f ScopeInfo)
-> (a -> f a)
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f a) -> ScopeInfo -> f ScopeInfo
Lens' ScopeInfo a
l

{-# INLINE withScope #-}
-- | Run a computation in a local scope.
withScope :: ReadTCState m => ScopeInfo -> m a -> m (a, ScopeInfo)
withScope :: forall (m :: * -> *) a.
ReadTCState m =>
ScopeInfo -> m a -> m (a, ScopeInfo)
withScope ScopeInfo
s m a
m = Lens' TCState ScopeInfo
-> (ScopeInfo -> ScopeInfo) -> m (a, ScopeInfo) -> m (a, ScopeInfo)
forall a b. Lens' TCState a -> (a -> a) -> m b -> m b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState (ScopeInfo -> f ScopeInfo) -> TCState -> f TCState
Lens' TCState ScopeInfo
stScope (ScopeInfo -> ScopeInfo
recomputeInverseScopeMaps (ScopeInfo -> ScopeInfo)
-> (ScopeInfo -> ScopeInfo) -> ScopeInfo -> ScopeInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeInfo -> ScopeInfo -> ScopeInfo
forall a b. a -> b -> a
const ScopeInfo
s) (m (a, ScopeInfo) -> m (a, ScopeInfo))
-> m (a, ScopeInfo) -> m (a, ScopeInfo)
forall a b. (a -> b) -> a -> b
$ (,) (a -> ScopeInfo -> (a, ScopeInfo))
-> m a -> m (ScopeInfo -> (a, ScopeInfo))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a
m m (ScopeInfo -> (a, ScopeInfo)) -> m ScopeInfo -> m (a, ScopeInfo)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope

{-# INLINE withScope_ #-}
-- | Same as 'withScope', but discard the scope from the computation.
withScope_ :: ReadTCState m => ScopeInfo -> m a -> m a
withScope_ :: forall (m :: * -> *) a. ReadTCState m => ScopeInfo -> m a -> m a
withScope_ ScopeInfo
s m a
m = (a, ScopeInfo) -> a
forall a b. (a, b) -> a
fst ((a, ScopeInfo) -> a) -> m (a, ScopeInfo) -> m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ScopeInfo -> m a -> m (a, ScopeInfo)
forall (m :: * -> *) a.
ReadTCState m =>
ScopeInfo -> m a -> m (a, ScopeInfo)
withScope ScopeInfo
s m a
m

-- | Discard any changes to the scope by a computation.
localScope :: TCM a -> TCM a
localScope :: forall a. TCM a -> TCM a
localScope TCM a
m = do
  scope <- TCMT IO ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  x <- m
  setScope scope
  return x

-- | Scope error.
notInScopeError :: C.QName -> TCM a
notInScopeError :: forall a. QName -> TCM a
notInScopeError QName
x = do
  [Char] -> Int -> [Char] -> TCM ()
printScope [Char]
"unbound" Int
25 [Char]
""
  TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ QName -> TypeError
NotInScope QName
x

notInScopeWarning :: C.QName -> TCM ()
notInScopeWarning :: QName -> TCM ()
notInScopeWarning QName
x = do
  [Char] -> Int -> [Char] -> TCM ()
printScope [Char]
"unbound" Int
25 [Char]
""
  Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> Warning
NotInScopeW QName
x

-- | Debug print the scope.
printScope :: String -> Int -> String -> TCM ()
printScope :: [Char] -> Int -> [Char] -> TCM ()
printScope [Char]
tag Int
v [Char]
s = [Char] -> Int -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS ([Char]
"scope." [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
tag) Int
v (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
  scope <- TCMT IO ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  reportSDoc ("scope." ++ tag) v $ return $ vcat [ text s, pretty scope ]

---------------------------------------------------------------------------
-- * Signature
---------------------------------------------------------------------------

-- ** Lens for 'stSignature' and 'stImports'

{-# INLINE modifySignature  #-}
modifySignature :: MonadTCState m => (Signature -> Signature) -> m ()
modifySignature :: forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature Signature -> Signature
f = (Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stSignature Lens' TCState Signature -> (Signature -> Signature) -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` Signature -> Signature
f

{-# INLINE modifyImportedSignature #-}
modifyImportedSignature :: MonadTCState m => (Signature -> Signature) -> m ()
modifyImportedSignature :: forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifyImportedSignature Signature -> Signature
f = (Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stImports Lens' TCState Signature -> (Signature -> Signature) -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` Signature -> Signature
f

{-# INLINE getSignature #-}
getSignature :: ReadTCState m => m Signature
getSignature :: forall (m :: * -> *). ReadTCState m => m Signature
getSignature = Lens' TCState Signature -> m Signature
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stSignature

{-# SPECIALIZE modifyGlobalDefinition :: QName -> (Definition -> Definition) -> TCM () #-}
-- | Update a possibly imported definition. Warning: changes made to imported
--   definitions (during type checking) will not persist outside the current
--   module. This function is currently used to update the compiled
--   representation of a function during compilation.
modifyGlobalDefinition :: MonadTCState m => QName -> (Definition -> Definition) -> m ()
modifyGlobalDefinition :: forall (m :: * -> *).
MonadTCState m =>
QName -> (Definition -> Definition) -> m ()
modifyGlobalDefinition QName
q Definition -> Definition
f = do
  (Signature -> Signature) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature         ((Signature -> Signature) -> m ())
-> (Signature -> Signature) -> m ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q Definition -> Definition
f
  (Signature -> Signature) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifyImportedSignature ((Signature -> Signature) -> m ())
-> (Signature -> Signature) -> m ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q Definition -> Definition
f

{-# INLINE setSignature #-}
setSignature :: MonadTCState m => Signature -> m ()
setSignature :: forall (m :: * -> *). MonadTCState m => Signature -> m ()
setSignature Signature
sig = (Signature -> Signature) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> m ())
-> (Signature -> Signature) -> m ()
forall a b. (a -> b) -> a -> b
$ Signature -> Signature -> Signature
forall a b. a -> b -> a
const Signature
sig

{-# SPECIALIZE withSignature :: Signature -> TCM a -> TCM a #-}
-- | Run some computation in a different signature, restore original signature.
withSignature :: (ReadTCState m, MonadTCState m) => Signature -> m a -> m a
withSignature :: forall (m :: * -> *) a.
(ReadTCState m, MonadTCState m) =>
Signature -> m a -> m a
withSignature Signature
sig m a
m = do
  sig0 <- m Signature
forall (m :: * -> *). ReadTCState m => m Signature
getSignature
  setSignature sig
  r <- m
  setSignature sig0
  return r

-- ** Modifiers for rewrite rules
addRewriteRulesFor :: QName -> RewriteRules -> [QName] -> Signature -> Signature
addRewriteRulesFor :: QName -> RewriteRules -> [QName] -> Signature -> Signature
addRewriteRulesFor QName
f RewriteRules
rews [QName]
matchables =
    Lens' Signature (HashMap QName RewriteRules)
-> LensMap Signature (HashMap QName RewriteRules)
forall o i. Lens' o i -> LensMap o i
over (HashMap QName RewriteRules -> f (HashMap QName RewriteRules))
-> Signature -> f Signature
Lens' Signature (HashMap QName RewriteRules)
sigRewriteRules ((RewriteRules -> RewriteRules -> RewriteRules)
-> QName
-> RewriteRules
-> HashMap QName RewriteRules
-> HashMap QName RewriteRules
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
HMap.insertWith RewriteRules -> RewriteRules -> RewriteRules
forall a. Monoid a => a -> a -> a
mappend QName
f RewriteRules
rews)
  (Signature -> Signature)
-> (Signature -> Signature) -> Signature -> Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
f ((Defn -> Defn) -> Definition -> Definition
updateTheDef Defn -> Defn
setNotInjective (Definition -> Definition)
-> (Definition -> Definition) -> Definition -> Definition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Definition
setCopatternLHS)
  (Signature -> Signature)
-> (Signature -> Signature) -> Signature -> Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName -> [QName] -> Signature -> Signature
setMatchableSymbols QName
f [QName]
matchables)
    where
      setNotInjective :: Defn -> Defn
setNotInjective def :: Defn
def@Function{} = Defn
def { funInv = NotInjective }
      setNotInjective Defn
def            = Defn
def

      setCopatternLHS :: Definition -> Definition
setCopatternLHS =
        (Bool -> Bool) -> Definition -> Definition
updateDefCopatternLHS (Bool -> Bool -> Bool
|| (RewriteRule -> Bool) -> RewriteRules -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any RewriteRule -> Bool
hasProjectionPattern RewriteRules
rews)

      hasProjectionPattern :: RewriteRule -> Bool
hasProjectionPattern RewriteRule
rew = (Elim' NLPat -> Bool) -> [Elim' NLPat] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe (ProjOrigin, QName) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (ProjOrigin, QName) -> Bool)
-> (Elim' NLPat -> Maybe (ProjOrigin, QName))
-> Elim' NLPat
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elim' NLPat -> Maybe (ProjOrigin, QName)
forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
isProjElim) ([Elim' NLPat] -> Bool) -> [Elim' NLPat] -> Bool
forall a b. (a -> b) -> a -> b
$ RewriteRule -> [Elim' NLPat]
rewPats RewriteRule
rew

setMatchableSymbols :: QName -> [QName] -> Signature -> Signature
setMatchableSymbols :: QName -> [QName] -> Signature -> Signature
setMatchableSymbols QName
f [QName]
matchables =
  (QName -> (Signature -> Signature) -> Signature -> Signature)
-> (Signature -> Signature) -> [QName] -> Signature -> Signature
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Signature -> Signature)
-> (Signature -> Signature) -> Signature -> Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) ((Signature -> Signature)
 -> (Signature -> Signature) -> Signature -> Signature)
-> (QName -> Signature -> Signature)
-> QName
-> (Signature -> Signature)
-> Signature
-> Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\QName
g -> QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
g Definition -> Definition
setMatchable)) Signature -> Signature
forall a. a -> a
id [QName]
matchables
    where
      setMatchable :: Definition -> Definition
setMatchable Definition
def = Definition
def { defMatchable = Set.insert f $ defMatchable def }

-- ** 'modify' methods for the signature

modifyRecEta :: MonadTCState m => QName -> (EtaEquality -> EtaEquality) -> m ()
modifyRecEta :: forall (m :: * -> *).
MonadTCState m =>
QName -> (EtaEquality -> EtaEquality) -> m ()
modifyRecEta QName
q EtaEquality -> EtaEquality
f =
  (Signature -> Signature) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> m ())
-> (Signature -> Signature) -> m ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ Lens' Definition EtaEquality -> LensMap Definition EtaEquality
forall o i. Lens' o i -> LensMap o i
over ((Defn -> f Defn) -> Definition -> f Definition
Lens' Definition Defn
lensTheDef ((Defn -> f Defn) -> Definition -> f Definition)
-> ((EtaEquality -> f EtaEquality) -> Defn -> f Defn)
-> (EtaEquality -> f EtaEquality)
-> Definition
-> f Definition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RecordData -> f RecordData) -> Defn -> f Defn
Lens' Defn RecordData
lensRecord ((RecordData -> f RecordData) -> Defn -> f Defn)
-> ((EtaEquality -> f EtaEquality) -> RecordData -> f RecordData)
-> (EtaEquality -> f EtaEquality)
-> Defn
-> f Defn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (EtaEquality -> f EtaEquality) -> RecordData -> f RecordData
Lens' RecordData EtaEquality
lensRecEta) EtaEquality -> EtaEquality
f

-- ** Modifiers for parts of the signature

lookupDefinition :: QName -> Signature -> Maybe Definition
lookupDefinition :: QName -> Signature -> Maybe Definition
lookupDefinition QName
q Signature
sig = QName -> HashMap QName Definition -> Maybe Definition
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
q (HashMap QName Definition -> Maybe Definition)
-> HashMap QName Definition -> Maybe Definition
forall a b. (a -> b) -> a -> b
$ Signature
sig Signature
-> Lens' Signature (HashMap QName Definition)
-> HashMap QName Definition
forall o i. o -> Lens' o i -> i
^. (HashMap QName Definition -> f (HashMap QName Definition))
-> Signature -> f Signature
Lens' Signature (HashMap QName Definition)
sigDefinitions

updateDefinitions :: (Definitions -> Definitions) -> Signature -> Signature
updateDefinitions :: (HashMap QName Definition -> HashMap QName Definition)
-> Signature -> Signature
updateDefinitions = Lens' Signature (HashMap QName Definition)
-> (HashMap QName Definition -> HashMap QName Definition)
-> Signature
-> Signature
forall o i. Lens' o i -> LensMap o i
over (HashMap QName Definition -> f (HashMap QName Definition))
-> Signature -> f Signature
Lens' Signature (HashMap QName Definition)
sigDefinitions

updateDefinition :: QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition :: QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q Definition -> Definition
f = (HashMap QName Definition -> HashMap QName Definition)
-> Signature -> Signature
updateDefinitions ((HashMap QName Definition -> HashMap QName Definition)
 -> Signature -> Signature)
-> (HashMap QName Definition -> HashMap QName Definition)
-> Signature
-> Signature
forall a b. (a -> b) -> a -> b
$ (Definition -> Definition)
-> QName -> HashMap QName Definition -> HashMap QName Definition
forall k v.
(Eq k, Hashable k) =>
(v -> v) -> k -> HashMap k v -> HashMap k v
HMap.adjust Definition -> Definition
f QName
q

updateTheDef :: (Defn -> Defn) -> (Definition -> Definition)
updateTheDef :: (Defn -> Defn) -> Definition -> Definition
updateTheDef Defn -> Defn
f Definition
def = Definition
def { theDef = f (theDef def) }

updateDefType :: (Type -> Type) -> (Definition -> Definition)
updateDefType :: (Type -> Type) -> Definition -> Definition
updateDefType Type -> Type
f Definition
def = Definition
def { defType = f (defType def) }

updateDefArgOccurrences :: ([Occurrence] -> [Occurrence]) -> (Definition -> Definition)
updateDefArgOccurrences :: ([Occurrence] -> [Occurrence]) -> Definition -> Definition
updateDefArgOccurrences [Occurrence] -> [Occurrence]
f Definition
def = Definition
def { defArgOccurrences = f (defArgOccurrences def) }

updateDefPolarity :: ([Polarity] -> [Polarity]) -> (Definition -> Definition)
updateDefPolarity :: ([Polarity] -> [Polarity]) -> Definition -> Definition
updateDefPolarity [Polarity] -> [Polarity]
f Definition
def = Definition
def { defPolarity = f (defPolarity def) }

updateDefCompiledRep :: (CompiledRepresentation -> CompiledRepresentation) -> (Definition -> Definition)
updateDefCompiledRep :: (CompiledRepresentation -> CompiledRepresentation)
-> Definition -> Definition
updateDefCompiledRep CompiledRepresentation -> CompiledRepresentation
f Definition
def = Definition
def { defCompiledRep = f (defCompiledRep def) }

addCompilerPragma :: BackendName -> CompilerPragma -> Definition -> Definition
addCompilerPragma :: BackendName -> CompilerPragma -> Definition -> Definition
addCompilerPragma BackendName
backend CompilerPragma
pragma = (CompiledRepresentation -> CompiledRepresentation)
-> Definition -> Definition
updateDefCompiledRep ((CompiledRepresentation -> CompiledRepresentation)
 -> Definition -> Definition)
-> (CompiledRepresentation -> CompiledRepresentation)
-> Definition
-> Definition
forall a b. (a -> b) -> a -> b
$ ([CompilerPragma] -> [CompilerPragma] -> [CompilerPragma])
-> BackendName
-> [CompilerPragma]
-> CompiledRepresentation
-> CompiledRepresentation
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [CompilerPragma] -> [CompilerPragma] -> [CompilerPragma]
forall a. [a] -> [a] -> [a]
(++) BackendName
backend [CompilerPragma
pragma]

updateFunClauses :: ([Clause] -> [Clause]) -> (Defn -> Defn)
updateFunClauses :: ([Clause] -> [Clause]) -> Defn -> Defn
updateFunClauses [Clause] -> [Clause]
f def :: Defn
def@Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs} = Defn
def { funClauses = f cs }
updateFunClauses [Clause] -> [Clause]
f Defn
_                              = Defn
forall a. HasCallStack => a
__IMPOSSIBLE__

updateCovering :: ([Clause] -> [Clause]) -> (Defn -> Defn)
updateCovering :: ([Clause] -> [Clause]) -> Defn -> Defn
updateCovering [Clause] -> [Clause]
f def :: Defn
def@Function{ funCovering :: Defn -> [Clause]
funCovering = [Clause]
cs} = Defn
def { funCovering = f cs }
updateCovering [Clause] -> [Clause]
f Defn
_                               = Defn
forall a. HasCallStack => a
__IMPOSSIBLE__

updateCompiledClauses :: (Maybe CompiledClauses -> Maybe CompiledClauses) -> (Defn -> Defn)
updateCompiledClauses :: (Maybe CompiledClauses -> Maybe CompiledClauses) -> Defn -> Defn
updateCompiledClauses Maybe CompiledClauses -> Maybe CompiledClauses
f def :: Defn
def@Function{ funCompiled :: Defn -> Maybe CompiledClauses
funCompiled = Maybe CompiledClauses
cc} = Defn
def { funCompiled = f cc }
updateCompiledClauses Maybe CompiledClauses -> Maybe CompiledClauses
f Defn
_                              = Defn
forall a. HasCallStack => a
__IMPOSSIBLE__

updateDefCopatternLHS :: (Bool -> Bool) -> Definition -> Definition
updateDefCopatternLHS :: (Bool -> Bool) -> Definition -> Definition
updateDefCopatternLHS Bool -> Bool
f def :: Definition
def@Defn{ defCopatternLHS :: Definition -> Bool
defCopatternLHS = Bool
b } = Definition
def { defCopatternLHS = f b }

updateDefBlocked :: (Blocked_ -> Blocked_) -> Definition -> Definition
updateDefBlocked :: (Blocked_ -> Blocked_) -> Definition -> Definition
updateDefBlocked Blocked_ -> Blocked_
f def :: Definition
def@Defn{ defBlocked :: Definition -> Blocked_
defBlocked = Blocked_
b } = Definition
def { defBlocked = f b }

---------------------------------------------------------------------------
-- * Top level module
---------------------------------------------------------------------------

-- | Tries to convert a raw top-level module name to a top-level
-- module name.

topLevelModuleName :: RawTopLevelModuleName -> TCM TopLevelModuleName
topLevelModuleName :: RawTopLevelModuleName -> TCM TopLevelModuleName
topLevelModuleName RawTopLevelModuleName
raw = do
  hash <- RawTopLevelModuleName
-> BiMap RawTopLevelModuleName ModuleNameHash
-> Maybe ModuleNameHash
forall k v. Ord k => k -> BiMap k v -> Maybe v
BiMap.lookup RawTopLevelModuleName
raw (BiMap RawTopLevelModuleName ModuleNameHash
 -> Maybe ModuleNameHash)
-> TCMT IO (BiMap RawTopLevelModuleName ModuleNameHash)
-> TCMT IO (Maybe ModuleNameHash)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
-> TCMT IO (BiMap RawTopLevelModuleName ModuleNameHash)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (BiMap RawTopLevelModuleName ModuleNameHash
 -> f (BiMap RawTopLevelModuleName ModuleNameHash))
-> TCState -> f TCState
Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
stTopLevelModuleNames
  case hash of
    Just ModuleNameHash
hash -> TopLevelModuleName -> TCM TopLevelModuleName
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (RawTopLevelModuleName -> ModuleNameHash -> TopLevelModuleName
unsafeTopLevelModuleName RawTopLevelModuleName
raw ModuleNameHash
hash)
    Maybe ModuleNameHash
Nothing   -> do
      let hash :: ModuleNameHash
hash = RawTopLevelModuleName -> ModuleNameHash
hashRawTopLevelModuleName RawTopLevelModuleName
raw
      Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when (ModuleNameHash
hash ModuleNameHash -> ModuleNameHash -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleNameHash
noModuleNameHash) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ RawTopLevelModuleName -> Maybe RawTopLevelModuleName -> TypeError
ModuleNameHashCollision RawTopLevelModuleName
raw Maybe RawTopLevelModuleName
forall a. Maybe a
Nothing
      raw' <- Tag ModuleNameHash
-> BiMap RawTopLevelModuleName ModuleNameHash
-> Maybe RawTopLevelModuleName
forall v k. Ord (Tag v) => Tag v -> BiMap k v -> Maybe k
BiMap.invLookup Tag ModuleNameHash
ModuleNameHash
hash (BiMap RawTopLevelModuleName ModuleNameHash
 -> Maybe RawTopLevelModuleName)
-> TCMT IO (BiMap RawTopLevelModuleName ModuleNameHash)
-> TCMT IO (Maybe RawTopLevelModuleName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
-> TCMT IO (BiMap RawTopLevelModuleName ModuleNameHash)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (BiMap RawTopLevelModuleName ModuleNameHash
 -> f (BiMap RawTopLevelModuleName ModuleNameHash))
-> TCState -> f TCState
Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
stTopLevelModuleNames
      case raw' of
        Just RawTopLevelModuleName
raw' -> TypeError -> TCM TopLevelModuleName
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM TopLevelModuleName)
-> TypeError -> TCM TopLevelModuleName
forall a b. (a -> b) -> a -> b
$ RawTopLevelModuleName -> Maybe RawTopLevelModuleName -> TypeError
ModuleNameHashCollision RawTopLevelModuleName
raw (RawTopLevelModuleName -> Maybe RawTopLevelModuleName
forall a. a -> Maybe a
Just RawTopLevelModuleName
raw')
        Maybe RawTopLevelModuleName
Nothing -> do
          (BiMap RawTopLevelModuleName ModuleNameHash
 -> f (BiMap RawTopLevelModuleName ModuleNameHash))
-> TCState -> f TCState
Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
stTopLevelModuleNames Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
-> (BiMap RawTopLevelModuleName ModuleNameHash
    -> BiMap RawTopLevelModuleName ModuleNameHash)
-> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens'`
            RawTopLevelModuleName
-> ModuleNameHash
-> BiMap RawTopLevelModuleName ModuleNameHash
-> BiMap RawTopLevelModuleName ModuleNameHash
forall k v.
(Ord k, HasTag v, Ord (Tag v)) =>
k -> v -> BiMap k v -> BiMap k v
BiMap.insert (KillRangeT RawTopLevelModuleName
forall a. KillRange a => KillRangeT a
killRange RawTopLevelModuleName
raw) ModuleNameHash
hash
          TopLevelModuleName -> TCM TopLevelModuleName
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (RawTopLevelModuleName -> ModuleNameHash -> TopLevelModuleName
unsafeTopLevelModuleName RawTopLevelModuleName
raw ModuleNameHash
hash)

-- | Set the top-level module. This affects the global module id of freshly
--   generated names.

setTopLevelModule :: TopLevelModuleName -> TCM ()
setTopLevelModule :: TopLevelModuleName -> TCM ()
setTopLevelModule TopLevelModuleName
top = do
  let hash :: ModuleNameHash
hash = TopLevelModuleName -> ModuleNameHash
forall range. TopLevelModuleName' range -> ModuleNameHash
moduleNameId TopLevelModuleName
top
  (NameId -> f NameId) -> TCState -> f TCState
Lens' TCState NameId
stFreshNameId Lens' TCState NameId -> NameId -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens'` Word64 -> ModuleNameHash -> NameId
NameId Word64
0 ModuleNameHash
hash
  (OpaqueId -> f OpaqueId) -> TCState -> f TCState
Lens' TCState OpaqueId
stFreshOpaqueId Lens' TCState OpaqueId -> OpaqueId -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens'` Word64 -> ModuleNameHash -> OpaqueId
OpaqueId Word64
0 ModuleNameHash
hash
  (MetaId -> f MetaId) -> TCState -> f TCState
Lens' TCState MetaId
stFreshMetaId Lens' TCState MetaId -> MetaId -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens'`
    MetaId { metaId :: Word64
metaId     = Word64
0
           , metaModule :: ModuleNameHash
metaModule = ModuleNameHash
hash
           }

-- | The name of the current top-level module, if any.
{-# SPECIALIZE
    currentTopLevelModule :: TCM (Maybe TopLevelModuleName) #-}
{-# SPECIALIZE
    currentTopLevelModule :: ReduceM (Maybe TopLevelModuleName) #-}
currentTopLevelModule ::
  (MonadTCEnv m, ReadTCState m) => m (Maybe TopLevelModuleName)
currentTopLevelModule :: forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
m (Maybe TopLevelModuleName)
currentTopLevelModule = do
  Lens' TCState (Maybe (ModuleName, TopLevelModuleName))
-> m (Maybe (ModuleName, TopLevelModuleName))
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Maybe (ModuleName, TopLevelModuleName)
 -> f (Maybe (ModuleName, TopLevelModuleName)))
-> TCState -> f TCState
Lens' TCState (Maybe (ModuleName, TopLevelModuleName))
stCurrentModule m (Maybe (ModuleName, TopLevelModuleName))
-> (Maybe (ModuleName, TopLevelModuleName)
    -> m (Maybe TopLevelModuleName))
-> m (Maybe TopLevelModuleName)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just (ModuleName
_, TopLevelModuleName
top) -> Maybe TopLevelModuleName -> m (Maybe TopLevelModuleName)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (TopLevelModuleName -> Maybe TopLevelModuleName
forall a. a -> Maybe a
Just TopLevelModuleName
top)
    Maybe (ModuleName, TopLevelModuleName)
Nothing       -> [TopLevelModuleName] -> Maybe TopLevelModuleName
forall a. [a] -> Maybe a
listToMaybe ([TopLevelModuleName] -> Maybe TopLevelModuleName)
-> m [TopLevelModuleName] -> m (Maybe TopLevelModuleName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> [TopLevelModuleName]) -> m [TopLevelModuleName]
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> [TopLevelModuleName]
envImportPath

-- | Use a different top-level module for a computation. Used when generating
--   names for imported modules.
withTopLevelModule :: TopLevelModuleName -> TCM a -> TCM a
withTopLevelModule :: forall a. TopLevelModuleName -> TCM a -> TCM a
withTopLevelModule TopLevelModuleName
x TCM a
m = do
  nextN <- Lens' TCState NameId -> TCMT IO NameId
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (NameId -> f NameId) -> TCState -> f TCState
Lens' TCState NameId
stFreshNameId
  nextM <- useTC stFreshMetaId
  nextO <- useTC stFreshOpaqueId
  setTopLevelModule x
  y <- m
  stFreshMetaId `setTCLens` nextM
  stFreshNameId `setTCLens` nextN
  stFreshOpaqueId `setTCLens` nextO
  return y

{-# SPECIALIZE currentModuleNameHash :: TCM ModuleNameHash #-}
currentModuleNameHash :: ReadTCState m => m ModuleNameHash
currentModuleNameHash :: forall (m :: * -> *). ReadTCState m => m ModuleNameHash
currentModuleNameHash = do
  NameId _ h <- Lens' TCState NameId -> m NameId
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (NameId -> f NameId) -> TCState -> f TCState
Lens' TCState NameId
stFreshNameId
  return h

---------------------------------------------------------------------------
-- * Backends and foreign code
---------------------------------------------------------------------------

-- | Look for a backend of the given name.

lookupBackend :: BackendName -> TCM (Maybe Backend)
lookupBackend :: BackendName -> TCM (Maybe Backend)
lookupBackend BackendName
name = Lens' TCState [Backend] -> TCMT IO [Backend]
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC ([Backend] -> f [Backend]) -> TCState -> f TCState
Lens' TCState [Backend]
stBackends TCMT IO [Backend]
-> ([Backend] -> Maybe Backend) -> TCM (Maybe Backend)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ [Backend]
backends ->
  [Backend] -> Maybe Backend
forall a. [a] -> Maybe a
listToMaybe [ Backend
b | b :: Backend
b@(Backend Backend'_boot Definition (TCMT IO) opts env menv mod def
b') <- [Backend]
backends, Backend'_boot Definition (TCMT IO) opts env menv mod def
-> BackendName
forall definition (tcm :: * -> *) opts env menv mod def.
Backend'_boot definition tcm opts env menv mod def -> BackendName
backendName Backend'_boot Definition (TCMT IO) opts env menv mod def
b' BackendName -> BackendName -> Bool
forall a. Eq a => a -> a -> Bool
== BackendName
name ]

-- | Get the currently active backend (if any).

activeBackend :: TCM (Maybe Backend)
activeBackend :: TCM (Maybe Backend)
activeBackend = MaybeT (TCMT IO) Backend -> TCM (Maybe Backend)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (TCMT IO) Backend -> TCM (Maybe Backend))
-> MaybeT (TCMT IO) Backend -> TCM (Maybe Backend)
forall a b. (a -> b) -> a -> b
$ do
  bname <- TCMT IO (Maybe BackendName) -> MaybeT (TCMT IO) BackendName
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe BackendName) -> MaybeT (TCMT IO) BackendName)
-> TCMT IO (Maybe BackendName) -> MaybeT (TCMT IO) BackendName
forall a b. (a -> b) -> a -> b
$ (TCEnv -> Maybe BackendName) -> TCMT IO (Maybe BackendName)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe BackendName
envActiveBackendName
  lift $ fromMaybe __IMPOSSIBLE__ <$> lookupBackend bname

-- | Ask the active backend whether a type may be erased.
--   See issue #3732.

activeBackendMayEraseType :: QName -> TCM Bool
activeBackendMayEraseType :: QName -> TCM Bool
activeBackendMayEraseType QName
q = do
  Backend b <- Backend -> Maybe Backend -> Backend
forall a. a -> Maybe a -> a
fromMaybe Backend
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Backend -> Backend)
-> TCM (Maybe Backend) -> TCMT IO Backend
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM (Maybe Backend)
activeBackend
  mayEraseType b q

addForeignCode :: BackendName -> String -> TCM ()
addForeignCode :: BackendName -> [Char] -> TCM ()
addForeignCode BackendName
backend [Char]
code = do
  r <- (TCEnv -> Range) -> TCMT IO Range
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Range
envRange  -- can't use TypeChecking.Monad.Trace.getCurrentRange without cycle
  modifyTCLens (stForeignCode . key backend) $
    Just . ForeignCodeStack . (ForeignCode r code :) . maybe [] getForeignCodeStack

---------------------------------------------------------------------------
-- * Interaction output callback
---------------------------------------------------------------------------

getInteractionOutputCallback :: ReadTCState m => m InteractionOutputCallback
getInteractionOutputCallback :: forall (m :: * -> *). ReadTCState m => m InteractionOutputCallback
getInteractionOutputCallback
  = (TCState -> InteractionOutputCallback)
-> m InteractionOutputCallback
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC ((TCState -> InteractionOutputCallback)
 -> m InteractionOutputCallback)
-> (TCState -> InteractionOutputCallback)
-> m InteractionOutputCallback
forall a b. (a -> b) -> a -> b
$ PersistentTCState -> InteractionOutputCallback
stInteractionOutputCallback (PersistentTCState -> InteractionOutputCallback)
-> (TCState -> PersistentTCState)
-> TCState
-> InteractionOutputCallback
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState

appInteractionOutputCallback :: Response -> TCM ()
appInteractionOutputCallback :: InteractionOutputCallback
appInteractionOutputCallback Response
r
  = TCMT IO InteractionOutputCallback
forall (m :: * -> *). ReadTCState m => m InteractionOutputCallback
getInteractionOutputCallback TCMT IO InteractionOutputCallback
-> (InteractionOutputCallback -> TCM ()) -> TCM ()
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ InteractionOutputCallback
cb -> InteractionOutputCallback
cb Response
r

setInteractionOutputCallback :: InteractionOutputCallback -> TCM ()
setInteractionOutputCallback :: InteractionOutputCallback -> TCM ()
setInteractionOutputCallback InteractionOutputCallback
cb
  = (PersistentTCState -> PersistentTCState) -> TCM ()
modifyPersistentState ((PersistentTCState -> PersistentTCState) -> TCM ())
-> (PersistentTCState -> PersistentTCState) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ PersistentTCState
s -> PersistentTCState
s { stInteractionOutputCallback = cb }

---------------------------------------------------------------------------
-- * Pattern synonyms
---------------------------------------------------------------------------

getPatternSyns :: ReadTCState m => m PatternSynDefns
getPatternSyns :: forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getPatternSyns = Lens' TCState PatternSynDefns -> m PatternSynDefns
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (PatternSynDefns -> f PatternSynDefns) -> TCState -> f TCState
Lens' TCState PatternSynDefns
stPatternSyns

setPatternSyns :: PatternSynDefns -> TCM ()
setPatternSyns :: PatternSynDefns -> TCM ()
setPatternSyns PatternSynDefns
m = (PatternSynDefns -> PatternSynDefns) -> TCM ()
modifyPatternSyns (PatternSynDefns -> PatternSynDefns -> PatternSynDefns
forall a b. a -> b -> a
const PatternSynDefns
m)

-- | Lens for 'stPatternSyns'.
modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
modifyPatternSyns PatternSynDefns -> PatternSynDefns
f = (PatternSynDefns -> f PatternSynDefns) -> TCState -> f TCState
Lens' TCState PatternSynDefns
stPatternSyns Lens' TCState PatternSynDefns
-> (PatternSynDefns -> PatternSynDefns) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` PatternSynDefns -> PatternSynDefns
f

getPatternSynImports :: ReadTCState m => m PatternSynDefns
getPatternSynImports :: forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getPatternSynImports = Lens' TCState PatternSynDefns -> m PatternSynDefns
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (PatternSynDefns -> f PatternSynDefns) -> TCState -> f TCState
Lens' TCState PatternSynDefns
stPatternSynImports

-- | Get both local and imported pattern synonyms
getAllPatternSyns :: ReadTCState m => m PatternSynDefns
getAllPatternSyns :: forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getAllPatternSyns = PatternSynDefns -> PatternSynDefns -> PatternSynDefns
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (PatternSynDefns -> PatternSynDefns -> PatternSynDefns)
-> m PatternSynDefns -> m (PatternSynDefns -> PatternSynDefns)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PatternSynDefns
forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getPatternSyns m (PatternSynDefns -> PatternSynDefns)
-> m PatternSynDefns -> m PatternSynDefns
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m PatternSynDefns
forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getPatternSynImports

lookupPatternSyn :: AmbiguousQName -> TCM PatternSynDefn
lookupPatternSyn :: AmbiguousQName -> TCM PatternSynDefn
lookupPatternSyn (AmbQ List1 QName
xs) = do
  defs <- (QName -> TCM PatternSynDefn)
-> List1 QName -> TCMT IO (NonEmpty PatternSynDefn)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NonEmpty a -> f (NonEmpty b)
traverse QName -> TCM PatternSynDefn
lookupSinglePatternSyn List1 QName
xs
  case mergePatternSynDefs defs of
    Just PatternSynDefn
def   -> PatternSynDefn -> TCM PatternSynDefn
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return PatternSynDefn
def
    Maybe PatternSynDefn
Nothing    -> TypeError -> TCM PatternSynDefn
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM PatternSynDefn)
-> TypeError -> TCM PatternSynDefn
forall a b. (a -> b) -> a -> b
$ List1 (QName, PatternSynDefn) -> TypeError
CannotResolveAmbiguousPatternSynonym (List1 (QName, PatternSynDefn) -> TypeError)
-> List1 (QName, PatternSynDefn) -> TypeError
forall a b. (a -> b) -> a -> b
$ List1 QName
-> NonEmpty PatternSynDefn -> List1 (QName, PatternSynDefn)
forall a b. NonEmpty a -> NonEmpty b -> NonEmpty (a, b)
List1.zip List1 QName
xs NonEmpty PatternSynDefn
defs

lookupSinglePatternSyn :: QName -> TCM PatternSynDefn
lookupSinglePatternSyn :: QName -> TCM PatternSynDefn
lookupSinglePatternSyn QName
x = do
    s <- TCMT IO PatternSynDefns
forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getPatternSyns
    case Map.lookup x s of
        Just PatternSynDefn
d  -> PatternSynDefn -> TCM PatternSynDefn
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return PatternSynDefn
d
        Maybe PatternSynDefn
Nothing -> do
            si <- TCMT IO PatternSynDefns
forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getPatternSynImports
            case Map.lookup x si of
                Just PatternSynDefn
d  -> PatternSynDefn -> TCM PatternSynDefn
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return PatternSynDefn
d
                Maybe PatternSynDefn
Nothing -> QName -> TCM PatternSynDefn
forall a. QName -> TCM a
notInScopeError (QName -> TCM PatternSynDefn) -> QName -> TCM PatternSynDefn
forall a b. (a -> b) -> a -> b
$ QName -> QName
qnameToConcrete QName
x

---------------------------------------------------------------------------
-- * Benchmark
---------------------------------------------------------------------------

-- | Lens getter for 'Benchmark' from 'TCState'.
theBenchmark :: TCState -> Benchmark
theBenchmark :: TCState -> Benchmark
theBenchmark = PersistentTCState -> Benchmark
stBenchmark (PersistentTCState -> Benchmark)
-> (TCState -> PersistentTCState) -> TCState -> Benchmark
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState

{-# INLINE updateBenchmark #-}
-- | Lens map for 'Benchmark'.
updateBenchmark :: (Benchmark -> Benchmark) -> TCState -> TCState
updateBenchmark :: (Benchmark -> Benchmark) -> TCState -> TCState
updateBenchmark Benchmark -> Benchmark
f = (PersistentTCState -> PersistentTCState) -> TCState -> TCState
updatePersistentState ((PersistentTCState -> PersistentTCState) -> TCState -> TCState)
-> (PersistentTCState -> PersistentTCState) -> TCState -> TCState
forall a b. (a -> b) -> a -> b
$ \ PersistentTCState
s -> PersistentTCState
s { stBenchmark = f (stBenchmark s) }

-- | Lens getter for 'Benchmark' from 'TCM'.
getBenchmark :: TCM Benchmark
getBenchmark :: TCM Benchmark
getBenchmark = (TCState -> Benchmark) -> TCM Benchmark
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC ((TCState -> Benchmark) -> TCM Benchmark)
-> (TCState -> Benchmark) -> TCM Benchmark
forall a b. (a -> b) -> a -> b
$ TCState -> Benchmark
theBenchmark

{-# INLINE modifyBenchmark #-}
-- | Lens modify for 'Benchmark'.
modifyBenchmark :: (Benchmark -> Benchmark) -> TCM ()
modifyBenchmark :: (Benchmark -> Benchmark) -> TCM ()
modifyBenchmark = (TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC' ((TCState -> TCState) -> TCM ())
-> ((Benchmark -> Benchmark) -> TCState -> TCState)
-> (Benchmark -> Benchmark)
-> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Benchmark -> Benchmark) -> TCState -> TCState
updateBenchmark

---------------------------------------------------------------------------
-- * Instance definitions
---------------------------------------------------------------------------

-- | Lens for 'stInstanceDefs'.
updateInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> (TCState -> TCState)
updateInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCState -> TCState
updateInstanceDefs = Lens' TCState TempInstanceTable
-> (TempInstanceTable -> TempInstanceTable) -> TCState -> TCState
forall o i. Lens' o i -> LensMap o i
over (TempInstanceTable -> f TempInstanceTable) -> TCState -> f TCState
Lens' TCState TempInstanceTable
stInstanceDefs

modifyInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCM ()
modifyInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCM ()
modifyInstanceDefs = (TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> TCM ())
-> ((TempInstanceTable -> TempInstanceTable) -> TCState -> TCState)
-> (TempInstanceTable -> TempInstanceTable)
-> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TempInstanceTable -> TempInstanceTable) -> TCState -> TCState
updateInstanceDefs

getAllInstanceDefs :: TCM TempInstanceTable
getAllInstanceDefs :: TCM TempInstanceTable
getAllInstanceDefs = do
  (table, xs) <- Lens' TCState TempInstanceTable -> TCM TempInstanceTable
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (TempInstanceTable -> f TempInstanceTable) -> TCState -> f TCState
Lens' TCState TempInstanceTable
stInstanceDefs
  itable <- useTC (stImports . sigInstances)
  let table' = InstanceTable
table InstanceTable -> InstanceTable -> InstanceTable
forall a. Semigroup a => a -> a -> a
<> InstanceTable
itable
  () <- liftIO $ evaluate (rnf table')
  return (table', xs)

getAnonInstanceDefs :: TCM (Set QName)
getAnonInstanceDefs :: TCM (Set QName)
getAnonInstanceDefs = TempInstanceTable -> Set QName
forall a b. (a, b) -> b
snd (TempInstanceTable -> Set QName)
-> TCM TempInstanceTable -> TCM (Set QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM TempInstanceTable
getAllInstanceDefs

-- | Remove an instance from the set of unresolved instances.
clearUnknownInstance :: QName -> TCM ()
clearUnknownInstance :: QName -> TCM ()
clearUnknownInstance QName
q = (TempInstanceTable -> TempInstanceTable) -> TCM ()
modifyInstanceDefs ((TempInstanceTable -> TempInstanceTable) -> TCM ())
-> (TempInstanceTable -> TempInstanceTable) -> TCM ()
forall a b. (a -> b) -> a -> b
$ (Set QName -> Set QName) -> TempInstanceTable -> TempInstanceTable
forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd ((Set QName -> Set QName)
 -> TempInstanceTable -> TempInstanceTable)
-> (Set QName -> Set QName)
-> TempInstanceTable
-> TempInstanceTable
forall a b. (a -> b) -> a -> b
$ QName -> Set QName -> Set QName
forall a. Ord a => a -> Set a -> Set a
Set.delete QName
q

-- | Add an instance whose type is still unresolved.
addUnknownInstance :: QName -> TCM ()
addUnknownInstance :: QName -> TCM ()
addUnknownInstance QName
x = do
  [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.decl.instance" Int
10 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$
    [Char]
"adding definition " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
    [Char]
" to the instance table (the type is not yet known)"
  (TempInstanceTable -> TempInstanceTable) -> TCM ()
modifyInstanceDefs ((TempInstanceTable -> TempInstanceTable) -> TCM ())
-> (TempInstanceTable -> TempInstanceTable) -> TCM ()
forall a b. (a -> b) -> a -> b
$ (Set QName -> Set QName) -> TempInstanceTable -> TempInstanceTable
forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd ((Set QName -> Set QName)
 -> TempInstanceTable -> TempInstanceTable)
-> (Set QName -> Set QName)
-> TempInstanceTable
-> TempInstanceTable
forall a b. (a -> b) -> a -> b
$ QName -> Set QName -> Set QName
forall a. Ord a => a -> Set a -> Set a
Set.insert QName
x