{-# OPTIONS_GHC -Wunused-imports #-}

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_boot(..), Backend',Backend'_boot(..), Definition, Recompile(..))
import Agda.Compiler.Common (curIF, IsMain(IsMain, NotMain))

import Agda.Interaction.Options
  ( ArgDescr(NoArg, ReqArg)
  , CommandLineOptions ( optGHCiInteraction, optPragmaOptions )
  , 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 -> [Char]
latexFlagOutDir        :: FilePath
  , LaTeXFlags -> Maybe [Char]
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
$c== :: LaTeXFlags -> LaTeXFlags -> Bool
== :: LaTeXFlags -> LaTeXFlags -> Bool
$c/= :: LaTeXFlags -> LaTeXFlags -> Bool
/= :: 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
$cfrom :: forall x. LaTeXFlags -> Rep LaTeXFlags x
from :: forall x. LaTeXFlags -> Rep LaTeXFlags x
$cto :: forall x. Rep LaTeXFlags x -> LaTeXFlags
to :: forall x. Rep LaTeXFlags x -> LaTeXFlags
Generic)

instance NFData LaTeXFlags

-- | The default output directory for LaTeX.

defaultLaTeXDir :: FilePath
defaultLaTeXDir :: [Char]
defaultLaTeXDir = [Char]
"latex"

defaultLaTeXFlags :: LaTeXFlags
defaultLaTeXFlags :: LaTeXFlags
defaultLaTeXFlags = LaTeXFlags
  { latexFlagOutDir :: [Char]
latexFlagOutDir        = [Char]
defaultLaTeXDir
  , latexFlagSourceFile :: Maybe [Char]
latexFlagSourceFile    = Maybe [Char]
forall a. Maybe a
Nothing
  , latexFlagGenerateLaTeX :: Bool
latexFlagGenerateLaTeX = Bool
False
  }

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

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

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

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

latexBackend :: Backend
latexBackend :: Backend
latexBackend = Backend'_boot
  TCM LaTeXFlags LaTeXCompileEnv LaTeXModuleEnv LaTeXModule LaTeXDef
-> Backend
forall opts (tcm :: * -> *) env menv mod def.
NFData opts =>
Backend'_boot tcm opts env menv mod def -> Backend_boot tcm
Backend Backend'_boot
  TCM LaTeXFlags LaTeXCompileEnv LaTeXModuleEnv LaTeXModule LaTeXDef
latexBackend'

latexBackend' :: Backend' LaTeXFlags LaTeXCompileEnv LaTeXModuleEnv LaTeXModule LaTeXDef
latexBackend' :: Backend'_boot
  TCM LaTeXFlags LaTeXCompileEnv LaTeXModuleEnv LaTeXModule LaTeXDef
