-- | Lenses for 'TCState' and more.

module Agda.TypeChecking.Monad.State where


import qualified Control.Exception as E

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

import Data.Maybe

import qualified Data.Map as Map

import qualified Data.List.NonEmpty as NonEmpty
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.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 Agda.Utils.Hash
import Agda.Utils.Lens
import Agda.Utils.Monad (bracket_)
import Agda.Utils.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 <- (TCState -> PersistentTCState) -> TCMT IO PersistentTCState
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC TCState -> PersistentTCState
stPersistentState
    TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC (TCState -> TCM ()) -> TCState -> TCM ()
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 <- Lens' [Backend] TCState -> TCMT IO [Backend]
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' [Backend] TCState
stBackends
    TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC (TCState -> TCM ()) -> TCState -> TCM ()
forall a b. (a -> b) -> a -> b
$ (PersistentTCState -> PersistentTCState) -> TCState -> TCState
updatePersistentState (\ PersistentTCState
s -> PersistentTCState
s { stBenchmark :: Benchmark
stBenchmark = Benchmark
b }) TCState
initState
    Lens' [Backend] TCState
stBackends Lens' [Backend] TCState -> [Backend] -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> 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 :: TCM a -> TCM a
localTCState = TCMT IO TCState -> (TCState -> TCM ()) -> TCM a -> TCM a
forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC (\ TCState
s -> do
   Benchmark
b <- TCM Benchmark
getBenchmark
   TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
s
   (Benchmark -> Benchmark) -> TCM ()
modifyBenchmark ((Benchmark -> Benchmark) -> TCM ())
-> (Benchmark -> Benchmark) -> TCM ()
forall a b. (a -> b) -> a -> b
$ Benchmark -> Benchmark -> Benchmark
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 :: TCM a -> TCM (a, TCState)
localTCStateSaving TCM a
compute = do
  TCState
oldState <- TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
  a
result <- TCM a
compute
  TCState
newState <- TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
  do
    Benchmark
b <- TCM Benchmark
getBenchmark
    TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
oldState
    (Benchmark -> Benchmark) -> TCM ()
modifyBenchmark ((Benchmark -> Benchmark) -> TCM ())
-> (Benchmark -> Benchmark) -> TCM ()
forall a b. (a -> b) -> a -> b
$ Benchmark -> Benchmark -> Benchmark
forall a b. a -> b -> a
const Benchmark
b
  (a, TCState) -> TCM (a, TCState)
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 :: TCM a -> TCM a
localTCStateSavingWarnings TCM a
compute = do
  (a
result, TCState
newState) <- TCM a -> TCM (a, TCState)
forall a. TCM a -> TCM (a, TCState)
localTCStateSaving TCM a
compute
  (TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> TCM ()) -> (TCState -> TCState) -> TCM ()
forall a b. (a -> b) -> a -> b
$ Lens' [TCWarning] TCState -> LensMap [TCWarning] TCState
forall i o. Lens' i o -> LensMap i o
over Lens' [TCWarning] TCState
stTCWarnings LensMap [TCWarning] TCState -> LensMap [TCWarning] TCState
forall a b. (a -> b) -> a -> b
$ [TCWarning] -> [TCWarning] -> [TCWarning]
forall a b. a -> b -> a
const ([TCWarning] -> [TCWarning] -> [TCWarning])
-> [TCWarning] -> [TCWarning] -> [TCWarning]
forall a b. (a -> b) -> a -> b
$ TCState
newState TCState -> Lens' [TCWarning] TCState -> [TCWarning]
forall o i. o -> Lens' i o -> i
^. Lens' [TCWarning] TCState
stTCWarnings
  a -> TCM a
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 :: TCM (a, SpeculateResult) -> TCM a
speculateTCState TCM (a, SpeculateResult)
m = do
  ((a
x, SpeculateResult
res), TCState
newState) <- TCM (a, SpeculateResult) -> TCM ((a, SpeculateResult), TCState)
forall a. TCM a -> TCM (a, TCState)
localTCStateSaving TCM (a, SpeculateResult)
m
  case SpeculateResult
res of
    SpeculateResult
SpeculateAbort  -> a -> TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
    SpeculateResult
SpeculateCommit -> a
x a -> TCM () -> TCM a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
newState

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

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

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

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

lensPersistentState :: Lens' PersistentTCState TCState
lensPersistentState :: (PersistentTCState -> f PersistentTCState) -> TCState -> f TCState
lensPersistentState PersistentTCState -> f PersistentTCState
f TCState
s =
  PersistentTCState -> f PersistentTCState
f (TCState -> PersistentTCState
stPersistentState TCState
s) f PersistentTCState -> (PersistentTCState -> TCState) -> f TCState
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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 = (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' Statistics PersistentTCState
lensAccumStatisticsP :: (Statistics -> f Statistics)
-> PersistentTCState -> f PersistentTCState
lensAccumStatisticsP Statistics -> f Statistics
f PersistentTCState
s = Statistics -> f Statistics
f (PersistentTCState -> Statistics
stAccumStatistics PersistentTCState
s) f Statistics
-> (Statistics -> PersistentTCState) -> f PersistentTCState
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Statistics
a ->
  PersistentTCState
s { stAccumStatistics :: Statistics
stAccumStatistics = Statistics
a }

lensAccumStatistics :: Lens' Statistics TCState
lensAccumStatistics :: (Statistics -> f Statistics) -> TCState -> f TCState
lensAccumStatistics =  (PersistentTCState -> f PersistentTCState) -> TCState -> f TCState
Lens' PersistentTCState TCState
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' Statistics PersistentTCState
lensAccumStatisticsP

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

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

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

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

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

-- | Get a part of the current scope.
useScope :: ReadTCState m => Lens' a ScopeInfo -> m a
useScope :: Lens' a ScopeInfo -> m a
useScope Lens' a ScopeInfo
l = Lens' a TCState -> m a
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR (Lens' a TCState -> m a) -> Lens' a TCState -> m a
forall a b. (a -> b) -> a -> b
$ (ScopeInfo -> f ScopeInfo) -> TCState -> f TCState
Lens' ScopeInfo TCState
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' a ScopeInfo
l

-- | Run a computation in a modified scope.
locallyScope :: ReadTCState m => Lens' a ScopeInfo -> (a -> a) -> m b -> m b
locallyScope :: Lens' a ScopeInfo -> (a -> a) -> m b -> m b
locallyScope Lens' a ScopeInfo
l = Lens' a TCState -> (a -> a) -> m b -> m b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a TCState -> (a -> a) -> m b -> m b
locallyTCState (Lens' a TCState -> (a -> a) -> m b -> m b)
-> Lens' a TCState -> (a -> a) -> m b -> m b
forall a b. (a -> b) -> a -> b
$ (ScopeInfo -> f ScopeInfo) -> TCState -> f TCState
Lens' ScopeInfo TCState
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' a ScopeInfo
l

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

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

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

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

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

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

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

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

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

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

getSignature :: ReadTCState m => m Signature
getSignature :: m Signature
getSignature = Lens' Signature TCState -> m Signature
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' Signature TCState
stSignature

-- | 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 :: QName -> (Definition -> Definition) -> m ()
modifyGlobalDefinition QName
q Definition -> Definition
f = do
  (Signature -> Signature) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature         ((Signature -> Signature) -> m ())
-> (Signature -> Signature) -> m ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q Definition -> Definition
f
  (Signature -> Signature) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifyImportedSignature ((Signature -> Signature) -> m ())
-> (Signature -> Signature) -> m ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q Definition -> Definition
f

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

-- | Run some computation in a different signature, restore original signature.
withSignature :: (ReadTCState m, MonadTCState m) => Signature -> m a -> m a
withSignature :: Signature -> m a -> m a
withSignature Signature
sig m a
m = do
  Signature
sig0 <- m Signature
forall (m :: * -> *). ReadTCState m => m Signature
getSignature
  Signature -> m ()
forall (m :: * -> *). MonadTCState m => Signature -> m ()
setSignature Signature
sig
  a
r <- m a
m
  Signature -> m ()
forall (m :: * -> *). MonadTCState m => Signature -> m ()
setSignature Signature
sig0
  a -> m a
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 =
    Lens' (HashMap QName RewriteRules) Signature
-> LensMap (HashMap QName RewriteRules) Signature
forall i o. Lens' i o -> LensMap i o
over Lens' (HashMap QName RewriteRules) Signature
sigRewriteRules ((RewriteRules -> RewriteRules -> RewriteRules)
-> QName
-> RewriteRules
-> HashMap QName RewriteRules
-> HashMap QName RewriteRules
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
HMap.insertWith RewriteRules -> RewriteRules -> RewriteRules
forall a. Monoid a => a -> a -> a
mappend QName
f RewriteRules
rews)
  (Signature -> Signature)
-> (Signature -> Signature) -> Signature -> Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
f ((Defn -> Defn) -> Definition -> Definition
updateTheDef Defn -> Defn
setNotInjective (Definition -> Definition)
-> (Definition -> Definition) -> Definition -> Definition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Definition
setCopatternLHS)
  (Signature -> Signature)
-> (Signature -> Signature) -> Signature -> Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName -> [QName] -> Signature -> Signature
setMatchableSymbols QName
f [QName]
matchables)
    where
      setNotInjective :: Defn -> Defn
setNotInjective def :: Defn
def@Function{} = Defn
def { funInv :: FunctionInverse
funInv = FunctionInverse
forall c. FunctionInverse' c
NotInjective }
      setNotInjective Defn
def            = Defn
def

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

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

setMatchableSymbols :: QName -> [QName] -> Signature -> Signature
setMatchableSymbols :: QName -> [QName] -> Signature -> Signature
setMatchableSymbols QName
f [QName]
matchables =
  (QName -> (Signature -> Signature) -> Signature -> Signature)
-> (Signature -> Signature) -> [QName] -> Signature -> Signature
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Signature -> Signature)
-> (Signature -> Signature) -> Signature -> Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) ((Signature -> Signature)
 -> (Signature -> Signature) -> Signature -> Signature)
-> (QName -> Signature -> Signature)
-> QName
-> (Signature -> Signature)
-> Signature
-> Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\QName
g -> QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
g Definition -> Definition
setMatchable)) Signature -> Signature
forall a. a -> a
id [QName]
matchables
    where
      setMatchable :: Definition -> Definition
