grisette 0.3.0.0 → 0.3.1.0

raw patch · 23 files changed

+985/−12 lines, 23 filesdep +QuickCheckdep +prettyprinterdep +textPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: QuickCheck, prettyprinter, text

API changes (from Hackage documentation)

Files

• CHANGELOG.md +15/−0
• grisette.cabal +17/−6
• src/Grisette/Core.hs +4/−0
• src/Grisette/Core/Control/Monad/UnionM.hs +13/−0
• src/Grisette/Core/Data/BV.hs +33/−2
• src/Grisette/Core/Data/Class/Bool.hs +2/−0
• src/Grisette/Core/Data/Class/Evaluate.hs +2/−0
• src/Grisette/Core/Data/Class/ExtractSymbolics.hs +67/−0
• src/Grisette/Core/Data/Class/GPretty.hs +376/−0
• src/Grisette/Core/Data/Class/GenSym.hs +3/−0
• src/Grisette/Core/Data/Class/Mergeable.hs +2/−0
• src/Grisette/Core/Data/Class/SOrd.hs +2/−0
• src/Grisette/Core/Data/Class/Substitute.hs +2/−0
• src/Grisette/Core/Data/Class/ToCon.hs +2/−0
• src/Grisette/Core/Data/Class/ToSym.hs +2/−0
• src/Grisette/Core/Data/Union.hs +23/−0
• src/Grisette/Experimental/GenSymConstrained.hs +0/−1
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs +25/−0
• src/Grisette/IR/SymPrim/Data/SymPrim.hs +31/−0
• src/Grisette/IR/SymPrim/Data/SymPrim.hs-boot +3/−0
• test/Grisette/Core/Data/BVTests.hs +7/−0
• test/Grisette/Core/Data/Class/GPrettyTests.hs +342/−0
• test/Main.hs +12/−3

@@ -5,6 +5,17 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## [0.3.1.0] -- 2023-07-19++### Added+- Added support to `Data.Text`. ([#95](https://github.com/lsrcz/grisette/pull/95))+- Added `Arbitrary` instances for bit vectors. ([#97](https://github.com/lsrcz/grisette/pull/97))+- Added pretty printers for Grisette data types. ([#101](https://github.com/lsrcz/grisette/pull/101))+- Added `ExtractSymbolics` instances for tuples longer than 2. ([#103](https://github.com/lsrcz/grisette/pull/103))++### Fixed+- Fixed the `Read` instance for bit vectors. ([#99](https://github.com/lsrcz/grisette/pull/99), [#100](https://github.com/lsrcz/grisette/pull/100))+ ## [0.3.0.0] -- 2023-07-07  ### Added@@ -52,6 +63,10 @@ ### Added - Initial release for Grisette. +[Unreleased]: https://github.com/lsrcz/grisette/compare/v0.3.1.0...HEAD+[0.3.1.0]: https://github.com/lsrcz/grisette/compare/v0.3.0.0...v0.3.1.0+[0.3.0.0]: https://github.com/lsrcz/grisette/compare/v0.2.0.0...v0.3.0.0+[Unreleased]: https://github.com/lsrcz/grisette/compare/v0.3.0.0...HEAD [0.3.0.0]: https://github.com/lsrcz/grisette/compare/v0.2.0.0...v0.3.0.0 [0.2.0.0]: https://github.com/lsrcz/grisette/compare/v0.1.0.0...v0.2.0.0 [0.1.0.0]: https://github.com/lsrcz/grisette/tree/v0.1.0.0

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           grisette-version:        0.3.0.0+version:        0.3.1.0 synopsis:       Symbolic evaluation as a library description:    Grisette is a reusable symbolic evaluation library for Haskell. By                 translating programs into constraints, Grisette can help the development of@@ -16,8 +16,8 @@                 .                 For more details, please checkout the README. category:       Formal Methods, Theorem Provers, Symbolic Computation, SMT-homepage:       https://github.com/lsrcz/grisette-haskell#readme-bug-reports:    https://github.com/lsrcz/grisette-haskell/issues+homepage:       https://github.com/lsrcz/grisette#readme+bug-reports:    https://github.com/lsrcz/grisette/issues author:         Sirui Lu, Rastislav Bodík maintainer:     Sirui Lu (siruilu@cs.washington.edu) copyright:      2021-2023 Sirui Lu@@ -36,7 +36,7 @@  source-repository head   type: git-  location: https://github.com/lsrcz/grisette-haskell+  location: https://github.com/lsrcz/grisette  flag fast   description: Compile with O2 optimization@@ -66,6 +66,7 @@       Grisette.Core.Data.Class.ExtractSymbolics       Grisette.Core.Data.Class.Function       Grisette.Core.Data.Class.GenSym+      Grisette.Core.Data.Class.GPretty       Grisette.Core.Data.Class.Mergeable       Grisette.Core.Data.Class.ModelOps       Grisette.Core.Data.Class.SafeArith@@ -126,7 +127,8 @@   hs-source-dirs:       src   build-depends:-      array >=0.5.4 && <0.6+      QuickCheck >=2.13.2 && <2.15+    , array >=0.5.4 && <0.6     , base >=4.14 && <5     , bytestring >=0.10.12 && <0.12     , call-stack >=0.1 && <0.5@@ -138,8 +140,10 @@     , loch-th >=0.2.2 && <0.3     , mtl >=2.2.2 && <2.4     , parallel >=3.2.2.0 && <3.3+    , prettyprinter >=1.5.0 && <1.8     , sbv >=8.11 && <10.3     , template-haskell >=2.16 && <2.21+    , text >=1.2.4.1 && <2.1     , th-compat >=0.1.2 && <0.2     , transformers >=0.5.6 && <0.7     , unordered-containers >=0.2.11 && <0.3@@ -159,6 +163,7 @@       doctest   build-depends:       Glob+    , QuickCheck >=2.13.2 && <2.15     , array >=0.5.4 && <0.6     , base >=4.14 && <5     , bytestring >=0.10.12 && <0.12@@ -173,8 +178,10 @@     , loch-th >=0.2.2 && <0.3     , mtl >=2.2.2 && <2.4     , parallel >=3.2.2.0 && <3.3+    , prettyprinter >=1.5.0 && <1.8     , sbv >=8.11 && <10.3     , template-haskell >=2.16 && <2.21+    , text >=1.2.4.1 && <2.1     , th-compat >=0.1.2 && <0.2     , transformers >=0.5.6 && <0.7     , unordered-containers >=0.2.11 && <0.3@@ -195,6 +202,7 @@       Grisette.Backend.SBV.Data.SMT.TermRewritingTests       Grisette.Core.Control.Monad.UnionMTests       Grisette.Core.Data.BVTests+      Grisette.Core.Data.Class.GPrettyTests       Grisette.IR.SymPrim.Data.Prim.BitsTests       Grisette.IR.SymPrim.Data.Prim.BoolTests       Grisette.IR.SymPrim.Data.Prim.BVTests@@ -208,7 +216,8 @@   hs-source-dirs:       test   build-depends:-      array >=0.5.4 && <0.6+      QuickCheck >=2.13.2 && <2.15+    , array >=0.5.4 && <0.6     , base >=4.14 && <5     , bytestring >=0.10.12 && <0.12     , call-stack >=0.1 && <0.5@@ -221,12 +230,14 @@     , loch-th >=0.2.2 && <0.3     , mtl >=2.2.2 && <2.4     , parallel >=3.2.2.0 && <3.3+    , prettyprinter >=1.5.0 && <1.8     , sbv >=8.11 && <10.3     , tasty >=1.1.0.3 && <1.5     , tasty-hunit ==0.10.*     , tasty-quickcheck >=0.10.1 && <0.11     , tasty-test-reporter >=0.1.1.2 && <0.2     , template-haskell >=2.16 && <2.21+    , text >=1.2.4.1 && <2.1     , th-compat >=0.1.2 && <0.2     , transformers >=0.5.6 && <0.7     , unordered-containers >=0.2.11 && <0.3

