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.Position (mkRangeFile, rangeFilePath)
import Agda.Syntax.TopLevelModuleName (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
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. 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
  { latexFlagOutDir :: FilePath
latexFlagOutDir        = FilePath
defaultLaTeXDir
  , latexFlagSourceFile :: Maybe FilePath
latexFlagSourceFile    = forall a. Maybe a
Nothing
  , latexFlagGenerateLaTeX :: Bool
latexFlagGenerateLaTeX = Bool
False
  }

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

latexFlag :: Flag LaTeXFlags
latexFlag :: Flag LaTeXFlags
latexFlag LaTeXFlags
o = forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall (m :: * -> *) a. Monad m => a -> m a
return 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 = 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'
  { backendName :: FilePath
backendName           = FilePath
"LaTeX"
  , backendVersion :: Maybe FilePath
backendVersion        = 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            = forall (m :: * -> *).
Applicative m =>
LaTeXFlags -> m LaTeXCompileEnv
preCompileLaTeX
  , preModule :: LaTeXCompileEnv
-> IsMain
-> TopLevelModuleName
-> Maybe FilePath
-> TCM (Recompile LaTeXModuleEnv LaTeXModule)
preModule             = forall (m :: * -> *).
(HasOptions m, ReadTCState m) =>
LaTeXCompileEnv
-> IsMain
-> TopLevelModuleName
-> Maybe FilePath
-> m (Recompile LaTeXModuleEnv LaTeXModule)
preModuleLaTeX
  , compileDef :: LaTeXCompileEnv
-> LaTeXModuleEnv -> IsMain -> Definition -> TCM LaTeXDef
compileDef            = forall (m :: * -> *).
Applicative m =>
LaTeXCompileEnv
-> LaTeXModuleEnv -> IsMain -> Definition -> m LaTeXDef
compileDefLaTeX
  , postModule :: LaTeXCompileEnv
-> LaTeXModuleEnv
-> IsMain
-> TopLevelModuleName
-> [LaTeXDef]
-> TCM LaTeXModule
postModule            = forall (m :: * -> *).
(MonadDebug m, ReadTCState m, MonadIO m) =>
LaTeXCompileEnv
-> LaTeXModuleEnv
-> IsMain
-> TopLevelModuleName
-> [LaTeXDef]
-> m LaTeXModule
postModuleLaTeX
  , postCompile :: LaTeXCompileEnv
-> IsMain -> Map TopLevelModuleName LaTeXModule -> TCM ()
postCompile           = forall (m :: * -> *).
Applicative m =>
LaTeXCompileEnv
-> IsMain -> Map TopLevelModuleName LaTeXModule -> m ()
postCompileLaTeX
  , scopeCheckingSuffices :: Bool
scopeCheckingSuffices = Bool
True
  , mayEraseType :: QName -> TCM Bool
mayEraseType          = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *) a.
Monad m =>
(LogMessage -> m ()) -> LogLaTeXT m a -> m a
runLogLaTeXTWith forall a b. (a -> b) -> a -> b
$ (forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
FilePath -> VerboseLevel -> a -> m ()
reportS FilePath
"compile.latex" VerboseLevel
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
T.unpack 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 <- forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  Map TopLevelModuleName AbsolutePath
modFiles <- forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map TopLevelModuleName AbsolutePath) TCState
stModuleToSource
  let
    mSrcFileName :: Maybe RangeFile
mSrcFileName =
      (\AbsolutePath
f -> AbsolutePath -> Maybe TopLevelModuleName -> RangeFile
mkRangeFile (FilePath -> AbsolutePath
mkAbsolute (AbsolutePath -> FilePath
filePath AbsolutePath
f)) (forall a. a -> Maybe a
Just TopLevelModuleName
moduleName)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandLineOptions -> PragmaOptions
optPragmaOptions 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 RangeFile
mSrcFileName, CommandLineOptions -> Bool
optGHCiInteraction CommandLineOptions
options) of
      (Just RangeFile
sourceFile, Bool
True) ->
        AbsolutePath -> FilePath
filePath (AbsolutePath -> TopLevelModuleName -> AbsolutePath
projectRoot (RangeFile -> AbsolutePath
rangeFilePath RangeFile
sourceFile) TopLevelModuleName
moduleName) FilePath -> FilePath -> FilePath
</>
        FilePath
latexDir
      (Maybe RangeFile, Bool)
_ -> FilePath
latexDir
  forall (m :: * -> *) a. Monad m => a -> m a
return LaTeXOptions
    { latexOptOutDir :: FilePath
latexOptOutDir         = FilePath
outDir
    , latexOptSourceFileName :: Maybe RangeFile
latexOptSourceFileName = Maybe RangeFile
mSrcFileName
    , latexOptCountClusters :: Bool
latexOptCountClusters  = Bool
countClusters
    }

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

preModuleLaTeX
  :: (HasOptions m, ReadTCState m)
  => LaTeXCompileEnv
  -> IsMain
  -> TopLevelModuleName
  -> Maybe FilePath
  -> m (Recompile LaTeXModuleEnv LaTeXModule)
preModuleLaTeX :: forall (m :: * -> *).
(HasOptions m, ReadTCState m) =>
LaTeXCompileEnv
-> IsMain
-> TopLevelModuleName
-> Maybe FilePath
-> m (Recompile LaTeXModuleEnv LaTeXModule)
preModuleLaTeX (LaTeXCompileEnv LaTeXFlags
flags) IsMain
isMain TopLevelModuleName
moduleName Maybe FilePath
_ifacePath = case IsMain
isMain of
  IsMain
IsMain  -> forall menv mod. menv -> Recompile menv mod
Recompile forall b c a. (b -> c) -> (a -> b) -> a -> c
. LaTeXOptions -> LaTeXModuleEnv
LaTeXModuleEnv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasOptions m, ReadTCState m) =>
LaTeXFlags -> TopLevelModuleName -> m LaTeXOptions
resolveLaTeXOptions LaTeXFlags
flags TopLevelModuleName
moduleName
  IsMain
NotMain -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure LaTeXDef
LaTeXDef

postModuleLaTeX
  :: (MonadDebug m, ReadTCState m, MonadIO m)
  => LaTeXCompileEnv
  -> LaTeXModuleEnv
  -> IsMain
  -> TopLevelModuleName
  -> [LaTeXDef]
  -> m LaTeXModule
postModuleLaTeX :: forall (m :: * -> *).
(MonadDebug m, ReadTCState m, MonadIO m) =>
LaTeXCompileEnv
-> LaTeXModuleEnv
-> IsMain
-> TopLevelModuleName
-> [LaTeXDef]
-> m LaTeXModule
postModuleLaTeX LaTeXCompileEnv
_cenv (LaTeXModuleEnv LaTeXOptions
latexOpts) IsMain
_main TopLevelModuleName
_moduleName [LaTeXDef]
_defs = do
  Interface
i <- forall (m :: * -> *). ReadTCState m => m Interface
curIF
  forall (m :: * -> *) a. MonadDebug m => LogLaTeXT m a -> m a
runLogLaTeXWithMonadDebug 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.
    forall (m :: * -> *).
(MonadLogLaTeX m, MonadIO m) =>
FilePath -> m ()
prepareCommonAssets (LaTeXOptions -> FilePath
latexOptOutDir LaTeXOptions
latexOpts)
    forall (m :: * -> *).
(MonadLogLaTeX m, MonadIO m) =>
LaTeXOptions -> Interface -> m ()
generateLaTeXIO LaTeXOptions
latexOpts Interface
i
  forall (m :: * -> *) a. Monad m => a -> m a
return LaTeXModule
LaTeXModule

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