{-# LANGUAGE CPP #-}
{-# LANGUAGE ViewPatterns #-}

-- | Function for generating highlighted and aligned LaTeX from literate
-- Agda source.

module Agda.Interaction.Highlighting.LaTeX.Base
  ( generateLaTeXIO
  , prepareCommonAssets
  , runLogLaTeXTWith
  , logMsgToText
  , LogMessage(..)
  , MonadLogLaTeX
  , LogLaTeXT
  , LaTeXOptions(..)
  ) where

import Prelude hiding (log)

import Data.Bifunctor (second)
import Data.Char
import Data.Maybe
import Data.Function
import Data.Foldable (toList)
#if !(MIN_VERSION_base(4,11,0))
import Data.Semigroup (Semigroup(..))
#endif
import qualified Data.Text as T

import Control.Exception.Base (IOException, try)
import Control.Monad (forM_, mapM_, unless, when)
import Control.Monad.Trans.Reader as R ( ReaderT(runReaderT))
import Control.Monad.RWS.Strict
  ( RWST(runRWST)
  , MonadReader(..), asks
  , MonadState(..), gets, modify
  , lift, tell
  )
import Control.Monad.IO.Class
  ( MonadIO(..)
  )

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.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.Common
import Agda.Syntax.Parser.Literate (literateTeX, LayerRole, atomizeLayers)
import qualified Agda.Syntax.Parser.Literate as L
import Agda.Syntax.Position (RangeFile, startPos)
import Agda.Syntax.TopLevelModuleName
  (TopLevelModuleName, moduleNameParts)

import Agda.Interaction.Highlighting.Precise hiding (toList)

import Agda.TypeChecking.Monad (Interface(..)) --, reportSLn)

import Agda.Utils.Function (applyWhen)
import Agda.Utils.Functor  ((<&>))
import Agda.Utils.List     (last1, updateHead, updateLast)
import Agda.Utils.Maybe    (whenJust)
import Agda.Utils.Monad
import qualified Agda.Utils.List1 as List1

import Agda.Utils.Impossible

------------------------------------------------------------------------
-- * Logging

class Monad m => MonadLogLaTeX m where
  logLaTeX :: LogMessage -> m ()

-- | Log LaTeX messages using a provided action.
--
-- This could be accomplished by putting logs into the RWST output and splitting it
-- into a WriterT, but that becomes slightly more complicated to reason about in
-- the presence of IO exceptions.
--
-- We want the logging to be reasonably polymorphic, avoid space leaks that can occur
-- with WriterT, and also be usable during outer phases such as directory preparation.
--
-- I'm not certain this is the best way to do it, but whatever.
type LogLaTeXT m = ReaderT (LogMessage -> m ()) m

instance Monad m => MonadLogLaTeX (LogLaTeXT m) where
  logLaTeX :: LogMessage -> LogLaTeXT m ()
logLaTeX LogMessage
message = do
    LogMessage -> m ()
doLog <- forall r (m :: * -> *). MonadReader r m => m r
ask
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ LogMessage -> m ()
doLog LogMessage
message

runLogLaTeXTWith :: Monad m => (LogMessage -> m ()) -> LogLaTeXT m a -> m a
runLogLaTeXTWith :: forall (m :: * -> *) a.
Monad m =>
(LogMessage -> m ()) -> LogLaTeXT m a -> m a
runLogLaTeXTWith = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT

-- Not currently used, but for example:
-- runLogLaTeXWithIO :: MonadIO m => LogLaTeXT m a -> m a
-- runLogLaTeXWithIO = runLogLaTeXTWith $ liftIO . T.putStrLn . logMsgToText

------------------------------------------------------------------------
-- * Datatypes.

-- | The @LaTeX@ monad is a combination of @ExceptT@, @RWST@ and
-- a logger @m@. The error part is just used to keep track whether we finished or
-- not, the reader part contains static options used, the writer is where the
-- output goes and the state is for keeping track of the tokens and some
-- other useful info, and the MonadLogLaTeX part is used for printing debugging info.

type LaTeX a = forall m. MonadLogLaTeX m => RWST Env [Output] State m a

-- | Output items.

data LogMessage = LogMessage Debug Text [Text] deriving Int -> LogMessage -> ShowS
[LogMessage] -> ShowS
LogMessage -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [LogMessage] -> ShowS
$cshowList :: [LogMessage] -> ShowS
show :: LogMessage -> [Char]
$cshow :: LogMessage -> [Char]
showsPrec :: Int -> LogMessage -> ShowS
$cshowsPrec :: Int -> LogMessage -> ShowS
Show

data Output
  = Text !Text
    -- ^ A piece of text.
  | MaybeColumn !AlignmentColumn
    -- ^ A column. If it turns out to be an indentation column that is
    --   not used to indent or align something, then no column will be
    --   generated, only whitespace ('agdaSpace').
  deriving Int -> Output -> ShowS
[Output] -> ShowS
Output -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Output] -> ShowS
$cshowList :: [Output] -> ShowS
show :: Output -> [Char]
$cshow :: Output -> [Char]
showsPrec :: Int -> Output -> ShowS
$cshowsPrec :: Int -> Output -> ShowS
Show

-- | Column kinds.

data Kind
  = Indentation
    -- ^ Used only for indentation (the placement of the first token
    -- on a line, relative to tokens on previous lines).
  | Alignment
    -- ^ Used both for indentation and for alignment.
  deriving (Kind -> Kind -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Kind -> Kind -> Bool
$c/= :: Kind -> Kind -> Bool
== :: Kind -> Kind -> Bool
$c== :: Kind -> Kind -> Bool
Eq, Int -> Kind -> ShowS
[Kind] -> ShowS
Kind -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Kind] -> ShowS
$cshowList :: [Kind] -> ShowS
show :: Kind -> [Char]
$cshow :: Kind -> [Char]
showsPrec :: Int -> Kind -> ShowS
$cshowsPrec :: Int -> Kind -> ShowS
Show)

-- | Unique identifiers for indentation columns.

type IndentationColumnId = Int

-- | Alignment and indentation columns.

data AlignmentColumn = AlignmentColumn
  { AlignmentColumn -> Int
columnCodeBlock :: !Int
    -- ^ The column's code block.
  , AlignmentColumn -> Int
columnColumn :: !Int
    -- ^ The column number.
  , AlignmentColumn -> Maybe Int
columnKind :: Maybe IndentationColumnId
    -- ^ The column kind. 'Nothing' for alignment columns and @'Just'
    -- i@ for indentation columns, where @i@ is the column's unique
    -- identifier.
  } deriving Int -> AlignmentColumn -> ShowS
[AlignmentColumn] -> ShowS
AlignmentColumn -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [AlignmentColumn] -> ShowS
$cshowList :: [AlignmentColumn] -> ShowS
show :: AlignmentColumn -> [Char]
$cshow :: AlignmentColumn -> [Char]
showsPrec :: Int -> AlignmentColumn -> ShowS
$cshowsPrec :: Int -> AlignmentColumn -> ShowS
Show

