From b21bf2ddeaba32a853741fa49970b1efd8bdc148 Mon Sep 17 00:00:00 2001
From: Sirui Lu <siruilu@cs.washington.edu>
Date: Fri, 6 Sep 2024 19:07:59 -0700
Subject: [PATCH] :zap: Remove Show and pformatSym in SupportedPrim

---
 src/Grisette/Core.hs                          |  2 +-
 .../Internal/Core/Data/Class/ModelOps.hs      | 12 ++++++------
 .../Internal/Core/Data/Class/Solver.hs        |  6 +++---
 .../Internal/SymPrim/FunInstanceGen.hs        |  1 +
 src/Grisette/Internal/SymPrim/ModelRep.hs     |  2 +-
 .../Internal/SymPrim/Prim/Internal/Caches.hs  |  9 ++++++---
 .../Internal/SymPrim/Prim/Internal/Term.hs    | 11 +++--------
 src/Grisette/Internal/SymPrim/Prim/Model.hs   |  2 +-
 test/Grisette/Backend/TermRewritingTests.hs   | 19 ++++++++++++++-----
 .../Core/Data/Class/SafeSymRotateTests.hs     |  9 ++++-----
 .../Core/Data/Class/SafeSymShiftTests.hs      |  9 ++++-----
 .../Core/Data/Class/SymRotateTests.hs         |  3 ++-
 .../Grisette/Core/Data/Class/SymShiftTests.hs |  4 ++--
 13 files changed, 48 insertions(+), 41 deletions(-)

diff --git a/src/Grisette/Core.hs b/src/Grisette/Core.hs
index f6e31230..66fa735c 100644
--- a/src/Grisette/Core.hs
+++ b/src/Grisette/Core.hs
@@ -1047,7 +1047,7 @@ module Grisette.Core
     -- >>> res
     -- ExceptT {If (|| a (! b)) (If a (Left Error1) (Left Error2)) (Right c)}
     -- >>> solveExcept z3 (\case Left _ -> con False; Right x -> x) res
-    -- Right (Model {a -> False :: Bool, b -> True :: Bool, c -> True :: Bool})
+    -- Right (Model {a -> false :: Bool, b -> true :: Bool, c -> true :: Bool})
     --
     -- The solver call in the above example means that we want the solver to
     -- find the conditions under which no error is thrown, and the result is
diff --git a/src/Grisette/Internal/Core/Data/Class/ModelOps.hs b/src/Grisette/Internal/Core/Data/Class/ModelOps.hs
index 405a33e6..aca732db 100644
--- a/src/Grisette/Internal/Core/Data/Class/ModelOps.hs
+++ b/src/Grisette/Internal/Core/Data/Class/ModelOps.hs
@@ -106,17 +106,17 @@ class
 -- >>> valueOf bBool (buildModel (aBool ::= True) :: Model)
 -- Nothing
 -- >>> insertValue bBool False (buildModel (aBool ::= True) :: Model)
--- Model {a -> True :: Bool, b -> False :: Bool}
+-- Model {a -> true :: Bool, b -> false :: Bool}
 -- >>> let abModel = buildModel (aBool ::= True, bBool ::= False) :: Model
 -- >>> let acSet = buildSymbolSet (aBool, cBool) :: AnySymbolSet
 -- >>> exceptFor acSet abModel
--- Model {b -> False :: Bool}
+-- Model {b -> false :: Bool}
 -- >>> restrictTo acSet abModel
--- Model {a -> True :: Bool}
+-- Model {a -> true :: Bool}
 -- >>> extendTo acSet abModel
--- Model {a -> True :: Bool, b -> False :: Bool, c -> False :: Bool}
+-- Model {a -> true :: Bool, b -> false :: Bool, c -> false :: Bool}
 -- >>> exact acSet abModel
--- Model {a -> True :: Bool, c -> False :: Bool}
+-- Model {a -> true :: Bool, c -> false :: Bool}
 class
   (SymbolSetOps symbolSet typedSymbol) =>
   ModelOps model symbolSet typedSymbol
