{- |
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 (Int -> LabelKind -> ShowS
[LabelKind] -> ShowS
LabelKind -> String
(Int -> LabelKind -> ShowS)
-> (LabelKind -> String)
-> ([LabelKind] -> ShowS)
-> Show LabelKind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LabelKind] -> ShowS
$cshowList :: [LabelKind] -> ShowS
show :: LabelKind -> String
$cshow :: LabelKind -> String
showsPrec :: Int -> LabelKind -> ShowS
$cshowsPrec :: Int -> LabelKind -> ShowS
Show, LabelKind -> LabelKind -> Bool
(LabelKind -> LabelKind -> Bool)
-> (LabelKind -> LabelKind -> Bool) -> Eq LabelKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LabelKind -> LabelKind -> Bool
$c/= :: LabelKind -> LabelKind -> Bool
== :: LabelKind -> LabelKind -> Bool
$c== :: LabelKind -> LabelKind -> Bool
Eq)

data TextKind =
    IdKind | IdSymb | Symbol | Comment | Keyword | TopKey Int
           | Indexed | StructId | Native | HetsLabel
           | IdLabel LabelKind TextKind Id deriving Int -> TextKind -> ShowS
[TextKind] -> ShowS
TextKind -> String
(Int -> TextKind -> ShowS)
-> (TextKind -> String) -> ([TextKind] -> ShowS) -> Show TextKind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TextKind] -> ShowS
$cshowList :: [TextKind] -> ShowS
show :: TextKind -> String
$cshow :: TextKind -> String
showsPrec :: Int -> TextKind -> ShowS
$cshowsPrec :: Int -> TextKind -> ShowS
Show

data Format = Small | FlushRight deriving Int -> Format -> ShowS
[Format] -> ShowS
Format -> String
(Int -> Format -> ShowS)
-> (Format -> String) -> ([Format] -> ShowS) -> Show Format
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Format] -> ShowS
$cshowList :: [Format] -> ShowS
show :: Format -> String
$cshow :: Format -> String
showsPrec :: Int -> Format -> ShowS
$cshowsPrec :: Int -> Format -> ShowS
Show

data ComposeKind
    = Vert   -- ($+$) (no support for $$!)
    | Horiz  -- (<>)
    | HorizOrVert -- either Horiz or Vert
    | Fill
      deriving (ComposeKind -> ComposeKind -> Bool
(ComposeKind -> ComposeKind -> Bool)
-> (ComposeKind -> ComposeKind -> Bool) -> Eq ComposeKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ComposeKind -> ComposeKind -> Bool
$c/= :: ComposeKind -> ComposeKind -> Bool
== :: ComposeKind -> ComposeKind -> Bool
$c== :: ComposeKind -> ComposeKind -> Bool
Eq, Int -> ComposeKind -> ShowS
[ComposeKind] -> ShowS
ComposeKind -> String
(Int -> ComposeKind -> ShowS)
-> (ComposeKind -> String)
-> ([ComposeKind] -> ShowS)
-> Show ComposeKind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ComposeKind] -> ShowS
$cshowList :: [ComposeKind] -> ShowS
show :: ComposeKind -> String
$cshow :: ComposeKind -> String
showsPrec :: Int -> ComposeKind -> ShowS
$cshowsPrec :: Int -> ComposeKind -> ShowS
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 :: [Doc] -> String
showRawList l :: [Doc]
l = "[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " ((Doc -> String) -> [Doc] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Doc -> String
showRaw [Doc]
l) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "]"

showRaw :: Doc -> String
showRaw :: Doc -> String
showRaw gd :: Doc
gd =
    case Doc
gd of
      Empty -> "Empty"
      AnnoDoc an :: Annotation
an -> "AnnoDoc(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Annotation -> String
forall a. Show a => a -> String
show Annotation
an String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
      IdDoc lk :: LabelKind
lk n :: Id
n -> "IdDoc" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (LabelKind, Id) -> String
forall a. Show a => a -> String
show (LabelKind
lk, Id
n)
      IdApplDoc b :: Bool
b n :: Id
n l :: [Doc]
l ->
        "IdApplDoc(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> String
forall a. Show a => a -> String
show Bool
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ ", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ ", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Doc] -> String
showRawList [Doc]
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
      Text tk :: TextKind
tk s :: String
s -> "Text(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TextKind -> String
forall a. Show a => a -> String
show TextKind
tk String -> ShowS
forall a. [a] -> [a] -> [a]
++ ", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
      Cat ck :: ComposeKind
ck l :: [Doc]
l ->
        "Cat(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ComposeKind -> String
forall a. Show a => a -> String
show ComposeKind
ck String -> ShowS
forall a. [a] -> [a] -> [a]
++ ", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Doc] -> String
showRawList [Doc]
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
      Attr fm :: Format
fm d :: Doc
d -> "Attr(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Format -> String
forall a. Show a => a -> String
show Format
fm String -> ShowS
forall a. [a] -> [a] -> [a]
++ ", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
showRaw Doc
d String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
      ChangeGlobalAnnos _ d :: Doc
d -> "ChangeGlobalAnnos(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
showRaw Doc
d String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"

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

renderText :: GlobalAnnos -> Doc -> String
renderText :: GlobalAnnos -> Doc -> String
renderText = StripComment -> GlobalAnnos -> Doc -> String
renderExtText (StripComment -> GlobalAnnos -> Doc -> String)
-> StripComment -> GlobalAnnos -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Bool -> StripComment
StripComment Bool
False

renderExtText :: StripComment -> GlobalAnnos -> Doc -> String
renderExtText :: StripComment -> GlobalAnnos -> Doc -> String
renderExtText stripCs :: StripComment
stripCs ga :: GlobalAnnos
ga =
  ShowS
forall a. a -> a
id ShowS -> (Doc -> String) -> Doc -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Style -> Doc -> String
Pretty.renderStyle Style
textStyle (Doc -> String) -> (Doc -> Doc) -> Doc -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StripComment -> GlobalAnnos -> Doc -> Doc
toText StripComment
stripCs GlobalAnnos
ga