-- | Type of function for estimating column width of text.

type TextWidthEstimator = Text -> Int

data Env = Env
  { Env -> TextWidthEstimator
estimateTextWidth :: !TextWidthEstimator
    -- ^ How to estimate the column width of text (i.e. Count extended grapheme clusters vs. code points).
  , Env -> [Debug]
debugs :: [Debug]
    -- ^ Says what debug information should printed.
  }

data State = State
  { State -> Int
codeBlock     :: !Int   -- ^ The number of the current code block.
  , State -> Int
column        :: !Int   -- ^ The current column number.
  , State -> [AlignmentColumn]
columns       :: [AlignmentColumn]
                            -- ^ All alignment columns found on the
                            --   current line (so far), in reverse
                            --   order.
  , State -> [AlignmentColumn]
columnsPrev   :: [AlignmentColumn]
                            -- ^ All alignment columns found in
                            --   previous lines (in any code block),
                            --   with larger columns coming first.
  , State -> Int
nextId        :: !IndentationColumnId
                            -- ^ The next indentation column
                            -- identifier.
  , State -> HashSet Int
usedColumns   :: HashSet IndentationColumnId
                            -- ^ Indentation columns that have
                            -- actually
                            --   been used.
  }

type Tokens = [Token]

data Token = Token
  { Token -> Text
text     :: !Text
  , Token -> Aspects
info     :: Aspects
  }
  deriving Int -> Token -> ShowS
[Token] -> ShowS
Token -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Token] -> ShowS
$cshowList :: [Token] -> ShowS
show :: Token -> [Char]
$cshow :: Token -> [Char]
showsPrec :: Int -> Token -> ShowS
$cshowsPrec :: Int -> Token -> ShowS
Show

withTokenText :: (Text -> Text) -> Token -> Token
withTokenText :: (Text -> Text) -> Token -> Token
withTokenText Text -> Text
f tok :: Token
tok@Token{text :: Token -> Text
text = Text
t} = Token
tok{text :: Text
text = Text -> Text
f Text
t}

data Debug = MoveColumn | NonCode | Code | Spaces | Output | FileSystem
  deriving (Debug -> Debug -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Debug -> Debug -> Bool
$c/= :: Debug -> Debug -> Bool
== :: Debug -> Debug -> Bool
$c== :: Debug -> Debug -> Bool
Eq, Int -> Debug -> ShowS
[Debug] -> ShowS
Debug -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Debug] -> ShowS
$cshowList :: [Debug] -> ShowS
show :: Debug -> [Char]
$cshow :: Debug -> [Char]
showsPrec :: Int -> Debug -> ShowS
$cshowsPrec :: Int -> Debug -> ShowS
Show)

-- | Run function for the @LaTeX@ monad.
runLaTeX :: MonadLogLaTeX m =>
  LaTeX a -> Env -> State -> m (a, State, [Output])
-- ASR (2021-02-07). The eta-expansion is required by GHC >= 9.0.1
-- (see Issue #4955).
runLaTeX :: forall (m :: * -> *) a.
MonadLogLaTeX m =>
LaTeX a -> Env -> State -> m (a, State, [Output])
runLaTeX LaTeX a
l = forall r w s (m :: * -> *) a.
RWST r w s m a -> r -> s -> m (a, s, w)
runRWST LaTeX a
l

emptyState :: State
emptyState :: State
emptyState = State
  { codeBlock :: Int
codeBlock     = Int
0
  , column :: Int
column        = Int
0
  , columns :: [AlignmentColumn]
columns       = []
  , columnsPrev :: [AlignmentColumn]
columnsPrev   = []
  , nextId :: Int
nextId        = Int
0
  , usedColumns :: HashSet Int
usedColumns   = forall a. HashSet a
Set.empty
  }

emptyEnv
  :: TextWidthEstimator  -- ^ Count extended grapheme clusters?
  -> Env
emptyEnv :: TextWidthEstimator -> Env
emptyEnv TextWidthEstimator
twe = TextWidthEstimator -> [Debug] -> Env
Env TextWidthEstimator
twe []


------------------------------------------------------------------------
-- * Some helpers.

-- | Gives the size of the string. If cluster counting is enabled,
-- then the number of extended grapheme clusters is computed (the root
-- locale is used), and otherwise the number of code points.

size :: Text -> LaTeX Int
size :: Text -> LaTeX Int
size Text
t = forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Env -> TextWidthEstimator
estimateTextWidth forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> (forall a b. (a -> b) -> a -> b
$ Text
t)

-- | Does the string consist solely of whitespace?

isSpaces :: Text -> Bool
isSpaces :: Text -> Bool
isSpaces = (Char -> Bool) -> Text -> Bool
T.all Char -> Bool
isSpace

-- | Is the character a whitespace character distinct from '\n'?

isSpaceNotNewline :: Char -> Bool
isSpaceNotNewline :: Char -> Bool
isSpaceNotNewline Char
c = Char -> Bool
isSpace Char
c Bool -> Bool -> Bool
&& Char
c forall a. Eq a => a -> a -> Bool
/= Char
'\n'

-- | Replaces all forms of whitespace, except for new-line characters,
-- with spaces.

replaceSpaces :: Text -> Text
replaceSpaces :: Text -> Text
replaceSpaces = (Char -> Char) -> Text -> Text
T.map (\Char
c -> if Char -> Bool
isSpaceNotNewline Char
c then Char
' ' else Char
c)


-- | If the `Token` consists of spaces, the internal column counter is advanced
--   by the length of the token. Otherwise, `moveColumnForToken` is a no-op.
moveColumnForToken :: Token -> LaTeX ()
moveColumnForToken :: Token -> LaTeX ()
moveColumnForToken Token{ text :: Token -> Text
text = Text
t } = do
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Text -> Bool
isSpaces Text
t) forall a b. (a -> b) -> a -> b
$ do
    Debug -> Text -> LaTeX ()
log Debug
MoveColumn Text
t
    -- ASR (2021-02-07). The eta-expansion is required by GHC >= 9.0.1
    -- (see Issue #4955).
    Int
n <- Text -> LaTeX Int
size Text
t
    Int -> LaTeX ()
moveColumn Int
n

-- | Merges 'columns' into 'columnsPrev', resets 'column' and
-- 'columns'

resetColumn :: LaTeX ()
resetColumn :: LaTeX ()
resetColumn = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \State
s ->
  State
s { column :: Int
column      = Int
0
    , columnsPrev :: [AlignmentColumn]
columnsPrev = [AlignmentColumn] -> [AlignmentColumn] -> [AlignmentColumn]
mergeCols (State -> [AlignmentColumn]
columns State
s) (State -> [AlignmentColumn]
columnsPrev State
s)
    , columns :: [AlignmentColumn]
columns     = []
    }
  where
  -- Remove shadowed columns from old.
  mergeCols :: [AlignmentColumn] -> [AlignmentColumn] -> [AlignmentColumn]
mergeCols []         [AlignmentColumn]
old = [AlignmentColumn]
old
  mergeCols new :: [AlignmentColumn]
new@(AlignmentColumn
n:[AlignmentColumn]
ns) [AlignmentColumn]
old = [AlignmentColumn]
new forall a. [a] -> [a] -> [a]
++ forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Ord a => a -> a -> Bool
< Int
leastNew) forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlignmentColumn -> Int
columnColumn) [AlignmentColumn]
old
    where
    leastNew :: Int
