module Theory.Text.Pretty (
module Text.PrettyPrint.Highlight
, vsep
, fsepList
, lineComment
, multiComment
, lineComment_
, multiComment_
, kwTheoryHeader
, kwEnd
, kwModulo
, kwBy
, kwCase
, kwNext
, kwQED
, kwLemma
, kwAxiom
, kwRuleModulo
, kwInstanceModulo
, kwVariantsModulo
, kwTypesModulo
, opProvides
, opRequires
, opAction
, opPath
, opLess
, opEqual
, opDedBefore
, opEdge
, opExists
, opForall
, opLAnd
, opLOr
, opImp
, opIff
, opDot
) where
import Text.PrettyPrint.Highlight
vsep :: Document d => [d] -> d
vsep = foldr ($--$) emptyDoc
fsepList :: Document d => (a -> d) -> [a] -> d
fsepList pp = fsep . punctuate comma . map pp
lineComment :: HighlightDocument d => d -> d
lineComment d = comment $ text "//" <-> d
lineComment_ :: HighlightDocument d => String -> d
lineComment_ = lineComment . text
multiComment :: HighlightDocument d => d -> d
multiComment d = comment $ fsep [text "/*", d, text "*/"]
multiComment_ :: HighlightDocument d => [String] -> d
multiComment_ ls = comment $ fsep [text "/*", vcat $ map text ls, text "*/"]
kwTheoryHeader :: HighlightDocument d => d -> d
kwTheoryHeader name = keyword_ "theory" <-> name <-> keyword_ "begin"
kwEnd, kwBy, kwCase, kwNext, kwQED, kwAxiom, kwLemma :: HighlightDocument d => d
kwEnd = keyword_ "end"
kwBy = keyword_ "by"
kwCase = keyword_ "case"
kwNext = keyword_ "next"
kwQED = keyword_ "qed"
kwAxiom = keyword_ "axiom"
kwLemma = keyword_ "lemma"
kwModulo :: HighlightDocument d
=> String
-> String
-> d
kwModulo what thy = keyword_ what <-> parens (keyword_ "modulo" <-> text thy)
kwRuleModulo, kwInstanceModulo, kwTypesModulo, kwVariantsModulo
:: HighlightDocument d => String -> d
kwRuleModulo = kwModulo "rule"
kwInstanceModulo = kwModulo "instance"
kwTypesModulo = kwModulo "type assertions"
kwVariantsModulo = kwModulo "variants"
opProvides, opRequires, opAction, opPath, opLess, opEqual, opDedBefore, opEdge,
opExists, opForall, opLAnd, opLOr, opImp, opIff, opDot
:: HighlightDocument d => d
opProvides = operator_ ":>"
opRequires = operator_ "<:"
opAction = operator_ "@"
opPath = operator_ ">+>"
opLess = operator_ "<"
opEqual = operator_ "="
opDedBefore = operator_ "--|"
opEdge = operator_ ">->"
opExists = operator_ "∃ "
opForall = operator_ "∀ "
opLAnd = operator_ "∧"
opLOr = operator_ "∨"
opImp = operator_ "⇒"
opIff = operator_ "⇔"
opDot = operator_ "."