{-# LANGUAGE CPP #-}

module Agda.Compiler.Common where

import Data.List as List
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.HashMap.Strict as HMap
import Data.Char
import Data.Function
#if __GLASGOW_HASKELL__ < 804
import Data.Semigroup
#endif

import Control.Monad
import Control.Monad.State  hiding (mapM_, forM_, mapM, forM, sequence)

import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Internal as I

import Agda.Interaction.FindFile
import Agda.Interaction.Options

import Agda.TypeChecking.Monad

import Agda.Utils.FileName
import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Pretty

import Agda.Utils.Impossible

data IsMain = IsMain | NotMain
  deriving (IsMain -> IsMain -> Bool
(IsMain -> IsMain -> Bool)
-> (IsMain -> IsMain -> Bool) -> Eq IsMain
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IsMain -> IsMain -> Bool
$c/= :: IsMain -> IsMain -> Bool
== :: IsMain -> IsMain -> Bool
$c== :: IsMain -> IsMain -> Bool
Eq, Int -> IsMain -> ShowS
[IsMain] -> ShowS
IsMain -> String
(Int -> IsMain -> ShowS)
-> (IsMain -> String) -> ([IsMain] -> ShowS) -> Show IsMain
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IsMain] -> ShowS
$cshowList :: [IsMain] -> ShowS
show :: IsMain -> String
$cshow :: IsMain -> String
showsPrec :: Int -> IsMain -> ShowS
$cshowsPrec :: Int -> IsMain -> ShowS
Show)

-- | Conjunctive semigroup ('NotMain' is absorbing).
instance Semigroup IsMain where
  IsMain
NotMain <> :: IsMain -> IsMain -> IsMain
<> IsMain
_ = IsMain
NotMain
  IsMain
_       <> IsMain
NotMain = IsMain
NotMain
  IsMain
IsMain  <> IsMain
IsMain = IsMain
IsMain

instance Monoid IsMain where
  mempty :: IsMain
mempty = IsMain
IsMain
  mappend :: IsMain -> IsMain -> IsMain
mappend = IsMain -> IsMain -> IsMain
forall a. Semigroup a => a -> a -> a
(<>)

doCompile :: forall r. Monoid r => IsMain -> Interface -> (IsMain -> Interface -> TCM r) -> TCM r
doCompile :: IsMain -> Interface -> (IsMain -> Interface -> TCM r) -> TCM r
doCompile IsMain
isMain Interface
i IsMain -> Interface -> TCM r
f = do
  -- The Agda.Primitive module is implicitly assumed to be always imported,
  -- even though it not necesseraly occurs in iImportedModules.
  -- TODO: there should be a better way to get hold of Agda.Primitive?
  [Interface
agdaPrimInter] <- (Interface -> Bool) -> [Interface] -> [Interface]
forall a. (a -> Bool) -> [a] -> [a]
filter ((String
"Agda.Primitive"String -> String -> Bool
forall a. Eq a => a -> a -> Bool
==) (String -> Bool) -> (Interface -> String) -> Interface -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> String
forall a. Pretty a => a -> String
prettyShow (ModuleName -> String)
-> (Interface -> ModuleName) -> Interface -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interface -> ModuleName
iModuleName)
    ([Interface] -> [Interface])
-> (Map TopLevelModuleName ModuleInfo -> [Interface])
-> Map TopLevelModuleName ModuleInfo
-> [Interface]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleInfo -> Interface) -> [ModuleInfo] -> [Interface]
forall a b. (a -> b) -> [a] -> [b]
map ModuleInfo -> Interface
miInterface ([ModuleInfo] -> [Interface])
-> (Map TopLevelModuleName ModuleInfo -> [ModuleInfo])
-> Map TopLevelModuleName ModuleInfo
-> [Interface]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map TopLevelModuleName ModuleInfo -> [ModuleInfo]
forall k a. Map k a -> [a]
Map.elems
      (Map TopLevelModuleName ModuleInfo -> [Interface])
