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

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

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.Utils.FileName (filePath, AbsolutePath, mkAbsolute)

import Agda.Utils.Impossible

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

-- | The @LaTeX@ monad is a combination of @ExceptT@, @RWST@ and
-- @IO@. The error part is just used to keep track whether we finished
-- or not, the reader part isn't 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 I/O part is used for printing debugging info.

type LaTeX = RWST () [Output] State IO

-- | Output items.

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 -> String
(Int -> Output -> ShowS)
-> (Output -> String) -> ([Output] -> ShowS) -> Show Output
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Output] -> ShowS
$cshowList :: [Output] -> ShowS
show :: Output -> String
$cshow :: Output -> String
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
(Kind -> Kind -> Bool) -> (Kind -> Kind -> Bool) -> Eq Kind
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 -> String
(Int -> Kind -> ShowS)
-> (Kind -> String) -> ([Kind] -> ShowS) -> Show Kind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Kind] -> ShowS
$cshowList :: [Kind] -> ShowS
show :: Kind -> String
$cshow :: Kind -> String
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 -> String
(Int -> AlignmentColumn -> ShowS)
-> (AlignmentColumn -> String)
-> ([AlignmentColumn] -> ShowS)
-> Show AlignmentColumn
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AlignmentColumn] -> ShowS
$cshowList :: [AlignmentColumn] -> ShowS
show :: AlignmentColumn -> String
$cshow :: AlignmentColumn -> String
showsPrec :: Int -> AlignmentColumn -> ShowS
$cshowsPrec :: Int -> AlignmentColumn -> ShowS
Show

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.
  , State -> Bool
countClusters :: !Bool  -- ^ Count extended grapheme clusters?
  }

type Tokens = [Token]

data Token = Token
  { Token -> Text
text     :: !Text
  , Token -> Aspects
info     :: Aspects
  }
  deriving Int -> Token -> ShowS
[Token] -> ShowS
Token -> String
(Int -> Token -> ShowS)
-> (Token -> String) -> ([Token] -> ShowS) -> Show Token
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Token] -> ShowS
$cshowList :: [Token] -> ShowS
show :: Token -> String
$cshow :: Token -> String
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
  deriving (Debug -> Debug -> Bool
(Debug -> Debug -> Bool) -> (Debug -> Debug -> Bool) -> Eq Debug
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 -> String
(Int -> Debug -> ShowS)
-> (Debug -> String) -> ([Debug] -> ShowS) -> Show Debug
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Debug] -> ShowS
$cshowList :: [Debug] -> ShowS
show :: Debug -> String
$cshow :: Debug -> String
showsPrec :: Int -> Debug -> ShowS
$cshowsPrec :: Int -> Debug -> ShowS
Show)

-- | Says what debug information should printed.

debugs :: [Debug]
debugs :: [Debug]
debugs = []

-- | Run function for the @LaTeX@ monad.
runLaTeX ::
  LaTeX a -> () -> State -> IO (a, State, [Output])
runLaTeX :: LaTeX a -> () -> State -> IO (a, State, [Output])
runLaTeX = LaTeX a -> () -> State -> IO (a, State, [Output])
forall r w s (m :: * -> *) a.
RWST r w s m a -> r -> s -> m (a, s, w)
runRWST

emptyState
  :: Bool  -- ^ Count extended grapheme clusters?
  -> State
emptyState :: Bool -> State
emptyState Bool
cc = State :: Int
-> Int
-> [AlignmentColumn]
-> [AlignmentColumn]
-> Int
-> HashSet Int
-> Bool
-> State
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   = HashSet Int
forall a. HashSet a
Set.empty
  , countClusters :: Bool
countClusters = Bool
cc
  }

------------------------------------------------------------------------
-- * 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 = do
  Bool
cc <- State -> Bool
countClusters (State -> Bool)
-> RWST () [Output] State IO State
-> RWST () [Output] State IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RWST () [Output] State IO State
forall s (m :: * -> *). MonadState s m => m s
get
  if Bool
cc then
#ifdef COUNT_CLUSTERS
    return $ length $ ICU.breaks (ICU.breakCharacter ICU.Root) t
#else
    LaTeX Int
forall a. HasCallStack => a
__IMPOSSIBLE__
#endif
   else
    Int -> LaTeX Int
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> LaTeX Int) -> Int -> LaTeX Int
forall a b. (a -> b) -> a -> b
$ Text -> Int
T.length Text
t

(<+>) :: Text -> Text -> Text
<+> :: Text -> Text -> Text
(<+>) = Text -> Text -> Text
T.append

-- | 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 Char -> Char -> Bool
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
t = do
  Bool -> LaTeX () -> LaTeX ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Text -> Bool
isSpaces (Token -> Text
text Token
t)) (LaTeX () -> LaTeX ()) -> LaTeX () -> LaTeX ()
forall a b. (a -> b) -> a -> b
$ do
    Debug -> Text -> LaTeX ()
log Debug
MoveColumn (Text -> LaTeX ()) -> Text -> LaTeX ()
forall a b. (a -> b) -> a -> b
$ Token -> Text
text Token
t
    Int -> LaTeX ()
moveColumn (Int -> LaTeX ()) -> LaTeX Int -> LaTeX ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Text -> LaTeX Int
size (Token -> Text
text Token
t)

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

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

