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
  { 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'
  { 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
    { 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 ()