leastNew = AlignmentColumn -> Int
columnColumn (forall a. a -> [a] -> a
last1 AlignmentColumn
n [AlignmentColumn]
ns)

moveColumn :: Int -> LaTeX ()
moveColumn :: Int -> LaTeX ()
moveColumn Int
i = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \State
s -> State
s { column :: Int
column = Int
i forall a. Num a => a -> a -> a
+ State -> Int
column State
s }

-- | Registers a column of the given kind. The column is returned.

registerColumn :: Kind -> LaTeX AlignmentColumn
registerColumn :: Kind -> LaTeX AlignmentColumn
registerColumn Kind
kind = do
  Int
column    <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> Int
column
  Int
codeBlock <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> Int
codeBlock
  Maybe Int
colKind   <- case Kind
kind of
                 Kind
Alignment   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
                 Kind
Indentation -> do
                   Int
nextId <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> Int
nextId
                   forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \State
s -> State
s { nextId :: Int
nextId = forall a. Enum a => a -> a
succ Int
nextId }
                   forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Int
nextId)
  let c :: AlignmentColumn
c = AlignmentColumn { columnColumn :: Int
columnColumn    = Int
column
                          , columnCodeBlock :: Int
columnCodeBlock = Int
codeBlock
                          , columnKind :: Maybe Int
columnKind      = Maybe Int
colKind
                          }
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \State
s -> State
s { columns :: [AlignmentColumn]
columns = AlignmentColumn
c forall a. a -> [a] -> [a]
: State -> [AlignmentColumn]
columns State
s }
  forall (m :: * -> *) a. Monad m => a -> m a
return AlignmentColumn
c

-- | Registers the given column as used (if it is an indentation
-- column).

useColumn :: AlignmentColumn -> LaTeX ()
useColumn :: AlignmentColumn -> LaTeX ()
useColumn AlignmentColumn
c = forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (AlignmentColumn -> Maybe Int
columnKind AlignmentColumn
c) forall a b. (a -> b) -> a -> b
$ \ Int
i ->
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \ State
s -> State
s { usedColumns :: HashSet Int
usedColumns = forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
Set.insert Int
i (State -> HashSet Int
usedColumns State
s) }

-- | Alignment column zero in the current code block.

columnZero :: LaTeX AlignmentColumn
columnZero :: LaTeX AlignmentColumn
columnZero = do
  Int
codeBlock <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> Int
codeBlock
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ AlignmentColumn { columnColumn :: Int
columnColumn    = Int
0
                           , columnCodeBlock :: Int
columnCodeBlock = Int
codeBlock
                           , columnKind :: Maybe Int
columnKind      = forall a. Maybe a
Nothing
                           }

-- | Registers column zero as an alignment column.

registerColumnZero :: LaTeX ()
registerColumnZero :: LaTeX ()
registerColumnZero = do
  AlignmentColumn
c <- LaTeX AlignmentColumn
columnZero
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \State
s -> State
s { columns :: [AlignmentColumn]
columns = [AlignmentColumn
c] }

-- | Changes to the state that are performed at the start of a code
-- block.

enterCode :: LaTeX ()
enterCode :: LaTeX ()
enterCode = do
  LaTeX ()
resetColumn
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \State
s -> State
s { codeBlock :: Int
codeBlock = State -> Int
codeBlock State
s forall a. Num a => a -> a -> a
+ Int
1 }

-- | Changes to the state that are performed at the end of a code
-- block.

leaveCode :: LaTeX ()
leaveCode :: LaTeX ()
leaveCode = forall (m :: * -> *) a. Monad m => a -> m a
return ()

tshow :: Show a => a -> Text
tshow :: forall a. Show a => a -> Text
tshow = [Char] -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show

logMsgToText :: LogMessage -> Text
logMsgToText :: LogMessage -> Text
logMsgToText (LogMessage Debug
messageLabel Text
text [Text]
extra) = [Text] -> Text
T.concat forall a b. (a -> b) -> a -> b
$
  [ forall a. Show a => a -> Text
tshow Debug
messageLabel, Text
": '", Text
text, Text
"' "
  ] forall a. [a] -> [a] -> [a]
++ if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Text]
extra then [] else [Text
"(", [Text] -> Text
T.unwords [Text]
extra, Text
")"]

logHelper :: Debug -> Text -> [Text] -> LaTeX ()
logHelper :: Debug -> Text -> [Text] -> LaTeX ()
logHelper Debug
debug Text
text [Text]
extra = do
  [Debug]
logLevels <- Env -> [Debug]
debugs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *). MonadReader r m => m r
ask
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Debug
debug forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Debug]
logLevels) forall a b. (a -> b) -> a -> b
$ do
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadLogLaTeX m => LogMessage -> m ()
logLaTeX (Debug -> Text -> [Text] -> LogMessage
LogMessage Debug
debug Text
text [Text]
extra)

log :: Debug -> Text -> LaTeX ()
log :: Debug -> Text -> LaTeX ()
log Debug
MoveColumn Text
text = do
  [AlignmentColumn]
cols <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> [AlignmentColumn]
columns
  Debug -> Text -> [Text] -> LaTeX ()
logHelper Debug
MoveColumn Text
text [Text
"columns=", forall a. Show a => a -> Text
tshow [AlignmentColumn]
cols]
log Debug
Code Text
text = do
  [AlignmentColumn]
cols <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> [AlignmentColumn]
columns
  Int
col <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> Int
column
  Debug -> Text -> [Text] -> LaTeX ()
logHelper Debug
Code Text
text [Text
"columns=", forall a. Show a => a -> Text
tshow [AlignmentColumn]
cols, Text
"col=", forall a. Show a => a -> Text
tshow Int
col]
log Debug
debug Text
text = Debug -> Text -> [Text] -> LaTeX ()
logHelper Debug
debug Text
text []

output :: Output -> LaTeX ()
output :: Output -> LaTeX ()
output Output
item = do
  Debug -> Text -> LaTeX ()
log Debug
Output forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> Text
tshow Output
item
  forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Output
item]

------------------------------------------------------------------------
-- * LaTeX and polytable strings.

-- Polytable, http://www.ctan.org/pkg/polytable, is used for code
-- alignment, similar to lhs2TeX's approach.

nl :: Text
nl :: Text
nl = Text
"%\n"

-- | A command that is used when two tokens are put next to each other
-- in the same column.

