{-# 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 String
x) = String -> Doc
text String
x

instance PP Ident where
  pp :: Ident -> Doc
pp (I Name
x [Integer]
is) = Name -> Doc
forall t. PP t => t -> Doc
pp Name
x Doc -> Doc -> Doc
<> case [Integer]
is of
                          [] -> Doc
empty
                          [Integer]
_  -> 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 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 Quant
Forall = String -> Doc
text String
"forall"
  pp Quant
Exists = String -> Doc
text String
"exists"

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

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

    where
    ppUnwrap :: Formula -> Doc
ppUnwrap Formula
form1 =
      case Formula
form1 of
        Conn Conn
c [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 Quant
q [Binder]
bs Formula
f  ->
          case [Binder]
bs of
            [] -> Formula -> Doc
forall t. PP t => t -> Doc
pp Formula
f
            [Binder]
_  -> 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 Name
x Term
t Formula
f     -> String -> Doc
text String
"let" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (Char -> Doc
char 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 Name
x Formula
f1 Formula
f2  -> String -> Doc
text String
"flet" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (Char -> Doc
char 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 Ident
p [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 Formula
f [Annot]
as   -> Formula -> Doc
ppUnwrap Formula
f Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
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
_             -> Formula -> Doc
forall t. PP t => t -> Doc
pp Formula
form1


instance PP Annot where
  pp :: Annot -> Doc
pp (Attr Name
x Maybe String
v) = Char -> Doc
char 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 Char
'{' = String
"\\{"
    esc Char
c   = [Char
c]

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

    where
    ppUnwrap :: Term -> Doc
ppUnwrap Term
term1 =
      case Term
term1 of
        App Ident
f [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 Formula
f Term
t1 Term
t2 -> String -> Doc
text String
"ite" Doc -> Doc -> Doc
<+> Formula -> Doc
forall t. PP t => t -> Doc
pp Formula
f Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
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 Term
t [Annot]
as -> Term -> Doc
ppUnwrap Term
t Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
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
_           -> Term -> Doc
forall t. PP t => t -> Doc
pp Term
term1


instance PP Literal where
  pp :: Literal -> Doc
pp Literal
lit =
    case Literal
lit of
      LitNum Integer
n  -> Integer -> Doc
integer Integer
n
      LitFrac 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 String
x  -> String -> Doc
text (String -> String
forall a. Show a => a -> String
show String
x)

instance PP FunDecl where
  pp :: FunDecl -> Doc
pp 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 Int
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 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 Int
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 Status
stat =
    case Status
stat of
      Status
Sat       -> String -> Doc
text String
"sat"
      Status
Unsat     -> String -> Doc
text String
"unsat"
      Status
Unknown   -> String -> Doc
text String
"unknown"

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

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

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

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

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

          str :: t Char -> Doc
str t Char
s     = (Char -> Doc
char 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 Char
'"')





instance PP Script where
  pp :: Script -> Doc
pp Script
s  = Doc -> Doc
parens (String -> Doc
text String
"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 Int
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))))