-- | Lenses for 'TCState' and more.

module Agda.TypeChecking.Monad.State where

import qualified Control.Exception as E

import Control.Monad       (void, when)
import Control.Monad.Trans (MonadIO, liftIO)

import Data.Maybe

import qualified Data.Map as Map

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

import Agda.Benchmarking

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 (bracket_)
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
    PersistentTCState
pers <- forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC TCState -> PersistentTCState
stPersistentState
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC forall a b. (a -> b) -> a -> b
$ TCState
initState { stPersistentState :: PersistentTCState
stPersistentState = PersistentTCState
pers }

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

resetAllState :: TCM ()
resetAllState :: TCM ()
resetAllState = do
    Benchmark
b <- TCM Benchmark
getBenchmark
    [Backend]
backends <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState [Backend]
stBackends
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC forall a b. (a -> b) -> a -> b
$ (PersistentTCState -> PersistentTCState) -> TCState -> TCState
updatePersistentState (\ PersistentTCState
s -> PersistentTCState
s { stBenchmark :: Benchmark
stBenchmark = Benchmark
b }) TCState
initState
    Lens' TCState [Backend]
stBackends forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens` [Backend]
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 = forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ forall (m :: * -> *). MonadTCState m => m TCState
getTC (\ TCState
s -> do
   Benchmark
b <- TCM Benchmark
getBenchmark
   forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
s
   (Benchmark -> Benchmark) -> TCM ()
modifyBenchmark forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const Benchmark
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
  TCState
oldState <- forall (m :: * -> *). MonadTCState m => m TCState
getTC
  a
result <- TCM a
compute
  TCState
newState <- forall (m :: * -> *). MonadTCState m => m TCState
getTC
  do
    Benchmark
b <- TCM Benchmark
getBenchmark
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
oldState
    (Benchmark -> Benchmark) -> TCM ()
modifyBenchmark forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const Benchmark
b
  forall (m :: * -> *) a. Monad m => a -> m a
return (a
result, TCState
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
  (a
result, TCState
newState) <- forall a. TCM a -> TCM (a, TCState)
localTCStateSaving TCM a
compute
  forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC forall a b. (a -> b) -> a -> b
$ forall o i. Lens' o i -> LensMap o i
over Lens' TCState [TCWarning]
stTCWarnings forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ TCState
newState forall o i. o -> Lens' o i -> i
^. Lens' TCState [TCWarning]
stTCWarnings
  forall (m :: * -> *) a. Monad m => a -> m a
return a
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
  ((a
x, SpeculateResult
res), TCState
newState) <- forall a. TCM a -> TCM (a, TCState)
localTCStateSaving TCM (a, SpeculateResult)
m
  case SpeculateResult
res of
    SpeculateResult
SpeculateAbort  -> forall (m :: * -> *) a. Monad m => a -> m a
return a
x
    SpeculateResult
SpeculateCommit -> a
x forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
newState

speculateTCState_ :: TCM SpeculateResult -> TCM ()
speculateTCState_ :: TCM SpeculateResult -> TCM ()
speculateTCState_ TCM SpeculateResult
m = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall a. TCM (a, SpeculateResult) -> TCM a
speculateTCState forall a b. (a -> b) -> a -> b
$ ((),) 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
  PersistentTCState
ps <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState PersistentTCState
lensPersistentState
  let s :: TCState
s = forall o i. Lens' o i -> LensSet o i
set Lens' TCState PersistentTCState
lensPersistentState PersistentTCState
ps TCState
initState
  Either TCErr (a, TCState)
r <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ (forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a.
MonadIO m =>
TCEnv -> TCState -> TCMT m a -> m (a, TCState)
runTCM TCEnv
initEnv TCState
s TCM a
m) forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`E.catch` (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left)
  case Either TCErr (a, TCState)
r of
    Right (a
a, TCState
s) -> do
      forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
setTCLens Lens' TCState PersistentTCState
lensPersistentState forall a b. (a -> b) -> a -> b
$ TCState
s forall o i. o -> Lens' o i -> i
^. Lens' TCState PersistentTCState
lensPersistentState
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 } ->
          forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
setTCLens Lens' TCState PersistentTCState
lensPersistentState forall a b. (a -> b) -> a -> b
$ TCState
s forall o i. o -> Lens' o i -> i
^. Lens' TCState PersistentTCState
lensPersistentState
        IOException TCState
s Range
_ IOException
_ ->
          forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
setTCLens Lens' TCState PersistentTCState
lensPersistentState forall a b. (a -> b) -> a -> b
$ TCState
s forall o i. o -> Lens' o i -> i
^. Lens' TCState PersistentTCState
lensPersistentState
        TCErr
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left TCErr
err

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

lensPersistentState :: Lens' TCState PersistentTCState
lensPersistentState :: Lens' TCState PersistentTCState
lensPersistentState PersistentTCState -> f PersistentTCState
f TCState
s =
  PersistentTCState -> f PersistentTCState
f (TCState -> PersistentTCState
stPersistentState TCState
s) forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ PersistentTCState
p -> TCState
s { stPersistentState :: PersistentTCState
stPersistentState = PersistentTCState
p }

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

modifyPersistentState :: (PersistentTCState -> PersistentTCState) -> TCM ()
modifyPersistentState :: (PersistentTCState -> PersistentTCState) -> TCM ()
modifyPersistentState = forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC 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) forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Statistics
a ->
  PersistentTCState
s { stAccumStatistics :: Statistics
stAccumStatistics = Statistics
a }

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

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

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

{-# INLINE setScope #-}
-- | Set the current scope.
setScope :: ScopeInfo -> TCM ()
setScope :: ScopeInfo -> TCM ()
setScope ScopeInfo
scope = forall (m :: * -> *).
MonadTCState m =>
(ScopeInfo -> ScopeInfo) -> m ()
modifyScope (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 = Lens' TCState ScopeInfo
stScope 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 = forall (m :: * -> *).
MonadTCState m =>
(ScopeInfo -> ScopeInfo) -> m ()
modifyScope_ (ScopeInfo -> ScopeInfo
recomputeInverseScopeMaps 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 = forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR forall a b. (a -> b) -> a -> b
$ Lens' TCState ScopeInfo
stScope forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState forall a b. (a -> b) -> a -> b
$ Lens' TCState ScopeInfo
stScope forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState Lens' TCState ScopeInfo
stScope (ScopeInfo -> ScopeInfo
recomputeInverseScopeMaps forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const ScopeInfo
s) forall a b. (a -> b) -> a -> b
$ (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a
m forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
  ScopeInfo
scope <- forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  a
x <- TCM a
m
  ScopeInfo -> TCM ()
setScope ScopeInfo
scope
  forall (m :: * -> *) a. Monad m => a -> m a
return a
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
5 [Char]
""
  forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError 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
5 [Char]
""
  forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning 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 = forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS ([Char]
"scope." forall a. [a] -> [a] -> [a]
++ [Char]
tag) Int
v forall a b. (a -> b) -> a -> b
$ do
  ScopeInfo
scope <- forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc ([Char]
"scope." forall a. [a] -> [a] -> [a]
++ [Char]
tag) Int
v forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat [ forall a. [Char] -> Doc a
text [Char]
s, forall a. Pretty a => a -> Doc
pretty ScopeInfo
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 = Lens' TCState Signature
stSignature 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 = Lens' TCState Signature
stImports 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 = forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR 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
  forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature         forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q Definition -> Definition
f
  forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifyImportedSignature 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 = forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ 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
  Signature
sig0 <- forall (m :: * -> *). ReadTCState m => m Signature
getSignature
  forall (m :: * -> *). MonadTCState m => Signature -> m ()
setSignature Signature
sig
  a
r <- m a
m
  forall (m :: * -> *). MonadTCState m => Signature -> m ()
setSignature Signature
sig0
  forall (m :: * -> *) a. Monad m => a -> m a
return a
r

-- ** Modifiers for rewrite rules
addRewriteRulesFor :: QName -> RewriteRules -> [QName] -> Signature -> Signature
addRewriteRulesFor :: QName -> RewriteRules -> [QName] -> Signature -> Signature
addRewriteRulesFor QName
f RewriteRules
rews [QName]
matchables =
    forall o i. Lens' o i -> LensMap o i
over Lens' Signature RewriteRuleMap
sigRewriteRules (forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
HMap.insertWith forall a. Monoid a => a -> a -> a
mappend QName
f RewriteRules
rews)
  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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Definition
setCopatternLHS)
  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 :: FunctionInverse
funInv = forall c. FunctionInverse' c
NotInjective }
      setNotInjective Defn
def            = Defn
def

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

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

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

-- ** Modifiers for parts of the signature

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

updateDefinitions :: (Definitions -> Definitions) -> Signature -> Signature
updateDefinitions :: (HashMap QName Definition -> HashMap QName Definition)
-> Signature -> Signature
updateDefinitions = forall o i. Lens' o i -> LensMap o i
over 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 forall a b. (a -> b) -> a -> b
$ 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 :: Defn
theDef = Defn -> Defn
f (Definition -> Defn
theDef Definition
def) }

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

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

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

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

addCompilerPragma :: BackendName -> CompilerPragma -> Definition -> Definition
addCompilerPragma :: [Char] -> CompilerPragma -> Definition -> Definition
addCompilerPragma [Char]
backend CompilerPragma
pragma = (CompiledRepresentation -> CompiledRepresentation)
-> Definition -> Definition
updateDefCompiledRep forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith forall a. [a] -> [a] -> [a]
(++) [Char]
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 :: [Clause]
funClauses = [Clause] -> [Clause]
f [Clause]
cs }
updateFunClauses [Clause] -> [Clause]
f 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 :: [Clause]
funCovering = [Clause] -> [Clause]
f [Clause]
cs }
updateCovering [Clause] -> [Clause]
f 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 :: Maybe CompiledClauses
funCompiled = Maybe CompiledClauses -> Maybe CompiledClauses
f Maybe CompiledClauses
cc }
updateCompiledClauses Maybe CompiledClauses -> Maybe CompiledClauses
f 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 :: Bool
defCopatternLHS = Bool -> Bool
f Bool
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 :: Blocked_
defBlocked = Blocked_ -> Blocked_
f Blocked_
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
  Maybe ModuleNameHash
hash <- forall k v. Ord k => k -> BiMap k v -> Maybe v
BiMap.lookup RawTopLevelModuleName
raw forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
stTopLevelModuleNames
  case Maybe ModuleNameHash
hash of
    Just ModuleNameHash
hash -> 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
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ModuleNameHash
hash forall a. Eq a => a -> a -> Bool
== ModuleNameHash
noModuleNameHash) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
        [Char]
"The module name " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow RawTopLevelModuleName
raw forall a. [a] -> [a] -> [a]
++ [Char]
" has a reserved " forall a. [a] -> [a] -> [a]
++
        [Char]
"hash (you may want to consider renaming the module with " forall a. [a] -> [a] -> [a]
++
        [Char]
"this name)"
      Maybe RawTopLevelModuleName
raw' <- forall v k. Ord (Tag v) => Tag v -> BiMap k v -> Maybe k
BiMap.invLookup ModuleNameHash
hash forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
stTopLevelModuleNames
      case Maybe RawTopLevelModuleName
raw' of
        Just RawTopLevelModuleName
raw' -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
          [Char]
"Module name hash collision for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow RawTopLevelModuleName
raw forall a. [a] -> [a] -> [a]
++
          [Char]
" and " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow RawTopLevelModuleName
raw' forall a. [a] -> [a] -> [a]
++ [Char]
" (you may want to consider " forall a. [a] -> [a] -> [a]
++
          [Char]
"renaming one of these modules)"
        Maybe RawTopLevelModuleName
Nothing -> do
          Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
stTopLevelModuleNames forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens'`
            forall k v.
