{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint () where
import Control.Monad.Except (ExceptT)
import Control.Monad.Identity
( Identity (Identity),
IdentityT (IdentityT),
)
import Control.Monad.Trans.Maybe (MaybeT)
import qualified Control.Monad.Writer.Lazy as WriterLazy
import qualified Control.Monad.Writer.Strict as WriterStrict
import qualified Data.ByteString as B
import qualified Data.ByteString.Char8 as C
import Data.Functor.Compose (Compose (Compose))
import Data.Functor.Const (Const)
import Data.Functor.Product (Product)
import Data.Functor.Sum (Sum)
import qualified Data.HashMap.Lazy as HM
import qualified Data.HashSet as HS
import Data.Int (Int16, Int32, Int64, Int8)
import Data.Monoid (Alt, Ap)
import qualified Data.Monoid as Monoid
import Data.Ord (Down)
import Data.Proxy (Proxy)
import Data.Ratio (Ratio, denominator, numerator)
import qualified Data.Text as T
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.Generics
( K1 (K1),
M1 (M1),
Par1 (Par1),
Rec1 (Rec1),
V1,
(:.:) (Comp1),
type (:*:),
)
import GHC.Real (ratioPrec, ratioPrec1)
import GHC.TypeLits (KnownNat, type (<=))
import Generics.Deriving
( Default (Default),
Default1 (Default1),
U1,
(:+:),
)
import Grisette.Internal.Core.Control.Exception
( AssertionError,
VerificationConditions,
)
import Grisette.Internal.Core.Data.Symbol (Identifier, Symbol)
import Grisette.Internal.Internal.Decl.Core.Data.Class.PPrint
( Doc,
PPrint (pformat, pformatList, pformatPrec),
PPrint1 (liftPFormatList, liftPFormatPrec),
PPrint2 (liftPFormatList2, liftPFormatPrec2),
Pretty (pretty),
condEnclose,
pformatListLike,
pformatPrec1,
pformatWithConstructor,
viaShow,
viaShowsPrec,
)
import Grisette.Internal.SymPrim.AlgReal (AlgReal)
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.FP
( FP,
FPRoundingMode,
NotRepresentableFPError,
ValidFP,
)
import Grisette.Internal.SymPrim.GeneralFun (type (-->))
import Grisette.Internal.SymPrim.Prim.Internal.Term (Term)
import Grisette.Internal.SymPrim.Prim.Model
( Model (Model),
SymbolSet (SymbolSet),
)
import Grisette.Internal.SymPrim.Prim.SomeTerm (SomeTerm (SomeTerm))
import Grisette.Internal.SymPrim.Prim.Term
( ModelValue,
SomeTypedSymbol (SomeTypedSymbol),
TypedSymbol (unTypedSymbol),
prettyPrintTerm,
)
import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal (SymAlgReal))
import Grisette.Internal.SymPrim.SymBV
( SymIntN (SymIntN),
SymWordN (SymWordN),
)
import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))
import Grisette.Internal.SymPrim.SymFP
( SymFP (SymFP),
SymFPRoundingMode (SymFPRoundingMode),
)
import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>) (SymGeneralFun))
import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger))
import Grisette.Internal.SymPrim.SymTabularFun (type (=~>) (SymTabularFun))
import Grisette.Internal.SymPrim.TabularFun (type (=->))
import Grisette.Internal.TH.Derivation.Derive (derive)
#define FORMAT_SIMPLE(type) \
instance PPrint type where pformatPrec = viaShowsPrec showsPrec
#if 1
FORMAT_SIMPLE(Bool)
FORMAT_SIMPLE(Integer)
FORMAT_SIMPLE(Int)
FORMAT_SIMPLE(Int8)
FORMAT_SIMPLE(Int16)
FORMAT_SIMPLE(Int32)
FORMAT_SIMPLE(Int64)
FORMAT_SIMPLE(Word)
FORMAT_SIMPLE(Word8)
FORMAT_SIMPLE(Word16)
FORMAT_SIMPLE(Word32)
FORMAT_SIMPLE(Word64)
FORMAT_SIMPLE(Float)
FORMAT_SIMPLE(Double)
FORMAT_SIMPLE(FPRoundingMode)
FORMAT_SIMPLE(Monoid.All)
FORMAT_SIMPLE(Monoid.Any)
FORMAT_SIMPLE(Ordering)
FORMAT_SIMPLE(AlgReal)
#endif
instance PPrint (Proxy a) where
pformatPrec :: forall ann. Int -> Proxy a -> Doc ann
pformatPrec Int
_ Proxy a
_ = Doc ann
"Proxy"
{-# INLINE pformatPrec #-}
instance PPrint1 Proxy where
liftPFormatPrec :: forall a ann.
(Int -> a -> Doc ann)
-> ([a] -> Doc ann) -> Int -> Proxy a -> Doc ann
liftPFormatPrec Int -> a -> Doc ann
_ [a] -> Doc ann
_ Int
_ Proxy a
_ = Doc ann
"Proxy"
{-# INLINE liftPFormatPrec #-}
instance (PPrint a) => PPrint (Ratio a) where
pformatPrec :: forall ann. Int -> Ratio a -> Doc ann
pformatPrec Int
p Ratio a
r =
Bool -> Doc ann -> Doc ann -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann -> Doc ann -> Doc ann
condEnclose (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
ratioPrec) Doc ann
"(" Doc ann
")" (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
Int -> a -> Doc ann
forall ann. Int -> a -> Doc ann
forall a ann. PPrint a => Int -> a -> Doc ann
pformatPrec Int
ratioPrec1 (Ratio a -> a
forall a. Ratio a -> a
numerator Ratio a
r)
Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"%"
Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Int -> a -> Doc ann
forall ann. Int -> a -> Doc ann
forall a ann. PPrint a => Int -> a -> Doc ann
pformatPrec Int
ratioPrec1 (Ratio a -> a
forall a. Ratio a -> a
denominator Ratio a
r)
instance PPrint B.ByteString where
pformat :: forall ann. ByteString -> Doc ann
pformat = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String -> Doc ann)
-> (ByteString -> String) -> ByteString -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> String
C.unpack
instance PPrint T.Text where
pformat :: forall ann. Text -> Doc ann
pformat = Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Text -> Doc ann
pretty
instance (KnownNat n, 1 <= n) => PPrint (IntN n) where
pformat :: forall ann. IntN n -> Doc ann
pformat = IntN n -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow
instance (KnownNat n, 1 <= n) => PPrint (WordN n) where
pformat :: forall ann. WordN n -> Doc ann
pformat = WordN n -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow
instance (ValidFP eb sb) => PPrint (FP eb sb) where
pformat :: forall ann. FP eb sb -> Doc ann
pformat = FP eb sb -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow
instance (Show a, Show b) => PPrint (a =-> b) where
pformat :: forall ann. (a =-> b) -> Doc ann
pformat = (a =-> b) -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow
instance PPrint (a --> b) where
pformat :: forall ann. (a --> b) -> Doc ann
pformat = (a --> b) -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow
instance PPrint (Term t) where
pformat :: forall ann. Term t -> Doc ann
pformat = Term t -> Doc ann
forall t ann. Term t -> Doc ann
prettyPrintTerm
instance PPrint SomeTerm where
pformat :: forall ann. SomeTerm -> Doc ann
pformat (SomeTerm Term a
t) = Term a -> Doc ann
forall t ann. Term t -> Doc ann
prettyPrintTerm Term a
t
#define FORMAT_SYM_SIMPLE(symtype) \
instance PPrint symtype where \
pformat (symtype t) = prettyPrintTerm t
#define FORMAT_SYM_BV(symtype) \
instance (KnownNat n, 1 <= n) => PPrint (symtype n) where \
pformat (symtype t) = prettyPrintTerm t
#define FORMAT_SYM_FUN(op, cons) \
instance PPrint (sa op sb) where \
pformat (cons t) = prettyPrintTerm t
#if 1
FORMAT_SYM_SIMPLE(SymBool)
FORMAT_SYM_SIMPLE(SymInteger)
FORMAT_SYM_SIMPLE(SymFPRoundingMode)
FORMAT_SYM_SIMPLE(SymAlgReal)
FORMAT_SYM_BV(SymIntN)
FORMAT_SYM_BV(SymWordN)
FORMAT_SYM_FUN(=~>, SymTabularFun)
FORMAT_SYM_FUN(-~>, SymGeneralFun)
#endif
instance (ValidFP eb sb) => PPrint (SymFP eb sb) where
pformat :: forall ann. SymFP eb sb -> Doc ann
pformat (SymFP Term (FP eb sb)
t) = Term (FP eb sb) -> Doc ann
forall t ann. Term t -> Doc ann
prettyPrintTerm Term (FP eb sb)
t
derive
[ ''(),
''AssertionError,
''VerificationConditions,
''NotRepresentableFPError
]
[''PPrint]