{-# 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))
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))))