{-# LANGUAGE Rank2Types #-}
module Twee.Pretty(module Twee.Pretty, module Text.PrettyPrint.HughesPJClass, Pretty(..)) where
import Text.PrettyPrint.HughesPJClass hiding (empty, (<>))
import qualified Text.PrettyPrint.HughesPJClass as PP
import qualified Data.Map as Map
import Data.Map(Map)
import qualified Data.Set as Set
import Data.Set(Set)
import Data.Ratio
import Twee.Term
prettyPrint :: Pretty a => a -> IO ()
prettyPrint x = putStrLn (prettyShow x)
infixl 6 <#>
(<#>) :: Doc -> Doc -> Doc
(<#>) = (PP.<>)
pPrintEmpty :: Doc
pPrintEmpty = PP.empty
instance Pretty Doc where pPrint = id
pPrintTuple :: [Doc] -> Doc
pPrintTuple = parens . fsep . punctuate comma
instance Pretty a => Pretty (Set a) where
pPrint = pPrintSet . map pPrint . Set.toList
pPrintSet :: [Doc] -> Doc
pPrintSet = braces . fsep . punctuate comma
instance Pretty Var where
pPrint (V n) =
text $
vars !! (n `mod` length vars):
case n `div` length vars of
0 -> ""
m -> show (m+1)
where
vars = "XYZWVUTS"
instance (Pretty k, Pretty v) => Pretty (Map k v) where
pPrint = pPrintSet . map binding . Map.toList
where
binding (x, v) = hang (pPrint x <+> text "=>") 2 (pPrint v)
instance (Eq a, Integral a, Pretty a) => Pretty (Ratio a) where
pPrint a
| denominator a == 1 = pPrint (numerator a)
| otherwise = text "(" <+> pPrint (numerator a) <#> text "/" <#> pPrint (denominator a) <+> text ")"
supply :: [String] -> [String]
supply names =
names ++
[ name ++ show i | i <- [2..], name <- names ]
instance Pretty f => Pretty (Fun f) where
pPrintPrec l p = pPrintPrec l p . fun_value
instance PrettyTerm f => PrettyTerm (Fun f) where
termStyle f = termStyle (fun_value f)
instance PrettyTerm f => Pretty (Term f) where
pPrintPrec l p (Var x) = pPrintPrec l p x
pPrintPrec l p (App f xs) =
pPrintTerm (termStyle f) l p (pPrint f) (unpack xs)
instance PrettyTerm f => Pretty (TermList f) where
pPrintPrec _ _ = pPrint . unpack
instance PrettyTerm f => Pretty (Subst f) where
pPrint sub = text "{" <#> fsep (punctuate (text ",") docs) <#> text "}"
where
docs =
[ hang (pPrint x <+> text "->") 2 (pPrint t)
| (x, t) <- substToList sub ]
class Pretty f => PrettyTerm f where
termStyle :: f -> TermStyle
termStyle _ = curried
newtype TermStyle =
TermStyle {
pPrintTerm :: forall a. Pretty a => PrettyLevel -> Rational -> Doc -> [a] -> Doc }
invisible, curried, uncurried, prefix, postfix :: TermStyle
invisible =
TermStyle $ \l p d ->
let
f [] = d
f [t] = pPrintPrec l p t
f (t:ts) =
maybeParens (p > 10) $
pPrint t <+>
(hsep (map (pPrintPrec l 11) ts))
in f
curried =
TermStyle $ \l p d ->
let
f [] = d
f xs =
maybeParens (p > 10) $
d <+>
(hsep (map (pPrintPrec l 11) xs))
in f
uncurried =
TermStyle $ \l _ d ->
let
f [] = d
f xs =
d <#> parens (hsep (punctuate comma (map (pPrintPrec l 0) xs)))
in f
fixedArity :: Int -> TermStyle -> TermStyle
fixedArity arity style =
TermStyle $ \l p d ->
let
f xs
| length xs < arity = pPrintTerm curried l p (parens d) xs
| length xs > arity =
maybeParens (p > 10) $
hsep (pPrintTerm style l 11 d ys:
map (pPrintPrec l 11) zs)
| otherwise = pPrintTerm style l p d xs
where
(ys, zs) = splitAt arity xs
in f
implicitArguments :: Int -> TermStyle -> TermStyle
implicitArguments n (TermStyle pp) =
TermStyle $ \l p d xs -> pp l p d (drop n xs)
prefix =
fixedArity 1 $
TermStyle $ \l _ d [x] ->
d <#> pPrintPrec l 11 x
postfix =
fixedArity 1 $
TermStyle $ \l _ d [x] ->
pPrintPrec l 11 x <#> d
infixStyle :: Int -> TermStyle
infixStyle pOp =
fixedArity 2 $
TermStyle $ \l p d [x, y] ->
maybeParens (p > fromIntegral pOp) $
pPrintPrec l (fromIntegral pOp+1) x <+> d <+>
pPrintPrec l (fromIntegral pOp+1) y
tupleStyle :: TermStyle
tupleStyle =
TermStyle $ \l _ _ xs ->
parens (hsep (punctuate comma (map (pPrintPrec l 0) xs)))