@@ -166,5 +166,5 @@ class ModelRep rep model | rep -> model where
   -- >>> let aBool = "a" :: TypedAnySymbol Bool
   -- >>> let bBool = "b" :: TypedAnySymbol Bool
   -- >>> buildModel (aBool ::= True, bBool ::= False) :: Model
-  -- Model {a -> True :: Bool, b -> False :: Bool}
+  -- Model {a -> true :: Bool, b -> false :: Bool}
   buildModel :: rep -> model
diff --git a/src/Grisette/Internal/Core/Data/Class/Solver.hs b/src/Grisette/Internal/Core/Data/Class/Solver.hs
index 7ea8c7dc..76cde709 100644
--- a/src/Grisette/Internal/Core/Data/Class/Solver.hs
+++ b/src/Grisette/Internal/Core/Data/Class/Solver.hs
@@ -167,7 +167,7 @@ class Solver handle where
   --
   -- >>> solver <- newSolver z3
   -- >>> solverSolve solver "a"
-  -- Right (Model {a -> True :: Bool})
+  -- Right (Model {a -> true :: Bool})
   -- >>> solverSolve solver $ symNot "a"
   -- Left Unsat
   --
@@ -176,7 +176,7 @@ class Solver handle where
   -- >>> solverResetAssertions solver
   -- Right ()
   -- >>> solverSolve solver $ symNot "a"
-  -- Right (Model {a -> False :: Bool})
+  -- Right (Model {a -> false :: Bool})
   solverResetAssertions :: handle -> IO (Either SolvingFailure ())
   solverResetAssertions handle =
     solverRunCommand (const $ return $ Right ()) handle SolverResetAssertions
@@ -313,7 +313,7 @@ withSolver config action =
 -- | Solve a single formula. Find an assignment to it to make it true.
 --
 -- >>> solve z3 ("a" .&& ("b" :: SymInteger) .== 1)
--- Right (Model {a -> True :: Bool, b -> 1 :: Integer})
+-- Right (Model {a -> true :: Bool, b -> 1 :: Integer})
 -- >>> solve z3 ("a" .&& symNot "a")
 -- Left Unsat
 solve ::
diff --git a/src/Grisette/Internal/SymPrim/FunInstanceGen.hs b/src/Grisette/Internal/SymPrim/FunInstanceGen.hs
index 47d7b7ee..fa4165ad 100644
--- a/src/Grisette/Internal/SymPrim/FunInstanceGen.hs
+++ b/src/Grisette/Internal/SymPrim/FunInstanceGen.hs
@@ -226,6 +226,7 @@ supportedPrimFun
                 sequence
                   [ [t|SupportedNonFuncPrim $ty|],
                     [t|Eq $ty|],
+                    [t|Show $ty|],
                     [t|Hashable $ty|]
                   ]
             )
diff --git a/src/Grisette/Internal/SymPrim/ModelRep.hs b/src/Grisette/Internal/SymPrim/ModelRep.hs
index fe88acf8..265459a8 100644
--- a/src/Grisette/Internal/SymPrim/ModelRep.hs
+++ b/src/Grisette/Internal/SymPrim/ModelRep.hs
@@ -33,7 +33,7 @@ import Grisette.Internal.SymPrim.Prim.Term
 -- This is used to build a model from a list of symbolic constants and their values.
 --
 -- >>> buildModel ("a" := (1 :: Integer), "b" := True) :: Model
--- Model {a -> 1 :: Integer, b -> True :: Bool}
+-- Model {a -> 1 :: Integer, b -> true :: Bool}
 data ModelSymPair ct st where
   (:=) :: (LinkedRep ct st) => st -> ct -> ModelSymPair ct st
 
diff --git a/src/Grisette/Internal/SymPrim/Prim/Internal/Caches.hs b/src/Grisette/Internal/SymPrim/Prim/Internal/Caches.hs
index f2e1675b..fa3474a2 100644
--- a/src/Grisette/Internal/SymPrim/Prim/Internal/Caches.hs
+++ b/src/Grisette/Internal/SymPrim/Prim/Internal/Caches.hs
@@ -26,7 +26,7 @@ module Grisette.Internal.SymPrim.Prim.Internal.Caches
     intern,
     haveCache,
     threadCacheSize,
