{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.Compiler.Common
  ( module Agda.Compiler.Common
  , IsMain(..)
  )
  where

import Prelude hiding ((!!))

import Data.List (sortBy, isPrefixOf)
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 (on)

import Control.Monad
import Control.Monad.State

import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.TopLevelModuleName

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

import Agda.TypeChecking.Monad as TCM

import Agda.Utils.FileName
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.List1          ( pattern (:|) )
import Agda.Utils.Maybe
import Agda.Utils.WithDefault    ( lensCollapseDefault )

import Agda.Utils.Impossible

doCompile :: Monoid r => (IsMain -> Interface -> TCM r) -> IsMain -> Interface -> TCM r
doCompile :: forall r.
Monoid r =>
(IsMain -> Interface -> TCM r) -> IsMain -> Interface -> TCM r
doCompile IsMain -> Interface -> TCM r
f IsMain
isMain Interface
i = do
  (StateT (Set ModuleName) (TCMT IO) r -> Set ModuleName -> TCM r)
-> Set ModuleName -> StateT (Set ModuleName) (TCMT IO) r -> TCM r
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT (Set ModuleName) (TCMT IO) 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) (TCMT IO) r -> TCM r)
-> StateT (Set ModuleName) (TCMT IO) r -> TCM r
forall a b. (a -> b) -> a -> b
$ StateT (Set ModuleName) (TCMT IO) r
-> StateT (Set ModuleName) (TCMT IO) r
compilePrim (StateT (Set ModuleName) (TCMT IO) r
 -> StateT (Set ModuleName) (TCMT IO) r)
-> StateT (Set ModuleName) (TCMT IO) r
-> StateT (Set ModuleName) (TCMT IO) r
forall a b. (a -> b) -> a -> b
$ (IsMain -> Interface -> TCM r)
-> IsMain -> Interface -> StateT (Set ModuleName) (TCMT IO) r
forall r.
Monoid r =>
(IsMain -> Interface -> TCM r)
-> IsMain -> Interface -> StateT (Set ModuleName) (TCMT IO) r
doCompile' IsMain -> Interface -> TCM r
f IsMain
isMain Interface
i
  where
  -- The Agda.Primitive module is only loaded if the --no-load-primitives flag was not given,
  -- thus, only try to compile it if we have visited it.
  compilePrim :: StateT (Set ModuleName) (TCMT IO) r
-> StateT (Set ModuleName) (TCMT IO) r
compilePrim StateT (Set ModuleName) (TCMT IO) r
cont = do
    Maybe ModuleInfo
agdaPrim <- TCMT IO (Maybe ModuleInfo)
-> StateT (Set ModuleName) (TCMT IO) (Maybe ModuleInfo)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Set ModuleName) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO (Maybe ModuleInfo)
 -> StateT (Set ModuleName) (TCMT IO) (Maybe ModuleInfo))
-> TCMT IO (Maybe ModuleInfo)
-> StateT (Set ModuleName) (TCMT IO) (Maybe ModuleInfo)
forall a b. (a -> b) -> a -> b
$ do
      TopLevelModuleName
agdaPrim <- RawTopLevelModuleName -> TCM TopLevelModuleName
TCM.topLevelModuleName RawTopLevelModuleName
agdaPrim
      TopLevelModuleName
-> Map TopLevelModuleName ModuleInfo -> Maybe ModuleInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TopLevelModuleName
agdaPrim (Map TopLevelModuleName ModuleInfo -> Maybe ModuleInfo)
-> TCMT IO (Map TopLevelModuleName ModuleInfo)
-> TCMT IO (Maybe ModuleInfo)
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
    case Maybe ModuleInfo
agdaPrim of
      Maybe ModuleInfo
Nothing   -> StateT (Set ModuleName) (TCMT IO) r
cont
      Just ModuleInfo
prim ->
        r -> r -> r