(Ord k, HasTag v, Ord (Tag v)) =>
k -> v -> BiMap k v -> BiMap k v
BiMap.insert (forall a. KillRange a => KillRangeT a
killRange RawTopLevelModuleName
raw) ModuleNameHash
hash
          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 = forall range. TopLevelModuleName' range -> ModuleNameHash
moduleNameId TopLevelModuleName
top
  Lens' TCState NameId
stFreshNameId forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens'` Word64 -> ModuleNameHash -> NameId
NameId Word64
0 ModuleNameHash
hash
  Lens' TCState OpaqueId
stFreshOpaqueId forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens'` Word64 -> ModuleNameHash -> OpaqueId
OpaqueId Word64
0 ModuleNameHash
hash
  Lens' TCState MetaId
stFreshMetaId 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
  Maybe (ModuleName, TopLevelModuleName)
m <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR Lens' TCState (Maybe (ModuleName, TopLevelModuleName))
stCurrentModule
  case Maybe (ModuleName, TopLevelModuleName)
m of
    Just (ModuleName
_, TopLevelModuleName
top) -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just TopLevelModuleName
top)
    Maybe (ModuleName, TopLevelModuleName)
Nothing       -> do
      [TopLevelModuleName]
p <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> [TopLevelModuleName]
envImportPath
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case [TopLevelModuleName]
p of
        TopLevelModuleName