-    dumpThreadCache,
+    -- dumpThreadCache,
     threadCacheLiveSize,
   )
 where
@@ -83,8 +83,7 @@ data CacheState t where
 
 -- | A class for interning terms.
 class
-  ( Show (Description t),
-    Hashable (Description t),
+  ( Hashable (Description t),
     Eq (Description t),
     Typeable t,
     Show t
@@ -242,6 +241,7 @@ cacheStateLiveSize (CacheState sem s) = do
   putMVar sem ()
   return r
 
+{-
 dumpCacheState :: CacheState t -> IO ()
 dumpCacheState (CacheState sem s) = do
   takeMVar sem
@@ -258,6 +258,7 @@ dumpCacheState (CacheState sem s) = do
 
 dumpCache :: Cache t -> IO ()
 dumpCache (Cache a) = mapM_ dumpCacheState (A.elems a)
+-}
 
 cacheSize :: Cache t -> IO Int
 cacheSize (Cache a) = sum <$> mapM cacheStateSize (A.elems a)
@@ -285,6 +286,7 @@ threadCacheLiveSize tid = do
       sum <$> mapM cacheLiveSize (HM.elems cache)
     Nothing -> return 0
 
+{-
 -- | Dump the current thread's cache.
 dumpThreadCache :: WeakThreadId -> IO ()
 dumpThreadCache tid = do
@@ -294,3 +296,4 @@ dumpThreadCache tid = do
       cache <- readIORef cref
       mapM_ dumpCache (HM.elems cache)
     Nothing -> return ()
+-}
\ No newline at end of file
diff --git a/src/Grisette/Internal/SymPrim/Prim/Internal/Term.hs b/src/Grisette/Internal/SymPrim/Prim/Internal/Term.hs
index f5a12dd3..8d508f2d 100644
--- a/src/Grisette/Internal/SymPrim/Prim/Internal/Term.hs
+++ b/src/Grisette/Internal/SymPrim/Prim/Internal/Term.hs
@@ -393,7 +393,6 @@ class SupportedPrimConstraint t where
 class
   ( Lift t,
     Typeable t,
-    Show t,
     NFData t,
     SupportedPrimConstraint t,
     SBVRep t
@@ -409,8 +408,6 @@ class
   pformatCon :: t -> String
   default pformatCon :: (Show t) => t -> String
   pformatCon = show
-  pformatSym :: TypedSymbol 'AnyKind t -> String
-  pformatSym = showUntyped
   defaultValue :: t
   defaultValueDynamic :: proxy t -> ModelValue
   default defaultValueDynamic :: (Hashable t) => proxy t -> ModelValue
@@ -466,7 +463,7 @@ data ModelValue where
   ModelValue :: forall v. (SupportedPrim v) => v -> ModelValue
 
 instance Show ModelValue where
-  show (ModelValue (v :: v)) = show v ++ " :: " ++ show (typeRep @v)
+  show (ModelValue (v :: v)) = pformatCon v ++ " :: " ++ show (typeRep @v)
 
 instance Eq ModelValue where
   (ModelValue (v1 :: v1)) == (ModelValue (v2 :: v2)) =
@@ -1609,7 +1606,7 @@ introSupportedPrimConstraint ToFPTerm {} x = x
 -- | Pretty-print a term.
 pformatTerm :: forall t. Term t -> String
 pformatTerm (ConTerm _ _ _ t) = pformatCon t
-pformatTerm (SymTerm _ _ _ sym) = pformatSym sym
+pformatTerm (SymTerm _ _ _ sym) = showUntyped sym
 pformatTerm (ForallTerm _ _ _ sym arg) = "(forall " ++ show sym ++ " " ++ pformatTerm arg ++ ")"
 pformatTerm (ExistsTerm _ _ _ sym arg) = "(exists " ++ show sym ++ " " ++ pformatTerm arg ++ ")"
 pformatTerm (NotTerm _ _ _ arg) = "(! " ++ pformatTerm arg ++ ")"
@@ -1675,7 +1672,7 @@ instance Lift (Term t) where
 
 instance Show (Term ty) where
   show (ConTerm tid _ i v) =
-    "ConTerm{tid=" ++ show tid ++ ", id=" ++ show i ++ ", v=" ++ show v ++ "}"
+    "ConTerm{tid=" ++ show tid ++ ", id=" ++ show i ++ ", v=" ++ pformatCon v ++ "}"
   show (SymTerm tid _ i name) =
     "SymTerm{tid="
       ++ show tid
@@ -3306,8 +3303,6 @@ termThreadId (FromFPOrTerm tid _ _ _ _ _) = tid
 termThreadId (ToFPTerm tid _ _ _ _ _ _) = tid
 {-# INLINE termThreadId #-}
 
-deriving instance (SupportedPrim t) => Show (Description (Term t))
-
 instance (SupportedPrim t) => Eq (Description (Term t)) where
   DConTerm _ (l :: tyl) == DConTerm _ (r :: tyr) =
     case cast @tyl @tyr l of
diff --git a/src/Grisette/Internal/SymPrim/Prim/Model.hs b/src/Grisette/Internal/SymPrim/Prim/Model.hs
index 6a17207c..426e9aec 100644
--- a/src/Grisette/Internal/SymPrim/Prim/Model.hs
+++ b/src/Grisette/Internal/SymPrim/Prim/Model.hs
@@ -386,7 +386,7 @@ evalTerm fillDefault (Model ma) =
 -- A type used for building a model by hand.
 --
 -- >>> buildModel ("x" ::= (1 :: Integer), "y" ::= True) :: Model
--- Model {x -> 1 :: Integer, y -> True :: Bool}
+-- Model {x -> 1 :: Integer, y -> true :: Bool}
 data ModelValuePair t = (TypedAnySymbol t) ::= t deriving (Show)
 
 instance ModelRep (ModelValuePair t) Model where
diff --git a/test/Grisette/Backend/TermRewritingTests.hs b/test/Grisette/Backend/TermRewritingTests.hs
index eed0c47b..a1919a56 100644
--- a/test/Grisette/Backend/TermRewritingTests.hs
+++ b/test/Grisette/Backend/TermRewritingTests.hs
@@ -633,7 +633,11 @@ termRewritingTests =
       testGroup "bitCast" $ do
         let bitCastCase ::
               forall a b.
-              (Arbitrary a, PEvalBitCastTerm a b, SupportedNonFuncPrim a) =>
+              ( Arbitrary a,
+                PEvalBitCastTerm a b,
+                SupportedNonFuncPrim a,
+                Show a
+              ) =>
               Test
             bitCastCase = testProperty
               (show (typeRep @a) <> " -> " <> show (typeRep @b))
@@ -650,7 +654,9 @@ termRewritingTests =
                 Arbitrary b,
                 PEvalBitCastOrTerm a b,
                 RealFloat a,
-                SupportedNonFuncPrim a
+                SupportedNonFuncPrim a,
+                Show b,
+                Show a
               ) =>
               Test
             fromFPCase = testProperty
@@ -668,7 +674,8 @@ termRewritingTests =
               ( Arbitrary a,
                 PEvalBitCastTerm a b,
                 RealFloat b,
-                SupportedNonFuncPrim a
+                SupportedNonFuncPrim a,
+                Show a
               ) =>
               Test
             toFPCase = testProperty
@@ -746,7 +753,8 @@ termRewritingTests =
               ( ValidFP eb sb,
                 Arbitrary b,
                 PEvalIEEEFPConvertibleTerm b,
-                TermRewritingSpec spec b
+                TermRewritingSpec spec b,
+                Show b
               ) =>
               Bool ->
               Test
@@ -815,7 +823,8 @@ termRewritingTests =
                 SupportedNonFuncPrim b,
                 LinkedRep b bs,
                 Solvable b bs,
-                SymEq bs
+                SymEq bs,
+                Show b
               ) =>
               Test
             toFPCase = testProperty
diff --git a/test/Grisette/Core/Data/Class/SafeSymRotateTests.hs b/test/Grisette/Core/Data/Class/SafeSymRotateTests.hs
index 5c6ca9a4..c4cbfa5d 100644
--- a/test/Grisette/Core/Data/Class/SafeSymRotateTests.hs
+++ b/test/Grisette/Core/Data/Class/SafeSymRotateTests.hs
@@ -25,7 +25,6 @@ import Grisette
     Union,
     WordN,
   )
-import Grisette.Internal.SymPrim.Prim.Term (LinkedRep)
 import Grisette.Lib.Control.Monad (mrgReturn)
 import Grisette.Lib.Control.Monad.Except (mrgThrowError)
 import Test.Framework (Test, testGroup)
@@ -99,8 +98,8 @@ concreteUnsignedSymTypeSafeSymRotateTests ::
     FiniteBits c,
     Bounded c,
     Integral c,
-    LinkedRep c s,
-    Solvable c s
+    Solvable c s,
+    Show c
   ) =>
   proxy s ->
   [Test]
