-----------------------------------------------------------------------------
-- |
-- 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 DeriveAnyClass       #-}
{-# LANGUAGE DeriveDataTypeable   #-}
{-# LANGUAGE DeriveGeneric        #-}
{-# 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
        , eqCheckIsObjectEq, expandKinds
        ) 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, sort)
import Control.DeepSeq (NFData)

import Data.Containers.ListUtils (nubOrd)

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

import GHC.TypeLits

import Data.SBV.Utils.Lib (isKString)

import GHC.Generics
import qualified Data.Generics.Uniplate.Data as G

-- | 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
          | KArray  Kind Kind
          deriving (Kind -> Kind -> Bool
(Kind -> Kind -> Bool) -> (Kind -> Kind -> Bool) -> Eq Kind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Kind -> Kind -> Bool
== :: Kind -> Kind -> Bool
$c/= :: Kind -> Kind -> Bool
/= :: 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
$ccompare :: Kind -> Kind -> Ordering
compare :: Kind -> Kind -> Ordering
$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
>= :: Kind -> Kind -> Bool
$cmax :: Kind -> Kind -> Kind
max :: Kind -> Kind -> Kind
$cmin :: Kind -> Kind -> Kind
min :: Kind -> Kind -> Kind
Ord, Typeable Kind
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 -> Constr
Kind -> DataType
(forall b. Data b => b -> b) -> Kind -> 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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Kind -> c Kind
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Kind -> c Kind
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Kind
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Kind
$ctoConstr :: Kind -> Constr
toConstr :: Kind -> Constr
$cdataTypeOf :: Kind -> DataType
dataTypeOf :: Kind -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Kind)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Kind)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Kind)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Kind)
$cgmapT :: (forall b. Data b => b -> b) -> Kind -> Kind
gmapT :: (forall b. Data b => b -> b) -> Kind -> Kind
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r
gmapQl :: forall r r'.
(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
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Kind -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Kind -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Kind -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Kind -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Kind -> m Kind
gmapM :: forall (m :: * -> *).
Monad m =>
(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
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(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
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Kind -> m Kind
G.Data, Kind -> ()
(Kind -> ()) -> NFData Kind
forall a. (a -> ()) -> NFData a
$crnf :: Kind -> ()
rnf :: Kind -> ()
NFData, (forall x. Kind -> Rep Kind x)
-> (forall x. Rep Kind x -> Kind) -> Generic Kind
forall x. Rep Kind x -> Kind
forall x. Kind -> Rep Kind x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Kind -> Rep Kind x
from :: forall x. Kind -> Rep Kind x
$cto :: forall x. Rep Kind x -> Kind
to :: forall x. Rep Kind x -> Kind
Generic)

-- Expand such that the resulting list has all the kinds we touch
expandKinds :: Kind -> [Kind]
expandKinds :: Kind -> [Kind]
expandKinds = [Kind] -> [Kind]
forall a. Ord a => [a] -> [a]
sort ([Kind] -> [Kind]) -> (Kind -> [Kind]) -> Kind -> [Kind]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Kind] -> [Kind]
forall a. Ord a => [a] -> [a]
nubOrd ([Kind] -> [Kind]) -> (Kind -> [Kind]) -> Kind -> [Kind]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> [Kind]
forall on. Uniplate on => on -> [on]
G.universe

-- | 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 Kind
KRational          = String
"SRational"
  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 (KArray Kind
k1 Kind
k2)     = String
"SArray "  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@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)
        sh (KArray  Kind
k1 Kind
k2)    = String
"Array "  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 a. Eq a => a -> [a] -> 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 a. [a] -> 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
")"
smtType (KArray  Kind
k1 Kind
k2) = String
"(Array "      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
                    KArray{}     -> 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 :: forall a. (Read a, Data a) => 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
  isArray     :: 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)
                  KArray  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)Array)"  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

  isArray         (a -> Kind
forall a. HasKind a => a -> Kind
kindOf -> KArray{})     = Bool
True
  isArray         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 :: forall (n :: Nat). KnownNat n => 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

-- | Is this a type we can safely do equality on? Essentially it avoids floats (@NaN@ /= @NaN@, @+0 = -0@), and reals (due
-- to the possible presence of non-exact rationals.
eqCheckIsObjectEq :: Kind -> Bool
eqCheckIsObjectEq :: Kind -> Bool
eqCheckIsObjectEq = Bool -> Bool
not (Bool -> Bool) -> (Kind -> Bool) -> Kind -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Kind -> Bool) -> [Kind] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
bad ([Kind] -> Bool) -> (Kind -> [Kind]) -> Kind -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> [Kind]
expandKinds
  where bad :: Kind -> Bool
bad Kind
KFloat  = Bool
True
        bad Kind
KDouble = Bool
True
        bad KFP{}   = Bool
True
        bad Kind
KReal   = Bool
True
        bad Kind
_       = Bool
False

-- | Do we have a completely uninterpreted sort lying around anywhere?
hasUninterpretedSorts :: Kind -> Bool
hasUninterpretedSorts :: Kind -> Bool
hasUninterpretedSorts = (Kind -> Bool) -> [Kind] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
check ([Kind] -> Bool) -> (Kind -> [Kind]) -> Kind -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> [Kind]
expandKinds
  where check :: Kind -> Bool
check (KUserSort String
_ Maybe [String]
Nothing)  = Bool
True   -- These are the completely uninterpreted sorts, which we are looking for here
        check (KUserSort String
_ (Just{})) = Bool
False  -- These are the enumerated sorts, and they are perfectly fine
        check Kind
