{-# 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
          -- 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 ""))
          _ -> 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))  -- XXX: Good enough?

      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)