moveColumn :: Int -> LaTeX ()
moveColumn :: Int -> LaTeX ()
moveColumn Int
i = (State -> State) -> LaTeX ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((State -> State) -> LaTeX ()) -> (State -> State) -> LaTeX ()
forall a b. (a -> b) -> a -> b
$ \State
s -> State
s { column :: Int
column = Int
i Int -> Int -> Int
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    <- (State -> Int) -> LaTeX Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> Int
column
  Int
codeBlock <- (State -> Int) -> LaTeX Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> Int
codeBlock
  Maybe Int
kind      <- case Kind
kind of
                 Kind
Alignment   -> Maybe Int -> RWST () [Output] State IO (Maybe Int)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Int
forall a. Maybe a
Nothing
                 Kind
Indentation -> do
                   Int
nextId <- (State -> Int) -> LaTeX Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> Int
nextId
                   (State -> State) -> LaTeX ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((State -> State) -> LaTeX ()) -> (State -> State) -> LaTeX ()
forall a b. (a -> b) -> a -> b
$ \State
s -> State
s { nextId :: Int
nextId = Int -> Int
forall a. Enum a => a -> a
succ Int
nextId }
                   Maybe Int -> RWST () [Output] State IO (Maybe Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
nextId)
  let c :: AlignmentColumn
c = AlignmentColumn :: Int -> Int -> Maybe Int -> AlignmentColumn
AlignmentColumn { columnColumn :: Int
columnColumn    = Int
column
                          , columnCodeBlock :: Int
columnCodeBlock = Int
codeBlock
                          , columnKind :: Maybe Int
columnKind      = Maybe Int
kind
                          }
  (State -> State) -> LaTeX ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((State -> State) -> LaTeX ()) -> (State -> State) -> LaTeX ()
forall a b. (a -> b) -> a -> b
$ \State
s -> State
s { columns :: [AlignmentColumn]
columns = AlignmentColumn
c AlignmentColumn -> [AlignmentColumn] -> [AlignmentColumn]
forall a. a -> [a] -> [a]
: State -> [AlignmentColumn]
columns State
s }
  AlignmentColumn -> LaTeX AlignmentColumn
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 = case AlignmentColumn -> Maybe Int
columnKind AlignmentColumn
c of
  Maybe Int
Nothing -> () -> LaTeX ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  Just Int
i  -> (State -> State) -> LaTeX ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((State -> State) -> LaTeX ()) -> (State -> State) -> LaTeX ()
forall a b. (a -> b) -> a -> b
$ \State
s ->
               State
s { usedColumns :: HashSet Int
usedColumns = Int -> HashSet Int -> HashSet Int
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 <- (State -> Int) -> LaTeX Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> Int
codeBlock
  AlignmentColumn -> LaTeX AlignmentColumn
forall (m :: * -> *) a. Monad m => a -> m a
return (AlignmentColumn -> LaTeX AlignmentColumn)
-> AlignmentColumn -> LaTeX AlignmentColumn
forall a b. (a -> b) -> a -> b
$ AlignmentColumn :: Int -> Int -> Maybe Int -> AlignmentColumn
AlignmentColumn { columnColumn :: Int
columnColumn    = Int
0
                           , columnCodeBlock :: Int
columnCodeBlock = Int
codeBlock
                           , columnKind :: Maybe Int
columnKind      = Maybe Int
forall a. Maybe a
Nothing
                           }

-- | Registers column zero as an alignment column.

registerColumnZero :: LaTeX ()
registerColumnZero :: LaTeX ()
registerColumnZero = do
  AlignmentColumn
c <- LaTeX AlignmentColumn
columnZero
  (State -> State) -> LaTeX ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((State -> State) -> LaTeX ()) -> (State -> State) -> LaTeX ()
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
  (State -> State) -> LaTeX ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((State -> State) -> LaTeX ()) -> (State -> State) -> LaTeX ()
forall a b. (a -> b) -> a -> b
$ \State
s -> State
s { codeBlock :: Int
codeBlock = State -> Int
codeBlock State
s Int -> Int -> Int
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 = () -> LaTeX ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

logHelper :: Debug -> Text -> [String] -> LaTeX ()
logHelper :: Debug -> Text -> [String] -> LaTeX ()
logHelper Debug
debug Text
text [String]
extra =
  Bool -> LaTeX () -> LaTeX ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Debug
debug Debug -> [Debug] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Debug]
debugs) (LaTeX () -> LaTeX ()) -> LaTeX () -> LaTeX ()
forall a b. (a -> b) -> a -> b
$ do
    IO () -> LaTeX ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> LaTeX ()) -> IO () -> LaTeX ()
