Switch from ansi-wl-pprint to the prettyprinter package.

This patch converts packages `what4`, `what4-abc`, and `what4-blt`.

what4-abc/src/What4/Solver/ABC.hs

@@ -70,11 +70,11 @@ import qualified Data.Set as Set
 import qualified Data.Text as T
 import           Foreign.C.Types
 import           Numeric.Natural
+import           Prettyprinter
 import           System.Directory
 import           System.IO
 import qualified System.IO.Streams as Streams
 import           System.Process
-import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
 
 import           What4.BaseTypes
 import           What4.Concrete
@@ -108,7 +108,7 @@ abcQbfIterations = configOption BaseIntegerRepr "abc.qbf_max_iterations"
 abcOptions :: [ConfigDesc]
 abcOptions =
   [ opt abcQbfIterations (ConcreteInteger (toInteger (maxBound :: CInt)))
-    (text "Max number of iterations to run ABC's QBF solver")
+    ("Max number of iterations to run ABC's QBF solver" :: T.Text)
   ]
 
 abcAdapter :: SolverAdapter st
@@ -132,7 +132,7 @@ satCommand = configOption knownRepr "sat_command"
 genericSatOptions :: [ConfigDesc]
 genericSatOptions =
   [ opt satCommand (ConcreteString "glucose $1")
-    (text "Generic SAT solving command to run")
+    ("Generic SAT solving command to run" :: T.Text)
   ]
 
 genericSatAdapter :: SolverAdapter st
@@ -249,16 +249,20 @@ eval' ntk e = do
 
 failAt :: ProgramLoc -> String -> IO a
 failAt l msg = fail $ show $
-   text msg <$$>
-   text "From term created at" <+> pretty (plSourceLoc l)
+  vcat
+  [ text msg
+  , text "From term created at" <+> pretty (plSourceLoc l)
+  ]
 
 failTerm :: Expr t tp -> String -> IO a
 failTerm e nm = do
   fail $ show $
-    text "The" <+> text nm <+> text "created at"
+    vcat
+    [ text "The" <+> text nm <+> text "created at"
          <+> pretty (plSourceLoc (exprLoc e))
-         <+> text "is not supported by ABC:" <$$>
-    indent 2 (ppExpr e)
+         <+> text "is not supported by ABC:"
+    , indent 2 (ppExpr e)
+    ]
 
 bitblastPred :: Network t s -> NonceAppExpr t tp -> IO (NameType s tp)
 bitblastPred h e = do
@@ -731,8 +735,10 @@ checkSupportedByAbc vars = do
   let errors = Fold.toList (vars^.varErrors)
   -- Check no errors where reported in result.
   when (not (null errors)) $ do
-    fail $ show $ text "This formula is not supported by abc:" <$$>
-                  indent 2 (vcat errors)
+    fail $ show $ vcat
+      [ text "This formula is not supported by abc:"
+      , indent 2 (vcat errors)
+      ]
 
 checkNoLatches :: MonadFail m => CollectedVarInfo t -> m ()
 checkNoLatches vars = do
@@ -1039,3 +1045,6 @@ getInputCount ntk = GIA.inputCount (gia ntk)
 -- | Return number of outputs so far in network.
 getOutputCount :: Network t s -> IO Int
 getOutputCount ntk = length <$> readIORef (revOutputs ntk)
+
+text :: String -> Doc ann
+text = pretty

what4-abc/what4-abc.cabal

@@ -20,7 +20,6 @@ library
     base >= 4.7 && < 4.15,
     aig,
     abcBridge >= 0.11,
-    ansi-wl-pprint,
     bv-sized >= 1.0.0,
     containers,
     what4 >= 0.4,
@@ -29,6 +28,7 @@ library
     lens,
     mtl,
     parameterized-utils,
+    prettyprinter >= 1.7.0,
     process,
     text,
     transformers,

what4-blt/src/What4/Solver/BLT.hs

@@ -77,7 +77,7 @@ import qualified Data.Text as T
 import           Data.Traversable
 import           Data.Typeable
 import           System.IO (hPutStrLn, stderr)
-import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
+import           Prettyprinter
 
 import qualified Data.Parameterized.HashTable as PH
 import           Data.Parameterized.Nonce
@@ -106,7 +106,7 @@ bltParams = configOption knownRepr "blt_params"
 bltOptions :: [ConfigDesc]
 bltOptions =
   [ opt         bltParams         (ConcreteString (UnicodeLiteral ""))
-    (text "Command-line parameters to send to BLT")
+    ("Command-line parameters to send to BLT" :: T.Text)
   ]
 
 bltAdapter :: SolverAdapter t
@@ -415,8 +415,10 @@ assume h (NonceAppExpr (nonceExprApp -> Annotation _ _ x)) =
   assume h x
 assume _ (NonceAppExpr e) =
   fail . show $
-    text "Unsupported term created at" <+> pretty (plSourceLoc l) <>
-    text ":" <$$> indent 2 (pretty (NonceAppExpr e))
+  vcat
+  [ "Unsupported term created at" <+> pretty (plSourceLoc l) <> ":"
+  , indent 2 (pretty (NonceAppExpr e))
+  ]
   where
   l = nonceExprLoc e
 assume h (BoolExpr b l)
@@ -447,9 +449,11 @@ assume h b@(AppExpr ba) =
         appLEq x' y'
       _ -> unsupported
   where