@@ -129,8 +128,8 @@ concreteSignedAtLeastThreeBitsSymTypeSafeSymRotateTests ::
     FiniteBits c,
     Bounded c,
     Integral c,
-    LinkedRep c s,
-    Solvable c s
+    Solvable c s,
+    Show c
   ) =>
   proxy s ->
   [Test]
diff --git a/test/Grisette/Core/Data/Class/SafeSymShiftTests.hs b/test/Grisette/Core/Data/Class/SafeSymShiftTests.hs
index 2a1bdc38..5ee985c9 100644
--- a/test/Grisette/Core/Data/Class/SafeSymShiftTests.hs
+++ b/test/Grisette/Core/Data/Class/SafeSymShiftTests.hs
@@ -27,7 +27,6 @@ import Grisette
     Union,
     WordN,
   )
-import Grisette.Internal.SymPrim.Prim.Term (LinkedRep)
 import Grisette.Lib.Control.Monad (mrgReturn)
 import Grisette.Lib.Control.Monad.Except (mrgThrowError)
 import Test.Framework (Test, testGroup)
@@ -115,8 +114,8 @@ concreteUnsignedSymTypeSafeSymShiftTests ::
     FiniteBits c,
     FiniteBits s,
     Bounded c,
-    LinkedRep c s,
-    Solvable c s
+    Solvable c s,
+    Show c
   ) =>
   proxy s ->
   [Test]
