Doc.hs

{- |
Module      :  ./Common/Doc.hs
Description :  document data type Doc for (pretty) printing in various formats
Copyright   :  (c) Christian Maeder and Uni Bremen 2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

This module contains a document data type 'Doc' for displaying
(heterogenous) CASL specifications at least as plain text and latex
(and maybe html as well)

Inspired by John Hughes's and Simon Peyton Jones's Pretty Printer
Combinators in Text.PrettyPrint.HughesPJ, Thomas Hallgren's
PrettyDoc within programatica,
Daan Leijen's PPrint: A prettier printer 2001, and Olaf Chiti's Pretty
printing with lazy Dequeues 2003

The main combinators are those of HughesPJ except
nest, hang and $$. Instead of $$ '$+$' must be used that always forces a
line break. Indentation must be constructed using '<>' or '<+>', i.e.
'text' \"spec\" '<+>' MultilineBlock.

Also char, ptext, int, integer, float, double and rational do not
exist. These can all be simulated using 'text' (and 'show'). There's
an instance for 'Int' in "Common.DocUtils".

Furthermore, documents can no longer be tested with isEmpty. 'empty'
documents are silently ignored (as by HughesPJ) and
often it is more natural (or even necessary anyway) to test the
original data structure for emptiness.

Putting a document into braces should be done using 'specBraces' (but
a function braces is also exported), ensuring that opening and closing
braces are in the same column if the whole document does not fit on a
single line.

Rendering of documents is achieved by translations to the old
"Common.Lib.Pretty". For plain text simply 'show' can be
used. Any document can be translated to LaTeX via 'toLatex' and then
processed further by "Common.PrintLaTeX". If you like the output is a
different question, but the result should be legal LaTeX in
conjunction with the hetcasl.sty file.

For nicer looking LaTeX the predefined symbol constants should be
used! There is a difference between 'bullet' and 'dot' that is not
visible in plain text.

There are also three kinds of keywords, a plain 'keyword', a
'topSigKey' having the width of \"preds\", and a 'topKey' having the
width of \"view\". In plain text only inserted spaces are visible.

Strings in small caps are created by 'structId' and
'indexed'. The latter puts the string also into a LaTeX index.

In order to avoid considering display annotations and precedences,
documents can be constructed using 'annoDoc', 'idDoc', and 'idApplDoc'.

Currently only a few annotations (i.e. labels and %implied) are
printed 'flushRight'. This function is problematic as it does not
prevent something to be appended using '<>' or '<+>'. Furthermore
flushed parts are currently only visible in plain text, if they don't
fit on the same line (as nest is used for indenting).

Further functions are documented in "Common.DocUtils".

Examples can be produced using: hets -v2 -o pp.dol,pp.tex
-}

module Common.Doc
    ( -- * the document type
      Doc
    , Label (..)
    , StripComment (..)
    , renderHtml
    , renderExtHtml
    , renderText
    , renderExtText
      -- * primitive documents
    , empty
    , space
    , semi
    , comma
    , colon
    , quMarkD
    , equals
    , lparen
    , rparen
    , lbrack
    , rbrack
    , lbrace
    , rbrace
      -- * converting strings into documents
    , plainText
    , text
    , codeToken
    , commentText
    , keyword
    , topSigKey
    , topKey
    , indexed
    , structId
      -- * wrapping documents in delimiters
    , parens
    , brackets
    , braces
    , specBraces
    , quotes
    , doubleQuotes
      -- * combining documents
    -- , (<>)  -- exported via instance Semigroup Doc
    , (<+>)
    , hcat
    , hsep
    , ($+$)
    , ($++$)
    , vcat
    , vsep
    , sep
    , cat
    , fsep
    , fcat
    , punctuate
    , sepByCommas
    , sepBySemis
      -- * symbols possibly rendered differently for Text or LaTeX
    , dot
    , bullet
    , defn
    , less
    , greater
    , lambda
    , mapsto
    , funArrow
    , pfun
    , cfun
    , pcfun
    , exequal
    , forallDoc
    , exists
    , unique
    , cross
    , bar
    , notDoc
    , inDoc
    , andDoc
    , orDoc
    , implies
    , equiv
    , prefix_proc
    , sequential
    , interleave
    , synchronous
    , genpar_open
    , genpar_close
    , alpar_open
    , alpar_sep
    , alpar_close
    , external_choice
    , internal_choice
    , hiding_proc
    , ren_proc_open
    , ren_proc_close
    , dagger
    , vdash
    , dashv
    , breve
      -- * for Hybrid casl
    , prettyAt
    , prettyHere
    , prettyBind
    , prettyUniv
    , prettyExist
      -- * docifying annotations and ids
    , annoDoc
    , idDoc
    , idLabelDoc
    , predIdApplDoc
    , idApplDoc
      -- * transforming to existing formats
    , toLatex
    , toLatexAux
      -- * manipulating documents
    , flushRight
    , changeGlobalAnnos
    , rmTopKey
    , showRaw
    ) where

import Common.AS_Annotation
import Common.ConvertLiteral
import Common.GlobalAnnotations
import Common.Id
import Common.IRI
import Common.Keywords
import Common.LaTeX_funs
import Common.Prec
import qualified Common.Lib.Pretty as Pretty

import Data.Char
import Data.List
import Data.Maybe
import qualified Data.Map as Map
import qualified Data.Set as Set

infixr 6 <+>
infixl 5 $+$
infixl 5 $++$

-- * the data type

data LabelKind = IdDecl | IdAppl deriving (Show, Eq)

data TextKind =
    IdKind | IdSymb | Symbol | Comment | Keyword | TopKey Int
           | Indexed | StructId | Native | HetsLabel
           | IdLabel LabelKind TextKind Id deriving Show

data Format = Small | FlushRight deriving Show

data ComposeKind
    = Vert   -- ($+$) (no support for $$!)
    | Horiz  -- (<>)
    | HorizOrVert -- either Horiz or Vert
    | Fill
      deriving (Eq, Show)