instance Show Doc where
    show :: Doc -> String
show = GlobalAnnos -> Doc -> String
renderText GlobalAnnos
emptyGlobalAnnos

renderHtml :: GlobalAnnos -> Doc -> String
renderHtml :: GlobalAnnos -> Doc -> String
renderHtml = StripComment -> Label -> GlobalAnnos -> Doc -> String
renderExtHtml (Bool -> StripComment
StripComment Bool
False) (Label -> GlobalAnnos -> Doc -> String)
-> Label -> GlobalAnnos -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Bool -> Label
MkLabel Bool
False

renderExtHtml :: StripComment -> Label -> GlobalAnnos -> Doc -> String
renderExtHtml :: StripComment -> Label -> GlobalAnnos -> Doc -> String
renderExtHtml stripCs :: StripComment
stripCs lbl :: Label
lbl ga :: GlobalAnnos
ga = Int -> ShowS
replSpacesForHtml 0
  ShowS -> (Doc -> String) -> Doc -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Style -> Doc -> String
Pretty.renderStyle Style
textStyle (Doc -> String) -> (Doc -> Doc) -> Doc -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StripComment -> Label -> GlobalAnnos -> Doc -> Doc
toHtml StripComment
stripCs Label
lbl GlobalAnnos
ga

replSpacesForHtml :: Int -> String -> String
replSpacesForHtml :: Int -> ShowS
replSpacesForHtml n :: Int
n s :: String
s = case String
s of
  "" -> ""
  c :: Char
c : r :: String
r -> case Char
c of
    '\n' -> Char
c Char -> ShowS
forall a. a -> [a] -> [a]
: "<br />" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> ShowS
replSpacesForHtml 0 String
r
    ' ' -> Int -> ShowS
replSpacesForHtml (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) String
r
    _ -> (case Int
n of
      0 -> (Char
c Char -> ShowS
forall a. a -> [a] -> [a]
:)
      1 -> ([' ', Char
c] String -> ShowS
forall a. [a] -> [a] -> [a]
++)
      _ -> ((' ' Char -> ShowS
forall a. a -> [a] -> [a]
: [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Int -> String -> [String]
forall a. Int -> a -> [a]
replicate Int
n "&nbsp; ") String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char
c]) String -> ShowS
forall a. [a] -> [a] -> [a]
++))
      ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> ShowS
replSpacesForHtml 0 String
r

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


-- * the visible interface

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

plainText :: String -> Doc
plainText :: String -> Doc
plainText = TextKind -> String -> Doc
Text TextKind
IdKind

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | move the opening brace inwards
addLBrace :: Doc -> Doc
addLBrace :: Doc -> Doc
addLBrace d :: Doc
d = case Doc
d of
    Cat k :: ComposeKind
k (e :: Doc
e : r :: [Doc]
r) -> ComposeKind -> [Doc] -> Doc
Cat ComposeKind
k ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
addLBrace Doc
e Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [Doc]
r
    ChangeGlobalAnnos f :: GlobalAnnos -> GlobalAnnos
f e :: Doc
e -> (GlobalAnnos -> GlobalAnnos) -> Doc -> Doc
ChangeGlobalAnnos GlobalAnnos -> GlobalAnnos
f (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
addLBrace Doc
e
    _ -> Doc
lbrace Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
d

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

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

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

rmEmpties :: [Doc] -> [Doc]
rmEmpties :: [Doc] -> [Doc]
rmEmpties = (Doc -> Bool) -> [Doc] -> [Doc]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Doc -> Bool) -> Doc -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Bool
isEmpty)

hcat :: [Doc] -> Doc          -- ^List version of '<>'
hcat :: [Doc] -> Doc
hcat = ComposeKind -> [Doc] -> Doc
Cat ComposeKind
Horiz ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> [Doc]
rmEmpties

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

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

hsep :: [Doc] -> Doc         -- ^List version of '<+>'
hsep :: [Doc] -> Doc
hsep = ComposeKind -> [Doc] -> Doc
Cat ComposeKind
Horiz ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
space ([Doc] -> [Doc]) -> ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> [Doc]
rmEmpties

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

-- | vertical composition with a specified number of blank lines
aboveWithNLs :: Int -> Doc -> Doc -> Doc
aboveWithNLs :: Int -> Doc -> Doc -> Doc
aboveWithNLs n :: Int
n d1 :: Doc
d1 d2 :: Doc
d2
  | Doc -> Bool
isEmpty Doc
d2 = Doc
d1
  | Doc -> Bool
isEmpty Doc
d1 = Doc
d2
  | Bool
otherwise = Doc
d1 Doc -> Doc -> Doc
$+$ (Doc -> Doc -> Doc) -> Doc -> [Doc] -> Doc
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Doc -> Doc -> Doc
($+$) Doc
d2 (Int -> Doc -> [Doc]
forall a. Int -> a -> [a]
replicate Int
n (Doc -> [Doc]) -> Doc -> [Doc]
forall a b. (a -> b) -> a -> b
$ String -> Doc
text "")

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

-- | list version of '($++$)'
vsep :: [Doc] -> Doc
vsep :: [Doc] -> Doc
vsep = (Doc -> Doc -> Doc) -> Doc -> [Doc] -> Doc
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Doc -> Doc -> Doc
($++$) Doc
empty

vcat :: [Doc] -> Doc          -- ^List version of '$+$'
vcat :: [Doc] -> Doc
vcat = ComposeKind -> [Doc] -> Doc
Cat ComposeKind
Vert ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> [Doc]
rmEmpties

cat :: [Doc] -> Doc          -- ^ Either hcat or vcat
cat :: [Doc] -> Doc
cat = ComposeKind -> [Doc] -> Doc
Cat ComposeKind
HorizOrVert ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> [Doc]
rmEmpties