_                      = Bool
False

instance (Typeable a, HasKind a) => HasKind [a] where
   kindOf :: [a] -> Kind
kindOf [a]
x | 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 (forall t. Proxy t
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 (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a), Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
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 (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a), Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b), Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
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 (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a), Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b), Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @c), Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
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 (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a), Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b), Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @c), Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @d), Proxy e -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
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 (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a), Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b), Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @c), Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @d), Proxy e -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @e), Proxy f -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
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 (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a), Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b), Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @c), Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @d), Proxy e -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @e), Proxy f -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @f), Proxy g -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
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 (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a), Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b), Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @c), Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @d), Proxy e -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @e), Proxy f -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @f), Proxy g -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @g), Proxy h -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
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 (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) (Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
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 (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a))

instance (HasKind a, HasKind b) => HasKind (a -> b) where
  kindOf :: (a -> b) -> Kind
kindOf a -> b
_ = Kind -> Kind -> Kind
KArray (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) (Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b))

-- | 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 -> Bool) -> [Kind] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
check ([Kind] -> Bool) -> (Kind -> [Kind]) -> Kind -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> [Kind]
expandKinds
  where check :: Kind -> Bool
check KList{}     = Bool
True
        check KSet{}      = Bool
True
        check KTuple{}    = Bool
True
        check KMaybe{}    = Bool
True
        check KEither{}   = Bool
True
        check KArray{}    = Bool
True

        -- no need to expand bases
        check Kind
KBool       = Bool
False
        check KBounded{}  = Bool
False
        check Kind
KUnbounded  = Bool
False
        check Kind
KReal       = Bool
False
        check KUserSort{} = Bool
False
        check Kind
KFloat      = Bool
False
        check Kind
KDouble     = Bool
False
        check KFP{}       = Bool
False
        check Kind
KChar       = Bool
False
        check Kind
KString     = Bool
False
        check Kind
KRational   = Bool
False

-- | 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
$c== :: RoundingMode -> RoundingMode -> Bool
== :: RoundingMode -> RoundingMode -> Bool
$c/= :: RoundingMode -> RoundingMode -> Bool
/= :: 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
$ccompare :: RoundingMode -> RoundingMode -> Ordering
compare :: RoundingMode -> RoundingMode -> Ordering
$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
>= :: RoundingMode -> RoundingMode -> Bool
$cmax :: RoundingMode -> RoundingMode -> RoundingMode
max :: RoundingMode -> RoundingMode -> RoundingMode
$cmin :: RoundingMode -> RoundingMode -> RoundingMode
min :: RoundingMode -> RoundingMode -> 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
$cshowsPrec :: Int -> RoundingMode -> ShowS
showsPrec :: Int -> RoundingMode -> ShowS
$cshow :: RoundingMode -> String
show :: RoundingMode -> String
$cshowList :: [RoundingMode] -> ShowS
showList :: [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
$creadsPrec :: Int -> ReadS RoundingMode
readsPrec :: Int -> ReadS RoundingMode
$creadList :: ReadS [RoundingMode]
readList :: ReadS [RoundingMode]
$creadPrec :: ReadPrec RoundingMode
readPrec :: ReadPrec RoundingMode
$creadListPrec :: ReadPrec [RoundingMode]
readListPrec :: ReadPrec [RoundingMode]
Read, Typeable RoundingMode
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 -> Constr
RoundingMode -> DataType
(forall b. Data b => b -> b) -> RoundingMode -> 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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RoundingMode -> c RoundingMode
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RoundingMode -> c RoundingMode
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RoundingMode
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RoundingMode
$ctoConstr :: RoundingMode -> Constr
toConstr :: RoundingMode -> Constr
$cdataTypeOf :: RoundingMode -> DataType
dataTypeOf :: RoundingMode -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RoundingMode)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RoundingMode)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c RoundingMode)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c RoundingMode)
$cgmapT :: (forall b. Data b => b -> b) -> RoundingMode -> RoundingMode
gmapT :: (forall b. Data b => b -> b) -> RoundingMode -> RoundingMode
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
gmapQl :: forall r r'.
(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
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> RoundingMode -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> RoundingMode -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> RoundingMode -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> RoundingMode -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
gmapM :: forall (m :: * -> *).
Monad m =>
(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
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(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
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
G.Data, RoundingMode
RoundingMode -> RoundingMode -> Bounded RoundingMode
forall a. a -> a -> Bounded a
$cminBound :: RoundingMode
minBound :: RoundingMode
$cmaxBound :: RoundingMode
maxBound :: 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
$csucc :: RoundingMode -> RoundingMode
succ :: RoundingMode -> RoundingMode
$cpred :: RoundingMode -> RoundingMode
pred :: RoundingMode -> RoundingMode
$ctoEnum :: Int -> RoundingMode
toEnum :: Int -> RoundingMode
$cfromEnum :: RoundingMode -> Int
fromEnum :: RoundingMode -> Int
$cenumFrom :: RoundingMode -> [RoundingMode]
enumFrom :: RoundingMode -> [RoundingMode]
$cenumFromThen :: RoundingMode -> RoundingMode -> [RoundingMode]
enumFromThen :: RoundingMode -> RoundingMode -> [RoundingMode]
$cenumFromTo :: RoundingMode -> RoundingMode -> [RoundingMode]
enumFromTo :: RoundingMode -> RoundingMode -> [RoundingMode]
$cenumFromThenTo :: RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode]
enumFromThenTo :: RoundingMode -> RoundingMode -> 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"