module Agda.TypeChecking.Monad.Imports where

import Control.Monad.State


import Data.Set (Set)
import qualified Data.Map as Map
import qualified Data.Set as Set

import Agda.Syntax.Abstract.Name
import qualified Agda.Syntax.Concrete.Name as C
import Agda.TypeChecking.Monad.Base
import Agda.Utils.List ( caseListM )


import Agda.Utils.Impossible

addImport :: ModuleName -> TCM ()
addImport :: ModuleName -> TCM ()
addImport ModuleName
m = Lens' (Set ModuleName) TCState
-> (Set ModuleName -> Set ModuleName) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
modifyTCLens Lens' (Set ModuleName) TCState
stImportedModules ((Set ModuleName -> Set ModuleName) -> TCM ())
-> (Set ModuleName -> Set ModuleName) -> TCM ()
forall a b. (a -> b) -> a -> b
$ ModuleName -> Set ModuleName -> Set ModuleName
forall a. Ord a => a -> Set a -> Set a
Set.insert ModuleName
m

addImportCycleCheck :: C.TopLevelModuleName -> TCM a -> TCM a
addImportCycleCheck :: TopLevelModuleName -> TCM a -> TCM a
addImportCycleCheck TopLevelModuleName
m =
    (TCEnv -> TCEnv) -> TCM a -> TCM a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> TCM a -> TCM a)
-> (TCEnv -> TCEnv) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ \TCEnv
e -> TCEnv
e { envImportPath :: [TopLevelModuleName]
envImportPath = TopLevelModuleName
m TopLevelModuleName -> [TopLevelModuleName] -> [TopLevelModuleName]
forall a. a -> [a] -> [a]
: TCEnv -> [TopLevelModuleName]
envImportPath TCEnv
e }

getImports :: TCM (Set ModuleName)
getImports :: TCM (Set ModuleName)
getImports = Lens' (Set ModuleName) TCState -> TCM (Set ModuleName)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Set ModuleName) TCState
stImportedModules

isImported :: ModuleName -> TCM Bool
isImported :: ModuleName -> TCM Bool
isImported ModuleName
m = ModuleName -> Set ModuleName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member ModuleName
m (Set ModuleName -> Bool) -> TCM (Set ModuleName) -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM (Set ModuleName)
getImports

getImportPath :: TCM [C.TopLevelModuleName]
getImportPath :: TCM [TopLevelModuleName]
getImportPath = (TCEnv -> [TopLevelModuleName]) -> TCM [TopLevelModuleName]
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> [TopLevelModuleName]
envImportPath

visitModule :: ModuleInfo -> TCM ()
visitModule :: ModuleInfo -> TCM ()
visitModule ModuleInfo
mi =
  Lens' (Map TopLevelModuleName ModuleInfo) TCState
-> (Map TopLevelModuleName ModuleInfo
    -> Map TopLevelModuleName ModuleInfo)
-> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
modifyTCLens Lens' (Map TopLevelModuleName ModuleInfo) TCState
stVisitedModules ((Map TopLevelModuleName ModuleInfo
  -> Map TopLevelModuleName ModuleInfo)
 -> TCM ())
-> (Map TopLevelModuleName ModuleInfo
    -> Map TopLevelModuleName ModuleInfo)
-> TCM ()
forall a b. (a -> b) -> a -> b
$
    TopLevelModuleName
-> ModuleInfo
-> Map TopLevelModuleName ModuleInfo
-> Map TopLevelModuleName ModuleInfo
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (ModuleName -> TopLevelModuleName
toTopLevelModuleName (ModuleName -> TopLevelModuleName)
-> ModuleName -> TopLevelModuleName
forall a b. (a -> b) -> a -> b
$ Interface -> ModuleName
iModuleName (Interface -> ModuleName) -> Interface -> ModuleName
forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Interface
miInterface ModuleInfo
mi) ModuleInfo
mi

setVisitedModules :: VisitedModules -> TCM ()
setVisitedModules :: Map TopLevelModuleName ModuleInfo -> TCM ()
setVisitedModules Map TopLevelModuleName ModuleInfo
ms = Lens' (Map TopLevelModuleName ModuleInfo) TCState
-> Map TopLevelModuleName ModuleInfo -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
setTCLens Lens' (Map TopLevelModuleName ModuleInfo) TCState
stVisitedModules Map TopLevelModuleName ModuleInfo
ms

