-----------------------------------------------------------------------------
-- |
-- 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 CPP                  #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE DefaultSignatures    #-}
{-# LANGUAGE DeriveDataTypeable   #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE LambdaCase           #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE ViewPatterns         #-}
{-# LANGUAGE UndecidableInstances #-}

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

module Data.SBV.Core.Kind (
          Kind(..), HasKind(..), constructUKind, smtType, hasUninterpretedSorts
        , BVIsNonZero, ValidFloat, intOfProxy
        , showBaseKind, needsFlattening, RoundingMode(..), smtRoundingMode
        ) 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.Kind

import Data.List (isPrefixOf, intercalate)

import Data.Typeable (Typeable)
import Data.Type.Bool
import Data.Type.Equality

import GHC.TypeLits

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
          | KFP !Int !Int
          | KChar
          | KString
          | KList Kind
          | KSet  Kind
          | KTuple [Kind]
          | KMaybe  Kind
          | KRational
          | 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
$cKRational :: Constr
$cKMaybe :: Constr
$cKTuple :: Constr
$cKSet :: Constr
$cKList :: Constr
$cKString :: Constr
$cKChar :: Constr
$cKFP :: 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 (KFP Int
eb Int
sb)        = String
"SFloatingPoint " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
eb String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
sb
  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)
  show Kind
KRational          = String
"SRational"

-- | 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@KFP{}            = 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 Kind
KRational          = String
"Rational"
        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 (KFP Int
eb Int
sb)     = String
"(_ FloatingPoint " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
eb String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
sb String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
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 Kind
KRational       = String
"SBVRational"
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
                    KFP{}        -> Bool
True
                    Kind
KRational    -> 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"
                      , String
"SRational"
                      ]

        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
  isRational  :: a -> Bool
  isFP        :: 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        -> Int
32
                  Kind
KDouble       -> Int
64
                  KFP Int
i Int
j       -> Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
j
                  Kind
KRational     -> String -> Int
forall a. HasCallStack => String -> a
error String
"SBV.HasKind.intSizeOf((S)Rational)"
                  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

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

  isRational      (a -> Kind
forall a. HasKind a => a -> Kind
kindOf -> KRational{})  = Bool
True
  isRational      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 Rational where kindOf :: Rational -> Kind
kindOf Rational
_ = Kind
KRational
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

-- | Grab the bit-size from the proxy. If the nat is too large to fit in an int,
-- we throw an error. (This would mean too big of a bit-size, that we can't
-- really deal with in any practical realm.) In fact, even the range allowed
-- by this conversion (i.e., the entire range of a 64-bit int) is just impractical,
-- but it's hard to come up with a better bound.
intOfProxy :: KnownNat n => Proxy n -> Int
intOfProxy :: Proxy n -> Int
intOfProxy Proxy n
p
  | Integer
iv Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
r = Int
r
  | Bool
True                 = String -> Int
forall a. HasCallStack => String -> a
error (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"Data.SBV: Too large bit-vector size: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
iv
                                           , String
""
                                           , String
"No reasonable proof can be performed with such large bit vectors involved,"
                                           , String
"So, cowardly refusing to proceed any further! Please file this as a"
                                           , String
"feature request."
                                           ]
  where iv :: Integer
        iv :: Integer
iv = Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Proxy n
p

        r :: Int
        r :: Int
r  = Integer -> Int
forall a. Enum a => a -> Int
fromEnum Integer
iv

-- | 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 KFP{}                  = Bool
False
hasUninterpretedSorts Kind
KRational              = 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 KFP{}       = Bool
False
needsFlattening Kind
KRational   = 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

-- | Catch 0-width cases
type BVZeroWidth = 'Text "Zero-width bit-vectors are not allowed."

-- | Type family to create the appropriate non-zero constraint
type family BVIsNonZero (arg :: Nat) :: Constraint where
   BVIsNonZero 0 = TypeError BVZeroWidth
   BVIsNonZero _ = ()

#include "MachDeps.h"