setMatchable Definition
def = Definition
def { defMatchable :: Set QName
defMatchable = QName -> Set QName -> Set QName
forall a. Ord a => a -> Set a -> Set a
Set.insert QName
f (Set QName -> Set QName) -> Set QName -> Set QName
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 = QName -> HashMap QName Definition -> Maybe Definition
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
q (HashMap QName Definition -> Maybe Definition)
-> HashMap QName Definition -> Maybe Definition
forall a b. (a -> b) -> a -> b
$ Signature
sig Signature
-> Lens' (HashMap QName Definition) Signature
-> HashMap QName Definition
forall o i. o -> Lens' i o -> i
^. Lens' (HashMap QName Definition) Signature
sigDefinitions

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

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

updateTheDef :: (Defn -> Defn) -> (Definition -> Definition)
updateTheDef :: (Defn -> Defn) -> Definition -> Definition
updateTheDef Defn -> Defn
f Definition
def = Definition
def { theDef :: 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 :: String -> CompilerPragma -> Definition -> Definition
addCompilerPragma String
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])
-> String
-> [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]
(++) String
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
_                              = 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
_                               = 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
_                              = 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
---------------------------------------------------------------------------

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

-- TODO: Is the hash-function collision-free? If not, then the
-- implementation of 'setTopLevelModule' should be changed.