agdaSpace :: Text
agdaSpace :: Text
agdaSpace = Text
cmdPrefix forall a. Semigroup a => a -> a -> a
<> Text
"Space" forall a. Semigroup a => a -> a -> a
<> Text -> Text
cmdArg Text
T.empty forall a. Semigroup a => a -> a -> a
<> Text
nl

-- | The column's name.
--
-- Indentation columns have unique names, distinct from all alignment
-- column names.

columnName :: AlignmentColumn -> Text
columnName :: AlignmentColumn -> Text
columnName AlignmentColumn
c = [Char] -> Text
T.pack forall a b. (a -> b) -> a -> b
$ case AlignmentColumn -> Maybe Int
columnKind AlignmentColumn
c of
  Maybe Int
Nothing -> forall a. Show a => a -> [Char]
show (AlignmentColumn -> Int
columnColumn AlignmentColumn
c)
  Just Int
i  -> forall a. Show a => a -> [Char]
show Int
i forall a. [a] -> [a] -> [a]
++ [Char]
"I"

-- | Opens a column with the given name.

ptOpen' :: Text -> Text
ptOpen' :: Text -> Text
ptOpen' Text
name = Text
"\\>[" forall a. Semigroup a => a -> a -> a
<> Text
name forall a. Semigroup a => a -> a -> a
<> Text
"]"

-- | Opens the given column.

ptOpen :: AlignmentColumn -> Text
ptOpen :: AlignmentColumn -> Text
ptOpen AlignmentColumn
c = Text -> Text
ptOpen' (AlignmentColumn -> Text
columnName AlignmentColumn
c)

-- | Opens a special column that is only used at the beginning of
-- lines.

ptOpenBeginningOfLine :: Text
ptOpenBeginningOfLine :: Text
ptOpenBeginningOfLine = Text -> Text
ptOpen' Text
"." forall a. Semigroup a => a -> a -> a
<> Text
"[@{}l@{}]"

-- | Opens the given column, and inserts an indentation instruction
-- with the given argument at the end of it.

ptOpenIndent
  :: AlignmentColumn
  -> Int              -- ^ Indentation instruction argument.
  -> Text
ptOpenIndent :: AlignmentColumn -> Int -> Text
ptOpenIndent AlignmentColumn
c Int
delta =
  AlignmentColumn -> Text
ptOpen AlignmentColumn
c forall a. Semigroup a => a -> a -> a
<> Text
"[@{}l@{"
           forall a. Semigroup a => a -> a -> a
<> Text
cmdPrefix
           forall a. Semigroup a => a -> a -> a
<> Text
"Indent"
           forall a. Semigroup a => a -> a -> a
<> Text -> Text
cmdArg ([Char] -> Text
T.pack forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show Int
delta)
           forall a. Semigroup a => a -> a -> a
<> Text
"}]"

ptClose :: Text
ptClose :: Text
ptClose = Text
"\\<"

ptClose' :: AlignmentColumn -> Text
ptClose' :: AlignmentColumn -> Text
ptClose' AlignmentColumn
c =
  Text
ptClose forall a. Semigroup a => a -> a -> a
<> Text
"[" forall a. Semigroup a => a -> a -> a
<> AlignmentColumn -> Text
columnName AlignmentColumn
c forall a. Semigroup a => a -> a -> a
<> Text
"]"

ptNL :: Text
ptNL :: Text
ptNL = Text
nl forall a. Semigroup a => a -> a -> a
<> Text
"\\\\\n"

ptEmptyLine :: Text
ptEmptyLine :: Text
ptEmptyLine =
  Text
nl forall a. Semigroup a => a -> a -> a
<> Text
"\\\\["
     forall a. Semigroup a => a -> a -> a
<> Text
cmdPrefix
     forall a. Semigroup a => a -> a -> a
<> Text
"EmptyExtraSkip"
     forall a. Semigroup a => a -> a -> a
<> Text
"]%\n"

cmdPrefix :: Text
cmdPrefix :: Text
cmdPrefix = Text
"\\Agda"

cmdArg :: Text -> Text
cmdArg :: Text -> Text
cmdArg Text
x = Text
"{" forall a. Semigroup a => a -> a -> a
<> Text
x forall a. Semigroup a => a -> a -> a
<> Text
"}"

------------------------------------------------------------------------
-- * Output generation from a stream of labelled tokens.

processLayers :: [(LayerRole, Tokens)] -> LaTeX ()
-- ASR (2021-02-07). The eta-expansion on @lt@ is required by GHC >=
-- 9.0.1 (see Issue #4955).
processLayers :: [(LayerRole, [Token])] -> LaTeX ()
processLayers [(LayerRole, [Token])]
lt = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(LayerRole, [Token])]
lt forall a b. (a -> b) -> a -> b
$ \ (LayerRole
layerRole,[Token]
toks) -> do
  case LayerRole
layerRole of
    LayerRole
L.Markup  -> [Token] -> LaTeX ()
processMarkup  [Token]
toks
    LayerRole
L.Comment -> [Token] -> LaTeX ()
processComment [Token]
toks
    LayerRole
L.Code    -> [Token] -> LaTeX ()
processCode    [Token]
toks

-- | Deals with markup, which is output verbatim.
processMarkup :: Tokens -> LaTeX ()
-- ASR (2021-02-07). The eta-expansion on @ts@ is required by GHC >=
-- 9.0.1 (see Issue #4955).
processMarkup :: [Token] -> LaTeX ()
processMarkup [Token]
ts = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Token]
ts forall a b. (a -> b) -> a -> b
$ \ Token
t' -> do
  Token -> LaTeX ()
moveColumnForToken Token
t'
  Output -> LaTeX ()
