    module Agda.Interaction.Highlighting.LaTeX.Backend
      ( latexBackend
      ) where

    import Agda.Interaction.Highlighting.LaTeX.Base
      ( LaTeXOptions(..)
      , LogLaTeXT
      , runLogLaTeXTWith
      , logMsgToText
      , generateLaTeXIO
      , prepareCommonAssets
      )

    import Control.DeepSeq
    import Control.Monad.Trans (MonadIO)

    import qualified Data.Map as Map
    import Data.Map (Map)

    import qualified Data.Text as T

    import GHC.Generics (Generic)

    import System.FilePath ( (</>) )

    import Agda.Compiler.Backend (Backend(..), Backend'(..), Definition, Recompile(..))
    import Agda.Compiler.Common (curIF, IsMain(IsMain, NotMain))

    import Agda.Interaction.Options
      ( ArgDescr(NoArg, ReqArg)
      , CommandLineOptions ( optGHCiInteraction, optPragmaOptions )
      , PragmaOptions ( optCountClusters )
      , Flag
      , OptDescr(..)
      )

    import Agda.Syntax.Abstract.Name (ModuleName, toTopLevelModuleName)
    import Agda.Syntax.Concrete.Name (TopLevelModuleName, projectRoot)

    import Agda.TypeChecking.Monad
      ( HasOptions(commandLineOptions)
      , MonadDebug
      , stModuleToSource
      , useTC
      , ReadTCState
      , reportS
      )

    import Agda.Utils.FileName (filePath, mkAbsolute)

    ------------------------------------------------------------------------
    -- * Main.

    -- Command-line flag options, prior to e.g. path resolution and validation.
    data LaTeXFlags = LaTeXFlags
      { LaTeXFlags -> FilePath
    latexFlagOutDir        :: FilePath
      , LaTeXFlags -> Maybe FilePath
    latexFlagSourceFile    :: Maybe FilePath
      , LaTeXFlags -> Bool
    latexFlagGenerateLaTeX :: Bool
        -- ^ Are we going to try to generate LaTeX at all?
      } deriving (LaTeXFlags -> LaTeXFlags -> Bool
    (LaTeXFlags -> LaTeXFlags -> Bool)
    -> (LaTeXFlags -> LaTeXFlags -> Bool) -> Eq LaTeXFlags
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: LaTeXFlags -> LaTeXFlags -> Bool
    $c/= :: LaTeXFlags -> LaTeXFlags -> Bool
    == :: LaTeXFlags -> LaTeXFlags -> Bool
    $c== :: LaTeXFlags -> LaTeXFlags -> Bool
    Eq, (forall x. LaTeXFlags -> Rep LaTeXFlags x)
    -> (forall x. Rep LaTeXFlags x -> LaTeXFlags) -> Generic LaTeXFlags
    forall x. Rep LaTeXFlags x -> LaTeXFlags
    forall x. LaTeXFlags -> Rep LaTeXFlags x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep LaTeXFlags x -> LaTeXFlags
    $cfrom :: forall x. LaTeXFlags -> Rep LaTeXFlags x
    Generic)

    instance NFData LaTeXFlags

    -- | The default output directory for LaTeX.

    defaultLaTeXDir :: FilePath
    defaultLaTeXDir :: FilePath
    defaultLaTeXDir = FilePath
    "latex"

    defaultLaTeXFlags :: LaTeXFlags
    defaultLaTeXFlags :: LaTeXFlags
    defaultLaTeXFlags = LaTeXFlags :: FilePath -> Maybe FilePath -> Bool -> LaTeXFlags
    LaTeXFlags
      { latexFlagOutDir :: FilePath
    latexFlagOutDir        = FilePath
    defaultLaTeXDir
      , latexFlagSourceFile :: Maybe FilePath
    latexFlagSourceFile    = Maybe FilePath
    forall a. Maybe a
    Nothing
      , latexFlagGenerateLaTeX :: Bool
    latexFlagGenerateLaTeX = Bool
    False
      }

    latexFlagsDescriptions :: [OptDescr (Flag LaTeXFlags)]
    latexFlagsDescriptions :: [OptDescr (Flag LaTeXFlags)]
    latexFlagsDescriptions =
      [ FilePath
    -> [FilePath]
    -> ArgDescr (Flag LaTeXFlags)
    -> FilePath
    -> OptDescr (Flag LaTeXFlags)
    forall a.
    FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
    Option []     [FilePath
    "latex"] (Flag LaTeXFlags -> ArgDescr (Flag LaTeXFlags)
    forall a. a -> ArgDescr a
    NoArg Flag LaTeXFlags
    latexFlag)
                      FilePath
    "generate LaTeX with highlighted source code"
      , FilePath
    -> [FilePath]
    -> ArgDescr (Flag LaTeXFlags)
    -> FilePath
    -> OptDescr (Flag LaTeXFlags)
    forall a.
    FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
    Option []     [FilePath
    "latex-dir"] ((FilePath -> Flag LaTeXFlags)
    -> FilePath -> ArgDescr (Flag LaTeXFlags)
    forall a. (FilePath -> a) -> FilePath -> ArgDescr a
    ReqArg FilePath -> Flag LaTeXFlags
    latexDirFlag FilePath
    "DIR")
                      (FilePath
    "directory in which LaTeX files are placed (default: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++
                        FilePath
    defaultLaTeXDir FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    ")")
      ]

    latexFlag :: Flag LaTeXFlags
    latexFlag :: Flag LaTeXFlags
    latexFlag LaTeXFlags
    o = Flag LaTeXFlags
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag LaTeXFlags -> Flag LaTeXFlags
    forall a b. (a -> b) -> a -> b
    $ LaTeXFlags
    o { latexFlagGenerateLaTeX :: Bool
    latexFlagGenerateLaTeX = Bool
    True }

    latexDirFlag :: FilePath -> Flag LaTeXFlags
    latexDirFlag :: FilePath -> Flag LaTeXFlags
    latexDirFlag FilePath
    d LaTeXFlags
    o = Flag LaTeXFlags
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag LaTeXFlags -> Flag LaTeXFlags
    forall a b. (a -> b) -> a -> b
    $ LaTeXFlags
    o { latexFlagOutDir :: FilePath
    latexFlagOutDir = FilePath
    d }

    data LaTeXCompileEnv = LaTeXCompileEnv LaTeXFlags
    data LaTeXModuleEnv  = LaTeXModuleEnv LaTeXOptions
    data LaTeXModule     = LaTeXModule
    data LaTeXDef        = LaTeXDef

    latexBackend :: Backend
    latexBackend :: Backend
    latexBackend = Backend'
      LaTeXFlags LaTeXCompileEnv LaTeXModuleEnv LaTeXModule LaTeXDef
    -> Backend
    forall opts env menv mod def.
    NFData opts =>
    Backend' opts env menv mod def -> Backend
    Backend Backend'
      LaTeXFlags LaTeXCompileEnv LaTeXModuleEnv LaTeXModule LaTeXDef
    latexBackend'

    latexBackend' :: Backend' LaTeXFlags LaTeXCompileEnv LaTeXModuleEnv LaTeXModule LaTeXDef
    latexBackend' :: Backend'
      LaTeXFlags LaTeXCompileEnv LaTeXModuleEnv LaTeXModule LaTeXDef
    latexBackend' = Backend' :: forall opts env menv mod def.
    FilePath
    -> Maybe FilePath
    -> opts
    -> [OptDescr (Flag opts)]
    -> (opts -> Bool)
    -> (opts -> TCM env)
    -> (env -> IsMain -> Map ModuleName mod -> TCM ())
    -> (env
        -> IsMain
        -> ModuleName
        -> Maybe FilePath
        -> TCM (Recompile menv mod))
    -> (env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod)
    -> (env -> menv -> IsMain -> Definition -> TCM def)
    -> Bool
    -> (QName -> TCM Bool)
    -> Backend' opts env menv mod def
    Backend'
      { backendName :: FilePath
    backendName           = FilePath
    "LaTeX"
      , backendVersion :: Maybe FilePath
    backendVersion        = Maybe FilePath
    forall a. Maybe a
    Nothing
      , options :: LaTeXFlags
    options               = LaTeXFlags
    defaultLaTeXFlags
      , commandLineFlags :: [OptDescr (Flag LaTeXFlags)]
    commandLineFlags      = [OptDescr (Flag LaTeXFlags)]
    latexFlagsDescriptions
      , isEnabled :: LaTeXFlags -> Bool
    isEnabled             = LaTeXFlags -> Bool
    latexFlagGenerateLaTeX
      , preCompile :: LaTeXFlags -> TCM LaTeXCompileEnv
    preCompile            = LaTeXFlags -> TCM LaTeXCompileEnv
    forall (m :: * -> *).
    Applicative m =>
    LaTeXFlags -> m LaTeXCompileEnv
    preCompileLaTeX
      , preModule :: LaTeXCompileEnv
    -> IsMain
    -> ModuleName
    -> Maybe FilePath
    -> TCM (Recompile LaTeXModuleEnv LaTeXModule)
    preModule             = LaTeXCompileEnv
    -> IsMain
    -> ModuleName
    -> Maybe FilePath
    -> TCM (Recompile LaTeXModuleEnv LaTeXModule)
    forall (m :: * -> *).
    (HasOptions m, ReadTCState m) =>
    LaTeXCompileEnv
    -> IsMain
    -> ModuleName
    -> Maybe FilePath
    -> m (Recompile LaTeXModuleEnv LaTeXModule)
    preModuleLaTeX
      , compileDef :: LaTeXCompileEnv
    -> LaTeXModuleEnv -> IsMain -> Definition -> TCM LaTeXDef
    compileDef            = LaTeXCompileEnv
    -> LaTeXModuleEnv -> IsMain -> Definition -> TCM LaTeXDef
    forall (m :: * -> *).
    Applicative m =>
    LaTeXCompileEnv
    -> LaTeXModuleEnv -> IsMain -> Definition -> m LaTeXDef
    compileDefLaTeX
      , postModule :: LaTeXCompileEnv
    -> LaTeXModuleEnv
    -> IsMain
    -> ModuleName
    -> [LaTeXDef]
    -> TCM LaTeXModule
    postModule            = LaTeXCompileEnv
    -> LaTeXModuleEnv
    -> IsMain
    -> ModuleName
    -> [LaTeXDef]
    -> TCM LaTeXModule
    forall (m :: * -> *).
    (MonadDebug m, ReadTCState m, MonadIO m) =>
    LaTeXCompileEnv
    -> LaTeXModuleEnv
    -> IsMain
    -> ModuleName
    -> [LaTeXDef]
    -> m LaTeXModule
    postModuleLaTeX
      , postCompile :: LaTeXCompileEnv -> IsMain -> Map ModuleName LaTeXModule -> TCM ()
    postCompile           = LaTeXCompileEnv -> IsMain -> Map ModuleName LaTeXModule -> TCM ()
    forall (m :: * -> *).
    Applicative m =>
    LaTeXCompileEnv -> IsMain -> Map ModuleName LaTeXModule -> m ()
    postCompileLaTeX
      , scopeCheckingSuffices :: Bool
    scopeCheckingSuffices = Bool
    True
      , mayEraseType :: QName -> TCM Bool
    mayEraseType          = TCM Bool -> QName -> TCM Bool
    forall a b. a -> b -> a
    const (TCM Bool -> QName -> TCM Bool) -> TCM Bool -> QName -> TCM Bool
    forall a b. (a -> b) -> a -> b
    $ Bool -> TCM Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
      }

    runLogLaTeXWithMonadDebug :: MonadDebug m => LogLaTeXT m a -> m a
    runLogLaTeXWithMonadDebug :: forall (m :: * -> *) a. MonadDebug m => LogLaTeXT m a -> m a
    runLogLaTeXWithMonadDebug = (LogMessage -> m ()) -> LogLaTeXT m a -> m a
    forall (m :: * -> *) a.
    Monad m =>
    (LogMessage -> m ()) -> LogLaTeXT m a -> m a
    runLogLaTeXTWith ((LogMessage -> m ()) -> LogLaTeXT m a -> m a)
    -> (LogMessage -> m ()) -> LogLaTeXT m a -> m a
    forall a b. (a -> b) -> a -> b
    $ (FilePath -> VerboseLevel -> FilePath -> m ()
    forall a (m :: * -> *).
    (ReportS a, MonadDebug m) =>
    FilePath -> VerboseLevel -> a -> m ()
    reportS FilePath
    "compile.latex" VerboseLevel
    1) (FilePath -> m ())
    -> (LogMessage -> FilePath) -> LogMessage -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> FilePath
    T.unpack (Text -> FilePath)
    -> (LogMessage -> Text) -> LogMessage -> FilePath
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LogMessage -> Text
    logMsgToText

    -- Resolve the raw flags into usable LaTeX options.
    resolveLaTeXOptions :: (HasOptions m, ReadTCState m) => LaTeXFlags -> TopLevelModuleName -> m LaTeXOptions
    resolveLaTeXOptions :: forall (m :: * -> *).
    (HasOptions m, ReadTCState m) =>
    LaTeXFlags -> TopLevelModuleName -> m LaTeXOptions
    resolveLaTeXOptions LaTeXFlags
    flags TopLevelModuleName
    moduleName = do
      CommandLineOptions
    options <- m CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions
      Map TopLevelModuleName AbsolutePath
    modFiles <- Lens' (Map TopLevelModuleName AbsolutePath) TCState
    -> m (Map TopLevelModuleName AbsolutePath)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (Map TopLevelModuleName AbsolutePath) TCState
    stModuleToSource
      let
        mSrcFileName :: Maybe AbsolutePath
    mSrcFileName = (FilePath -> AbsolutePath
    mkAbsolute (FilePath -> AbsolutePath)
    -> (AbsolutePath -> FilePath) -> AbsolutePath -> AbsolutePath
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbsolutePath -> FilePath
    filePath) (AbsolutePath -> AbsolutePath)
    -> Maybe AbsolutePath -> Maybe AbsolutePath
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TopLevelModuleName
    -> Map TopLevelModuleName AbsolutePath -> Maybe AbsolutePath
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup TopLevelModuleName
    moduleName Map TopLevelModuleName AbsolutePath
    modFiles
        countClusters :: Bool
    countClusters = PragmaOptions -> Bool
    optCountClusters (PragmaOptions -> Bool)
    -> (CommandLineOptions -> PragmaOptions)
    -> CommandLineOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CommandLineOptions -> PragmaOptions
    optPragmaOptions (CommandLineOptions -> Bool) -> CommandLineOptions -> Bool
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    options
        latexDir :: FilePath
    latexDir = LaTeXFlags -> FilePath
    latexFlagOutDir LaTeXFlags
    flags
        -- FIXME: This reliance on emacs-mode to decide whether to interpret the output location as project-relative or
        -- cwd-relative is gross. Also it currently behaves differently for JSON mode :-/
        -- And it prevents us from doing a real "one-time" setup.
        outDir :: FilePath
    outDir = case (Maybe AbsolutePath
    mSrcFileName, CommandLineOptions -> Bool
    optGHCiInteraction CommandLineOptions
    options) of
          (Just AbsolutePath
    sourceFile, Bool
    True) -> AbsolutePath -> FilePath
    filePath (AbsolutePath -> TopLevelModuleName -> AbsolutePath
    projectRoot AbsolutePath
    sourceFile TopLevelModuleName
    moduleName) FilePath -> FilePath -> FilePath
    </> FilePath
    latexDir
          (Maybe AbsolutePath, Bool)
    _ -> FilePath
    latexDir
      LaTeXOptions -> m LaTeXOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return LaTeXOptions :: FilePath -> Maybe AbsolutePath -> Bool -> LaTeXOptions
    LaTeXOptions
        { latexOptOutDir :: FilePath
    latexOptOutDir         = FilePath
    outDir
        , latexOptSourceFileName :: Maybe AbsolutePath
    latexOptSourceFileName = Maybe AbsolutePath
    mSrcFileName
        , latexOptCountClusters :: Bool
    latexOptCountClusters  = Bool
    countClusters
        }

    preCompileLaTeX
      :: Applicative m
      => LaTeXFlags
      -> m LaTeXCompileEnv
    preCompileLaTeX :: forall (m :: * -> *).
    Applicative m =>
    LaTeXFlags -> m LaTeXCompileEnv
    preCompileLaTeX LaTeXFlags
    flags = LaTeXCompileEnv -> m LaTeXCompileEnv
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (LaTeXCompileEnv -> m LaTeXCompileEnv)
    -> LaTeXCompileEnv -> m LaTeXCompileEnv
    forall a b. (a -> b) -> a -> b
    $ LaTeXFlags -> LaTeXCompileEnv
    LaTeXCompileEnv LaTeXFlags
    flags

    preModuleLaTeX
      :: (HasOptions m, ReadTCState m)
      => LaTeXCompileEnv
      -> IsMain
      -> ModuleName
      -> Maybe FilePath
      -> m (Recompile LaTeXModuleEnv LaTeXModule)
    preModuleLaTeX :: forall (m :: * -> *).
    (HasOptions m, ReadTCState m) =>
    LaTeXCompileEnv
    -> IsMain
    -> ModuleName
    -> Maybe FilePath
    -> m (Recompile LaTeXModuleEnv LaTeXModule)
    preModuleLaTeX (LaTeXCompileEnv LaTeXFlags
    flags) IsMain
    isMain ModuleName
    moduleName Maybe FilePath
    _ifacePath = case IsMain
    isMain of
      IsMain
    IsMain  -> LaTeXModuleEnv -> Recompile LaTeXModuleEnv LaTeXModule
    forall menv mod. menv -> Recompile menv mod
    Recompile (LaTeXModuleEnv -> Recompile LaTeXModuleEnv LaTeXModule)
    -> (LaTeXOptions -> LaTeXModuleEnv)
    -> LaTeXOptions
    -> Recompile LaTeXModuleEnv LaTeXModule
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LaTeXOptions -> LaTeXModuleEnv
    LaTeXModuleEnv (LaTeXOptions -> Recompile LaTeXModuleEnv LaTeXModule)
    -> m LaTeXOptions -> m (Recompile LaTeXModuleEnv LaTeXModule)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> LaTeXFlags -> TopLevelModuleName -> m LaTeXOptions
    forall (m :: * -> *).
    (HasOptions m, ReadTCState m) =>
    LaTeXFlags -> TopLevelModuleName -> m LaTeXOptions
    resolveLaTeXOptions LaTeXFlags
    flags (ModuleName -> TopLevelModuleName
    toTopLevelModuleName ModuleName
    moduleName)
      IsMain
    NotMain -> Recompile LaTeXModuleEnv LaTeXModule
    -> m (Recompile LaTeXModuleEnv LaTeXModule)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Recompile LaTeXModuleEnv LaTeXModule
     -> m (Recompile LaTeXModuleEnv LaTeXModule))
    -> Recompile LaTeXModuleEnv LaTeXModule
    -> m (Recompile LaTeXModuleEnv LaTeXModule)
    forall a b. (a -> b) -> a -> b
    $ LaTeXModule -> Recompile LaTeXModuleEnv LaTeXModule
    forall menv mod. mod -> Recompile menv mod
    Skip LaTeXModule
    LaTeXModule

    compileDefLaTeX
      :: Applicative m
      => LaTeXCompileEnv
      -> LaTeXModuleEnv
      -> IsMain
      -> Definition
      -> m LaTeXDef
    compileDefLaTeX :: forall (m :: * -> *).
    Applicative m =>
    LaTeXCompileEnv
    -> LaTeXModuleEnv -> IsMain -> Definition -> m LaTeXDef
    compileDefLaTeX LaTeXCompileEnv
    _cenv LaTeXModuleEnv
    _menv IsMain
    _main Definition
    _def = LaTeXDef -> m LaTeXDef
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure LaTeXDef
    LaTeXDef

    postModuleLaTeX
      :: (MonadDebug m, ReadTCState m, MonadIO m)
      => LaTeXCompileEnv
      -> LaTeXModuleEnv
      -> IsMain
      -> ModuleName
      -> [LaTeXDef]
      -> m LaTeXModule
    postModuleLaTeX :: forall (m :: * -> *).
    (MonadDebug m, ReadTCState m, MonadIO m) =>
    LaTeXCompileEnv
    -> LaTeXModuleEnv
    -> IsMain
    -> ModuleName
    -> [LaTeXDef]
    -> m LaTeXModule
    postModuleLaTeX LaTeXCompileEnv
    _cenv (LaTeXModuleEnv LaTeXOptions
    latexOpts) IsMain
    _main ModuleName
    _moduleName [LaTeXDef]
    _defs = do
      Interface
    i <- m Interface
    forall (m :: * -> *). ReadTCState m => m Interface
    curIF
      LogLaTeXT m () -> m ()
    forall (m :: * -> *) a. MonadDebug m => LogLaTeXT m a -> m a
    runLogLaTeXWithMonadDebug (LogLaTeXT m () -> m ()) -> LogLaTeXT m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ do
        -- FIXME: It would be better to do "prepareCommonAssets" in @preCompileLaTeX@, but because
        -- the output directory depends on the module-relative project root (when in emacs-mode),
        -- we can't do that until we see the module.
        -- However, for now that is OK because we only generate LaTeX for the main module.
        FilePath -> LogLaTeXT m ()
    forall (m :: * -> *).
    (MonadLogLaTeX m, MonadIO m) =>
    FilePath -> m ()
    prepareCommonAssets (LaTeXOptions -> FilePath
    latexOptOutDir LaTeXOptions
    latexOpts)
        LaTeXOptions -> Interface -> LogLaTeXT m ()
    forall (m :: * -> *).
    (MonadLogLaTeX m, MonadIO m) =>
    LaTeXOptions -> Interface -> m ()
    generateLaTeXIO LaTeXOptions
    latexOpts Interface
    i
      LaTeXModule -> m LaTeXModule
    forall (m :: * -> *) a. Monad m => a -> m a
    return LaTeXModule
    LaTeXModule

    postCompileLaTeX
      :: Applicative m
      => LaTeXCompileEnv
      -> IsMain
      -> Map ModuleName LaTeXModule
      -> m ()
    postCompileLaTeX :: forall (m :: * -> *).
    Applicative m =>
    LaTeXCompileEnv -> IsMain -> Map ModuleName LaTeXModule -> m ()
    postCompileLaTeX LaTeXCompileEnv
    _cenv IsMain
    _main Map ModuleName LaTeXModule
    _modulesByName = () -> m ()
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()