-> TCMT IO (Map TopLevelModuleName ModuleInfo)
-> TCMT IO [Interface]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Map TopLevelModuleName ModuleInfo)
getVisitedModules
  (StateT (Set ModuleName) TCM r -> Set ModuleName -> TCM r)
-> Set ModuleName -> StateT (Set ModuleName) TCM r -> TCM r
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT (Set ModuleName) TCM r -> Set ModuleName -> TCM r
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT Set ModuleName
forall a. Set a
Set.empty (StateT (Set ModuleName) TCM r -> TCM r)
-> StateT (Set ModuleName) TCM r -> TCM r
forall a b. (a -> b) -> a -> b
$ r -> r -> r
forall a. Monoid a => a -> a -> a
mappend (r -> r -> r)
-> StateT (Set ModuleName) TCM r
-> StateT (Set ModuleName) TCM (r -> r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IsMain -> Interface -> StateT (Set ModuleName) TCM r
comp IsMain
NotMain Interface
agdaPrimInter StateT (Set ModuleName) TCM (r -> r)
-> StateT (Set ModuleName) TCM r -> StateT (Set ModuleName) TCM r
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IsMain -> Interface -> StateT (Set ModuleName) TCM r
comp IsMain
isMain Interface
i
  where
    comp :: IsMain -> Interface -> StateT (Set ModuleName) TCM r
    comp :: IsMain -> Interface -> StateT (Set ModuleName) TCM r
comp IsMain
isMain Interface
i = do
      Bool
alreadyDone <- ModuleName -> Set ModuleName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Interface -> ModuleName
iModuleName Interface
i) (Set ModuleName -> Bool)
-> StateT (Set ModuleName) TCM (Set ModuleName)
-> StateT (Set ModuleName) TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (Set ModuleName) TCM (Set ModuleName)
forall s (m :: * -> *). MonadState s m => m s
get
      if Bool
alreadyDone then r -> StateT (Set ModuleName) TCM r
forall (m :: * -> *) a. Monad m => a -> m a
return r
forall a. Monoid a => a
mempty else do
        [Interface]
imps <- TCMT IO [Interface] -> StateT (Set ModuleName) TCM [Interface]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO [Interface] -> StateT (Set ModuleName) TCM [Interface])
-> TCMT IO [Interface] -> StateT (Set ModuleName) TCM [Interface]
forall a b. (a -> b) -> a -> b
$
          (ModuleInfo -> Interface) -> [ModuleInfo] -> [Interface]
forall a b. (a -> b) -> [a] -> [b]
map ModuleInfo -> Interface
miInterface ([ModuleInfo] -> [Interface])
-> ([Maybe ModuleInfo] -> [ModuleInfo])
-> [Maybe ModuleInfo]
-> [Interface]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe ModuleInfo] -> [ModuleInfo]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe ModuleInfo] -> [Interface])
-> TCMT IO [Maybe ModuleInfo] -> TCMT IO [Interface]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
            ((ModuleName, Hash) -> TCMT IO (Maybe ModuleInfo))
-> [(ModuleName, Hash)] -> TCMT IO [Maybe ModuleInfo]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (TopLevelModuleName -> TCMT IO (Maybe ModuleInfo)
getVisitedModule (TopLevelModuleName -> TCMT IO (Maybe ModuleInfo))
-> ((ModuleName, Hash) -> TopLevelModuleName)
-> (ModuleName, Hash)
-> TCMT IO (Maybe ModuleInfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> TopLevelModuleName
toTopLevelModuleName (ModuleName -> TopLevelModuleName)
-> ((ModuleName, Hash) -> ModuleName)
-> (ModuleName, Hash)
-> TopLevelModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleName, Hash) -> ModuleName
forall a b. (a, b) -> a
fst) (Interface -> [(ModuleName, Hash)]
iImportedModules Interface
i)
        r
