{-# LANGUAGE Safe #-}
module SMTLib1.PP where

import Prelude hiding ((<>))
import SMTLib1.AST
import Text.PrettyPrint

class PP t where
  pp :: t -> Doc

instance PP Name where
  pp :: Name -> Doc
pp (N x :: String
x) = String -> Doc
text String
x

instance PP Ident where
  pp :: Ident -> Doc
pp (I x :: Name
x is :: [Integer]
is) = Name -> Doc
forall t. PP t => t -> Doc
pp Name
x Doc -> Doc -> Doc
<> case [Integer]
is of
                          [] -> Doc
empty
                          _  -> Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate (Char -> Doc
char ':')
                                                ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Integer -> Doc) -> [Integer] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> Doc
integer [Integer]
is

instance PP Quant where
  pp :: Quant -> Doc
pp Forall = String -> Doc
text "forall"
  pp Exists = String -> Doc
text "exists"

instance PP Conn where
  pp :: Conn -> Doc
pp conn :: Conn
conn =
    case Conn
conn of
      Not        -> String -> Doc
text "not"
      Implies    -> String -> Doc
text "implies"
      And        -> String -> Doc
text "and"
      Or         -> String -> Doc
text "or"
      Xor        -> String -> Doc
text "xor"
      Iff        -> String -> Doc
text "iff"
      IfThenElse -> String -> Doc
text "if_then_else"

instance PP Binder where
  pp :: Binder -> Doc
pp (Bind x :: Name
x t :: Ident
t) = Doc -> Doc
parens (Char -> Doc
char '?' Doc -> Doc -> Doc
<> Name -> Doc
forall t. PP t => t -> Doc
pp Name
x Doc -> Doc -> Doc
<+> Ident -> Doc
forall t. PP t => t -> Doc
pp Ident
t)

instance PP Formula where
  pp :: Formula -> Doc
pp form :: Formula
form =
    case Formula
form of
      FTrue       -> String -> Doc
text "true"
      FFalse      -> String -> Doc
text "false"
      FVar x :: Name
x      -> Char -> Doc
char '$' Doc -> Doc -> Doc
<> Name -> Doc
forall t. PP t => t -> Doc
pp Name
x
      FPred p :: Ident
p []  -> Ident -> Doc
forall t. PP t => t -> Doc
pp Ident
p
      _           -> Doc -> Doc
parens (Formula -> Doc
ppUnwrap Formula
form)

    where
    ppUnwrap :: Formula -> Doc
ppUnwrap form1 :: Formula
form1 =
      case Formula
form1 of
        Conn c :: Conn
c fs :: [Formula]
fs     -> Conn -> Doc
forall t. PP t => t -> Doc
pp Conn
c Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((Formula -> Doc) -> [Formula] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Formula -> Doc
forall t. PP t => t -> Doc
pp [Formula]
fs)
        Quant q :: Quant
q bs :: [Binder]
bs f :: Formula
f  ->
          case [Binder]
bs of
            [] -> Formula -> Doc
forall t. PP t => t -> Doc
pp Formula
f
            _  -> Quant -> Doc
forall t. PP t => t -> Doc
pp Quant
q Doc -> Doc -> Doc
<+> [Doc] -> Doc
sep ((Binder -> Doc) -> [Binder] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Binder -> Doc
forall t. PP t => t -> Doc
pp [Binder]
bs) Doc -> Doc -> Doc
<+> Formula -> Doc
forall t. PP t => t -> Doc
pp Formula
f
        Let x :: Name
x t :: Term
t f :: Formula
f     -> String -> Doc
text "let" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (Char -> Doc
char '?' Doc -> Doc -> Doc
<> Name -> Doc
forall t. PP t => t -> Doc
pp Name
x Doc -> Doc -> Doc
<+> Term -> Doc
forall t. PP t => t -> Doc
pp Term
t)
                      Doc -> Doc -> Doc
$$ Formula -> Doc
forall t. PP t => t -> Doc
pp Formula
f
        FLet x :: Name
x f1 :: Formula
f1 f2 :: Formula
f2  -> String -> Doc
text "flet" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (Char -> Doc
char '$' Doc -> Doc -> Doc
<> Name -> Doc
forall t. PP t => t -> Doc
pp Name
x Doc -> Doc -> Doc
<+> Formula -> Doc
forall t. PP t => t -> Doc
pp Formula
f1)
                      Doc -> Doc -> Doc
