    {-# LANGUAGE CPP #-}
    {-# LANGUAGE ScopedTypeVariables #-}

    module Agda.Compiler.Common where

    import Data.List as List
    import Data.Map (Map)
    import qualified Data.Map as Map
    import Data.Set (Set)
    import qualified Data.Set as Set
    import Data.Char
    import Data.Function
    import Data.Semigroup
    import Data.Monoid hiding ((<>))

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

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

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

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Pretty hiding ((<>))
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope

    import Agda.Utils.FileName
    import qualified Agda.Utils.HashMap as HMap
    import Agda.Utils.Lens
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Pretty hiding ((<>))

    #include "undefined.h"
    import Agda.Utils.Impossible

    data IsMain = IsMain | NotMain
      deriving (Eq, Show)

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

    instance Monoid IsMain where
      mempty = IsMain
      mappend = (<>)

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

    setInterface :: Interface -> TCM ()
    setInterface i = do
      opts <- getsTC (stPersistentOptions . stPersistentState)
      setCommandLineOptions opts
      mapM_ setOptionsFromPragma (iPragmaOptions i)
      stImportedModules `setTCLens` Set.fromList (map fst $ iImportedModules i)
      stCurrentModule   `setTCLens` Just (iModuleName i)

    curIF :: TCM Interface
    curIF = do
      mName <- useTC stCurrentModule
      case mName of
        Nothing   -> __IMPOSSIBLE__
        Just name -> do
          mm <- getVisitedModule (toTopLevelModuleName name)
          case mm of
            Nothing -> __IMPOSSIBLE__
            Just mi -> return $ miInterface mi

    curSig :: TCM Signature
    curSig = iSignature <$> curIF

    curMName :: TCM ModuleName
    curMName = sigMName <$> curSig

    curDefs :: TCM Definitions
    curDefs = fmap (HMap.filter (not . defNoCompilation)) $ (^. sigDefinitions) <$> curSig

    sortDefs :: Definitions -> [(QName, Definition)]
    sortDefs 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).
      List.sortBy (compare `on` fst) $
      HMap.toList defs

    sigMName :: Signature -> ModuleName
    sigMName sig = case Map.keys (sig ^. sigSections) of
      []    -> __IMPOSSIBLE__
      m : _ -> m

    compileDir :: TCM FilePath
    compileDir = do
      mdir <- optCompileDir <$> commandLineOptions
      case mdir of
        Just dir -> return dir
        Nothing  -> __IMPOSSIBLE__

    repl :: [String] -> String -> String
    repl subs = go where
      go ('<':'<':c:'>':'>':s) | 0 <= i && i < length subs = subs !! i ++ go s
         where i = ord c - ord '0'
      go (c:s) = c : go s
      go []    = []

    -- | Copy pasted from MAlonzo....
    --   Move somewhere else!
    conArityAndPars :: QName -> TCM (Nat, Nat)
    conArityAndPars q = do
      def <- getConstInfo q
      n   <- typeArity (defType def)
      let Constructor{ conPars = np } = theDef def
      return (n - np, np)

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

        -- Compute the output directory. Note: using commandLineOptions would make
        -- the current pragma options persistent when we setCommandLineOptions
        -- below.
        opts <- getsTC $ stPersistentOptions . stPersistentState
        compileDir <- case optCompileDir opts of
          Just dir -> return dir
          Nothing  -> do
            -- The default output directory is the project root.
            let tm = toTopLevelModuleName $ iModuleName mainI
            f <- findFile tm
            return $ filePath $ C.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.
        when (["--no-main"] `elem` iPragmaOptions mainI) $
          stPragmaOptions `modifyTCLens` \ o -> o { optCompileNoMain = True }

        setScope (iInsideScope mainI) -- so that compiler errors don't use overly qualified names
        ignoreAbstractMode $ do
          cont
      -- keep generated warnings
      let newWarnings = stPostTCWarnings $  stPostScopeState $ s
      stTCWarnings `setTCLens` newWarnings
      return a

    topLevelModuleName :: ModuleName -> TCM ModuleName
    topLevelModuleName m = do
      -- get the names of the visited modules
      visited <- List.map (iModuleName . miInterface) . Map.elems <$>
        getVisitedModules
      -- find the module with the longest matching prefix to m
      let ms = sortBy (compare `on` (length . mnameToList)) $
           List.filter (\ m' -> mnameToList m' `isPrefixOf` mnameToList m) visited
      case ms of
        (m' : _) -> return m'
        -- if we did not get anything, it may be because m is a section
        -- (a module _ ), see e.g. #1866
        []       -> curMName