@@ -158,8 +157,8 @@ concreteSignedAtLeastThreeBitsSymTypeSafeSymShiftTests ::
     FiniteBits s,
     Bounded c,
     Integral c,
-    LinkedRep c s,
-    Solvable c s
+    Solvable c s,
+    Show c
   ) =>
   proxy s ->
   [Test]
diff --git a/test/Grisette/Core/Data/Class/SymRotateTests.hs b/test/Grisette/Core/Data/Class/SymRotateTests.hs
index 18c48e28..c640824e 100644
--- a/test/Grisette/Core/Data/Class/SymRotateTests.hs
+++ b/test/Grisette/Core/Data/Class/SymRotateTests.hs
@@ -127,7 +127,8 @@ symbolicTypeSymRotateTests ::
     Typeable s,
     Integral c,
     LinkedRep c s,
-    Solvable c s
+    Solvable c s,
+    Show c
   ) =>
   proxy s ->
   Test
diff --git a/test/Grisette/Core/Data/Class/SymShiftTests.hs b/test/Grisette/Core/Data/Class/SymShiftTests.hs
index 6dc786b0..039612ce 100644
--- a/test/Grisette/Core/Data/Class/SymShiftTests.hs
+++ b/test/Grisette/Core/Data/Class/SymShiftTests.hs
@@ -116,8 +116,8 @@ symbolicTypeSymShiftTests ::
     Bounded c,
     Typeable s,
     Integral c,
-    LinkedRep c s,
-    Solvable c s
+    Solvable c s,
+    Show c
   ) =>
   proxy s ->
   Test