sep :: [Doc] -> Doc          -- ^ Either hsep or vcat
sep :: [Doc] -> Doc
sep = ComposeKind -> [Doc] -> Doc
Cat ComposeKind
HorizOrVert ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
space ([Doc] -> [Doc]) -> ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> [Doc]
rmEmpties

fcat :: [Doc] -> Doc          -- ^ \"Paragraph fill\" version of cat
fcat :: [Doc] -> Doc
fcat = ComposeKind -> [Doc] -> Doc
Cat ComposeKind
Fill ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> [Doc]
rmEmpties

fsep :: [Doc] -> Doc          -- ^ \"Paragraph fill\" version of sep
fsep :: [Doc] -> Doc
fsep = ComposeKind -> [Doc] -> Doc
Cat ComposeKind
Fill ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
space ([Doc] -> [Doc]) -> ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> [Doc]
rmEmpties

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

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

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

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

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

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

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

small :: Doc -> Doc
small :: Doc -> Doc
small = Format -> Doc -> Doc
Attr Format
Small

-- * folding stuff

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

foldDoc :: DocRecord a -> Doc -> a
foldDoc :: DocRecord a -> Doc -> a
foldDoc r :: DocRecord a
r d :: Doc
d = case Doc
d of
    Empty -> DocRecord a -> Doc -> a
forall a. DocRecord a -> Doc -> a
foldEmpty DocRecord a
r Doc
d
    AnnoDoc a :: Annotation
a -> DocRecord a -> Doc -> Annotation -> a
forall a. DocRecord a -> Doc -> Annotation -> a
foldAnnoDoc DocRecord a
r Doc
d Annotation
a
    IdDoc l :: LabelKind
l i :: Id
i -> DocRecord a -> Doc -> LabelKind -> Id -> a
forall a. DocRecord a -> Doc -> LabelKind -> Id -> a
foldIdDoc DocRecord a
r Doc
d LabelKind
l Id
i
    IdApplDoc b :: Bool
b i :: Id
i l :: [Doc]
l -> DocRecord a -> Doc -> Bool -> Id -> [a] -> a
forall a. DocRecord a -> Doc -> Bool -> Id -> [a] -> a
foldIdApplDoc DocRecord a
r Doc
d Bool
b Id
i ([a] -> a) -> [a] -> a
forall a b. (a -> b) -> a -> b
$ (Doc -> a) -> [Doc] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (DocRecord a -> Doc -> a
forall a. DocRecord a -> Doc -> a
foldDoc DocRecord a
r) [Doc]
l
    Text k :: TextKind
k s :: String
s -> DocRecord a -> Doc -> TextKind -> String -> a
forall a. DocRecord a -> Doc -> TextKind -> String -> a
foldText DocRecord a
r Doc
d TextKind
k String
s
    Cat k :: ComposeKind
k l :: [Doc]
l -> DocRecord a -> Doc -> ComposeKind -> [a] -> a
forall a. DocRecord a -> Doc -> ComposeKind -> [a] -> a
foldCat DocRecord a
r Doc
d ComposeKind
k ([a] -> a) -> [a] -> a
forall a b. (a -> b) -> a -> b
$ (Doc -> a) -> [Doc] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (DocRecord a -> Doc -> a
forall a. DocRecord a -> Doc -> a
foldDoc DocRecord a
r) [Doc]
l
    Attr a :: Format