forall a b. (a -> b) -> a -> b
$ Text -> IO ()
T.putStrLn (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack (Debug -> String
forall a. Show a => a -> String
show Debug
debug String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": ") Text -> Text -> Text
<+>
      Text
"'" Text -> Text -> Text
<+> Text
text Text -> Text -> Text
<+> Text
"' " Text -> Text -> Text
<+>
      if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
extra
         then Text
T.empty
         else Text
"(" Text -> Text -> Text
<+> String -> Text
T.pack ([String] -> String
unwords [String]
extra) Text -> Text -> Text
<+> Text
")"

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

log' :: Debug -> String -> LaTeX ()
log' :: Debug -> String -> LaTeX ()
log' Debug
d = Debug -> Text -> LaTeX ()
log Debug
d (Text -> LaTeX ()) -> (String -> Text) -> String -> LaTeX ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack

output :: Output -> LaTeX ()
output :: Output -> LaTeX ()
output Output
item = do
  Debug -> String -> LaTeX ()
log' Debug
Output (Output -> String
forall a. Show a => a -> String
show Output
item)
  [Output] -> LaTeX ()
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 Text -> Text -> Text
<+> Text
"Space" Text -> Text -> Text
<+> Text -> Text
cmdArg Text
T.empty Text -> Text -> Text
<+> 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 = String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ case AlignmentColumn -> Maybe Int
columnKind AlignmentColumn
c of
  Maybe Int
Nothing -> Int -> String
forall a. Show a => a -> String
show (AlignmentColumn -> Int
columnColumn AlignmentColumn
c)
  Just Int
i  -> Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"I"

-- | Opens a column with the given name.

ptOpen' :: Text -> Text
ptOpen' :: Text -> Text
ptOpen' Text
name = Text
"\\>[" Text -> Text -> Text
<+> Text
name Text -> Text -> Text
<+> 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
"." Text -> Text -> Text
<+> 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 Text -> Text -> Text
<+> Text
"[@{}l@{"
           Text -> Text -> Text
<+> Text
cmdPrefix
           Text -> Text -> Text
<+> Text
"Indent"
           Text -> Text -> Text
<+> Text -> Text
cmdArg (String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
delta)
           Text -> Text -> Text
<+> Text
"}]"

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

ptClose' :: AlignmentColumn -> Text
ptClose' :: AlignmentColumn -> Text
ptClose' AlignmentColumn
c =
  Text
ptClose Text -> Text -> Text
<+> Text
"[" Text -> Text -> Text
<+> AlignmentColumn -> Text
columnName AlignmentColumn
c Text -> Text -> Text
<+> Text
"]"

ptNL :: Text
ptNL :: Text
ptNL = Text
nl Text -> Text -> Text
<+> Text
"\\\\\n"

ptEmptyLine :: Text
ptEmptyLine :: Text
ptEmptyLine =
  Text
nl Text -> Text -> Text
<+> Text
"\\\\["
     Text -> Text -> Text
<+> Text
cmdPrefix
     Text -> Text -> Text
<+> Text
"EmptyExtraSkip"
     Text -> Text -> Text
<+> Text
"]%\n"

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

cmdArg :: Text -> Text
cmdArg :: Text -> Text
cmdArg Text
x = Text
"{" Text -> Text -> Text
<+> Text
x Text -> Text -> Text
<+> Text
"}"

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

processLayers :: [(LayerRole, Tokens)] -> LaTeX ()
processLayers :: [(LayerRole, [Token])] -> LaTeX ()
processLayers = ((LayerRole, [Token]) -> LaTeX ())
-> [(LayerRole, [Token])] -> LaTeX ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (((LayerRole, [Token]) -> LaTeX ())
 -> [(LayerRole, [Token])] -> LaTeX ())
-> ((LayerRole, [Token]) -> LaTeX ())
-> [(LayerRole, [Token])]
-> LaTeX ()
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

processMarkup, processComment, processCode :: Tokens -> LaTeX ()

-- | Deals with markup, which is output verbatim.
processMarkup :: [Token] -> LaTeX ()
processMarkup = (Token -> LaTeX ()) -> [Token] -> LaTeX ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Token -> LaTeX ()) -> [Token] -> LaTeX ())
-> (Token -> LaTeX ()) -> [Token] -> LaTeX ()
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 :: [Token] -> LaTeX ()
processComment = (Token -> LaTeX ()) -> [Token] -> LaTeX ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Token -> LaTeX ()) -> [Token] -> LaTeX ())
-> (Token -> LaTeX ()) -> [Token] -> LaTeX ()
forall a b. (a -> b) -> a -> b
$ \Token
t -> do
  Bool -> LaTeX () -> LaTeX ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Text
"%" Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Text -> Text
T.take Int
1 (Text -> Text
T.stripStart (Token -> Text
text Token
t))) (LaTeX () -> LaTeX ()) -> LaTeX () -> LaTeX ()
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 :: [Token] -> LaTeX ()
processCode [Token]
toks' = do
  Output -> LaTeX ()
output (Output -> LaTeX ()) -> Output -> LaTeX ()
forall a b. (a -> b) -> a -> b
$ Text -> Output
Text Text
nl
  LaTeX ()
enterCode
  (Token -> LaTeX ()) -> [Token] -> LaTeX ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Token -> LaTeX ()
go [Token]
toks'
  Int -> LaTeX ()
forall a. (Eq a, Num a) => a -> LaTeX ()
ptOpenWhenColumnZero (Int -> LaTeX ()) -> LaTeX Int -> LaTeX ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (State -> Int) -> LaTeX Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> Int
column
  Output -> LaTeX ()
output (Output -> LaTeX ()) -> Output -> LaTeX ()
forall a b. (a -> b) -> a -> b
$ Text -> Output
Text (Text -> Output) -> Text -> Output
forall a b. (a -> b) -> a -> b
$ Text
ptClose Text -> Text -> Text
<+> Text
nl
  LaTeX ()
leaveCode

  where
    go :: Token -> LaTeX ()
go Token
tok' = do
      -- Get the column information before grabbing the token, since
      -- grabbing (possibly) moves the column.
      Int
col  <- (State -> Int) -> LaTeX Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> Int
column

      Token -> LaTeX ()
moveColumnForToken Token
tok'
      let tok :: Text
