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