a e :: Doc
e -> DocRecord a -> Doc -> Format -> a -> a
forall a. DocRecord a -> Doc -> Format -> a -> a
foldAttr DocRecord a
r Doc
d Format
a (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ DocRecord a -> Doc -> a
forall a. DocRecord a -> Doc -> a
foldDoc DocRecord a
r Doc
e
    ChangeGlobalAnnos f :: GlobalAnnos -> GlobalAnnos
f e :: Doc
e -> DocRecord a -> Doc -> (GlobalAnnos -> GlobalAnnos) -> a -> a
forall a.
DocRecord a -> Doc -> (GlobalAnnos -> GlobalAnnos) -> a -> a
foldChangeGlobalAnnos DocRecord a
r Doc
d GlobalAnnos -> GlobalAnnos
f (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ DocRecord a -> Doc -> a
forall a. DocRecord a -> Doc -> a
foldDoc DocRecord a
r Doc
e

idRecord :: DocRecord Doc
idRecord :: DocRecord Doc
idRecord = DocRecord :: forall a.
(Doc -> a)
-> (Doc -> Annotation -> a)
-> (Doc -> LabelKind -> Id -> a)
-> (Doc -> Bool -> Id -> [a] -> a)
-> (Doc -> TextKind -> String -> a)
-> (Doc -> ComposeKind -> [a] -> a)
-> (Doc -> Format -> a -> a)
-> (Doc -> (GlobalAnnos -> GlobalAnnos) -> a -> a)
-> DocRecord a
DocRecord
    { foldEmpty :: Doc -> Doc
foldEmpty = Doc -> Doc -> Doc
forall a b. a -> b -> a
const Doc
Empty
    , foldAnnoDoc :: Doc -> Annotation -> Doc
foldAnnoDoc = (Annotation -> Doc) -> Doc -> Annotation -> Doc
forall a b. a -> b -> a
const Annotation -> Doc
AnnoDoc
    , foldIdDoc :: Doc -> LabelKind -> Id -> Doc
foldIdDoc = (LabelKind -> Id -> Doc) -> Doc -> LabelKind -> Id -> Doc
forall a b. a -> b -> a
const LabelKind -> Id -> Doc
IdDoc
    , foldIdApplDoc :: Doc -> Bool -> Id -> [Doc] -> Doc
foldIdApplDoc = (Bool -> Id -> [Doc] -> Doc) -> Doc -> Bool -> Id -> [Doc] -> Doc
forall a b. a -> b -> a
const Bool -> Id -> [Doc] -> Doc
IdApplDoc
    , foldText :: Doc -> TextKind -> String -> Doc
foldText = (TextKind -> String -> Doc) -> Doc -> TextKind -> String -> Doc
forall a b. a -> b -> a
const TextKind -> String -> Doc
Text
    , foldCat :: Doc -> ComposeKind -> [Doc] -> Doc
foldCat = (ComposeKind -> [Doc] -> Doc) -> Doc -> ComposeKind -> [Doc] -> Doc
forall a b. a -> b -> a
const ComposeKind -> [Doc] -> Doc
Cat
    , foldAttr :: Doc -> Format -> Doc -> Doc
foldAttr = (Format -> Doc -> Doc) -> Doc -> Format -> Doc -> Doc
forall a b. a -> b -> a
const Format -> Doc -> Doc
Attr
    , foldChangeGlobalAnnos :: Doc -> (GlobalAnnos -> GlobalAnnos) -> Doc -> Doc
foldChangeGlobalAnnos = ((GlobalAnnos -> GlobalAnnos) -> Doc -> Doc)
-> Doc -> (GlobalAnnos -> GlobalAnnos) -> Doc -> Doc
forall a b. a -> b -> a
const (GlobalAnnos -> GlobalAnnos) -> Doc -> Doc
ChangeGlobalAnnos
    }

anyRecord :: DocRecord a
anyRecord :: DocRecord a
anyRecord = DocRecord :: forall a.
(Doc -> a)
-> (Doc -> Annotation -> a)
-> (Doc -> LabelKind -> Id -> a)
-> (Doc -> Bool -> Id -> [a] -> a)
-> (Doc -> TextKind -> String -> a)
-> (Doc -> ComposeKind -> [a] -> a)
-> (Doc -> Format -> a -> a)
-> (Doc -> (GlobalAnnos -> GlobalAnnos) -> a -> a)
-> DocRecord a
DocRecord
    { foldEmpty :: Doc -> a
foldEmpty = String -> Doc -> a
forall a. HasCallStack => String -> a
error "anyRecord.Empty"
    , foldAnnoDoc :: Doc -> Annotation -> a
foldAnnoDoc = String -> Doc -> Annotation -> a
forall a. HasCallStack => String -> a
error "anyRecord.AnnoDoc"
    , foldIdDoc :: Doc -> LabelKind -> Id -> a
foldIdDoc = String -> Doc -> LabelKind -> Id -> a
forall a. HasCallStack => String -> a
error "anyRecord.IdDoc"
    , foldIdApplDoc :: Doc -> Bool -> Id -> [a] -> a
foldIdApplDoc = String -> Doc -> Bool -> Id -> [a] -> a
forall a. HasCallStack => String -> a
error "anyRecord.IdApplDoc"
    , foldText :: Doc -> TextKind -> String -> a
foldText = String -> Doc -> TextKind -> String -> a
forall a. HasCallStack => String -> a
error "anyRecord.Text"
    , foldCat :: Doc -> ComposeKind -> [a] -> a
foldCat = String -> Doc -> ComposeKind -> [a] -> a
forall a. HasCallStack => String -> a
error "anyRecord.Cat"
    , foldAttr :: Doc -> Format -> a -> a
foldAttr = String -> Doc -> Format -> a -> a
forall a. HasCallStack => String -> a
error "anyRecord.Attr"
    , foldChangeGlobalAnnos :: Doc -> (GlobalAnnos -> GlobalAnnos) -> a -> a
foldChangeGlobalAnnos = String -> Doc -> (GlobalAnnos -> GlobalAnnos) -> a -> a
forall a. HasCallStack => String -> a
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 :: StripComment -> GlobalAnnos -> Doc -> Doc
toText stripCs :: StripComment
stripCs ga :: GlobalAnnos
ga = Doc -> Doc
toTextAux (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StripComment
-> GlobalAnnos
-> PrecMap
-> Maybe Display_format
-> Map Id [Token]
-> Doc
-> Doc
codeOut StripComment
stripCs GlobalAnnos
ga
  (Rel Id -> PrecMap
mkPrecIntMap (Rel Id -> PrecMap) -> Rel Id -> PrecMap
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> Rel Id
prec_annos GlobalAnnos
ga) Maybe Display_format
forall a. Maybe a
Nothing Map Id [Token]
forall k a. Map k a
Map.empty

toTextAux :: Doc -> Pretty.Doc
toTextAux :: Doc -> Doc
toTextAux = DocRecord Doc -> Doc -> Doc
forall a. DocRecord a -> Doc -> a
foldDoc DocRecord Doc
forall a. DocRecord a
anyRecord
    { foldEmpty :: Doc -> Doc
foldEmpty = Doc -> Doc -> Doc
forall a b. a -> b -> a
const Doc
Pretty.empty
    , foldText :: Doc -> TextKind -> String -> Doc
foldText = \ _ k :: TextKind
k s :: String
s -> case TextKind
k of
          TopKey n :: Int
n -> String -> Doc
Pretty.text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s) ' '
          _ -> String -> Doc
Pretty.text String
s
    , foldCat :: Doc -> ComposeKind -> [Doc] -> Doc
foldCat = \ d :: Doc
d c :: ComposeKind
c l :: [Doc]
l -> case Doc
d of
        Cat _ ds :: [Doc]
ds@(_ : _) -> if (Doc -> Bool) -> [Doc] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Doc -> Bool
hasSpace ([Doc] -> Bool) -> [Doc] -> Bool
forall a b. (a -> b) -> a -> b
$ [Doc] -> [Doc]
forall a. [a] -> [a]
init [Doc]
ds then
          (case ComposeKind
c of
          Vert -> [Doc] -> Doc
Pretty.vcat
          Horiz -> [Doc] -> Doc
Pretty.hsep
          HorizOrVert -> [Doc] -> Doc
Pretty.sep
          Fill -> [Doc] -> Doc
Pretty.fsep) ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Doc -> Doc) -> [Doc] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
toTextAux (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Doc
rmSpace) [Doc]
ds
          else (case ComposeKind
c of
          Vert -> [Doc] -> Doc
Pretty.vcat
          Horiz -> [Doc] -> Doc
Pretty.hcat
          HorizOrVert -> [Doc] -> Doc
Pretty.cat
          Fill -> [Doc] -> Doc
Pretty.fcat) [Doc]
l
        _ -> Doc
Pretty.empty
    , foldAttr :: Doc -> Format -> Doc -> Doc
foldAttr = \ _ k :: Format
k d :: Doc
d -> case Format
k of
          FlushRight -> let l :: Int
l = String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show Doc
d in
            if Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 66 then Int -> Doc -> Doc
Pretty.nest (66 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
l) Doc
d else Doc
d
          _ -> Doc
d
    , foldChangeGlobalAnnos :: Doc -> (GlobalAnnos -> GlobalAnnos) -> Doc -> Doc
foldChangeGlobalAnnos = \ _ _ d :: Doc
d -> Doc
d
    }

-- * conversion to html

-- | conversion to html
toHtml :: StripComment -> Label -> GlobalAnnos -> Doc -> Pretty.Doc
toHtml :: StripComment -> Label -> GlobalAnnos -> Doc -> Doc
toHtml stripCs :: StripComment
stripCs lbl :: Label
lbl ga :: GlobalAnnos
ga d :: Doc
d = let
  dm :: Map Id [Token]
dm = (Map Display_format [Token] -> [Token])
-> Map Id (Map Display_format [Token]) -> Map Id [Token]
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Map Display_format [Token] -> Display_format -> [Token]
forall k a. Ord k => Map k a -> k -> a
Map.! Display_format
DF_HTML)
       (Map Id (Map Display_format [Token]) -> Map Id [Token])
-> (Map Id (Map Display_format [Token])
    -> Map Id (Map Display_format [Token]))
-> Map Id (Map Display_format [Token])
-> Map Id [Token]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map Display_format [Token] -> Bool)
-> Map Id (Map Display_format [Token])
-> Map Id (Map Display_format [Token])
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Display_format -> Map Display_format [Token] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Display_format
DF_HTML) (Map Id (Map Display_format [Token]) -> Map Id [Token])
-> Map Id (Map Display_format [Token]) -> Map Id [Token]
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> Map Id (Map Display_format [Token])
display_annos GlobalAnnos
ga
  dis :: Set Id
