    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Core.Kind
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Internal data-structures for the sbv library
    -----------------------------------------------------------------------------

    {-# LANGUAGE CPP                  #-}
    {-# LANGUAGE DataKinds            #-}
    {-# LANGUAGE DefaultSignatures    #-}
    {-# LANGUAGE DeriveDataTypeable   #-}
    {-# LANGUAGE FlexibleInstances    #-}
    {-# LANGUAGE LambdaCase           #-}
    {-# LANGUAGE ScopedTypeVariables  #-}
    {-# LANGUAGE TypeFamilies         #-}
    {-# LANGUAGE TypeApplications     #-}
    {-# LANGUAGE TypeOperators        #-}
    {-# LANGUAGE ViewPatterns         #-}
    {-# LANGUAGE UndecidableInstances #-}

    {-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}

    module Data.SBV.Core.Kind (
              Kind(..), HasKind(..), constructUKind, smtType, hasUninterpretedSorts
            , BVIsNonZero, ValidFloat, intOfProxy
            , showBaseKind, needsFlattening, RoundingMode(..), smtRoundingMode
            ) where

    import qualified Data.Generics as G (Data(..), DataType, dataTypeName, dataTypeOf, tyconUQname, dataTypeConstrs, constrFields)

    import Data.Char (isSpace)

    import Data.Int
    import Data.Word
    import Data.SBV.Core.AlgReals

    import Data.Proxy
    import Data.Kind

    import Data.List (isPrefixOf, intercalate)

    import Data.Typeable (Typeable)
    import Data.Type.Bool
    import Data.Type.Equality

    import GHC.TypeLits

    import Data.SBV.Utils.Lib (isKString)

    -- | Kind of symbolic value
    data Kind = KBool
              | KBounded !Bool !Int
              | KUnbounded
              | KReal
              | KUserSort String (Maybe [String])  -- name. Uninterpreted, or enumeration constants.
              | KFloat
              | KDouble
              | KFP !Int !Int
              | KChar
              | KString
              | KList Kind
              | KSet  Kind
              | KTuple [Kind]
              | KMaybe  Kind
              | KRational
              | KEither Kind Kind
              deriving (Kind -> Kind -> Bool
    (Kind -> Kind -> Bool) -> (Kind -> Kind -> Bool) -> Eq Kind
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Kind -> Kind -> Bool
    == :: Kind -> Kind -> Bool
    $c/= :: Kind -> Kind -> Bool
    /= :: Kind -> Kind -> Bool
    Eq, Eq Kind
    Eq Kind =>
    (Kind -> Kind -> Ordering)
    -> (Kind -> Kind -> Bool)
    -> (Kind -> Kind -> Bool)
    -> (Kind -> Kind -> Bool)
    -> (Kind -> Kind -> Bool)
    -> (Kind -> Kind -> Kind)
    -> (Kind -> Kind -> Kind)
    -> Ord Kind
    Kind -> Kind -> Bool
    Kind -> Kind -> Ordering
    Kind -> Kind -> Kind
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: Kind -> Kind -> Ordering
    compare :: Kind -> Kind -> Ordering
    $c< :: Kind -> Kind -> Bool
    < :: Kind -> Kind -> Bool
    $c<= :: Kind -> Kind -> Bool
    <= :: Kind -> Kind -> Bool
    $c> :: Kind -> Kind -> Bool
    > :: Kind -> Kind -> Bool
    $c>= :: Kind -> Kind -> Bool
    >= :: Kind -> Kind -> Bool
    $cmax :: Kind -> Kind -> Kind
    max :: Kind -> Kind -> Kind
    $cmin :: Kind -> Kind -> Kind
    min :: Kind -> Kind -> Kind
    Ord, Typeable Kind
    Typeable Kind =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> Kind -> c Kind)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c Kind)
    -> (Kind -> Constr)
    -> (Kind -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c Kind))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Kind))
    -> ((forall b. Data b => b -> b) -> Kind -> Kind)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r)
    -> (forall u. (forall d. Data d => d -> u) -> Kind -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> Kind -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> Kind -> m Kind)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Kind -> m Kind)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> Kind -> m Kind)
    -> Data Kind
    Kind -> Constr
    Kind -> DataType
    (forall b. Data b => b -> b) -> Kind -> Kind
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> Kind -> u
    forall u. (forall d. Data d => d -> u) -> Kind -> [u]
    forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r
    forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Kind -> m Kind
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Kind -> m Kind
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Kind
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Kind -> c Kind
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Kind)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Kind)
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Kind -> c Kind
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Kind -> c Kind
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Kind
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Kind
    $ctoConstr :: Kind -> Constr
    toConstr :: Kind -> Constr
    $cdataTypeOf :: Kind -> DataType
    dataTypeOf :: Kind -> DataType
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Kind)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Kind)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Kind)
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Kind)
    $cgmapT :: (forall b. Data b => b -> b) -> Kind -> Kind
    gmapT :: (forall b. Data b => b -> b) -> Kind -> Kind
    $cgmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r
    gmapQl :: forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r
    gmapQr :: forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Kind -> [u]
    gmapQ :: forall u. (forall d. Data d => d -> u) -> Kind -> [u]
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Kind -> u
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Kind -> u
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Kind -> m Kind
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Kind -> m Kind
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Kind -> m Kind
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Kind -> m Kind
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Kind -> m Kind
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Kind -> m Kind
    G.Data)

    -- | The interesting about the show instance is that it can tell apart two kinds nicely; since it conveniently
    -- ignores the enumeration constructors. Also, when we construct a 'KUserSort', we make sure we don't use any of
    -- the reserved names; see 'constructUKind' for details.
    instance Show Kind where
      show :: Kind -> String
    show Kind
    KBool              = String
    "SBool"
      show (KBounded Bool
    False Int
    n) = Int -> String -> ShowS
    pickType Int
    n String
    "SWord" String
    "SWord " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n
      show (KBounded Bool
    True Int
    n)  = Int -> String -> ShowS
    pickType Int
    n String
    "SInt"  String
    "SInt "  String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n
      show Kind
    KUnbounded         = String
    "SInteger"
      show Kind
    KReal              = String
    "SReal"
      show (KUserSort String
    s Maybe [String]
    _)    = String
    s
      show Kind
    KFloat             = String
    "SFloat"
      show Kind
    KDouble            = String
    "SDouble"
      show (KFP Int
    eb Int
    sb)        = String
    "SFloatingPoint " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    eb String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    sb
      show Kind
    KString            = String
    "SString"
      show Kind
    KChar              = String
    "SChar"
      show (KList Kind
    e)          = String
    "[" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    e String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "]"
      show (KSet  Kind
    e)          = String
    "{" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    e String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "}"
      show (KTuple [Kind]
    m)         = String
    "(" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " (Kind -> String
    forall a. Show a => a -> String
    show (Kind -> String) -> [Kind] -> [String]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Kind]
    m) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
      show (KMaybe Kind
    k)         = String
    "SMaybe "  String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    kindParen (Kind -> String
    showBaseKind Kind
    k)
      show (KEither Kind
    k1 Kind
    k2)    = String
    "SEither " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    kindParen (Kind -> String
    showBaseKind Kind
    k1) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    kindParen (Kind -> String
    showBaseKind Kind
    k2)
      show Kind
    KRational          = String
    "SRational"

    -- | A version of show for kinds that says Bool instead of SBool
    showBaseKind :: Kind -> String
    showBaseKind :: Kind -> String
    showBaseKind = Kind -> String
    sh
      where sh :: Kind -> String
    sh k :: Kind
    k@Kind
    KBool            = ShowS
    noS (Kind -> String
    forall a. Show a => a -> String
    show Kind
    k)
            sh (KBounded Bool
    False Int
    n) = Int -> String -> ShowS
    pickType Int
    n String
    "Word" String
    "WordN " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n
            sh (KBounded Bool
    True Int
    n)  = Int -> String -> ShowS
    pickType Int
    n String
    "Int"  String
    "IntN "  String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n
            sh k :: Kind
    k@Kind
    KUnbounded       = ShowS
    noS (Kind -> String
    forall a. Show a => a -> String
    show Kind
    k)
            sh k :: Kind
    k@Kind
    KReal            = ShowS
    noS (Kind -> String
    forall a. Show a => a -> String
    show Kind
    k)
            sh k :: Kind
    k@KUserSort{}      = Kind -> String
    forall a. Show a => a -> String
    show Kind
    k     -- Leave user-sorts untouched!
            sh k :: Kind
    k@Kind
    KFloat           = ShowS
    noS (Kind -> String
    forall a. Show a => a -> String
    show Kind
    k)
            sh k :: Kind
    k@Kind
    KDouble          = ShowS
    noS (Kind -> String
    forall a. Show a => a -> String
    show Kind
    k)
            sh k :: Kind
    k@KFP{}            = ShowS
    noS (Kind -> String
    forall a. Show a => a -> String
    show Kind
    k)
            sh k :: Kind
    k@Kind
    KChar            = ShowS
    noS (Kind -> String
    forall a. Show a => a -> String
    show Kind
    k)
            sh k :: Kind
    k@Kind
    KString          = ShowS
    noS (Kind -> String
    forall a. Show a => a -> String
    show Kind
    k)
            sh Kind
    KRational          = String
    "Rational"
            sh (KList Kind
    k)          = String
    "[" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    sh Kind
    k String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "]"
            sh (KSet Kind
    k)           = String
    "{" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    sh Kind
    k String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "}"
            sh (KTuple [Kind]
    ks)        = String
    "(" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " ((Kind -> String) -> [Kind] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Kind -> String
    sh [Kind]
    ks) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            sh (KMaybe Kind
    k)         = String
    "Maybe "  String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    kindParen (Kind -> String
    sh Kind
    k)
            sh (KEither Kind
    k1 Kind
    k2)    = String
    "Either " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    kindParen (Kind -> String
    sh Kind
    k1) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    kindParen (Kind -> String
    sh Kind
    k2)

            -- Drop the initial S if it's there
            noS :: ShowS
    noS (Char
    'S':String
    s) = String
    s
            noS String
    s       = String
    s

    -- For historical reasons, we show 8-16-32-64 bit values with no space; others with a space.
    pickType :: Int -> String -> String -> String
    pickType :: Int -> String -> ShowS
    pickType Int
    i String
    standard String
    other
      | Int
    i Int -> [Int] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Int
    8, Int
    16, Int
    32, Int
    64] = String
    standard
      | Bool
    True                     = String
    other

    -- | Put parens if necessary. This test is rather crummy, but seems to work ok
    kindParen :: String -> String
    kindParen :: ShowS
    kindParen s :: String
    s@(Char
    '[':String
    _) = String
    s
    kindParen s :: String
    s@(Char
    '(':String
    _) = String
    s
    kindParen String
    s | (Char -> Bool) -> String -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Char -> Bool
    isSpace String
    s = Char
    '(' Char -> ShowS
    forall a. a -> [a] -> [a]
    : String
    s String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
                | Bool
    True          = String
    s

    -- | How the type maps to SMT land
    smtType :: Kind -> String
    smtType :: Kind -> String
    smtType Kind
    KBool           = String
    "Bool"
    smtType (KBounded Bool
    _ Int
    sz) = String
    "(_ BitVec " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    sz String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
    smtType Kind
    KUnbounded      = String
    "Int"
    smtType Kind
    KReal           = String
    "Real"
    smtType Kind
    KFloat          = String
    "(_ FloatingPoint  8 24)"
    smtType Kind
    KDouble         = String
    "(_ FloatingPoint 11 53)"
    smtType (KFP Int
    eb Int
    sb)     = String
    "(_ FloatingPoint " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    eb String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    sb String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
    smtType Kind
    KString         = String
    "String"
    smtType Kind
    KChar           = String
    "String"
    smtType (KList Kind
    k)       = String
    "(Seq "   String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    k String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
    smtType (KSet  Kind
    k)       = String
    "(Array " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    k String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " Bool)"
    smtType (KUserSort String
    s Maybe [String]
    _) = String
    s
    smtType (KTuple [])     = String
    "SBVTuple0"
    smtType (KTuple [Kind]
    kinds)  = String
    "(SBVTuple" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show ([Kind] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Kind]
    kinds) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords (Kind -> String
    smtType (Kind -> String) -> [Kind] -> [String]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Kind]
    kinds) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
    smtType Kind
    KRational       = String
    "SBVRational"
    smtType (KMaybe Kind
    k)      = String
    "(SBVMaybe " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    k String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
    smtType (KEither Kind
    k1 Kind
    k2) = String
    "(SBVEither "  String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    k1 String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    k2 String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"

    instance Eq  G.DataType where
       DataType
    a == :: DataType -> DataType -> Bool
    == DataType
    b = ShowS
    G.tyconUQname (DataType -> String
    G.dataTypeName DataType
    a) String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == ShowS
    G.tyconUQname (DataType -> String
    G.dataTypeName DataType
    b)

    instance Ord G.DataType where
       DataType
    a compare :: DataType -> DataType -> Ordering
    `compare` DataType
    b = ShowS
    G.tyconUQname (DataType -> String
    G.dataTypeName DataType
    a) String -> String -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare` ShowS
    G.tyconUQname (DataType -> String
    G.dataTypeName DataType
    b)

    -- | Does this kind represent a signed quantity?
    kindHasSign :: Kind -> Bool
    kindHasSign :: Kind -> Bool
    kindHasSign = \case Kind
    KBool        -> Bool
    False
                        KBounded Bool
    b Int
    _ -> Bool
    b
                        Kind
    KUnbounded   -> Bool
    True
                        Kind
    KReal        -> Bool
    True
                        Kind
    KFloat       -> Bool
    True
                        Kind
    KDouble      -> Bool
    True
                        KFP{}        -> Bool
    True
                        Kind
    KRational    -> Bool
    True
                        KUserSort{}  -> Bool
    False
                        Kind
    KString      -> Bool
    False
                        Kind
    KChar        -> Bool
    False
                        KList{}      -> Bool
    False
                        KSet{}       -> Bool
    False
                        KTuple{}     -> Bool
    False
                        KMaybe{}     -> Bool
    False
                        KEither{}    -> Bool
    False

    -- | Construct an uninterpreted/enumerated kind from a piece of data; we distinguish simple enumerations as those
    -- are mapped to proper SMT-Lib2 data-types; while others go completely uninterpreted
    constructUKind :: forall a. (Read a, G.Data a) => a -> Kind
    constructUKind :: forall a. (Read a, Data a) => a -> Kind
    constructUKind a
    a
      | (String -> Bool) -> [String] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (String -> String -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isPrefixOf` String
    sortName) [String]
    badPrefixes
      = String -> Kind
    forall a. HasCallStack => String -> a
    error (String -> Kind) -> String -> Kind
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ String
    "*** Data.SBV: Cannot construct user-sort with name: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    sortName
                        , String
    "***"
                        , String
    "***  Must not start with any of: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " [String]
    badPrefixes
                        ]
      | Bool
    True
      = case ([Constr]
    constrs, (Constr -> [String]) -> [Constr] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Constr -> [String]
    G.constrFields [Constr]
    constrs) of
          ([], [String]
    _)  -> String -> Maybe [String] -> Kind
    KUserSort String
    sortName   Maybe [String]
    forall a. Maybe a
    Nothing
          ([Constr]
    cs, []) -> String -> Maybe [String] -> Kind
    KUserSort String
    sortName (Maybe [String] -> Kind) -> Maybe [String] -> Kind
    forall a b. (a -> b) -> a -> b
    $ [String] -> Maybe [String]
    forall a. a -> Maybe a
    Just ((Constr -> String) -> [Constr] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Constr -> String
    forall a. Show a => a -> String
    show [Constr]
    cs)
          ([Constr], [String])
    _        -> String -> Kind
    forall a. HasCallStack => String -> a
    error (String -> Kind) -> String -> Kind
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ String
    "*** Data.SBV: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    sortName String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " is not an enumeration."
                                      , String
    "***"
                                      , String
    "*** To declare an enumeration, constructors should not have any fields."
                                      , String
    "*** To declare an uninterpreted sort, use a datatype with no constructors."
                                      ]

      where -- make sure we don't step on ourselves:
            -- NB. The sort "RoundingMode" is special. It's treated by SBV as a user-defined
            -- sort, even though it's internally handled differently. So, that name doesn't appear
            -- below.
            badPrefixes :: [String]
    badPrefixes = [ String
    "SBool",   String
    "SWord", String
    "SInt", String
    "SInteger", String
    "SReal",  String
    "SFloat", String
    "SDouble"
                          , String
    "SString", String
    "SChar", String
    "[",    String
    "SSet",     String
    "STuple", String
    "SMaybe", String
    "SEither"
                          , String
    "SRational"
                          ]

            dataType :: DataType
    dataType    = a -> DataType
    forall a. Data a => a -> DataType
    G.dataTypeOf a
    a
            sortName :: String
    sortName    = ShowS
    G.tyconUQname ShowS -> (DataType -> String) -> DataType -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DataType -> String
    G.dataTypeName (DataType -> String) -> DataType -> String
    forall a b. (a -> b) -> a -> b
    $ DataType
    dataType
            constrs :: [Constr]
    constrs     = DataType -> [Constr]
    G.dataTypeConstrs DataType
    dataType

    -- | A class for capturing values that have a sign and a size (finite or infinite)
    -- minimal complete definition: kindOf, unless you can take advantage of the default
    -- signature: This class can be automatically derived for data-types that have
    -- a 'G.Data' instance; this is useful for creating uninterpreted sorts. So, in
    -- reality, end users should almost never need to define any methods.
    class HasKind a where
      kindOf      :: a -> Kind
      hasSign     :: a -> Bool
      intSizeOf   :: a -> Int
      isBoolean   :: a -> Bool
      isBounded   :: a -> Bool   -- NB. This really means word/int; i.e., Real/Float will test False
      isReal      :: a -> Bool
      isFloat     :: a -> Bool
      isDouble    :: a -> Bool
      isRational  :: a -> Bool
      isFP        :: a -> Bool
      isUnbounded :: a -> Bool
      isUserSort  :: a -> Bool
      isChar      :: a -> Bool
      isString    :: a -> Bool
      isList      :: a -> Bool
      isSet       :: a -> Bool
      isTuple     :: a -> Bool
      isMaybe     :: a -> Bool
      isEither    :: a -> Bool
      showType    :: a -> String
      -- defaults
      hasSign a
    x = Kind -> Bool
    kindHasSign (a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    x)

      intSizeOf a
    x = case a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    x of
                      Kind
    KBool         -> String -> Int
    forall a. HasCallStack => String -> a
    error String
    "SBV.HasKind.intSizeOf((S)Bool)"
                      KBounded Bool
    _ Int
    s  -> Int
    s
                      Kind
    KUnbounded    -> String -> Int
    forall a. HasCallStack => String -> a
    error String
    "SBV.HasKind.intSizeOf((S)Integer)"
                      Kind
    KReal         -> String -> Int
    forall a. HasCallStack => String -> a
    error String
    "SBV.HasKind.intSizeOf((S)Real)"
                      Kind
    KFloat        -> Int
    32
                      Kind
    KDouble       -> Int
    64
                      KFP Int
    i Int
    j       -> Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    j
                      Kind
    KRational     -> String -> Int
    forall a. HasCallStack => String -> a
    error String
    "SBV.HasKind.intSizeOf((S)Rational)"
                      KUserSort String
    s Maybe [String]
    _ -> String -> Int
    forall a. HasCallStack => String -> a
    error (String -> Int) -> String -> Int
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.HasKind.intSizeOf: Uninterpreted sort: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    s
                      Kind
    KString       -> String -> Int
    forall a. HasCallStack => String -> a
    error String
    "SBV.HasKind.intSizeOf((S)Double)"
                      Kind
    KChar         -> String -> Int
    forall a. HasCallStack => String -> a
    error String
    "SBV.HasKind.intSizeOf((S)Char)"
                      KList Kind
    ek      -> String -> Int
    forall a. HasCallStack => String -> a
    error (String -> Int) -> String -> Int
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.HasKind.intSizeOf((S)List)" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    ek
                      KSet  Kind
    ek      -> String -> Int
    forall a. HasCallStack => String -> a
    error (String -> Int) -> String -> Int
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.HasKind.intSizeOf((S)Set)"  String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    ek
                      KTuple [Kind]
    tys    -> String -> Int
    forall a. HasCallStack => String -> a
    error (String -> Int) -> String -> Int
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.HasKind.intSizeOf((S)Tuple)" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Kind] -> String
    forall a. Show a => a -> String
    show [Kind]
    tys
                      KMaybe Kind
    k      -> String -> Int
    forall a. HasCallStack => String -> a
    error (String -> Int) -> String -> Int
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.HasKind.intSizeOf((S)Maybe)" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                      KEither Kind
    k1 Kind
    k2 -> String -> Int
    forall a. HasCallStack => String -> a
    error (String -> Int) -> String -> Int
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.HasKind.intSizeOf((S)Either)" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (Kind, Kind) -> String
    forall a. Show a => a -> String
    show (Kind
    k1, Kind
    k2)

      isBoolean       (a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf -> KBool{})      = Bool
    True
      isBoolean       a
    _                        = Bool
    False

      isBounded       (a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf -> KBounded{})   = Bool
    True
      isBounded       a
    _                        = Bool
    False

      isReal          (a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf -> KReal{})      = Bool
    True
      isReal          a
    _                        = Bool
    False

      isFloat         (a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf -> KFloat{})     = Bool
    True
      isFloat         a
    _                        = Bool
    False

      isDouble        (a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf -> KDouble{})    = Bool
    True
      isDouble        a
    _                        = Bool
    False

      isFP            (a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf -> KFP{})        = Bool
    True
      isFP            a
    _                        = Bool
    False

      isRational      (a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf -> KRational{})  = Bool
    True
      isRational      a
    _                        = Bool
    False

      isUnbounded     (a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf -> KUnbounded{}) = Bool
    True
      isUnbounded     a
    _                        = Bool
    False

      isUserSort      (a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf -> KUserSort{})  = Bool
    True
      isUserSort      a
    _                        = Bool
    False

      isChar          (a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf -> KChar{})      = Bool
    True
      isChar          a
    _                        = Bool
    False

      isString        (a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf -> KString{})    = Bool
    True
      isString        a
    _                        = Bool
    False

      isList          (a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf -> KList{})      = Bool
    True
      isList          a
    _                        = Bool
    False

      isSet           (a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf -> KSet{})       = Bool
    True
      isSet           a
    _                        = Bool
    False

      isTuple         (a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf -> KTuple{})     = Bool
    True
      isTuple         a
    _                        = Bool
    False

      isMaybe         (a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf -> KMaybe{})     = Bool
    True
      isMaybe         a
    _                        = Bool
    False

      isEither        (a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf -> KEither{})    = Bool
    True
      isEither        a
    _                        = Bool
    False

      showType = Kind -> String
    forall a. Show a => a -> String
    show (Kind -> String) -> (a -> Kind) -> a -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf

      -- default signature for uninterpreted/enumerated kinds
      default kindOf :: (Read a, G.Data a) => a -> Kind
      kindOf = a -> Kind
    forall a. (Read a, Data a) => a -> Kind
    constructUKind

    -- | This instance allows us to use the `kindOf (Proxy @a)` idiom instead of
    -- the `kindOf (undefined :: a)`, which is safer and looks more idiomatic.
    instance HasKind a => HasKind (Proxy a) where
      kindOf :: Proxy a -> Kind
    kindOf Proxy a
    _ = a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (a
    forall a. HasCallStack => a
    undefined :: a)

    instance HasKind Bool     where kindOf :: Bool -> Kind
    kindOf Bool
    _ = Kind
    KBool
    instance HasKind Int8     where kindOf :: Int8 -> Kind
    kindOf Int8
    _ = Bool -> Int -> Kind
    KBounded Bool
    True  Int
    8
    instance HasKind Word8    where kindOf :: Word8 -> Kind
    kindOf Word8
    _ = Bool -> Int -> Kind
    KBounded Bool
    False Int
    8
    instance HasKind Int16    where kindOf :: Int16 -> Kind
    kindOf Int16
    _ = Bool -> Int -> Kind
    KBounded Bool
    True  Int
    16
    instance HasKind Word16   where kindOf :: Word16 -> Kind
    kindOf Word16
    _ = Bool -> Int -> Kind
    KBounded Bool
    False Int
    16
    instance HasKind Int32    where kindOf :: Int32 -> Kind
    kindOf Int32
    _ = Bool -> Int -> Kind
    KBounded Bool
    True  Int
    32
    instance HasKind Word32   where kindOf :: Word32 -> Kind
    kindOf Word32
    _ = Bool -> Int -> Kind
    KBounded Bool
    False Int
    32
    instance HasKind Int64    where kindOf :: Int64 -> Kind
    kindOf Int64
    _ = Bool -> Int -> Kind
    KBounded Bool
    True  Int
    64
    instance HasKind Word64   where kindOf :: Word64 -> Kind
    kindOf Word64
    _ = Bool -> Int -> Kind
    KBounded Bool
    False Int
    64
    instance HasKind Integer  where kindOf :: Integer -> Kind
    kindOf Integer
    _ = Kind
    KUnbounded
    instance HasKind AlgReal  where kindOf :: AlgReal -> Kind
    kindOf AlgReal
    _ = Kind
    KReal
    instance HasKind Rational where kindOf :: Rational -> Kind
    kindOf Rational
    _ = Kind
    KRational
    instance HasKind Float    where kindOf :: Float -> Kind
    kindOf Float
    _ = Kind
    KFloat
    instance HasKind Double   where kindOf :: Double -> Kind
    kindOf Double
    _ = Kind
    KDouble
    instance HasKind Char     where kindOf :: Char -> Kind
    kindOf Char
    _ = Kind
    KChar

    -- | Grab the bit-size from the proxy. If the nat is too large to fit in an int,
    -- we throw an error. (This would mean too big of a bit-size, that we can't
    -- really deal with in any practical realm.) In fact, even the range allowed
    -- by this conversion (i.e., the entire range of a 64-bit int) is just impractical,
    -- but it's hard to come up with a better bound.
    intOfProxy :: KnownNat n => Proxy n -> Int
    intOfProxy :: forall (n :: Nat). KnownNat n => Proxy n -> Int
    intOfProxy Proxy n
    p
      | Integer
    iv Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    r = Int
    r
      | Bool
    True                 = String -> Int
    forall a. HasCallStack => String -> a
    error (String -> Int) -> String -> Int
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ String
    "Data.SBV: Too large bit-vector size: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show Integer
    iv
                                               , String
    ""
                                               , String
    "No reasonable proof can be performed with such large bit vectors involved,"
                                               , String
    "So, cowardly refusing to proceed any further! Please file this as a"
                                               , String
    "feature request."
                                               ]
      where iv :: Integer
            iv :: Integer
    iv = Proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal Proxy n
    p

            r :: Int
            r :: Int
    r  = Integer -> Int
    forall a. Enum a => a -> Int
    fromEnum Integer
    iv

    -- | Do we have a completely uninterpreted sort lying around anywhere?
    hasUninterpretedSorts :: Kind -> Bool
    hasUninterpretedSorts :: Kind -> Bool
    hasUninterpretedSorts Kind
    KBool                  = Bool
    False
    hasUninterpretedSorts KBounded{}             = Bool
    False
    hasUninterpretedSorts Kind
    KUnbounded             = Bool
    False
    hasUninterpretedSorts Kind
    KReal                  = Bool
    False
    hasUninterpretedSorts (KUserSort String
    _ (Just [String]
    _)) = Bool
    False  -- These are the enumerated sorts, and they are perfectly fine
    hasUninterpretedSorts (KUserSort String
    _ Maybe [String]
    Nothing)  = Bool
    True   -- These are the completely uninterpreted sorts, which we are looking for here
    hasUninterpretedSorts Kind
    KFloat                 = Bool
    False
    hasUninterpretedSorts Kind
    KDouble                = Bool
    False
    hasUninterpretedSorts KFP{}                  = Bool
    False
    hasUninterpretedSorts Kind
    KRational              = Bool
    False
    hasUninterpretedSorts Kind
    KChar                  = Bool
    False
    hasUninterpretedSorts Kind
    KString                = Bool
    False
    hasUninterpretedSorts (KList Kind
    k)              = Kind -> Bool
    hasUninterpretedSorts Kind
    k
    hasUninterpretedSorts (KSet Kind
    k)               = Kind -> Bool
    hasUninterpretedSorts Kind
    k
    hasUninterpretedSorts (KTuple [Kind]
    ks)            = (Kind -> Bool) -> [Kind] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Kind -> Bool
    hasUninterpretedSorts [Kind]
    ks
    hasUninterpretedSorts (KMaybe Kind
    k)             = Kind -> Bool
    hasUninterpretedSorts Kind
    k
    hasUninterpretedSorts (KEither Kind
    k1 Kind
    k2)        = (Kind -> Bool) -> [Kind] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Kind -> Bool
    hasUninterpretedSorts [Kind
    k1, Kind
    k2]

    instance (Typeable a, HasKind a) => HasKind [a] where
       kindOf :: [a] -> Kind
    kindOf [a]
    x | forall a. Typeable a => a -> Bool
    isKString @[a] [a]
    x = Kind
    KString
                | Bool
    True             = Kind -> Kind
    KList (Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a))

    instance HasKind Kind where
      kindOf :: Kind -> Kind
    kindOf = Kind -> Kind
    forall a. a -> a
    id

    instance HasKind () where
      kindOf :: () -> Kind
    kindOf ()
    _ = [Kind] -> Kind
    KTuple []

    instance (HasKind a, HasKind b) => HasKind (a, b) where
      kindOf :: (a, b) -> Kind
    kindOf (a, b)
    _ = [Kind] -> Kind
    KTuple [Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a), Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @b)]

    instance (HasKind a, HasKind b, HasKind c) => HasKind (a, b, c) where
      kindOf :: (a, b, c) -> Kind
    kindOf (a, b, c)
    _ = [Kind] -> Kind
    KTuple [Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a), Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @b), Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @c)]

    instance (HasKind a, HasKind b, HasKind c, HasKind d) => HasKind (a, b, c, d) where
      kindOf :: (a, b, c, d) -> Kind
    kindOf (a, b, c, d)
    _ = [Kind] -> Kind
    KTuple [Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a), Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @b), Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @c), Proxy d -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @d)]

    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e) => HasKind (a, b, c, d, e) where
      kindOf :: (a, b, c, d, e) -> Kind
    kindOf (a, b, c, d, e)
    _ = [Kind] -> Kind
    KTuple [Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a), Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @b), Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @c), Proxy d -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @d), Proxy e -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @e)]

    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f) => HasKind (a, b, c, d, e, f) where
      kindOf :: (a, b, c, d, e, f) -> Kind
    kindOf (a, b, c, d, e, f)
    _ = [Kind] -> Kind
    KTuple [Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a), Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @b), Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @c), Proxy d -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @d), Proxy e -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @e), Proxy f -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @f)]

    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g) => HasKind (a, b, c, d, e, f, g) where
      kindOf :: (a, b, c, d, e, f, g) -> Kind
    kindOf (a, b, c, d, e, f, g)
    _ = [Kind] -> Kind
    KTuple [Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a), Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @b), Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @c), Proxy d -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @d), Proxy e -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @e), Proxy f -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @f), Proxy g -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @g)]

    instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g, HasKind h) => HasKind (a, b, c, d, e, f, g, h) where
      kindOf :: (a, b, c, d, e, f, g, h) -> Kind
    kindOf (a, b, c, d, e, f, g, h)
    _ = [Kind] -> Kind
    KTuple [Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a), Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @b), Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @c), Proxy d -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @d), Proxy e -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @e), Proxy f -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @f), Proxy g -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @g), Proxy h -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @h)]

    instance (HasKind a, HasKind b) => HasKind (Either a b) where
      kindOf :: Either a b -> Kind
    kindOf Either a b
    _ = Kind -> Kind -> Kind
    KEither (Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a)) (Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @b))

    instance HasKind a => HasKind (Maybe a) where
      kindOf :: Maybe a -> Kind
    kindOf Maybe a
    _ = Kind -> Kind
    KMaybe (Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (forall t. Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @a))

    -- | Should we ask the solver to flatten the output? This comes in handy so output is parseable
    -- Essentially, we're being conservative here and simply requesting flattening anything that has
    -- some structure to it.
    needsFlattening :: Kind -> Bool
    needsFlattening :: Kind -> Bool
    needsFlattening Kind
    KBool       = Bool
    False
    needsFlattening KBounded{}  = Bool
    False
    needsFlattening Kind
    KUnbounded  = Bool
    False
    needsFlattening Kind
    KReal       = Bool
    False
    needsFlattening KUserSort{} = Bool
    False
    needsFlattening Kind
    KFloat      = Bool
    False
    needsFlattening Kind
    KDouble     = Bool
    False
    needsFlattening KFP{}       = Bool
    False
    needsFlattening Kind
    KRational   = Bool
    False
    needsFlattening Kind
    KChar       = Bool
    False
    needsFlattening Kind
    KString     = Bool
    False
    needsFlattening KList{}     = Bool
    True
    needsFlattening KSet{}      = Bool
    True
    needsFlattening KTuple{}    = Bool
    True
    needsFlattening KMaybe{}    = Bool
    True
    needsFlattening KEither{}   = Bool
    True

    -- | Catch 0-width cases
    type BVZeroWidth = 'Text "Zero-width bit-vectors are not allowed."

    -- | Type family to create the appropriate non-zero constraint
    type family BVIsNonZero (arg :: Nat) :: Constraint where
       BVIsNonZero 0 = TypeError BVZeroWidth
       BVIsNonZero _ = ()

    #include "MachDeps.h"

    -- Allowed sizes for floats, imposed by LibBF.
    --
    -- NB. In LibBF bindings (and libbf itself as well), minimum number of exponent bits is specified as 3. But this
    -- seems unnecessarily restrictive; that constant doesn't seem to be used anywhere, and furthermore my tests with sb = 2
    -- didn't reveal anything going wrong. I emailed the author of libbf regarding this, and he said:
    --
    --   I had no clear reason to use BF_EXP_BITS_MIN = 3. So if "2" is OK then
    --   why not. The important is that the basic operations are OK. It is likely
    --   there are tricky cases in the transcendental operations but even with
    --   large exponents libbf may have problems with them !
    --
    -- So, in SBV, we allow sb == 2. If this proves problematic, change the number below in definition of FP_MIN_EB to 3!
    --
    -- NB. It would be nice if we could use the LibBF constants expBitsMin, expBitsMax, precBitsMin, precBitsMax
    -- for determining the valid range. Unfortunately this doesn't seem to be possible.
    -- See <https://stackoverflow.com/questions/51900360/making-a-type-constraint-based-on-runtime-value-of-maxbound-int> for a discussion.
    -- So, we use CPP to work-around that.
    #define FP_MIN_EB 2
    #define FP_MIN_SB 2
    #if WORD_SIZE_IN_BITS == 64
    #define FP_MAX_EB 61
    #define FP_MAX_SB 4611686018427387902
    #else
    #define FP_MAX_EB 29
    #define FP_MAX_SB 1073741822
    #endif

    -- | Catch an invalid FP.
    type InvalidFloat (eb :: Nat) (sb :: Nat)
            =     'Text "Invalid floating point type `SFloatingPoint " ':<>: 'ShowType eb ':<>: 'Text " " ':<>: 'ShowType sb ':<>: 'Text "'"
            ':$$: 'Text ""
            ':$$: 'Text "A valid float of type 'SFloatingPoint eb sb' must satisfy:"
            ':$$: 'Text "     eb `elem` [" ':<>: 'ShowType FP_MIN_EB ':<>: 'Text " .. " ':<>: 'ShowType FP_MAX_EB ':<>: 'Text "]"
            ':$$: 'Text "     sb `elem` [" ':<>: 'ShowType FP_MIN_SB ':<>: 'Text " .. " ':<>: 'ShowType FP_MAX_SB ':<>: 'Text "]"
            ':$$: 'Text ""
            ':$$: 'Text "Given type falls outside of this range, or the sizes are not known naturals."

    -- | A valid float has restrictions on eb/sb values.
    -- NB. In the below encoding, I found that CPP is very finicky about substitution of the machine-dependent
    -- macros. If you try to put the conditionals in the same line, it fails to substitute for some reason. Hence the awkward spacing.
    -- Filed this as a bug report for CPPHS at <https://github.com/malcolmwallace/cpphs/issues/25>.
    type family ValidFloat (eb :: Nat) (sb :: Nat) :: Constraint where
      ValidFloat (eb :: Nat) (sb :: Nat) = ( KnownNat eb
                                           , KnownNat sb
                                           , If (   (   eb `CmpNat` FP_MIN_EB == 'EQ
                                                     || eb `CmpNat` FP_MIN_EB == 'GT)
                                                 && (   eb `CmpNat` FP_MAX_EB == 'EQ
                                                     || eb `CmpNat` FP_MAX_EB == 'LT)
                                                 && (   sb `CmpNat` FP_MIN_SB == 'EQ
                                                     || sb `CmpNat` FP_MIN_SB == 'GT)
                                                 && (   sb `CmpNat` FP_MAX_SB == 'EQ
                                                     || sb `CmpNat` FP_MAX_SB == 'LT))
                                                (() :: Constraint)
                                                (TypeError (InvalidFloat eb sb))
                                           )

    -- | Rounding mode to be used for the IEEE floating-point operations.
    -- Note that Haskell's default is 'RoundNearestTiesToEven'. If you use
    -- a different rounding mode, then the counter-examples you get may not
    -- match what you observe in Haskell.
    data RoundingMode = RoundNearestTiesToEven  -- ^ Round to nearest representable floating point value.
                                                -- If precisely at half-way, pick the even number.
                                                -- (In this context, /even/ means the lowest-order bit is zero.)
                      | RoundNearestTiesToAway  -- ^ Round to nearest representable floating point value.
                                                -- If precisely at half-way, pick the number further away from 0.
                                                -- (That is, for positive values, pick the greater; for negative values, pick the smaller.)
                      | RoundTowardPositive     -- ^ Round towards positive infinity. (Also known as rounding-up or ceiling.)
                      | RoundTowardNegative     -- ^ Round towards negative infinity. (Also known as rounding-down or floor.)
                      | RoundTowardZero         -- ^ Round towards zero. (Also known as truncation.)
                      deriving (RoundingMode -> RoundingMode -> Bool
    (RoundingMode -> RoundingMode -> Bool)
    -> (RoundingMode -> RoundingMode -> Bool) -> Eq RoundingMode
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: RoundingMode -> RoundingMode -> Bool
    == :: RoundingMode -> RoundingMode -> Bool
    $c/= :: RoundingMode -> RoundingMode -> Bool
    /= :: RoundingMode -> RoundingMode -> Bool
    Eq, Eq RoundingMode
    Eq RoundingMode =>
    (RoundingMode -> RoundingMode -> Ordering)
    -> (RoundingMode -> RoundingMode -> Bool)
    -> (RoundingMode -> RoundingMode -> Bool)
    -> (RoundingMode -> RoundingMode -> Bool)
    -> (RoundingMode -> RoundingMode -> Bool)
    -> (RoundingMode -> RoundingMode -> RoundingMode)
    -> (RoundingMode -> RoundingMode -> RoundingMode)
    -> Ord RoundingMode
    RoundingMode -> RoundingMode -> Bool
    RoundingMode -> RoundingMode -> Ordering
    RoundingMode -> RoundingMode -> RoundingMode
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: RoundingMode -> RoundingMode -> Ordering
    compare :: RoundingMode -> RoundingMode -> Ordering
    $c< :: RoundingMode -> RoundingMode -> Bool
    < :: RoundingMode -> RoundingMode -> Bool
    $c<= :: RoundingMode -> RoundingMode -> Bool
    <= :: RoundingMode -> RoundingMode -> Bool
    $c> :: RoundingMode -> RoundingMode -> Bool
    > :: RoundingMode -> RoundingMode -> Bool
    $c>= :: RoundingMode -> RoundingMode -> Bool
    >= :: RoundingMode -> RoundingMode -> Bool
    $cmax :: RoundingMode -> RoundingMode -> RoundingMode
    max :: RoundingMode -> RoundingMode -> RoundingMode
    $cmin :: RoundingMode -> RoundingMode -> RoundingMode
    min :: RoundingMode -> RoundingMode -> RoundingMode
    Ord, Int -> RoundingMode -> ShowS
    [RoundingMode] -> ShowS
    RoundingMode -> String
    (Int -> RoundingMode -> ShowS)
    -> (RoundingMode -> String)
    -> ([RoundingMode] -> ShowS)
    -> Show RoundingMode
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> RoundingMode -> ShowS
    showsPrec :: Int -> RoundingMode -> ShowS
    $cshow :: RoundingMode -> String
    show :: RoundingMode -> String
    $cshowList :: [RoundingMode] -> ShowS
    showList :: [RoundingMode] -> ShowS
    Show, ReadPrec [RoundingMode]
    ReadPrec RoundingMode
    Int -> ReadS RoundingMode
    ReadS [RoundingMode]
    (Int -> ReadS RoundingMode)
    -> ReadS [RoundingMode]
    -> ReadPrec RoundingMode
    -> ReadPrec [RoundingMode]
    -> Read RoundingMode
    forall a.
    (Int -> ReadS a)
    -> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
    $creadsPrec :: Int -> ReadS RoundingMode
    readsPrec :: Int -> ReadS RoundingMode
    $creadList :: ReadS [RoundingMode]
    readList :: ReadS [RoundingMode]
    $creadPrec :: ReadPrec RoundingMode
    readPrec :: ReadPrec RoundingMode
    $creadListPrec :: ReadPrec [RoundingMode]
    readListPrec :: ReadPrec [RoundingMode]
    Read, Typeable RoundingMode
    Typeable RoundingMode =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> RoundingMode -> c RoundingMode)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c RoundingMode)
    -> (RoundingMode -> Constr)
    -> (RoundingMode -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c RoundingMode))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e))
        -> Maybe (c RoundingMode))
    -> ((forall b. Data b => b -> b) -> RoundingMode -> RoundingMode)
    -> (forall r r'.
        (r -> r' -> r)
        -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r)
    -> (forall r r'.
        (r' -> r -> r)
        -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r)
    -> (forall u. (forall d. Data d => d -> u) -> RoundingMode -> [u])
    -> (forall u.
        Int -> (forall d. Data d => d -> u) -> RoundingMode -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode)
    -> Data RoundingMode
    RoundingMode -> Constr
    RoundingMode -> DataType
    (forall b. Data b => b -> b) -> RoundingMode -> RoundingMode
    forall a.
    Typeable a =>
    (forall (c :: * -> *).
     (forall d b. Data d => c (d -> b) -> d -> c b)
     -> (forall g. g -> c g) -> a -> c a)
    -> (forall (c :: * -> *).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c a)
    -> (a -> Constr)
    -> (a -> DataType)
    -> (forall (t :: * -> *) (c :: * -> *).
        Typeable t =>
        (forall d. Data d => c (t d)) -> Maybe (c a))
    -> (forall (t :: * -> * -> *) (c :: * -> *).
        Typeable t =>
        (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
    -> ((forall b. Data b => b -> b) -> a -> a)
    -> (forall r r'.
        (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall r r'.
        (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
    -> (forall u. (forall d. Data d => d -> u) -> a -> [u])
    -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
    -> (forall (m :: * -> *).
        Monad m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> (forall (m :: * -> *).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> a -> m a)
    -> Data a
    forall u. Int -> (forall d. Data d => d -> u) -> RoundingMode -> u
    forall u. (forall d. Data d => d -> u) -> RoundingMode -> [u]
    forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
    forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
    forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
    forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
    forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c RoundingMode
    forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> RoundingMode -> c RoundingMode
    forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c RoundingMode)
    forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c RoundingMode)
    $cgfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> RoundingMode -> c RoundingMode
    gfoldl :: forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> RoundingMode -> c RoundingMode
    $cgunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c RoundingMode
    gunfold :: forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c RoundingMode
    $ctoConstr :: RoundingMode -> Constr
    toConstr :: RoundingMode -> Constr
    $cdataTypeOf :: RoundingMode -> DataType
    dataTypeOf :: RoundingMode -> DataType
    $cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c RoundingMode)
    dataCast1 :: forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c RoundingMode)
    $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c RoundingMode)
    dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c RoundingMode)
    $cgmapT :: (forall b. Data b => b -> b) -> RoundingMode -> RoundingMode
    gmapT :: (forall b. Data b => b -> b) -> RoundingMode -> RoundingMode
    $cgmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
    gmapQl :: forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> RoundingMode -> [u]
    gmapQ :: forall u. (forall d. Data d => d -> u) -> RoundingMode -> [u]
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> RoundingMode -> u
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> RoundingMode -> u
    $cgmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
    gmapM :: forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
    $cgmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
    gmapMp :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
    $cgmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
    gmapMo :: forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
    G.Data, RoundingMode
    RoundingMode -> RoundingMode -> Bounded RoundingMode
    forall a. a -> a -> Bounded a
    $cminBound :: RoundingMode
    minBound :: RoundingMode
    $cmaxBound :: RoundingMode
    maxBound :: RoundingMode
    Bounded, Int -> RoundingMode
    RoundingMode -> Int
    RoundingMode -> [RoundingMode]
    RoundingMode -> RoundingMode
    RoundingMode -> RoundingMode -> [RoundingMode]
    RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode]
    (RoundingMode -> RoundingMode)
    -> (RoundingMode -> RoundingMode)
    -> (Int -> RoundingMode)
    -> (RoundingMode -> Int)
    -> (RoundingMode -> [RoundingMode])
    -> (RoundingMode -> RoundingMode -> [RoundingMode])
    -> (RoundingMode -> RoundingMode -> [RoundingMode])
    -> (RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode])
    -> Enum RoundingMode
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    $csucc :: RoundingMode -> RoundingMode
    succ :: RoundingMode -> RoundingMode
    $cpred :: RoundingMode -> RoundingMode
    pred :: RoundingMode -> RoundingMode
    $ctoEnum :: Int -> RoundingMode
    toEnum :: Int -> RoundingMode
    $cfromEnum :: RoundingMode -> Int
    fromEnum :: RoundingMode -> Int
    $cenumFrom :: RoundingMode -> [RoundingMode]
    enumFrom :: RoundingMode -> [RoundingMode]
    $cenumFromThen :: RoundingMode -> RoundingMode -> [RoundingMode]
    enumFromThen :: RoundingMode -> RoundingMode -> [RoundingMode]
    $cenumFromTo :: RoundingMode -> RoundingMode -> [RoundingMode]
    enumFromTo :: RoundingMode -> RoundingMode -> [RoundingMode]
    $cenumFromThenTo :: RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode]
    enumFromThenTo :: RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode]
    Enum)

    -- | 'RoundingMode' kind
    instance HasKind RoundingMode

    -- | Convert a rounding mode to the format SMT-Lib2 understands.
    smtRoundingMode :: RoundingMode -> String
    smtRoundingMode :: RoundingMode -> String
    smtRoundingMode RoundingMode
    RoundNearestTiesToEven = String
    "roundNearestTiesToEven"
    smtRoundingMode RoundingMode
    RoundNearestTiesToAway = String
    "roundNearestTiesToAway"
    smtRoundingMode RoundingMode
    RoundTowardPositive    = String
    "roundTowardPositive"
    smtRoundingMode RoundingMode
    RoundTowardNegative    = String
    "roundTowardNegative"
    smtRoundingMode RoundingMode
    RoundTowardZero        = String
    "roundTowardZero"