{-# OPTIONS_GHC -Wunused-imports #-}

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

import Control.Arrow   ( (***) )
import Control.Monad   ( when )

import qualified Data.Set as Set
import qualified Data.Map as Map

import Agda.Syntax.TopLevelModuleName
import Agda.TypeChecking.Monad.Base

import Agda.Utils.List ( caseListM )
import Agda.Syntax.Common.Pretty

import Agda.Utils.Impossible

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

addImportCycleCheck :: 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 a. (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 = m : envImportPath e }

getImportPath :: TCM [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' TCState (Map TopLevelModuleName ModuleInfo)
-> (Map TopLevelModuleName ModuleInfo
    -> Map TopLevelModuleName ModuleInfo)
-> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
modifyTCLens (Map TopLevelModuleName ModuleInfo
 -> f (Map TopLevelModuleName ModuleInfo))
-> TCState -> f TCState
Lens' TCState (Map TopLevelModuleName ModuleInfo)
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 (Interface -> TopLevelModuleName
iTopLevelModuleName (Interface -> TopLevelModuleName)
-> Interface -> TopLevelModuleName
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' TCState (Map TopLevelModuleName ModuleInfo)
-> Map TopLevelModuleName ModuleInfo -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
setTCLens (Map TopLevelModuleName ModuleInfo
 -> f (Map TopLevelModuleName ModuleInfo))
-> TCState -> f TCState
Lens' TCState (Map TopLevelModuleName ModuleInfo)
stVisitedModules Map TopLevelModuleName ModuleInfo
ms

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

getPrettyVisitedModules :: ReadTCState m => m Doc
getPrettyVisitedModules :: forall (m :: * -> *). ReadTCState m => m Doc
getPrettyVisitedModules = do
  [Doc]
visited <-  ((TopLevelModuleName, ModuleInfo) -> Doc)
-> [(TopLevelModuleName, ModuleInfo)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
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 b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
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 a. a -> m a
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
                 => 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' TCState (Map TopLevelModuleName ModuleInfo)
-> m (Map TopLevelModuleName ModuleInfo)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Map TopLevelModuleName ModuleInfo
 -> f (Map TopLevelModuleName ModuleInfo))
-> TCState -> f TCState
Lens' TCState (Map TopLevelModuleName ModuleInfo)
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 = (stPersistentState s) { stDecodedModules = ms } }

getDecodedModule :: 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 =
        (stPersistentState s) { stDecodedModules =
          Map.insert (iTopLevelModuleName $ miInterface mi) mi $
            stDecodedModules (stPersistentState s)
        }
  }

dropDecodedModule :: 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 =
        (stPersistentState s) { stDecodedModules =
                                  Map.delete x $ stDecodedModules $ stPersistentState s
                              }
  }

withImportPath :: [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 a. (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 = 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 a. Eq a => a -> [a] -> 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)