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

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

module Data.SBV.Core.Kind (
          Kind(..), HasKind(..), smtType, hasUninterpretedSorts
        , BVIsNonZero, ValidFloat, intOfProxy
        , showBaseKind, needsFlattening
        , eqCheckIsObjectEq, containsFloats, isSomeKindOfFloat, expandKinds
        , substituteADTVars
        , kRoundingMode
        ) where

import qualified Data.Generics as G (Data(..), DataType, dataTypeName, tyconUQname)

import Data.Char (isSpace)
import Data.Int
import Data.Word
import Data.SBV.Core.AlgReals

import Data.Proxy
import Data.Kind

import Data.List (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 Data.SBV.Utils.Numeric (RoundingMode)

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

-- | Kind of symbolic value
data Kind =
          -- Base types
            KBool

          -- Word and Int. Boolean is True for Int.
          | KBounded !Bool !Int

          -- Unbounded integers
          | KUnbounded

          -- Reals
          | KReal

          -- Floats, standard and generalized
          | KFloat
          | KDouble
          | KFP !Int !Int

          -- Rationals
          | KRational

          -- Chars and strings
          | KChar
          | KString

          -- Algebraic datatypes
          | KVar String         -- only used temporarily during ADT construction
          | KApp String [Kind]  -- Application of a constructor to a bunch of types
          | KADT String
                 [(String, Kind)]   -- Parameters, applied to these args
                 [(String, [Kind])] -- Constructors, and their fields

          -- Collections
          | KList Kind
          | KSet  Kind
          | KTuple [Kind]

          -- Arrays
          | 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)

-- | Built in kind for rounding mode
kRoundingMode :: Kind
kRoundingMode :: Kind
kRoundingMode = String -> [(String, Kind)] -> [(String, [Kind])] -> Kind
KADT String
"RoundingMode" [] ((RoundingMode -> (String, [Kind]))
-> [RoundingMode] -> [(String, [Kind])]
forall a b. (a -> b) -> [a] -> [b]
map (\RoundingMode
r -> (RoundingMode -> String
forall a. Show a => a -> String
show RoundingMode
r, [])) [RoundingMode
forall a. Bounded a => a
minBound .. RoundingMode
forall a. Bounded a => a
maxBound :: RoundingMode])

-- | 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

-- | For an ADT kind, substitute kinds for the variables.
substituteADTVars :: String -> [(String, Kind)] -> Kind -> Kind
substituteADTVars :: String -> [(String, Kind)] -> Kind -> Kind
substituteADTVars String
t [(String, Kind)]
dict = (Kind -> Kind) -> Kind -> Kind
forall on. Uniplate on => (on -> on) -> on -> on
G.transform Kind -> Kind
sub
  where sub :: Kind -> Kind
        sub :: Kind -> Kind
sub (KVar String
v)
          | Just Kind
k <- String
v String -> [(String, Kind)] -> Maybe Kind
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(String, Kind)]
dict = Kind
k
          | Bool
True                      = String -> Kind
forall a. HasCallStack => String -> a
error (String -> Kind) -> String -> Kind
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.ADT: Kind find variable in param subst: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String, String, [(String, Kind)]) -> String
forall a. Show a => a -> String
show (String
t, String
v, [(String, Kind)]
dict)
        sub Kind
k = Kind
k

-- | The interesting about the show instance is that it can tell apart two kinds nicely. Otherwise the string produced isn't parsed back.
instance Show Kind where
  show :: Kind -> String
show (KVar String
s)           = String
s
  show Kind
KBool              = String
"SBool"
  show (KBounded Bool
False Int
n) = Int -> String -> String -> String
pickType Int
n String
"SWord" String
"SWord " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
  show (KBounded Bool
True Int
n)  = Int -> String -> String -> String
pickType Int
n String
"SInt"  String
"SInt "  String -> String -> String
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 (KApp String
c [Kind]
ks)        = [String] -> String
unwords (String
c String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Kind -> String) -> [Kind] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String
kindParen (String -> String) -> (Kind -> String) -> Kind -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> String
showBaseKind      )  [Kind]
ks)
  show (KADT String
s [(String, Kind)]
pks [(String, [Kind])]
_)     = [String] -> String
unwords (String
s String -> [String] -> [String]
forall a. a -> [a] -> [a]
: ((String, Kind) -> String) -> [(String, Kind)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String
kindParen (String -> String)
-> ((String, Kind) -> String) -> (String, Kind) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> String
showBaseKind (Kind -> String)
-> ((String, Kind) -> Kind) -> (String, Kind) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Kind) -> Kind
forall a b. (a, b) -> b
snd) [(String, Kind)]
pks)
  show Kind
