    {-# 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 String
    x) = String -> Doc
    text String
    x

    instance PP Ident where
      pp :: Ident -> Doc
    pp (I Name
    x [Integer]
    is) = Name -> Doc
    forall t. PP t => t -> Doc
    pp Name
    x Doc -> Doc -> Doc
    <> case [Integer]
    is of
                              [] -> Doc
    empty
                              [Integer]
    _  -> 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 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 Quant
    Forall = String -> Doc
    text String
    "forall"
      pp Quant
    Exists = String -> Doc
    text String
    "exists"

    instance PP Conn where
      pp :: Conn -> Doc
    pp Conn
    conn =
        case Conn
    conn of
          Conn
    Not        -> String -> Doc
    text String
    "not"
          Conn
    Implies    -> String -> Doc
    text String
    "implies"
          Conn
    And        -> String -> Doc
    text String
    "and"
          Conn
    Or         -> String -> Doc
    text String
    "or"
          Conn
    Xor        -> String -> Doc
    text String
    "xor"
          Conn
    Iff        -> String -> Doc
    text String
    "iff"
          Conn
    IfThenElse -> String -> Doc
    text String
    "if_then_else"

    instance PP Binder where
      pp :: Binder -> Doc
    pp (Bind Name
    x Ident
    t) = Doc -> Doc
    parens (Char -> Doc
    char 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 Formula
    form =
        case Formula
    form of
          Formula
    FTrue       -> String -> Doc
    text String
    "true"
          Formula
    FFalse      -> String -> Doc
    text String
    "false"
          FVar Name
    x      -> Char -> Doc
    char Char
    '$' Doc -> Doc -> Doc
    <> Name -> Doc
    forall t. PP t => t -> Doc
    pp Name
    x
          FPred Ident
    p []  -> Ident -> Doc
    forall t. PP t => t -> Doc
    pp Ident
    p
          Formula
    _           -> Doc -> Doc
    parens (Formula -> Doc
    ppUnwrap Formula
    form)

        where
        ppUnwrap :: Formula -> Doc
    ppUnwrap Formula
    form1 =
          case Formula
    form1 of
            Conn Conn
    c [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 Quant
    q [Binder]
    bs Formula
    f  ->
              case [Binder]
    bs of
                [] -> Formula -> Doc
    forall t. PP t => t -> Doc
    pp Formula
    f
                [Binder]
    _  -> 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 Name
    x Term
    t Formula
    f     -> String -> Doc
    text String
    "let" Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens (Char -> Doc
    char 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 Name
    x Formula
    f1 Formula
    f2  -> String -> Doc
    text String
    "flet" Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens (Char -> Doc
    char 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 Ident
    p [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 Formula
    f [Annot]
    as   -> Formula -> Doc
    ppUnwrap Formula
    f Doc -> Doc -> Doc
    $$ Int -> Doc -> Doc
    nest Int
    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
    _             -> Formula -> Doc
    forall t. PP t => t -> Doc
    pp Formula
    form1

    instance PP Annot where
      pp :: Annot -> Doc
    pp (Attr Name
    x Maybe String
    v) = Char -> Doc
    char 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 Char
    '{' = String
    "\\{"
        esc Char
    c   = [Char
    c]

    instance PP Term where
      pp :: Term -> Doc
    pp Term
    term =
        case Term
    term of
          Var Name
    n     -> Char -> Doc
    char Char
    '?' Doc -> Doc -> Doc
    <> Name -> Doc
    forall t. PP t => t -> Doc
    pp Name
    n
          App Ident
    f []  -> Ident -> Doc
    forall t. PP t => t -> Doc
    pp Ident
    f
          Lit Literal
    l     -> Literal -> Doc
    forall t. PP t => t -> Doc
    pp Literal
    l
          Term
    _         -> Doc -> Doc
    parens (Term -> Doc
    ppUnwrap Term
    term)

        where
        ppUnwrap :: Term -> Doc
    ppUnwrap Term
    term1 =
          case Term
    term1 of
            App Ident
    f [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 Formula
    f Term
    t1 Term
    t2 -> String -> Doc
    text String
    "ite" Doc -> Doc -> Doc
    <+> Formula -> Doc
    forall t. PP t => t -> Doc
    pp Formula
    f Doc -> Doc -> Doc
    $$ Int -> Doc -> Doc
    nest Int
    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 Term
    t [Annot]
    as -> Term -> Doc
    ppUnwrap Term
    t Doc -> Doc -> Doc
    $$ Int -> Doc -> Doc
    nest Int
    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
    _           -> Term -> Doc
    forall t. PP t => t -> Doc
    pp Term
    term1

    instance PP Literal where
      pp :: Literal -> Doc
    pp Literal
    lit =
        case Literal
    lit of
          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
    text (String -> String
    forall a. Show a => a -> String
    show String
    x)

    instance PP FunDecl where
      pp :: FunDecl -> Doc
    pp 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 Int
    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 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 Int
    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 Status
    stat =
        case Status
    stat of
          Status
    Sat       -> String -> Doc
    text String
    "sat"
          Status
    Unsat     -> String -> Doc
    text String
    "unsat"
          Status
    Unknown   -> String -> Doc
    text String
    "unknown"

    instance PP Command where
      pp :: Command -> Doc
    pp Command
    cmd =
        case Command
    cmd of
          CmdLogic Ident
    n      -> String -> Ident -> Doc
    forall {t}. PP t => String -> t -> Doc
    std String
    "logic" Ident
    n
          CmdAssumption Formula
    f -> String -> Formula -> Doc
    forall {t}. PP t => String -> t -> Doc
    std String
    "assumption" Formula
    f
          CmdFormula Formula
    f    -> String -> Formula -> Doc
    forall {t}. PP t => String -> t -> Doc
    std String
    "formula" Formula
    f
          CmdStatus Status
    s     -> String -> Status -> Doc
    forall {t}. PP t => String -> t -> Doc
    std String
    "status" Status
    s
          CmdExtraSorts [Ident]
    s -> String -> [Ident] -> Doc
    forall {a}. PP a => String -> [a] -> Doc
    many String
    "extrasorts" [Ident]
    s
          CmdExtraFuns  [FunDecl]
    f -> String -> [FunDecl] -> Doc
    forall {a}. PP a => String -> [a] -> Doc
    many String
    "extrafuns" [FunDecl]
    f
          CmdExtraPreds [PredDecl]
    p -> String -> [PredDecl] -> Doc
    forall {a}. PP a => String -> [a] -> Doc
    many String
    "extrapreds" [PredDecl]
    p
          CmdNotes String
    s      -> String -> Doc -> Doc
    mk String
    "notes" (String -> Doc
    forall {t :: * -> *}. Foldable t => t Char -> Doc
    str String
    s)
          CmdAnnot Annot
    a      -> Annot -> Doc
    forall t. PP t => t -> Doc
    pp Annot
    a

        where mk :: String -> Doc -> Doc
    mk String
    x Doc
    d    = Char -> Doc
    char Char
    ':' Doc -> Doc -> Doc
    <> String -> Doc
    text String
    x Doc -> Doc -> Doc
    <+> Doc
    d

              std :: String -> t -> Doc
    std String
    x t
    n   = String -> Doc -> Doc
    mk String
    x (t -> Doc
    forall t. PP t => t -> Doc
    pp t
    n)

              many :: String -> [a] -> Doc
    many String
    _ [] = Doc
    empty
              many String
    x [a]
    ns = String -> Doc -> Doc
    mk String
    x (Doc -> Doc
    parens ([Doc] -> Doc
    vcat ((a -> Doc) -> [a] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Doc
    forall t. PP t => t -> Doc
    pp [a]
    ns)))

              esc :: Char -> String
    esc Char
    '"'   = String
    "\\\""
              esc Char
    c     = [Char
    c]

              str :: t Char -> Doc
    str t Char
    s     = (Char -> Doc
    char 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 Char
    '"')

    instance PP Script where
      pp :: Script -> Doc
    pp Script
    s  = Doc -> Doc
    parens (String -> Doc
    text String
    "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 Int
    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))))