module Agda.Interaction.Highlighting.LaTeX
( generateLaTeX
) where
import Prelude hiding (log)
import Data.Char
import Data.Maybe
import Data.Function
import Control.Monad.RWS
import Control.Monad.Error
import System.Directory
import System.FilePath
import Data.Text (Text)
import qualified Data.Text as T
import qualified Data.Text.IO as T
import qualified Data.Text.Encoding as E
import qualified Data.ByteString as BS
import qualified Data.List as List
import qualified Data.Map as Map
import Paths_Agda
import Agda.Syntax.Common
import Agda.Syntax.Concrete (TopLevelModuleName, moduleNameParts)
import qualified Agda.Interaction.FindFile as Find
import Agda.Interaction.Highlighting.Precise
import Agda.TypeChecking.Monad (TCM)
import qualified Agda.TypeChecking.Monad as TCM
import Agda.Interaction.Options
import Agda.Compiler.CallCompiler
import qualified Agda.Utils.IO.UTF8 as UTF8
import Agda.Utils.FileName (filePath)
import Agda.Utils.Pretty (pretty, render)
#include "../../undefined.h"
import Agda.Utils.Impossible
type LaTeX = ErrorT String (RWST () Text State IO)
data State = State
{ tokens :: Tokens
, column :: Int
, indent :: Int
, indentPrev :: Int
, inCode :: Bool
, debugs :: [Debug]
}
type Tokens = [Token]
data Token = Token
{ text :: Text
, info :: MetaInfo
, position :: Integer
}
deriving Show
data Debug = MoveColumn | NonCode | Code | Spaces | Output
deriving (Eq, Show)
runLaTeX :: LaTeX a -> () -> State -> IO (Either String a, State, Text)
runLaTeX = runRWST . runErrorT
emptyState :: State
emptyState = State
{ tokens = []
, column = 0
, indent = 0
, indentPrev = 0
, inCode = False
, debugs = []
}
(<+>) = T.append
isInfixOf' :: Text -> Text -> Maybe (Text, Text)
isInfixOf' needle haystack = go (T.tails haystack) 0
where
go [] n = Nothing
go ((T.stripPrefix needle -> Just suf) : xss) n = Just (T.take n haystack, suf)
go (_ : xss) n = go xss (n + 1)
isInfixOfRev :: Text -> Text -> Maybe (Text, Text)
isInfixOfRev needle haystack
= case T.reverse needle `isInfixOf'` T.reverse haystack of
Nothing -> Nothing
Just (pre, suf) -> Just (T.reverse suf, T.reverse pre)
isSpaces :: Text -> Bool
isSpaces = T.all isSpace
isActualSpaces :: Text -> Bool
isActualSpaces = T.all (== ' ')
nextToken' :: LaTeX Token
nextToken' = do
toks <- gets tokens
case toks of
[] -> throwError "Done"
t : ts | text t == beginCode || text t == endCode ||
T.singleton '%' == T.take 1 (T.stripStart (text t)) -> do
modify $ \s -> s { tokens = ts }
return t
t : ts -> do
modify $ \s -> s { tokens = ts }
inCode <- gets inCode
let code = if inCode then endCode else beginCode
case code `isInfixOf'` text t of
Nothing -> do
unless (isSpaces (text t)) $ do
log MoveColumn $ text t
moveColumn $ T.length $ text t
return t
Just (pre, suf) -> do
let (textToReturn, textsToPutBack) =
if code == beginCode && isSpaces suf
then case T.singleton '\n' `isInfixOf'` suf of
Nothing -> (pre, [ beginCode ])
Just (_, suf') -> (pre, [ beginCode, suf' ])
else if code == endCode && isSpaces pre
then case T.singleton '\n' `isInfixOfRev` pre of
Nothing -> (code, [ suf ])
Just (pre', suf') ->
(pre' <+> T.dropWhile (`elem` [' ', '\t']) suf',
[ code, suf ])
else (pre, [ code, suf ])
let tokToReturn = t { text = textToReturn }
let toksToPutBack = map (\txt -> t { text = txt }) textsToPutBack
unless (isSpaces pre) $ do
log MoveColumn pre
moveColumn $ T.length pre
modify $ \s -> s { tokens = toksToPutBack ++ tokens s }
return tokToReturn
nextToken :: LaTeX Text
nextToken = text `fmap` nextToken'
resetColumn :: LaTeX ()
resetColumn = modify $ \s -> s { column = 0 }
moveColumn :: Int -> LaTeX ()
moveColumn i = modify $ \s -> s { column = i + column s }
setIndent :: Int -> LaTeX ()
setIndent i = modify $ \s -> s { indent = i }
resetIndent :: LaTeX ()
resetIndent = modify $ \s -> s { indent = 0 }
setIndentPrev :: Int -> LaTeX ()
setIndentPrev i = modify $ \s -> s { indentPrev = i }
resetIndentPrev :: LaTeX ()
resetIndentPrev = modify $ \s -> s { indentPrev = 0 }
setInCode :: LaTeX ()
setInCode = modify $ \s -> s { inCode = True }
unsetInCode :: LaTeX ()
unsetInCode = modify $ \s -> s { inCode = False }
logHelper :: Debug -> Text -> [String] -> LaTeX ()
logHelper debug text extra = do
debugs <- gets debugs
when (debug `elem` debugs) $ do
lift $ lift $ T.putStrLn $ T.pack (show debug ++ ": ") <+>
T.pack "'" <+> text <+> T.pack "' " <+>
if null extra
then T.empty
else T.pack "(" <+> T.pack (unwords extra) <+> T.pack ")"
log :: Debug -> Text -> LaTeX ()
log MoveColumn text = do
ind <- gets indent
logHelper MoveColumn text ["ind=", show ind]
log Code text = do
ind <- gets indent
col <- gets column
logHelper Code text ["ind=", show ind, "col=", show col]
log debug text = logHelper debug text []
log' :: Debug -> String -> LaTeX ()
log' d = log d . T.pack
output :: Text -> LaTeX ()
output text = do
log Output text
tell text
nl = T.pack "%\n"
beginCode = T.pack "\\begin{code}"
endCode = T.pack "\\end{code}"
ptOpen = T.pack "\\>"
ptOpen' i = ptOpen <+> T.pack ("[" ++ show i ++ "]")
ptClose = T.pack "\\<"
ptClose' i = ptClose <+> T.pack ("[" ++ show i ++ "]")
ptNL = nl <+> T.pack "\\\\\n"
cmdPrefix = T.pack "\\Agda"
cmdArg x = T.singleton '{' <+> x <+> T.singleton '}'
cmdIndent i = cmdPrefix <+> T.pack "Indent" <+>
cmdArg (T.pack (show i)) <+> cmdArg T.empty
infixl' = T.pack "infixl"
infix' = T.pack "infix"
infixr' = T.pack "infixr"
nonCode :: LaTeX ()
nonCode = do
tok <- nextToken
log NonCode tok
if tok == beginCode
then do
output $ beginCode <+> nl
resetColumn
setInCode
code
else do
output tok
nonCode
code :: LaTeX ()
code = do
col <- gets column
tok' <- nextToken'
let tok = text tok'
log Code tok
when (tok == T.empty) code
when (col == 0 && not (isActualSpaces tok)) $ do
output ptOpen
when (tok == endCode) $ do
output $ ptClose <+> nl <+> endCode
unsetInCode
nonCode
when (tok `elem` [ infixl', infix', infixr' ]) $ do
output $ cmdPrefix <+> T.pack "Keyword" <+> cmdArg tok
fixity
code
when (isSpaces tok) $ do
spaces $ T.group tok
code
case aspect (info tok') of
Nothing -> output $ escape tok
Just a -> case cmd a of
"" -> output $ escape tok
s -> output $ cmdPrefix <+> T.pack s <+> cmdArg (escape tok)
code
where
cmd :: Aspect -> String
cmd (Name mKind _) = maybe "" showKind mKind
where
showKind :: NameKind -> String
showKind (Constructor Inductive) = "InductiveConstructor"
showKind (Constructor CoInductive) = "CoinductiveConstructor"
showKind k = show k
cmd a = show a
escape :: Text -> Text
escape (T.uncons -> Nothing) = T.empty
escape (T.uncons -> Just (c, s)) = T.pack (replace c) <+> escape s
where
replace :: Char -> String
replace c = case c of
'_' -> "\\_"
'{' -> "\\{"
'}' -> "\\}"
'#' -> "\\#"
'$' -> "\\$"
'&' -> "\\&"
'%' -> "\\%"
'~' -> "\\textasciitilde"
'^' -> "\\textasciicircum"
'\\' -> "\\textbackslash"
'\n' -> "\\<\\\\\n\\>"
_ -> [ c ]
escape _ = __IMPOSSIBLE__
fixity :: LaTeX ()
fixity = do
tok <- nextToken
case T.breakOn (T.pack "\n") tok of
(sps, nls) | nls == T.empty && isSpaces sps -> do
spaces $ T.group sps
fixity
(num, nls) | nls == T.empty -> do
output $ cmdPrefix <+> T.pack "Number" <+> cmdArg num
fixity
(ops, nls) | otherwise -> do
output $ escape ops
spaces (T.group nls)
spaces :: [Text] -> LaTeX ()
spaces [] = return ()
spaces ((T.uncons -> Nothing) : ss) = __IMPOSSIBLE__
spaces ((T.uncons -> Just (' ', s)) : []) | T.null s = do
col <- gets column
when (col == 0) $ do
output ptOpen
moveColumn 1
output $ T.singleton ' '
spaces (s@(T.uncons -> Just (' ', _)) : ss) = do
let len = T.length s
col <- gets column
moveColumn len
if col /= 0
then do
log' Spaces "col /= 0"
output $ T.singleton ' '
col <- gets column
output $ ptClose' col <+> nl <+> ptOpen' col
else do
log' Spaces "col == 0"
indent <- gets indent
indentPrev <- gets indentPrev
case compare len indent of
GT -> do
log' Spaces "GT"
setIndent len
setIndentPrev indent
output $ ptOpen' indent
output $ cmdIndent len
output $ ptClose' len <+> nl <+> ptOpen' len
EQ -> do
log' Spaces "EQ"
output $ ptOpen' indentPrev
output $ cmdIndent len
output $ ptClose' len <+> nl <+> ptOpen' len
LT -> do
log' Spaces "LT"
setIndent len
resetIndentPrev
output $ ptOpen' 0
output $ cmdIndent len
output $ ptClose' len <+> nl <+> ptOpen' len
spaces ss
spaces (s@(T.uncons -> Just ('\n', _)) : ss) = do
resetColumn
output $ ptClose <+> T.replicate (T.length s) ptNL
spaces ss
spaces (s@(T.uncons -> Just ('\t', _)) : ss) =
spaces $ T.replicate (T.length s) (T.singleton ' ') : ss
spaces (_ : ss) = __IMPOSSIBLE__
defaultStyFile = "agda.sty"
generateLaTeX :: TopLevelModuleName -> HighlightingInfo -> TCM ()
generateLaTeX mod hi = do
options <- TCM.commandLineOptions
let dir = optLaTeXDir options
liftIO $ createDirectoryIfMissing True dir
TCM.reportSLn "latex" 1 $ unlines
[ ""
, "Checking if " ++ defaultStyFile ++ " is found by the LaTeX environment."
]
merrors <- callCompiler' "kpsewhich" [ "--path=" ++ dir, defaultStyFile ]
when (isJust merrors) $ do
TCM.reportSLn "latex" 1 $ unlines
[ ""
, defaultStyFile ++ " was not found. Copying a default version of " ++
defaultStyFile
, "into the directory " ++ dir ++ "."
]
liftIO $ do
styFile <- getDataFileName defaultStyFile
liftIO $ copyFile styFile (dir </> defaultStyFile)
let outPath = modToFile mod
inAbsPath <- liftM filePath (Find.findFile mod)
liftIO $ do
source <- UTF8.readTextFile inAbsPath
latex <- E.encodeUtf8 `fmap` toLaTeX source hi
createDirectoryIfMissing True $ dir </> takeDirectory outPath
BS.writeFile (dir </> outPath) latex
where
modToFile :: TopLevelModuleName -> FilePath
modToFile m = List.intercalate [pathSeparator] (moduleNameParts m) <.> "tex"
toLaTeX :: String -> HighlightingInfo -> IO Text
toLaTeX source hi
= processTokens
. map (\xs -> case xs of
(mi, (pos, _)) : _ ->
Token { text = T.pack $ map (\(_, (_, c)) -> c) xs
, info = maybe mempty id mi
, position = pos
}
[] -> __IMPOSSIBLE__)
. List.groupBy ((==) `on` fst)
. map (\(pos, char) ->
(Map.lookup pos infoMap, (pos, char)))
. zip [1..]
$ source
where
infoMap = toMap (decompress hi)
processTokens :: Tokens -> IO Text
processTokens ts = do
(x, _, s) <- runLaTeX nonCode () (emptyState { tokens = ts })
case x of
Left "Done" -> return s
_ -> __IMPOSSIBLE__