-- | an abstract data type
data Doc
    = Empty          -- creates an empty line if composed vertically
    | AnnoDoc Annotation -- we know how to print annotations
    | IdDoc LabelKind Id -- for plain ids outside applications
    | IdApplDoc Bool Id [Doc] -- for mixfix applications and literal terms
    | Text TextKind String -- non-empty and no white spaces inside
    | Cat ComposeKind [Doc]
    | Attr Format Doc      -- for annotations
    | ChangeGlobalAnnos (GlobalAnnos -> GlobalAnnos) Doc

showRawList :: [Doc] -> String
showRawList l = "[" ++ intercalate ", " (map showRaw l) ++ "]"

showRaw :: Doc -> String
showRaw gd =
    case gd of
      Empty -> "Empty"
      AnnoDoc an -> "AnnoDoc(" ++ show an ++ ")"
      IdDoc lk n -> "IdDoc" ++ show (lk, n)
      IdApplDoc b n l ->
        "IdApplDoc(" ++ show b ++ ", " ++ show n ++ ", " ++ showRawList l ++ ")"
      Text tk s -> "Text(" ++ show tk ++ ", " ++ s ++ ")"
      Cat ck l ->
        "Cat(" ++ show ck ++ ", " ++ showRawList l ++ ")"
      Attr fm d -> "Attr(" ++ show fm ++ ", " ++ showRaw d ++ ")"
      ChangeGlobalAnnos _ d -> "ChangeGlobalAnnos(" ++ showRaw d ++ ")"

textStyle :: Pretty.Style
textStyle = Pretty.style
  { Pretty.ribbonsPerLine = 1.19
  , Pretty.lineLength = 80 }

renderText :: GlobalAnnos -> Doc -> String
renderText = renderExtText $ StripComment False

renderExtText :: StripComment -> GlobalAnnos -> Doc -> String
renderExtText stripCs ga =
  id . Pretty.renderStyle textStyle . toText stripCs ga

instance Show Doc where
    show = renderText emptyGlobalAnnos

renderHtml :: GlobalAnnos -> Doc -> String
renderHtml = renderExtHtml (StripComment False) $ MkLabel False

renderExtHtml :: StripComment -> Label -> GlobalAnnos -> Doc -> String
renderExtHtml stripCs lbl ga = replSpacesForHtml 0
  . Pretty.renderStyle textStyle . toHtml stripCs lbl ga

replSpacesForHtml :: Int -> String -> String
replSpacesForHtml n s = case s of
  "" -> ""
  c : r -> case c of
    '\n' -> c : "<br />" ++ replSpacesForHtml 0 r
    ' ' -> replSpacesForHtml (n + 1) r
    _ -> (case n of
      0 -> (c :)
      1 -> ([' ', c] ++)
      _ -> ((' ' : concat (replicate n "&nbsp; ") ++ [c]) ++))
      $ replSpacesForHtml 0 r

isEmpty :: Doc -> Bool
isEmpty d = case d of
              Empty -> True
              Cat _ [] -> True
              _ -> False


-- * the visible interface

empty :: Doc                 -- ^ An empty document
empty = Empty

plainText :: String -> Doc
plainText = Text IdKind

text :: String -> Doc
text s = case lines s of
    [] -> Text IdKind ""
    [x] -> Text IdKind x
    l -> vcat $ map (Text IdKind) l

semi :: Doc                 -- ^ A ';' character
semi = text ";"

comma :: Doc                 -- ^ A ',' character
comma = text ","

colon :: Doc                 -- ^ A ':' character
colon = symbol colonS

-- the only legal white space within Text
space :: Doc                 -- ^ A horizontal space (omitted at end of line)
space = text " "

equals :: Doc                 -- ^ A '=' character
equals = symbol equalS

-- use symbol for signs that need to be put in mathmode for latex
symbol :: String -> Doc
symbol = Text Symbol

-- for text within comments
commentText :: String -> Doc
commentText = Text Comment

-- put this string into math mode for latex and don't escape it
native :: String -> Doc
native = Text Native

lparen, rparen, lbrack, rbrack, lbrace, rbrace, quote, doubleQuote :: Doc

lparen = text "("
rparen = text ")"
lbrack = text "["
rbrack = text "]"
lbrace = symbol "{"  -- to allow for latex translations
rbrace = symbol "}"
quote = symbol "\'"
doubleQuote = symbol "\""

parens :: Doc -> Doc     -- ^ Wrap document in @(...)@
parens d = hcat [lparen, d, rparen]

brackets :: Doc -> Doc     -- ^ Wrap document in @[...]@
brackets d = hcat [lbrack, d, rbrack]

braces :: Doc -> Doc     -- ^ Wrap document in @{...}@
braces d = hcat [lbrace, d, rbrace]

specBraces :: Doc -> Doc     -- ^ Wrap document in @{...}@
specBraces d = cat [addLBrace d, rbrace]

-- | move the opening brace inwards
addLBrace :: Doc -> Doc
addLBrace d = case d of
    Cat k (e : r) -> Cat k $ addLBrace e : r
    ChangeGlobalAnnos f e -> ChangeGlobalAnnos f $ addLBrace e
    _ -> lbrace <> d

quotes :: Doc -> Doc     -- ^ Wrap document in @\'...\'@
quotes d = hcat [quote, d, quote]

doubleQuotes :: Doc -> Doc     -- ^ Wrap document in @\"...\"@
doubleQuotes d = hcat [doubleQuote, d, doubleQuote]

instance Semigroup Doc where
  a <> b = hcat [a, b]

rmEmpties :: [Doc] -> [Doc]
rmEmpties = filter (not . isEmpty)

hcat :: [Doc] -> Doc          -- ^List version of '<>'
hcat = Cat Horiz . rmEmpties

(<+>) :: Doc -> Doc -> Doc     -- ^Beside, separated by space
a <+> b = hsep [a, b]