top : [TopLevelModuleName]
_ -> forall a. a -> Maybe a
Just TopLevelModuleName
top
        []      -> forall a. Maybe a
Nothing

-- | 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
  NameId
nextN <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState NameId
stFreshNameId
  MetaId
nextM <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState MetaId
stFreshMetaId
  OpaqueId
nextO <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState OpaqueId
stFreshOpaqueId
  TopLevelModuleName -> TCM ()
setTopLevelModule TopLevelModuleName
x
  a
y <- TCM a
m
  Lens' TCState MetaId
stFreshMetaId forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens` MetaId
nextM
  Lens' TCState NameId
stFreshNameId forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens` NameId
nextN
  Lens' TCState OpaqueId
stFreshOpaqueId forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens` OpaqueId
nextO
  forall (m :: * -> *) a. Monad m => a -> m a
return a
y

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

---------------------------------------------------------------------------
-- * Foreign code
---------------------------------------------------------------------------

addForeignCode :: BackendName -> String -> TCM ()
addForeignCode :: [Char] -> [Char] -> TCM ()
addForeignCode [Char]
backend [Char]
code = do
  Range
r <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Range
envRange  -- can't use TypeChecking.Monad.Trace.getCurrentRange without cycle
  forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
modifyTCLens (Lens' TCState (Map [Char] ForeignCodeStack)
stForeignCode forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. Ord k => k -> Lens' (Map k v) (Maybe v)
key [Char]
backend) forall a b. (a -> b) -> a -> b
$
    forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ForeignCode] -> ForeignCodeStack
ForeignCodeStack forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Range -> [Char] -> ForeignCode
ForeignCode Range
r [Char]
code forall a. a -> [a] -> [a]
:) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] ForeignCodeStack -> [ForeignCode]
getForeignCodeStack

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

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

appInteractionOutputCallback :: Response -> TCM ()
appInteractionOutputCallback :: InteractionOutputCallback
appInteractionOutputCallback Response
r
  = forall (m :: * -> *). ReadTCState m => m InteractionOutputCallback
getInteractionOutputCallback 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 forall a b. (a -> b) -> a -> b
$ \ PersistentTCState
s -> PersistentTCState
s { stInteractionOutputCallback :: InteractionOutputCallback
stInteractionOutputCallback = InteractionOutputCallback
cb }

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

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

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

-- | Lens for 'stPatternSyns'.
modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
modifyPatternSyns PatternSynDefns -> PatternSynDefns
f = Lens' TCState PatternSynDefns
stPatternSyns 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 = forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR Lens' TCState PatternSynDefns
stPatternSynImports

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

lookupPatternSyn :: AmbiguousQName -> TCM PatternSynDefn
lookupPatternSyn :: AmbiguousQName -> TCM PatternSynDefn
lookupPatternSyn (AmbQ List1 QName
xs) = do
  NonEmpty PatternSynDefn
defs <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse QName -> TCM PatternSynDefn
lookupSinglePatternSyn List1 QName
xs
  case NonEmpty PatternSynDefn -> Maybe PatternSynDefn
mergePatternSynDefs NonEmpty PatternSynDefn
defs of
    Just PatternSynDefn
def   -> forall (m :: * -> *) a. Monad m => a -> m a
return PatternSynDefn
def
    Maybe PatternSynDefn
Nothing    -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ List1 (QName, PatternSynDefn) -> TypeError
CannotResolveAmbiguousPatternSynonym forall a b. (a -> b) -> a -> b
$ 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
    PatternSynDefns
s <- forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getPatternSyns
    case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
x PatternSynDefns
s of
        Just PatternSynDefn
d  -> forall (m :: * -> *) a. Monad m => a -> m a
return PatternSynDefn
d
        Maybe PatternSynDefn
Nothing -> do
            PatternSynDefns
si <- forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getPatternSynImports
            case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
x PatternSynDefns
si of
                Just PatternSynDefn
d  -> forall (m :: * -> *) a. Monad m => a -> m a
return PatternSynDefn
d
                Maybe PatternSynDefn
Nothing -> forall a. QName -> TCM a
notInScopeError 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 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 forall a b. (a -> b) -> a -> b
$ \ PersistentTCState
s -> PersistentTCState
s { stBenchmark :: Benchmark
stBenchmark = Benchmark -> Benchmark
f (PersistentTCState -> Benchmark
stBenchmark PersistentTCState
s) }

-- | Lens getter for 'Benchmark' from 'TCM'.
getBenchmark :: TCM Benchmark
getBenchmark :: TCM Benchmark
getBenchmark = forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC 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 = forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC' forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Benchmark -> Benchmark) -> TCState -> TCState
updateBenchmark

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

-- | Look through the signature and reconstruct the instance table.
addImportedInstances :: Signature -> TCM ()
addImportedInstances :: Signature -> TCM ()
addImportedInstances Signature
sig = do
  let itable :: Map QName (Set QName)
itable = forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. Ord a => Set a -> Set a -> Set a
Set.union
               [ (QName
c, forall a. a -> Set a
Set.singleton QName
i)
               | (QName
i, Defn{ defInstance :: Definition -> Maybe QName
defInstance = Just QName
c }) <- forall k v. HashMap k v -> [(k, v)]
HMap.toList forall a b. (a -> b) -> a -> b
$ Signature
sig forall o i. o -> Lens' o i -> i
^. Lens' Signature (HashMap QName Definition)
sigDefinitions ]
  Lens' TCState (Map QName (Set QName))
stImportedInstanceDefs forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith forall a. Ord a => Set a -> Set a -> Set a
Set.union Map QName (Set QName)
itable

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

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

getAllInstanceDefs :: TCM TempInstanceTable
getAllInstanceDefs :: TCM TempInstanceTable
getAllInstanceDefs = do
  (Map QName (Set QName)
table,Set QName
xs) <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState TempInstanceTable
stInstanceDefs
  Map QName (Set QName)
itable <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState (Map QName (Set QName))
stImportedInstanceDefs
  let !table' :: Map QName (Set QName)
table' = forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith forall a. Ord a => Set a -> Set a -> Set a
Set.union Map QName (Set QName)
itable Map QName (Set QName)
table
  forall (m :: * -> *) a. Monad m => a -> m a
return (Map QName (Set QName)
table', Set QName
xs)

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

-- | Remove all instances whose type is still unresolved.
clearAnonInstanceDefs :: TCM ()
clearAnonInstanceDefs :: TCM ()
clearAnonInstanceDefs = (TempInstanceTable -> TempInstanceTable) -> TCM ()
modifyInstanceDefs forall a b. (a -> b) -> a -> b
$ forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a. Set a
Set.empty

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

-- | Add instance to some ``class''.
addNamedInstance
  :: QName  -- ^ Name of the instance.
  -> QName  -- ^ Name of the class.
  -> TCM ()
addNamedInstance :: QName -> QName -> TCM ()
addNamedInstance QName
x QName
n = do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.decl.instance" Int
10 forall a b. (a -> b) -> a -> b
$
    [Char]
"adding definition " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
x forall a. [a] -> [a] -> [a]
++ [Char]
" to instance table for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
n
  -- Mark x as instance for n.
  forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
x forall a b. (a -> b) -> a -> b
$ \ Definition
d -> Definition
d { defInstance :: Maybe QName
defInstance = forall a. a -> Maybe a
Just QName
n }
  -- Add x to n's instances.
  (TempInstanceTable -> TempInstanceTable) -> TCM ()
modifyInstanceDefs forall a b. (a -> b) -> a -> b
$ forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith forall a. Ord a => Set a -> Set a -> Set a
Set.union QName
n forall a b. (a -> b) -> a -> b
$ forall a. a -> Set a
Set.singleton QName
x