KFloat             = String
"SFloat"
  show Kind
KDouble            = String
"SDouble"
  show (KFP Int
eb Int
sb)        = String
"SFloatingPoint " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
eb String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
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 -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]"
  show (KSet  Kind
e)          = String
"{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"
  show (KTuple [Kind]
m)         = String
"(" String -> String -> String
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 -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
  show Kind
KRational          = String
"SRational"
  show (KArray Kind
k1 Kind
k2)     = String
"SArray "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
kindParen (Kind -> String
showBaseKind Kind
k1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
kindParen (Kind -> String
showBaseKind Kind
k2)

-- | A version of show for kinds that says Bool instead of SBool, Float instead of SFloat, etc.
showBaseKind :: Kind -> String
showBaseKind :: Kind -> String
showBaseKind = Kind -> String
sh
  where sh :: Kind -> String
sh (KVar String
s)           = String
s
        sh k :: Kind
k@Kind
KBool            = String -> String
noS (Kind -> String
forall a. Show a => a -> String
show Kind
k)
        sh (KBounded Bool
False Int
n) = Int -> String -> String -> String
pickType Int
n String
"Word" String
"WordN " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
        sh (KBounded Bool
True Int
n)  = Int -> String -> String -> String
pickType Int
n String
"Int"  String
"IntN "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
        sh (KApp String
s [Kind]
ks)        = [String] -> String
unwords (String
s String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Kind -> String) -> [Kind] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String
kindParen (String -> String) -> (Kind -> String) -> Kind -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> String
sh) [Kind]
ks)
        sh k :: Kind
k@Kind
KUnbounded       = String -> String
noS (Kind -> String
forall a. Show a => a -> String
show Kind
k)
        sh k :: Kind
k@Kind
KReal            = String -> String
noS (Kind -> String
forall a. Show a => a -> String
show Kind
k)
        sh k :: Kind
k@KADT{}           = Kind -> String
forall a. Show a => a -> String
show Kind
k     -- Leave user-sorts untouched!
        sh k :: Kind
k@Kind
KFloat           = String -> String
noS (Kind -> String
forall a. Show a => a -> String
show Kind
k)
        sh k :: Kind
k@Kind
KDouble          = String -> String
noS (Kind -> String
forall a. Show a => a -> String
show Kind
k)
        sh k :: Kind
k@KFP{}            = String -> String
noS (Kind -> String
forall a. Show a => a -> String
show Kind
k)
        sh k :: Kind
k@Kind
KChar            = String -> String
noS (Kind -> String
forall a. Show a => a -> String
show Kind
k)
        sh k :: Kind
k@Kind
KString          = String -> String
noS (Kind -> String
forall a. Show a => a -> String
show Kind
k)
        sh Kind
KRational          = String
"Rational"
        sh (KList Kind
k)          = String
"[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
sh Kind
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]"
        sh (KSet Kind
k)           = String
"{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
sh Kind
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"
        sh (KTuple [Kind]
ks)        = String
"(" String -> String -> String
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 -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (KArray  Kind
k1 Kind
k2)    = String
"Array "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
kindParen (Kind -> String
sh Kind
k1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
kindParen (Kind -> String
sh Kind
k2)

        -- Drop the initial S if it's there
        noS :: String -> String
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 -> String -> String
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 :: String -> String
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 -> String -> String
forall a. a -> [a] -> [a]
: String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
            | Bool
True          = String
s

-- | How the type maps to SMT land
smtType :: Kind -> String
smtType :: Kind -> String
smtType (KVar String
s)        = String
s
smtType Kind
KBool           = String
"Bool"
smtType (KBounded Bool
_ Int
sz) = String
"(_ BitVec " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
sz String -> String -> String
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 -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
eb String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
sb String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
smtType Kind
KString         = String
"String"
smtType Kind
KChar           = String
"String"
smtType (KList Kind
k)       = String
"(Seq "   String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
smtType (KSet  Kind
k)       = String
"(Array " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" Bool)"
smtType (KApp String
s [Kind]
ks)     = String -> String
kindParen (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords (String
s String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Kind -> String) -> [Kind] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Kind -> String
smtType          [Kind]
ks)
smtType (KADT String
s [(String, Kind)]
pks [(String, [Kind])]
_)  = String -> String
kindParen (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords (String
s String -> [String] -> [String]
forall a. a -> [a] -> [a]
: ((String, Kind) -> String) -> [(String, Kind)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Kind -> String
smtType (Kind -> String)
-> ((String, Kind) -> Kind) -> (String, Kind) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Kind) -> Kind
forall a b. (a, b) -> b
snd) [(String, Kind)]
pks)
smtType (KTuple [])     = String
"SBVTuple0"
smtType (KTuple [Kind]
kinds)  = String
"(SBVTuple" String -> String -> String
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 -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
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 -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
smtType Kind
KRational       = String
"SBVRational"
smtType (KArray  Kind
k1 Kind
k2) = String
"(Array "      String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
k1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
k2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

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

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

-- | Does this kind represent a signed quantity?
kindHasSign :: Kind -> Bool
kindHasSign :: Kind -> Bool
kindHasSign = \case KVar String
_       -> Bool
False
                    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
                    KApp{}       -> Bool
False
                    KADT{}       -> Bool
False
                    Kind
KString      -> Bool
False
                    Kind
KChar        -> Bool
False
                    KList{}      -> Bool
False
                    KSet{}       -> Bool
False
                    KTuple{}     -> Bool
False
                    KArray{}     -> Bool
False

-- | 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
  isADT           :: a -> Bool
  isChar          :: a -> Bool
  isString        :: a -> Bool
  isList          :: a -> Bool
  isSet           :: a -> Bool
  isTuple         :: a -> Bool
  isArray         :: a -> Bool
  isRoundingMode  :: a -> Bool
  isUninterpreted :: 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
                  KVar{}        -> String -> Int
forall a. HasCallStack => String -> a
error String
"SBV.HasKind.intSizeOf(KVar)"
                  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)"
                  KApp String
