{-# LANGUAGE Safe #-}
module SMTLib2.PP where
import Prelude hiding ((<>))
import SMTLib2.AST
import Text.PrettyPrint
import Numeric
import Data.List(genericReplicate)
class PP t where
pp :: t -> Doc
instance PP Bool where
pp :: Bool -> Doc
pp True = String -> Doc
text "true"
pp False = String -> Doc
text "false"
instance PP Integer where
pp :: Integer -> Doc
pp = Integer -> Doc
integer
ppString :: String -> Doc
ppString :: String -> Doc
ppString = String -> Doc
text (String -> Doc) -> (String -> String) -> String -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
forall a. Show a => a -> String
show
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 []) = Name -> Doc
forall t. PP t => t -> Doc
pp Name
x
pp (I x :: Name
x is :: [Integer]
is) = Doc -> Doc
parens (Char -> Doc
char '_' Doc -> Doc -> Doc
<+> Name -> Doc
forall t. PP t => t -> Doc
pp Name
x Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((Integer -> Doc) -> [Integer] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> Doc
integer [Integer]
is))
instance PP Attr where
pp :: Attr -> Doc
pp (Attr x :: Name
x v :: Maybe AttrVal
v) = Char -> Doc
char ':' Doc -> Doc -> Doc
<> Name -> Doc
forall t. PP t => t -> Doc
pp Name
x Doc -> Doc -> Doc
<+> Doc -> (AttrVal -> Doc) -> Maybe AttrVal -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
empty AttrVal -> Doc
forall t. PP t => t -> Doc
pp Maybe AttrVal
v
instance PP Quant where
pp :: Quant -> Doc
pp Forall = String -> Doc
text "forall"
pp Exists = String -> Doc
text "exists"
instance PP Expr where
pp :: AttrVal -> Doc
pp expr :: AttrVal
expr =
case AttrVal
expr of
Lit l :: Literal
l -> Literal -> Doc
forall t. PP t => t -> Doc
pp Literal
l
App c :: Ident
c ty :: Maybe Type
ty ts :: [AttrVal]
ts ->
case [AttrVal]
ts of
[] -> Doc
ppFun
_ -> Doc -> Doc
parens (Doc
ppFun Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((AttrVal -> Doc) -> [AttrVal] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map AttrVal -> Doc
forall t. PP t => t -> Doc
pp [AttrVal]
ts))
where ppFun :: Doc
ppFun = case Maybe Type
ty of
Nothing -> Ident -> Doc
forall t. PP t => t -> Doc
pp Ident
c
Just t :: Type
t -> Doc -> Doc
parens (String -> Doc
text "as" Doc -> Doc -> Doc
<+> Ident -> Doc
forall t. PP t => t -> Doc
pp Ident
c Doc -> Doc -> Doc
<+> Type -> Doc
forall t. PP t => t -> Doc
pp Type
t)
Quant q :: Quant
q bs :: [Binder]
bs e :: AttrVal
e ->
case [Binder]
bs of
[] -> AttrVal -> Doc
forall t. PP t => t -> Doc
pp AttrVal
e
_ -> Doc -> Doc
parens (Quant -> Doc
forall t. PP t => t -> Doc
pp Quant
q Doc -> Doc -> Doc
<+> Doc -> Doc
parens ([Doc] -> Doc
fsep ((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
$$ Int -> Doc -> Doc
nest 2 (AttrVal -> Doc
forall t. PP t => t -> Doc
pp AttrVal
e))
Let ds :: [Defn]
ds e :: AttrVal
e ->
case [Defn]
ds of
[] -> AttrVal -> Doc
forall t. PP t => t -> Doc
pp AttrVal
e
_ -> Doc -> Doc
parens (String -> Doc
text "let" Doc -> Doc -> Doc
<+> (Doc -> Doc
parens ([Doc] -> Doc
vcat ((Defn -> Doc) -> [Defn] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Defn -> Doc
forall t. PP t => t -> Doc
pp [Defn]
ds)) Doc -> Doc -> Doc
$$ AttrVal -> Doc
forall t. PP t => t -> Doc
pp AttrVal
e))
Annot e :: AttrVal
e as :: [Attr]
as ->
case [Attr]
as of
[] -> AttrVal -> Doc
forall t. PP t => t -> Doc
pp AttrVal
e
_ -> Doc -> Doc
parens (Char -> Doc
char '!' Doc -> Doc -> Doc
<+> AttrVal -> Doc
forall t. PP t => t -> Doc
pp AttrVal
e Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 2 ([Doc] -> Doc
vcat ((Attr -> Doc) -> [Attr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Attr -> Doc
forall t. PP t => t -> Doc
pp [Attr]
as)))
instance PP Binder where
pp :: Binder -> Doc
pp (Bind x :: Name
x t :: Type
t) = Doc -> Doc
parens (Name -> Doc
forall t. PP t => t -> Doc
pp Name
x Doc -> Doc -> Doc
<+> Type -> Doc
forall t. PP t => t -> Doc
pp Type
t)
instance PP Defn where
pp :: Defn -> Doc
pp (Defn x :: Name
x e :: AttrVal
e) = Doc -> Doc
parens (Name -> Doc
forall t. PP t => t -> Doc
pp Name
x Doc -> Doc -> Doc
<+> AttrVal -> Doc
forall t. PP t => t -> Doc
pp AttrVal
e)
instance PP Type where
pp :: Type -> Doc
pp ty :: Type
ty =
case Type
ty of
TApp c :: Ident
c ts :: [Type]
ts ->
case [Type]
ts of
[] -> Ident -> Doc
forall t. PP t => t -> Doc
pp Ident
c
_ -> Doc -> Doc
parens (Ident -> Doc
forall t. PP t => t -> Doc
pp Ident
c Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((Type -> Doc) -> [Type] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Doc
forall t. PP t => t -> Doc
pp [Type]
ts))
TVar x :: Name
x -> Name -> Doc
forall t. PP t => t -> Doc
pp Name
x
instance PP Literal where
pp :: Literal -> Doc
pp lit :: Literal
lit =
case Literal
lit of
LitBV n :: Integer
n w :: Integer
w ->
case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod Integer
w 4 of
_ -> String -> Doc
text "#b" Doc -> Doc -> Doc
<> String -> Doc
text (Integer -> String -> String
forall i. Integral i => i -> String -> String
pad Integer
w (Integer -> (Int -> Char) -> Integer -> String -> String
forall a.
(Integral a, Show a) =>
a -> (Int -> Char) -> a -> String -> String
showIntAtBase 2 (String -> Char
forall a. [a] -> a
head (String -> Char) -> (Int -> String) -> Int -> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show) Integer
v ""))
where pad :: i -> String -> String
pad digs :: i
digs xs :: String
xs = i -> Char -> String
forall i a. Integral i => i -> a -> [a]
genericReplicate
(i
digs i -> i -> i
forall a. Num a => a -> a -> a
- Int -> i
forall a b. (Integral a, Num b) => a -> b
fromIntegral (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
xs)) '0' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
xs
v :: Integer
v = if Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 0 then 2Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n else Integer
n
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
ppString String
x
instance PP Option where
pp :: Option -> Doc
pp opt :: Option
opt =
case Option
opt of
OptPrintSuccess b :: Bool
b -> String -> Bool -> Doc
forall t. PP t => String -> t -> Doc
std "print-success" Bool
b
OptExpandDefinitions b :: Bool
b -> String -> Bool -> Doc
forall t. PP t => String -> t -> Doc
std "expand-definitions" Bool
b
OptInteractiveMode b :: Bool
b -> String -> Bool -> Doc
forall t. PP t => String -> t -> Doc
std "interactive-mode" Bool
b
OptProduceProofs b :: Bool
b -> String -> Bool -> Doc
forall t. PP t => String -> t -> Doc
std "produce-proofs" Bool
b
OptProduceUnsatCores b :: Bool
b -> String -> Bool -> Doc
forall t. PP t => String -> t -> Doc
std "produce-unsat-cores" Bool
b
OptProduceModels b :: Bool
b -> String -> Bool -> Doc
forall t. PP t => String -> t -> Doc
std "produce-models" Bool
b
OptProduceAssignments b :: Bool
b -> String -> Bool -> Doc
forall t. PP t => String -> t -> Doc
std "produce-assignments" Bool
b
OptRegularOutputChannel s :: String
s -> String -> String -> Doc
str "regular-output-channel" String
s
OptDiagnosticOutputChannel s :: String
s -> String -> String -> Doc
str "diagnostic-output-channel" String
s
OptRandomSeed n :: Integer
n -> String -> Integer -> Doc
forall t. PP t => String -> t -> Doc
std "random-seed" Integer
n
OptVerbosity n :: Integer
n -> String -> Integer -> Doc
forall t. PP t => String -> t -> Doc
std "verbosity" Integer
n
OptAttr a :: Attr
a -> Attr -> Doc
forall t. PP t => t -> Doc
pp Attr
a
where mk :: String -> Doc -> Doc
mk a :: String
a b :: Doc
b = Char -> Doc
char ':' Doc -> Doc -> Doc
<> String -> Doc
text String
a Doc -> Doc -> Doc
<+> Doc
b
std :: String -> t -> Doc
std a :: String
a b :: t
b = String -> Doc -> Doc
mk String
a (t -> Doc
forall t. PP t => t -> Doc
pp t
b)
str :: String -> String -> Doc
str a :: String
a b :: String
b = String -> Doc -> Doc
mk String
a (String -> Doc
ppString String
b)
instance PP InfoFlag where
pp :: InfoFlag -> Doc
pp info :: InfoFlag
info =
case InfoFlag
info of
InfoAllStatistics -> String -> Doc
mk "all-statistics"
InfoErrorBehavior -> String -> Doc
mk "error-behavior"
InfoName -> String -> Doc
mk "name"
InfoAuthors -> String -> Doc
mk "authors"
InfoVersion -> String -> Doc
mk "version"
InfoStatus -> String -> Doc
mk "status"
InfoReasonUnknown -> String -> Doc
mk "reason-unknown"
InfoAttr a :: Attr
a -> Attr -> Doc
forall t. PP t => t -> Doc
pp Attr
a
where mk :: String -> Doc
mk x :: String
x = Char -> Doc
char ':' Doc -> Doc -> Doc
<> String -> Doc
text String
x
instance PP Command where
pp :: Command -> Doc
pp cmd :: Command
cmd =
case Command
cmd of
CmdSetLogic n :: Name
n -> String -> Name -> Doc
forall t. PP t => String -> t -> Doc
std "set-logic" Name
n
CmdSetOption o :: Option
o -> String -> Option -> Doc
forall t. PP t => String -> t -> Doc
std "set-option" Option
o
CmdSetInfo a :: Attr
a -> String -> Attr -> Doc
forall t. PP t => String -> t -> Doc
std "set-info" Attr
a
CmdDeclareType x :: Name
x n :: Integer
n -> String -> Doc -> Doc
mk "declare-sort" (Name -> Doc
forall t. PP t => t -> Doc
pp Name
x Doc -> Doc -> Doc
<+> Integer -> Doc
integer Integer
n)
CmdDefineType x :: Name
x as :: [Name]
as t :: Type
t -> String -> Name -> [Name] -> Doc -> Doc
forall t t. (PP t, PP t) => String -> t -> [t] -> Doc -> Doc
fun "define-sort" Name
x [Name]
as (Type -> Doc
forall t. PP t => t -> Doc
pp Type
t)
CmdDeclareConst x :: Name
x t :: Type
t -> String -> Doc -> Doc
mk "declare-const" (Name -> Doc
forall t. PP t => t -> Doc
pp Name
x Doc -> Doc -> Doc
<+> Type -> Doc
forall t. PP t => t -> Doc
pp Type
t)
CmdDeclareFun x :: Name
x ts :: [Type]
ts t :: Type
t -> String -> Name -> [Type] -> Doc -> Doc
forall t t. (PP t, PP t) => String -> t -> [t] -> Doc -> Doc
fun "declare-fun" Name
x [Type]
ts (Type -> Doc
forall t. PP t => t -> Doc
pp Type
t)
CmdDefineFun x :: Name
x bs :: [Binder]
bs t :: Type
t e :: AttrVal
e -> String -> Name -> [Binder] -> Doc -> Doc
forall t t. (PP t, PP t) => String -> t -> [t] -> Doc -> Doc
fun "define-fun" Name
x [Binder]
bs (Type -> Doc
forall t. PP t => t -> Doc
pp Type
t Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 2 (AttrVal -> Doc
forall t. PP t => t -> Doc
pp AttrVal
e))
CmdPush n :: Integer
n -> String -> Integer -> Doc
forall t. PP t => String -> t -> Doc
std "push" Integer
n
CmdPop n :: Integer
n -> String -> Integer -> Doc
forall t. PP t => String -> t -> Doc
std "pop" Integer
n
CmdAssert e :: AttrVal
e -> String -> AttrVal -> Doc
forall t. PP t => String -> t -> Doc
std "assert" AttrVal
e
CmdCheckSat -> String -> Doc
one "check-sat"
CmdGetAssertions -> String -> Doc
one "get-assertions"
CmdGetValue es :: [AttrVal]
es -> String -> Doc -> Doc
mk "get-value" (Doc -> Doc
parens ([Doc] -> Doc
fsep ((AttrVal -> Doc) -> [AttrVal] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map AttrVal -> Doc
forall t. PP t => t -> Doc
pp [AttrVal]
es)))
CmdGetProof -> String -> Doc
one "get-proof"
CmdGetUnsatCore -> String -> Doc
one "get-unsat-core"
CmdGetInfo i :: InfoFlag
i -> String -> InfoFlag -> Doc
forall t. PP t => String -> t -> Doc
std "get-info" InfoFlag
i
CmdGetOption n :: Name
n -> String -> Name -> Doc
forall t. PP t => String -> t -> Doc
std "get-option" Name
n
CmdComment s :: String
s -> [Doc] -> Doc
vcat ((String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
comment (String -> [String]
lines String
s))
CmdExit -> String -> Doc
one "exit"
where mk :: String -> Doc -> Doc
mk x :: String
x d :: Doc
d = Doc -> Doc
parens (String -> Doc
text String
x Doc -> Doc -> Doc
<+> Doc
d)
one :: String -> Doc
one x :: String
x = String -> Doc -> Doc
mk String
x Doc
empty
std :: String -> t -> Doc
std x :: String
x a :: t
a = String -> Doc -> Doc
mk String
x (t -> Doc
forall t. PP t => t -> Doc
pp t
a)
fun :: String -> t -> [t] -> Doc -> Doc
fun x :: String
x y :: t
y as :: [t]
as d :: Doc
d = String -> Doc -> Doc
mk String
x (t -> Doc
forall t. PP t => t -> Doc
pp t
y Doc -> Doc -> Doc
<+> Doc -> Doc
parens ([Doc] -> Doc
fsep ((t -> Doc) -> [t] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map t -> Doc
forall t. PP t => t -> Doc
pp [t]
as)) Doc -> Doc -> Doc
<+> Doc
d)
comment :: String -> Doc
comment s :: String
s = String -> Doc
text ";" Doc -> Doc -> Doc
<+> String -> Doc
text String
s
instance PP Script where
pp :: Script -> Doc
pp (Script cs :: [Command]
cs) = [Doc] -> Doc
vcat ((Command -> Doc) -> [Command] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Command -> Doc
forall t. PP t => t -> Doc
pp [Command]
cs)