    {-# 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.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
        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
          agdaPrim <- RawTopLevelModuleName -> TCM TopLevelModuleName
    TCM.topLevelModuleName RawTopLevelModuleName
    agdaPrim
          Map.lookup agdaPrim <$> getVisitedModules
        case 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]
    : []
          , rawModuleNameInferred :: Bool
    rawModuleNameInferred = Bool
    False
          }
          -- 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
      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 alreadyDone then return mempty else do
        imps <- lift $
          map miInterface . catMaybes <$>
            mapM (getVisitedModule . fst) (iImportedModules i)
        ri <- mconcat <$> mapM (doCompile' f NotMain) imps
        lift $ setInterface i
        r <- lift $ f isMain i
        modify (Set.insert $ iModuleName i)
        return $ mappend ri r

    setInterface :: Interface -> TCM ()
    setInterface :: Interface -> TCMT IO ()
    setInterface Interface
    i = do
      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)
      setCommandLineOptions opts
      mapM_ setOptionsFromPragma (iDefaultPragmaOptions i ++ iFilePragmaOptions 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.
      stImportedModules `setTCLens'`
        Set.fromList (map fst (iImportedModules i))
      stCurrentModule `setTCLens'`
        Just (iModuleName i, iTopLevelModuleName i)

    curIF :: ReadTCState m => m Interface
    curIF :: forall (m :: * -> *). ReadTCState m => m Interface
    curIF = do
      name <- m TopLevelModuleName
    forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
    curMName
      maybe __IMPOSSIBLE__ miInterface <$> getVisitedModule 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 String
    compileDir = do
      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
      maybe __IMPOSSIBLE__ return mdir

    repl :: [String] -> String -> String
    repl :: [String] -> String -> String
    repl [String]
    subs = String -> String
    go where
      go :: String -> String
    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
    < [String] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [String]
    subs = [String]
    subs [String] -> Int -> String
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    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 -> String -> String
    forall a. a -> [a] -> [a]
    : String -> String
    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 , 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.
        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
        compileDir <- case optCompileDir opts of
            Just String
    dir -> String -> TCMT IO String
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure String
    dir
            Maybe String
    Nothing  -> do
              -- The default output directory is the project root.
              let tm :: TopLevelModuleName
    tm = Interface -> TopLevelModuleName
    iTopLevelModuleName Interface
    mainI
              f <- SourceFile -> TCMT IO AbsolutePath
    forall (m :: * -> *). MonadFileId m => SourceFile -> m AbsolutePath
    srcFilePath (SourceFile -> TCMT IO AbsolutePath)
    -> SourceFile -> TCMT IO AbsolutePath
    forall a b. (a -> b) -> a -> b
    $ Source -> SourceFile
    srcOrigin Source
    checkedSource
              pure $ filePath $ projectRoot f tm
        setCommandLineOptions $
          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 = (OptionsPragma -> [String]) -> [OptionsPragma] -> [[String]]
    forall a b. (a -> b) -> [a] -> [b]
    map OptionsPragma -> [String]
    pragmaStrings ([OptionsPragma] -> [[String]])
    -> (Interface -> [OptionsPragma]) -> Interface -> [[String]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Interface -> [OptionsPragma]
    iFilePragmaOptions
        when (["--no-main"] `elem` iFilePragmaStrings mainI) $
          setTCLens (stPragmaOptions . lensOptCompileMain . lensCollapseDefault) 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:
        when (any ("--cubical" `elem`) $ iFilePragmaStrings mainI) $
          setTCLens (stPragmaOptions . lensOptCubical) $ Just CFull
        when (any ("--erased-cubical" `elem`) $ iFilePragmaStrings mainI) $
          setTCLens (stPragmaOptions . lensOptCubical) $ Just CErased

        setScope (iInsideScope mainI) -- so that compiler errors don't use overly qualified names
        ignoreAbstractMode cont
      -- keep generated warnings
      let newWarnings = PostScopeState -> Set TCWarning
    stPostTCWarnings (PostScopeState -> Set TCWarning)
    -> PostScopeState -> Set TCWarning
    forall a b. (a -> b) -> a -> b
    $  TCState -> PostScopeState
    stPostScopeState (TCState -> PostScopeState) -> TCState -> PostScopeState
    forall a b. (a -> b) -> a -> b
    $ TCState
    s
      stTCWarnings `setTCLens` newWarnings
      return a

    topLevelModuleName ::
      ReadTCState m => ModuleName -> m TopLevelModuleName
    topLevelModuleName :: forall (m :: * -> *).
    ReadTCState m =>
    ModuleName -> m TopLevelModuleName
    topLevelModuleName ModuleName
    m = do
      -- Interfaces of visited modules.
      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 -> 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 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