-----------------------------------------------------------------------------
-- |
-- 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