{-# LANGUAGE BangPatterns #-}
module Agda.TypeChecking.Monad.State where
import qualified Control.Exception as E
import Control.Monad.State (void)
import Control.Monad.Trans (liftIO)
import Data.Maybe
import qualified Data.Map as Map
import Data.List.NonEmpty (NonEmpty(..))
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 Data.Traversable (traverse)
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
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 }
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 (\ s :: 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
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 (\ s :: 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)
localTCStateSaving :: TCM a -> TCM (a, TCState)
localTCStateSaving :: TCM a -> TCM (a, TCState)
localTCStateSaving compute :: 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)
localTCStateSavingWarnings :: TCM a -> TCM a
localTCStateSavingWarnings :: TCM a -> TCM a
localTCStateSavingWarnings compute :: TCM a
compute = do
(result :: a
result, newState :: 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
speculateTCState :: TCM (a, SpeculateResult) -> TCM a
speculateTCState :: TCM (a, SpeculateResult) -> TCM a
speculateTCState m :: TCM (a, SpeculateResult)
m = do
((x :: a
x, res :: SpeculateResult
res), newState :: 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
SpeculateAbort -> a -> TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
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_ m :: 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
freshTCM :: TCM a -> TCM (Either TCErr a)
freshTCM :: TCM a -> TCM (Either TCErr a)
freshTCM m :: 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
a, s :: 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 err :: 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 s :: 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
_ -> () -> 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
lensPersistentState :: Lens' PersistentTCState TCState
lensPersistentState :: (PersistentTCState -> f PersistentTCState) -> TCState -> f TCState
lensPersistentState f :: PersistentTCState -> f PersistentTCState
f s :: 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
<&> \ p :: PersistentTCState
p -> TCState
s { stPersistentState :: PersistentTCState
stPersistentState = PersistentTCState
p }
updatePersistentState
:: (PersistentTCState -> PersistentTCState) -> (TCState -> TCState)
updatePersistentState :: (PersistentTCState -> PersistentTCState) -> TCState -> TCState
updatePersistentState f :: PersistentTCState -> PersistentTCState
f s :: 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
lensAccumStatisticsP :: Lens' Statistics PersistentTCState
lensAccumStatisticsP :: (Statistics -> f Statistics)
-> PersistentTCState -> f PersistentTCState
lensAccumStatisticsP f :: Statistics -> f Statistics
f s :: 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
<&> \ a :: 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
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
setScope :: ScopeInfo -> TCM ()
setScope :: ScopeInfo -> TCM ()
setScope scope :: 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)
modifyScope_ :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m ()
modifyScope_ :: (ScopeInfo -> ScopeInfo) -> m ()
modifyScope_ f :: 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
modifyScope :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m ()
modifyScope :: (ScopeInfo -> ScopeInfo) -> m ()
modifyScope f :: 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)
useScope :: ReadTCState m => Lens' a ScopeInfo -> m a
useScope :: Lens' a ScopeInfo -> m a
useScope l :: 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
locallyScope :: ReadTCState m => Lens' a ScopeInfo -> (a -> a) -> m b -> m b
locallyScope :: Lens' a ScopeInfo -> (a -> a) -> m b -> m b
locallyScope l :: 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
withScope :: ReadTCState m => ScopeInfo -> m a -> m (a, ScopeInfo)
withScope :: ScopeInfo -> m a -> m (a, ScopeInfo)
withScope s :: ScopeInfo
s m :: 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
withScope_ :: ReadTCState m => ScopeInfo -> m a -> m a
withScope_ :: ScopeInfo -> m a -> m a
withScope_ s :: ScopeInfo
s m :: 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
localScope :: TCM a -> TCM a
localScope :: TCM a -> TCM a
localScope m :: 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
notInScopeError :: C.QName -> TCM a
notInScopeError :: QName -> TCM a
notInScopeError x :: QName
x = do
String -> Int -> String -> TCM ()
printScope "unbound" 5 ""
TypeError -> TCM a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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 x :: QName
x = do
String -> Int -> String -> TCM ()
printScope "unbound" 5 ""
Warning -> TCM ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ [QName] -> Warning
NotInScopeW [QName
x]
printScope :: String -> Int -> String -> TCM ()
printScope :: String -> Int -> String -> TCM ()
printScope tag :: String
tag v :: Int
v s :: String
s = String -> Int -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => String -> Int -> m () -> m ()
verboseS ("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 ("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
vcat [ String -> Doc
text String
s, ScopeInfo -> Doc
forall a. Pretty a => a -> Doc
pretty ScopeInfo
scope ]
modifySignature :: (Signature -> Signature) -> TCM ()
modifySignature :: (Signature -> Signature) -> TCM ()
modifySignature f :: Signature -> Signature
f = Lens' Signature TCState
stSignature Lens' Signature TCState -> (Signature -> Signature) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` Signature -> Signature
f
modifyImportedSignature :: (Signature -> Signature) -> TCM ()
modifyImportedSignature :: (Signature -> Signature) -> TCM ()
modifyImportedSignature f :: Signature -> Signature
f = Lens' Signature TCState
stImports Lens' Signature TCState -> (Signature -> Signature) -> TCM ()
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
modifyGlobalDefinition :: QName -> (Definition -> Definition) -> TCM ()
modifyGlobalDefinition :: QName -> (Definition -> Definition) -> TCM ()
modifyGlobalDefinition q :: QName
q f :: Definition -> Definition
f = do
(Signature -> Signature) -> TCM ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q Definition -> Definition
f
(Signature -> Signature) -> TCM ()
modifyImportedSignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q Definition -> Definition
f
setSignature :: Signature -> TCM ()
setSignature :: Signature -> TCM ()
setSignature sig :: Signature
sig = (Signature -> Signature) -> TCM ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ Signature -> Signature -> Signature
forall a b. a -> b -> a
const Signature
sig
withSignature :: Signature -> TCM a -> TCM a
withSignature :: Signature -> TCM a -> TCM a
withSignature sig :: Signature
sig m :: TCM a
m = do
Signature
sig0 <- TCMT IO Signature
forall (m :: * -> *). ReadTCState m => m Signature
getSignature
Signature -> TCM ()
setSignature Signature
sig
a
r <- TCM a
m
Signature -> TCM ()
setSignature Signature
sig0
a -> TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r
addRewriteRulesFor :: QName -> RewriteRules -> [QName] -> Signature -> Signature
addRewriteRulesFor :: QName -> RewriteRules -> [QName] -> Signature -> Signature
addRewriteRulesFor f :: QName
f rews :: RewriteRules
rews matchables :: [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 LensMap (HashMap QName RewriteRules) Signature
-> LensMap (HashMap QName RewriteRules) Signature
forall a b. (a -> b) -> a -> b
$ (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 ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (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 def :: 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 rew :: 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 f :: QName
f matchables :: [QName]
matchables =
((Signature -> Signature)
-> (Signature -> Signature) -> Signature -> Signature)
-> (Signature -> Signature)
-> [Signature -> Signature]
-> 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
forall a. a -> a
id ([Signature -> Signature] -> Signature -> Signature)
-> [Signature -> Signature] -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (QName -> Signature -> Signature)
-> [QName] -> [Signature -> Signature]
forall a b. (a -> b) -> [a] -> [b]
map (\g :: QName
g -> QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
g ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ Definition -> Definition
setMatchable) [QName]
matchables
where
setMatchable :: Definition -> Definition
setMatchable def :: 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 }
lookupDefinition :: QName -> Signature -> Maybe Definition
lookupDefinition :: QName -> Signature -> Maybe Definition
lookupDefinition q :: QName
q sig :: 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 q :: QName
q f :: 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 f :: Defn -> Defn
f def :: 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 f :: Type -> Type
f def :: 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 f :: [Occurrence] -> [Occurrence]
f def :: 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 f :: [Polarity] -> [Polarity]
f def :: 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 f :: CompiledRepresentation -> CompiledRepresentation
f def :: 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 backend :: String
backend pragma :: 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 f :: [Clause] -> [Clause]
f def :: Defn
def@Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs} = Defn
def { funClauses :: [Clause]
funClauses = [Clause] -> [Clause]
f [Clause]
cs }
updateFunClauses f :: [Clause] -> [Clause]
f _ = Defn
forall a. HasCallStack => a
__IMPOSSIBLE__
updateCovering :: ([Clause] -> [Clause]) -> (Defn -> Defn)
updateCovering :: ([Clause] -> [Clause]) -> Defn -> Defn
updateCovering f :: [Clause] -> [Clause]
f def :: Defn
def@Function{ funCovering :: Defn -> [Clause]
funCovering = [Clause]
cs} = Defn
def { funCovering :: [Clause]
funCovering = [Clause] -> [Clause]
f [Clause]
cs }
updateCovering f :: [Clause] -> [Clause]
f _ = Defn
forall a. HasCallStack => a
__IMPOSSIBLE__
updateCompiledClauses :: (Maybe CompiledClauses -> Maybe CompiledClauses) -> (Defn -> Defn)
updateCompiledClauses :: (Maybe CompiledClauses -> Maybe CompiledClauses) -> Defn -> Defn
updateCompiledClauses f :: 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 f :: Maybe CompiledClauses -> Maybe CompiledClauses
f _ = Defn
forall a. HasCallStack => a
__IMPOSSIBLE__
updateDefCopatternLHS :: (Bool -> Bool) -> Definition -> Definition
updateDefCopatternLHS :: (Bool -> Bool) -> Definition -> Definition
updateDefCopatternLHS f :: 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 f :: Blocked_ -> Blocked_
f def :: Definition
def@Defn{ defBlocked :: Definition -> Blocked_
defBlocked = Blocked_
b } = Definition
def { defBlocked :: Blocked_
defBlocked = Blocked_ -> Blocked_
f Blocked_
b }
setTopLevelModule :: C.QName -> TCM ()
setTopLevelModule :: QName -> TCM ()
setTopLevelModule x :: QName
x = Lens' NameId TCState
stFreshNameId Lens' NameId TCState -> NameId -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` Word64 -> Word64 -> NameId
NameId 0 (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)
withTopLevelModule :: C.QName -> TCM a -> TCM a
withTopLevelModule :: QName -> TCM a -> TCM a
withTopLevelModule x :: QName
x m :: 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
addForeignCode :: BackendName -> String -> TCM ()
addForeignCode :: String -> String -> TCM ()
addForeignCode backend :: String
backend code :: String
code = do
Range
r <- (TCEnv -> Range) -> TCMT IO Range
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Range
envRange
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 []
getInteractionOutputCallback :: TCM InteractionOutputCallback
getInteractionOutputCallback :: TCM InteractionOutputCallback
getInteractionOutputCallback
= (TCState -> InteractionOutputCallback)
-> TCM InteractionOutputCallback
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC ((TCState -> InteractionOutputCallback)
-> TCM InteractionOutputCallback)
-> (TCState -> InteractionOutputCallback)
-> TCM 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 r :: Response
r
= TCM InteractionOutputCallback
getInteractionOutputCallback TCM InteractionOutputCallback
-> (InteractionOutputCallback -> TCM ()) -> TCM ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ cb :: InteractionOutputCallback
cb -> InteractionOutputCallback
cb Response
r
setInteractionOutputCallback :: InteractionOutputCallback -> TCM ()
setInteractionOutputCallback :: InteractionOutputCallback -> TCM ()
setInteractionOutputCallback cb :: InteractionOutputCallback
cb
= (PersistentTCState -> PersistentTCState) -> TCM ()
modifyPersistentState ((PersistentTCState -> PersistentTCState) -> TCM ())
-> (PersistentTCState -> PersistentTCState) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ s :: PersistentTCState
s -> PersistentTCState
s { stInteractionOutputCallback :: InteractionOutputCallback
stInteractionOutputCallback = InteractionOutputCallback
cb }
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 m :: PatternSynDefns
m = (PatternSynDefns -> PatternSynDefns) -> TCM ()
modifyPatternSyns (PatternSynDefns -> PatternSynDefns -> PatternSynDefns
forall a b. a -> b -> a
const PatternSynDefns
m)
modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
modifyPatternSyns f :: 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
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 xs :: NonEmpty QName
xs) = do
NonEmpty PatternSynDefn
defs <- (QName -> TCM PatternSynDefn)
-> NonEmpty 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 NonEmpty QName
xs
case NonEmpty PatternSynDefn -> Maybe PatternSynDefn
mergePatternSynDefs NonEmpty PatternSynDefn
defs of
Just def :: PatternSynDefn
def -> PatternSynDefn -> TCM PatternSynDefn
forall (m :: * -> *) a. Monad m => a -> m a
return PatternSynDefn
def
Nothing -> TypeError -> TCM PatternSynDefn
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM PatternSynDefn)
-> TypeError -> TCM PatternSynDefn
forall a b. (a -> b) -> a -> b
$ NonEmpty (QName, PatternSynDefn) -> TypeError
CannotResolveAmbiguousPatternSynonym (NonEmpty QName
-> NonEmpty PatternSynDefn -> NonEmpty (QName, PatternSynDefn)
forall a b. NonEmpty a -> NonEmpty b -> NonEmpty (a, b)
NonEmpty.zip NonEmpty QName
xs NonEmpty PatternSynDefn
defs)
lookupSinglePatternSyn :: QName -> TCM PatternSynDefn
lookupSinglePatternSyn :: QName -> TCM PatternSynDefn
lookupSinglePatternSyn x :: 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 d :: PatternSynDefn
d -> PatternSynDefn -> TCM PatternSynDefn
forall (m :: * -> *) a. Monad m => a -> m a
return PatternSynDefn
d
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 d :: PatternSynDefn
d -> PatternSynDefn -> TCM PatternSynDefn
forall (m :: * -> *) a. Monad m => a -> m a
return PatternSynDefn
d
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
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
updateBenchmark :: (Benchmark -> Benchmark) -> TCState -> TCState
updateBenchmark :: (Benchmark -> Benchmark) -> TCState -> TCState
updateBenchmark f :: Benchmark -> Benchmark
f = (PersistentTCState -> PersistentTCState) -> TCState -> TCState
updatePersistentState ((PersistentTCState -> PersistentTCState) -> TCState -> TCState)
-> (PersistentTCState -> PersistentTCState) -> TCState -> TCState
forall a b. (a -> b) -> a -> b
$ \ s :: PersistentTCState
s -> PersistentTCState
s { stBenchmark :: Benchmark
stBenchmark = Benchmark -> Benchmark
f (PersistentTCState -> Benchmark
stBenchmark PersistentTCState
s) }
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
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
addImportedInstances :: Signature -> TCM ()
addImportedInstances :: Signature -> TCM ()
addImportedInstances sig :: 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)
| (i :: QName
i, Defn{ defInstance :: Definition -> Maybe QName
defInstance = Just c :: 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
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
(table :: Map QName (Set QName)
table,xs :: 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
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
addUnknownInstance :: QName -> TCM ()
addUnknownInstance :: QName -> TCM ()
addUnknownInstance x :: QName
x = do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "tc.decl.instance" 10 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$
"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]
++
" 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
addNamedInstance
:: QName
-> QName
-> TCM ()
addNamedInstance :: QName -> QName -> TCM ()
addNamedInstance x :: QName
x n :: QName
n = do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "tc.decl.instance" 10 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$
"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]
++ " to instance table for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
n
(Signature -> Signature) -> TCM ()
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
$ \ d :: Definition
d -> Definition
d { defInstance :: Maybe QName
defInstance = QName -> Maybe QName
forall a. a -> Maybe a
Just QName
n }
(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