@@ -613,6 +613,9 @@     ToCon (..),     ToSym (..), +    -- * Pretty printing+    GPretty (..),+     -- * Symbolic Generation      -- | It is usually useful to generate complex symbolic values. For example,@@ -1020,6 +1023,7 @@ import Grisette.Core.Data.Class.Evaluate import Grisette.Core.Data.Class.ExtractSymbolics import Grisette.Core.Data.Class.Function+import Grisette.Core.Data.Class.GPretty import Grisette.Core.Data.Class.GenSym import Grisette.Core.Data.Class.Mergeable import Grisette.Core.Data.Class.ModelOps

@@ -7,6 +7,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskellQuotes #-} {-# LANGUAGE Trustworthy #-}@@ -55,6 +56,7 @@ import Grisette.Core.Data.Class.Evaluate import Grisette.Core.Data.Class.ExtractSymbolics import Grisette.Core.Data.Class.Function+import Grisette.Core.Data.Class.GPretty import Grisette.Core.Data.Class.GenSym import Grisette.Core.Data.Class.Mergeable import Grisette.Core.Data.Class.SOrd@@ -71,6 +73,12 @@ import Language.Haskell.TH.Syntax import Language.Haskell.TH.Syntax.Compat (unTypeSplice) +#if MIN_VERSION_prettyprinter(1,7,0)+import Prettyprinter+#else+import Data.Text.Prettyprint.Doc+#endif+ -- $setup -- >>> import Grisette.Core -- >>> import Grisette.IR.SymPrim@@ -238,6 +246,11 @@     wrapBracket '{' '}'       . liftShowsPrecUnion sp sl 0       $ a++instance (GPretty a) => GPretty (UnionM a) where+  gpretty = \case+    (UAny a) -> groupedEnclose "<" ">" $ gpretty a+    (UMrg _ a) -> groupedEnclose "{" "}" $ gpretty a  -- | Extract the underlying Union. May be unmerged. underlyingUnion :: UnionM a -> Union a

