-- | Lenses for 'TCState' and more.

module Mikan.TypeChecking.Monad.State where

import Control.Exception qualified 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 Data.EnumMap.Strict qualified as EnumMap
import Data.HashMap.Strict qualified as HMap
import Data.Map qualified as Map
import Data.Set (Set)
import Data.Set qualified as Set

import Mikan.Benchmarking

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

import Mikan.Interaction.Library ( classifyBuiltinModule_ )
import Mikan.Interaction.Response
  (InteractionOutputCallback, Response)

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

import Mikan.TypeChecking.Monad.Base
import Mikan.TypeChecking.Monad.Diagnostic
import Mikan.TypeChecking.Warnings

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

import Mikan.Utils.BiMap qualified as BiMap
import Mikan.Utils.List1 qualified as List1
import Mikan.Utils.FileId ( File, getIdFile, registerFileId' )
import Mikan.Utils.Atomic
import Mikan.Utils.Maybe
import Mikan.Utils.Monad
import Mikan.Utils.Tuple
import Mikan.Utils.Lens
import Mikan.Utils.Tuple.Strict (Pair(..))
import Mikan.Utils.Tuple.Strict qualified as Strict
import Mikan.Utils.Maybe.Strict qualified as Strict

import Mikan.Utils.Impossible
import Control.Monad.Catch qualified as Catch

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

resetState :: TCM ()
resetState :: TCM ()
resetState = (TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC \ TCState
s -> PersistentTCState -> TCState
initStateFromPersistentState (TCState
s TCState
-> Getting PersistentTCState TCState PersistentTCState
-> PersistentTCState
forall s a. s -> Getting a s a -> a
^. Getting PersistentTCState TCState PersistentTCState
Lens' TCState PersistentTCState
lensPersistentState)

-- | Resets all of the type checking state.
--
--   Keep only the session state (backend information, 'Benchmark', file ids).

resetAllState :: TCM ()
resetAllState :: TCM ()
resetAllState = (TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC \ TCState
s -> Atomic SessionState -> TCState
initStateFromSessionState (PersistentTCState -> Atomic SessionState
stPersistentSession (TCState -> PersistentTCState
stPersistentState TCState
s))

-- | Set the 'TCState', preserving any parts of the state which should
-- persist through speculation (e.g., statistics).
putTCPreservingStats :: TCState -> TCM ()
putTCPreservingStats :: TCState -> TCM ()
putTCPreservingStats = TCMT IO Statistics -> (Statistics -> TCM ()) -> TCM () -> TCM ()
forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ TCMT IO Statistics
get Statistics -> TCM ()
put (TCM () -> TCM ()) -> (TCState -> TCM ()) -> TCState -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC where
  get :: TCMT IO Statistics
get = Getter TCState Statistics -> TCMT IO Statistics
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC (Statistics -> f Statistics) -> TCState -> f TCState
Lens' TCState Statistics
Getter TCState Statistics
stStatistics
  put :: Statistics -> TCM ()
put = ASetter' TCState Statistics -> Statistics -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> a -> m ()
setTCLens ASetter' TCState Statistics
Lens' TCState Statistics
stStatistics

-- | Restore 'TCState' after performing subcomputation.
--
-- Parts of the state which should not be reset on speculation (e.g.,
-- statistics) will not be reset.
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 -> TCM ()
putTCPreservingStats

-- | 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 = TCM (a, TCState) -> TCM (a, TCState)
forall a. TCM a -> TCM a
localTCState (TCM (a, TCState) -> TCM (a, TCState))
-> TCM (a, TCState) -> TCM (a, TCState)
forall a b. (a -> b) -> a -> b
$ (a -> TCState -> (a, TCState))
-> TCM a -> TCMT IO TCState -> TCM (a, TCState)
forall a b c. (a -> b -> c) -> TCMT IO a -> TCMT IO b -> TCMT IO c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (,) TCM a
compute TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC

-- | 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

-- | 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

  -- Run m in fresh TCM that only kept the current persistent state.
  ps <- Getter TCState PersistentTCState -> TCMT IO PersistentTCState
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC (PersistentTCState -> f PersistentTCState) -> TCState -> f TCState
Lens' TCState PersistentTCState
Getter TCState PersistentTCState
lensPersistentState
  let s0 = PersistentTCState -> TCState
initStateFromPersistentState PersistentTCState
ps
  r <- liftIO $ (Right <$> runTCM initEnv s0 m) `E.catch` (return . Left)

  -- Keep m's changes to the persistent state, if possible.
  let keepPersistent TCState
s = ASetter' TCState PersistentTCState -> PersistentTCState -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> a -> m ()
setTCLens ASetter' TCState PersistentTCState
Lens' TCState PersistentTCState
lensPersistentState (PersistentTCState -> m ()) -> PersistentTCState -> m ()
forall a b. (a -> b) -> a -> b
$ TCState
s TCState
-> Getting PersistentTCState TCState PersistentTCState
-> PersistentTCState
forall s a. s -> Getting a s a -> a
^. Getting PersistentTCState TCState PersistentTCState
Lens' TCState PersistentTCState
lensPersistentState
  case r of
    Right (a
a, TCState
s) -> a -> Either TCErr a
forall a b. b -> Either a b
Right a
a Either TCErr a -> TCM () -> TCMT IO (Either TCErr 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 ()
keepPersistent TCState
s
    Left TCErr
err -> TCErr -> Either TCErr a
forall a b. a -> Either a b
Left TCErr
err Either TCErr a -> TCM () -> TCMT IO (Either TCErr a)
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$
      case TCErr
err of
        TypeError { tcErrState :: TCErr -> TCState
tcErrState = TCState
s } -> TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
keepPersistent TCState
s
        IOException (Just TCState
s) Range
_ IOException
_     -> TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
keepPersistent TCState
s
        IOException Maybe TCState
Nothing  Range
_ IOException
_     -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        GenericException [Char]
_           -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        ParserError ParseError
_                -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        PatternErr Blocker
_                 -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

---------------------------------------------------------------------------
-- * 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 -> Identity ScopeInfo) -> TCState -> Identity TCState
Lens' TCState ScopeInfo
stScope ((ScopeInfo -> Identity ScopeInfo) -> TCState -> Identity TCState)
-> (ScopeInfo -> ScopeInfo) -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
`modifyingTC` ScopeInfo -> ScopeInfo
f

{-# INLINE recomputeInverseScope #-}
-- | Recompute inverse names, inverse modules and InScopeSet-s.
recomputeInverseScope :: MonadTCState m => m ()
recomputeInverseScope :: forall (m :: * -> *). MonadTCState m => m ()
recomputeInverseScope = (ScopeInfo -> ScopeInfo) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(ScopeInfo -> ScopeInfo) -> m ()
modifyScope ScopeInfo -> ScopeInfo
recomputeInverseScope'

{-# 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 -> 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 evalWithScope #-}
-- | Same as 'withScope', but discard the scope from the computation.
evalWithScope :: ReadTCState m => ScopeInfo -> m a -> m a
evalWithScope :: forall (m :: * -> *) a. ReadTCState m => ScopeInfo -> m a -> m a
evalWithScope 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 :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> 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 :: * -> *) e.
(HasCallStack, MonadWarning m, Diagnostic e) =>
e -> 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
  reportS ("scope." ++ tag) v $ vcat [ text s, pretty scope ]

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

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

{-# 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

{-# INLINE setSignature #-}
setSignature :: MonadTCState m => Signature -> m ()
setSignature :: forall (m :: * -> *). MonadTCState m => Signature -> m ()
setSignature Signature
sig = ASetter' TCState Signature -> (Signature -> Signature) -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
modifyingTC ASetter' TCState Signature
Lens' TCState Signature
stSignature ((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

-- ** 'modify' methods for the signature

modifyRecEta :: MonadTCState m => QName -> (EtaEquality -> EtaEquality) -> m ()
modifyRecEta :: forall (m :: * -> *).
MonadTCState m =>
QName -> (EtaEquality -> EtaEquality) -> m ()
modifyRecEta QName
q = ASetter' TCState EtaEquality
-> (EtaEquality -> EtaEquality) -> m ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
modifyingTC (ASetter' TCState EtaEquality
 -> (EtaEquality -> EtaEquality) -> m ())
-> ASetter' TCState EtaEquality
-> (EtaEquality -> EtaEquality)
-> m ()
forall a b. (a -> b) -> a -> b
$ ASetter' TCState Signature
Lens' TCState Signature
stSignature ASetter' TCState Signature
-> ((EtaEquality -> Identity EtaEquality)
    -> Signature -> Identity Signature)
-> ASetter' TCState EtaEquality
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index Signature -> Traversal' Signature (IxValue Signature)
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index Signature
QName
q ((Definition -> Identity Definition)
 -> Signature -> Identity Signature)
-> ((EtaEquality -> Identity EtaEquality)
    -> Definition -> Identity Definition)
-> (EtaEquality -> Identity EtaEquality)
-> Signature
-> Identity Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Defn -> Identity Defn) -> Definition -> Identity Definition
Lens' Definition Defn
lensTheDef ((Defn -> Identity Defn) -> Definition -> Identity Definition)
-> ((EtaEquality -> Identity EtaEquality) -> Defn -> Identity Defn)
-> (EtaEquality -> Identity EtaEquality)
-> Definition
-> Identity Definition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RecordData -> Identity RecordData) -> Defn -> Identity Defn
Lens' Defn RecordData
lensRecord ((RecordData -> Identity RecordData) -> Defn -> Identity Defn)
-> ((EtaEquality -> Identity EtaEquality)
    -> RecordData -> Identity RecordData)
-> (EtaEquality -> Identity EtaEquality)
-> Defn
-> Identity Defn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (EtaEquality -> Identity EtaEquality)
-> RecordData -> Identity RecordData
Lens' RecordData EtaEquality
lensRecEta

-- ** Modifiers for parts of the signature

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 }

---------------------------------------------------------------------------
-- * File identification
---------------------------------------------------------------------------

-- | Translate an absolute path to a file id, and register a new file id
--   if the path has not seen before.
--   Also register whether the path belongs to one of Agda's builtin modules.
--
registerFileIdWithBuiltin :: File -> FileDictWithBuiltins -> (FileId, FileDictWithBuiltins)
registerFileIdWithBuiltin :: File -> FileDictWithBuiltins -> (FileId, FileDictWithBuiltins)
registerFileIdWithBuiltin File
f (FileDictWithBuiltins FileDictBuilder
d BuiltinModuleIds
b File
primLibDir) =
  (FileId
fi, FileDictBuilder -> BuiltinModuleIds -> File -> FileDictWithBuiltins
FileDictWithBuiltins FileDictBuilder
d' BuiltinModuleIds
b' File
primLibDir)
  where
    ((FileId
fi, Bool
new), FileDictBuilder
d') = File -> FileDictBuilder -> ((FileId, Bool), FileDictBuilder)
registerFileId' File
f FileDictBuilder
d
    b' :: BuiltinModuleIds
b' = case File -> File -> Maybe IsBuiltinModule
classifyBuiltinModule_ File
primLibDir File
f of
      Maybe IsBuiltinModule
Nothing -> BuiltinModuleIds
b
      Just IsBuiltinModule
c  -> FileId -> IsBuiltinModule -> BuiltinModuleIds -> BuiltinModuleIds
forall k a. Enum k => k -> a -> EnumMap k a -> EnumMap k a
EnumMap.insert FileId
fi IsBuiltinModule
c BuiltinModuleIds
b

instance (MonadIO m, Catch.MonadMask m) => MonadFileId (TCMT m) where
  fileFromId :: HasCallStack => FileId -> TCMT m File
fileFromId FileId
fi = Lens' SessionState FileDictWithBuiltins
-> TCMT m FileDictWithBuiltins
forall (m :: * -> *) a.
ReadTCState m =>
Lens' SessionState a -> m a
useSession (FileDictWithBuiltins -> f FileDictWithBuiltins)
-> SessionState -> f SessionState
Lens' SessionState FileDictWithBuiltins
lensFileDict TCMT m FileDictWithBuiltins
-> (FileDictWithBuiltins -> File) -> TCMT m File
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (FileDictWithBuiltins -> FileId -> File
forall a. GetIdFile a => a -> FileId -> File
`getIdFile` FileId
fi)
  idFromFile :: File -> TCMT m FileId
idFromFile = Lens' SessionState FileDictWithBuiltins
-> (FileDictWithBuiltins -> (FileId, FileDictWithBuiltins))
-> TCMT m FileId
forall (m :: * -> *) a r.
ModifySession m =>
Lens' SessionState a -> (a -> (r, a)) -> m r
stateSessionLens (FileDictWithBuiltins -> f FileDictWithBuiltins)
-> SessionState -> f SessionState
Lens' SessionState FileDictWithBuiltins
lensFileDict ((FileDictWithBuiltins -> (FileId, FileDictWithBuiltins))
 -> TCMT m FileId)
-> (File -> FileDictWithBuiltins -> (FileId, FileDictWithBuiltins))
-> File
-> TCMT m FileId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. File -> FileDictWithBuiltins -> (FileId, FileDictWithBuiltins)
registerFileIdWithBuiltin

instance MonadFileId ReduceM where
  fileFromId :: HasCallStack => FileId -> ReduceM File
fileFromId FileId
fi = Lens' SessionState FileDictWithBuiltins
-> ReduceM FileDictWithBuiltins
forall (m :: * -> *) a.
ReadTCState m =>
Lens' SessionState a -> m a
useSession (FileDictWithBuiltins -> f FileDictWithBuiltins)
-> SessionState -> f SessionState
Lens' SessionState FileDictWithBuiltins
lensFileDict ReduceM FileDictWithBuiltins
-> (FileDictWithBuiltins -> File) -> ReduceM File
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (FileDictWithBuiltins -> FileId -> File
forall a. GetIdFile a => a -> FileId -> File
`getIdFile` FileId
fi)
  idFromFile :: File -> ReduceM FileId
idFromFile = File -> ReduceM FileId
forall a. HasCallStack => a
__IMPOSSIBLE__
    -- we cannot write to the state here, so we cannot do sth like
    -- stateTCLens stFileDict . registerFileIdWithBuiltin

-- | Does the given 'FileId' belong to one of Agda's builtin modules?

isBuiltinModule :: ReadTCState m => FileId -> m (Maybe IsBuiltinModule)
isBuiltinModule :: forall (m :: * -> *).
ReadTCState m =>
FileId -> m (Maybe IsBuiltinModule)
isBuiltinModule FileId
fi = FileId -> BuiltinModuleIds -> Maybe IsBuiltinModule
forall k a. Enum k => k -> EnumMap k a -> Maybe a
EnumMap.lookup FileId
fi (BuiltinModuleIds -> Maybe IsBuiltinModule)
-> m BuiltinModuleIds -> m (Maybe IsBuiltinModule)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' SessionState BuiltinModuleIds -> m BuiltinModuleIds
forall (m :: * -> *) a.
ReadTCState m =>
Lens' SessionState a -> m a
useSession (BuiltinModuleIds -> f BuiltinModuleIds)
-> SessionState -> f SessionState
Lens' SessionState BuiltinModuleIds
lensBuiltinModuleIds

-- | Does the given 'FileId' belong to one of Agda's builtin modules that only uses safe postulates?
--
-- Implies @isJust . 'isBuiltinModule'@.

isBuiltinModuleWithSafePostulates :: ReadTCState m => FileId -> m Bool
isBuiltinModuleWithSafePostulates :: forall (m :: * -> *). ReadTCState m => FileId -> m Bool
isBuiltinModuleWithSafePostulates FileId
fi = do
  FileId -> m (Maybe IsBuiltinModule)
forall (m :: * -> *).
ReadTCState m =>
FileId -> m (Maybe IsBuiltinModule)
isBuiltinModule FileId
fi m (Maybe IsBuiltinModule)
-> (Maybe IsBuiltinModule -> Bool) -> m Bool
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
    Maybe IsBuiltinModule
Nothing                                -> Bool
False
    Just IsBuiltinModule
IsBuiltinModule                   -> Bool
False
    Just IsBuiltinModule
IsBuiltinModuleWithSafePostulates -> Bool
True
    Just IsBuiltinModule
IsPrimitiveModule                 -> Bool
True

-- | Does the given 'FileId' belong to one of Agda's magical primitive modules?
--
-- Implies 'isBuiltinModuleWithSafePostulates'.

isPrimitiveModule :: ReadTCState m => FileId -> m Bool
isPrimitiveModule :: forall (m :: * -> *). ReadTCState m => FileId -> m Bool
isPrimitiveModule  FileId
fi = do
  FileId -> m (Maybe IsBuiltinModule)
forall (m :: * -> *).
ReadTCState m =>
FileId -> m (Maybe IsBuiltinModule)
isBuiltinModule FileId
fi m (Maybe IsBuiltinModule)
-> (Maybe IsBuiltinModule -> Bool) -> m Bool
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
    Maybe IsBuiltinModule
Nothing                                -> Bool
False
    Just IsBuiltinModule
IsBuiltinModule                   -> Bool
False
    Just IsBuiltinModule
IsBuiltinModuleWithSafePostulates -> Bool
False
    Just IsBuiltinModule
IsPrimitiveModule                 -> Bool
True

---------------------------------------------------------------------------
-- * 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
  (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) TCMT IO (Maybe ModuleNameHash)
-> (Maybe ModuleNameHash -> TCM TopLevelModuleName)
-> TCM TopLevelModuleName
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
>>= \case
    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 :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> 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
      (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) TCMT IO (Maybe RawTopLevelModuleName)
-> (Maybe RawTopLevelModuleName -> TCM TopLevelModuleName)
-> TCM TopLevelModuleName
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
>>= \case
        raw' :: Maybe RawTopLevelModuleName
raw'@Just{} -> TypeError -> TCM TopLevelModuleName
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> TCM TopLevelModuleName)
-> TypeError -> TCM TopLevelModuleName
forall a b. (a -> b) -> a -> b
$ RawTopLevelModuleName -> Maybe RawTopLevelModuleName -> TypeError
ModuleNameHashCollision RawTopLevelModuleName
raw Maybe RawTopLevelModuleName
raw'
        Maybe RawTopLevelModuleName
Nothing -> do
          (BiMap RawTopLevelModuleName ModuleNameHash
 -> Identity (BiMap RawTopLevelModuleName ModuleNameHash))
-> TCState -> Identity TCState
Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
stTopLevelModuleNames ((BiMap RawTopLevelModuleName ModuleNameHash
  -> Identity (BiMap RawTopLevelModuleName ModuleNameHash))
 -> TCState -> Identity TCState)
-> (BiMap RawTopLevelModuleName ModuleNameHash
    -> BiMap RawTopLevelModuleName ModuleNameHash)
-> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
`modifyingTC`
            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 -> Identity NameId) -> TCState -> Identity TCState
Lens' TCState NameId
stFreshNameId ((NameId -> Identity NameId) -> TCState -> Identity TCState)
-> NameId -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> a -> m ()
`setTCLens` Word64 -> ModuleNameHash -> NameId
NameId Word64
0 ModuleNameHash
hash
  (OpaqueId -> Identity OpaqueId) -> TCState -> Identity TCState
Lens' TCState OpaqueId
stFreshOpaqueId ((OpaqueId -> Identity OpaqueId) -> TCState -> Identity TCState)
-> OpaqueId -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> a -> m ()
`setTCLens` Word64 -> ModuleNameHash -> OpaqueId
OpaqueId Word64
0 ModuleNameHash
hash
  (MetaId -> Identity MetaId) -> TCState -> Identity TCState
Lens' TCState MetaId
stFreshMetaId ((MetaId -> Identity MetaId) -> TCState -> Identity TCState)
-> MetaId -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' 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 (Pair ModuleName TopLevelModuleName))
-> m (Maybe (Pair ModuleName TopLevelModuleName))
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Maybe (Pair ModuleName TopLevelModuleName)
 -> f (Maybe (Pair ModuleName TopLevelModuleName)))
-> TCState -> f TCState
Lens' TCState (Maybe (Pair ModuleName TopLevelModuleName))
stCurrentModule m (Maybe (Pair ModuleName TopLevelModuleName))
-> (Maybe (Pair 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
    Strict.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 (Pair ModuleName TopLevelModuleName)
Strict.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
<$> Lens' TCEnv [TopLevelModuleName] -> m [TopLevelModuleName]
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC ([TopLevelModuleName] -> f [TopLevelModuleName])
-> TCEnv -> f TCEnv
Lens' TCEnv [TopLevelModuleName]
eImportStack

-- | 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 <- Getter TCState NameId -> TCMT IO NameId
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC (NameId -> f NameId) -> TCState -> f TCState
Lens' TCState NameId
Getter 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 <- Getter TCState NameId -> m NameId
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC (NameId -> f NameId) -> TCState -> f TCState
Lens' TCState NameId
Getter TCState NameId
stFreshNameId
  return h

-- | Get a function that completes 'TopLevelModuleName's
--   with their 'SourceFile' to 'TopLevelModuleNameWithSourceFile's.
topLevelModuleNameWithSourceFileCompleter :: ReadTCState m
  => m (TopLevelModuleName -> TopLevelModuleNameWithSourceFile)
topLevelModuleNameWithSourceFileCompleter :: forall (m :: * -> *).
ReadTCState m =>
m (TopLevelModuleName -> TopLevelModuleNameWithSourceFile)
topLevelModuleNameWithSourceFileCompleter = do
  ModuleToSource _dict m2s <- Lens' SessionState ModuleToSource -> m ModuleToSource
forall (m :: * -> *) a.
ReadTCState m =>
Lens' SessionState a -> m a
useSession (ModuleToSource -> f ModuleToSource)
-> SessionState -> f SessionState
Lens' SessionState ModuleToSource
lensModuleToSource
  return \ TopLevelModuleName
m -> TopLevelModuleName
-> SourceFile -> TopLevelModuleNameWithSourceFile
TopLevelModuleNameWithSourceFile TopLevelModuleName
m (SourceFile -> TopLevelModuleNameWithSourceFile)
-> SourceFile -> TopLevelModuleNameWithSourceFile
forall a b. (a -> b) -> a -> b
$ SourceFile -> TopLevelModuleName -> ModuleToSourceId -> SourceFile
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault SourceFile
forall a. HasCallStack => a
__IMPOSSIBLE__ TopLevelModuleName
m ModuleToSourceId
m2s

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

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

lookupBackend :: ReadTCState m => BackendName -> m (Maybe Backend)
lookupBackend :: forall (m :: * -> *).
ReadTCState m =>
BackendName -> m (Maybe Backend)
lookupBackend BackendName
name = Lens' SessionState [Backend] -> m [Backend]
forall (m :: * -> *) a.
ReadTCState m =>
Lens' SessionState a -> m a
useSession ([Backend] -> f [Backend]) -> SessionState -> f SessionState
Lens' SessionState [Backend]
lensBackends m [Backend] -> ([Backend] -> Maybe Backend) -> m (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
$ Lens' TCEnv (Maybe BackendName) -> TCMT IO (Maybe BackendName)
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Maybe BackendName -> f (Maybe BackendName)) -> TCEnv -> f TCEnv
Lens' TCEnv (Maybe BackendName)
eActiveBackendName
  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 <- Lens' TCEnv Range -> TCMT IO Range
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Range -> f Range) -> TCEnv -> f TCEnv
Lens' TCEnv Range
eRange -- can't use TypeChecking.Monad.Trace.getCurrentRange without cycle
  modifyingTC (stForeignCode . key backend) $
    Just . ForeignCodeStack . (ForeignCode r code :) . maybe [] getForeignCodeStack

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

{-# INLINE getInteractionOutputCallback #-}
getInteractionOutputCallback :: ReadTCState m => m InteractionOutputCallback
getInteractionOutputCallback :: forall (m :: * -> *). ReadTCState m => m InteractionOutputCallback
getInteractionOutputCallback = Lens' SessionState InteractionOutputCallback
-> m InteractionOutputCallback
forall (m :: * -> *) a.
ReadTCState m =>
Lens' SessionState a -> m a
useSession (InteractionOutputCallback -> f InteractionOutputCallback)
-> SessionState -> f SessionState
Lens' SessionState InteractionOutputCallback
lensInteractionOutputCallback

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 = Lens' SessionState InteractionOutputCallback
-> InteractionOutputCallback -> TCM ()
forall (m :: * -> *) a.
ModifySession m =>
Lens' SessionState a -> a -> m ()
setSession (InteractionOutputCallback -> f InteractionOutputCallback)
-> SessionState -> f SessionState
Lens' SessionState InteractionOutputCallback
lensInteractionOutputCallback

---------------------------------------------------------------------------
-- * 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 -> Identity PatternSynDefns)
-> TCState -> Identity TCState
Lens' TCState PatternSynDefns
stPatternSyns ((PatternSynDefns -> Identity PatternSynDefns)
 -> TCState -> Identity TCState)
-> (PatternSynDefns -> PatternSynDefns) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
`modifyingTC` 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

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

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

-- | Lens for 'stInstanceDefs'.
updateInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> (TCState -> TCState)
updateInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCState -> TCState
updateInstanceDefs = ASetter TCState TCState TempInstanceTable TempInstanceTable
-> (TempInstanceTable -> TempInstanceTable) -> TCState -> TCState
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter TCState TCState TempInstanceTable TempInstanceTable
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) <- Getter TCState TempInstanceTable -> TCM TempInstanceTable
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC (TempInstanceTable -> f TempInstanceTable) -> TCState -> f TCState
Lens' TCState TempInstanceTable
Getter 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 c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((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 c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((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