ri <- [r] -> r
forall a. Monoid a => [a] -> a
mconcat ([r] -> r)
-> StateT (Set ModuleName) TCM [r] -> StateT (Set ModuleName) TCM r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Interface -> StateT (Set ModuleName) TCM r)
-> [Interface] -> StateT (Set ModuleName) TCM [r]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (IsMain -> Interface -> StateT (Set ModuleName) TCM r
comp IsMain
NotMain) [Interface]
imps
        TCMT IO () -> StateT (Set ModuleName) TCM ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO () -> StateT (Set ModuleName) TCM ())
-> TCMT IO () -> StateT (Set ModuleName) TCM ()
forall a b. (a -> b) -> a -> b
$ Interface -> TCMT IO ()
setInterface Interface
i
        r
r <- TCM r -> StateT (Set ModuleName) TCM r
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM r -> StateT (Set ModuleName) TCM r)
-> TCM r -> StateT (Set ModuleName) TCM r
forall a b. (a -> b) -> a -> b
$ IsMain -> Interface -> TCM r
f IsMain
isMain Interface
i
        (Set ModuleName -> Set ModuleName)
-> StateT (Set ModuleName) TCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (ModuleName -> Set ModuleName -> Set ModuleName
forall a. Ord a => a -> Set a -> Set a
Set.insert (ModuleName -> Set ModuleName -> Set ModuleName)
-> ModuleName -> Set ModuleName -> Set ModuleName
forall a b. (a -> b) -> a -> b
$ Interface -> ModuleName
iModuleName Interface
i)
        r -> StateT (Set ModuleName) TCM r
forall (m :: * -> *) a. Monad m => a -> m a
return (r -> StateT (Set ModuleName) TCM r)
-> r -> StateT (Set ModuleName) TCM r
forall a b. (a -> b) -> a -> b
$ r -> r -> r
forall a. Monoid a => a -> a -> a
mappend r
ri r
r

setInterface :: Interface -> TCM ()
setInterface :: Interface -> TCMT IO ()
setInterface Interface
i = do
  CommandLineOptions
opts <- (TCState -> CommandLineOptions) -> TCMT IO CommandLineOptions
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC (PersistentTCState -> CommandLineOptions
stPersistentOptions (PersistentTCState -> CommandLineOptions)
-> (TCState -> PersistentTCState) -> TCState -> CommandLineOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState)
  CommandLineOptions -> TCMT IO ()
setCommandLineOptions CommandLineOptions
opts
  (OptionsPragma -> TCMT IO ()) -> [OptionsPragma] -> TCMT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ OptionsPragma -> TCMT IO ()
setOptionsFromPragma (Interface -> [OptionsPragma]
iPragmaOptions Interface
i)
  Lens' (Set ModuleName) TCState
stImportedModules Lens' (Set ModuleName) TCState -> Set ModuleName -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` [ModuleName] -> Set ModuleName
forall a. Ord a => [a] -> Set a
Set.fromList (((ModuleName, Hash) -> ModuleName)
-> [(ModuleName, Hash)] -> [ModuleName]
forall a b. (a -> b) -> [a] -> [b]
map (ModuleName, Hash) -> ModuleName
forall a b. (a, b) -> a
fst ([(ModuleName, Hash)] -> [ModuleName])
-> [(ModuleName, Hash)] -> [ModuleName]
forall a b. (a -> b) -> a -> b
$ Interface -> [(ModuleName, Hash)]
iImportedModules Interface
i)
  Lens' (Maybe ModuleName) TCState
stCurrentModule   Lens' (Maybe ModuleName) TCState -> Maybe ModuleName -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` ModuleName -> Maybe ModuleName
forall a. a -> Maybe a
Just (Interface -> ModuleName
iModuleName Interface
i)

curIF :: TCM Interface
curIF :: TCM Interface
curIF = do
  Maybe ModuleName
mName <- Lens' (Maybe ModuleName) TCState -> TCMT IO (Maybe ModuleName)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Maybe ModuleName) TCState
stCurrentModule
  case Maybe ModuleName