forall a. Monoid a => a -> a -> a
mappend (r -> r -> r)
-> StateT (Set ModuleName) (TCMT IO) r
-> StateT (Set ModuleName) (TCMT IO) (r -> r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (IsMain -> Interface -> TCM r)
-> IsMain -> Interface -> StateT (Set ModuleName) (TCMT IO) r
forall r.
Monoid r =>
(IsMain -> Interface -> TCM r)
-> IsMain -> Interface -> StateT (Set ModuleName) (TCMT IO) r
doCompile' IsMain -> Interface -> TCM r
f IsMain
NotMain (ModuleInfo -> Interface
miInterface ModuleInfo
prim) StateT (Set ModuleName) (TCMT IO) (r -> r)
-> StateT (Set ModuleName) (TCMT IO) r
-> StateT (Set ModuleName) (TCMT IO) r
forall a b.
StateT (Set ModuleName) (TCMT IO) (a -> b)
-> StateT (Set ModuleName) (TCMT IO) a
-> StateT (Set ModuleName) (TCMT IO) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT (Set ModuleName) (TCMT IO) r
cont
    where
    agdaPrim :: RawTopLevelModuleName
agdaPrim = RawTopLevelModuleName
      { rawModuleNameRange :: Range
rawModuleNameRange = Range
forall a. Monoid a => a
mempty
      , rawModuleNameParts :: TopLevelModuleNameParts
rawModuleNameParts = Text
"Agda" Text -> [Text] -> TopLevelModuleNameParts
forall a. a -> [a] -> NonEmpty a
:| Text
"Primitive" Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: []
      }
      -- N.B. The Range in TopLevelModuleName is ignored for Ord, so we can set it to mempty.

-- 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' :: forall r.
Monoid r =>
(IsMain -> Interface -> TCM r)
-> IsMain -> Interface -> StateT (Set ModuleName) (TCMT IO) r
doCompile' IsMain -> Interface -> TCM r
f IsMain
isMain Interface
i = do
  Bool
alreadyDone <- (Set ModuleName -> Bool) -> StateT (Set ModuleName) (TCMT IO) 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) (TCMT IO) r
forall a. a -> StateT (Set ModuleName) (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return r
forall a. Monoid a => a
mempty else do
    [Interface]
imps <- TCM [Interface] -> StateT (Set ModuleName) (TCMT IO) [Interface]
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Set ModuleName) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM [Interface] -> StateT (Set ModuleName) (TCMT IO) [Interface])
-> TCM [Interface] -> StateT (Set ModuleName) (TCMT IO) [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] -> TCM [Interface]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        ((TopLevelModuleName, Hash) -> TCMT IO (Maybe ModuleInfo))
-> [(TopLevelModuleName, Hash)] -> TCMT IO [Maybe ModuleInfo]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (TopLevelModuleName -> TCMT IO (Maybe ModuleInfo)
forall (m :: * -> *).
ReadTCState m =>
TopLevelModuleName -> m (Maybe ModuleInfo)
getVisitedModule (TopLevelModuleName -> TCMT IO (Maybe ModuleInfo))
-> ((TopLevelModuleName, Hash) -> TopLevelModuleName)
-> (TopLevelModuleName, Hash)
-> TCMT IO (Maybe ModuleInfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopLevelModuleName, Hash) -> TopLevelModuleName
forall a b. (a, b) -> a
fst) (Interface -> [(TopLevelModuleName, Hash)]
iImportedModules Interface
i)
    r
