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.HashSet as HSet
import qualified Data.Map as Map

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

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


import Agda.Utils.Impossible

addImport :: TopLevelModuleName -> TCM ()
addImport :: TopLevelModuleName -> TCM ()
addImport TopLevelModuleName
top = forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
modifyTCLens' Lens' (HashSet TopLevelModuleName) TCState
stImportedModules forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HSet.insert TopLevelModuleName
top

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

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

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

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

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

getPrettyVisitedModules :: ReadTCState m => m Doc
getPrettyVisitedModules :: forall (m :: * -> *). ReadTCState m => m Doc
getPrettyVisitedModules = do
  [Doc]
visited <-  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Semigroup a => a -> a -> a
(<>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Pretty a => a -> Doc
pretty forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** (ModuleCheckMode -> Doc
prettyCheckMode forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleInfo -> ModuleCheckMode
miMode))) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [(k, a)]
Map.toList
          forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m VisitedModules
getVisitedModules
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat forall a b. (a -> b) -> a -> b
$ 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 = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TopLevelModuleName
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' VisitedModules TCState
stVisitedModules

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

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

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

storeDecodedModule :: ModuleInfo -> TCM ()
storeDecodedModule :: ModuleInfo -> TCM ()
storeDecodedModule ModuleInfo
mi = forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC forall a b. (a -> b) -> a -> b
$ \TCState
s ->
  TCState
s { stPersistentState :: PersistentTCState
stPersistentState =
        (TCState -> PersistentTCState
stPersistentState TCState
s) { stDecodedModules :: VisitedModules
stDecodedModules =
          forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Interface -> TopLevelModuleName
iTopLevelModuleName forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Interface
miInterface ModuleInfo
mi) ModuleInfo
mi forall a b. (a -> b) -> a -> b
$
            PersistentTCState -> VisitedModules
stDecodedModules (TCState -> PersistentTCState
stPersistentState TCState
s)
        }
  }

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

withImportPath :: [TopLevelModuleName] -> TCM a -> TCM a
withImportPath :: forall a. [TopLevelModuleName] -> TCM a -> TCM a
withImportPath [TopLevelModuleName]
path = forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC 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
  forall (m :: * -> *) a b.
Monad m =>
m [a] -> m b -> (a -> [a] -> m b) -> m b
caseListM TCM [TopLevelModuleName]
getImportPath forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ \ TopLevelModuleName
m [TopLevelModuleName]
ms -> do
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (TopLevelModuleName
m forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TopLevelModuleName]
ms) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [TopLevelModuleName] -> TypeError
CyclicModuleDependency
                                   forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
dropWhile (forall a. Eq a => a -> a -> Bool
/= TopLevelModuleName
m) forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse (TopLevelModuleName
mforall a. a -> [a] -> [a]
:[TopLevelModuleName]
ms)