module Horname.Internal.SMT.Pretty where
import Data.Text (Text)
import qualified Data.Text.Lazy as Text
import Horname.Internal.SMT
import Text.PrettyPrint.Leijen.Text
dontIndent :: [Text]
dontIndent = ["+", "-", "*", "=", "<=", "<", ">=", ">"]
ppSExpr :: SExpr -> Doc
ppSExpr (IntLit i) = text . Text.pack $ show i
ppSExpr (StringLit s) = text . Text.fromStrict $ s
ppSExpr (List args'@(StringLit name:args))
| name `elem` dontIndent = parens $ hsep (map ppSExpr args')
| otherwise =
parens $ text (Text.fromStrict name) <+> align (vsep (map ppSExpr args))
ppSExpr (List args) =
parens $ align (vsep (map ppSExpr args))
ppSort :: Sort -> Doc
ppSort (Sort t) = text (Text.fromStrict t)
ppVarName :: VarName -> Doc
ppVarName (VarName t) = text (Text.fromStrict t)
ppArg :: Arg -> Doc
ppArg (Arg name sort) = parens (ppVarName name <+> ppSort sort)
ppDefineFun :: DefineFun -> Doc
ppDefineFun (DefineFun name args retType expr) =
parens $
text "define-fun" <+>
align
(vsep
[ text (Text.fromStrict name)
, parens (hsep (map ppArg args)) <+> ppSort retType
, ppSExpr expr
])