packages feed

Agda-2.7.0: src/full/Agda/Interaction/Highlighting/LaTeX/Backend.hs

{-# 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
  { latexFlagOutDir        :: FilePath
  , latexFlagSourceFile    :: Maybe FilePath
  , latexFlagGenerateLaTeX :: Bool
    -- ^ Are we going to try to generate LaTeX at all?
  } deriving (Eq, Generic)

instance NFData LaTeXFlags

-- | The default output directory for LaTeX.

defaultLaTeXDir :: FilePath
defaultLaTeXDir = "latex"

defaultLaTeXFlags :: LaTeXFlags
defaultLaTeXFlags = LaTeXFlags
  { latexFlagOutDir        = defaultLaTeXDir
  , latexFlagSourceFile    = Nothing
  , latexFlagGenerateLaTeX = False
  }

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

latexFlag :: Flag LaTeXFlags
latexFlag o = return $ o { latexFlagGenerateLaTeX = True }

latexDirFlag :: FilePath -> Flag LaTeXFlags
latexDirFlag d o = return $ o { latexFlagOutDir = d }

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

latexBackend :: Backend
latexBackend = Backend latexBackend'

latexBackend' :: Backend' LaTeXFlags LaTeXCompileEnv LaTeXModuleEnv LaTeXModule LaTeXDef
latexBackend' = Backend'
  { backendName           = "LaTeX"
  , backendVersion        = Nothing
  , options               = defaultLaTeXFlags
  , commandLineFlags      = latexFlagsDescriptions
  , isEnabled             = latexFlagGenerateLaTeX
  , preCompile            = preCompileLaTeX
  , preModule             = preModuleLaTeX
  , compileDef            = compileDefLaTeX
  , postModule            = postModuleLaTeX
  , postCompile           = postCompileLaTeX
  , scopeCheckingSuffices = True
  , mayEraseType          = const $ return False
  }

runLogLaTeXWithMonadDebug :: MonadDebug m => LogLaTeXT m a -> m a
runLogLaTeXWithMonadDebug = runLogLaTeXTWith $ (reportS "compile.latex" 1) . T.unpack . logMsgToText

-- Resolve the raw flags into usable LaTeX options.
resolveLaTeXOptions :: (HasOptions m, ReadTCState m) => LaTeXFlags -> TopLevelModuleName -> m LaTeXOptions
resolveLaTeXOptions flags moduleName = do
  options <- commandLineOptions
  modFiles <- useTC stModuleToSource
  let
    mSrcFileName =
      (\f -> mkRangeFile (mkAbsolute (filePath f)) (Just moduleName)) <$>
      Map.lookup moduleName modFiles
    countClusters = optCountClusters . optPragmaOptions $ options
    latexDir = latexFlagOutDir 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 (mSrcFileName, optGHCiInteraction options) of
      (Just sourceFile, True) ->
        filePath (projectRoot (rangeFilePath sourceFile) moduleName) </>
        latexDir
      _ -> latexDir
  return LaTeXOptions
    { latexOptOutDir         = outDir
    , latexOptSourceFileName = mSrcFileName
    , latexOptCountClusters  = countClusters
    }

preCompileLaTeX
  :: Applicative m
  => LaTeXFlags
  -> m LaTeXCompileEnv
preCompileLaTeX flags = pure $ LaTeXCompileEnv flags

preModuleLaTeX
  :: (HasOptions m, ReadTCState m)
  => LaTeXCompileEnv
  -> IsMain
  -> TopLevelModuleName
  -> Maybe FilePath
  -> m (Recompile LaTeXModuleEnv LaTeXModule)
preModuleLaTeX (LaTeXCompileEnv flags) isMain moduleName _ifacePath = case isMain of
  IsMain  -> Recompile . LaTeXModuleEnv <$> resolveLaTeXOptions flags moduleName
  NotMain -> return $ Skip LaTeXModule

compileDefLaTeX
  :: Applicative m
  => LaTeXCompileEnv
  -> LaTeXModuleEnv
  -> IsMain
  -> Definition
  -> m LaTeXDef
compileDefLaTeX _cenv _menv _main _def = pure LaTeXDef

postModuleLaTeX
  :: (MonadDebug m, ReadTCState m, MonadIO m)
  => LaTeXCompileEnv
  -> LaTeXModuleEnv
  -> IsMain
  -> TopLevelModuleName
  -> [LaTeXDef]
  -> m LaTeXModule
postModuleLaTeX _cenv (LaTeXModuleEnv latexOpts) _main _moduleName _defs = do
  i <- 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 _cenv _main _modulesByName = pure ()