ri <- [r] -> r
forall a. Monoid a => [a] -> a
mconcat ([r] -> r)
-> StateT (Set ModuleName) (TCMT IO) [r]
-> StateT (Set ModuleName) (TCMT IO) r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Interface -> StateT (Set ModuleName) (TCMT IO) r)
-> [Interface] -> StateT (Set ModuleName) (TCMT IO) [r]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((IsMain -> Interface -> TCM r)
-> IsMain -> Interface -> StateT (Set ModuleName) (TCMT IO) r
forall r.
Monoid r =>
(IsMain -> Interface -> TCM r)
-> IsMain -> Interface -> StateT (Set ModuleName) (TCMT IO) r
doCompile' IsMain -> Interface -> TCM r
f IsMain
NotMain) [Interface]
imps
    TCMT IO () -> StateT (Set ModuleName) (TCMT IO) ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Set ModuleName) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO () -> StateT (Set ModuleName) (TCMT IO) ())
-> TCMT IO () -> StateT (Set ModuleName) (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ Interface -> TCMT IO ()
setInterface Interface
i
    r
r <- TCM r -> StateT (Set ModuleName) (TCMT IO) r
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Set ModuleName) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM r -> StateT (Set ModuleName) (TCMT IO) r)
-> TCM r -> StateT (Set ModuleName) (TCMT IO) r
forall a b. (a -> b) -> a -> b
$ IsMain -> Interface -> TCM r
f IsMain
isMain Interface
i
    (Set ModuleName -> Set ModuleName)
-> StateT (Set ModuleName) (TCMT IO) ()
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) (TCMT IO) r
forall a. a -> StateT (Set ModuleName) (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (r -> StateT (Set ModuleName) (TCMT IO) r)
-> r -> StateT (Set ModuleName) (TCMT IO) 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)
  -- One could perhaps make the following command lazy. Note, however,
  -- that it doesn't suffice to replace setTCLens' with setTCLens,
  -- because the stPreImportedModules field is strict.
  (Set TopLevelModuleName -> f (Set TopLevelModuleName))
-> TCState -> f TCState
Lens' TCState (Set TopLevelModuleName)
stImportedModules Lens' TCState (Set TopLevelModuleName)
-> Set TopLevelModuleName -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens'`
    [TopLevelModuleName] -> Set TopLevelModuleName
forall a. Ord a => [a] -> Set a
Set.fromList (((TopLevelModuleName, Hash) -> TopLevelModuleName)
-> [(TopLevelModuleName, Hash)] -> [TopLevelModuleName]
forall a b. (a -> b) -> [a] -> [b]
map (TopLevelModuleName, Hash) -> TopLevelModuleName
forall a b. (a, b) -> a
fst (Interface -> [(TopLevelModuleName, Hash)]
iImportedModules Interface
i))
  (Maybe (ModuleName, TopLevelModuleName)
 -> f (Maybe (ModuleName, TopLevelModuleName)))
-> TCState -> f TCState
Lens' TCState (Maybe (ModuleName, TopLevelModuleName))
stCurrentModule Lens' TCState (Maybe (ModuleName, TopLevelModuleName))
-> Maybe (ModuleName, TopLevelModuleName) -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens'`
    (ModuleName, TopLevelModuleName)
-> Maybe (ModuleName, TopLevelModuleName)
forall a. a -> Maybe a
Just (Interface -> ModuleName
iModuleName Interface
i, Interface -> TopLevelModuleName
iTopLevelModuleName Interface
i)

curIF :: ReadTCState m => m Interface
curIF :: forall (m :: * -> *). ReadTCState m => m Interface
curIF = do
  TopLevelModuleName
name <- m TopLevelModuleName
forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
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 TopLevelModuleName
name

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

curDefs :: ReadTCState m => m Definitions
curDefs :: forall (m :: * -> *). ReadTCState m => 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' Signature Definitions -> Definitions
forall o i. o -> Lens' o i -> i
^. (Definitions -> f Definitions) -> Signature -> f Signature
Lens' Signature Definitions
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]
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 :: forall (m :: * -> *). HasOptions m => m FilePath
compileDir = do
  Maybe FilePath