tok = Token -> Text
text Token
tok'
      Debug -> Text -> LaTeX ()
log Debug
Code Text
tok

      if (Text
tok Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
T.empty) then () -> LaTeX ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      else do
        if (Text -> Bool
isSpaces Text
tok) then do
            [Text] -> LaTeX ()
spaces ([Text] -> LaTeX ()) -> [Text] -> LaTeX ()
forall a b. (a -> b) -> a -> b
$ Text -> [Text]
T.group (Text -> [Text]) -> Text -> [Text]
forall a b. (a -> b) -> a -> b
$ Text -> Text
replaceSpaces Text
tok
        else do
          Int -> LaTeX ()
forall a. (Eq a, Num a) => a -> LaTeX ()
ptOpenWhenColumnZero Int
col
          Output -> LaTeX ()
output (Output -> LaTeX ()) -> Output -> LaTeX ()
forall a b. (a -> b) -> a -> b
$ Text -> Output
Text (Text -> Output) -> Text -> Output
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)
            (String -> Text -> Text) -> Text -> [String] -> Text
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\String
c Text
t -> Text
cmdPrefix Text -> Text -> Text
<+> String -> Text
T.pack String
c Text -> Text -> Text
<+> Text -> Text
cmdArg Text
t)
                  (Text -> Text
escape Text
tok)
                  ([String] -> Text) -> [String] -> Text
forall a b. (a -> b) -> a -> b
$ (OtherAspect -> String) -> [OtherAspect] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map OtherAspect -> String
fromOtherAspect (Set OtherAspect -> [OtherAspect]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Set OtherAspect -> [OtherAspect])
-> Set OtherAspect -> [OtherAspect]
forall a b. (a -> b) -> a -> b
$ Aspects -> Set OtherAspect
otherAspects (Aspects -> Set OtherAspect) -> Aspects -> Set OtherAspect
forall a b. (a -> b) -> a -> b
$ Token -> Aspects
info Token
tok') [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                    (Aspect -> [String]) -> [Aspect] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Aspect -> [String]
fromAspect (Maybe Aspect -> [Aspect]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Maybe Aspect -> [Aspect]) -> Maybe Aspect -> [Aspect]
forall a b. (a -> b) -> a -> b
$ Aspects -> Maybe Aspect
aspect (Aspects -> Maybe Aspect) -> Aspects -> Maybe 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 -> LaTeX ()
ptOpenWhenColumnZero a
col =
        Bool -> LaTeX () -> LaTeX ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (a
col a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0) (LaTeX () -> LaTeX ()) -> LaTeX () -> LaTeX ()
forall a b. (a -> b) -> a -> b
$ do
          LaTeX ()
registerColumnZero
          Output -> LaTeX ()
output (Output -> LaTeX ())
-> (AlignmentColumn -> Output) -> AlignmentColumn -> LaTeX ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Output
Text (Text -> Output)
-> (AlignmentColumn -> Text) -> AlignmentColumn -> Output
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlignmentColumn -> Text
ptOpen (AlignmentColumn -> LaTeX ()) -> LaTeX AlignmentColumn -> LaTeX ()
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 -> String
fromOtherAspect = OtherAspect -> String
forall a. Show a => a -> String
show

    fromAspect :: Aspect -> [String]
    fromAspect :: Aspect -> [String]
fromAspect Aspect
a = let s :: [String]
s = [Aspect -> String
forall a. Show a => a -> String
show Aspect
a] in case Aspect
a of
      Aspect
Comment           -> [String]
s
      Aspect
Keyword           -> [String]
s
      Aspect
String            -> [String]
s
      Aspect
Number            -> [String]
s
      Aspect
Symbol            -> [String]
s
      Aspect
PrimitiveType     -> [String]
s
      Aspect
Pragma            -> [String]
s
      Aspect
Background        -> [String]
s
      Aspect
Markup            -> [String]
s
      Name Maybe NameKind
Nothing Bool
isOp -> Aspect -> [String]
fromAspect (Maybe NameKind -> Bool -> Aspect
Name (NameKind -> Maybe NameKind
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 ->
        (\String
c -> if Bool
isOp then [String
"Operator", String
c] else [String
c]) (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$
        case NameKind
kind of
          NameKind
Bound                     -> String
s
          NameKind
Generalizable             -> String
s
          Constructor Induction
Inductive     -> String
"InductiveConstructor"
          Constructor Induction
CoInductive   -> String
"CoinductiveConstructor"
          NameKind
Datatype                  -> String
s
          NameKind
Field                     -> String
s
          NameKind
Function                  -> String
s
          NameKind
Module                    -> String
s
          NameKind
Postulate                 -> String
s
          NameKind
Primitive                 -> String
s
          NameKind
Record                    -> String
s
          NameKind
Argument                  -> String
s
          NameKind
Macro                     -> String
s
        where
        s :: String
s = NameKind -> String
forall a. Show a => a -> String
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)) = String -> Text
T.pack (Char -> String
replace Char
c) Text -> Text -> Text
<+> Text -> Text
escape Text
s
  where
  replace :: Char -> String
  replace :: Char -> String
replace Char
c = case Char
c of
    Char
'_'  -> String
"\\AgdaUnderscore{}"
    Char
'{'  -> String
"\\{"
    Char
'}'  -> String
"\\}"
    Char
'#'  -> String
"\\#"
    Char
'$'  -> String
"\\$"
    Char
'&'  -> String
"\\&"
    Char
'%'  -> String
"\\%"
    Char
'~'  -> String
"\\textasciitilde{}"
    Char
'^'  -> String
"\\textasciicircum{}"
    Char
'\\' -> String
"\\textbackslash{}"
    Char
_    -> [ Char
c ]
#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 [] = () -> LaTeX ()
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 <- (State -> Int) -> LaTeX Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> Int
column
  Bool -> LaTeX () -> LaTeX ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
col Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0) (LaTeX () -> LaTeX ()) -> LaTeX () -> LaTeX ()
forall a b. (a -> b) -> a -> b
$
    Output -> LaTeX ()