s [Kind]
_      -> String -> Int
forall a. HasCallStack => String -> a
error (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ String
"SBV.HasKind.intSizeOf: Type application: "    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
                  KADT String
s [(String, Kind)]
_ [(String, [Kind])]
_    -> String -> Int
forall a. HasCallStack => String -> a
error (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ String
"SBV.HasKind.intSizeOf: Algebraic data type: " String -> String -> String
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 -> String -> String
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 -> String -> String
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 -> String -> String
forall a. [a] -> [a] -> [a]
++ [Kind] -> String
forall a. Show a => a -> String
show [Kind]
tys
                  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 -> String -> String
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

  isADT           (a -> Kind
forall a. HasKind a => a -> Kind
kindOf -> KADT{})       = Bool
True
  isADT           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

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

  -- Derived kinds
  isRoundingMode  (a -> Kind
forall a. HasKind a => a -> Kind
kindOf -> Kind
k)            = Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
kRoundingMode
  isUninterpreted (a -> Kind
forall a. HasKind a => a -> Kind
kindOf -> Kind
k)            = case Kind
k of
                                               KADT String
_ [] [] -> Bool
True
                                               Kind
_            -> 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

  {-# MINIMAL kindOf #-}

-- | 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
instance HasKind RoundingMode where kindOf :: RoundingMode -> Kind
kindOf RoundingMode
_ = Kind
kRoundingMode

-- | 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 -> String -> String
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. In short, this will return True if there are no floats/reals under the hood.
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
KReal   = Bool
True
        bad Kind
k       = Kind -> Bool
isSomeKindOfFloat Kind
k

-- | Same as above, except only for floats
containsFloats :: Kind -> Bool
containsFloats :: Kind -> Bool
containsFloats = (Kind -> Bool) -> [Kind] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
isSomeKindOfFloat ([Kind] -> Bool) -> (Kind -> [Kind]) -> Kind -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> [Kind]
expandKinds

-- | Is some sort of a float?
isSomeKindOfFloat :: Kind -> Bool
isSomeKindOfFloat :: Kind -> Bool
isSomeKindOfFloat Kind
k = Kind -> Bool
forall a. HasKind a => a -> Bool
isFloat Kind
k Bool -> Bool -> Bool
|| Kind -> Bool
forall a. HasKind a => a -> Bool
isDouble Kind
k Bool -> Bool -> Bool
|| Kind -> Bool
forall a. HasKind a => a -> Bool
isFP Kind
k

-- | 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
forall a. HasKind a => a -> Bool
isUninterpreted ([Kind] -> Bool) -> (Kind -> [Kind]) -> Kind -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> [Kind]
expandKinds

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 (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 KArray{}    = Bool
True
        check KApp{}      = Bool
True
        check k :: Kind
k@KADT{}    = Bool -> Bool
not (Kind -> Bool
forall a. HasKind a => a -> Bool
isUninterpreted Kind
k Bool -> Bool -> Bool
|| Kind -> Bool
forall a. HasKind a => a -> Bool
isRoundingMode Kind
k)

        -- no need to expand bases
        check KVar{}      = Bool
False
        check Kind
KBool       = Bool
False
        check KBounded{}  = Bool
False
        check Kind
KUnbounded  = Bool
False
        check Kind
KReal       = 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 _ = ()

-- 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.
-- 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))
                                       )