{-# 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

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

import Agda.Interaction.FindFile ( srcFilePath )
import Agda.Interaction.Options
import Agda.Interaction.Imports ( CheckResult, crInterface, crSource, Source(..) )

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 :: Monoid r => (IsMain -> Interface -> TCM r) -> IsMain -> Interface -> TCM r
doCompile :: (IsMain -> Interface -> TCM r) -> IsMain -> Interface -> TCM r
doCompile IsMain -> Interface -> TCM r
f IsMain
isMain Interface
i = 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)
forall (m :: * -> *).
ReadTCState m =>
m (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 -> TCM r)
-> IsMain -> Interface -> StateT (Set ModuleName) TCM r
forall r.
Monoid r =>
(IsMain -> Interface -> TCM r)
-> IsMain -> Interface -> StateT (Set ModuleName) TCM r
doCompile' IsMain -> Interface -> TCM r
f 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 -> TCM r)
-> IsMain -> Interface -> StateT (Set ModuleName) TCM r
forall r.
Monoid r =>
(IsMain -> Interface -> TCM r)
-> IsMain -> Interface -> StateT (Set ModuleName) TCM r
doCompile' IsMain -> Interface -> TCM r
f IsMain
isMain Interface
i

-- This helper function is called for both `Agda.Primitive` and the module in question.
-- It's also called for each imported module, recursively. (Avoiding duplicates).
doCompile'
  :: Monoid r
  => (IsMain -> Interface -> TCM r) -> (IsMain -> Interface -> StateT (Set ModuleName) TCM r)
doCompile' :: (IsMain -> Interface -> TCM r)
-> IsMain -> Interface -> StateT (Set ModuleName) TCM r
doCompile' IsMain -> Interface -> TCM r
f IsMain
isMain Interface
i = do
  Bool
alreadyDone <- (Set ModuleName -> Bool) -> StateT (Set ModuleName) TCM Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (ModuleName -> Set ModuleName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Interface -> ModuleName
iModuleName Interface
i))
  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])
-> TCM [Maybe ModuleInfo] -> TCMT IO [Interface]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        ((ModuleName, Hash) -> TCM (Maybe ModuleInfo))
-> [(ModuleName, Hash)] -> TCM [Maybe ModuleInfo]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (TopLevelModuleName -> TCM (Maybe ModuleInfo)
forall (m :: * -> *).
ReadTCState m =>
TopLevelModuleName -> m (Maybe ModuleInfo)
getVisitedModule (TopLevelModuleName -> TCM (Maybe ModuleInfo))
-> ((ModuleName, Hash) -> TopLevelModuleName)
-> (ModuleName, Hash)
-> TCM (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 -> TCM r)
-> IsMain -> Interface -> StateT (Set ModuleName) TCM r
forall r.
Monoid r =>
(IsMain -> Interface -> TCM r)
-> IsMain -> Interface -> StateT (Set ModuleName) TCM r
doCompile' IsMain -> Interface -> TCM r
f 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]
iDefaultPragmaOptions Interface
i [OptionsPragma] -> [OptionsPragma] -> [OptionsPragma]
forall a. [a] -> [a] -> [a]
++ Interface -> [OptionsPragma]
iFilePragmaOptions 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 :: ReadTCState m => m Interface
curIF :: m Interface
curIF = do
  ModuleName
name <- m ModuleName
forall (m :: * -> *). ReadTCState m => m ModuleName
curMName
  Interface
-> (ModuleInfo -> Interface) -> Maybe ModuleInfo -> Interface
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Interface
forall a. HasCallStack => a
__IMPOSSIBLE__ ModuleInfo -> Interface
miInterface (Maybe ModuleInfo -> Interface)
-> m (Maybe ModuleInfo) -> m Interface
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TopLevelModuleName -> m (Maybe ModuleInfo)
forall (m :: * -> *).
ReadTCState m =>
TopLevelModuleName -> m (Maybe ModuleInfo)
getVisitedModule (ModuleName -> TopLevelModuleName
toTopLevelModuleName ModuleName
name)

curMName :: ReadTCState m => m ModuleName
curMName :: m ModuleName
curMName = ModuleName -> Maybe ModuleName -> ModuleName
forall a. a -> Maybe a -> a
fromMaybe ModuleName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe ModuleName -> ModuleName)
-> m (Maybe ModuleName) -> m ModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' (Maybe ModuleName) TCState -> m (Maybe ModuleName)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Maybe ModuleName) TCState
stCurrentModule

curDefs :: ReadTCState m => m Definitions
curDefs :: m Definitions
curDefs = (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) (Definitions -> Definitions)
-> (Interface -> Definitions) -> Interface -> Definitions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Signature -> Lens' Definitions Signature -> Definitions
forall o i. o -> Lens' i o -> i
^. Lens' Definitions Signature
sigDefinitions) (Signature -> Definitions)
-> (Interface -> Signature) -> Interface -> Definitions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interface -> Signature
iSignature (Interface -> Definitions) -> m Interface -> m Definitions
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Interface
forall (m :: * -> *). ReadTCState m => m Interface
curIF

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

compileDir :: HasOptions m => m FilePath
compileDir :: m String
compileDir = do
  Maybe String
mdir <- CommandLineOptions -> Maybe String
optCompileDir (CommandLineOptions -> Maybe String)
-> m CommandLineOptions -> m (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  m String -> (String -> m String) -> Maybe String -> m String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m String
forall a. HasCallStack => a
__IMPOSSIBLE__ String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe String
mdir


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 :: CheckResult -> TCM a -> TCM a
inCompilerEnv :: CheckResult -> TCM a -> TCM a
inCompilerEnv CheckResult
checkResult TCM a
cont = do
  let mainI :: Interface
mainI = CheckResult -> Interface
crInterface CheckResult
checkResult
      checkedSource :: Source
checkedSource = CheckResult -> Source
crSource CheckResult
checkResult

  -- 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
    let compileDir :: String
compileDir = case CommandLineOptions -> Maybe String
optCompileDir CommandLineOptions
opts of
          Just String
dir -> String
dir
          Maybe String
Nothing  ->
            -- 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
                f :: AbsolutePath
f  = SourceFile -> AbsolutePath
srcFilePath (SourceFile -> AbsolutePath) -> SourceFile -> AbsolutePath
forall a b. (a -> b) -> a -> b
$ Source -> SourceFile
srcOrigin Source
checkedSource
            in 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]
iFilePragmaOptions 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 }

    -- Perhaps all pragma options from the top-level module should be
    -- made available to the compiler in a suitable way. Here are more
    -- hacks:
    Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((OptionsPragma -> Bool) -> [OptionsPragma] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (String
"--cubical" String -> OptionsPragma -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`) (Interface -> [OptionsPragma]
iFilePragmaOptions 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 { optCubical :: Maybe Cubical
optCubical = Cubical -> Maybe Cubical
forall a. a -> Maybe a
Just Cubical
CFull }
    Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((OptionsPragma -> Bool) -> [OptionsPragma] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (String
"--erased-cubical" String -> OptionsPragma -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`) (Interface -> [OptionsPragma]
iFilePragmaOptions 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 { optCubical :: Maybe Cubical
optCubical = Cubical -> Maybe Cubical
forall a. a -> Maybe a
Just Cubical
CErased }

    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 :: ReadTCState m => ModuleName -> m ModuleName
topLevelModuleName :: ModuleName -> m 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])
-> m (Map TopLevelModuleName ModuleInfo) -> m [ModuleName]
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
  -- 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 -> m 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
    []       -> m ModuleName
forall (m :: * -> *). ReadTCState m => m ModuleName
curMName