{-# 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 Bool
True   = String -> Doc
text String
"true"
  pp Bool
False  = String -> Doc
text String
"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 String
x) = String -> Doc
text String
x

instance PP Ident where
  pp :: Ident -> Doc
pp (I Name
x []) = Name -> Doc
forall t. PP t => t -> Doc
pp Name
x
  pp (I Name
x [Integer]
is) = Doc -> Doc
parens (Char -> Doc
char 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 Name
x Maybe AttrVal
v) = Char -> Doc
char 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 Quant
Forall = String -> Doc
text String
"forall"
  pp Quant
Exists = String -> Doc
text String
"exists"

instance PP Expr where
  pp :: AttrVal -> Doc
pp AttrVal
expr =
    case AttrVal
expr of

      Lit Literal
l     -> Literal -> Doc
forall t. PP t => t -> Doc
pp Literal
l

      App Ident
c Maybe Type
ty [AttrVal]
ts  ->
        case [AttrVal]
ts of
          [] -> Doc
ppFun
          [AttrVal]
_  -> 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
                        Maybe Type
Nothing -> Ident -> Doc
forall t. PP t => t -> Doc
pp Ident
c
                        Just Type
t  -> Doc -> Doc
parens (String -> Doc
text String
"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 Quant
q [Binder]
bs AttrVal
e ->
        case [Binder]
bs of
          [] -> AttrVal -> Doc
forall t. PP t => t -> Doc
pp AttrVal
e
          [Binder]
_  -> 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 Int
2 (AttrVal -> Doc
forall t. PP t => t -> Doc
pp AttrVal
e))

      Let [Defn]
ds AttrVal
e ->
        case [Defn]
ds of
          [] -> AttrVal -> Doc
forall t. PP t => t -> Doc
pp AttrVal
e
          [Defn]
_  -> Doc -> Doc
parens (String -> Doc
text String
"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 AttrVal
e [Attr]
as ->
        case [Attr]
as of
          [] -> AttrVal -> Doc
forall t. PP t => t -> Doc
pp AttrVal
e
          [Attr]
_  -> Doc -> Doc
parens (Char -> Doc
char Char
'!' Doc -> Doc -> Doc
<+> AttrVal -> Doc
forall t. PP t => t -> Doc
pp AttrVal
e Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
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 Name
x 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 Name
x 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 Type
ty =
    case Type
ty of
      TApp Ident
c [Type]
ts ->
        case [Type]
ts of
          [] -> Ident -> Doc
forall t. PP t => t -> Doc
pp Ident
c
          [Type]
_  -> 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 Name
x -> Name -> Doc
forall t. PP t => t -> Doc
pp Name
x

instance PP Literal where
  pp :: Literal -> Doc
pp Literal
lit =
    case Literal
lit of

      LitBV Integer
n Integer
w ->
        case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod Integer
w Integer
4 of
          -- For the moment we do not print using HEX literals as
          -- some solvers do not support them (how hard is that???)
          -- (x,0) -> text "#x" <> text (pad x (showHex v ""))
          (Integer, Integer)
_ -> String -> Doc
text String
"#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 => a -> (Int -> Char) -> a -> String -> String
showIntAtBase Integer
2 (String -> Char
forall a. HasCallStack => [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 String
""))

        where pad :: i -> String -> String
pad i
digs 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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
xs)) Char
'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
< Integer
0 then Integer
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 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
ppString String
x



instance PP Option where
  pp :: Option -> Doc
pp Option
opt =
    case Option
opt of
      OptPrintSuccess Bool
b             -> String -> Bool -> Doc
forall {t}. PP t => String -> t -> Doc
std String
"print-success" Bool
b
      OptExpandDefinitions Bool
b        -> String -> Bool -> Doc
forall {t}. PP t => String -> t -> Doc
std String
"expand-definitions" Bool
b
      OptInteractiveMode Bool
b          -> String -> Bool -> Doc
forall {t}. PP t => String -> t -> Doc
std String
"interactive-mode" Bool
b
      OptProduceProofs Bool
b            -> String -> Bool -> Doc
forall {t}. PP t => String -> t -> Doc
std String
"produce-proofs" Bool
b
      OptProduceUnsatCores Bool
b        -> String -> Bool -> Doc
forall {t}. PP t => String -> t -> Doc
std String
"produce-unsat-cores" Bool
b
      OptProduceModels Bool
b            -> String -> Bool -> Doc
forall {t}. PP t => String -> t -> Doc
std String
"produce-models" Bool
b
      OptProduceAssignments Bool
b       -> String -> Bool -> Doc
forall {t}. PP t => String -> t -> Doc
std String
"produce-assignments" Bool
b
      OptRegularOutputChannel String
s     -> String -> String -> Doc
str String
"regular-output-channel" String
s
      OptDiagnosticOutputChannel String
s  -> String -> String -> Doc
str String
"diagnostic-output-channel" String
s
      OptRandomSeed Integer
n               -> String -> Integer -> Doc
forall {t}. PP t => String -> t -> Doc
std String
"random-seed" Integer
n
      OptVerbosity Integer
n                -> String -> Integer -> Doc
forall {t}. PP t => String -> t -> Doc
std String
"verbosity" Integer
n
      OptAttr Attr
a                     -> Attr -> Doc
forall t. PP t => t -> Doc
pp Attr
a

    where mk :: String -> Doc -> Doc
mk String
a Doc
b  = Char -> Doc
char Char
':' Doc -> Doc -> Doc
<> String -> Doc
text String
a Doc -> Doc -> Doc
<+> Doc
b
          std :: String -> t -> Doc