mName of
    Maybe ModuleName
Nothing   -> TCM Interface
forall a. HasCallStack => a
__IMPOSSIBLE__
    Just ModuleName
name -> do
      Maybe ModuleInfo
mm <- TopLevelModuleName -> TCMT IO (Maybe ModuleInfo)
getVisitedModule (ModuleName -> TopLevelModuleName
toTopLevelModuleName ModuleName
name)
      case Maybe ModuleInfo
mm of
        Maybe ModuleInfo
Nothing -> TCM Interface
forall a. HasCallStack => a
__IMPOSSIBLE__
        Just ModuleInfo
mi -> Interface -> TCM Interface
forall (m :: * -> *) a. Monad m => a -> m a
return (Interface -> TCM Interface) -> Interface -> TCM Interface
forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Interface
miInterface ModuleInfo
mi


curSig :: TCM Signature
curSig :: TCM Signature
curSig = Interface -> Signature
iSignature (Interface -> Signature) -> TCM Interface -> TCM Signature
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Interface
curIF

curMName :: TCM ModuleName
curMName :: TCM ModuleName
curMName = Signature -> ModuleName
sigMName (Signature -> ModuleName) -> TCM Signature -> TCM ModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Signature
curSig

curDefs :: TCM Definitions
curDefs :: TCM Definitions
curDefs = (Definitions -> Definitions) -> TCM Definitions -> TCM Definitions
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Definition -> Bool) -> Definitions -> Definitions
forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
HMap.filter (Bool -> Bool
not (Bool -> Bool) -> (Definition -> Bool) -> Definition -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Bool
defNoCompilation)) (TCM Definitions -> TCM Definitions)
-> TCM Definitions -> TCM Definitions
forall a b. (a -> b) -> a -> b
$ (Signature -> Lens' Definitions Signature -> Definitions
forall o i. o -> Lens' i o -> i
^. Lens' Definitions Signature
sigDefinitions) (Signature -> Definitions) -> TCM Signature -> TCM Definitions
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Signature
curSig

sortDefs :: Definitions -> [(QName, Definition)]
sortDefs :: Definitions -> [(QName, Definition)]
sortDefs Definitions
defs =
  -- The list is sorted to ensure that the order of the generated
  -- definitions does not depend on things like the number of bits
  -- in an Int (see Issue 1900).
  ((QName, Definition) -> (QName, Definition) -> Ordering)