output (Output -> LaTeX ())
-> (AlignmentColumn -> Output) -> AlignmentColumn -> LaTeX ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Output
Text (Text -> Output)
-> (AlignmentColumn -> Text) -> AlignmentColumn -> Output
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlignmentColumn -> Text
ptOpen (AlignmentColumn -> LaTeX ()) -> LaTeX AlignmentColumn -> LaTeX ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< LaTeX AlignmentColumn
columnZero
  Output -> LaTeX ()
output (Output -> LaTeX ()) -> Output -> LaTeX ()
forall a b. (a -> b) -> a -> b
$ Text -> Output
Text (Text -> Output) -> Text -> Output
forall a b. (a -> b) -> a -> b
$ Text
ptClose Text -> Text -> Text
<+> Text
ptNL Text -> Text -> Text
<+>
                  Int -> Text -> Text
T.replicate (Text -> Int
T.length Text
s Int -> Int -> Int
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 <- (State -> Int) -> LaTeX Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> Int
column

  let len :: Int
len  = Text -> Int
T.length Text
s
      kind :: Kind
kind = if Int
col Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0 Bool -> Bool -> Bool
&& Int
len Int -> Int -> Bool
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0
  then Debug -> String -> LaTeX ()
log' Debug
Spaces String
"col /= 0"
  else do
    [AlignmentColumn]
columns    <- (State -> [AlignmentColumn])
-> RWST () [Output] State IO [AlignmentColumn]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> [AlignmentColumn]
columnsPrev
    Int
codeBlock  <- (State -> Int) -> LaTeX Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets State -> Int
codeBlock

    Debug -> String -> LaTeX ()
log' Debug
Spaces (String -> LaTeX ()) -> String -> LaTeX ()
forall a b. (a -> b) -> a -> b
$
      String
"col == 0: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int, [AlignmentColumn]) -> String
forall a. Show a => a -> String
show (Int
len, [AlignmentColumn]
columns)

    case (AlignmentColumn -> Bool) -> [AlignmentColumn] -> [AlignmentColumn]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
len) (Int -> Bool)
-> (AlignmentColumn -> Int) -> AlignmentColumn -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlignmentColumn -> Int
columnColumn) [AlignmentColumn]
columns of
      AlignmentColumn
c : [AlignmentColumn]
_ | AlignmentColumn -> Int
columnColumn AlignmentColumn
c Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
len, Maybe Int -> Bool
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 (Output -> LaTeX ()) -> Output -> LaTeX ()
forall a b. (a -> b) -> a -> b
$ Text -> Output
Text (Text -> Output) -> Text -> Output
forall a b. (a -> b) -> a -> b
$ Text
ptOpenBeginningOfLine
        Output -> LaTeX ()
output (Output -> LaTeX ()) -> Output -> LaTeX ()
forall a b. (a -> b) -> a -> b
$ Text -> Output
Text (Text -> Output) -> Text -> Output
forall a b. (a -> b) -> a -> b
$ AlignmentColumn -> Text
ptClose' AlignmentColumn
c
      AlignmentColumn
c : [AlignmentColumn]
_ | AlignmentColumn -> Int
columnColumn AlignmentColumn
c Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<  Int
len -> do
        -- Indent.
        AlignmentColumn -> LaTeX ()
useColumn AlignmentColumn
c
        Output -> LaTeX ()
output (Output -> LaTeX ()) -> Output -> LaTeX ()
forall a b. (a -> b) -> a -> b
$ Text -> Output
Text (Text -> Output) -> Text -> Output
forall a b. (a -> b) -> a -> b
$ AlignmentColumn -> Int -> Text
ptOpenIndent AlignmentColumn
c (Int
codeBlock Int -> Int -> Int
forall a. Num a => a -> a -> a
- AlignmentColumn -> Int
columnCodeBlock AlignmentColumn
c)
      [AlignmentColumn]
_ -> () -> LaTeX ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  Output -> LaTeX ()
output (Output -> LaTeX ()) -> Output -> LaTeX ()
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) Maybe Aspect -> Maybe Aspect -> Bool
forall a. Eq a => a -> a -> Bool
== Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just Aspect
String =
  (Text -> Token) -> [Text] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map (\ Text
x -> Token
t { text :: Text
text = Text
x })
          ([Text] -> [Token]) -> [Text] -> [Token]
forall a b. (a -> b) -> a -> b
$ (Text -> [Text]) -> [Text] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Text -> [Text]
leadingSpaces
          ([Text] -> [Text]) -> [Text] -> [Text]
forall a b. (a -> b) -> a -> b
$ Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
List.intersperse Text
"\n"
          ([Text] -> [Text]) -> [Text] -> [Text]
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
t = [Text
pre, Text
suf]
    where (Text
pre , Text
suf) = (Char -> Bool) -> Text -> (Text, Text)
T.span Char -> Bool
isSpaceNotNewline Text
t