-  unsupported = fail $ show $
-        text "Unsupported term created at" <+> pretty (plSourceLoc l) <>
-        text ":" <$$> indent 2 (pretty b)
+  unsupported =
+    fail $ show $ vcat
+    [ "Unsupported term created at" <+> pretty (plSourceLoc l) <> ":"
+    , indent 2 (pretty b)
+    ]
   l = appExprLoc ba
   appLEq lhs rhs =
     let (lhs', rhs') = normalizeLEQ lhs rhs in

what4-blt/what4-blt.cabal

@@ -18,12 +18,12 @@ Description:
 library
   build-depends:
     base >= 4.7 && < 4.15,
-    ansi-wl-pprint,
     blt >= 0.12.1,
     containers,
     what4 >= 0.4,
     lens >= 1.2,
     parameterized-utils,
+    prettyprinter >= 1.7.0,
     text,
     transformers
 

what4/src/What4/BaseTypes.hs

@@ -84,7 +84,7 @@ import qualified Data.Parameterized.Context as Ctx
 import           Data.Parameterized.NatRepr
 import           Data.Parameterized.TH.GADT
 import           GHC.TypeNats as TypeNats
-import           Text.PrettyPrint.ANSI.Leijen
+import           Prettyprinter
 
 --------------------------------------------------------------------------------
 -- KnownCtx
@@ -290,19 +290,19 @@ instance Hashable (StringInfoRepr si) where
   hashWithSalt = $(structuralHashWithSalt [t|StringInfoRepr|] [])
 
 instance Pretty (BaseTypeRepr bt) where
-  pretty = text . show
+  pretty = pretty . show
 instance Show (BaseTypeRepr bt) where
   showsPrec = $(structuralShowsPrec [t|BaseTypeRepr|])
 instance ShowF BaseTypeRepr
 
 instance Pretty (FloatPrecisionRepr fpp) where
-  pretty = text . show
+  pretty = pretty . show
 instance Show (FloatPrecisionRepr fpp) where
   showsPrec = $(structuralShowsPrec [t|FloatPrecisionRepr|])
 instance ShowF FloatPrecisionRepr
 
 instance Pretty (StringInfoRepr si) where
-  pretty = text . show
+  pretty = pretty . show
 instance Show (StringInfoRepr si) where
   showsPrec = $(structuralShowsPrec [t|StringInfoRepr|])
 instance ShowF StringInfoRepr

what4/src/What4/Concrete.hs

@@ -52,7 +52,7 @@ import           Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import qualified Numeric as N
 import           Numeric.Natural
-import qualified Text.PrettyPrint.ANSI.Leijen as PP
+import qualified Prettyprinter as PP
 
 import qualified Data.BitVector.Sized as BV
 import           Data.Parameterized.Classes
@@ -148,26 +148,30 @@ instance OrdF ConcreteVal where
 instance Ord (ConcreteVal tp) where
   compare x y = toOrdering (compareF x y)
 
+-- | Pretty-print a rational number.
+ppRational :: Rational -> PP.Doc ann
+ppRational x = PP.pretty (show x)
+
 -- | Pretty-print a concrete value
-ppConcrete :: ConcreteVal tp -> PP.Doc
+ppConcrete :: ConcreteVal tp -> PP.Doc ann
 ppConcrete = \case
-  ConcreteBool x -> PP.text (show x)
-  ConcreteNat x -> PP.text (show x)
-  ConcreteInteger x -> PP.text (show x)
-  ConcreteReal x -> PP.text (show x)
-  ConcreteString x -> PP.text (show x)
-  ConcreteBV w x -> PP.text ("0x" ++ (N.showHex (BV.asUnsigned x) (":[" ++ show w ++ "]")))
-  ConcreteComplex (r :+ i) -> PP.text "complex(" PP.<> PP.text (show r) PP.<> PP.text ", " PP.<> PP.text (show i) PP.<> PP.text ")"
-  ConcreteStruct xs -> PP.text "struct(" PP.<> PP.cat (intersperse PP.comma (toListFC ppConcrete xs)) PP.<> PP.text ")"
-  ConcreteArray _ def xs0 -> go (Map.toAscList xs0) (PP.text "constArray(" PP.<> ppConcrete def PP.<> PP.text ")")
+  ConcreteBool x -> PP.pretty x
+  ConcreteNat x -> PP.pretty x
+  ConcreteInteger x -> PP.pretty x
+  ConcreteReal x -> ppRational x
+  ConcreteString x -> PP.pretty (show x)
+  ConcreteBV w x -> PP.pretty ("0x" ++ (N.showHex (BV.asUnsigned x) (":[" ++ show w ++ "]")))
+  ConcreteComplex (r :+ i) -> PP.pretty "complex(" PP.<> ppRational r PP.<> PP.pretty ", " PP.<> ppRational i PP.<> PP.pretty ")"
+  ConcreteStruct xs -> PP.pretty "struct(" PP.<> PP.cat (intersperse PP.comma (toListFC ppConcrete xs)) PP.<> PP.pretty ")"
+  ConcreteArray _ def xs0 -> go (Map.toAscList xs0) (PP.pretty "constArray(" PP.<> ppConcrete def PP.<> PP.pretty ")")
     where
     go  [] doc = doc
     go ((i,x):xs) doc = ppUpd i x (go xs doc)
 
     ppUpd i x doc =
-       PP.text "update(" PP.<> PP.cat (intersperse PP.comma (toListFC ppConcrete i))
+       PP.pretty "update(" PP.<> PP.cat (intersperse PP.comma (toListFC ppConcrete i))
                          PP.<> PP.comma
                          PP.<> ppConcrete x
                          PP.<> PP.comma
                          PP.<> doc
-                         PP.<> PP.text ")"
+                         PP.<> PP.pretty ")"