module Language.Fixpoint.PrettyPrint where
import Text.PrettyPrint.HughesPJ
import Language.Fixpoint.Types
import Language.Fixpoint.Misc
import Control.Applicative ((<$>))
import Text.Parsec
import qualified Data.Text as T
class PPrint a where
pprint :: a -> Doc
showpp :: (PPrint a) => a -> String
showpp = render . pprint
instance PPrint a => PPrint (Maybe a) where
pprint = maybe (text "Nothing") ((text "Just" <+>) . pprint)
instance PPrint a => PPrint [a] where
pprint = brackets . intersperse comma . map pprint
instance (PPrint a, PPrint b, PPrint c) => PPrint (a, b, c) where
pprint (x, y, z) = parens $ (pprint x) <> text "," <> (pprint y) <> text "," <> (pprint z)
instance (PPrint a, PPrint b) => PPrint (a,b) where
pprint (x, y) = (pprint x) <+> text ":" <+> (pprint y)
instance PPrint SourcePos where
pprint = text . show
instance PPrint () where
pprint = text . show
instance PPrint String where
pprint = text
instance PPrint Int where
pprint = toFix
instance PPrint Integer where
pprint = toFix
instance PPrint Constant where
pprint = toFix
instance PPrint Brel where
pprint Eq = text "=="
pprint Ne = text "/="
pprint r = toFix r
instance PPrint Bop where
pprint = toFix
instance PPrint Sort where
pprint = toFix
instance PPrint Symbol where
pprint = toFix
instance PPrint SymConst where
pprint (SL x) = doubleQuotes $ text $ T.unpack x
instance PPrint Expr where
pprint (EApp f es) = parens $ intersperse empty $ (pprint f) : (pprint <$> es)
pprint (ESym c) = pprint c
pprint (ECon c) = pprint c
pprint (EVar s) = pprint s
pprint (ELit s _) = pprint s
pprint (EBin o e1 e2) = parens $ pprint e1 <+> pprint o <+> pprint e2
pprint (EIte p e1 e2) = parens $ text "if" <+> pprint p <+> text "then" <+> pprint e1 <+> text "else" <+> pprint e2
pprint (ECst e so) = parens $ pprint e <+> text " : " <+> pprint so
pprint (EBot) = text "_|_"
instance PPrint Pred where
pprint PTop = text "???"
pprint PTrue = trueD
pprint PFalse = falseD
pprint (PBexp e) = parens $ pprint e
pprint (PNot p) = parens $ text "not" <+> parens (pprint p)
pprint (PImp p1 p2) = parens $ (pprint p1) <+> text "=>" <+> (pprint p2)
pprint (PIff p1 p2) = parens $ (pprint p1) <+> text "<=>" <+> (pprint p2)
pprint (PAnd ps) = parens $ pprintBin trueD andD ps
pprint (POr ps) = parens $ pprintBin falseD orD ps
pprint (PAtom r e1 e2) = parens $ pprint e1 <+> pprint r <+> pprint e2
pprint (PAll xts p) = text "forall" <+> toFix xts <+> text "." <+> pprint p
trueD = text "true"
falseD = text "false"
andD = text " &&"
orD = text " ||"
pprintBin b _ [] = b
pprintBin _ o xs = intersperse o $ pprint <$> xs
instance PPrint Refa where
pprint (RConc p) = pprint p
pprint k = toFix k
instance PPrint Reft where
pprint r@(Reft (_,ras))
| isTauto r = text "true"
| otherwise = pprintBin trueD andD $ flattenRefas ras
instance PPrint SortedReft where
pprint (RR so (Reft (v, ras)))
= braces
$ (pprint v) <+> (text ":") <+> (toFix so) <+> (text "|") <+> pprint ras
instance PPrint a => PPrint (Located a) where
pprint (Loc _ x) = pprint x