punctuate :: Doc -> [Doc] -> [Doc]
punctuate d l = case l of
     x : r@(_ : _) -> (x <> d) : punctuate d r
     _ -> l

hsep :: [Doc] -> Doc         -- ^List version of '<+>'
hsep = Cat Horiz . punctuate space . rmEmpties

($+$) :: Doc -> Doc -> Doc    -- ^Above, without dovetailing.
a $+$ b = vcat [a, b]

-- | vertical composition with a specified number of blank lines
aboveWithNLs :: Int -> Doc -> Doc -> Doc
aboveWithNLs n d1 d2
  | isEmpty d2 = d1
  | isEmpty d1 = d2
  | otherwise = d1 $+$ foldr ($+$) d2 (replicate n $ text "")

-- | vertical composition with one blank line
($++$) :: Doc -> Doc -> Doc
($++$) = aboveWithNLs 1

-- | list version of '($++$)'
vsep :: [Doc] -> Doc
vsep = foldr ($++$) empty

vcat :: [Doc] -> Doc          -- ^List version of '$+$'
vcat = Cat Vert . rmEmpties

cat :: [Doc] -> Doc          -- ^ Either hcat or vcat
cat = Cat HorizOrVert . rmEmpties

sep :: [Doc] -> Doc          -- ^ Either hsep or vcat
sep = Cat HorizOrVert . punctuate space . rmEmpties

fcat :: [Doc] -> Doc          -- ^ \"Paragraph fill\" version of cat
fcat = Cat Fill . rmEmpties

fsep :: [Doc] -> Doc          -- ^ \"Paragraph fill\" version of sep
fsep = Cat Fill . punctuate space . rmEmpties

keyword, topSigKey, topKey, indexed, structId :: String -> Doc
keyword = Text Keyword
indexed = Text Indexed
structId = Text StructId
topKey = Text (TopKey 4)
topSigKey = Text (TopKey 5)

lambdaSymb, daggerS, vdashS, dashvS, breveS :: String
lambdaSymb = "\\"
daggerS = "!"
vdashS = "|-"
dashvS = "-|"
breveS = "~"

-- docs possibly rendered differently for Text or LaTeX
quMarkD, dot, bullet, defn, less, greater, lambda, mapsto, funArrow, pfun,
   cfun, pcfun, exequal, forallDoc, exists, unique, cross, bar, notDoc,
   inDoc, andDoc, orDoc, implies, equiv, prefix_proc, sequential,
   interleave, synchronous, genpar_open, genpar_close, alpar_open,
   alpar_sep, alpar_close, external_choice, internal_choice, hiding_proc,
   ren_proc_open, ren_proc_close, dagger, vdash, dashv, breve, prettyAt,
   prettyHere, prettyBind, prettyUniv, prettyExist :: Doc

quMarkD = text quMark
dot = text dotS
bullet = symbol dotS
defn = symbol defnS
less = symbol lessS
greater = symbol greaterS
lambda = symbol lambdaSymb
mapsto = symbol mapsTo
funArrow = symbol funS
pfun = symbol pFun
cfun = symbol contFun
pcfun = symbol pContFun
exequal = symbol exEqual
forallDoc = symbol forallS
exists = symbol existsS
unique = symbol existsUnique
cross = symbol prodS
bar = symbol barS
notDoc = symbol notS
inDoc = symbol inS
andDoc = symbol lAnd
orDoc = symbol lOr
implies = symbol implS
equiv = symbol equivS
prefix_proc = symbol prefix_procS
sequential = text sequentialS
interleave = symbol interleavingS
synchronous = symbol synchronousS
genpar_open = symbol genpar_openS
genpar_close = symbol genpar_closeS
alpar_open = symbol alpar_openS
-- note that alpar_sepS and synchronousS are equal
alpar_sep = symbol alpar_sepS
alpar_close = symbol alpar_closeS
external_choice = symbol external_choiceS
internal_choice = symbol internal_choiceS
hiding_proc = text hiding_procS -- otherwise it clashes with lambda
ren_proc_open = symbol ren_proc_openS
ren_proc_close = symbol ren_proc_closeS
dagger = symbol daggerS
vdash = symbol vdashS
dashv = symbol dashvS
breve = symbol breveS
-- * for hybrid casl
prettyAt = symbol asP
prettyHere = symbol "Here"
prettyBind = symbol "Bind"
prettyUniv = symbol "Univ"
prettyExist = symbol "Exist"
-- | we know how to print annotations
annoDoc :: Annotation -> Doc
annoDoc = AnnoDoc

-- | for plain ids outside of terms
idDoc :: Id -> Doc
idDoc = IdDoc IdAppl

-- | for newly declared ids
idLabelDoc :: Id -> Doc
idLabelDoc = IdDoc IdDecl