stringLiteral Token
t = [Token
t]

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

defaultStyFile :: String
defaultStyFile :: String
defaultStyFile = String
"agda.sty"

-- | Generates a LaTeX file for the given interface.
--
-- The underlying source file is assumed to match the interface, but
-- this is not checked. TODO: Fix this problem, perhaps by storing the
-- source code in the interface.
generateLaTeX :: Interface -> TCM ()
generateLaTeX :: Interface -> TCM ()
generateLaTeX Interface
i = do
  let mod :: TopLevelModuleName
mod = ModuleName -> TopLevelModuleName
toTopLevelModuleName (ModuleName -> TopLevelModuleName)
-> ModuleName -> TopLevelModuleName
forall a b. (a -> b) -> a -> b
$ Interface -> ModuleName
iModuleName Interface
i
      hi :: HighlightingInfo
hi  = Interface -> HighlightingInfo
iHighlighting Interface
i

  CommandLineOptions
options <- TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
TCM.commandLineOptions

  String
dir <- case CommandLineOptions -> Bool
O.optGHCiInteraction CommandLineOptions
options of
    Bool
False -> String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> TCMT IO String) -> String -> TCMT IO String
forall a b. (a -> b) -> a -> b
$ CommandLineOptions -> String
O.optLaTeXDir CommandLineOptions
options
    Bool
True  -> do
      AbsolutePath
sourceFile <- SourceFile -> AbsolutePath
Find.srcFilePath (SourceFile -> AbsolutePath)
-> TCMT IO SourceFile -> TCMT IO AbsolutePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TopLevelModuleName -> TCMT IO SourceFile
Find.findFile TopLevelModuleName
mod
      String -> TCMT IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> TCMT IO String) -> String -> TCMT IO String
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> String
filePath (AbsolutePath -> TopLevelModuleName -> AbsolutePath
projectRoot AbsolutePath
sourceFile TopLevelModuleName
mod)
                 String -> ShowS
</> CommandLineOptions -> String
O.optLaTeXDir CommandLineOptions
options
  IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Bool -> String -> IO ()
createDirectoryIfMissing Bool
True String
dir

  (ExitCode
code, String
_, String
_) <- IO (ExitCode, String, String) -> TCMT IO (ExitCode, String, String)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ExitCode, String, String)
 -> TCMT IO (ExitCode, String, String))
-> IO (ExitCode, String, String)
-> TCMT IO (ExitCode, String, String)
forall a b. (a -> b) -> a -> b
$ String -> [String] -> String -> IO (ExitCode, String, String)
readProcessWithExitCode
                    String
"kpsewhich" [ String
"--path=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
dir,  String
defaultStyFile ] String
""

  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ExitCode
code ExitCode -> ExitCode -> Bool
forall a. Eq a => a -> a -> Bool
/= ExitCode
ExitSuccess) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    String -> Int -> [String] -> TCM ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Int -> a -> m ()
TCM.reportS String
"compile.latex" Int
1
      [ String
defaultStyFile String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" was not found. Copying a default version of " String -> ShowS
forall a. [a] -> [a] -> [a]
++
          String
defaultStyFile
      , String
"into " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
dir String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
      ]

    IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      String
styFile <- String -> IO String
getDataFileName String
defaultStyFile
      IO () -> IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> IO ()
copyFile String
styFile (String
dir String -> ShowS
</> String
defaultStyFile)

  let outPath :: String
outPath = TopLevelModuleName -> String
modToFile TopLevelModuleName
mod
  String
inAbsPath <- (AbsolutePath -> String) -> TCMT IO AbsolutePath -> TCMT IO String
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM AbsolutePath -> String
filePath (SourceFile -> AbsolutePath
Find.srcFilePath (SourceFile -> AbsolutePath)
-> TCMT IO SourceFile -> TCMT IO AbsolutePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TopLevelModuleName -> TCMT IO SourceFile
Find.findFile TopLevelModuleName
mod)

  IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    ByteString
