    -----------------------------------------------------------------------------
    -- |
    -- 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 DefaultSignatures   #-}
    {-# LANGUAGE FlexibleInstances   #-}
    {-# LANGUAGE LambdaCase          #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeApplications    #-}
    {-# LANGUAGE ViewPatterns        #-}

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

    module Data.SBV.Core.Kind (Kind(..), HasKind(..), constructUKind, smtType, hasUninterpretedSorts, showBaseKind, needsFlattening) 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.List (isPrefixOf, intercalate)

    import Data.Typeable (Typeable)

    import Data.SBV.Utils.Lib (isKString)

    -- | Kind of symbolic value
    data Kind = KBool
              | KBounded !Bool !Int
              | KUnbounded
              | KReal
              | KUninterpreted String (Either String [String])  -- name. Left: uninterpreted. Right: enum constructors.
              | KFloat
              | KDouble
              | KChar
              | KString
              | KList Kind
              | KSet  Kind
              | KTuple [Kind]
              | KMaybe  Kind
              | 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
    /= :: Kind -> Kind -> Bool
    $c/= :: Kind -> Kind -> Bool
    == :: Kind -> Kind -> Bool
    $c== :: 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
    min :: Kind -> Kind -> Kind
    $cmin :: Kind -> Kind -> Kind
    max :: Kind -> Kind -> Kind
    $cmax :: Kind -> Kind -> Kind
    >= :: Kind -> Kind -> Bool
    $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
    compare :: Kind -> Kind -> Ordering
    $ccompare :: Kind -> Kind -> Ordering
    $cp1Ord :: Eq Kind
    Ord)

    -- | 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 'KUninterpreted', we make sure we don't use any of
    -- the reserved names; see 'constructUKind' for details.
    instance Show Kind where
      show :: Kind -> String
    show KBool                = "SBool"
      show (KBounded False n :: Int
    n)   = Int -> String -> ShowS
    pickType Int
    n "SWord" "SWord " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n
      show (KBounded True n :: Int
    n)    = Int -> String -> ShowS
    pickType Int
    n "SInt"  "SInt "  String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n
      show KUnbounded           = "SInteger"
      show KReal                = "SReal"
      show (KUninterpreted s :: String
    s _) = String
    s
      show KFloat               = "SFloat"
      show KDouble              = "SDouble"
      show KString              = "SString"
      show KChar                = "SChar"
      show (KList e :: Kind
    e)            = "[" 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]
    ++ "]"
      show (KSet  e :: Kind
    e)            = "{" 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]
    ++ "}"
      show (KTuple m :: [Kind]
    m)           = "(" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ", " (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]
    ++ ")"
      show (KMaybe k :: Kind
    k)           = "SMaybe "  String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    kindParen (Kind -> String
    showBaseKind Kind
    k)
      show (KEither k1 :: Kind
    k1 k2 :: Kind
    k2)      = "SEither " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    kindParen (Kind -> String
    showBaseKind Kind
    k1) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    kindParen (Kind -> String
    showBaseKind Kind
    k2)

    -- | 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 False n :: Int
    n)  = Int -> String -> ShowS
    pickType Int
    n "Word" "WordN " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n
            sh (KBounded True n :: Int
    n)   = Int -> String -> ShowS
    pickType Int
    n "Int"  "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@KUninterpreted{}  = 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@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 (KList k :: Kind
    k)           = "[" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    sh Kind
    k String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "]"
            sh (KSet k :: Kind
    k)            = "{" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    sh Kind
    k String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "}"
            sh (KTuple ks :: [Kind]
    ks)         = "(" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ", " ((Kind -> String) -> [Kind] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Kind -> String
    sh [Kind]
    ks) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"
            sh (KMaybe k :: Kind
    k)          = "Maybe "  String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    kindParen (Kind -> String
    sh Kind
    k)
            sh (KEither k1 :: Kind
    k1 k2 :: Kind
    k2)     = "Either " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    kindParen (Kind -> String
    sh Kind
    k1) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " " 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 ('S':s :: String
    s) = String
    s
            noS s :: 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 i :: Int
    i standard :: String
    standard other :: String
    other
      | Int
    i Int -> [Int] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [8, 16, 32, 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@('[':_) = String
    s
    kindParen s :: String
    s@('(':_) = String
    s
    kindParen s :: String
    s | (Char -> Bool) -> String -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Char -> Bool
    isSpace String
    s = '(' Char -> ShowS
    forall a. a -> [a] -> [a]
    : String
    s String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"
                | Bool
    True          = String
    s

    -- | How the type maps to SMT land
    smtType :: Kind -> String
    smtType :: Kind -> String
    smtType KBool                = "Bool"
    smtType (KBounded _ sz :: Int
    sz)      = "(_ 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]
    ++ ")"
    smtType KUnbounded           = "Int"
    smtType KReal                = "Real"
    smtType KFloat               = "(_ FloatingPoint  8 24)"
    smtType KDouble              = "(_ FloatingPoint 11 53)"
    smtType KString              = "String"
    smtType KChar                = "(_ BitVec 8)"
    smtType (KList k :: Kind
    k)            = "(Seq "   String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    k String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"
    smtType (KSet  k :: Kind
    k)            = "(Array " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    k String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " Bool)"
    smtType (KUninterpreted s :: String
    s _) = String
    s
    smtType (KTuple [])          = "SBVTuple0"
    smtType (KTuple kinds :: [Kind]
    kinds)       = "(SBVTuple" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show ([Kind] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Kind]
    kinds) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " " 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]
    ++ ")"
    smtType (KMaybe k :: Kind
    k)           = "(SBVMaybe " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    k String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"
    smtType (KEither k1 :: Kind
    k1 k2 :: Kind
    k2)      = "(SBVEither "  String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    k1 String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    smtType Kind
    k2 String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ")"

    instance Eq  G.DataType where
       a :: DataType
    a == :: DataType -> DataType -> Bool
    == b :: 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
       a :: DataType
    a compare :: DataType -> DataType -> Ordering
    `compare` b :: 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 KBool            -> Bool
    False
                        KBounded b :: Bool
    b _     -> Bool
    b
                        KUnbounded       -> Bool
    True
                        KReal            -> Bool
    True
                        KFloat           -> Bool
    True
                        KDouble          -> Bool
    True
                        KUninterpreted{} -> Bool
    False
                        KString          -> Bool
    False
                        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 :: a -> Kind
    constructUKind a :: 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
    $ "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 -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ": Must not start with any of " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ", " [String]
    badPrefixes
      | Bool
    True
      = String -> Either String [String] -> Kind
    KUninterpreted String
    sortName Either String [String]
    mbEnumFields
      where -- make sure we don't step on ourselves:
            badPrefixes :: [String]
    badPrefixes   = ["SBool", "SWord", "SInt", "SInteger", "SReal", "SFloat", "SDouble", "SString", "SChar", "["]

            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
            isEnumeration :: Bool
    isEnumeration = Bool -> Bool
    not ([Constr] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Constr]
    constrs) Bool -> Bool -> Bool
    && (Constr -> Bool) -> [Constr] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all ([String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null ([String] -> Bool) -> (Constr -> [String]) -> Constr -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Constr -> [String]
    G.constrFields) [Constr]
    constrs
            mbEnumFields :: Either String [String]
    mbEnumFields
             | Bool
    isEnumeration = [Constr] -> [String] -> Either String [String]
    forall a. Show a => [a] -> [String] -> Either String [String]
    check [Constr]
    constrs []
             | Bool
    True          = String -> Either String [String]
    forall a b. a -> Either a b
    Left (String -> Either String [String])
    -> String -> Either String [String]
    forall a b. (a -> b) -> a -> b
    $ String
    sortName String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " is not a finite non-empty enumeration"
            check :: [a] -> [String] -> Either String [String]
    check []     sofar :: [String]
    sofar = [String] -> Either String [String]
    forall a b. b -> Either a b
    Right ([String] -> Either String [String])
    -> [String] -> Either String [String]
    forall a b. (a -> b) -> a -> b
    $ [String] -> [String]
    forall a. [a] -> [a]
    reverse [String]
    sofar
            check (c :: a
    c:cs :: [a]
    cs) sofar :: [String]
    sofar = case a -> Maybe String
    forall a. Show a => a -> Maybe String
    checkConstr a
    c of
                                    Nothing -> [a] -> [String] -> Either String [String]
    check [a]
    cs (a -> String
    forall a. Show a => a -> String
    show a
    c String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    sofar)
                                    Just s :: String
    s  -> String -> Either String [String]
    forall a b. a -> Either a b
    Left (String -> Either String [String])
    -> String -> Either String [String]
    forall a b. (a -> b) -> a -> b
    $ String
    sortName String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "." String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    c String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ": " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    s
            checkConstr :: a -> Maybe String
    checkConstr c :: a
    c = case (ReadS a
    forall a. Read a => ReadS a
    reads (a -> String
    forall a. Show a => a -> String
    show a
    c) :: [(a, String)]) of
                              ((_, "") : _)  -> Maybe String
    forall a. Maybe a
    Nothing
                              _              -> String -> Maybe String
    forall a. a -> Maybe a
    Just "not a nullary constructor"

    -- | 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
      isUnbounded     :: a -> Bool
      isUninterpreted :: 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 x :: a
    x = Kind -> Bool
    kindHasSign (a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    x)

      intSizeOf x :: a
    x = case a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    x of
                      KBool              -> String -> Int
    forall a. HasCallStack => String -> a
    error "SBV.HasKind.intSizeOf((S)Bool)"
                      KBounded _ s :: Int
    s       -> Int
    s
                      KUnbounded         -> String -> Int
    forall a. HasCallStack => String -> a
    error "SBV.HasKind.intSizeOf((S)Integer)"
                      KReal              -> String -> Int
    forall a. HasCallStack => String -> a
    error "SBV.HasKind.intSizeOf((S)Real)"
                      KFloat             -> String -> Int
    forall a. HasCallStack => String -> a
    error "SBV.HasKind.intSizeOf((S)Float)"
                      KDouble            -> String -> Int
    forall a. HasCallStack => String -> a
    error "SBV.HasKind.intSizeOf((S)Double)"
                      KUninterpreted s :: String
    s _ -> String -> Int
    forall a. HasCallStack => String -> a
    error (String -> Int) -> String -> Int
    forall a b. (a -> b) -> a -> b
    $ "SBV.HasKind.intSizeOf: Uninterpreted sort: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    s
                      KString            -> String -> Int
    forall a. HasCallStack => String -> a
    error "SBV.HasKind.intSizeOf((S)Double)"
                      KChar              -> String -> Int
    forall a. HasCallStack => String -> a
    error "SBV.HasKind.intSizeOf((S)Char)"
                      KList ek :: Kind
    ek           -> String -> Int
    forall a. HasCallStack => String -> a
    error (String -> Int) -> String -> Int
    forall a b. (a -> b) -> a -> b
    $ "SBV.HasKind.intSizeOf((S)List)" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    ek
                      KSet  ek :: Kind
    ek           -> String -> Int
    forall a. HasCallStack => String -> a
    error (String -> Int) -> String -> Int
    forall a b. (a -> b) -> a -> b
    $ "SBV.HasKind.intSizeOf((S)Set)"  String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    ek
                      KTuple tys :: [Kind]
    tys         -> String -> Int
    forall a. HasCallStack => String -> a
    error (String -> Int) -> String -> Int
    forall a b. (a -> b) -> a -> b
    $ "SBV.HasKind.intSizeOf((S)Tuple)" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Kind] -> String
    forall a. Show a => a -> String
    show [Kind]
    tys
                      KMaybe k :: Kind
    k           -> String -> Int
    forall a. HasCallStack => String -> a
    error (String -> Int) -> String -> Int
    forall a b. (a -> b) -> a -> b
    $ "SBV.HasKind.intSizeOf((S)Maybe)" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                      KEither k1 :: Kind
    k1 k2 :: Kind
    k2      -> String -> Int
    forall a. HasCallStack => String -> a
    error (String -> Int) -> String -> Int
    forall a b. (a -> b) -> a -> b
    $ "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       _                            = Bool
    False

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

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

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

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

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

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

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

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

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

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

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

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

      isEither        (a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf -> KEither{})        = Bool
    True
      isEither        _                            = 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 _ = a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (a
    forall a. HasCallStack => a
    undefined :: a)

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

    -- | Do we have a completely uninterpreted sort lying around anywhere?
    hasUninterpretedSorts :: Kind -> Bool
    hasUninterpretedSorts :: Kind -> Bool
    hasUninterpretedSorts KBool                        = Bool
    False
    hasUninterpretedSorts KBounded{}                   = Bool
    False
    hasUninterpretedSorts KUnbounded                   = Bool
    False
    hasUninterpretedSorts KReal                        = Bool
    False
    hasUninterpretedSorts (KUninterpreted _ (Right _)) = Bool
    False  -- These are the enumerated sorts, and they are perfectly fine
    hasUninterpretedSorts (KUninterpreted _ (Left  _)) = Bool
    True   -- These are the completely uninterpreted sorts, which we are looking for here
    hasUninterpretedSorts KFloat                       = Bool
    False
    hasUninterpretedSorts KDouble                      = Bool
    False
    hasUninterpretedSorts KChar                        = Bool
    False
    hasUninterpretedSorts KString                      = Bool
    False
    hasUninterpretedSorts (KList k :: Kind
    k)                    = Kind -> Bool
    hasUninterpretedSorts Kind
    k
    hasUninterpretedSorts (KSet k :: Kind
    k)                     = Kind -> Bool
    hasUninterpretedSorts Kind
    k
    hasUninterpretedSorts (KTuple ks :: [Kind]
    ks)                  = (Kind -> Bool) -> [Kind] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Kind -> Bool
    hasUninterpretedSorts [Kind]
    ks
    hasUninterpretedSorts (KMaybe k :: Kind
    k)                   = Kind -> Bool
    hasUninterpretedSorts Kind
    k
    hasUninterpretedSorts (KEither k1 :: Kind
    k1 k2 :: 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 x :: [a]
    x | [a] -> Bool
    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 (Proxy a
    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 _ = [Kind] -> Kind
    KTuple [Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a), Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    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 _ = [Kind] -> Kind
    KTuple [Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a), Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b), Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy c
    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 _ = [Kind] -> Kind
    KTuple [Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a), Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b), Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy c
    forall k (t :: k). Proxy t
    Proxy @c), Proxy d -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy d
    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 _ = [Kind] -> Kind
    KTuple [Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a), Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b), Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy c
    forall k (t :: k). Proxy t
    Proxy @c), Proxy d -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy d
    forall k (t :: k). Proxy t
    Proxy @d), Proxy e -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy e
    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 _ = [Kind] -> Kind
    KTuple [Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a), Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b), Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy c
    forall k (t :: k). Proxy t
    Proxy @c), Proxy d -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy d
    forall k (t :: k). Proxy t
    Proxy @d), Proxy e -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy e
    forall k (t :: k). Proxy t
    Proxy @e), Proxy f -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy f
    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 _ = [Kind] -> Kind
    KTuple [Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a), Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b), Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy c
    forall k (t :: k). Proxy t
    Proxy @c), Proxy d -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy d
    forall k (t :: k). Proxy t
    Proxy @d), Proxy e -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy e
    forall k (t :: k). Proxy t
    Proxy @e), Proxy f -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy f
    forall k (t :: k). Proxy t
    Proxy @f), Proxy g -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy g
    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 _ = [Kind] -> Kind
    KTuple [Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    forall k (t :: k). Proxy t
    Proxy @a), Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b), Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy c
    forall k (t :: k). Proxy t
    Proxy @c), Proxy d -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy d
    forall k (t :: k). Proxy t
    Proxy @d), Proxy e -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy e
    forall k (t :: k). Proxy t
    Proxy @e), Proxy f -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy f
    forall k (t :: k). Proxy t
    Proxy @f), Proxy g -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy g
    forall k (t :: k). Proxy t
    Proxy @g), Proxy h -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy h
    forall k (t :: k). Proxy t
    Proxy @h)]

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

    instance HasKind a => HasKind (Maybe a) where
      kindOf :: Maybe a -> Kind
    kindOf _ = Kind -> Kind
    KMaybe (Proxy a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy a
    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 KBool            = Bool
    False
    needsFlattening KBounded{}       = Bool
    False
    needsFlattening KUnbounded       = Bool
    False
    needsFlattening KReal            = Bool
    False
    needsFlattening KUninterpreted{} = Bool
    False
    needsFlattening KFloat           = Bool
    False
    needsFlattening KDouble          = Bool
    False
    needsFlattening KChar            = Bool
    False
    needsFlattening KString          = Bool
    False
    needsFlattening KList{}          = Bool
    True
    needsFlattening KSet{}           = Bool
    True
    needsFlattening KTuple{}         = Bool
    True
    needsFlattening KMaybe{}         = Bool
    True
    needsFlattening KEither{}        = Bool
    True