{-# 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)
data Kind = KBool
| KBounded !Bool !Int
| KUnbounded
| KReal
| KUninterpreted String (Either String [String])
| 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)
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)
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
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)
noS :: ShowS
noS ('S':s :: String
s) = String
s
noS s :: String
s = String
s
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
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
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)
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
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
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"
class HasKind a where
kindOf :: a -> Kind
hasSign :: a -> Bool
intSizeOf :: a -> Int
isBoolean :: a -> Bool
isBounded :: a -> Bool
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
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 kindOf :: (Read a, G.Data a) => a -> Kind
kindOf = a -> Kind
forall a. (Read a, Data a) => a -> Kind
constructUKind
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
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
hasUninterpretedSorts (KUninterpreted _ (Left _)) = Bool
True
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))
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