{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ViewPatterns #-}
module Agda.Interaction.Highlighting.LaTeX
( generateLaTeX
) where
import Prelude hiding (log)
import Data.Char
import Data.Maybe
import Data.Function
import Data.Foldable (toList)
import Control.Monad.RWS.Strict
import Control.Arrow (second)
import System.Directory
import System.Exit
import System.FilePath
import System.Process
import Data.Text (Text)
import qualified Data.Text as T
#ifdef COUNT_CLUSTERS
import qualified Data.Text.ICU as ICU
#endif
import qualified Data.Text.IO as T
import qualified Data.Text.Lazy as L
import qualified Data.Text.Lazy.Encoding as E
import qualified Data.ByteString.Lazy as BS
import Data.HashSet (HashSet)
import qualified Data.HashSet as Set
import qualified Data.IntMap as IntMap
import qualified Data.List as List
import Paths_Agda
import Agda.Syntax.Abstract (toTopLevelModuleName)
import Agda.Syntax.Common
import Agda.Syntax.Concrete
(TopLevelModuleName, moduleNameParts, projectRoot)
import Agda.Syntax.Parser.Literate (literateTeX, LayerRole, atomizeLayers)
import qualified Agda.Syntax.Parser.Literate as L
import Agda.Syntax.Position (startPos)
import qualified Agda.Interaction.FindFile as Find
import Agda.Interaction.Highlighting.Precise
import Agda.TypeChecking.Monad (TCM, Interface(..))
import qualified Agda.TypeChecking.Monad as TCM
import qualified Agda.Interaction.Options as O
import Agda.Compiler.CallCompiler
import qualified Agda.Utils.IO.UTF8 as UTF8
import Agda.Utils.FileName (filePath, AbsolutePath, mkAbsolute)
#include "undefined.h"
import Agda.Utils.Impossible
type LaTeX = RWST () [Output] State IO
data Output
= Text !Text
| MaybeColumn !AlignmentColumn
deriving Show
data Kind
= Indentation
| Alignment
deriving (Eq, Show)
type IndentationColumnId = Int
data AlignmentColumn = AlignmentColumn
{ columnCodeBlock :: !Int
, columnColumn :: !Int
, columnKind :: Maybe IndentationColumnId
} deriving Show
data State = State
{ codeBlock :: !Int
, column :: !Int
, columns :: [AlignmentColumn]
, columnsPrev :: [AlignmentColumn]
, nextId :: !IndentationColumnId
, usedColumns :: HashSet IndentationColumnId
, countClusters :: !Bool
}
type Tokens = [Token]
data Token = Token
{ text :: !Text
, info :: Aspects
}
deriving Show
withTokenText :: (Text -> Text) -> Token -> Token
withTokenText f tok@Token{text = t} = tok{text = f t}
data Debug = MoveColumn | NonCode | Code | Spaces | Output
deriving (Eq, Show)
debugs :: [Debug]
debugs = []
runLaTeX ::
LaTeX a -> () -> State -> IO (a, State, [Output])
runLaTeX = runRWST
emptyState
:: Bool
-> State
emptyState cc = State
{ codeBlock = 0
, column = 0
, columns = []
, columnsPrev = []
, nextId = 0
, usedColumns = Set.empty
, countClusters = cc
}
size :: Text -> LaTeX Int
size t = do
cc <- countClusters <$> get
if cc then
#ifdef COUNT_CLUSTERS
return $ length $ ICU.breaks (ICU.breakCharacter ICU.Root) t
#else
__IMPOSSIBLE__
#endif
else
return $ T.length t
(<+>) :: Text -> Text -> Text
(<+>) = 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
isSpaceNotNewline :: Char -> Bool
isSpaceNotNewline c = isSpace c && c /= '\n'
replaceSpaces :: Text -> Text
replaceSpaces = T.map (\c -> if isSpaceNotNewline c then ' ' else c)
moveColumnForToken :: Token -> LaTeX ()
moveColumnForToken t = do
unless (isSpaces (text t)) $ do
log MoveColumn $ text t
moveColumn =<< size (text t)
resetColumn :: LaTeX ()
resetColumn = modify $ \s ->
s { column = 0
, columnsPrev = merge (columns s) (columnsPrev s)
, columns = []
}
where
merge [] old = old
merge new old = new ++ filter ((< leastNew) . columnColumn) old
where
leastNew = columnColumn (last new)
moveColumn :: Int -> LaTeX ()
moveColumn i = modify $ \s -> s { column = i + column s }
registerColumn :: Kind -> LaTeX AlignmentColumn
registerColumn kind = do
column <- gets column
codeBlock <- gets codeBlock
kind <- case kind of
Alignment -> return Nothing
Indentation -> do
nextId <- gets nextId
modify $ \s -> s { nextId = succ nextId }
return (Just nextId)
let c = AlignmentColumn { columnColumn = column
, columnCodeBlock = codeBlock
, columnKind = kind
}
modify $ \s -> s { columns = c : columns s }
return c
useColumn :: AlignmentColumn -> LaTeX ()
useColumn c = case columnKind c of
Nothing -> return ()
Just i -> modify $ \s ->
s { usedColumns = Set.insert i (usedColumns s) }
columnZero :: LaTeX AlignmentColumn
columnZero = do
codeBlock <- gets codeBlock
return $ AlignmentColumn { columnColumn = 0
, columnCodeBlock = codeBlock
, columnKind = Nothing
}
registerColumnZero :: LaTeX ()
registerColumnZero = do
c <- columnZero
modify $ \s -> s { columns = [c] }
enterCode :: LaTeX ()
enterCode = do
resetColumn
modify $ \s -> s { codeBlock = codeBlock s + 1 }
leaveCode :: LaTeX ()
leaveCode = return ()
logHelper :: Debug -> Text -> [String] -> LaTeX ()
logHelper debug text extra =
when (debug `elem` debugs) $ do
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
cols <- gets columns
logHelper MoveColumn text ["columns=", show cols]
log Code text = do
cols <- gets columns
col <- gets column
logHelper Code text ["columns=", show cols, "col=", show col]
log debug text = logHelper debug text []
log' :: Debug -> String -> LaTeX ()
log' d = log d . T.pack
output :: Output -> LaTeX ()
output item = do
log' Output (show item)
tell [item]
nl, beginCode, endCode :: Text
nl = T.pack "%\n"
beginCode = T.pack "\\begin{code}"
endCode = T.pack "\\end{code}"
agdaSpace :: Text
agdaSpace = cmdPrefix <+> T.pack "Space" <+> cmdArg T.empty <+> nl
columnName :: AlignmentColumn -> Text
columnName c = T.pack $ case columnKind c of
Nothing -> show (columnColumn c)
Just i -> show i ++ "I"
ptOpen' :: Text -> Text
ptOpen' name = T.pack "\\>[" <+> name <+> T.singleton ']'
ptOpen :: AlignmentColumn -> Text
ptOpen c = ptOpen' (columnName c)
ptOpenBeginningOfLine :: Text
ptOpenBeginningOfLine = ptOpen' (T.pack ".")
ptOpenIndent
:: AlignmentColumn
-> Int
-> Text
ptOpenIndent c delta =
ptOpen c <+> T.pack "[@{}l@{"
<+> cmdPrefix
<+> T.pack "Indent"
<+> cmdArg (T.pack $ show delta)
<+> T.pack "}]"
ptClose :: Text
ptClose = T.pack "\\<"
ptClose' :: AlignmentColumn -> Text
ptClose' c =
ptClose <+> T.singleton '[' <+> columnName c <+> T.singleton ']'
ptNL :: Text
ptNL = nl <+> T.pack "\\\\\n"
ptEmptyLine :: Text
ptEmptyLine =
nl <+> T.pack "\\\\["
<+> cmdPrefix
<+> T.pack "EmptyExtraSkip"
<+> T.pack "]%\n"
cmdPrefix :: Text
cmdPrefix = T.pack "\\Agda"
cmdArg :: Text -> Text
cmdArg x = T.singleton '{' <+> x <+> T.singleton '}'
processLayers :: [(LayerRole, Tokens)] -> LaTeX ()
processLayers = mapM_ $ \(layerRole,toks) -> do
case layerRole of
L.Markup -> processMarkup toks
L.Comment -> processComment toks
L.Code -> processCode toks
processMarkup, processComment, processCode :: Tokens -> LaTeX ()
processMarkup = mapM_ $ \t -> do
moveColumnForToken t
output (Text (text t))
processComment = mapM_ $ \t -> do
unless (T.singleton '%' == T.take 1 (T.stripStart (text t))) $ do
moveColumnForToken t
output (Text (text t))
processCode toks' = do
output $ Text nl
enterCode
mapM_ go toks'
ptOpenWhenColumnZero =<< gets column
output $ Text $ ptClose <+> nl
leaveCode
where
go tok' = do
col <- gets column
moveColumnForToken tok'
let tok = text tok'
log Code tok
if (tok == T.empty) then return ()
else do
if (isSpaces tok) then do
spaces $ T.group $ replaceSpaces tok
else do
ptOpenWhenColumnZero col
output $ Text $
foldr (\c t -> cmdPrefix <+> T.pack c <+> cmdArg t)
(escape tok)
$ concatMap fromAspect (toList $ aspect $ info tok')
++ map fromOtherAspect (otherAspects $ info tok')
ptOpenWhenColumnZero col =
when (col == 0) $ do
registerColumnZero
output . Text . ptOpen =<< columnZero
fromOtherAspect :: OtherAspect -> String
fromOtherAspect = show
fromAspect :: Aspect -> [String]
fromAspect a = let s = [show a] in case a of
Comment -> s
Option -> s
Keyword -> s
String -> s
Number -> s
Symbol -> s
PrimitiveType -> s
Name Nothing isOp -> fromAspect (Name (Just Postulate) isOp)
Name (Just kind) isOp ->
(\c -> if isOp then ["Operator", c] else [c]) $
case kind of
Bound -> s
Constructor Inductive -> "InductiveConstructor"
Constructor CoInductive -> "CoinductiveConstructor"
Datatype -> s
Field -> s
Function -> s
Module -> s
Postulate -> s
Primitive -> s
Record -> s
Argument -> s
Macro -> s
where
s = show kind
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
'_' -> "\\AgdaUnderscore{}"
'{' -> "\\{"
'}' -> "\\}"
'#' -> "\\#"
'$' -> "\\$"
'&' -> "\\&"
'%' -> "\\%"
'~' -> "\\textasciitilde{}"
'^' -> "\\textasciicircum{}"
'\\' -> "\\textbackslash{}"
'-' -> "{-}"
_ -> [ c ]
escape _ = __IMPOSSIBLE__
spaces :: [Text] -> LaTeX ()
spaces [] = return ()
spaces (s@(T.uncons -> Just ('\n', _)) : ss) = do
col <- gets column
when (col == 0) $
output . Text . ptOpen =<< columnZero
output $ Text $ ptClose <+> ptNL <+>
T.replicate (T.length s - 1) ptEmptyLine
resetColumn
spaces ss
spaces (_ : ss@(_ : _)) = spaces ss
spaces [ s ] = do
col <- gets column
let len = T.length s
kind = if col /= 0 && len == 1
then Indentation
else Alignment
moveColumn len
column <- registerColumn kind
if col /= 0
then log' Spaces "col /= 0"
else do
columns <- gets columnsPrev
codeBlock <- gets codeBlock
log' Spaces $
"col == 0: " ++ show (len, columns)
case filter ((<= len) . columnColumn) columns of
c : _ | columnColumn c == len, isJust (columnKind c) -> do
useColumn c
output $ Text $ ptOpenBeginningOfLine
output $ Text $ ptClose' c
c : _ | columnColumn c < len -> do
useColumn c
output $ Text $ ptOpenIndent c (codeBlock - columnCodeBlock c)
_ -> return ()
output $ MaybeColumn column
stringLiteral :: Token -> Tokens
stringLiteral t | aspect (info t) == Just String =
reverse $ foldl (\xs x -> t { text = x } : xs) []
$ concatMap leadingSpaces
$ List.intersperse (T.pack "\n")
$ T.lines (text t)
where
leadingSpaces :: Text -> [Text]
leadingSpaces t = [pre, suf]
where (pre , suf) = T.span isSpaceNotNewline t
stringLiteral t = [t]
defaultStyFile :: String
defaultStyFile = "agda.sty"
generateLaTeX :: Interface -> TCM ()
generateLaTeX i = do
let mod = toTopLevelModuleName $ iModuleName i
hi = iHighlighting i
options <- TCM.commandLineOptions
dir <- case O.optGHCiInteraction options of
False -> return $ O.optLaTeXDir options
True -> do
sourceFile <- Find.findFile mod
return $ filePath (projectRoot sourceFile mod)
</> O.optLaTeXDir options
liftIO $ createDirectoryIfMissing True dir
(code, _, _) <- liftIO $ readProcessWithExitCode
"kpsewhich" [ "--path=" ++ dir, defaultStyFile ] ""
when (code /= ExitSuccess) $ do
TCM.reportSLn "compile.latex" 1 $ unlines
[ defaultStyFile ++ " was not found. Copying a default version of " ++
defaultStyFile
, "into " ++ 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 (O.optCountClusters $ O.optPragmaOptions options)
(mkAbsolute inAbsPath) source hi
createDirectoryIfMissing True $ dir </> takeDirectory outPath
BS.writeFile (dir </> outPath) latex
where
modToFile :: TopLevelModuleName -> FilePath
modToFile m = List.intercalate [pathSeparator] (moduleNameParts m) <.> "tex"
groupByFst :: forall a b. Eq a => [(a,b)] -> [(a,[b])]
groupByFst =
map (\xs -> case xs of
[] -> __IMPOSSIBLE__
(tag, _): _ -> (tag, map snd xs))
. List.groupBy ((==) `on` fst)
toLaTeX
:: Bool
-> AbsolutePath
-> String
-> HighlightingInfo
-> IO L.Text
toLaTeX cc path source hi
= processTokens cc
. map (\(role, tokens) -> (role,) $
(if L.isCode role then
whenMoreThanOne
(withLast $
withTokenText $ \suf ->
fromMaybe suf $
fmap (T.dropWhileEnd isSpaceNotNewline) $
T.stripSuffix (T.singleton '\n') suf)
.
(withLast $ withTokenText $ T.dropWhileEnd isSpaceNotNewline)
.
(withFirst $
withTokenText $ \pre ->
fromMaybe pre $
T.stripPrefix (T.singleton '\n') $
T.dropWhile isSpaceNotNewline pre)
else
id) tokens)
. map (second (
concatMap stringLiteral
. map (\(mi, cs) ->
Token { text = T.pack cs
, info = fromMaybe mempty mi
})
. groupByFst
))
. groupByFst
. map (\(pos, (role, char)) -> (role, (IntMap.lookup pos infoMap, char)))
. zip [1..]
. atomizeLayers . literateTeX (startPos (Just path))
$ source
where
infoMap = toMap (decompress hi)
withLast :: (a -> a) -> [a] -> [a]
withLast f [] = []
withLast f [a] = [f a]
withLast f (a:as) = a:withLast f as
withFirst :: (a -> a) -> [a] -> [a]
withFirst _ [] = []
withFirst f (a:as) = f a:as
whenMoreThanOne :: ([a] -> [a]) -> [a] -> [a]
whenMoreThanOne f xs@(_:_:_) = f xs
whenMoreThanOne _ xs = xs
processTokens
:: Bool
-> [(LayerRole, Tokens)]
-> IO L.Text
processTokens cc ts = do
((), s, os) <- runLaTeX (processLayers ts) () (emptyState cc)
return $ L.fromChunks $ map (render s) os
where
render _ (Text s) = s
render s (MaybeColumn c)
| Just i <- columnKind c,
not (Set.member i (usedColumns s)) = agdaSpace
| otherwise = nl <+> ptOpen c