mdir <- CommandLineOptions -> Maybe FilePath
optCompileDir (CommandLineOptions -> Maybe FilePath)
-> m CommandLineOptions -> m (Maybe FilePath)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  m FilePath
-> (FilePath -> m FilePath) -> Maybe FilePath -> m FilePath
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m FilePath
forall a. HasCallStack => a
__IMPOSSIBLE__ FilePath -> m FilePath
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe FilePath
mdir


repl :: [String] -> String -> String
repl :: [FilePath] -> FilePath -> FilePath
repl [FilePath]
subs = FilePath -> FilePath
go where
  go :: FilePath -> FilePath
go (Char
'<':Char
'<':Char
c:Char
'>':Char
'>':FilePath
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
< [FilePath] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FilePath]
subs = [FilePath]
subs [FilePath] -> Int -> FilePath
forall a. HasCallStack => [a] -> Int -> a
!! Int
i FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
go FilePath
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:FilePath
s) = Char
c Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath -> FilePath
go FilePath
s
  go []    = []


-- | Sets up the compilation environment.
inCompilerEnv :: CheckResult -> TCM a -> TCM a
inCompilerEnv :: forall a. 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 :: FilePath
compileDir = case CommandLineOptions -> Maybe FilePath
optCompileDir CommandLineOptions
opts of
          Just FilePath
dir -> FilePath
dir
          Maybe FilePath
Nothing  ->
            -- The default output directory is the project root.
            let tm :: TopLevelModuleName
tm = Interface -> TopLevelModuleName
iTopLevelModuleName 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 -> FilePath
filePath (AbsolutePath -> FilePath) -> AbsolutePath -> FilePath
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> TopLevelModuleName -> AbsolutePath
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 = Just 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.
    let iFilePragmaStrings :: Interface -> [[FilePath]]
iFilePragmaStrings = (OptionsPragma -> [FilePath]) -> [OptionsPragma] -> [[FilePath]]
forall a b. (a -> b) -> [a] -> [b]
map OptionsPragma -> [FilePath]
pragmaStrings ([OptionsPragma] -> [[FilePath]])
-> (Interface -> [OptionsPragma]) -> Interface -> [[FilePath]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interface -> [OptionsPragma]
iFilePragmaOptions
    Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([FilePath
"--no-main"] [FilePath] -> [[FilePath]] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Interface -> [[FilePath]]
iFilePragmaStrings Interface
mainI) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
      Lens' TCState Bool -> Bool -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
setTCLens ((PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
Lens' TCState PragmaOptions
stPragmaOptions ((PragmaOptions -> f PragmaOptions) -> TCState -> f TCState)
-> ((Bool -> f Bool) -> PragmaOptions -> f PragmaOptions)
-> (Bool -> f Bool)
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WithDefault 'True -> f (WithDefault 'True))
-> PragmaOptions -> f PragmaOptions
forall (f :: * -> *).
Functor f =>
(WithDefault 'True -> f (WithDefault 'True))
-> PragmaOptions -> f PragmaOptions
lensOptCompileMain ((WithDefault 'True -> f (WithDefault 'True))
 -> PragmaOptions -> f PragmaOptions)