std String
a t
b = String -> Doc -> Doc
mk String
a (t -> Doc
forall t. PP t => t -> Doc
pp t
b)
          str :: String -> String -> Doc
str String
a String
b = String -> Doc -> Doc
mk String
a (String -> Doc
ppString String
b)

instance PP InfoFlag where
  pp :: InfoFlag -> Doc
pp InfoFlag
info =
    case InfoFlag
info of
      InfoFlag
InfoAllStatistics -> String -> Doc
mk String
"all-statistics"
      InfoFlag
InfoErrorBehavior -> String -> Doc
mk String
"error-behavior"
      InfoFlag
InfoName          -> String -> Doc
mk String
"name"
      InfoFlag
InfoAuthors       -> String -> Doc
mk String
"authors"
      InfoFlag
InfoVersion       -> String -> Doc
mk String
"version"
      InfoFlag
InfoStatus        -> String -> Doc
mk String
"status"
      InfoFlag
InfoReasonUnknown -> String -> Doc
mk String
"reason-unknown"
      InfoAttr Attr
a        -> Attr -> Doc
forall t. PP t => t -> Doc
pp Attr
a
    where mk :: String -> Doc
mk String
x = Char -> Doc
char Char
':' Doc -> Doc -> Doc
<> String -> Doc
text String
x

instance PP Command where
  pp :: Command -> Doc
pp Command
cmd =
    case Command
cmd of
      CmdSetLogic Name
n     -> String -> Name -> Doc
forall {t}. PP t => String -> t -> Doc
std String
"set-logic" Name
n
      CmdSetOption Option
o    -> String -> Option -> Doc
forall {t}. PP t => String -> t -> Doc
std String
"set-option" Option
o
      CmdSetInfo Attr
a      -> String -> Attr -> Doc
forall {t}. PP t => String -> t -> Doc
std String
"set-info" Attr
a
      CmdDeclareType Name
x Integer
n    -> String -> Doc -> Doc
mk String
"declare-sort" (Name -> Doc
forall t. PP t => t -> Doc
pp Name
x Doc -> Doc -> Doc
<+> Integer -> Doc
integer Integer
n)
      CmdDefineType Name
x [Name]
as Type
t  -> String -> Name -> [Name] -> Doc -> Doc
forall {t} {a}. (PP t, PP a) => String -> t -> [a] -> Doc -> Doc
fun String
"define-sort" Name
x [Name]
as (Type -> Doc
forall t. PP t => t -> Doc
pp Type
t)
      CmdDeclareConst Name
x Type
t   -> String -> Doc -> Doc
mk String
"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 Name
x [Type]
ts Type
t  -> String -> Name -> [Type] -> Doc -> Doc
forall {t} {a}. (PP t, PP a) => String -> t -> [a] -> Doc -> Doc
fun String
"declare-fun" Name
x [Type]
ts (Type -> Doc
forall t. PP t => t -> Doc
pp Type
t)
      CmdDefineFun Name
x [Binder]
bs Type
t AttrVal
e -> String -> Name -> [Binder] -> Doc -> Doc
forall {t} {a}. (PP t, PP a) => String -> t -> [a] -> Doc -> Doc
fun String
"define-fun" Name
x [Binder]
bs (Type -> Doc
forall t. PP t => t -> Doc
pp Type
t Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 (AttrVal -> Doc
forall t. PP t => t -> Doc
pp AttrVal
e))
      CmdPush Integer
n         -> String -> Integer -> Doc
forall {t}. PP t => String -> t -> Doc
std String
"push" Integer
n
      CmdPop Integer
n          -> String -> Integer -> Doc
forall {t}. PP t => String -> t -> Doc
std String
"pop" Integer
n
      CmdAssert AttrVal
e       -> String -> AttrVal -> Doc
forall {t}. PP t => String -> t -> Doc
std String
"assert" AttrVal
e
      Command
CmdCheckSat       -> String -> Doc
one String
"check-sat"
      Command
CmdGetAssertions  -> String -> Doc
one String
"get-assertions"
      CmdGetValue [AttrVal]
es    -> String -> Doc -> Doc
mk  String
"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)))
      Command
CmdGetProof       -> String -> Doc
one String
"get-proof"
      Command
CmdGetUnsatCore   -> String -> Doc
one String
"get-unsat-core"
      CmdGetInfo InfoFlag
i      -> String -> InfoFlag -> Doc
forall {t}. PP t => String -> t -> Doc
std String
"get-info" InfoFlag
i
      CmdGetOption Name
n    -> String -> Name -> Doc
forall {t}. PP t => String -> t -> Doc
std String
"get-option" Name
n
      CmdComment 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))
      Command
CmdExit           -> String -> Doc
one String
"exit"
    where mk :: String -> Doc -> Doc
mk String
x Doc
d = Doc -> Doc
parens (String -> Doc
text String
x Doc -> Doc -> Doc
<+> Doc
d)
          one :: String -> Doc
one String
x   = String -> Doc -> Doc
mk String
x Doc
empty
          std :: String -> t -> Doc
std String
x t
a = String -> Doc -> Doc
mk String
x (t -> Doc
forall t. PP t => t -> Doc
pp t
a)
          fun :: String -> t -> [a] -> Doc -> Doc
fun String
x t
y [a]
as 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 ((a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall t. PP t => t -> Doc
pp [a]
as)) Doc -> Doc -> Doc
<+> Doc
d)
          comment :: String -> Doc
comment String
s = String -> Doc
text String
";" Doc -> Doc -> Doc
<+> String -> Doc
text String
s

instance PP Script where
  pp :: Script -> Doc
pp (Script [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)