module Agda.TypeChecking.Monad.Imports
  ( addImport
  , addImportCycleCheck
  , checkForImportCycle
  , dropDecodedModule
  , getDecodedModule
  , getDecodedModules
  , getImportPath
  , getImports
  , getPrettyVisitedModules
  , getVisitedModule
  , getVisitedModules
  , isImported
  , setDecodedModules
  , setVisitedModules
  , storeDecodedModule
  , visitModule
  , withImportPath
  ) where

import Control.Arrow ( (***) )
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.Pretty


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 :: forall a. TopLevelModuleName -> TCM a -> TCM a
addImportCycleCheck TopLevelModuleName
m =
    (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a)
-> (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO 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 :: ReadTCState m => m VisitedModules
getVisitedModules :: forall (m :: * -> *).
ReadTCState m =>
m (Map TopLevelModuleName ModuleInfo)
getVisitedModules = Lens' (Map TopLevelModuleName ModuleInfo) TCState
-> m (Map TopLevelModuleName ModuleInfo)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map TopLevelModuleName ModuleInfo) TCState
stVisitedModules

getPrettyVisitedModules :: ReadTCState m => m Doc
getPrettyVisitedModules :: forall (m :: * -> *). ReadTCState m => m Doc
getPrettyVisitedModules = do
  [Doc]
visited <-  ((TopLevelModuleName, ModuleInfo) -> Doc)
-> [(TopLevelModuleName, ModuleInfo)] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Doc -> Doc -> Doc) -> (Doc, Doc) -> Doc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
(<>) ((Doc, Doc) -> Doc)
-> ((TopLevelModuleName, ModuleInfo) -> (Doc, Doc))
-> (TopLevelModuleName, ModuleInfo)
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopLevelModuleName -> Doc
forall a. Pretty a => a -> Doc
pretty (TopLevelModuleName -> Doc)
-> (ModuleInfo -> Doc)
-> (TopLevelModuleName, ModuleInfo)
-> (Doc, Doc)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** (ModuleCheckMode -> Doc
prettyCheckMode (ModuleCheckMode -> Doc)
-> (ModuleInfo -> ModuleCheckMode) -> ModuleInfo -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleInfo -> ModuleCheckMode
miMode))) ([(TopLevelModuleName, ModuleInfo)] -> [Doc])
-> (Map TopLevelModuleName ModuleInfo
    -> [(TopLevelModuleName, ModuleInfo)])
-> Map TopLevelModuleName ModuleInfo
-> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map TopLevelModuleName ModuleInfo
-> [(TopLevelModuleName, ModuleInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList
          (Map TopLevelModuleName ModuleInfo -> [Doc])
-> m (Map TopLevelModuleName ModuleInfo) -> m [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Map TopLevelModuleName ModuleInfo)
forall (m :: * -> *).
ReadTCState m =>
m (Map TopLevelModuleName ModuleInfo)
getVisitedModules
  Doc -> m Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> m Doc) -> Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
", " [Doc]
visited
  where
  prettyCheckMode :: ModuleCheckMode -> Doc
  prettyCheckMode :: ModuleCheckMode -> Doc
prettyCheckMode ModuleCheckMode
ModuleTypeChecked                  = Doc
""
  prettyCheckMode ModuleCheckMode
ModuleScopeChecked                 = Doc
" (scope only)"

getVisitedModule :: ReadTCState m
                 => C.TopLevelModuleName
                 -> m (Maybe ModuleInfo)
getVisitedModule :: forall (m :: * -> *).
ReadTCState m =>
TopLevelModuleName -> m (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)
-> m (Map TopLevelModuleName ModuleInfo) -> m (Maybe ModuleInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' (Map TopLevelModuleName ModuleInfo) TCState
-> m (Map TopLevelModuleName ModuleInfo)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map TopLevelModuleName ModuleInfo) TCState
stVisitedModules

getDecodedModules :: TCM DecodedModules
getDecodedModules :: TCM (Map TopLevelModuleName ModuleInfo)
getDecodedModules = PersistentTCState -> Map TopLevelModuleName ModuleInfo
stDecodedModules (PersistentTCState -> Map TopLevelModuleName ModuleInfo)
-> (TCState -> PersistentTCState)
-> TCState
-> Map TopLevelModuleName ModuleInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState (TCState -> Map TopLevelModuleName ModuleInfo)
-> TCMT IO TCState -> TCM (Map TopLevelModuleName ModuleInfo)
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 :: Map TopLevelModuleName ModuleInfo -> TCM ()
setDecodedModules Map TopLevelModuleName ModuleInfo
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 :: Map TopLevelModuleName ModuleInfo
stDecodedModules = Map TopLevelModuleName ModuleInfo
ms } }

getDecodedModule :: C.TopLevelModuleName -> TCM (Maybe ModuleInfo)
getDecodedModule :: TopLevelModuleName -> TCM (Maybe ModuleInfo)
getDecodedModule 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)
-> (TCState -> Map TopLevelModuleName ModuleInfo)
-> TCState
-> Maybe ModuleInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PersistentTCState -> Map TopLevelModuleName ModuleInfo
stDecodedModules (PersistentTCState -> Map TopLevelModuleName ModuleInfo)
-> (TCState -> PersistentTCState)
-> TCState
-> Map TopLevelModuleName ModuleInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState (TCState -> Maybe ModuleInfo)
-> TCMT IO TCState -> TCM (Maybe ModuleInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC

storeDecodedModule :: ModuleInfo -> TCM ()
storeDecodedModule :: ModuleInfo -> TCM ()
storeDecodedModule ModuleInfo
mi = (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 :: Map TopLevelModuleName ModuleInfo
stDecodedModules =
          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 (Map TopLevelModuleName ModuleInfo
 -> Map TopLevelModuleName ModuleInfo)
-> Map TopLevelModuleName ModuleInfo
-> Map TopLevelModuleName ModuleInfo
forall a b. (a -> b) -> a -> b
$
            PersistentTCState -> Map TopLevelModuleName ModuleInfo
stDecodedModules (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 :: Map TopLevelModuleName ModuleInfo
stDecodedModules =
                                  TopLevelModuleName
-> Map TopLevelModuleName ModuleInfo
-> Map TopLevelModuleName ModuleInfo
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete TopLevelModuleName
x (Map TopLevelModuleName ModuleInfo
 -> Map TopLevelModuleName ModuleInfo)
-> Map TopLevelModuleName ModuleInfo
-> Map TopLevelModuleName ModuleInfo
forall a b. (a -> b) -> a -> b
$ PersistentTCState -> Map TopLevelModuleName ModuleInfo
stDecodedModules (PersistentTCState -> Map TopLevelModuleName ModuleInfo)
-> PersistentTCState -> Map TopLevelModuleName ModuleInfo
forall a b. (a -> b) -> a -> b
$ TCState -> PersistentTCState
stPersistentState TCState
s
                              }
  }

withImportPath :: [C.TopLevelModuleName] -> TCM a -> TCM a
withImportPath :: forall a. [TopLevelModuleName] -> TCM a -> TCM a
withImportPath [TopLevelModuleName]
path = (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC ((TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a)
-> (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO 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.
(HasCallStack, MonadTCError 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)