latexBackend' = Backend'
  { backendName :: [Char]
backendName           = [Char]
"LaTeX"
  , backendVersion :: Maybe [Char]
backendVersion        = Maybe [Char]
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
-> TopLevelModuleName
-> Maybe [Char]
-> TCM (Recompile LaTeXModuleEnv LaTeXModule)
preModule             = LaTeXCompileEnv
-> IsMain
-> TopLevelModuleName
-> Maybe [Char]
-> TCM (Recompile LaTeXModuleEnv LaTeXModule)
forall (m :: * -> *).
(HasOptions m, ReadTCState m) =>
LaTeXCompileEnv
-> IsMain
-> TopLevelModuleName
-> Maybe [Char]
-> 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
-> TopLevelModuleName
-> [LaTeXDef]
-> TCM LaTeXModule
postModule            = LaTeXCompileEnv
-> LaTeXModuleEnv
-> IsMain
-> TopLevelModuleName
-> [LaTeXDef]
-> TCM LaTeXModule
forall (m :: * -> *).
(MonadDebug m, ReadTCState m, MonadIO m) =>
LaTeXCompileEnv
-> LaTeXModuleEnv
-> IsMain
-> TopLevelModuleName
-> [LaTeXDef]
-> m LaTeXModule
postModuleLaTeX
  , postCompile :: LaTeXCompileEnv
-> IsMain -> Map TopLevelModuleName LaTeXModule -> TCM ()
postCompile           = LaTeXCompileEnv
-> IsMain -> Map TopLevelModuleName LaTeXModule -> TCM ()
forall (m :: * -> *).
Applicative m =>
LaTeXCompileEnv
-> IsMain -> Map TopLevelModuleName 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 a. a -> TCM a
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
$ ([Char] -> VerboseLevel -> [Char] -> m ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> VerboseLevel -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportS [Char]
"compile.latex" VerboseLevel
1) ([Char] -> m ()) -> (LogMessage -> [Char]) -> LogMessage -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [Char]
T.unpack (Text -> [Char]) -> (LogMessage -> Text) -> LogMessage -> [Char]
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
  options <- m CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  modFiles <- useTC stModuleToSource
  let
    mSrcFileName =
      (\AbsolutePath
f -> AbsolutePath -> Maybe TopLevelModuleName -> RangeFile
mkRangeFile ([Char] -> AbsolutePath
mkAbsolute (AbsolutePath -> [Char]
filePath AbsolutePath
f)) (TopLevelModuleName -> Maybe TopLevelModuleName
forall a. a -> Maybe a
Just TopLevelModuleName
moduleName)) (AbsolutePath -> RangeFile)
-> Maybe AbsolutePath -> Maybe RangeFile
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 = 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 = LaTeXFlags -> [Char]
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 = case (Maybe RangeFile
mSrcFileName, CommandLineOptions -> Bool
optGHCiInteraction CommandLineOptions
options) of
      (Just RangeFile
sourceFile, Bool
True) ->
        AbsolutePath -> [Char]
filePath (AbsolutePath -> TopLevelModuleName -> AbsolutePath
projectRoot (RangeFile -> AbsolutePath
rangeFilePath RangeFile
sourceFile) TopLevelModuleName
moduleName) [Char] -> [Char] -> [Char]
</>
        [Char]
latexDir
      (Maybe RangeFile, Bool)
_ -> [Char]
latexDir
  return LaTeXOptions
    { latexOptOutDir         = outDir
    , latexOptSourceFileName = mSrcFileName
    , latexOptCountClusters  = countClusters
    }

preCompileLaTeX
  :: Applicative m
  => LaTeXFlags
  -> m LaTeXCompileEnv
preCompileLaTeX :: forall (m :: * -> *).
Applicative m =>
LaTeXFlags -> m LaTeXCompileEnv
preCompileLaTeX LaTeXFlags
flags = LaTeXCompileEnv -> m LaTeXCompileEnv
forall a. a -> m a
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
  -> TopLevelModuleName
  -> Maybe FilePath
  -> m (Recompile LaTeXModuleEnv LaTeXModule)
preModuleLaTeX :: forall (m :: * -> *).
(HasOptions m, ReadTCState m) =>
LaTeXCompileEnv
-> IsMain
-> TopLevelModuleName
-> Maybe [Char]
-> m (Recompile LaTeXModuleEnv LaTeXModule)
preModuleLaTeX (LaTeXCompileEnv LaTeXFlags
flags) IsMain
isMain TopLevelModuleName
moduleName Maybe [Char]
_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 TopLevelModuleName
moduleName
  IsMain
NotMain -> Recompile LaTeXModuleEnv LaTeXModule
-> m (Recompile LaTeXModuleEnv LaTeXModule)
forall a. a -> m a
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 a. a -> m a
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
  i <- m Interface
forall (m :: * -> *). ReadTCState m => m Interface
curIF
  runLogLaTeXWithMonadDebug $ 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.
    prepareCommonAssets (latexOptOutDir latexOpts)
    generateLaTeXIO latexOpts i
  return 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 = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()