setTopLevelModule :: C.QName -> TCM ()
setTopLevelModule :: QName -> TCM ()
setTopLevelModule QName
x = Lens' NameId TCState
stFreshNameId Lens' NameId TCState -> NameId -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` Word64 -> ModuleNameHash -> NameId
NameId Word64
0 (Word64 -> ModuleNameHash
ModuleNameHash (Word64 -> ModuleNameHash) -> Word64 -> ModuleNameHash
forall a b. (a -> b) -> a -> b
$ String -> Word64
hashString (String -> Word64) -> String -> Word64
forall a b. (a -> b) -> a -> b
$ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
x)

-- | Use a different top-level module for a computation. Used when generating
--   names for imported modules.
withTopLevelModule :: C.QName -> TCM a -> TCM a
withTopLevelModule :: QName -> TCM a -> TCM a
withTopLevelModule QName
x TCM a
m = do
  NameId
next <- Lens' NameId TCState -> TCMT IO NameId
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' NameId TCState
stFreshNameId
  QName -> TCM ()
setTopLevelModule QName
x
  a
y <- TCM a
m
  Lens' NameId TCState
stFreshNameId Lens' NameId TCState -> NameId -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` NameId
next
  a -> TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
y

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

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

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

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

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

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

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

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

getPatternSyns :: ReadTCState m => m PatternSynDefns
getPatternSyns :: m PatternSynDefns
getPatternSyns = Lens' PatternSynDefns TCState -> m PatternSynDefns
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' PatternSynDefns TCState
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 = Lens' PatternSynDefns TCState
stPatternSyns Lens' PatternSynDefns TCState
-> (PatternSynDefns -> PatternSynDefns) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` PatternSynDefns -> PatternSynDefns
f

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

-- | Get both local and imported pattern synonyms
getAllPatternSyns :: ReadTCState m => m PatternSynDefns
getAllPatternSyns :: 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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m PatternSynDefns
forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getPatternSynImports

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

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

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

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

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

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

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

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

-- | 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 = (Set QName -> Set QName -> Set QName)
-> [(QName, Set QName)] -> Map QName (Set QName)
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Set QName -> Set QName -> Set QName
forall a. Ord a => Set a -> Set a -> Set a
Set.union
               [ (QName
c, QName -> Set QName
forall a. a -> Set a
Set.singleton QName
i)
               | (QName
i, Defn{ defInstance :: Definition -> Maybe QName
defInstance = Just QName
c }) <- HashMap QName Definition -> [(QName, Definition)]
forall k v. HashMap k v -> [(k, v)]
HMap.toList (HashMap QName Definition -> [(QName, Definition)])
-> HashMap QName Definition -> [(QName, Definition)]
forall a b. (a -> b) -> a -> b
$ Signature
sig Signature
-> Lens' (HashMap QName Definition) Signature
-> HashMap QName Definition
forall o i. o -> Lens' i o -> i
^. Lens' (HashMap QName Definition) Signature
sigDefinitions ]
  Lens' (Map QName (Set QName)) TCState
stImportedInstanceDefs Lens' (Map QName (Set QName)) TCState
-> (Map QName (Set QName) -> Map QName (Set QName)) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` (Set QName -> Set QName -> Set QName)
-> Map QName (Set QName)
-> Map QName (Set QName)
-> Map QName (Set QName)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set QName -> Set QName -> Set QName
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 = Lens' TempInstanceTable TCState
-> (TempInstanceTable -> TempInstanceTable) -> TCState -> TCState
forall i o. Lens' i o -> LensMap i o
over Lens' TempInstanceTable TCState
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
  (Map QName (Set QName)
table,Set QName
xs) <- Lens' TempInstanceTable TCState -> TCM TempInstanceTable
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' TempInstanceTable TCState
stInstanceDefs
  Map QName (Set QName)
