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