dis = Doc -> Set Id
getDeclIds Doc
d
  in DocRecord Doc -> Doc -> Doc
forall a. DocRecord a -> Doc -> a
foldDoc (Label -> Set Id -> DocRecord Doc
toHtmlRecord Label
lbl Set Id
dis) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ StripComment
-> GlobalAnnos
-> PrecMap
-> Maybe Display_format
-> Map Id [Token]
-> Doc
-> Doc
codeOut StripComment
stripCs GlobalAnnos
ga
                 (Rel Id -> PrecMap
mkPrecIntMap (Rel Id -> PrecMap) -> Rel Id -> PrecMap
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> Rel Id
prec_annos GlobalAnnos
ga) (Display_format -> Maybe Display_format
forall a. a -> Maybe a
Just Display_format
DF_HTML) Map Id [Token]
dm Doc
d

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

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

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

escapeHtml :: String -> ShowS
escapeHtml :: String -> ShowS
escapeHtml cs :: String
cs rs :: String
rs = (Char -> ShowS) -> String -> ShowS
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Char -> ShowS
escChar String
rs String
cs

-- * conversion to latex

toLatex :: GlobalAnnos -> Doc -> Pretty.Doc
toLatex :: GlobalAnnos -> Doc -> Doc
toLatex = StripComment -> Label -> GlobalAnnos -> Doc -> Doc
toLatexAux (Bool -> StripComment
StripComment Bool
False) (Label -> GlobalAnnos -> Doc -> Doc)
-> Label -> GlobalAnnos -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Bool -> Label
MkLabel Bool
False

toLatexAux :: StripComment -> Label -> GlobalAnnos -> Doc -> Pretty.Doc
toLatexAux :: StripComment -> Label -> GlobalAnnos -> Doc -> Doc
toLatexAux stripCs :: StripComment
stripCs lbl :: Label
lbl ga :: GlobalAnnos
ga d :: Doc
d = let
  dm :: Map Id [Token]
dm = (Map Display_format [Token] -> [Token])
-> Map Id (Map Display_format [Token]) -> Map Id [Token]
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Map Display_format [Token] -> Display_format -> [Token]
forall k a. Ord k => Map k a -> k -> a
Map.! Display_format
DF_LATEX) (Map Id (Map Display_format [Token]) -> Map Id [Token])
-> (Map Id (Map Display_format [Token])
    -> Map Id (Map Display_format [Token]))
-> Map Id (Map Display_format [Token])
-> Map Id [Token]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                      (Map Display_format [Token] -> Bool)
-> Map Id (Map Display_format [Token])
-> Map Id (Map Display_format [Token])
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Display_format -> Map Display_format [Token] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Display_format
DF_LATEX) (Map Id (Map Display_format [Token]) -> Map Id [Token])
-> Map Id (Map Display_format [Token]) -> Map Id [Token]
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> Map Id (Map Display_format [Token])
display_annos GlobalAnnos
ga
  dis :: Set Id
dis = Doc -> Set Id
getDeclIds Doc
d
    in DocRecord Doc -> Doc -> Doc