itable <- Lens' (Map QName (Set QName)) TCState
-> TCMT IO (Map QName (Set QName))
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map QName (Set QName)) TCState
stImportedInstanceDefs
  let !table' :: Map QName (Set QName)
table' = (Set QName -> Set QName -> Set QName)
-> Map QName (Set QName)
-> Map QName (Set QName)
-> Map QName (Set QName)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set QName -> Set QName -> Set QName
forall a. Ord a => Set a -> Set a -> Set a
Set.union Map QName (Set QName)
itable Map QName (Set QName)
table
  TempInstanceTable -> TCM TempInstanceTable
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 = 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 all instances whose type is still unresolved.
clearAnonInstanceDefs :: TCM ()
clearAnonInstanceDefs :: TCM ()
clearAnonInstanceDefs = (TempInstanceTable -> TempInstanceTable) -> TCM ()
modifyInstanceDefs ((TempInstanceTable -> TempInstanceTable) -> TCM ())
-> (TempInstanceTable -> TempInstanceTable) -> TCM ()
forall a b. (a -> b) -> a -> b
$ (Set QName -> Set QName) -> TempInstanceTable -> TempInstanceTable
forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd ((Set QName -> Set QName)
 -> TempInstanceTable -> TempInstanceTable)
-> (Set QName -> Set QName)
-> TempInstanceTable
-> TempInstanceTable
forall a b. (a -> b) -> a -> b
$ Set QName -> Set QName -> Set QName
forall a b. a -> b -> a
const Set QName
forall a. Set a
Set.empty

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

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