-- | for mixfix applications and literal terms (may print \"\" for empty)
idApplDoc :: Id -> [Doc] -> Doc
idApplDoc = IdApplDoc False

-- | for mixfix applications of predicate identifiers
predIdApplDoc :: Id -> [Doc] -> Doc
predIdApplDoc = IdApplDoc True

-- | put document as far to the right as fits (for annotations)
flushRight :: Doc -> Doc
flushRight = Attr FlushRight

small :: Doc -> Doc
small = Attr Small

-- * folding stuff

data DocRecord a = DocRecord
    { foldEmpty :: Doc -> a
    , foldAnnoDoc :: Doc -> Annotation -> a
    , foldIdDoc :: Doc -> LabelKind -> Id -> a
    , foldIdApplDoc :: Doc -> Bool -> Id -> [a] -> a
    , foldText :: Doc -> TextKind -> String -> a
    , foldCat :: Doc -> ComposeKind -> [a] -> a
    , foldAttr :: Doc -> Format -> a -> a
    , foldChangeGlobalAnnos :: Doc -> (GlobalAnnos -> GlobalAnnos) -> a -> a
    }

foldDoc :: DocRecord a -> Doc -> a
foldDoc r d = case d of
    Empty -> foldEmpty r d
    AnnoDoc a -> foldAnnoDoc r d a
    IdDoc l i -> foldIdDoc r d l i
    IdApplDoc b i l -> foldIdApplDoc r d b i $ map (foldDoc r) l
    Text k s -> foldText r d k s
    Cat k l -> foldCat r d k $ map (foldDoc r) l
    Attr a e -> foldAttr r d a $ foldDoc r e
    ChangeGlobalAnnos f e -> foldChangeGlobalAnnos r d f $ foldDoc r e

idRecord :: DocRecord Doc
idRecord = DocRecord
    { foldEmpty = const Empty
    , foldAnnoDoc = const AnnoDoc
    , foldIdDoc = const IdDoc
    , foldIdApplDoc = const IdApplDoc
    , foldText = const Text
    , foldCat = const Cat
    , foldAttr = const Attr
    , foldChangeGlobalAnnos = const ChangeGlobalAnnos
    }

anyRecord :: DocRecord a
anyRecord = DocRecord
    { foldEmpty = error "anyRecord.Empty"
    , foldAnnoDoc = error "anyRecord.AnnoDoc"
    , foldIdDoc = error "anyRecord.IdDoc"
    , foldIdApplDoc = error "anyRecord.IdApplDoc"
    , foldText = error "anyRecord.Text"
    , foldCat = error "anyRecord.Cat"
    , foldAttr = error "anyRecord.Attr"
    , foldChangeGlobalAnnos = error "anyRecord.ChangeGlobalAnnos"
    }

newtype Label = MkLabel Bool

newtype StripComment = StripComment Bool

-- * conversion to plain text

-- | simple conversion to a standard text document
toText :: StripComment -> GlobalAnnos -> Doc -> Pretty.Doc
toText stripCs ga = toTextAux . codeOut stripCs ga
  (mkPrecIntMap $ prec_annos ga) Nothing Map.empty

toTextAux :: Doc -> Pretty.Doc
toTextAux = foldDoc anyRecord
    { foldEmpty = const Pretty.empty
    , foldText = \ _ k s -> case k of
          TopKey n -> Pretty.text $ s ++ replicate (n - length s) ' '
          _ -> Pretty.text s
    , foldCat = \ d c l -> case d of
        Cat _ ds@(_ : _) -> if all hasSpace $ init ds then
          (case c of
          Vert -> Pretty.vcat
          Horiz -> Pretty.hsep
          HorizOrVert -> Pretty.sep
          Fill -> Pretty.fsep) $ map (toTextAux . rmSpace) ds
          else (case c of
          Vert -> Pretty.vcat
          Horiz -> Pretty.hcat
          HorizOrVert -> Pretty.cat
          Fill -> Pretty.fcat) l
        _ -> Pretty.empty
    , foldAttr = \ _ k d -> case k of
          FlushRight -> let l = length $ show d in
            if l < 66 then Pretty.nest (66 - l) d else d
          _ -> d
    , foldChangeGlobalAnnos = \ _ _ d -> d
    }

-- * conversion to html

-- | conversion to html
toHtml :: StripComment -> Label -> GlobalAnnos -> Doc -> Pretty.Doc
toHtml stripCs lbl ga d = let
  dm = Map.map (Map.! DF_HTML)
       . Map.filter (Map.member DF_HTML) $ display_annos ga
  dis = getDeclIds d
  in foldDoc (toHtmlRecord lbl dis) $ codeOut stripCs ga
                 (mkPrecIntMap $ prec_annos ga) (Just DF_HTML) dm d

toHtmlRecord :: Label -> Set.Set Id -> DocRecord Pretty.Doc
toHtmlRecord lbl dis = anyRecord
    { foldEmpty = const Pretty.empty
    , foldText = const $ textToHtml lbl dis
    , foldCat = \ d c l -> case d of
        Cat _ ds@(_ : _) -> if all hasSpace $ init ds then
          (case c of
          Vert -> Pretty.vcat
          Horiz -> Pretty.hsep
          HorizOrVert -> Pretty.sep
          Fill -> Pretty.fsep)
            $ map (foldDoc (toHtmlRecord lbl dis) . rmSpace) ds
          else (case c of
          Vert -> Pretty.vcat
          Horiz -> Pretty.hcat
          HorizOrVert -> Pretty.cat
          Fill -> Pretty.fcat) l
        _ -> Pretty.empty
    , foldAttr = \ a k d -> case k of
          FlushRight ->
              let Attr _ o = a
                  l = length $ show $ toTextAux o
              in if l < 66 then Pretty.nest (66 - l) d else d
          _ -> d
    , foldChangeGlobalAnnos = \ _ _ d -> d
    }

textToHtml :: Label -> Set.Set Id -> TextKind -> String -> Pretty.Doc
textToHtml lbl@(MkLabel mkLbl) dis k s = let
  e = escapeHtml s ""
  h = Pretty.text e
  zeroText = Pretty.sizedText 0
  tagB t = '<' : t ++ ">"
  tagE t = tagB $ '/' : t
  tag t d = Pretty.hcat [zeroText (tagB t), d, zeroText (tagE t) ]
  tagBold = tag "strong"
  hi = tag "em" h
 in case k of
    Native -> Pretty.text s
    Keyword -> tagBold h
    TopKey n -> let l = n - length s in
      tagBold $ h Pretty.<> Pretty.text (replicate l ' ')
    Comment -> tag "small" h
    Indexed -> hi
    StructId -> hi
    HetsLabel -> tag "small" hi
    IdLabel appl tk i -> let
        d = textToHtml lbl dis tk s
        si = escapeHtml (showId i "") ""
        in if mkLbl && Set.member i dis then Pretty.hcat
        [zeroText $ "<a " ++ (if appl == IdAppl then "href=\"#" else "name=\"")
        ++ si ++ "\">", d, zeroText "</a>"]
        else d
    _ -> h

escChar :: Char -> ShowS
escChar c = case c of
  '\'' -> showString "&#39;"
  '<' -> showString "&lt;"
  '>' -> showString "&gt;"
  '&' -> showString "&amp;"
  '"' -> showString "&quot;"
  _ -> showChar c

escapeHtml :: String -> ShowS
escapeHtml cs rs = foldr escChar rs cs

-- * conversion to latex

toLatex :: GlobalAnnos -> Doc -> Pretty.Doc
toLatex = toLatexAux (StripComment False) $ MkLabel False

toLatexAux :: StripComment -> Label -> GlobalAnnos -> Doc -> Pretty.Doc
toLatexAux stripCs lbl ga d = let
  dm = Map.map (Map.! DF_LATEX) .
                      Map.filter (Map.member DF_LATEX) $ display_annos ga
  dis = getDeclIds d
    in foldDoc (toLatexRecord lbl dis False)
           . makeSmallMath False False $ codeOut stripCs ga
                 (mkPrecIntMap $ prec_annos ga) (Just DF_LATEX) dm d

-- avoid too many tabs
toLatexRecord :: Label -> Set.Set Id -> Bool -> DocRecord Pretty.Doc
toLatexRecord lbl dis tab = anyRecord
    { foldEmpty = const Pretty.empty
    , foldText = const $ textToLatex lbl dis False
    , foldCat = \ o _ _ -> case o of
        Cat c os@(d : r)
          | any isNative os -> Pretty.hcat $
             latex_macro "{\\Ax{"
             : map (foldDoc (toLatexRecord lbl dis False)
                       { foldText = \ _ k s ->
                          case k of
                            Native -> Pretty.sizedText (axiom_width s) s
                            IdLabel _ Native _ ->
                                Pretty.sizedText (axiom_width s) s
                            IdKind | s == " " ->
                                Pretty.sizedText (axiom_width s) "\\,"
                            _ -> textToLatex lbl dis False k s
                        }) os
              ++ [latex_macro "}}"]
          | null r -> foldDoc (toLatexRecord lbl dis tab) d
          | otherwise -> (if tab && c /= Horiz then
                             (latex_macro setTab Pretty.<>)
                         . (latex_macro startTab Pretty.<>)
                         . (Pretty.<> latex_macro endTab)
                        else id)
                        $ (case c of
                             Vert -> Pretty.vcat
                             Horiz -> Pretty.hcat
                             HorizOrVert -> Pretty.cat
                             Fill -> Pretty.fcat)
                        $ case c of
                            Vert ->
                              map (foldDoc $ toLatexRecord lbl dis False) os
                            _ -> foldDoc (toLatexRecord lbl dis False) d :
                              map (foldDoc $ toLatexRecord lbl dis True) r
        _ -> Pretty.empty
    , foldAttr = \ o k d -> case k of
          FlushRight -> flushright d
          Small -> case o of
              Attr Small (Text j s) -> textToLatex lbl dis True j s
              _ -> makeSmallLatex True d
    , foldChangeGlobalAnnos = \ _ _ d -> d
    }

-- | move a small attribute inwards but not into mathmode bits
makeSmallMath :: Bool -> Bool -> Doc -> Doc
makeSmallMath smll math =
    foldDoc idRecord
    { foldAttr = \ o _ _ -> case o of
                       Attr Small d -> makeSmallMath True math d
                       Attr k d -> Attr k $ makeSmallMath smll math d
                       _ -> error "makeSmallMath.foldAttr"
    , foldCat = \ o _ _ -> case o of
                  Cat c l
                    | any isNative l ->
                        (if smll then Attr Small else id)
                        -- flatten math mode bits
                           $ Cat Horiz $ map
                                 (makeSmallMath False True . rmSpace) l
                    | math -> Cat Horiz
                         $ map (makeSmallMath False True) l
                    | smll && allHoriz o ->
                    -- produce fewer small blocks with wrong size though
                             Attr Small $ Cat Horiz $
                              map (makeSmallMath False math) l
                    | otherwise -> Cat c $ map (makeSmallMath smll math) l
                  _ -> error "makeSmallMath.foldCat"
    , foldText = \ d _ _ -> if smll then Attr Small d else d
    }

-- | check for unbalanced braces
needsMathMode :: Int -> String -> Bool
needsMathMode i s = case s of
    [] -> i > 0
    '{' : r -> needsMathMode (i + 1) r
    '}' : r -> i == 0 || needsMathMode (i - 1) r
    _ : r -> needsMathMode i r

isMathLatex :: Doc -> Bool
isMathLatex d = case d of
               Text Native s -> needsMathMode 0 s
               Text (IdLabel _ Native _) s -> needsMathMode 0 s
               Attr Small f -> isMathLatex f
               _ -> False

isNative :: Doc -> Bool
isNative d = case d of
               Cat Horiz [t, _] -> isMathLatex t
               _ -> isMathLatex d

-- | remove the spaces inserted by punctuate
rmSpace :: Doc -> Doc
rmSpace = snd . anaSpace

hasSpace :: Doc -> Bool
hasSpace = fst . anaSpace

anaSpace :: Doc -> (Bool, Doc)
anaSpace d = case d of
              Cat Horiz [t, Text IdKind s] | s == " " -> (True, t)
              _ -> (False, d)

allHoriz :: Doc -> Bool
allHoriz d = case d of
               Text _ _ -> True
               Cat Horiz l -> all allHoriz l
               Attr _ f -> allHoriz f
               Empty -> True
               _ -> False

makeSmallLatex :: Bool -> Pretty.Doc -> Pretty.Doc
makeSmallLatex b d = if b then
    Pretty.hcat [latex_macro startAnno, d, latex_macro endAnno] else d

symbolToLatex :: String -> Pretty.Doc
symbolToLatex s =
    Map.findWithDefault (hc_sty_axiom $ escapeSpecial s) s latexSymbols

getDeclIds :: Doc -> Set.Set Id
getDeclIds = foldDoc anyRecord
    { foldEmpty = const Set.empty
    , foldText = \ _ _ _ -> Set.empty
    , foldCat = \ _ _ -> Set.unions
    , foldAttr = \ _ _ d -> d
    , foldChangeGlobalAnnos = \ _ _ d -> d
    , foldIdDoc = \ _ lk i ->
          if lk == IdDecl then Set.singleton i else Set.empty
    , foldIdApplDoc = \ _ _ _ _ -> Set.empty
    , foldAnnoDoc = \ _ _ -> Set.empty
    }

textToLatex :: Label -> Set.Set Id -> Bool -> TextKind -> String -> Pretty.Doc
textToLatex lbl@(MkLabel mkLbl) dis b k s = case s of
  "" -> Pretty.text ""
  h : _ -> let e = escapeLatex s in case k of
    IdKind -> makeSmallLatex b $ if elem s $ map (: []) ",;[]() "
              then casl_normal_latex s
              else hc_sty_id e
    IdSymb -> makeSmallLatex b $ if s == "__" then symbolToLatex s
              else if isAlpha h || elem h "._'" then hc_sty_id e
              else hc_sty_axiom (escapeSpecial s)
    Symbol -> makeSmallLatex b $ symbolToLatex s
    Comment -> makeSmallLatex b $ casl_comment_latex e
               -- multiple spaces should be replaced by \hspace
    Keyword -> (if b then makeSmallLatex b . hc_sty_small_keyword
                else hc_sty_plain_keyword) s
    TopKey _ -> hc_sty_casl_keyword s
    Indexed -> hc_sty_structid_indexed s
    StructId -> hc_sty_structid s
    Native -> hc_sty_axiom s
    HetsLabel -> let d = textToLatex lbl dis b Comment s in
       if mkLbl then Pretty.hcat [ latex_macro "\\HetsLabel{", d
                                 , latex_macro $ "}{" ++ escapeLabel s ++ "}" ]
       else d
    -- HetsLabel may be avoided by the Label case
    IdLabel appl tk i -> let
        d = textToLatex lbl dis b tk s
        si = showId i ""
        in if b || not mkLbl || appl == IdAppl && not (Set.member i dis)
               || not (isLegalLabel si)
           -- make this case True to avoid labels
           then d else Pretty.hcat
            [ latex_macro $ '\\' : shows appl "Label{"
            , d
            , latex_macro $ "}{" ++ escapeLabel si ++ "}" ]

escapeLabel :: String -> String
escapeLabel = map ( \ c -> if c == '_' then ':' else c)

latexSymbols :: Map.Map String Pretty.Doc
latexSymbols = Map.union (Map.fromList
    [ ("{", casl_normal_latex "\\{")
    , ("}", casl_normal_latex "\\}")
    , (barS, casl_normal_latex "\\AltBar{}")
    , (percentS, hc_sty_small_keyword "%")
    , (percents, hc_sty_small_keyword "%%")
    , (exEqual, Pretty.sizedText (axiom_width "=") "\\Ax{\\stackrel{e}{=}}") ])
    $ Map.map hc_sty_axiom $ Map.fromList
    [ (dotS, "\\bullet")
    , (diamondS, "\\Diamond")
    , ("__", "\\_\\_")
    , (lambdaSymb, "\\lambda")
    , (mapsTo, "\\mapsto")
    , (funS, "\\rightarrow")
    , (pFun, "\\rightarrow?")
    , (contFun, "\\stackrel{c}{\\rightarrow}")
    , (pContFun, "\\stackrel{c}{\\rightarrow}?")
    , (forallS, "\\forall")
    , (existsS, "\\exists")
    , (existsUnique, "\\exists!")
    , (prodS, "\\times")
    , (notS, "\\neg")
    , (inS, "\\in")
    , (lAnd, "\\wedge")
    , (lOr, "\\vee")
    , (daggerS, "\\dag")
    , (vdashS, "\\vdash")
    , (dashvS, "\\dashv")
    , (breveS, "\\breve{~}")
    , (implS, "\\Rightarrow")
    , (equivS, "\\Leftrightarrow")
    , (interleavingS, "{|}\\mkern-2mu{|}\\mkern-2mu{|}")
    , (synchronousS, "\\parallel")
    , (external_choiceS, "\\Box")
    , (internal_choiceS, "\\sqcap")
    , (ren_proc_openS, "[\\mkern-2mu{[}")
    , (ren_proc_closeS, "]\\mkern-2mu{]}")
    ]

-- * coding out stuff

{- | transform document according to a specific display map and other
global annotations like precedences, associativities, and literal
annotations. -}
codeOut :: StripComment -> GlobalAnnos -> PrecMap -> Maybe Display_format
        -> Map.Map Id [Token] -> Doc -> Doc
codeOut stripCs ga precs d m = foldDoc idRecord
    { foldAnnoDoc = \ _ -> small . codeOutAnno stripCs m
    , foldIdDoc = \ _ lk -> codeOutId lk m
    , foldIdApplDoc = \ o _ _ -> codeOutAppl stripCs ga precs d m o
    , foldChangeGlobalAnnos = \ o _ _ ->
          let ChangeGlobalAnnos fg e = o
              ng = fg ga
          in codeOut stripCs ng (mkPrecIntMap $ prec_annos ng) d
             (maybe m (\ f -> Map.map (Map.! f) .
                      Map.filter (Map.member f) $ display_annos ng) d) e
    }

codeToken :: String -> Doc
codeToken = Text IdSymb

codeOrigId :: LabelKind -> Map.Map Id [Token] -> Id -> [Doc]
codeOrigId lk m i@(Id ts cs _) = let
    (toks, places) = splitMixToken ts
    conv = reverse . snd . foldl ( \ (b, l) t ->
           let s = tokStr t
           in if isPlace t then (b, symbol s : l)
              else (True, (if b then codeToken s else makeLabel lk IdSymb s i)
                            : l)) (False, [])
    in if null cs then conv ts
       else conv toks ++ codeCompIds m cs : conv places

cCommaT :: Map.Map Id [Token] -> [Id] -> [Doc]
cCommaT m = punctuate comma . map (codeOutId IdAppl m)

codeCompIds :: Map.Map Id [Token] -> [Id] -> Doc
codeCompIds m = brackets . fcat . cCommaT m

codeOutId :: LabelKind -> Map.Map Id [Token] -> Id -> Doc
codeOutId lk m i = fcat $ case Map.lookup i m of
    Nothing -> codeOrigId lk m i
    Just ts -> reverse $ snd $ foldl ( \ (b, l) t ->
        let s = tokStr t
        in if isPlace t then (b, symbol s : l) else
            (True, (if b then native s else
                        makeLabel lk Native s i) : l)) (False, []) ts

makeLabel :: LabelKind -> TextKind -> String -> Id -> Doc
makeLabel l k s i = Text (IdLabel l k i) s

annoLine :: String -> Doc
annoLine w = percent <> keyword w

annoLparen :: String -> Doc
annoLparen w = percent <> keyword w <> lparen

wrapLines :: TextKind -> Doc -> [String] -> Doc -> Doc
wrapLines k a l b = let p = (null (head l), null (last l)) in
  case map (Text k) l of
    [] -> a <> b
    [x] -> hcat [a, x, b]
    [x, y] -> case p of
        (True, c) -> a $+$ if c then b else y <> b
        (False, True) -> a <> x $+$ b
        _ -> a <> (x $+$ y <> b)
    x : r -> let
      m = init r
      y = last r
      xm = x : m
      am = a : m
      yb = [y <> b]
      in case p of
        (True, c) -> vcat $ am ++ if c then [b] else yb
        (False, True) -> a <> vcat xm $+$ b
        _ -> a <> vcat (xm ++ yb)

wrapAnnoLines :: Doc -> [String] -> Doc -> Doc
wrapAnnoLines = wrapLines Comment

percent :: Doc
percent = symbol percentS

annoRparen :: Doc
annoRparen = rparen <> percent

hCommaT :: Map.Map Id [Token] -> [Id] -> Doc
hCommaT m = hsep . cCommaT m

fCommaT :: Map.Map Id [Token] -> [Id] -> Doc
fCommaT m = fsep . cCommaT m

codeOutAnno :: StripComment -> Map.Map Id [Token] -> Annotation -> Doc
codeOutAnno (StripComment stripCs) m a = case a of
    Unparsed_anno aw at _ -> if stripCs then empty else case at of
        Line_anno s -> (case aw of
            Annote_word w -> annoLine w
            Comment_start -> symbol percents) <> commentText s
        Group_anno l -> case aw of
            Annote_word w -> wrapAnnoLines (annoLparen w) l annoRparen
            Comment_start -> wrapAnnoLines (percent <> lbrace) l
                             $ rbrace <> percent
    Display_anno i ds _ -> annoLparen displayS <> fsep
        ( fcat (codeOrigId IdAppl m i) :
          map ( \ (df, s) -> percent <> commentText (lookupDisplayFormat df)
                <+> maybe (commentText s) (const $ codeOutId IdAppl m i)
                    (Map.lookup i m)) ds) <> annoRparen
    List_anno i1 i2 i3 _ -> annoLine listS <+> hCommaT m [i1, i2, i3]
    Number_anno i _ -> annoLine numberS <+> codeOutId IdAppl m i
    Float_anno i1 i2 _ -> annoLine floatingS <+> hCommaT m [i1, i2]
    String_anno i1 i2 _ -> annoLine stringS <+> hCommaT m [i1, i2]
    Prec_anno p l1 l2 _ -> annoLparen precS <>
        fsep [ braces $ fCommaT m l1
             , case p of
                 Lower -> less
                 Higher -> greater
                 BothDirections -> less <> greater
                 NoDirection -> greater <> less
             , braces $ fCommaT m l2
             ] <> annoRparen
    Assoc_anno s l _ -> annoLparen (case s of
                          ALeft -> left_assocS
                          ARight -> right_assocS)
                        <> fCommaT m l <> annoRparen
    Label l _ -> wrapLines (case l of
                  [x] -> if isLegalLabel x then HetsLabel else Comment
                  _ -> Comment) (percent <> lparen) l annoRparen
    Prefix_anno pm _ -> annoLparen prefixS <> vcat
        (map ( \ (s, i) -> text (s ++ ":")
                <+> text (iriToStringUnsecure $ setAngles True i)) pm)
        <> annoRparen
    Semantic_anno sa _ -> annoLine $ lookupSemanticAnno sa

isLegalLabel :: String -> Bool
isLegalLabel r = not (null r) && all ( \ c -> isAlphaNum c || elem c "_" ) r

splitDoc :: Doc -> Maybe (Id, [Doc])
splitDoc d = case d of
    IdApplDoc _ i l -> Just (i, l)
    _ -> Nothing

sepByCommas :: [Doc] -> Doc
sepByCommas = fsep . punctuate comma

sepBySemis :: [Doc] -> Doc
sepBySemis = fsep . punctuate semi

data Weight = Weight Int Id Id Id -- top, left, right

parenAppl :: GlobalAnnos -> PrecMap -> Doc -> [Bool] -> Doc -> [Bool]
parenAppl ga precs origDoc l arg = case origDoc of
  IdApplDoc isPred i _ -> let
    pa = prec_annos ga
    assocs = assoc_annos ga
    mx = maxWeight precs
    pm = precMap precs
    e = Map.findWithDefault mx eqId pm
    p = Map.findWithDefault (if isInfix i then e else mx) i pm
    in case getWeight ga precs arg of
                Nothing -> False : l
                Just (Weight q ta la ra) ->
                    let d = isBoth pa i ta
                        oArg = (q < e || p >= e &&
                                         (notElem i [eqId, exEq]
                                         || elem ta [eqId, exEq]))
                                  && isDiffAssoc assocs pa i ta
                                || d
                    in (if isLeftArg i l then
                     if checkArg ARight ga (i, p) (ta, q) ra
                       then oArg
                       else not (isPred || isSafeLhs i ta) || d
                    else if isRightArg i l then
                       if checkArg ALeft ga (i, p) (ta, q) la
                       then oArg
                       else (applId == i || isInfix ta)
                                && not isPred || d
                     else d) : l
  _ -> False : l

parenApplArgs :: GlobalAnnos -> PrecMap -> Doc -> [Bool]
parenApplArgs ga precs origDoc = case origDoc of
  IdApplDoc _ _ aas -> reverse $ foldl (parenAppl ga precs origDoc) [] aas
  _ -> []

-- print literal terms and mixfix applications
codeOutAppl :: StripComment -> GlobalAnnos -> PrecMap -> Maybe Display_format
            -> Map.Map Id [Token] -> Doc -> [Doc] -> Doc
codeOutAppl stripCs ga precs md m origDoc args = case origDoc of
  IdApplDoc _ i@(Id ts cs _) aas ->
    let mk = codeToken . tokStr
        doSplit = fromMaybe (error "doSplit") . splitDoc
        mkList op largs cl = fsep $ codeOutId IdAppl m op : punctuate comma
          (map (codeOut stripCs ga precs md m) largs)
          ++ [codeOutId IdAppl m cl]
    in if isGenNumber splitDoc ga i aas then
             mk $ toNumber doSplit i aas
         else if isGenFrac splitDoc ga i aas then
             mk $ toFrac doSplit aas
         else if isGenFloat splitDoc ga i aas then
             mk $ toFloat doSplit ga aas
         else if isGenString splitDoc ga i aas then
             mk $ toString doSplit ga i aas
         else if isGenList splitDoc ga i aas then
             toMixfixList mkList doSplit ga i aas
         else if null args || length args /= placeCount i then
             codeOutId IdAppl m i <> if null args then empty else
                                  parens (sepByCommas args)
         else let
             pars = parenApplArgs ga precs origDoc
             parArgs = zipWith (\ b -> if b then parens else id) pars args
             (fts, ncs, cFun) = case Map.lookup i m of
                            Nothing ->
                                (fst $ splitMixToken ts, cs, IdSymb)
                            Just nts -> (nts, [], Native)
             ((_, rArgs), fArgs) = mapAccumL ( \ (b, ac) t ->
               if isPlace t then case ac of
                 hd : tl -> ((b, tl), (False, hd))
                 _ -> error "Common.Doc.codeOutAppl1"
                 else ((True, ac), (True,
                       let s = tokStr t in
                       if b then Text cFun s else makeIdApplLabel cFun s i)))
                                                  (False, parArgs) fts
            in fsep $ hgroup $
               (if null ncs then fArgs
                else if null fArgs then error "Common.Doc.codeOutAppl2"
                     else init fArgs ++
                              [(True, snd (last fArgs) <> codeCompIds m cs)])
               ++ map ( \ d -> (False, d)) rArgs
  _ -> error "Common.Doc.codeOutAppl2"

hgroup :: [(Bool, Doc)] -> [Doc]
hgroup l = case l of
  (True, d1) : (False, d2) : r -> hsep [d1, d2] : hgroup r
  (_, d) : r -> d : hgroup r
  [] -> []

makeIdApplLabel :: TextKind -> String -> Id -> Doc
makeIdApplLabel k s i = Text (IdLabel IdAppl k i) s

getWeight :: GlobalAnnos -> PrecMap -> Doc -> Maybe Weight
getWeight ga precs d = let
    m = precMap precs
    in case d of
    IdApplDoc _ i aas@(hd : _) ->
        let p = Map.findWithDefault
              (if begPlace i || endPlace i then Map.findWithDefault 0 eqId m
               else maxWeight precs)
              i m in
        if isGenLiteral splitDoc ga i aas then Nothing else
        let pars@(par : _) = parenApplArgs ga precs d
            lw = case getWeight ga precs hd of
                   Just (Weight _ _ l _) -> nextWeight ALeft ga i l
                   Nothing -> i
            rw = case getWeight ga precs $ last aas of
                   Just (Weight _ _ _ r) -> nextWeight ARight ga i r
                   Nothing -> i
            in Just $ Weight p i (if par then i else lw)
               $ if last pars then i else rw
    _ -> Nothing

{- checkArg allows any nested infixes that are not listed in the
   precedence graph in order to report ambiguities when parsed. The
   following case require parens when printed. -}
isDiffAssoc :: AssocMap -> PrecedenceGraph -> Id -> Id -> Bool
isDiffAssoc assocs precs op arg = isInfix op && isInfix arg &&
            if op /= arg then
               arg /= applId && case precRel precs op arg of
               Lower -> False
               _ -> True
            else not $ Map.member arg assocs

-- no need for parens in the following cases
isSafeLhs :: Id -> Id -> Bool
isSafeLhs op arg = applId /= op &&
    (applId == arg || isPostfix arg || endPlace op && not (isInfix arg))

isBoth :: PrecedenceGraph -> Id -> Id -> Bool
isBoth precs op arg = case precRel precs op arg of
                    BothDirections -> True
                    _ -> False

-- | change top-level to plain keywords
rmTopKey :: Doc -> Doc
rmTopKey = foldDoc idRecord
    { foldText = \ d k s -> case k of
          TopKey _ -> Text Keyword s
          _ -> d
    }

-- | add global annotations for proper mixfix printing
changeGlobalAnnos :: (GlobalAnnos -> GlobalAnnos) -> Doc -> Doc
changeGlobalAnnos = ChangeGlobalAnnos