-----------------------------------------------------------------------------
-- |
-- 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 DeriveDataTypeable  #-}
{-# 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
          | KUserSort String (Maybe [String])  -- name. Uninterpreted, or enumeration constants.
          | 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, Typeable Kind
DataType
Constr
Typeable Kind
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Kind -> c Kind)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Kind)
-> (Kind -> Constr)
-> (Kind -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Kind))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Kind))
-> ((forall b. Data b => b -> b) -> Kind -> Kind)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r)
-> (forall u. (forall d. Data d => d -> u) -> Kind -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Kind -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Kind -> m Kind)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Kind -> m Kind)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Kind -> m Kind)
-> Data Kind
Kind -> DataType
Kind -> Constr
(forall b. Data b => b -> b) -> Kind -> Kind
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Kind -> c Kind
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Kind
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Kind -> u
forall u. (forall d. Data d => d -> u) -> Kind -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Kind -> m Kind
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Kind -> m Kind
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Kind
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Kind -> c Kind
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Kind)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Kind)
$cKEither :: Constr
$cKMaybe :: Constr
$cKTuple :: Constr
$cKSet :: Constr
$cKList :: Constr
$cKString :: Constr
$cKChar :: Constr
$cKDouble :: Constr
$cKFloat :: Constr
$cKUserSort :: Constr
$cKReal :: Constr
$cKUnbounded :: Constr
$cKBounded :: Constr
$cKBool :: Constr
$tKind :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Kind -> m Kind
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Kind -> m Kind
gmapMp :: (forall d. Data d => d -> m d) -> Kind -> m Kind
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Kind -> m Kind
gmapM :: (forall d. Data d => d -> m d) -> Kind -> m Kind
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Kind -> m Kind
gmapQi :: Int -> (forall d. Data d => d -> u) -> Kind -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Kind -> u
gmapQ :: (forall d. Data d => d -> u) -> Kind -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Kind -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r
gmapT :: (forall b. Data b => b -> b) -> Kind -> Kind
$cgmapT :: (forall b. Data b => b -> b) -> Kind -> Kind
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Kind)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Kind)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Kind)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Kind)
dataTypeOf :: Kind -> DataType
$cdataTypeOf :: Kind -> DataType
toConstr :: Kind -> Constr
$ctoConstr :: Kind -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Kind
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Kind
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Kind -> c Kind
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Kind -> c Kind
$cp1Data :: Typeable Kind
G.Data)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance (Typeable a, HasKind a) => HasKind [a] where
   kindOf :: [a] -> Kind
kindOf [a]
x | [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 (a, b)
_ = [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 (a, b, c)
_ = [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 (a, b, c, d)
_ = [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 (a, b, c, d, e)
_ = [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 (a, b, c, d, e, f)
_ = [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 (a, b, c, d, e, f, g)
_ = [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 (a, b, c, d, e, f, g, h)
_ = [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 Either a b
_ = 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 Maybe a
_ = 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 Kind
KBool       = Bool
False
needsFlattening KBounded{}  = Bool
False
needsFlattening Kind
KUnbounded  = Bool
False
needsFlattening Kind
KReal       = Bool
False
needsFlattening KUserSort{} = Bool
False
needsFlattening Kind
KFloat      = Bool
False
needsFlattening Kind
KDouble     = Bool
False
needsFlattening Kind
KChar       = Bool
False
needsFlattening Kind
KString     = Bool
False
needsFlattening KList{}     = Bool
True
needsFlattening KSet{}      = Bool
True
needsFlattening KTuple{}    = Bool
True
needsFlattening KMaybe{}    = Bool
True
needsFlattening KEither{}   = Bool
True