$$ Formula -> Doc
forall t. PP t => t -> Doc
pp Formula
f2
        FPred p :: Ident
p ts :: [Term]
ts    -> Ident -> Doc
forall t. PP t => t -> Doc
pp Ident
p Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((Term -> Doc) -> [Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc
forall t. PP t => t -> Doc
pp [Term]
ts)
        FAnnot f :: Formula
f as :: [Annot]
as   -> Formula -> Doc
ppUnwrap Formula
f Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 2 ([Doc] -> Doc
vcat ((Annot -> Doc) -> [Annot] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Annot -> Doc
forall t. PP t => t -> Doc
pp [Annot]
as))
        _             -> Formula -> Doc
forall t. PP t => t -> Doc
pp Formula
form1


instance PP Annot where
  pp :: Annot -> Doc
pp (Attr x :: Name
x v :: Maybe String
v) = Char -> Doc
char ':' Doc -> Doc -> Doc
<> Name -> Doc
forall t. PP t => t -> Doc
pp Name
x Doc -> Doc -> Doc
<+> Doc -> (String -> Doc) -> Maybe String -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
empty String -> Doc
ppUserValue Maybe String
v
    where
    ppUserValue :: String -> Doc
ppUserValue = Doc -> Doc
braces (Doc -> Doc) -> (String -> Doc) -> String -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc
text (String -> Doc) -> (String -> String) -> String -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> String) -> String -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
esc

    esc :: Char -> String
esc '{' = "\\{"
    esc c :: Char
c   = [Char
c]

instance PP Term where
  pp :: Term -> Doc
pp term :: Term
term =
    case Term
term of
      Var n :: Name
n     -> Char -> Doc
char '?' Doc -> Doc -> Doc
<> Name -> Doc
forall t. PP t => t -> Doc
pp Name
n
      App f :: Ident
f []  -> Ident -> Doc
forall t. PP t => t -> Doc
pp Ident
f
      Lit l :: Literal
l     -> Literal -> Doc
forall t. PP t => t -> Doc
pp Literal
l
      _         -> Doc -> Doc
parens (Term -> Doc
ppUnwrap Term
term)

    where
    ppUnwrap :: Term -> Doc
ppUnwrap term1 :: Term
term1 =
      case Term
term1 of
        App f :: Ident