@@ -44,11 +44,13 @@   ) where +import Control.Applicative import Control.DeepSeq import Control.Exception import Data.Bits import Data.CallStack import Data.Hashable+import Data.Maybe import Data.Proxy import Data.Typeable import GHC.Enum@@ -60,6 +62,9 @@ import Grisette.Utils.Parameterized import Language.Haskell.TH.Syntax import Numeric+import qualified Test.QuickCheck as QC+import Text.ParserCombinators.ReadP (skipSpaces, string)+import Text.ParserCombinators.ReadPrec import Text.Read import qualified Text.Read.Lex as L @@ -161,8 +166,26 @@   | Just i <- L.numberToInteger n = return (fromInteger i) convertInt _ = pfail +readBinary :: (Num a) => ReadPrec a+readBinary = parens $ do+  r0 <- look+  case r0 of+    ('-' : _) -> do+      _ <- get+      negate <$> parens parse0b+    _ -> parse0b+  where+    isDigit c = isJust (valDig c)+    valDigit c = fromMaybe 0 (valDig c)+    valDig '0' = Just 0+    valDig '1' = Just 1+    valDig _ = Nothing+    parse0b = do+      _ <- Text.Read.lift $ string "0b"+      fromInteger <$> Text.Read.lift (L.readIntP 2 isDigit valDigit)+ instance (KnownNat n, 1 <= n) => Read (WordN n) where-  readPrec = readNumber convertInt+  readPrec = readNumber convertInt <|> readBinary   readListPrec = readListPrecDefault   readList = readListDefault @@ -257,7 +280,7 @@       binRep = showIntAtBase 2 (\x -> if x == 0 then '0' else '1') w ""  instance (KnownNat n, 1 <= n) => Read (IntN n) where-  readPrec = readNumber convertInt+  readPrec = readNumber convertInt <|> readBinary   readListPrec = readListPrecDefault   readList = readListDefault @@ -417,6 +440,10 @@   signum = unarySomeWordNR1 signum   fromInteger = error "fromInteger is not defined for SomeWordN as no bitwidth is known" +instance (KnownNat n, 1 <= n) => QC.Arbitrary (WordN n) where+  arbitrary = QC.arbitrarySizedBoundedIntegral+  shrink = QC.shrinkIntegral+ minusOneIntN :: forall proxy n. (KnownNat n) => proxy n -> IntN n minusOneIntN _ = IntN (1 `shiftL` fromIntegral (natVal (Proxy :: Proxy n)) - 1) @@ -593,6 +620,10 @@       n = fromIntegral (natVal (Proxy :: Proxy n))       as = testBit a (n - 1)       bs = testBit b (n - 1)++instance (KnownNat n, 1 <= n) => QC.Arbitrary (IntN n) where+  arbitrary = QC.arbitrarySizedBoundedIntegral+  shrink = QC.shrinkIntegral  instance SizedBV WordN where   sizedBVConcat :: forall l r. (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => WordN l -> WordN r -> WordN (l + r)

@@ -41,6 +41,7 @@ import qualified Data.ByteString as B import Data.Functor.Sum import Data.Int+import qualified Data.Text as T import Data.Word import GHC.TypeNats import Generics.Deriving@@ -244,6 +245,7 @@ CONCRETE_SEQ(Word32) CONCRETE_SEQ(Word64) CONCRETE_SEQ(B.ByteString)+CONCRETE_SEQ(T.Text) CONCRETE_SEQ_BV(WordN) CONCRETE_SEQ_BV(IntN) CONCRETE_SEQ(SomeWordN)

@@ -34,6 +34,7 @@ import Data.Functor.Sum import Data.Int import Data.Maybe+import qualified Data.Text as T import Data.Word import GHC.TypeNats import Generics.Deriving@@ -127,6 +128,7 @@ CONCRETE_EVALUATESYM(SomeIntN) CONCRETE_EVALUATESYM(SomeWordN) CONCRETE_EVALUATESYM(B.ByteString)+CONCRETE_EVALUATESYM(T.Text) CONCRETE_EVALUATESYM_BV(IntN) CONCRETE_EVALUATESYM_BV(WordN) #endif

@@ -32,6 +32,7 @@ import qualified Data.ByteString as B import Data.Functor.Sum import Data.Int+import qualified Data.Text as T import Data.Word import GHC.TypeNats import Generics.Deriving@@ -115,6 +116,7 @@ CONCRETE_EXTRACT_SYMBOLICS(SomeWordN) CONCRETE_EXTRACT_SYMBOLICS(SomeIntN) CONCRETE_EXTRACT_SYMBOLICS(B.ByteString)+CONCRETE_EXTRACT_SYMBOLICS(T.Text) CONCRETE_EXTRACT_SYMBOLICS_BV(WordN) CONCRETE_EXTRACT_SYMBOLICS_BV(IntN) #endif@@ -155,6 +157,71 @@   instance     (ExtractSymbolics a, ExtractSymbolics b, ExtractSymbolics c) =>     ExtractSymbolics (a, b, c)++-- (,,,)+deriving via+  (Default (a, b, c, d))+  instance+    ( ExtractSymbolics a,+      ExtractSymbolics b,+      ExtractSymbolics c,+      ExtractSymbolics d+    ) =>+    ExtractSymbolics (a, b, c, d)++-- (,,,,)+deriving via+  (Default (a, b, c, d, e))+  instance+    ( ExtractSymbolics a,+      ExtractSymbolics b,+      ExtractSymbolics c,+      ExtractSymbolics d,+      ExtractSymbolics e+    ) =>+    ExtractSymbolics (a, b, c, d, e)++-- (,,,,,)+deriving via+  (Default (a, b, c, d, e, f))+  instance+    ( ExtractSymbolics a,+      ExtractSymbolics b,+      ExtractSymbolics c,+      ExtractSymbolics d,+      ExtractSymbolics e,+      ExtractSymbolics f+    ) =>+    ExtractSymbolics (a, b, c, d, e, f)++-- (,,,,,,)+deriving via+  (Default (a, b, c, d, e, f, g))+  instance+    ( ExtractSymbolics a,+      ExtractSymbolics b,+      ExtractSymbolics c,+      ExtractSymbolics d,+      ExtractSymbolics e,+      ExtractSymbolics f,+      ExtractSymbolics g+    ) =>+    ExtractSymbolics (a, b, c, d, e, f, g)++-- (,,,,,,,)+deriving via+  (Default (a, b, c, d, e, f, g, h))+  instance+    ( ExtractSymbolics a,+      ExtractSymbolics b,+      ExtractSymbolics c,+      ExtractSymbolics d,+      ExtractSymbolics e,+      ExtractSymbolics f,+      ExtractSymbolics g,+      ExtractSymbolics h+    ) =>+    ExtractSymbolics (a, b, c, d, e, f, g, h)  -- MaybeT instance (ExtractSymbolics (m (Maybe a))) => ExtractSymbolics (MaybeT m a) where

@@ -0,0 +1,376 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++module Grisette.Core.Data.Class.GPretty+  ( GPretty (..),+    groupedEnclose,+    condEnclose,+  )+where++import Control.Monad.Except+import Control.Monad.Identity+import Control.Monad.Trans.Maybe+import qualified Control.Monad.Writer.Lazy as WriterLazy+import qualified Control.Monad.Writer.Strict as WriterStrict+import qualified Data.ByteString as B+import Data.Functor.Sum+import Data.Int+import Data.Proxy+import Data.String+import qualified Data.Text as T+import Data.Word+import GHC.Generics+import GHC.TypeLits+import Generics.Deriving hiding (isNullary)+import Grisette.Core.Data.BV++#if MIN_VERSION_prettyprinter(1,7,0)+import Prettyprinter+#else+import Data.Text.Prettyprint.Doc+#endif++glist :: [Doc ann] -> Doc ann+glist l+  | null l = "[]"+  | length l == 1 = "[" <> head l <> "]"+  | otherwise = groupedEnclose "[" "]" $ encloseSep "" "" (flatAlt ", " ",") l++class GPretty a where+  gpretty :: a -> Doc ann+  gprettyPrec :: Int -> a -> Doc ann+  gprettyList :: [a] -> Doc ann+  gprettyList = align . glist . map gpretty++  gpretty = gprettyPrec 0+  gprettyPrec _ = gpretty++  {-# MINIMAL gpretty | gprettyPrec #-}++instance (Generic a, GPretty' (Rep a)) => GPretty (Default a) where+  gprettyPrec i v = gprettyPrec' Pref i $ from $ unDefault v++data Type = Rec | Tup | Pref | Inf String Int++class GPretty' a where+  gprettyPrec' :: Type -> Int -> a c -> Doc ann+  isNullary :: a c -> Bool+  isNullary = error "generic gpretty (isNullary): unnecessary case"++instance GPretty' V1 where+  gprettyPrec' _ _ x = case x of {}++instance GPretty' U1 where+  gprettyPrec' _ _ U1 = ""+  isNullary _ = True++instance (GPretty c) => GPretty' (K1 i c) where+  gprettyPrec' _ n (K1 a) = gprettyPrec n a+  isNullary _ = False++groupedEnclose :: Doc ann -> Doc ann -> Doc ann -> Doc ann+groupedEnclose l r d = group $ align $ vcat [l <> flatAlt " " "" <> d, r]++condEnclose :: Bool -> Doc ann -> Doc ann -> Doc ann -> Doc ann+condEnclose b = if b then groupedEnclose else const $ const id++instance (GPretty' a, Constructor c) => GPretty' (M1 C c a) where+  gprettyPrec' _ n c@(M1 x) =+    case t of+      Tup ->+        prettyBraces t (gprettyPrec' t 0 x)+      Inf _ m ->+        group $ condEnclose (n > m) "(" ")" $ gprettyPrec' t m x+      _ ->+        if isNullary x+          then pretty (conName c)+          else+            group $+              condEnclose (n > 10) "(" ")" $+                align $+                  nest 2 $+                    vsep+                      [ pretty (conName c),+                        prettyBraces t (gprettyPrec' t 11 x)+                      ]+    where+      prettyBraces :: Type -> Doc ann -> Doc ann+      prettyBraces Rec = groupedEnclose "{" "}"+      prettyBraces Tup = groupedEnclose "(" ")"+      prettyBraces Pref = id+      prettyBraces (Inf _ _) = id+      fixity = conFixity c+      t+        | conIsRecord c = Rec+        | conIsTuple c = Tup+        | otherwise = case fixity of+            Prefix -> Pref+            Infix _ i -> Inf (conName c) i+      conIsTuple :: C1 c f p -> Bool+      conIsTuple y = tupleName (conName y)+        where+          tupleName ('(' : ',' : _) = True+          tupleName _ = False++instance (Selector s, GPretty' a) => GPretty' (M1 S s a) where+  gprettyPrec' t n s@(M1 x)+    | selName s == "" =+        case t of+          Pref -> gprettyPrec' t (n + 1) x+          _ -> gprettyPrec' t (n + 1) x+    | otherwise =+        pretty (selName s) <+> "=" <+> gprettyPrec' t 0 x+  isNullary (M1 x) = isNullary x++instance (GPretty' a) => GPretty' (M1 D d a) where+  gprettyPrec' t n (M1 x) = gprettyPrec' t n x++instance (GPretty' a, GPretty' b) => GPretty' (a :+: b) where+  gprettyPrec' t n (L1 x) = gprettyPrec' t n x+  gprettyPrec' t n (R1 x) = gprettyPrec' t n x++instance (GPretty' a, GPretty' b) => GPretty' (a :*: b) where+  gprettyPrec' t@Rec n (a :*: b) =+    vcat+      [ gprettyPrec' t n a,+        "," <+> gprettyPrec' t n b+      ]+  gprettyPrec' t@(Inf s _) n (a :*: b) =+    align $+      nest 2 $+        vsep+          [ gprettyPrec' t n a,+            pretty s <+> gprettyPrec' t n b+          ]+  gprettyPrec' t@Tup n (a :*: b) =+    vcat+      [ gprettyPrec' t 0 a,+        "," <> flatAlt " " "" <> gprettyPrec' t 0 b+      ]+  gprettyPrec' t@Pref n (a :*: b) =+    vsep+      [ gprettyPrec' t (n + 1) a,+        gprettyPrec' t (n + 1) b+      ]+  isNullary _ = False++viaShowsPrec :: (Int -> a -> ShowS) -> Int -> a -> Doc ann+viaShowsPrec f n a = pretty (f n a "")++#define GPRETTY_SIMPLE(type) \+instance GPretty type where gprettyPrec = viaShowsPrec showsPrec++instance GPretty Char where+  gpretty = viaShow+  gprettyList v = pretty (fromString v :: T.Text)++#if 1+GPRETTY_SIMPLE(Bool)+GPRETTY_SIMPLE(Integer)+GPRETTY_SIMPLE(Int)+GPRETTY_SIMPLE(Int8)+GPRETTY_SIMPLE(Int16)+GPRETTY_SIMPLE(Int32)+GPRETTY_SIMPLE(Int64)+GPRETTY_SIMPLE(Word)+GPRETTY_SIMPLE(Word8)+GPRETTY_SIMPLE(Word16)+GPRETTY_SIMPLE(Word32)+GPRETTY_SIMPLE(Word64)+GPRETTY_SIMPLE(SomeIntN)+GPRETTY_SIMPLE(SomeWordN)+GPRETTY_SIMPLE(B.ByteString)+GPRETTY_SIMPLE(T.Text)+#endif++instance (KnownNat n, 1 <= n) => GPretty (IntN n) where+  gpretty = viaShow++instance (KnownNat n, 1 <= n) => GPretty (WordN n) where+  gpretty = viaShow++-- ()+instance GPretty () where+  gpretty = viaShow++-- Either+deriving via+  (Default (Either a b))+  instance+    (GPretty a, GPretty b) => GPretty (Either a b)++-- Maybe+deriving via+  (Default (Maybe a))+  instance+    (GPretty a) => GPretty (Maybe a)++-- List+instance (GPretty a) => GPretty [a] where+  gpretty = gprettyList++-- (,)+deriving via+  (Default (a, b))+  instance+    (GPretty a, GPretty b) => GPretty (a, b)++-- (,,)+deriving via+  (Default (a, b, c))+  instance+    (GPretty a, GPretty b, GPretty c) => GPretty (a, b, c)++-- (,,,)+deriving via+  (Default (a, b, c, d))+  instance+    ( GPretty a,+      GPretty b,+      GPretty c,+      GPretty d+    ) =>+    GPretty (a, b, c, d)++-- (,,,,)+deriving via+  (Default (a, b, c, d, e))+  instance+    ( GPretty a,+      GPretty b,+      GPretty c,+      GPretty d,+      GPretty e+    ) =>+    GPretty (a, b, c, d, e)++-- (,,,,,)+deriving via+  (Default (a, b, c, d, e, f))+  instance+    ( GPretty a,+      GPretty b,+      GPretty c,+      GPretty d,+      GPretty e,+      GPretty f+    ) =>+    GPretty (a, b, c, d, e, f)++-- (,,,,,,)+deriving via+  (Default (a, b, c, d, e, f, g))+  instance+    ( GPretty a,+      GPretty b,+      GPretty c,+      GPretty d,+      GPretty e,+      GPretty f,+      GPretty g+    ) =>+    GPretty (a, b, c, d, e, f, g)++-- (,,,,,,,)+deriving via+  (Default (a, b, c, d, e, f, g, h))+  instance+    ( GPretty a,+      GPretty b,+      GPretty c,+      GPretty d,+      GPretty e,+      GPretty f,+      GPretty g,+      GPretty h+    ) =>+    GPretty (a, b, c, d, e, f, g, h)++-- Sum+deriving via+  (Default (Sum f g a))+  instance+    (GPretty (f a), GPretty (g a)) =>+    GPretty (Sum f g a)++-- MaybeT+instance+  (GPretty (m (Maybe a))) =>+  GPretty (MaybeT m a)+  where+  gprettyPrec i (MaybeT a) =+    group $+      nest 2 $+        vsep+          [ "MaybeT",+            gprettyPrec 11 a+          ]++-- ExceptT+instance+  (GPretty (m (Either e a))) =>+  GPretty (ExceptT e m a)+  where+  gprettyPrec i (ExceptT a) =+    group $+      nest 2 $+        vsep+          [ "ExceptT",+            gprettyPrec 11 a+          ]++-- WriterT+instance+  (GPretty (m (a, w))) =>+  GPretty (WriterLazy.WriterT w m a)+  where+  gprettyPrec i (WriterLazy.WriterT a) =+    group $+      nest 2 $+        vsep+          [ "WriterT",+            gprettyPrec 11 a+          ]++instance+  (GPretty (m (a, w))) =>+  GPretty (WriterStrict.WriterT w m a)+  where+  gprettyPrec i (WriterStrict.WriterT a) =+    group $+      nest 2 $+        vsep+          [ "WriterT",+            gprettyPrec 11 a+          ]++-- Identity+instance (GPretty a) => GPretty (Identity a) where+  gprettyPrec i (Identity a) =+    group $+      nest 2 $+        vsep+          [ "Identity",+            gprettyPrec 11 a+          ]++-- IdentityT+instance (GPretty (m a)) => GPretty (IdentityT m a) where+  gprettyPrec i (IdentityT a) =+    group $+      nest 2 $+        vsep+          [ "IdentityT",+            gprettyPrec 11 a+          ]

@@ -87,6 +87,7 @@ import Data.Hashable import Data.Int import Data.String+import qualified Data.Text as T import Data.Typeable import Data.Word import GHC.TypeNats@@ -760,6 +761,7 @@ CONCRETE_GENSYM_SAME_SHAPE(SomeWordN) CONCRETE_GENSYM_SAME_SHAPE(SomeIntN) CONCRETE_GENSYM_SAME_SHAPE(B.ByteString)+CONCRETE_GENSYM_SAME_SHAPE(T.Text) CONCRETE_GENSYM_SAME_SHAPE_BV(WordN) CONCRETE_GENSYM_SAME_SHAPE_BV(IntN) @@ -779,6 +781,7 @@ CONCRETE_GENSYMSIMPLE_SAME_SHAPE(SomeWordN) CONCRETE_GENSYMSIMPLE_SAME_SHAPE(SomeIntN) CONCRETE_GENSYMSIMPLE_SAME_SHAPE(B.ByteString)+CONCRETE_GENSYMSIMPLE_SAME_SHAPE(T.Text) CONCRETE_GENSYMSIMPLE_SAME_SHAPE_BV(WordN) CONCRETE_GENSYMSIMPLE_SAME_SHAPE_BV(IntN) #endif

@@ -68,6 +68,7 @@ import Data.Int import Data.Kind import qualified Data.Monoid as Monoid+import qualified Data.Text as T import Data.Typeable import Data.Word import GHC.Natural@@ -458,6 +459,7 @@ CONCRETE_ORD_MERGEABLE(Word32) CONCRETE_ORD_MERGEABLE(Word64) CONCRETE_ORD_MERGEABLE(B.ByteString)+CONCRETE_ORD_MERGEABLE(T.Text) CONCRETE_ORD_MERGEABLE_BV(WordN) CONCRETE_ORD_MERGEABLE_BV(IntN) #endif

@@ -34,6 +34,7 @@ import qualified Data.ByteString as B import Data.Functor.Sum import Data.Int+import qualified Data.Text as T import Data.Word import GHC.TypeLits import Generics.Deriving@@ -249,6 +250,7 @@ CONCRETE_SORD(SomeWordN) CONCRETE_SORD(SomeIntN) CONCRETE_SORD(B.ByteString)+CONCRETE_SORD(T.Text) CONCRETE_SORD_BV(WordN) CONCRETE_SORD_BV(IntN) #endif

@@ -33,6 +33,7 @@ import qualified Data.ByteString as B import Data.Functor.Sum import Data.Int+import qualified Data.Text as T import Data.Word import GHC.TypeNats import Generics.Deriving@@ -119,6 +120,7 @@ CONCRETE_SUBSTITUTESYM(SomeWordN) CONCRETE_SUBSTITUTESYM(SomeIntN) CONCRETE_SUBSTITUTESYM(B.ByteString)+CONCRETE_SUBSTITUTESYM(T.Text) CONCRETE_SUBSTITUTESYM_BV(WordN) CONCRETE_SUBSTITUTESYM_BV(IntN) #endif

@@ -32,6 +32,7 @@ import qualified Data.ByteString as B import Data.Functor.Sum import Data.Int+import qualified Data.Text as T import Data.Word import GHC.Generics import GHC.TypeNats@@ -113,6 +114,7 @@ CONCRETE_TOCON(SomeWordN) CONCRETE_TOCON(SomeIntN) CONCRETE_TOCON(B.ByteString)+CONCRETE_TOCON(T.Text) CONCRETE_TOCON_BV(WordN) CONCRETE_TOCON_BV(IntN) #endif

@@ -35,6 +35,7 @@ import qualified Data.ByteString as B import Data.Functor.Sum import Data.Int+import qualified Data.Text as T import Data.Word import GHC.TypeNats import Generics.Deriving@@ -101,6 +102,7 @@ CONCRETE_TOSYM(SomeIntN) CONCRETE_TOSYM(SomeWordN) CONCRETE_TOSYM(B.ByteString)+CONCRETE_TOSYM(T.Text) CONCRETE_TOSYM_BV(IntN) CONCRETE_TOSYM_BV(WordN) #endif

@@ -1,7 +1,9 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveLift #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeFamilies #-} @@ -29,12 +31,19 @@ import Data.Hashable import GHC.Generics import Grisette.Core.Data.Class.Bool+import Grisette.Core.Data.Class.GPretty import Grisette.Core.Data.Class.Mergeable import Grisette.Core.Data.Class.SimpleMergeable import Grisette.Core.Data.Class.Solvable import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim import Language.Haskell.TH.Syntax +#if MIN_VERSION_prettyprinter(1,7,0)+import Prettyprinter+#else+import Data.Text.Prettyprint.Doc+#endif+ -- | The default union implementation. data Union a   = -- | A single value@@ -123,6 +132,20 @@  instance (Show a) => Show (Union a) where   showsPrec = showsPrec1++instance (GPretty a) => GPretty (Union a) where+  gprettyPrec n (Single a) = gprettyPrec n a+  gprettyPrec n (If _ _ cond t f) =+    group $+      condEnclose (n > 10) "(" ")" $+        align $+          nest 2 $+            vsep+              [ "If",+                gprettyPrec 11 cond,+                gprettyPrec 11 t,+                gprettyPrec 11 f+              ]  instance (Hashable a) => Hashable (Union a) where   s `hashWithSalt` (Single a) = s `hashWithSalt` (0 :: Int) `hashWithSalt` a

@@ -30,7 +30,6 @@  import Control.Monad.Except import Control.Monad.Trans.Maybe-import qualified Data.ByteString as B import Data.Int import Data.Word import Debug.Trace

@@ -1,4 +1,5 @@ {-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE CPP #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-}@@ -9,6 +10,8 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-}@@ -44,6 +47,7 @@     UTerm (..),     type (-->) (..),     buildGeneralFun,+    prettyPrintTerm,   ) where @@ -71,6 +75,12 @@ import Language.Haskell.TH.Syntax.Compat import Type.Reflection +#if MIN_VERSION_prettyprinter(1,7,0)+import Prettyprinter+#else+import Data.Text.Prettyprint.Doc+#endif+ -- $setup -- >>> import Grisette.Core -- >>> import Grisette.IR.SymPrim@@ -556,6 +566,21 @@     "QuotBoundedIntegral{id=" ++ show i ++ ", arg1=" ++ show arg1 ++ ", arg2=" ++ show arg2 ++ "}"   show (RemBoundedIntegralTerm i arg1 arg2) =     "RemBoundedIntegral{id=" ++ show i ++ ", arg1=" ++ show arg1 ++ ", arg2=" ++ show arg2 ++ "}"++prettyPrintTerm :: Term t -> Doc ann+prettyPrintTerm v =+  column+    ( \c ->+        pageWidth $ \case+          AvailablePerLine i r ->+            if fromIntegral (c + len) > fromIntegral i * r+              then "..."+              else pretty formatted+          Unbounded -> pretty formatted+    )+  where+    formatted = introSupportedPrimConstraint v $ pformat v+    len = length formatted  instance (SupportedPrim t) => Eq (Term t) where   (==) = (==) `on` identity

@@ -69,6 +69,7 @@ import Data.Int import Data.Proxy import Data.String+import qualified Data.Text as T import Data.Typeable import Data.Word import GHC.Generics@@ -82,6 +83,7 @@ import Grisette.Core.Data.Class.Evaluate import Grisette.Core.Data.Class.ExtractSymbolics import Grisette.Core.Data.Class.Function+import Grisette.Core.Data.Class.GPretty import Grisette.Core.Data.Class.GenSym import Grisette.Core.Data.Class.Mergeable import Grisette.Core.Data.Class.ModelOps@@ -606,6 +608,34 @@  -- Aggregate instances +-- Prettyprint+#define GPRETTY_SYM_SIMPLE(symtype) \+instance GPretty symtype where \+  gpretty (symtype t) = prettyPrintTerm t++#define GPRETTY_SYM_BV(symtype) \+instance (KnownNat n, 1 <= n) => GPretty (symtype n) where \+  gpretty (symtype t) = prettyPrintTerm t++#define GPRETTY_SYM_FUN(op, cons) \+instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb)\+  => GPretty (sa op sb) where \+  gpretty (cons t) = prettyPrintTerm t++#define GPRETTY_SYM_SOME_BV(symtype) \+instance GPretty symtype where \+  gpretty (symtype t) = gpretty t++#if 1+GPRETTY_SYM_SIMPLE(SymBool)+GPRETTY_SYM_SIMPLE(SymInteger)+GPRETTY_SYM_BV(SymIntN)+GPRETTY_SYM_BV(SymWordN)+GPRETTY_SYM_FUN(=~>, SymTabularFun)+GPRETTY_SYM_FUN(-~>, SymGeneralFun)+GPRETTY_SYM_SOME_BV(SomeSymIntN)+GPRETTY_SYM_SOME_BV(SomeSymWordN)+#endif -- Num  #define NUM_BV(symtype) \@@ -1509,6 +1539,7 @@ CONCRETE_ALLSYMS(Word32) CONCRETE_ALLSYMS(Word64) CONCRETE_ALLSYMS(B.ByteString)+CONCRETE_ALLSYMS(T.Text) ALLSYMS_SIMPLE(SymBool) ALLSYMS_SIMPLE(SymInteger) ALLSYMS_BV(SymIntN)

@@ -38,6 +38,7 @@ import Grisette.Core.Data.BV import Grisette.Core.Data.Class.Evaluate import Grisette.Core.Data.Class.ExtractSymbolics+import Grisette.Core.Data.Class.GPretty import Grisette.Core.Data.Class.Solvable import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term import Grisette.IR.SymPrim.Data.TabularFun@@ -89,6 +90,8 @@ instance EvaluateSym SymBool  instance ExtractSymbolics SymBool++instance GPretty SymBool  newtype SymInteger = SymInteger {underlyingIntegerTerm :: Term Integer} 

@@ -420,6 +420,13 @@             sizedBVSelect (Proxy :: Proxy 3) (Proxy :: Proxy 3) (0b1010000 :: IntN 8) @=? 0b10         ],       testGroup+        "read"+        [ testProperty "read . show" $ \(x :: IntN 8) -> read (show x) == x,+          testProperty "read . show" $ \(x :: WordN 8) -> read (show x) == x,+          testProperty "read . show" $ \(x :: IntN 9) -> read (show x) == x,+          testProperty "read . show" $ \(x :: WordN 9) -> read (show x) == x+        ],+      testGroup         "Regression"         [ testCase "division of min bound and minus one for signed bit vector should throw" $ do             shouldThrow "divMod" $ divMod (minBound :: IntN 8) (-1 :: IntN 8)

@@ -0,0 +1,342 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Grisette.Core.Data.Class.GPrettyTests where++import Data.Int+import Data.Text as T+import Data.Word+import GHC.Generics+import GHC.Stack+import Generics.Deriving+import Grisette.Core.Data.BV+import Grisette.Core.Data.Class.Bool+import Grisette.Core.Data.Class.GPretty+import Grisette.IR.SymPrim.Data.SymPrim+import Test.Tasty+import Test.Tasty.HUnit+import Test.Tasty.QuickCheck hiding ((.&.))++#if MIN_VERSION_prettyprinter(1,7,0)+import Prettyprinter+import Prettyprinter.Render.Text+#else+import Data.Text.Prettyprint.Doc+import Data.Text.Prettyprint.Doc.Render.Text+#endif++testGPretty :: (HasCallStack, GPretty a) => String -> Int -> a -> T.Text -> TestTree+testGPretty n i a s =+  testCase n $+    renderStrict+      ( layoutPretty+          (LayoutOptions $ AvailablePerLine i 1)+          (gpretty a)+      )+      @=? s++propertyGPrettyShow ::+  forall proxy a.+  (HasCallStack, GPretty a, Show a) =>+  String ->+  Gen a ->+  TestTree+propertyGPrettyShow n g =+  testProperty n $ forAll g $ \(a :: a) -> do+    renderStrict (layoutPretty (LayoutOptions Unbounded) (gpretty a)) == T.pack (show a)++propertyGPrettyRead ::+  forall proxy a.+  (HasCallStack, GPretty a, Read a, Show a, Eq a) =>+  String ->+  Gen a ->+  TestTree+propertyGPrettyRead n g =+  testProperty n $ \i -> forAll g $ \(a :: a) -> do+    read+      ( T.unpack+          ( renderStrict+              ( layoutPretty+                  (LayoutOptions $ AvailablePerLine (abs i) 0.8)+                  (gpretty a)+              )+          )+      )+      == a++propertyGPretty ::+  forall proxy a.+  (HasCallStack, GPretty a, Read a, Show a, Eq a) =>+  String ->+  Gen a ->+  TestTree+propertyGPretty n g =+  testGroup+    n+    [ propertyGPrettyShow "single line" g,+      propertyGPrettyRead "compact" g+    ]++data I5 a b = a :-: b+  deriving (Generic, Show, Read, Eq)+  deriving (GPretty) via (Default (I5 a b))++infixl 5 :-:++data I6 a b = a :--: b+  deriving (Generic, Show, Read, Eq)+  deriving (GPretty) via (Default (I6 a b))++infixl 6 :--:++instance+  (Arbitrary a, Arbitrary b) =>+  Arbitrary (I5 a b)+  where+  arbitrary = do+    a <- arbitrary+    b <- arbitrary+    return $ a :-: b++instance+  (Arbitrary a, Arbitrary b) =>+  Arbitrary (I6 a b)+  where+  arbitrary = do+    a <- arbitrary+    b <- arbitrary+    return $ a :--: b++data Record a b = Record {ra :: a, rb :: b}+  deriving (Generic, Show, Read, Eq)+  deriving (GPretty) via (Default (Record a b))++instance+  (Arbitrary a, Arbitrary b) =>+  Arbitrary (Record a b)+  where+  arbitrary = do+    a <- arbitrary+    Record a <$> arbitrary++gprettyTests :: TestTree+gprettyTests =+  testGroup+    "GPrettyTests"+    [ testGroup+        "simple tests"+        [ propertyGPretty "Bool" (arbitrary :: Gen Bool),+          propertyGPretty "Integer" (arbitrary :: Gen Integer),+          propertyGPretty "Int" (arbitrary :: Gen Int),+          propertyGPretty "Int8" (arbitrary :: Gen Int8),+          propertyGPretty "Int16" (arbitrary :: Gen Int16),+          propertyGPretty "Int32" (arbitrary :: Gen Int32),+          propertyGPretty "Int64" (arbitrary :: Gen Int64),+          propertyGPretty "Word" (arbitrary :: Gen Word),+          propertyGPretty "Word8" (arbitrary :: Gen Word8),+          propertyGPretty "Word16" (arbitrary :: Gen Word16),+          propertyGPretty "Word32" (arbitrary :: Gen Word32),+          propertyGPretty "Word64" (arbitrary :: Gen Word64),+          propertyGPrettyShow+            "SomeWordN"+            ( oneof+                [ SomeWordN <$> (arbitrary :: Gen (WordN 8)),+                  SomeWordN <$> (arbitrary :: Gen (WordN 9)),+                  SomeWordN <$> (arbitrary :: Gen (WordN 10))+                ]+            ),+          propertyGPretty "WordN 8" (arbitrary :: Gen (WordN 8)),+          propertyGPretty "WordN 9" (arbitrary :: Gen (WordN 9)),+          propertyGPrettyShow+            "SomeIntN"+            ( oneof+                [ SomeIntN <$> (arbitrary :: Gen (IntN 8)),+                  SomeIntN <$> (arbitrary :: Gen (IntN 9)),+                  SomeIntN <$> (arbitrary :: Gen (IntN 10))+                ]+            ),+          propertyGPretty "IntN 8" (arbitrary :: Gen (IntN 8)),+          propertyGPretty "IntN 9" (arbitrary :: Gen (IntN 9)),+          propertyGPretty "()" (arbitrary :: Gen ()),+          propertyGPretty+            "Either"+            ( arbitrary :: Gen (Either Int Bool)+            ),+          propertyGPretty+            "Maybe"+            ( arbitrary :: Gen (Maybe Int)+            ),+          propertyGPretty+            "List"+            ( arbitrary :: Gen [Int]+            ),+          propertyGPretty+            "(,)"+            ( arbitrary :: Gen (Int, Int)+            ),+          propertyGPretty+            "(,,)"+            ( arbitrary :: Gen (Int, Int, Int)+            ),+          propertyGPretty+            "(,,,)"+            ( arbitrary :: Gen (Int, Int, Int, Int)+            ),+          propertyGPretty+            "(,,,,)"+            ( arbitrary :: Gen (Int, Int, Int, Int, Int)+            ),+          propertyGPretty+            "(,,,,,)"+            ( arbitrary :: Gen (Int, Int, Int, Int, Int, Int)+            ),+          propertyGPretty+            "(,,,,,,)"+            ( arbitrary :: Gen (Int, Int, Int, Int, Int, Int, Int)+            ),+          propertyGPretty+            "(,,,,,,,)"+            ( arbitrary :: Gen (Int, Int, Int, Int, Int, Int, Int, Int)+            ),+          propertyGPretty+            "I5"+            ( arbitrary :: Gen (I5 Int Int)+            ),+          propertyGPretty+            "Record"+            ( arbitrary :: Gen (Record Int Int)+            )+        ],+      testGroup+        "Combined types"+        [ propertyGPretty+            "Maybe Maybe"+            ( arbitrary :: Gen (Maybe (Maybe Int))+            ),+          propertyGPretty+            "Maybe (,)"+            ( arbitrary :: Gen (Maybe (Int, Int))+            ),+          propertyGPretty+            "Maybe I5"+            ( arbitrary :: Gen (Maybe (I5 Int Int))+            ),+          propertyGPretty+            "Maybe []"+            ( arbitrary :: Gen (Maybe [Int])+            ),+          propertyGPretty+            "Maybe Record"+            ( arbitrary :: Gen (Maybe (Record Int Int))+            ),+          propertyGPretty+            "(Maybe,Either)"+            ( arbitrary :: Gen (Maybe Int, Either Int Int)+            ),+          propertyGPretty+            "((,),(,))"+            ( arbitrary :: Gen ((Int, Int), (Int, Int))+            ),+          propertyGPretty+            "(I5,I5)"+            ( arbitrary :: Gen (I5 Int Int, I5 Int Int)+            ),+          propertyGPretty+            "([],[])"+            ( arbitrary :: Gen ([Int], [Int])+            ),+          propertyGPretty+            "(Record,Record)"+            ( arbitrary :: Gen (Record Int Int, Record Int Int)+            ),+          propertyGPretty+            "I5 Maybe Either"+            ( arbitrary :: Gen (I5 (Maybe Int) (Either Int Int))+            ),+          propertyGPretty+            "I5 (,) (,)"+            ( arbitrary :: Gen (I5 (Int, Int) (Int, Int))+            ),+          propertyGPretty+            "I5 I6 I6"+            ( arbitrary :: Gen (I5 (I6 Int Int) (I6 Int Int))+            ),+          propertyGPretty+            "I5 I5 I5"+            ( arbitrary :: Gen (I5 (I5 Int Int) (I5 Int Int))+            ),+          propertyGPretty+            "I6 I5 I5"+            ( arbitrary :: Gen (I6 (I5 Int Int) (I5 Int Int))+            ),+          propertyGPretty+            "I6 I6 I6"+            ( arbitrary :: Gen (I6 (I6 Int Int) (I6 Int Int))+            ),+          propertyGPretty+            "I5 [] []"+            ( arbitrary :: Gen (I5 [Int] [Int])+            ),+          propertyGPretty+            "I5 Record Record"+            ( arbitrary :: Gen (I5 (Record Int Int) (Record Int Int))+            ),+          propertyGPretty+            "[Maybe]"+            ( arbitrary :: Gen [Maybe Int]+            ),+          propertyGPretty+            "[(,)]"+            ( arbitrary :: Gen [(Int, Int)]+            ),+          propertyGPretty+            "[I5]"+            ( arbitrary :: Gen [I5 Int Int]+            ),+          propertyGPretty+            "[[]]"+            ( arbitrary :: Gen [[Int]]+            ),+          propertyGPretty+            "[Record]"+            ( arbitrary :: Gen [Record Int Int]+            ),+          propertyGPretty+            "Record Maybe Either"+            ( arbitrary :: Gen (Record (Maybe Int) (Either Int Int))+            ),+          propertyGPretty+            "Record (,) (,)"+            ( arbitrary :: Gen (Record (Int, Int) (Int, Int))+            ),+          propertyGPretty+            "Record I5 I6"+            ( arbitrary :: Gen (Record (I5 Int Int) (I6 Int Int))+            ),+          propertyGPretty+            "Record []"+            ( arbitrary :: Gen (Record [Int] [Int])+            ),+          propertyGPretty+            "Record Record"+            ( arbitrary :: Gen (Record (Record Int Int) (Record Int Int))+            )+        ],+      testGroup+        "Symbolic types"+        [ testGPretty+            "enough space"+            80+            ("a" &&~ "b" :: SymBool)+            "(&& a b)",+          testGPretty+            "not enough space"+            6+            ("a" &&~ "b" :: SymBool)+            "..."+        ]+    ]

@@ -27,6 +27,7 @@ import Grisette.Backend.SBV.Data.SMT.TermRewritingTests import Grisette.Core.Control.Monad.UnionMTests import qualified Grisette.Core.Data.BVTests+import Grisette.Core.Data.Class.GPrettyTests import qualified Grisette.IR.SymPrim.Data.Prim.BVTests import Grisette.IR.SymPrim.Data.Prim.BitsTests import Grisette.IR.SymPrim.Data.Prim.BoolTests@@ -56,9 +57,17 @@ coreTests :: TestTree coreTests =   testGroup-    "Grisette.Core.Control.Monad.UnionM"-    [ unionMTests,-      Grisette.Core.Data.BVTests.bvTests+    "core"+    [ testGroup+        "Grisette.Core.Control.Monad.UnionM"+        [unionMTests],+      testGroup+        "Grisette.Core.Data"+        [ testGroup+            "Class"+            [gprettyTests],+          Grisette.Core.Data.BVTests.bvTests+        ]     ]  {-