{-# 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 (Eq, Ord)
instance Show Kind where
show KBool = "SBool"
show (KBounded False n) = "SWord" ++ show n
show (KBounded True n) = "SInt" ++ show n
show KUnbounded = "SInteger"
show KReal = "SReal"
show (KUninterpreted s _) = s
show KFloat = "SFloat"
show KDouble = "SDouble"
show KString = "SString"
show KChar = "SChar"
show (KList e) = "[" ++ show e ++ "]"
show (KSet e) = "{" ++ show e ++ "}"
show (KTuple m) = "(" ++ intercalate ", " (show <$> m) ++ ")"
show (KMaybe k) = "SMaybe " ++ kindParen (showBaseKind k)
show (KEither k1 k2) = "SEither " ++ kindParen (showBaseKind k1) ++ " " ++ kindParen (showBaseKind k2)
showBaseKind :: Kind -> String
showBaseKind = sh
where sh k@KBool = noS (show k)
sh k@KBounded{} = noS (show k)
sh k@KUnbounded = noS (show k)
sh k@KReal = noS (show k)
sh k@KUninterpreted{} = show k
sh k@KFloat = noS (show k)
sh k@KDouble = noS (show k)
sh k@KChar = noS (show k)
sh k@KString = noS (show k)
sh (KList k) = "[" ++ sh k ++ "]"
sh (KSet k) = "{" ++ sh k ++ "}"
sh (KTuple ks) = "(" ++ intercalate ", " (map sh ks) ++ ")"
sh (KMaybe k) = "Maybe " ++ kindParen (sh k)
sh (KEither k1 k2) = "Either " ++ kindParen (sh k1) ++ " " ++ kindParen (sh k2)
noS ('S':s) = s
noS s = s
kindParen :: String -> String
kindParen s@('[':_) = s
kindParen s@('(':_) = s
kindParen s | any isSpace s = '(' : s ++ ")"
| True = s
smtType :: Kind -> String
smtType KBool = "Bool"
smtType (KBounded _ sz) = "(_ BitVec " ++ show sz ++ ")"
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) = "(Seq " ++ smtType k ++ ")"
smtType (KSet k) = "(Array " ++ smtType k ++ " Bool)"
smtType (KUninterpreted s _) = s
smtType (KTuple []) = "SBVTuple0"
smtType (KTuple kinds) = "(SBVTuple" ++ show (length kinds) ++ " " ++ unwords (smtType <$> kinds) ++ ")"
smtType (KMaybe k) = "(SBVMaybe " ++ smtType k ++ ")"
smtType (KEither k1 k2) = "(SBVEither " ++ smtType k1 ++ " " ++ smtType k2 ++ ")"
instance Eq G.DataType where
a == b = G.tyconUQname (G.dataTypeName a) == G.tyconUQname (G.dataTypeName b)
instance Ord G.DataType where
a `compare` b = G.tyconUQname (G.dataTypeName a) `compare` G.tyconUQname (G.dataTypeName b)
kindHasSign :: Kind -> Bool
kindHasSign = \case KBool -> False
KBounded b _ -> b
KUnbounded -> True
KReal -> True
KFloat -> True
KDouble -> True
KUninterpreted{} -> False
KString -> False
KChar -> False
KList{} -> False
KSet{} -> False
KTuple{} -> False
KMaybe{} -> False
KEither{} -> False
constructUKind :: forall a. (Read a, G.Data a) => a -> Kind
constructUKind a
| any (`isPrefixOf` sortName) badPrefixes
= error $ "Data.SBV: Cannot construct user-sort with name: " ++ show sortName ++ ": Must not start with any of " ++ intercalate ", " badPrefixes
| True
= KUninterpreted sortName mbEnumFields
where
badPrefixes = ["SBool", "SWord", "SInt", "SInteger", "SReal", "SFloat", "SDouble", "SString", "SChar", "["]
dataType = G.dataTypeOf a
sortName = G.tyconUQname . G.dataTypeName $ dataType
constrs = G.dataTypeConstrs dataType
isEnumeration = not (null constrs) && all (null . G.constrFields) constrs
mbEnumFields
| isEnumeration = check constrs []
| True = Left $ sortName ++ " is not a finite non-empty enumeration"
check [] sofar = Right $ reverse sofar
check (c:cs) sofar = case checkConstr c of
Nothing -> check cs (show c : sofar)
Just s -> Left $ sortName ++ "." ++ show c ++ ": " ++ s
checkConstr c = case (reads (show c) :: [(a, String)]) of
((_, "") : _) -> Nothing
_ -> 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 = kindHasSign (kindOf x)
intSizeOf x = case kindOf x of
KBool -> error "SBV.HasKind.intSizeOf((S)Bool)"
KBounded _ s -> s
KUnbounded -> error "SBV.HasKind.intSizeOf((S)Integer)"
KReal -> error "SBV.HasKind.intSizeOf((S)Real)"
KFloat -> error "SBV.HasKind.intSizeOf((S)Float)"
KDouble -> error "SBV.HasKind.intSizeOf((S)Double)"
KUninterpreted s _ -> error $ "SBV.HasKind.intSizeOf: Uninterpreted sort: " ++ s
KString -> error "SBV.HasKind.intSizeOf((S)Double)"
KChar -> error "SBV.HasKind.intSizeOf((S)Char)"
KList ek -> error $ "SBV.HasKind.intSizeOf((S)List)" ++ show ek
KSet ek -> error $ "SBV.HasKind.intSizeOf((S)Set)" ++ show ek
KTuple tys -> error $ "SBV.HasKind.intSizeOf((S)Tuple)" ++ show tys
KMaybe k -> error $ "SBV.HasKind.intSizeOf((S)Maybe)" ++ show k
KEither k1 k2 -> error $ "SBV.HasKind.intSizeOf((S)Either)" ++ show (k1, k2)
isBoolean (kindOf -> KBool{}) = True
isBoolean _ = False
isBounded (kindOf -> KBounded{}) = True
isBounded _ = False
isReal (kindOf -> KReal{}) = True
isReal _ = False
isFloat (kindOf -> KFloat{}) = True
isFloat _ = False
isDouble (kindOf -> KDouble{}) = True
isDouble _ = False
isUnbounded (kindOf -> KUnbounded{}) = True
isUnbounded _ = False
isUninterpreted (kindOf -> KUninterpreted{}) = True
isUninterpreted _ = False
isChar (kindOf -> KChar{}) = True
isChar _ = False
isString (kindOf -> KString{}) = True
isString _ = False
isList (kindOf -> KList{}) = True
isList _ = False
isSet (kindOf -> KSet{}) = True
isSet _ = False
isTuple (kindOf -> KTuple{}) = True
isTuple _ = False
isMaybe (kindOf -> KMaybe{}) = True
isMaybe _ = False
isEither (kindOf -> KEither{}) = True
isEither _ = False
showType = show . kindOf
default kindOf :: (Read a, G.Data a) => a -> Kind
kindOf = constructUKind
instance HasKind a => HasKind (Proxy a) where
kindOf _ = kindOf (undefined :: a)
instance HasKind Bool where kindOf _ = KBool
instance HasKind Int8 where kindOf _ = KBounded True 8
instance HasKind Word8 where kindOf _ = KBounded False 8
instance HasKind Int16 where kindOf _ = KBounded True 16
instance HasKind Word16 where kindOf _ = KBounded False 16
instance HasKind Int32 where kindOf _ = KBounded True 32
instance HasKind Word32 where kindOf _ = KBounded False 32
instance HasKind Int64 where kindOf _ = KBounded True 64
instance HasKind Word64 where kindOf _ = KBounded False 64
instance HasKind Integer where kindOf _ = KUnbounded
instance HasKind AlgReal where kindOf _ = KReal
instance HasKind Float where kindOf _ = KFloat
instance HasKind Double where kindOf _ = KDouble
instance HasKind Char where kindOf _ = KChar
hasUninterpretedSorts :: Kind -> Bool
hasUninterpretedSorts KBool = False
hasUninterpretedSorts KBounded{} = False
hasUninterpretedSorts KUnbounded = False
hasUninterpretedSorts KReal = False
hasUninterpretedSorts (KUninterpreted _ (Right _)) = False
hasUninterpretedSorts (KUninterpreted _ (Left _)) = True
hasUninterpretedSorts KFloat = False
hasUninterpretedSorts KDouble = False
hasUninterpretedSorts KChar = False
hasUninterpretedSorts KString = False
hasUninterpretedSorts (KList k) = hasUninterpretedSorts k
hasUninterpretedSorts (KSet k) = hasUninterpretedSorts k
hasUninterpretedSorts (KTuple ks) = any hasUninterpretedSorts ks
hasUninterpretedSorts (KMaybe k) = hasUninterpretedSorts k
hasUninterpretedSorts (KEither k1 k2) = any hasUninterpretedSorts [k1, k2]
instance (Typeable a, HasKind a) => HasKind [a] where
kindOf x | isKString @[a] x = KString
| True = KList (kindOf (Proxy @a))
instance HasKind Kind where
kindOf = id
instance HasKind () where
kindOf _ = KTuple []
instance (HasKind a, HasKind b) => HasKind (a, b) where
kindOf _ = KTuple [kindOf (Proxy @a), kindOf (Proxy @b)]
instance (HasKind a, HasKind b, HasKind c) => HasKind (a, b, c) where
kindOf _ = KTuple [kindOf (Proxy @a), kindOf (Proxy @b), kindOf (Proxy @c)]
instance (HasKind a, HasKind b, HasKind c, HasKind d) => HasKind (a, b, c, d) where
kindOf _ = KTuple [kindOf (Proxy @a), kindOf (Proxy @b), kindOf (Proxy @c), kindOf (Proxy @d)]
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e) => HasKind (a, b, c, d, e) where
kindOf _ = KTuple [kindOf (Proxy @a), kindOf (Proxy @b), kindOf (Proxy @c), kindOf (Proxy @d), kindOf (Proxy @e)]
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f) => HasKind (a, b, c, d, e, f) where
kindOf _ = KTuple [kindOf (Proxy @a), kindOf (Proxy @b), kindOf (Proxy @c), kindOf (Proxy @d), kindOf (Proxy @e), kindOf (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 _ = KTuple [kindOf (Proxy @a), kindOf (Proxy @b), kindOf (Proxy @c), kindOf (Proxy @d), kindOf (Proxy @e), kindOf (Proxy @f), kindOf (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 _ = KTuple [kindOf (Proxy @a), kindOf (Proxy @b), kindOf (Proxy @c), kindOf (Proxy @d), kindOf (Proxy @e), kindOf (Proxy @f), kindOf (Proxy @g), kindOf (Proxy @h)]
instance (HasKind a, HasKind b) => HasKind (Either a b) where
kindOf _ = KEither (kindOf (Proxy @a)) (kindOf (Proxy @b))
instance HasKind a => HasKind (Maybe a) where
kindOf _ = KMaybe (kindOf (Proxy @a))
needsFlattening :: Kind -> Bool
needsFlattening KBool = False
needsFlattening KBounded{} = False
needsFlattening KUnbounded = False
needsFlattening KReal = False
needsFlattening KUninterpreted{} = False
needsFlattening KFloat = False
needsFlattening KDouble = False
needsFlattening KChar = False
needsFlattening KString = False
needsFlattening KList{} = True
needsFlattening KSet{} = True
needsFlattening KTuple{} = True
needsFlattening KMaybe{} = True
needsFlattening KEither{} = True