f ts :: [Term]
ts    -> Ident -> Doc
forall t. PP t => t -> Doc
pp Ident
f Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((Term -> Doc) -> [Term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Doc
forall t. PP t => t -> Doc
pp [Term]
ts)
        ITE f :: Formula
f t1 :: Term
t1 t2 :: Term
t2 -> String -> Doc
text "ite" Doc -> Doc -> Doc
<+> Formula -> Doc
forall t. PP t => t -> Doc
pp Formula
f Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 2 (Term -> Doc
forall t. PP t => t -> Doc
pp Term
t1 Doc -> Doc -> Doc
$$ Term -> Doc
forall t. PP t => t -> Doc
pp Term
t2)
        TAnnot t :: Term
t as :: [Annot]
as -> Term -> Doc
ppUnwrap Term
t Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 2 ([Doc] -> Doc
vcat ((Annot -> Doc) -> [Annot] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Annot -> Doc
forall t. PP t => t -> Doc
pp [Annot]
as))
        _           -> Term -> Doc
forall t. PP t => t -> Doc
pp Term
term1


instance PP Literal where
  pp :: Literal -> Doc
pp lit :: Literal
lit =
    case Literal
lit of
      LitNum n :: Integer
n  -> Integer -> Doc
integer Integer
n
      LitFrac x :: Rational
x -> String -> Doc
text (Double -> String
forall a. Show a => a -> String
show (Rational -> Double
forall a. Fractional a => Rational -> a
fromRational Rational
x :: Double)) -- XXX: Good enough?
      LitStr x :: String
x  -> String -> Doc
text (String -> String
forall a. Show a => a -> String
show String
x)

instance PP FunDecl where
  pp :: FunDecl -> Doc
pp d :: FunDecl
d = Doc -> Doc
parens (Ident -> Doc
forall t. PP t => t -> Doc
pp (FunDecl -> Ident
funName FunDecl
d) Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((Ident -> Doc) -> [Ident] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Ident -> Doc
forall t. PP t => t -> Doc
pp (FunDecl -> [Ident]
funArgs FunDecl
d)) Doc -> Doc -> Doc
<+> Ident -> Doc
forall t. PP t => t -> Doc
pp (FunDecl -> Ident
funRes FunDecl
d)
                  Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 2 ([Doc] -> Doc
vcat ((Annot -> Doc) -> [Annot] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Annot -> Doc
forall t. PP t => t -> Doc
pp (FunDecl -> [Annot]
funAnnots FunDecl
d))))

instance PP PredDecl where
  pp :: PredDecl -> Doc
pp d :: PredDecl
d = Doc -> Doc
parens (Ident -> Doc
forall t. PP t => t -> Doc
pp (PredDecl -> Ident
predName PredDecl
d) Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((Ident -> Doc) -> [Ident] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Ident -> Doc
forall t. PP t => t -> Doc
pp (PredDecl -> [Ident]
predArgs PredDecl
d))
                  Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 2 ([Doc] -> Doc
vcat ((Annot -> Doc) -> [Annot] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Annot -> Doc
forall t. PP t => t -> Doc
pp (PredDecl -> [Annot]
predAnnots PredDecl
d))))

instance PP Status where
  pp :: Status -> Doc
pp stat :: Status
stat =
    case Status
stat of
      Sat       -> String -> Doc
text "sat"
      Unsat     -> String -> Doc
text "unsat"
      Unknown   -> String -> Doc
text "unknown"

instance PP Command where
  pp :: Command -> Doc
pp cmd :: Command
cmd =
    case Command
cmd of
      CmdLogic n :: Ident
n      -> String -> Ident -> Doc
forall t. PP t => String -> t -> Doc
std "logic" Ident
n
      CmdAssumption f :: Formula
f -> String -> Formula -> Doc
forall t. PP t => String -> t -> Doc
std "assumption" Formula
f
      CmdFormula f :: Formula
f    -> String -> Formula -> Doc
forall t. PP t => String -> t -> Doc
std "formula" Formula
f
      CmdStatus s :: Status
s     -> String -> Status -> Doc
forall t. PP t => String -> t -> Doc
std "status" Status
s
      CmdExtraSorts s :: [Ident]
s -> String -> [Ident] -> Doc
forall t. PP t => String -> [t] -> Doc
many "extrasorts" [Ident]
s
      CmdExtraFuns  f :: [FunDecl]
f -> String -> [FunDecl] -> Doc
forall t. PP t => String -> [t] -> Doc
many "extrafuns" [FunDecl]
f
      CmdExtraPreds p :: [PredDecl]
p -> String -> [PredDecl] -> Doc
forall t. PP t => String -> [t] -> Doc
many "extrapreds" [PredDecl]
p
      CmdNotes s :: String
s      -> String -> Doc -> Doc
mk "notes" (String -> Doc
forall (t :: * -> *). Foldable t => t Char -> Doc
str String
s)
      CmdAnnot a :: Annot
a      -> Annot -> Doc
forall t. PP t => t -> Doc
pp Annot
a

    where mk :: String -> Doc -> Doc
mk x :: String
x d :: Doc
d    = Char -> Doc
char ':' Doc -> Doc -> Doc
<> String -> Doc
text String
x Doc -> Doc -> Doc
<+> Doc
d

          std :: String -> t -> Doc
std x :: String
x n :: t
n   = String -> Doc -> Doc
mk String
x (t -> Doc
forall t. PP t => t -> Doc
pp t
n)

          many :: String -> [t] -> Doc
many _ [] = Doc
empty
          many x :: String
x ns :: [t]
ns = String -> Doc -> Doc
mk String
x (Doc -> Doc
parens ([Doc] -> Doc
vcat ((t -> Doc) -> [t] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map t -> Doc
forall t. PP t => t -> Doc
pp [t]
ns)))

          esc :: Char -> String
esc '"'   = "\\\""
          esc c :: Char
c     = [Char
c]

          str :: t Char -> Doc
str s :: t Char
s     = (Char -> Doc
char '"' Doc -> Doc -> Doc
<> String -> Doc
text ((Char -> String) -> t Char -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
esc t Char
s) Doc -> Doc -> Doc
<> Char -> Doc
char '"')





instance PP Script where
  pp :: Script -> Doc
pp s :: Script
s  = Doc -> Doc
parens (String -> Doc
text "benchmark" Doc -> Doc -> Doc
<+> Ident -> Doc
forall t. PP t => t -> Doc
pp (Script -> Ident
scrName Script
s)
                  Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 2 ([Doc] -> Doc
vcat ((Command -> Doc) -> [Command] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Command -> Doc
forall t. PP t => t -> Doc
pp (Script -> [Command]
scrCommands Script
s))))