getVisitedModules :: TCM VisitedModules
getVisitedModules :: TCM (Map TopLevelModuleName ModuleInfo)
getVisitedModules = Lens' (Map TopLevelModuleName ModuleInfo) TCState
-> TCM (Map TopLevelModuleName ModuleInfo)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map TopLevelModuleName ModuleInfo) TCState
stVisitedModules

isVisited :: C.TopLevelModuleName -> TCM Bool
isVisited :: TopLevelModuleName -> TCM Bool
isVisited TopLevelModuleName
x = TopLevelModuleName -> Map TopLevelModuleName ModuleInfo -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member TopLevelModuleName
x (Map TopLevelModuleName ModuleInfo -> Bool)
-> TCM (Map TopLevelModuleName ModuleInfo) -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' (Map TopLevelModuleName ModuleInfo) TCState
-> TCM (Map TopLevelModuleName ModuleInfo)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map TopLevelModuleName ModuleInfo) TCState
stVisitedModules

getVisitedModule :: C.TopLevelModuleName
                 -> TCM (Maybe ModuleInfo)
getVisitedModule :: TopLevelModuleName -> TCM (Maybe ModuleInfo)
getVisitedModule TopLevelModuleName
x = TopLevelModuleName
-> Map TopLevelModuleName ModuleInfo -> Maybe ModuleInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TopLevelModuleName
x (Map TopLevelModuleName ModuleInfo -> Maybe ModuleInfo)
-> TCM (Map TopLevelModuleName ModuleInfo)
-> TCM (Maybe ModuleInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' (Map TopLevelModuleName ModuleInfo) TCState
-> TCM (Map TopLevelModuleName ModuleInfo)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map TopLevelModuleName ModuleInfo) TCState
stVisitedModules

mapVisitedModule :: C.TopLevelModuleName
                 -> (ModuleInfo -> ModuleInfo)
                 -> TCM ()
mapVisitedModule :: TopLevelModuleName -> (ModuleInfo -> ModuleInfo) -> TCM ()
mapVisitedModule TopLevelModuleName
x ModuleInfo -> ModuleInfo
f = Lens' (Map TopLevelModuleName ModuleInfo) TCState
-> (Map TopLevelModuleName ModuleInfo
    -> Map TopLevelModuleName ModuleInfo)
-> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
modifyTCLens Lens' (Map TopLevelModuleName ModuleInfo) TCState
stVisitedModules ((ModuleInfo -> ModuleInfo)
-> TopLevelModuleName
-> Map TopLevelModuleName ModuleInfo
-> Map TopLevelModuleName ModuleInfo
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust ModuleInfo -> ModuleInfo
f TopLevelModuleName
x)

getDecodedModules :: TCM DecodedModules
getDecodedModules :: TCM DecodedModules
getDecodedModules = PersistentTCState -> DecodedModules
stDecodedModules (PersistentTCState -> DecodedModules)
-> (TCState -> PersistentTCState) -> TCState -> DecodedModules
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState (TCState -> DecodedModules)
-> TCMT IO TCState -> TCM DecodedModules
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC

setDecodedModules :: DecodedModules -> TCM ()
setDecodedModules :: DecodedModules -> TCM ()
setDecodedModules DecodedModules
ms = (TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> TCM ()) -> (TCState -> TCState) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \TCState
s ->
  TCState
s { stPersistentState :: PersistentTCState
stPersistentState = (TCState -> PersistentTCState
stPersistentState TCState
s) { stDecodedModules :: DecodedModules
stDecodedModules = DecodedModules
ms } }

getDecodedModule :: C.TopLevelModuleName -> TCM (Maybe Interface)
getDecodedModule :: TopLevelModuleName -> TCM (Maybe Interface)
getDecodedModule TopLevelModuleName
x = TopLevelModuleName -> DecodedModules -> Maybe Interface
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TopLevelModuleName
x (DecodedModules -> Maybe Interface)
-> (TCState -> DecodedModules) -> TCState -> Maybe Interface
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PersistentTCState -> DecodedModules
stDecodedModules (PersistentTCState -> DecodedModules)
-> (TCState -> PersistentTCState) -> TCState -> DecodedModules
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState (TCState -> Maybe Interface)
-> TCMT IO TCState -> TCM (Maybe Interface)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC

storeDecodedModule :: Interface -> TCM ()
storeDecodedModule :: Interface -> TCM ()
storeDecodedModule Interface
i = (TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> TCM ()) -> (TCState -> TCState) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \TCState
s ->
  TCState