-> ((Bool -> f Bool) -> WithDefault 'True -> f (WithDefault 'True))
-> (Bool -> f Bool)
-> PragmaOptions
-> f PragmaOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> f Bool) -> WithDefault 'True -> f (WithDefault 'True)
forall a (b :: Bool).
(Boolean a, KnownBool b) =>
Lens' (WithDefault' a b) a
Lens' (WithDefault 'True) Bool
lensCollapseDefault) Bool
False

    -- 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 (([FilePath] -> Bool) -> [[FilePath]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (FilePath
"--cubical" FilePath -> [FilePath] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`) ([[FilePath]] -> Bool) -> [[FilePath]] -> Bool
forall a b. (a -> b) -> a -> b
$ Interface -> [[FilePath]]
iFilePragmaStrings Interface
mainI) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
      Lens' TCState (Maybe Cubical) -> Maybe Cubical -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
setTCLens ((PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
Lens' TCState PragmaOptions
stPragmaOptions ((PragmaOptions -> f PragmaOptions) -> TCState -> f TCState)
-> ((Maybe Cubical -> f (Maybe Cubical))
    -> PragmaOptions -> f PragmaOptions)
-> (Maybe Cubical -> f (Maybe Cubical))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Cubical -> f (Maybe Cubical))
-> PragmaOptions -> f PragmaOptions
forall (f :: * -> *).
Functor f =>
(Maybe Cubical -> f (Maybe Cubical))
-> PragmaOptions -> f PragmaOptions
lensOptCubical) (Maybe Cubical -> TCMT IO ()) -> Maybe Cubical -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Cubical -> Maybe Cubical
forall a. a -> Maybe a
Just Cubical
CFull
    Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (([FilePath] -> Bool) -> [[FilePath]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (FilePath
"--erased-cubical" FilePath -> [FilePath] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`) ([[FilePath]] -> Bool) -> [[FilePath]] -> Bool
forall a b. (a -> b) -> a -> b
$ Interface -> [[FilePath]]
iFilePragmaStrings Interface
mainI) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
      Lens' TCState (Maybe Cubical) -> Maybe Cubical -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
setTCLens ((PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
Lens' TCState PragmaOptions
stPragmaOptions ((PragmaOptions -> f PragmaOptions) -> TCState -> f TCState)
-> ((Maybe Cubical -> f (Maybe Cubical))
    -> PragmaOptions -> f PragmaOptions)
-> (Maybe Cubical -> f (Maybe Cubical))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Cubical -> f (Maybe Cubical))
-> PragmaOptions -> f PragmaOptions
forall (f :: * -> *).
Functor f =>
(Maybe Cubical -> f (Maybe Cubical))
-> PragmaOptions -> f PragmaOptions
lensOptCubical) (Maybe Cubical -> TCMT IO ()) -> Maybe Cubical -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ 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
  ([TCWarning] -> f [TCWarning]) -> TCState -> f TCState
Lens' TCState [TCWarning]
stTCWarnings Lens' TCState [TCWarning] -> [TCWarning] -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> a -> m ()
`setTCLens` [TCWarning]
newWarnings
  a -> TCM a
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

topLevelModuleName ::
  ReadTCState m => ModuleName -> m TopLevelModuleName
topLevelModuleName :: forall (m :: * -> *).
ReadTCState m =>
ModuleName -> m TopLevelModuleName
topLevelModuleName ModuleName
m = do
  -- Interfaces of visited modules.
  [Interface]
visited <- (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])
-> m (Map TopLevelModuleName ModuleInfo) -> m [Interface]
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 is :: [Interface]
is = (Interface -> Interface -> Ordering) -> [Interface] -> [Interface]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> (Interface -> Int) -> Interface -> Interface -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ([Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Name] -> Int) -> (Interface -> [Name]) -> Interface -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> [Name]
mnameToList (ModuleName -> [Name])
-> (Interface -> ModuleName) -> Interface -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interface -> ModuleName
iModuleName)) ([Interface] -> [Interface]) -> [Interface] -> [Interface]
forall a b. (a -> b) -> a -> b
$
           (Interface -> Bool) -> [Interface] -> [Interface]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Interface
i -> ModuleName -> [Name]
mnameToList (Interface -> ModuleName
iModuleName Interface
i) [Name] -> [Name] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf`
                         ModuleName -> [Name]
mnameToList ModuleName
m)
             [Interface]
visited
  case [Interface]
is of
    (Interface
i : [Interface]
_) -> TopLevelModuleName -> m TopLevelModuleName
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Interface -> TopLevelModuleName
iTopLevelModuleName Interface
i)
    -- if we did not get anything, it may be because m is a section
    -- (a module _ ), see e.g. #1866
    []       -> m TopLevelModuleName
forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
curMName