forall a. DocRecord a -> Doc -> a
foldDoc (Label -> Set Id -> Bool -> DocRecord Doc
toLatexRecord Label
lbl Set Id
dis Bool
False)
           (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool -> Doc -> Doc
makeSmallMath Bool
False Bool
False (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ StripComment
-> GlobalAnnos
-> PrecMap
-> Maybe Display_format
-> Map Id [Token]
-> Doc
-> Doc
codeOut StripComment
stripCs GlobalAnnos
ga
                 (Rel Id -> PrecMap
mkPrecIntMap (Rel Id -> PrecMap) -> Rel Id -> PrecMap
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> Rel Id
prec_annos GlobalAnnos
ga) (Display_format -> Maybe Display_format
forall a. a -> Maybe a
Just Display_format
DF_LATEX) Map Id [Token]
dm Doc
d

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

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

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

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

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

-- | remove the spaces inserted by punctuate
rmSpace :: Doc -> Doc
rmSpace :: Doc -> Doc
rmSpace = (Bool, Doc) -> Doc
forall a b. (a, b) -> b
snd ((Bool, Doc) -> Doc) -> (Doc -> (Bool, Doc)) -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> (Bool, Doc)
anaSpace

hasSpace :: Doc -> Bool
hasSpace :: Doc -> Bool
hasSpace = (Bool, Doc) -> Bool
forall a b. (a, b) -> a
fst ((Bool, Doc) -> Bool) -> (Doc -> (Bool, Doc)) -> Doc -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> (Bool, Doc)
anaSpace

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

allHoriz :: Doc -> Bool
allHoriz :: Doc -> Bool
allHoriz d :: Doc
d = case Doc
d of
               Text _ _ -> Bool
True
               Cat Horiz l :: [Doc]
l -> (Doc -> Bool) -> [Doc] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Doc -> Bool
allHoriz [Doc]
l
               Attr _ f :: Doc
f -> Doc -> Bool
allHoriz Doc
f
               Empty -> Bool
True
               _ -> Bool
False

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

symbolToLatex :: String -> Pretty.Doc
symbolToLatex :: String -> Doc
symbolToLatex s :: String
s =
    Doc -> String -> Map String Doc -> Doc
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Doc
hc_sty_axiom (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ ShowS
escapeSpecial String
s) String
s Map String Doc
latexSymbols

getDeclIds :: Doc -> Set.Set Id
getDeclIds :: Doc -> Set Id
getDeclIds = DocRecord (Set Id) -> Doc -> Set Id
forall a. DocRecord a -> Doc -> a
foldDoc DocRecord Any
forall a. DocRecord a
anyRecord
    { foldEmpty :: Doc -> Set Id
foldEmpty = Set Id -> Doc -> Set Id
forall a b. a -> b -> a
const Set Id
forall a. Set a
Set.empty
    , foldText :: Doc -> TextKind -> String -> Set Id
foldText = \ _ _ _ -> Set Id
forall a. Set a
Set.empty
    , foldCat :: Doc -> ComposeKind -> [Set Id] -> Set Id
foldCat = \ _ _ -> [Set Id] -> Set Id
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
    , foldAttr :: Doc -> Format -> Set Id -> Set Id
foldAttr = \ _ _ d :: Set Id
d -> Set Id
d
    , foldChangeGlobalAnnos :: Doc -> (GlobalAnnos -> GlobalAnnos) -> Set Id -> Set Id
foldChangeGlobalAnnos = \ _ _ d :: Set Id
d -> Set Id
d
    , foldIdDoc :: Doc -> LabelKind -> Id -> Set Id
foldIdDoc = \ _ lk :: LabelKind
lk i :: Id
i ->
          if LabelKind
lk LabelKind -> LabelKind -> Bool
forall a. Eq a => a -> a -> Bool
== LabelKind
IdDecl then Id -> Set Id
forall a. a -> Set a
Set.singleton Id
i else Set Id
forall a. Set a
Set.empty
    , foldIdApplDoc :: Doc -> Bool -> Id -> [Set Id] -> Set Id
foldIdApplDoc = \ _ _ _ _ -> Set Id
forall a. Set a
Set.empty
    , foldAnnoDoc :: Doc -> Annotation -> Set Id
foldAnnoDoc = \ _ _ -> Set Id
forall a. Set a
Set.empty
    }

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

escapeLabel :: String -> String
escapeLabel :: ShowS
escapeLabel = (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map ( \ c :: Char
c -> if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '_' then ':' else Char
c)

latexSymbols :: Map.Map String Pretty.Doc
latexSymbols :: Map String Doc
latexSymbols = Map String Doc -> Map String Doc -> Map String Doc
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union ([(String, Doc)] -> Map String Doc
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
    [ ("{", String -> Doc
casl_normal_latex "\\{")
    , ("}", String -> Doc
casl_normal_latex "\\}")
    , (String
barS, String -> Doc
casl_normal_latex "\\AltBar{}")
    , (String
percentS, String -> Doc
hc_sty_small_keyword "%")
    , (String
percents, String -> Doc
hc_sty_small_keyword "%%")
    , (String
exEqual, Int -> String -> Doc
Pretty.sizedText (String -> Int
axiom_width "=") "\\Ax{\\stackrel{e}{=}}") ])
    (Map String Doc -> Map String Doc)
-> Map String Doc -> Map String Doc
forall a b. (a -> b) -> a -> b
$ (String -> Doc) -> Map String String -> Map String Doc
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map String -> Doc
hc_sty_axiom (Map String String -> Map String Doc)
-> Map String String -> Map String Doc
forall a b. (a -> b) -> a -> b
$ [(String, String)] -> Map String String
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
    [ (String
dotS, "\\bullet")
    , (String
diamondS, "\\Diamond")
    , ("__", "\\_\\_")
    , (String
lambdaSymb, "\\lambda")
    , (String
mapsTo, "\\mapsto")
    , (String
funS, "\\rightarrow")
    , (String
pFun, "\\rightarrow?")
    , (String
contFun, "\\stackrel{c}{\\rightarrow}")
    , (String
pContFun, "\\stackrel{c}{\\rightarrow}?")
    , (String
forallS, "\\forall")
    , (String
existsS, "\\exists")
    , (String
existsUnique, "\\exists!")
    , (String
prodS, "\\times")
    , (String
notS, "\\neg")
    , (String
inS, "\\in")
    , (String
lAnd, "\\wedge")
    , (String
lOr, "\\vee")
    , (String
daggerS, "\\dag")
    , (String
vdashS, "\\vdash")
    , (String
dashvS, "\\dashv")
    , (String
breveS, "\\breve{~}")
    , (String
implS, "\\Rightarrow")
    , (String
equivS, "\\Leftrightarrow")
    , (String
interleavingS, "{|}\\mkern-2mu{|}\\mkern-2mu{|}")
    , (String
synchronousS, "\\parallel")
    , (String
external_choiceS, "\\Box")
    , (String
internal_choiceS, "\\sqcap")
    , (String
ren_proc_openS, "[\\mkern-2mu{[}")
    , (String
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 :: StripComment
-> GlobalAnnos
-> PrecMap
-> Maybe Display_format
-> Map Id [Token]
-> Doc
-> Doc
codeOut stripCs :: StripComment
stripCs ga :: GlobalAnnos
ga precs :: PrecMap
precs d :: Maybe Display_format
d m :: Map Id [Token]
m = DocRecord Doc -> Doc -> Doc
forall a. DocRecord a -> Doc -> a
foldDoc DocRecord Doc
idRecord
    { foldAnnoDoc :: Doc -> Annotation -> Doc
foldAnnoDoc = \ _ -> Doc -> Doc
small (Doc -> Doc) -> (Annotation -> Doc) -> Annotation -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StripComment -> Map Id [Token] -> Annotation -> Doc
codeOutAnno StripComment
stripCs Map Id [Token]
m
    , foldIdDoc :: Doc -> LabelKind -> Id -> Doc
foldIdDoc = \ _ lk :: LabelKind
lk -> LabelKind -> Map Id [Token] -> Id -> Doc
codeOutId LabelKind
lk Map Id [Token]
m
    , foldIdApplDoc :: Doc -> Bool -> Id -> [Doc] -> Doc
foldIdApplDoc = \ o :: Doc
o _ _ -> StripComment
-> GlobalAnnos
-> PrecMap
-> Maybe Display_format
-> Map Id [Token]
-> Doc
-> [Doc]
-> Doc
codeOutAppl StripComment
stripCs GlobalAnnos
ga PrecMap
precs Maybe Display_format
d Map Id [Token]
m Doc
o
    , foldChangeGlobalAnnos :: Doc -> (GlobalAnnos -> GlobalAnnos) -> Doc -> Doc
foldChangeGlobalAnnos = \ o :: Doc
o _ _ ->
          let ChangeGlobalAnnos fg :: GlobalAnnos -> GlobalAnnos
fg e :: Doc
e = Doc
o
              ng :: GlobalAnnos
ng = GlobalAnnos -> GlobalAnnos
fg GlobalAnnos
ga
          in StripComment
-> GlobalAnnos
-> PrecMap
-> Maybe Display_format
-> Map Id [Token]
-> Doc
-> Doc
codeOut StripComment
stripCs GlobalAnnos
ng (Rel Id -> PrecMap
mkPrecIntMap (Rel Id -> PrecMap) -> Rel Id -> PrecMap
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> Rel Id
prec_annos GlobalAnnos
ng) Maybe Display_format
d
             (Map Id [Token]
-> (Display_format -> Map Id [Token])
-> Maybe Display_format
-> Map Id [Token]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Map Id [Token]
m (\ f :: Display_format
f -> (Map Display_format [Token] -> [Token])
-> Map Id (Map Display_format [Token]) -> Map Id [Token]
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Map Display_format [Token] -> Display_format -> [Token]
forall k a. Ord k => Map k a -> k -> a
Map.! Display_format
f) (Map Id (Map Display_format [Token]) -> Map Id [Token])
-> (Map Id (Map Display_format [Token])
    -> Map Id (Map Display_format [Token]))
-> Map Id (Map Display_format [Token])
-> Map Id [Token]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                      (Map Display_format [Token] -> Bool)
-> Map Id (Map Display_format [Token])
-> Map Id (Map Display_format [Token])
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Display_format -> Map Display_format [Token] -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Display_format
f) (Map Id (Map Display_format [Token]) -> Map Id [Token])
-> Map Id (Map Display_format [Token]) -> Map Id [Token]
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> Map Id (Map Display_format [Token])
display_annos GlobalAnnos
ng) Maybe Display_format
d) Doc
e
    }

codeToken :: String -> Doc
codeToken :: String -> Doc
codeToken = TextKind -> String -> Doc
Text TextKind
IdSymb

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

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

codeCompIds :: Map.Map Id [Token] -> [Id] -> Doc
codeCompIds :: Map Id [Token] -> [Id] -> Doc
codeCompIds m :: Map Id [Token]
m = Doc -> Doc
brackets (Doc -> Doc) -> ([Id] -> Doc) -> [Id] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
fcat ([Doc] -> Doc) -> ([Id] -> [Doc]) -> [Id] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Id [Token] -> [Id] -> [Doc]
cCommaT Map Id [Token]
m

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

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

annoLine :: String -> Doc
annoLine :: String -> Doc
annoLine w :: String
w = Doc
percent Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
keyword String
w

annoLparen :: String -> Doc
annoLparen :: String -> Doc
annoLparen w :: String
w = Doc
percent Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
keyword String
w Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
lparen

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

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

percent :: Doc
percent :: Doc
percent = String -> Doc
symbol String
percentS

annoRparen :: Doc
annoRparen :: Doc
annoRparen = Doc
rparen Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
percent

hCommaT :: Map.Map Id [Token] -> [Id] -> Doc
hCommaT :: Map Id [Token] -> [Id] -> Doc
hCommaT m :: Map Id [Token]
m = [Doc] -> Doc
hsep ([Doc] -> Doc) -> ([Id] -> [Doc]) -> [Id] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Id [Token] -> [Id] -> [Doc]
cCommaT Map Id [Token]
m

fCommaT :: Map.Map Id [Token] -> [Id] -> Doc
fCommaT :: Map Id [Token] -> [Id] -> Doc
fCommaT m :: Map Id [Token]
m = [Doc] -> Doc
fsep ([Doc] -> Doc) -> ([Id] -> [Doc]) -> [Id] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Id [Token] -> [Id] -> [Doc]
cCommaT Map Id [Token]
m

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

isLegalLabel :: String -> Bool
isLegalLabel :: String -> Bool
isLegalLabel r :: String
r = Bool -> Bool
not (String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
r) Bool -> Bool -> Bool
&& (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ( \ c :: Char
c -> Char -> Bool
isAlphaNum Char
c Bool -> Bool -> Bool
|| Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
c "_" ) String
r

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

sepByCommas :: [Doc] -> Doc
sepByCommas :: [Doc] -> Doc
sepByCommas = [Doc] -> Doc
fsep ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
comma

sepBySemis :: [Doc] -> Doc
sepBySemis :: [Doc] -> Doc
sepBySemis = [Doc] -> Doc
fsep ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
semi

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

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

parenApplArgs :: GlobalAnnos -> PrecMap -> Doc -> [Bool]
parenApplArgs :: GlobalAnnos -> PrecMap -> Doc -> [Bool]
parenApplArgs ga :: GlobalAnnos
ga precs :: PrecMap
precs origDoc :: Doc
origDoc = case Doc
origDoc of
  IdApplDoc _ _ aas :: [Doc]
aas -> [Bool] -> [Bool]
forall a. [a] -> [a]
reverse ([Bool] -> [Bool]) -> [Bool] -> [Bool]
forall a b. (a -> b) -> a -> b
$ ([Bool] -> Doc -> [Bool]) -> [Bool] -> [Doc] -> [Bool]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (GlobalAnnos -> PrecMap -> Doc -> [Bool] -> Doc -> [Bool]
parenAppl GlobalAnnos
ga PrecMap
precs Doc
origDoc) [] [Doc]
aas
  _ -> []

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

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

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

getWeight :: GlobalAnnos -> PrecMap -> Doc -> Maybe Weight
getWeight :: GlobalAnnos -> PrecMap -> Doc -> Maybe Weight
getWeight ga :: GlobalAnnos
ga precs :: PrecMap
precs d :: Doc
d = let
    m :: Map Id Int
m = PrecMap -> Map Id Int
precMap PrecMap
precs
    in case Doc
d of
    IdApplDoc _ i :: Id
i aas :: [Doc]
aas@(hd :: Doc
hd : _) ->
        let p :: Int
p = Int -> Id -> Map Id Int -> Int
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
              (if Id -> Bool
begPlace Id
i Bool -> Bool -> Bool
|| Id -> Bool
endPlace Id
i then Int -> Id -> Map Id Int -> Int
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault 0 Id
eqId Map Id Int
m
               else PrecMap -> Int
maxWeight PrecMap
precs)
              Id
i Map Id Int
m in
        if (Doc -> Maybe (Id, [Doc])) -> GlobalAnnos -> Id -> [Doc] -> Bool
forall a. SplitM a -> GlobalAnnos -> Id -> [a] -> Bool
isGenLiteral Doc -> Maybe (Id, [Doc])
splitDoc GlobalAnnos
ga Id
i [Doc]
aas then Maybe Weight
forall a. Maybe a
Nothing else
        let pars :: [Bool]
pars@(par :: Bool
par : _) = GlobalAnnos -> PrecMap -> Doc -> [Bool]
parenApplArgs GlobalAnnos
ga PrecMap
precs Doc
d
            lw :: Id
lw = case GlobalAnnos -> PrecMap -> Doc -> Maybe Weight
getWeight GlobalAnnos
ga PrecMap
precs Doc
hd of
                   Just (Weight _ _ l :: Id
l _) -> AssocEither -> GlobalAnnos -> Id -> Id -> Id
nextWeight AssocEither
ALeft GlobalAnnos
ga Id
i Id
l
                   Nothing -> Id
i
            rw :: Id
rw = case GlobalAnnos -> PrecMap -> Doc -> Maybe Weight
getWeight GlobalAnnos
ga PrecMap
precs (Doc -> Maybe Weight) -> Doc -> Maybe Weight
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall a. [a] -> a
last [Doc]
aas of
                   Just (Weight _ _ _ r :: Id
r) -> AssocEither -> GlobalAnnos -> Id -> Id -> Id
nextWeight AssocEither
ARight GlobalAnnos
ga Id
i Id
r
                   Nothing -> Id
i
            in Weight -> Maybe Weight
forall a. a -> Maybe a
Just (Weight -> Maybe Weight) -> Weight -> Maybe Weight
forall a b. (a -> b) -> a -> b
$ Int -> Id -> Id -> Id -> Weight
Weight Int
p Id
i (if Bool
par then Id
i else Id
lw)
               (Id -> Weight) -> Id -> Weight
forall a b. (a -> b) -> a -> b
$ if [Bool] -> Bool
forall a. [a] -> a
last [Bool]
pars then Id
i else Id
rw
    _ -> Maybe Weight
forall a. Maybe a
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 :: AssocMap -> Rel Id -> Id -> Id -> Bool
isDiffAssoc assocs :: AssocMap
assocs precs :: Rel Id
precs op :: Id
op arg :: Id
arg = Id -> Bool
isInfix Id
op Bool -> Bool -> Bool
&& Id -> Bool
isInfix Id
arg Bool -> Bool -> Bool
&&
            if Id
op Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
/= Id
arg then
               Id
arg Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
/= Id
applId Bool -> Bool -> Bool
&& case Rel Id -> Id -> Id -> PrecRel
precRel Rel Id
precs Id
op Id
arg of
               Lower -> Bool
False
               _ -> Bool
True
            else Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Id -> AssocMap -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Id
arg AssocMap
assocs

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

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

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

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