-> [(QName, Definition)] -> [(QName, Definition)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (QName -> QName -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (QName -> QName -> Ordering)
-> ((QName, Definition) -> QName)
-> (QName, Definition)
-> (QName, Definition)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (QName, Definition) -> QName
forall a b. (a, b) -> a
fst) ([(QName, Definition)] -> [(QName, Definition)])
-> [(QName, Definition)] -> [(QName, Definition)]
forall a b. (a -> b) -> a -> b
$
  Definitions -> [(QName, Definition)]
forall k v. HashMap k v -> [(k, v)]
HMap.toList Definitions
defs

sigMName :: Signature -> ModuleName
sigMName :: Signature -> ModuleName
sigMName Signature
sig = case Map ModuleName Section -> [ModuleName]
forall k a. Map k a -> [k]
Map.keys (Signature
sig Signature
-> Lens' (Map ModuleName Section) Signature
-> Map ModuleName Section
forall o i. o -> Lens' i o -> i
^. Lens' (Map ModuleName Section) Signature
sigSections) of
  []    -> ModuleName
forall a. HasCallStack => a
__IMPOSSIBLE__
  ModuleName
m : [ModuleName]
_ -> ModuleName
m


compileDir :: TCM FilePath
compileDir :: TCM String
compileDir = do
  Maybe String
mdir <- CommandLineOptions -> Maybe String
optCompileDir (CommandLineOptions -> Maybe String)
-> TCMT IO CommandLineOptions -> TCMT IO (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  case Maybe String
mdir of
    Just String
dir -> String -> TCM String
forall (m :: * -> *) a. Monad m => a -> m a
return String
dir
    Maybe String
Nothing  -> TCM String
forall a. HasCallStack => a
__IMPOSSIBLE__


repl :: [String] -> String -> String
repl :: OptionsPragma -> ShowS
repl OptionsPragma
subs = ShowS
go where
  go :: ShowS
go (Char
'<':Char
'<':Char
c:Char
'>':Char
'>':String
s) | Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< OptionsPragma -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length OptionsPragma
subs = OptionsPragma
subs OptionsPragma -> Int -> String
forall a. [a] -> Int -> a
!! Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
go String
s
     where i :: Int
i = Char -> Int
ord Char
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Char -> Int
ord Char
'0'
  go (Char
c:String
s) = Char
c Char -> ShowS
forall a. a -> [a] -> [a]
: ShowS
go String
s
  go []    = []


-- | Sets up the compilation environment.
inCompilerEnv :: Interface -> TCM a -> TCM a
inCompilerEnv :: Interface -> TCM a -> TCM a
inCompilerEnv Interface
mainI TCM a
cont = do
  -- Preserve the state (the compiler modifies the state).
  -- Andreas, 2014-03-23 But we might want to collect Benchmark info,
  -- so use localTCState.
  -- FNF, 2017-02-22 we also want to keep the warnings we have encountered,
  -- so use localTCStateSaving and pick them out.
  (a
a , TCState
s) <- TCM a -> TCM (a, TCState)
forall a. TCM a -> TCM (a, TCState)
localTCStateSaving (TCM a -> TCM (a, TCState)) -> TCM a -> TCM (a, TCState)
forall a b. (a -> b) -> a -> b
$ do

    -- Compute the output directory. Note: using commandLineOptions would make
    -- the current pragma options persistent when we setCommandLineOptions
    -- below.
    CommandLineOptions
opts <- (TCState -> CommandLineOptions) -> TCMT IO CommandLineOptions
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC ((TCState -> CommandLineOptions) -> TCMT IO CommandLineOptions)
-> (TCState -> CommandLineOptions) -> TCMT IO CommandLineOptions
forall a b. (a -> b) -> a -> b
$ PersistentTCState -> CommandLineOptions
stPersistentOptions (PersistentTCState -> CommandLineOptions)
-> (TCState -> PersistentTCState) -> TCState -> CommandLineOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState
    String
compileDir <- case CommandLineOptions -> Maybe String
optCompileDir CommandLineOptions
opts of
      Just String
dir -> String -> TCM String
forall (m :: * -> *) a. Monad m => a -> m a
return String
dir
      Maybe String
Nothing  -> do
        -- The default output directory is the project root.
        let tm :: TopLevelModuleName
tm = ModuleName -> TopLevelModuleName
toTopLevelModuleName (ModuleName -> TopLevelModuleName)
-> ModuleName -> TopLevelModuleName
forall a b. (a -> b) -> a -> b
$ Interface -> ModuleName
iModuleName Interface
mainI
        AbsolutePath
f <- SourceFile -> AbsolutePath
srcFilePath (SourceFile -> AbsolutePath)
-> TCMT IO SourceFile -> TCMT IO AbsolutePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TopLevelModuleName -> TCMT IO SourceFile
findFile TopLevelModuleName
tm
        String -> TCM String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> TCM String) -> String -> TCM String
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> String
filePath (AbsolutePath -> String) -> AbsolutePath -> String
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> TopLevelModuleName -> AbsolutePath
C.projectRoot AbsolutePath
f TopLevelModuleName
tm
    CommandLineOptions -> TCMT IO ()
setCommandLineOptions (CommandLineOptions -> TCMT IO ())
-> CommandLineOptions -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
      CommandLineOptions
opts { optCompileDir :: Maybe String
optCompileDir = String -> Maybe String
forall a. a -> Maybe a
Just String
compileDir }

    -- Andreas, 2017-08-23, issue #2714 recover pragma option --no-main
    -- Unfortunately, a pragma option is stored in the interface file as
    -- just a list of strings, thus, the solution is a bit of hack:
    -- We match on whether @["--no-main"]@ is one of the stored options.
    Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([String
"--no-main"] OptionsPragma -> [OptionsPragma] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Interface -> [OptionsPragma]
iPragmaOptions Interface
mainI) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
      Lens' PragmaOptions TCState
stPragmaOptions Lens' PragmaOptions TCState
-> (PragmaOptions -> PragmaOptions) -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` \ PragmaOptions
o -> PragmaOptions
o { optCompileNoMain :: Bool
optCompileNoMain = Bool
True }

    ScopeInfo -> TCMT IO ()
setScope (Interface -> ScopeInfo
iInsideScope Interface
mainI) -- so that compiler errors don't use overly qualified names
    TCM a -> TCM a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode TCM a
cont
  -- keep generated warnings
  let newWarnings :: [TCWarning]
newWarnings = PostScopeState -> [TCWarning]
stPostTCWarnings (PostScopeState -> [TCWarning]) -> PostScopeState -> [TCWarning]
forall a b. (a -> b) -> a -> b
$  TCState -> PostScopeState
stPostScopeState (TCState -> PostScopeState) -> TCState -> PostScopeState
forall a b. (a -> b) -> a -> b
$ TCState
s
  Lens' [TCWarning] TCState
stTCWarnings Lens' [TCWarning] TCState -> [TCWarning] -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` [TCWarning]
newWarnings
  a -> TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

topLevelModuleName :: ModuleName -> TCM ModuleName
topLevelModuleName :: ModuleName -> TCM ModuleName
topLevelModuleName ModuleName
m = do
  -- get the names of the visited modules
  [ModuleName]
visited <- (ModuleInfo -> ModuleName) -> [ModuleInfo] -> [ModuleName]
forall a b. (a -> b) -> [a] -> [b]
List.map (Interface -> ModuleName
iModuleName (Interface -> ModuleName)
-> (ModuleInfo -> Interface) -> ModuleInfo -> ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleInfo -> Interface
miInterface) ([ModuleInfo] -> [ModuleName])
-> (Map TopLevelModuleName ModuleInfo -> [ModuleInfo])
-> Map TopLevelModuleName ModuleInfo
-> [ModuleName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map TopLevelModuleName ModuleInfo -> [ModuleInfo]
forall k a. Map k a -> [a]
Map.elems (Map TopLevelModuleName ModuleInfo -> [ModuleName])
-> TCMT IO (Map TopLevelModuleName ModuleInfo)
-> TCMT IO [ModuleName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    TCMT IO (Map TopLevelModuleName ModuleInfo)
getVisitedModules
  -- find the module with the longest matching prefix to m
  let ms :: [ModuleName]
ms = (ModuleName -> ModuleName -> Ordering)
-> [ModuleName] -> [ModuleName]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> (ModuleName -> Int) -> ModuleName -> ModuleName -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ([Name] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Name] -> Int) -> (ModuleName -> [Name]) -> ModuleName -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> [Name]
mnameToList)) ([ModuleName] -> [ModuleName]) -> [ModuleName] -> [ModuleName]
forall a b. (a -> b) -> a -> b
$
       (ModuleName -> Bool) -> [ModuleName] -> [ModuleName]
forall a. (a -> Bool) -> [a] -> [a]
List.filter (\ ModuleName
m' -> ModuleName -> [Name]
mnameToList ModuleName
m' [Name] -> [Name] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` ModuleName -> [Name]
mnameToList ModuleName
m) [ModuleName]
visited
  case [ModuleName]
ms of
    (ModuleName
m' : [ModuleName]
_) -> ModuleName -> TCM ModuleName
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleName
m'
    -- if we did not get anything, it may be because m is a section
    -- (a module _ ), see e.g. #1866
    []       -> TCM ModuleName
curMName