    {-# 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 :: forall r.
    Monoid r =>
    (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) (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
    $ 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 Interface
    agdaPrimInter StateT (Set ModuleName) (TCMT IO) (r -> r)
    -> StateT (Set ModuleName) (TCMT IO) r
    -> StateT (Set ModuleName) (TCMT IO) r
    forall (f :: * -> *) a b. Applicative f => 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
    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' :: 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 (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) (TCMT IO) [Interface]
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (TCMT IO [Interface]
     -> StateT (Set ModuleName) (TCMT IO) [Interface])
    -> TCMT IO [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])
    -> 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) (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)
    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 (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 (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 (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)
      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 :: forall (m :: * -> *). ReadTCState m => 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 :: forall (m :: * -> *). ReadTCState m => 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 :: 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' 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 :: forall (m :: * -> *). HasOptions m => 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 :: 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 :: 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 :: forall (m :: * -> *). ReadTCState m => 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