output (Text -> Output
Text (Token -> Text
text Token
t'))

-- | Deals with literate text, which is output verbatim
processComment :: Tokens -> LaTeX ()
-- ASR (2021-02-07). The eta-expansion with @ts@ is required by GHC >=
-- 9.0.1 (see Issue #4955).
processComment :: [Token] -> LaTeX ()
processComment [Token]
ts = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Token]
ts forall a b. (a -> b) -> a -> b
$ \ Token
t' -> do
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Text
"%" forall a. Eq a => a -> a -> Bool
== Int -> Text -> Text
T.take Int
1 (Text -> Text
T.stripStart (Token -> Text
text Token
t'))) forall a b. (a -> b) -> a -> b
$ do
    Token -> LaTeX ()
moveColumnForToken Token
t'
  Output -> LaTeX ()
output (Text -> Output
Text (Token -> Text
text Token
t'))

-- | Deals with code blocks. Every token, except spaces, is pretty
-- printed as a LaTeX command.
processCode :: Tokens -> LaTeX ()
processCode :: [Token] -> LaTeX ()
processCode [Token]
toks' = do
  Output -> LaTeX ()
output forall a b. (a -> b) -> a -> b
$ Text -> Output
Text Text
nl
  LaTeX ()
enterCode
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {m :: * -> *}.
MonadLogLaTeX m =>
Token -> RWST Env [Output] State m ()
go [Token]
toks'
  forall {m :: * -> *} {a}.
(Eq a, Num a, MonadLogLaTeX m) =>
a -> RWST Env [Output] State m ()
ptOpenWhenColumnZero forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> Int
column
  Output -> LaTeX ()
output forall a b. (a -> b) -> a -> b
$ Text -> Output
Text forall a b. (a -> b) -> a -> b
$ Text
ptClose forall a. Semigroup a => a -> a -> a
<> Text
nl
  LaTeX ()
leaveCode

  where
    go :: Token -> RWST Env [Output] State m ()
go tok' :: Token
tok'@Token{ text :: Token -> Text
text = Text
tok } = do
      -- Get the column information before grabbing the token, since
      -- grabbing (possibly) moves the column.
      Int
col  <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> Int
column

      Token -> LaTeX ()
moveColumnForToken Token
tok'
      Debug -> Text -> LaTeX ()
log Debug
Code Text
tok

      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Text -> Bool
T.null Text
tok) forall a b. (a -> b) -> a -> b
$
        if (Text -> Bool
isSpaces Text
tok) then do
            [Text] -> LaTeX ()
spaces forall a b. (a -> b) -> a -> b
$ Text -> [Text]
T.group forall a b. (a -> b) -> a -> b
$ Text -> Text
replaceSpaces Text
tok
        else do
          forall {m :: * -> *} {a}.
(Eq a, Num a, MonadLogLaTeX m) =>
a -> RWST Env [Output] State m ()
ptOpenWhenColumnZero Int
col
          Output -> LaTeX ()
output forall a b. (a -> b) -> a -> b
$ Text -> Output
Text forall a b. (a -> b) -> a -> b
$
            -- we return the escaped token wrapped in commands corresponding
            -- to its aspect (if any) and other aspects (e.g. error, unsolved meta)
            forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\[Char]
c Text
t -> Text
cmdPrefix forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
T.pack [Char]
c forall a. Semigroup a => a -> a -> a
<> Text -> Text
cmdArg Text
t)
                  (Text -> Text
escape Text
tok)
                  forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map OtherAspect -> [Char]
fromOtherAspect (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall a b. (a -> b) -> a -> b
$ Aspects -> Set OtherAspect
otherAspects forall a b. (a -> b) -> a -> b
$ Token -> Aspects
info Token
tok') forall a. [a] -> [a] -> [a]
++
                    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Aspect -> [[Char]]
fromAspect (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall a b. (a -> b) -> a -> b
$ Aspects -> Maybe Aspect
aspect forall a b. (a -> b) -> a -> b
$ Token -> Aspects
info Token
tok')

    -- Non-whitespace tokens at the start of a line trigger an
    -- alignment column.
    ptOpenWhenColumnZero :: a -> RWST Env [Output] State m ()
ptOpenWhenColumnZero a
col =
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (a
col forall a. Eq a => a -> a -> Bool
== a
0) forall a b. (a -> b) -> a -> b
$ do
          LaTeX ()
registerColumnZero
          -- ASR (2021-02-07). The eta-expansion @\o -> output o@ is
          -- required by GHC >= 9.0.1 (see Issue #4955).
          (\Output
o -> Output -> LaTeX ()
output Output
o)forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Output
Text forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlignmentColumn -> Text
ptOpen forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< LaTeX AlignmentColumn
columnZero

    -- Translation from OtherAspect to command strings. So far it happens
    -- to correspond to @show@ but it does not have to (cf. fromAspect)
    fromOtherAspect :: OtherAspect -> String
    fromOtherAspect :: OtherAspect -> [Char]
fromOtherAspect = forall a. Show a => a -> [Char]
show

    fromAspect :: Aspect -> [String]
    fromAspect :: Aspect -> [[Char]]
fromAspect Aspect
a = let s :: [[Char]]
s = [forall a. Show a => a -> [Char]
show Aspect
a] in case Aspect
a of
      Aspect
Comment           -> [[Char]]
s
      Aspect
Keyword           -> [[Char]]
s
      Aspect
Hole              -> [[Char]]
s
      Aspect
String            -> [[Char]]
s
      Aspect
Number            -> [[Char]]
s
      Aspect
Symbol            -> [[Char]]
s
      Aspect
PrimitiveType     -> [[Char]]
s
      Aspect
Pragma            -> [[Char]]
s
      Aspect
Background        -> [[Char]]
s
      Aspect
Markup            -> [[Char]]
s
      Name Maybe NameKind
Nothing Bool
isOp -> Aspect -> [[Char]]
fromAspect (Maybe NameKind -> Bool -> Aspect
Name (forall a. a -> Maybe a
Just NameKind
Postulate) Bool
isOp)
        -- At the time of writing the case above can be encountered in
        -- --only-scope-checking mode, for instance for the token "Size"
        -- in the following code:
        --
        --   {-# BUILTIN SIZE Size #-}
        --
        -- The choice of "Postulate" works for this example, but might
        -- be less appropriate for others.
      Name (Just NameKind
kind) Bool
isOp ->
        (\[Char]
c -> if Bool
isOp then [[Char]
"Operator", [Char]
c] else [[Char]
c]) forall a b. (a -> b) -> a -> b
$
        case NameKind
kind of
          NameKind
Bound                     -> [Char]
sk
          NameKind
Generalizable             -> [Char]
sk
          Constructor Induction
Inductive     -> [Char]
"InductiveConstructor"
          Constructor Induction
CoInductive   -> [Char]
"CoinductiveConstructor"
          NameKind
Datatype                  -> [Char]
sk
          NameKind
Field                     -> [Char]
sk
          NameKind
Function                  -> [Char]
sk
          NameKind
Module                    -> [Char]
sk
          NameKind
Postulate                 -> [Char]
sk
          NameKind
Primitive                 -> [Char]
sk
          NameKind
Record                    -> [Char]
sk
          NameKind
Argument                  -> [Char]
sk
          NameKind
Macro                     -> [Char]
sk
        where
        sk :: [Char]
sk = forall a. Show a => a -> [Char]
show NameKind
kind

-- | Escapes special characters.
escape :: Text -> Text
escape :: Text -> Text
escape (Text -> Maybe (Char, Text)
T.uncons -> Maybe (Char, Text)
Nothing)     = Text
T.empty
escape (Text -> Maybe (Char, Text)
T.uncons -> Just (Char
c, Text
s)) = [Char] -> Text
T.pack (Char -> [Char]
replace Char
c) forall a. Semigroup a => a -> a -> a
<> Text -> Text
escape Text
s
  where
  replace :: Char -> String
  replace :: Char -> [Char]
replace Char
char = case Char
char of
    Char
'_'  -> [Char]
"\\AgdaUnderscore{}"
    Char
'{'  -> [Char]
"\\{"
    Char
'}'  -> [Char]
"\\}"
    Char
'#'  -> [Char]
"\\#"
    Char
'$'  -> [Char]
"\\$"
    Char
'&'  -> [Char]
"\\&"
    Char
'%'  -> [Char]
"\\%"
    Char
'~'  -> [Char]
"\\textasciitilde{}"
    Char
'^'  -> [Char]
"\\textasciicircum{}"
    Char
'\\' -> [Char]
"\\textbackslash{}"
    Char
' '  -> [Char]
"\\ "
    Char
_    -> [ Char
char ]
#if __GLASGOW_HASKELL__ < 810
escape _                         = __IMPOSSIBLE__
#endif

-- | Every element in the list should consist of either one or more
-- newline characters, or one or more space characters. Two adjacent
-- list elements must not contain the same character.
--
-- If the final element of the list consists of spaces, then these
-- spaces are assumed to not be trailing whitespace.
spaces :: [Text] -> LaTeX ()
spaces :: [Text] -> LaTeX ()
spaces [] = forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- Newlines.
spaces (s :: Text
s@(Text -> Maybe (Char, Text)
T.uncons -> Just (Char
'\n', Text
_)) : [Text]
ss) = do
  Int
col <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> Int
column
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
col forall a. Eq a => a -> a -> Bool
== Int
0) forall a b. (a -> b) -> a -> b
$
    -- ASR (2021-02-07). The eta-expansion @\o -> output o@ is
    -- required by GHC >= 9.0.1 (see Issue #4955).
    (\Output
o -> Output -> LaTeX ()
output Output
o) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Output
Text forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlignmentColumn -> Text
ptOpen forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< LaTeX AlignmentColumn
columnZero
  Output -> LaTeX ()
output forall a b. (a -> b) -> a -> b
$ Text -> Output
Text forall a b. (a -> b) -> a -> b
$ Text
ptClose forall a. Semigroup a => a -> a -> a
<> Text
ptNL forall a. Semigroup a => a -> a -> a
<>
                  Int -> Text -> Text
T.replicate (TextWidthEstimator
T.length Text
s forall a. Num a => a -> a -> a
- Int
1) Text
ptEmptyLine
  LaTeX ()
resetColumn
  [Text] -> LaTeX ()
spaces [Text]
ss

-- Spaces followed by a newline character.
spaces (Text
_ : ss :: [Text]
ss@(Text
_ : [Text]
_)) = [Text] -> LaTeX ()
spaces [Text]
ss

-- Spaces that are not followed by a newline character.
spaces [ Text
s ] = do
  Int
col <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> Int
column

  let len :: Int
len  = TextWidthEstimator
T.length Text
s
      kind :: Kind
kind = if Int
col forall a. Eq a => a -> a -> Bool
/= Int
0 Bool -> Bool -> Bool
&& Int
len forall a. Eq a => a -> a -> Bool
== Int
1
             then Kind
Indentation
             else Kind
Alignment

  Int -> LaTeX ()
moveColumn Int
len
  AlignmentColumn
column <- Kind -> LaTeX AlignmentColumn
registerColumn Kind
kind

  if Int
col forall a. Eq a => a -> a -> Bool
/= Int
0
  then Debug -> Text -> LaTeX ()
log Debug
Spaces Text
"col /= 0"
  else do
    [AlignmentColumn]
columns    <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> [AlignmentColumn]
columnsPrev
    Int
codeBlock  <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> Int
codeBlock

    Debug -> Text -> LaTeX ()
log Debug
Spaces forall a b. (a -> b) -> a -> b
$
      Text
"col == 0: " forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
T.pack (forall a. Show a => a -> [Char]
show (Int
len, [AlignmentColumn]
columns))

    case forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Ord a => a -> a -> Bool
<= Int
len) forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlignmentColumn -> Int
columnColumn) [AlignmentColumn]
columns of
      AlignmentColumn
c : [AlignmentColumn]
_ | AlignmentColumn -> Int
columnColumn AlignmentColumn
c forall a. Eq a => a -> a -> Bool
== Int
len, forall a. Maybe a -> Bool
isJust (AlignmentColumn -> Maybe Int
columnKind AlignmentColumn
c) -> do
        -- Align. (This happens automatically if the column is an
        -- alignment column, but c is an indentation column.)
        AlignmentColumn -> LaTeX ()
useColumn AlignmentColumn
c
        Output -> LaTeX ()
output forall a b. (a -> b) -> a -> b
$ Text -> Output
Text forall a b. (a -> b) -> a -> b
$ Text
ptOpenBeginningOfLine
        Output -> LaTeX ()
output forall a b. (a -> b) -> a -> b
$ Text -> Output
Text forall a b. (a -> b) -> a -> b
$ AlignmentColumn -> Text
ptClose' AlignmentColumn
c
      AlignmentColumn
c : [AlignmentColumn]
_ | AlignmentColumn -> Int
columnColumn AlignmentColumn
c forall a. Ord a => a -> a -> Bool
<  Int
len -> do
        -- Indent.
        AlignmentColumn -> LaTeX ()
useColumn AlignmentColumn
c
        Output -> LaTeX ()
output forall a b. (a -> b) -> a -> b
$ Text -> Output
Text forall a b. (a -> b) -> a -> b
$ AlignmentColumn -> Int -> Text
ptOpenIndent AlignmentColumn
c (Int
codeBlock forall a. Num a => a -> a -> a
- AlignmentColumn -> Int
columnCodeBlock AlignmentColumn
c)
      [AlignmentColumn]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

  Output -> LaTeX ()
output forall a b. (a -> b) -> a -> b
$ AlignmentColumn -> Output
MaybeColumn AlignmentColumn
column

-- | Split multi-lines string literals into multiple string literals
-- Isolating leading spaces for the alignment machinery to work
-- properly
stringLiteral :: Token -> Tokens
stringLiteral :: Token -> [Token]
stringLiteral Token
t | Aspects -> Maybe Aspect
aspect (Token -> Aspects
info Token
t) forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Aspect
String =
  forall a b. (a -> b) -> [a] -> [b]
map (\ Text
x -> Token
t { text :: Text
text = Text
x })
          forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Text -> [Text]
leadingSpaces
          forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> [a]
List.intersperse Text
"\n"
          forall a b. (a -> b) -> a -> b
$ Text -> [Text]
T.lines (Token -> Text
text Token
t)
  where
  leadingSpaces :: Text -> [Text]
  leadingSpaces :: Text -> [Text]
leadingSpaces Text
tok = [Text
pre, Text
suf]
    where (Text
pre , Text
suf) = (Char -> Bool) -> Text -> (Text, Text)
T.span Char -> Bool
isSpaceNotNewline Text
tok

stringLiteral Token
t = [Token
t]

-- | Split multi-line comments into several tokens.
-- See issue #5398.
multiLineComment :: Token -> Tokens
multiLineComment :: Token -> [Token]
multiLineComment Token{ text :: Token -> Text
text = Text
s, info :: Token -> Aspects
info = Aspects
i } | Aspects -> Maybe Aspect
aspect Aspects
i forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Aspect
Comment =
  forall a b. (a -> b) -> [a] -> [b]
map (Text -> Aspects -> Token
`Token` Aspects
i)
    forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> [a]
List.intersperse Text
"\n"
    forall a b. (a -> b) -> a -> b
$ Text -> [Text]
T.lines Text
s
-- multiLineComment Token{ text = s, info = i } | aspect i == Just Comment =
--   map emptyToPar
--     $ List1.groupBy ((==) `on` T.null)
--     $ T.lines s
--   where
--   emptyToPar :: List1 Text -> Token
--   emptyToPar ts@(t :| _)
--     | T.null t  = Token{ text = "\n", info = mempty }
--     | otherwise = Token{ text = sconcat $ List1.intersperse "\n" ts, info = i }
multiLineComment Token
t = [Token
t]

------------------------------------------------------------------------
-- * Main.

-- | The Agda data directory containing the files for the LaTeX backend.

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

defaultStyFile :: String
defaultStyFile :: [Char]
defaultStyFile = [Char]
"agda.sty"

data LaTeXOptions = LaTeXOptions
  { LaTeXOptions -> [Char]
latexOptOutDir         :: FilePath
  , LaTeXOptions -> Maybe RangeFile
latexOptSourceFileName :: Maybe RangeFile
    -- ^ The parser uses a @Position@ which includes a source filename for
    -- error reporting and such. We don't actually get the source filename
    -- with an @Interface@, and it isn't necessary to look it up.
    -- This is a "nice-to-have" parameter.
  , LaTeXOptions -> Bool
latexOptCountClusters  :: Bool
    -- ^ Count extended grapheme clusters rather than code points when
    -- generating LaTeX.
  }

getTextWidthEstimator :: Bool -> TextWidthEstimator
getTextWidthEstimator :: Bool -> TextWidthEstimator
getTextWidthEstimator Bool
_countClusters =
#ifdef COUNT_CLUSTERS
  if _countClusters
    then length . (ICU.breaks (ICU.breakCharacter ICU.Root))
    else T.length
#else
  TextWidthEstimator
T.length
#endif

-- | Create the common base output directory and check for/install the style file.
prepareCommonAssets :: (MonadLogLaTeX m, MonadIO m) => FilePath -> m ()
prepareCommonAssets :: forall (m :: * -> *).
(MonadLogLaTeX m, MonadIO m) =>
[Char] -> m ()
prepareCommonAssets [Char]
dir = do
  -- Make sure @dir@ will exist.
  Bool
dirExisted <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ [Char] -> IO Bool
doesDirectoryExist [Char]
dir
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
dirExisted forall a b. (a -> b) -> a -> b
$
    -- Create directory @dir@ and parent directories.
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Bool -> [Char] -> IO ()
createDirectoryIfMissing Bool
True [Char]
dir

  -- Check whether TeX will find @agda.sty@.
  Either IOException [Char]
texFindsSty <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall e a. Exception e => IO a -> IO (Either e a)
try forall a b. (a -> b) -> a -> b
$
      [Char] -> [[Char]] -> [Char] -> IO [Char]
readProcess
        [Char]
"kpsewhich"
        (forall a. Bool -> (a -> a) -> a -> a
applyWhen Bool
dirExisted (([Char]
"--path=" forall a. [a] -> [a] -> [a]
++ [Char]
dir) forall a. a -> [a] -> [a]
:) [[Char]
defaultStyFile])
        [Char]
""
  case Either IOException [Char]
texFindsSty of
    Right [Char]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Left (IOException
e :: IOException) -> do
     -- -- we are lacking MonadDebug here, so no debug printing via reportSLn
     -- reportSLn "compile.latex.sty" 70 $ unlines
     --   [ unwords [ "Searching for", defaultStyFile, "in", dir, "returns:" ]
     --   , show e
     --   ]
     let agdaSty :: [Char]
agdaSty = [Char]
dir [Char] -> ShowS
</> [Char]
defaultStyFile
     forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
dirExisted forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ([Char] -> IO Bool
doesFileExist [Char]
agdaSty)) forall a b. (a -> b) -> a -> b
$ do
       -- It is safe now to create the default style file in @dir@ without overwriting
       -- a possibly user-edited copy there.
       forall (m :: * -> *). MonadLogLaTeX m => LogMessage -> m ()
logLaTeX forall a b. (a -> b) -> a -> b
$ Debug -> Text -> [Text] -> LogMessage
LogMessage Debug
FileSystem
         ([Char] -> Text
T.pack forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords [[Char]
defaultStyFile, [Char]
"was not found. Copying a default version of", [Char]
defaultStyFile, [Char]
"into", [Char]
dir])
         []
       forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ do
         [Char]
styFile <- [Char] -> IO [Char]
getDataFileName forall a b. (a -> b) -> a -> b
$
           [Char]
latexDataDir [Char] -> ShowS
</> [Char]
defaultStyFile
         [Char] -> [Char] -> IO ()
copyFile [Char]
styFile [Char]
agdaSty

-- | Generates a LaTeX file for the given interface.
generateLaTeXIO :: (MonadLogLaTeX m, MonadIO m) => LaTeXOptions -> Interface -> m ()
generateLaTeXIO :: forall (m :: * -> *).
(MonadLogLaTeX m, MonadIO m) =>
LaTeXOptions -> Interface -> m ()
generateLaTeXIO LaTeXOptions
opts Interface
i = do
  let textWidthEstimator :: TextWidthEstimator
textWidthEstimator = Bool -> TextWidthEstimator
getTextWidthEstimator (LaTeXOptions -> Bool
latexOptCountClusters LaTeXOptions
opts)
  let baseDir :: [Char]
baseDir = LaTeXOptions -> [Char]
latexOptOutDir LaTeXOptions
opts
  let outPath :: [Char]
outPath = [Char]
baseDir [Char] -> ShowS
</>
                TopLevelModuleName -> [Char]
latexOutRelativeFilePath (Interface -> TopLevelModuleName
iTopLevelModuleName Interface
i)
  ByteString
latex <- Text -> ByteString
E.encodeUtf8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadLogLaTeX m =>
Env -> Maybe RangeFile -> Text -> HighlightingInfo -> m Text
toLaTeX
              (TextWidthEstimator -> Env
emptyEnv TextWidthEstimator
textWidthEstimator)
              (LaTeXOptions -> Maybe RangeFile
latexOptSourceFileName LaTeXOptions
opts)
              (Interface -> Text
iSource Interface
i)
              (Interface -> HighlightingInfo
iHighlighting Interface
i)
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ do
    Bool -> [Char] -> IO ()
createDirectoryIfMissing Bool
True (ShowS
takeDirectory [Char]
outPath)
    [Char] -> ByteString -> IO ()
BS.writeFile [Char]
outPath ByteString
latex

latexOutRelativeFilePath :: TopLevelModuleName -> FilePath
latexOutRelativeFilePath :: TopLevelModuleName -> [Char]
latexOutRelativeFilePath TopLevelModuleName
m =
  forall a. [a] -> [[a]] -> [a]
List.intercalate [Char
pathSeparator]
    (forall a b. (a -> b) -> [a] -> [b]
map Text -> [Char]
T.unpack forall a b. (a -> b) -> a -> b
$ forall l. IsList l => l -> [Item l]
List1.toList forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> TopLevelModuleNameParts
moduleNameParts TopLevelModuleName
m) [Char] -> ShowS
<.>
  [Char]
"tex"

groupByFst :: forall a b. Eq a => [(a,b)] -> [(a,[b])]
groupByFst :: forall a b. Eq a => [(a, b)] -> [(a, [b])]
groupByFst =
    forall a b. (a -> b) -> [a] -> [b]
map (\[(a, b)]
xs -> case [(a, b)]
xs of                     -- Float the grouping to the top level
          []           -> forall a. HasCallStack => a
__IMPOSSIBLE__
          (a
tag, b
_): [(a, b)]
_ -> (a
tag, forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(a, b)]
xs))

  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Bool) -> [a] -> [[a]]
List.groupBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
fst)  -- Group together characters in the same
                                  -- role.

-- | Transforms the source code into LaTeX.
toLaTeX
  :: MonadLogLaTeX m
  => Env
  -> Maybe RangeFile
  -> L.Text
  -> HighlightingInfo
  -> m L.Text
toLaTeX :: forall (m :: * -> *).
MonadLogLaTeX m =>
Env -> Maybe RangeFile -> Text -> HighlightingInfo -> m Text
toLaTeX Env
env Maybe RangeFile
path Text
source HighlightingInfo
hi =

  forall (m :: * -> *).
MonadLogLaTeX m =>
Env -> [(LayerRole, [Token])] -> m Text
processTokens Env
env

    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map
      ( ( \(LayerRole
role, [Token]
tokens) ->
            (LayerRole
role,) forall a b. (a -> b) -> a -> b
$
              -- This bit fixes issue 954
              ( forall a. Bool -> (a -> a) -> a -> a
applyWhen (LayerRole -> Bool
L.isCode LayerRole
role) forall a b. (a -> b) -> a -> b
$
                  -- Remove trailing whitespace from the
                  -- final line; the function spaces
                  -- expects trailing whitespace to be
                  -- followed by a newline character.
                    forall a. ([a] -> [a]) -> [a] -> [a]
whenMoreThanOne
                      ( forall a. (a -> a) -> [a] -> [a]
updateLast
                          forall a b. (a -> b) -> a -> b
$ (Text -> Text) -> Token -> Token
withTokenText
                          forall a b. (a -> b) -> a -> b
$ \Text
suf ->
                            forall b a. b -> (a -> b) -> Maybe a -> b
maybe
                              Text
suf
                              ((Char -> Bool) -> Text -> Text
T.dropWhileEnd Char -> Bool
isSpaceNotNewline)
                              (Text -> Text -> Maybe Text
T.stripSuffix Text
"\n" Text
suf)
                      )
                      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a) -> [a] -> [a]
updateLast ((Text -> Text) -> Token -> Token
withTokenText forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> Text -> Text
T.dropWhileEnd Char -> Bool
isSpaceNotNewline)
                      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a) -> [a] -> [a]
updateHead
                        ( (Text -> Text) -> Token -> Token
withTokenText forall a b. (a -> b) -> a -> b
$
                            \Text
pre ->
                              forall a. a -> Maybe a -> a
fromMaybe Text
pre forall a b. (a -> b) -> a -> b
$ Text -> Text -> Maybe Text
T.stripPrefix Text
"\n" forall a b. (a -> b) -> a -> b
$
                                (Char -> Bool) -> Text -> Text
T.dropWhile
                                  Char -> Bool
isSpaceNotNewline
                                  Text
pre
                        )
              )
                [Token]
tokens
        ) forall b c a. (b -> c) -> (a -> b) -> a -> c
. ( forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second
                ( -- Split tokens at newlines
                  forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Token -> [Token]
stringLiteral
                forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Token -> [Token]
multiLineComment
                forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map ( \(Maybe Aspects
mi, [Char]
cs) ->
                              Token {text :: Text
text = [Char] -> Text
T.pack [Char]
cs, info :: Aspects
info = forall a. a -> Maybe a -> a
fromMaybe forall a. Monoid a => a
mempty Maybe Aspects
mi}
                      )
                forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Eq a => [(a, b)] -> [(a, [b])]
groupByFst
                )
            )
      )
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Eq a => [(a, b)] -> [(a, [b])]
groupByFst

  -- Look up the meta info at each position in the highlighting info.
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Int
pos (LayerRole
role, Char
char) -> (LayerRole
role, (forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
pos IntMap Aspects
infoMap, Char
char)))
            [Int
1..] forall b c a. (b -> c) -> (a -> b) -> a -> c
. -- Add position in file to each character.
              -- Map each character to its role
              Layers -> [(LayerRole, Char)]
atomizeLayers forall b c a. (b -> c) -> (a -> b) -> a -> c
. Position -> [Char] -> Layers
literateTeX (Maybe RangeFile -> Position
startPos Maybe RangeFile
path)

  forall a b. (a -> b) -> a -> b