-- Allowed sizes for floats, imposed by LibBF.
--
-- NB. In LibBF bindings (and libbf itself as well), minimum number of exponent bits is specified as 3. But this
-- seems unnecessarily restrictive; that constant doesn't seem to be used anywhere, and furthermore my tests with sb = 2
-- didn't reveal anything going wrong. I emailed the author of libbf regarding this, and he said:
--
--   I had no clear reason to use BF_EXP_BITS_MIN = 3. So if "2" is OK then
--   why not. The important is that the basic operations are OK. It is likely
--   there are tricky cases in the transcendental operations but even with
--   large exponents libbf may have problems with them !
--
-- So, in SBV, we allow sb == 2. If this proves problematic, change the number below in definition of FP_MIN_EB to 3!
--
-- NB. It would be nice if we could use the LibBF constants expBitsMin, expBitsMax, precBitsMin, precBitsMax
-- for determining the valid range. Unfortunately this doesn't seem to be possible.
-- See <https://stackoverflow.com/questions/51900360/making-a-type-constraint-based-on-runtime-value-of-maxbound-int> for a discussion.
-- So, we use CPP to work-around that.
#define FP_MIN_EB 2
#define FP_MIN_SB 2
#if WORD_SIZE_IN_BITS == 64
#define FP_MAX_EB 61
#define FP_MAX_SB 4611686018427387902
#else
#define FP_MAX_EB 29
#define FP_MAX_SB 1073741822
#endif

-- | Catch an invalid FP.
type InvalidFloat (eb :: Nat) (sb :: Nat)
        =     'Text "Invalid floating point type `SFloatingPoint " ':<>: 'ShowType eb ':<>: 'Text " " ':<>: 'ShowType sb ':<>: 'Text "'"
        ':$$: 'Text ""
        ':$$: 'Text "A valid float of type 'SFloatingPoint eb sb' must satisfy:"
        ':$$: 'Text "     eb `elem` [" ':<>: 'ShowType FP_MIN_EB ':<>: 'Text " .. " ':<>: 'ShowType FP_MAX_EB ':<>: 'Text "]"
        ':$$: 'Text "     sb `elem` [" ':<>: 'ShowType FP_MIN_SB ':<>: 'Text " .. " ':<>: 'ShowType FP_MAX_SB ':<>: 'Text "]"
        ':$$: 'Text ""
        ':$$: 'Text "Given type falls outside of this range, or the sizes are not known naturals."