s { stPersistentState :: PersistentTCState
stPersistentState =
        (TCState -> PersistentTCState
stPersistentState TCState
s) { stDecodedModules :: DecodedModules
stDecodedModules =
          TopLevelModuleName -> Interface -> DecodedModules -> DecodedModules
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (ModuleName -> TopLevelModuleName
toTopLevelModuleName (ModuleName -> TopLevelModuleName)
-> ModuleName -> TopLevelModuleName
forall a b. (a -> b) -> a -> b
$ Interface -> ModuleName
iModuleName Interface
i) Interface
i (DecodedModules -> DecodedModules)
-> DecodedModules -> DecodedModules
forall a b. (a -> b) -> a -> b
$
            (PersistentTCState -> DecodedModules
stDecodedModules (PersistentTCState -> DecodedModules)
-> PersistentTCState -> DecodedModules
forall a b. (a -> b) -> a -> b
$ TCState -> PersistentTCState
stPersistentState TCState
s)
        }
  }

dropDecodedModule :: C.TopLevelModuleName -> TCM ()
dropDecodedModule :: TopLevelModuleName -> TCM ()
dropDecodedModule TopLevelModuleName
x = (TCState -> TCState) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC ((TCState -> TCState) -> TCM ()) -> (TCState -> TCState) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \TCState
s ->
  TCState
s { stPersistentState :: PersistentTCState
stPersistentState =
        (TCState -> PersistentTCState
stPersistentState TCState
s) { stDecodedModules :: DecodedModules
stDecodedModules =
                                  TopLevelModuleName -> DecodedModules -> DecodedModules
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete TopLevelModuleName
x (DecodedModules -> DecodedModules)
-> DecodedModules -> DecodedModules
forall a b. (a -> b) -> a -> b
$ PersistentTCState -> DecodedModules
stDecodedModules (PersistentTCState -> DecodedModules)
-> PersistentTCState -> DecodedModules
forall a b. (a -> b) -> a -> b
$ TCState -> PersistentTCState
stPersistentState TCState
s
                              }
  }

withImportPath :: [C.TopLevelModuleName] -> TCM a -> TCM a
withImportPath :: [TopLevelModuleName] -> TCM a -> TCM a
withImportPath [TopLevelModuleName]
path = (TCEnv -> TCEnv) -> TCM a -> TCM a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> TCM a -> TCM a)
-> (TCEnv -> TCEnv) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ \TCEnv
e -> TCEnv
e { envImportPath :: [TopLevelModuleName]
envImportPath = [TopLevelModuleName]
path }

-- | Assumes that the first module in the import path is the module we are
--   worried about.
checkForImportCycle :: TCM ()
checkForImportCycle :: TCM ()
checkForImportCycle = do
  TCM [TopLevelModuleName]
-> TCM ()
-> (TopLevelModuleName -> [TopLevelModuleName] -> TCM ())
-> TCM ()
forall (m :: * -> *) a b.
Monad m =>
m [a] -> m b -> (a -> [a] -> m b) -> m b
caseListM TCM [TopLevelModuleName]
getImportPath TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__ ((TopLevelModuleName -> [TopLevelModuleName] -> TCM ()) -> TCM ())
-> (TopLevelModuleName -> [TopLevelModuleName] -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ TopLevelModuleName
m [TopLevelModuleName]
ms -> do
    Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TopLevelModuleName
m TopLevelModuleName -> [TopLevelModuleName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TopLevelModuleName]
ms) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TopLevelModuleName] -> TypeError
CyclicModuleDependency
                                   ([TopLevelModuleName] -> TypeError)
-> [TopLevelModuleName] -> TypeError
forall a b. (a -> b) -> a -> b
$ (TopLevelModuleName -> Bool)
-> [TopLevelModuleName] -> [TopLevelModuleName]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (TopLevelModuleName -> TopLevelModuleName -> Bool
forall a. Eq a => a -> a -> Bool
/= TopLevelModuleName
m) ([TopLevelModuleName] -> [TopLevelModuleName])
-> [TopLevelModuleName] -> [TopLevelModuleName]
forall a b. (a -> b) -> a -> b
$ [TopLevelModuleName] -> [TopLevelModuleName]
forall a. [a] -> [a]
reverse (TopLevelModuleName
mTopLevelModuleName -> [TopLevelModuleName] -> [TopLevelModuleName]
forall a. a -> [a] -> [a]
:[TopLevelModuleName]
ms)