$ Text -> [Char]
L.unpack Text
source
  where
  infoMap :: IntMap Aspects
infoMap = forall a m. IsBasicRangeMap a m => m -> IntMap a
toMap HighlightingInfo
hi

  whenMoreThanOne :: ([a] -> [a]) -> [a] -> [a]
  whenMoreThanOne :: forall a. ([a] -> [a]) -> [a] -> [a]
whenMoreThanOne [a] -> [a]
f xs :: [a]
xs@(a
_:a
_:[a]
_) = [a] -> [a]
f [a]
xs
  whenMoreThanOne [a] -> [a]
_ [a]
xs         = [a]
xs


processTokens
  :: MonadLogLaTeX m
  => Env
  -> [(LayerRole, Tokens)]
  -> m L.Text
processTokens :: forall (m :: * -> *).
MonadLogLaTeX m =>
Env -> [(LayerRole, [Token])] -> m Text
processTokens Env
env [(LayerRole, [Token])]
ts = do
  ((), State
s, [Output]
os) <- forall (m :: * -> *) a.
MonadLogLaTeX m =>
LaTeX a -> Env -> State -> m (a, State, [Output])
runLaTeX ([(LayerRole, [Token])] -> LaTeX ()
processLayers [(LayerRole, [Token])]
ts) Env
env State
emptyState
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Text] -> Text
L.fromChunks forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (State -> Output -> Text
render State
s) [Output]
os
  where
    render :: State -> Output -> Text
render State
_ (Text Text
s)        = Text
s
    render State
s (MaybeColumn AlignmentColumn
c)
      | Just Int
i <- AlignmentColumn -> Maybe Int
columnKind AlignmentColumn
c,
        Bool -> Bool
not (Int
i forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`Set.member` State -> HashSet Int
usedColumns State
s) = Text
agdaSpace
      | Bool
otherwise                          = Text
nl forall a. Semigroup a => a -> a -> a
<> AlignmentColumn -> Text
ptOpen AlignmentColumn
c