-- | A valid float has restrictions on eb/sb values.
-- NB. In the below encoding, I found that CPP is very finicky about substitution of the machine-dependent
-- macros. If you try to put the conditionals in the same line, it fails to substitute for some reason. Hence the awkward spacing.
-- Filed this as a bug report for CPPHS at <https://github.com/malcolmwallace/cpphs/issues/25>.
type family ValidFloat (eb :: Nat) (sb :: Nat) :: Constraint where
  ValidFloat (eb :: Nat) (sb :: Nat) = ( KnownNat eb
                                       , KnownNat sb
                                       , If (   (   eb `CmpNat` FP_MIN_EB == 'EQ
                                                 || eb `CmpNat` FP_MIN_EB == 'GT)
                                             && (   eb `CmpNat` FP_MAX_EB == 'EQ
                                                 || eb `CmpNat` FP_MAX_EB == 'LT)
                                             && (   sb `CmpNat` FP_MIN_SB == 'EQ
                                                 || sb `CmpNat` FP_MIN_SB == 'GT)
                                             && (   sb `CmpNat` FP_MAX_SB == 'EQ
                                                 || sb `CmpNat` FP_MAX_SB == 'LT))
                                            (() :: Constraint)
                                            (TypeError (InvalidFloat eb sb))
                                       )

-- | Rounding mode to be used for the IEEE floating-point operations.
-- Note that Haskell's default is 'RoundNearestTiesToEven'. If you use
-- a different rounding mode, then the counter-examples you get may not
-- match what you observe in Haskell.
data RoundingMode = RoundNearestTiesToEven  -- ^ Round to nearest representable floating point value.
                                            -- If precisely at half-way, pick the even number.
                                            -- (In this context, /even/ means the lowest-order bit is zero.)
                  | RoundNearestTiesToAway  -- ^ Round to nearest representable floating point value.
                                            -- If precisely at half-way, pick the number further away from 0.
                                            -- (That is, for positive values, pick the greater; for negative values, pick the smaller.)
                  | RoundTowardPositive     -- ^ Round towards positive infinity. (Also known as rounding-up or ceiling.)
                  | RoundTowardNegative     -- ^ Round towards negative infinity. (Also known as rounding-down or floor.)
                  | RoundTowardZero         -- ^ Round towards zero. (Also known as truncation.)
                  deriving (RoundingMode -> RoundingMode -> Bool
(RoundingMode -> RoundingMode -> Bool)
-> (RoundingMode -> RoundingMode -> Bool) -> Eq RoundingMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RoundingMode -> RoundingMode -> Bool
$c/= :: RoundingMode -> RoundingMode -> Bool
== :: RoundingMode -> RoundingMode -> Bool
$c== :: RoundingMode -> RoundingMode -> Bool
Eq, Eq RoundingMode
Eq RoundingMode
-> (RoundingMode -> RoundingMode -> Ordering)
-> (RoundingMode -> RoundingMode -> Bool)
-> (RoundingMode -> RoundingMode -> Bool)
-> (RoundingMode -> RoundingMode -> Bool)
-> (RoundingMode -> RoundingMode -> Bool)
-> (RoundingMode -> RoundingMode -> RoundingMode)
-> (RoundingMode -> RoundingMode -> RoundingMode)
-> Ord RoundingMode
RoundingMode -> RoundingMode -> Bool
RoundingMode -> RoundingMode -> Ordering
RoundingMode -> RoundingMode -> RoundingMode
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 :: RoundingMode -> RoundingMode -> RoundingMode
$cmin :: RoundingMode -> RoundingMode -> RoundingMode
max :: RoundingMode -> RoundingMode -> RoundingMode
$cmax :: RoundingMode -> RoundingMode -> RoundingMode
>= :: RoundingMode -> RoundingMode -> Bool
$c>= :: RoundingMode -> RoundingMode -> Bool
> :: RoundingMode -> RoundingMode -> Bool
$c> :: RoundingMode -> RoundingMode -> Bool
<= :: RoundingMode -> RoundingMode -> Bool
$c<= :: RoundingMode -> RoundingMode -> Bool
< :: RoundingMode -> RoundingMode -> Bool
$c< :: RoundingMode -> RoundingMode -> Bool
compare :: RoundingMode -> RoundingMode -> Ordering
$ccompare :: RoundingMode -> RoundingMode -> Ordering
$cp1Ord :: Eq RoundingMode
Ord, Int -> RoundingMode -> ShowS
[RoundingMode] -> ShowS
RoundingMode -> String
(Int -> RoundingMode -> ShowS)
-> (RoundingMode -> String)
-> ([RoundingMode] -> ShowS)
-> Show RoundingMode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RoundingMode] -> ShowS
$cshowList :: [RoundingMode] -> ShowS
show :: RoundingMode -> String
$cshow :: RoundingMode -> String
showsPrec :: Int -> RoundingMode -> ShowS
$cshowsPrec :: Int -> RoundingMode -> ShowS
Show, ReadPrec [RoundingMode]
ReadPrec RoundingMode
Int -> ReadS RoundingMode
ReadS [RoundingMode]
(Int -> ReadS RoundingMode)
-> ReadS [RoundingMode]
-> ReadPrec RoundingMode
-> ReadPrec [RoundingMode]
-> Read RoundingMode
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [RoundingMode]
$creadListPrec :: ReadPrec [RoundingMode]
readPrec :: ReadPrec RoundingMode
$creadPrec :: ReadPrec RoundingMode
readList :: ReadS [RoundingMode]
$creadList :: ReadS [RoundingMode]
readsPrec :: Int -> ReadS RoundingMode
$creadsPrec :: Int -> ReadS RoundingMode
Read, Typeable RoundingMode
DataType
Constr
Typeable RoundingMode
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> RoundingMode -> c RoundingMode)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c RoundingMode)
-> (RoundingMode -> Constr)
-> (RoundingMode -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c RoundingMode))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c RoundingMode))
-> ((forall b. Data b => b -> b) -> RoundingMode -> RoundingMode)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r)
-> (forall u. (forall d. Data d => d -> u) -> RoundingMode -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> RoundingMode -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode)
-> Data RoundingMode
RoundingMode -> DataType
RoundingMode -> Constr
(forall b. Data b => b -> b) -> RoundingMode -> RoundingMode
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RoundingMode -> c RoundingMode
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RoundingMode
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) -> RoundingMode -> u
forall u. (forall d. Data d => d -> u) -> RoundingMode -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RoundingMode
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RoundingMode -> c RoundingMode
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RoundingMode)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c RoundingMode)
$cRoundTowardZero :: Constr
$cRoundTowardNegative :: Constr
$cRoundTowardPositive :: Constr
$cRoundNearestTiesToAway :: Constr
$cRoundNearestTiesToEven :: Constr
$tRoundingMode :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
gmapMp :: (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
gmapM :: (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
gmapQi :: Int -> (forall d. Data d => d -> u) -> RoundingMode -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> RoundingMode -> u
gmapQ :: (forall d. Data d => d -> u) -> RoundingMode -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> RoundingMode -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
gmapT :: (forall b. Data b => b -> b) -> RoundingMode -> RoundingMode
$cgmapT :: (forall b. Data b => b -> b) -> RoundingMode -> RoundingMode
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c RoundingMode)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c RoundingMode)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c RoundingMode)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RoundingMode)
dataTypeOf :: RoundingMode -> DataType
$cdataTypeOf :: RoundingMode -> DataType
toConstr :: RoundingMode -> Constr
$ctoConstr :: RoundingMode -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RoundingMode
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RoundingMode
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RoundingMode -> c RoundingMode
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RoundingMode -> c RoundingMode
$cp1Data :: Typeable RoundingMode
G.Data, RoundingMode
RoundingMode -> RoundingMode -> Bounded RoundingMode
forall a. a -> a -> Bounded a
maxBound :: RoundingMode
$cmaxBound :: RoundingMode
minBound :: RoundingMode
$cminBound :: RoundingMode
Bounded, Int -> RoundingMode
RoundingMode -> Int
RoundingMode -> [RoundingMode]
RoundingMode -> RoundingMode
RoundingMode -> RoundingMode -> [RoundingMode]
RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode]
(RoundingMode -> RoundingMode)
-> (RoundingMode -> RoundingMode)
-> (Int -> RoundingMode)
-> (RoundingMode -> Int)
-> (RoundingMode -> [RoundingMode])
-> (RoundingMode -> RoundingMode -> [RoundingMode])
-> (RoundingMode -> RoundingMode -> [RoundingMode])
-> (RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode])
-> Enum RoundingMode
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode]
$cenumFromThenTo :: RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode]
enumFromTo :: RoundingMode -> RoundingMode -> [RoundingMode]
$cenumFromTo :: RoundingMode -> RoundingMode -> [RoundingMode]
enumFromThen :: RoundingMode -> RoundingMode -> [RoundingMode]
$cenumFromThen :: RoundingMode -> RoundingMode -> [RoundingMode]
enumFrom :: RoundingMode -> [RoundingMode]
$cenumFrom :: RoundingMode -> [RoundingMode]
fromEnum :: RoundingMode -> Int
$cfromEnum :: RoundingMode -> Int
toEnum :: Int -> RoundingMode
$ctoEnum :: Int -> RoundingMode
pred :: RoundingMode -> RoundingMode
$cpred :: RoundingMode -> RoundingMode
succ :: RoundingMode -> RoundingMode
$csucc :: RoundingMode -> RoundingMode
Enum)

-- | 'RoundingMode' kind
instance HasKind RoundingMode

-- | Convert a rounding mode to the format SMT-Lib2 understands.
smtRoundingMode :: RoundingMode -> String
smtRoundingMode :: RoundingMode -> String
smtRoundingMode RoundingMode
RoundNearestTiesToEven = String
"roundNearestTiesToEven"
smtRoundingMode RoundingMode
RoundNearestTiesToAway = String
"roundNearestTiesToAway"
smtRoundingMode RoundingMode
RoundTowardPositive    = String
"roundTowardPositive"
smtRoundingMode RoundingMode
RoundTowardNegative    = String
"roundTowardNegative"
smtRoundingMode RoundingMode
RoundTowardZero        = String
"roundTowardZero"