latex <- Text -> ByteString
E.encodeUtf8 (Text -> ByteString) -> IO Text -> IO ByteString
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap`
               Bool -> AbsolutePath -> Text -> HighlightingInfo -> IO Text
toLaTeX (PragmaOptions -> Bool
O.optCountClusters (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall a b. (a -> b) -> a -> b
$ CommandLineOptions -> PragmaOptions
O.optPragmaOptions CommandLineOptions
options)
                       (String -> AbsolutePath
mkAbsolute String
inAbsPath) (Interface -> Text
iSource Interface
i) HighlightingInfo
hi
    Bool -> String -> IO ()
createDirectoryIfMissing Bool
True (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
dir String -> ShowS
</> ShowS
takeDirectory String
outPath
    String -> ByteString -> IO ()
BS.writeFile (String
dir String -> ShowS
</> String
outPath) ByteString
latex

  where
    modToFile :: TopLevelModuleName -> FilePath
    modToFile :: TopLevelModuleName -> String
modToFile TopLevelModuleName
m = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate [Char
pathSeparator] (TopLevelModuleName -> [String]
moduleNameParts TopLevelModuleName
m) String -> ShowS
<.> String
"tex"

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

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

-- | Transforms the source code into LaTeX.
toLaTeX
  :: Bool
     -- ^ Count extended grapheme clusters?
  -> AbsolutePath
  -> L.Text
  -> HighlightingInfo
  -> IO L.Text
toLaTeX :: Bool -> AbsolutePath -> Text -> HighlightingInfo -> IO Text
toLaTeX Bool
cc AbsolutePath
path Text
source HighlightingInfo
hi

  = Bool -> [(LayerRole, [Token])] -> IO Text
processTokens Bool
cc

  ([(LayerRole, [Token])] -> IO Text)
-> (String -> [(LayerRole, [Token])]) -> String -> IO Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((LayerRole, [Token]) -> (LayerRole, [Token]))
-> [(LayerRole, [Token])] -> [(LayerRole, [Token])]
forall a b. (a -> b) -> [a] -> [b]
map (\(LayerRole
role, [Token]
tokens) -> (LayerRole
role,) ([Token] -> (LayerRole, [Token]))
-> [Token] -> (LayerRole, [Token])
forall a b. (a -> b) -> a -> b
$
      -- This bit fixes issue 954
      (if LayerRole -> Bool
L.isCode LayerRole
role then
        -- Remove trailing whitespace from the
        -- final line; the function spaces
        -- expects trailing whitespace to be
        -- followed by a newline character.
        ([Token] -> [Token]) -> [Token] -> [Token]
forall a. ([a] -> [a]) -> [a] -> [a]
whenMoreThanOne
          ((Token -> Token) -> [Token] -> [Token]
forall a. (a -> a) -> [a] -> [a]
withLast ((Token -> Token) -> [Token] -> [Token])
-> (Token -> Token) -> [Token] -> [Token]
forall a b. (a -> b) -> a -> b
$
            (Text -> Text) -> Token -> Token
withTokenText ((Text -> Text) -> Token -> Token)
-> (Text -> Text) -> Token -> Token
forall a b. (a -> b) -> a -> b
$ \Text
suf ->
              Text -> Maybe Text -> Text
forall a. a -> Maybe a -> a
fromMaybe Text
suf (Maybe Text -> Text) -> Maybe Text -> Text
forall a b. (a -> b) -> a -> b
$
                (Text -> Text) -> Maybe Text -> Maybe Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Char -> Bool) -> Text -> Text
T.dropWhileEnd Char -> Bool
isSpaceNotNewline) (Maybe Text -> Maybe Text) -> Maybe Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$
                  Text -> Text -> Maybe Text
T.stripSuffix Text
"\n" Text
suf)
        ([Token] -> [Token]) -> ([Token] -> [Token]) -> [Token] -> [Token]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        ((Token -> Token) -> [Token] -> [Token]
forall a. (a -> a) -> [a] -> [a]
withLast ((Token -> Token) -> [Token] -> [Token])
-> (Token -> Token) -> [Token] -> [Token]
forall a b. (a -> b) -> a -> b
$ (Text -> Text) -> Token -> Token
withTokenText ((Text -> Text) -> Token -> Token)
-> (Text -> Text) -> Token -> Token
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> Text -> Text
T.dropWhileEnd Char -> Bool
isSpaceNotNewline)
        ([Token] -> [Token]) -> ([Token] -> [Token]) -> [Token] -> [Token]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        ((Token -> Token) -> [Token] -> [Token]
forall a. (a -> a) -> [a] -> [a]
withFirst ((Token -> Token) -> [Token] -> [Token])
-> (Token -> Token) -> [Token] -> [Token]
forall a b. (a -> b) -> a -> b
$
          (Text -> Text) -> Token -> Token
withTokenText ((Text -> Text) -> Token -> Token)
-> (Text -> Text) -> Token -> Token
forall a b. (a -> b) -> a -> b
$ \Text
pre ->
              Text -> Maybe Text -> Text
forall a. a -> Maybe a -> a
fromMaybe Text
pre (Maybe Text -> Text) -> Maybe Text -> Text
forall a b. (a -> b) -> a -> b
$
                  Text -> Text -> Maybe Text
T.stripPrefix Text
"\n" (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$
                    (Char -> Bool) -> Text -> Text
T.dropWhile Char -> Bool
isSpaceNotNewline Text
pre)
      else
        -- do nothing
        [Token] -> [Token]
forall a. a -> a
id) [Token]
tokens)

  ([(LayerRole, [Token])] -> [(LayerRole, [Token])])
-> (String -> [(LayerRole, [Token])])
-> String
-> [(LayerRole, [Token])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((LayerRole, [(Maybe Aspects, Char)]) -> (LayerRole, [Token]))
-> [(LayerRole, [(Maybe Aspects, Char)])] -> [(LayerRole, [Token])]
forall a b. (a -> b) -> [a] -> [b]
map (([(Maybe Aspects, Char)] -> [Token])
-> (LayerRole, [(Maybe Aspects, Char)]) -> (LayerRole, [Token])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (
      -- Split tokens at newlines
      (Token -> [Token]) -> [Token] -> [Token]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Token -> [Token]
stringLiteral

      -- Head the list (the grouped chars contain the same meta info) and
      -- collect the characters into a string.
    ([Token] -> [Token])
-> ([(Maybe Aspects, Char)] -> [Token])
-> [(Maybe Aspects, Char)]
-> [Token]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Maybe Aspects, String) -> Token)
-> [(Maybe Aspects, String)] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map (\(Maybe Aspects
mi, String
cs) ->
                          Token :: Text -> Aspects -> Token
Token { text :: Text
text = String -> Text
T.pack String
cs
                                , info :: Aspects
info = Aspects -> Maybe Aspects -> Aspects
forall a. a -> Maybe a -> a
fromMaybe Aspects
forall a. Monoid a => a
mempty Maybe Aspects
mi
                                })
      -- Characters which share the same meta info are the same token, so
      -- group them together.
    ([(Maybe Aspects, String)] -> [Token])
-> ([(Maybe Aspects, Char)] -> [(Maybe Aspects, String)])
-> [(Maybe Aspects, Char)]
-> [Token]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Maybe Aspects, Char)] -> [(Maybe Aspects, String)]
forall a b. Eq a => [(a, b)] -> [(a, [b])]
groupByFst
    ))

  -- Characters in different layers belong to different tokens
  ([(LayerRole, [(Maybe Aspects, Char)])] -> [(LayerRole, [Token])])
-> (String -> [(LayerRole, [(Maybe Aspects, Char)])])
-> String
-> [(LayerRole, [Token])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(LayerRole, (Maybe Aspects, Char))]
-> [(LayerRole, [(Maybe Aspects, Char)])]
forall a b. Eq a => [(a, b)] -> [(a, [b])]
groupByFst

  -- Look up the meta info at each position in the highlighting info.
  ([(LayerRole, (Maybe Aspects, Char))]
 -> [(LayerRole, [(Maybe Aspects, Char)])])
-> (String -> [(LayerRole, (Maybe Aspects, Char))])
-> String
-> [(LayerRole, [(Maybe Aspects, Char)])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, (LayerRole, Char)) -> (LayerRole, (Maybe Aspects, Char)))
-> [(Int, (LayerRole, Char))]
-> [(LayerRole, (Maybe Aspects, Char))]
forall a b. (a -> b) -> [a] -> [b]
map (\(Int
pos, (LayerRole
role, Char
char)) -> (LayerRole
role, (Int -> IntMap Aspects -> Maybe Aspects
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
pos IntMap Aspects
infoMap, Char
char)))

  -- Add position in file to each character.
  ([(Int, (LayerRole, Char))]
 -> [(LayerRole, (Maybe Aspects, Char))])
-> (String -> [(Int, (LayerRole, Char))])
-> String
-> [(LayerRole, (Maybe Aspects, Char))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> [(LayerRole, Char)] -> [(Int, (LayerRole, Char))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..]

  -- Map each character to its role
  ([(LayerRole, Char)] -> [(Int, (LayerRole, Char))])
-> (String -> [(LayerRole, Char)])
-> String
-> [(Int, (LayerRole, Char))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Layers -> [(LayerRole, Char)]
atomizeLayers (Layers -> [(LayerRole, Char)])
-> (String -> Layers) -> String -> [(LayerRole, Char)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Position -> String -> Layers
literateTeX (Maybe AbsolutePath -> Position
startPos (AbsolutePath -> Maybe AbsolutePath
forall a. a -> Maybe a
Just AbsolutePath
path))

  (String -> IO Text) -> String -> IO Text
forall a b. (a -> b) -> a -> b
$ Text -> String
L.unpack Text
source
  where
  infoMap :: IntMap Aspects
infoMap = File -> IntMap Aspects
toMap (HighlightingInfo -> File
decompress HighlightingInfo
hi)

  -- | This function preserves laziness of the list
  withLast :: (a -> a) -> [a] -> [a]
  withLast :: (a -> a) -> [a] -> [a]
withLast a -> a
f [] = []
  withLast a -> a
f [a
a] = [a -> a
f a
a]
  withLast a -> a
f (a
a:[a]
as) = a
aa -> [a] -> [a]
forall a. a -> [a] -> [a]
:(a -> a) -> [a] -> [a]
forall a. (a -> a) -> [a] -> [a]
withLast a -> a
f [a]
as

  -- | This function preserves laziness of the list
  withFirst :: (a -> a) -> [a] -> [a]
  withFirst :: (a -> a) -> [a] -> [a]
withFirst a -> a
_ [] = []
  withFirst a -> a
f (a
a:[a]
as) = a -> a
f a
aa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
as

  whenMoreThanOne :: ([a] -> [a]) -> [a] -> [a]
  whenMoreThanOne :: ([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
  :: Bool
     -- ^ Count extended grapheme clusters?
  -> [(LayerRole, Tokens)]
  -> IO L.Text
processTokens :: Bool -> [(LayerRole, [Token])] -> IO Text
processTokens Bool
cc [(LayerRole, [Token])]
ts = do
  ((), State
s, [Output]
os) <- LaTeX () -> () -> State -> IO ((), State, [Output])
forall a. LaTeX a -> () -> State -> IO (a, State, [Output])
runLaTeX ([(LayerRole, [Token])] -> LaTeX ()
processLayers [(LayerRole, [Token])]
ts) () (Bool -> State
emptyState Bool
cc)
  Text -> IO Text
forall (m :: * -> *) a. Monad m => a -> m a
return (Text -> IO Text) -> Text -> IO Text
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
L.fromChunks ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ (Output -> Text) -> [Output] -> [Text]
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 -> HashSet Int -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
Set.member Int
i (State -> HashSet Int
usedColumns State
s)) = Text
agdaSpace
      | Bool
otherwise                          = Text
nl Text -> Text -> Text
<+> AlignmentColumn -> Text
ptOpen AlignmentColumn
c