-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Core.Concrete
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Operations on concrete values
-----------------------------------------------------------------------------

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE Rank2Types          #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Core.Concrete
  ( module Data.SBV.Core.Concrete
  ) where

import Control.Monad (replicateM)

import Data.Bits
import System.Random (randomIO, randomRIO)

import Data.Char (chr, isSpace)
import Data.List (isPrefixOf, intercalate)

import Data.SBV.Core.Kind
import Data.SBV.Core.AlgReals
import Data.SBV.Core.SizedFloats

import Data.Proxy

import Data.SBV.Utils.Numeric (fpIsEqualObjectH, fpCompareObjectH)

import Data.Set (Set)
import qualified Data.Set as Set

-- | A 'RCSet' is either a regular set or a set given by its complement from the corresponding universal set.
data RCSet a = RegularSet    (Set a)
             | ComplementSet (Set a)

-- | Show instance. Regular sets are shown as usual.
-- Complements are shown "U -" notation.
instance Show a => Show (RCSet a) where
  show :: RCSet a -> String
show RCSet a
rcs = case RCSet a
rcs of
               ComplementSet Set a
s | forall a. Set a -> Bool
Set.null Set a
s -> String
"U"
                               | Bool
True       -> String
"U - " forall a. [a] -> [a] -> [a]
++ forall {a}. Show a => [a] -> String
sh (forall a. Set a -> [a]
Set.toAscList Set a
s)
               RegularSet    Set a
s              ->           forall {a}. Show a => [a] -> String
sh (forall a. Set a -> [a]
Set.toAscList Set a
s)
   where sh :: [a] -> String
sh [a]
xs = Char
'{' forall a. a -> [a] -> [a]
: forall a. [a] -> [[a]] -> [a]
intercalate String
"," (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [a]
xs) forall a. [a] -> [a] -> [a]
++ String
"}"

-- | Structural equality for 'RCSet'. We need Eq/Ord instances for 'RCSet' because we want to put them in maps/tables. But
-- we don't want to derive these, nor make it an instance! Why? Because the same set can have multiple representations if the underlying
-- type is finite. For instance, @{True} = U - {False}@ for boolean sets! Instead, we use the following two functions,
-- which are equivalent to Eq/Ord instances and work for our purposes, but we do not export these to the user.
eqRCSet :: Eq a => RCSet a -> RCSet a -> Bool
eqRCSet :: forall a. Eq a => RCSet a -> RCSet a -> Bool
eqRCSet (RegularSet    Set a
a) (RegularSet    Set a
b) = Set a
a forall a. Eq a => a -> a -> Bool
== Set a
b
eqRCSet (ComplementSet Set a
a) (ComplementSet Set a
b) = Set a
a forall a. Eq a => a -> a -> Bool
== Set a
b
eqRCSet RCSet a
_                 RCSet a
_                 = Bool
False

-- | Comparing 'RCSet' values. See comments for 'eqRCSet' on why we don't define the 'Ord' instance.
compareRCSet :: Ord a => RCSet a -> RCSet a -> Ordering
compareRCSet :: forall a. Ord a => RCSet a -> RCSet a -> Ordering
compareRCSet (RegularSet    Set a
a) (RegularSet    Set a
b) = Set a
a forall a. Ord a => a -> a -> Ordering
`compare` Set a
b
compareRCSet (RegularSet    Set a
_) (ComplementSet Set a
_) = Ordering
LT
compareRCSet (ComplementSet Set a
_) (RegularSet    Set a
_) = Ordering
GT
compareRCSet (ComplementSet Set a
a) (ComplementSet Set a
b) = Set a
a forall a. Ord a => a -> a -> Ordering
`compare` Set a
b

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

-- | A constant value
data CVal = CAlgReal  !AlgReal             -- ^ Algebraic real
          | CInteger  !Integer             -- ^ Bit-vector/unbounded integer
          | CFloat    !Float               -- ^ Float
          | CDouble   !Double              -- ^ Double
          | CFP       !FP                  -- ^ Arbitrary float
          | CRational Rational             -- ^ Rational
          | CChar     !Char                -- ^ Character
          | CString   !String              -- ^ String
          | CList     ![CVal]              -- ^ List
          | CSet      !(RCSet CVal)        -- ^ Set. Can be regular or complemented.
          | CUserSort !(Maybe Int, String) -- ^ Value of an uninterpreted/user kind. The Maybe Int shows index position for enumerations
          | CTuple    ![CVal]              -- ^ Tuple
          | CMaybe    !(Maybe CVal)        -- ^ Maybe
          | CEither   !(Either CVal CVal)  -- ^ Disjoint union

-- | Assign a rank to constant values, this is structural and helps with ordering
cvRank :: CVal -> Int
cvRank :: CVal -> Int
cvRank CAlgReal  {} =  Int
0
cvRank CInteger  {} =  Int
1
cvRank CFloat    {} =  Int
2
cvRank CDouble   {} =  Int
3
cvRank CFP       {} =  Int
4
cvRank CRational {} =  Int
5
cvRank CChar     {} =  Int
6
cvRank CString   {} =  Int
7
cvRank CList     {} =  Int
8
cvRank CSet      {} =  Int
9
cvRank CUserSort {} = Int
10
cvRank CTuple    {} = Int
11
cvRank CMaybe    {} = Int
12
cvRank CEither   {} = Int
13

-- | Eq instance for CVVal. Note that we cannot simply derive Eq/Ord, since CVAlgReal doesn't have proper
-- instances for these when values are infinitely precise reals. However, we do
-- need a structural eq/ord for Map indexes; so define custom ones here:
instance Eq CVal where
  CAlgReal  AlgReal
a == :: CVal -> CVal -> Bool
== CAlgReal  AlgReal
b = AlgReal
a AlgReal -> AlgReal -> Bool
`algRealStructuralEqual` AlgReal
b
  CInteger  Integer
a == CInteger  Integer
b = Integer
a forall a. Eq a => a -> a -> Bool
== Integer
b
  CFloat    Float
a == CFloat    Float
b = Float
a forall a. RealFloat a => a -> a -> Bool
`fpIsEqualObjectH` Float
b   -- We don't want +0/-0 to be confused; and also we want NaN = NaN here!
  CDouble   Double
a == CDouble   Double
b = Double
a forall a. RealFloat a => a -> a -> Bool
`fpIsEqualObjectH` Double
b   -- ditto
  CRational Rational
a == CRational Rational
b = Rational
a forall a. Eq a => a -> a -> Bool
== Rational
b
  CChar     Char
a == CChar     Char
b = Char
a forall a. Eq a => a -> a -> Bool
== Char
b
  CString   String
a == CString   String
b = String
a forall a. Eq a => a -> a -> Bool
== String
b
  CList     [CVal]
a == CList     [CVal]
b = [CVal]
a forall a. Eq a => a -> a -> Bool
== [CVal]
b
  CSet      RCSet CVal
a == CSet      RCSet CVal
b = RCSet CVal
a forall a. Eq a => RCSet a -> RCSet a -> Bool
`eqRCSet` RCSet CVal
b
  CUserSort (Maybe Int, String)
a == CUserSort (Maybe Int, String)
b = (Maybe Int, String)
a forall a. Eq a => a -> a -> Bool
== (Maybe Int, String)
b
  CTuple    [CVal]
a == CTuple    [CVal]
b = [CVal]
a forall a. Eq a => a -> a -> Bool
== [CVal]
b
  CMaybe    Maybe CVal
a == CMaybe    Maybe CVal
b = Maybe CVal
a forall a. Eq a => a -> a -> Bool
== Maybe CVal
b
  CEither   Either CVal CVal
a == CEither   Either CVal CVal
b = Either CVal CVal
a forall a. Eq a => a -> a -> Bool
== Either CVal CVal
b
  CVal
a           == CVal
b           = if CVal -> Int
cvRank CVal
a forall a. Eq a => a -> a -> Bool
== CVal -> Int
cvRank CVal
b
                                  then forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                                       , String
"*** Data.SBV.Eq.CVal: Impossible happened: same rank in comparison fallthru"
                                                       , String
"***"
                                                       , String
"***   Received: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (CVal -> Int
cvRank CVal
a, CVal -> Int
cvRank CVal
b)
                                                       , String
"***"
                                                       , String
"*** Please report this as a bug!"
                                                       ]
                                  else Bool
False

-- | Ord instance for VWVal. Same comments as the 'Eq' instance why this cannot be derived.
instance Ord CVal where
  CAlgReal  AlgReal
a compare :: CVal -> CVal -> Ordering
`compare` CAlgReal  AlgReal
b = AlgReal
a AlgReal -> AlgReal -> Ordering
`algRealStructuralCompare` AlgReal
b
  CInteger  Integer
a `compare` CInteger  Integer
b = Integer
a forall a. Ord a => a -> a -> Ordering
`compare`                  Integer
b
  CFloat    Float
a `compare` CFloat    Float
b = Float
a forall a. RealFloat a => a -> a -> Ordering
`fpCompareObjectH`         Float
b
  CDouble   Double
a `compare` CDouble   Double
b = Double
a forall a. RealFloat a => a -> a -> Ordering
`fpCompareObjectH`         Double
b
  CRational Rational
a `compare` CRational Rational
b = Rational
a forall a. Ord a => a -> a -> Ordering
`compare`                  Rational
b
  CFP       FP
a `compare` CFP       FP
b = FP
a FP -> FP -> Ordering
`fprCompareObject`         FP
b
  CChar     Char
a `compare` CChar     Char
b = Char
a forall a. Ord a => a -> a -> Ordering
`compare`                  Char
b
  CString   String
a `compare` CString   String
b = String
a forall a. Ord a => a -> a -> Ordering
`compare`                  String
b
  CList     [CVal]
a `compare` CList     [CVal]
b = [CVal]
a forall a. Ord a => a -> a -> Ordering
`compare`                  [CVal]
b
  CSet      RCSet CVal
a `compare` CSet      RCSet CVal
b = RCSet CVal
a forall a. Ord a => RCSet a -> RCSet a -> Ordering
`compareRCSet`             RCSet CVal
b
  CUserSort (Maybe Int, String)
a `compare` CUserSort (Maybe Int, String)
b = (Maybe Int, String)
a forall a. Ord a => a -> a -> Ordering
`compare`                  (Maybe Int, String)
b
  CTuple    [CVal]
a `compare` CTuple    [CVal]
b = [CVal]
a forall a. Ord a => a -> a -> Ordering
`compare`                  [CVal]
b
  CMaybe    Maybe CVal
a `compare` CMaybe    Maybe CVal
b = Maybe CVal
a forall a. Ord a => a -> a -> Ordering
`compare`                  Maybe CVal
b
  CEither   Either CVal CVal
a `compare` CEither   Either CVal CVal
b = Either CVal CVal
a forall a. Ord a => a -> a -> Ordering
`compare`                  Either CVal CVal
b
  CVal
a           `compare` CVal
b           = let ra :: Int
ra = CVal -> Int
cvRank CVal
a
                                          rb :: Int
rb = CVal -> Int
cvRank CVal
b
                                      in if Int
ra forall a. Eq a => a -> a -> Bool
== Int
rb
                                            then forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                                                 , String
"*** Data.SBV.Ord.CVal: Impossible happened: same rank in comparison fallthru"
                                                                 , String
"***"
                                                                 , String
"***   Received: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Int
ra, Int
rb)
                                                                 , String
"***"
                                                                 , String
"*** Please report this as a bug!"
                                                                 ]
                                            else CVal -> Int
cvRank CVal
a forall a. Ord a => a -> a -> Ordering
`compare` CVal -> Int
cvRank CVal
b

-- | 'CV' represents a concrete word of a fixed size:
-- For signed words, the most significant digit is considered to be the sign.
data CV = CV { CV -> Kind
_cvKind  :: !Kind
             , CV -> CVal
cvVal    :: !CVal
             }
        deriving (CV -> CV -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CV -> CV -> Bool
$c/= :: CV -> CV -> Bool
== :: CV -> CV -> Bool
$c== :: CV -> CV -> Bool
Eq, Eq CV
CV -> CV -> Bool
CV -> CV -> Ordering
CV -> CV -> CV
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: CV -> CV -> CV
$cmin :: CV -> CV -> CV
max :: CV -> CV -> CV
$cmax :: CV -> CV -> CV
>= :: CV -> CV -> Bool
$c>= :: CV -> CV -> Bool
> :: CV -> CV -> Bool
$c> :: CV -> CV -> Bool
<= :: CV -> CV -> Bool
$c<= :: CV -> CV -> Bool
< :: CV -> CV -> Bool
$c< :: CV -> CV -> Bool
compare :: CV -> CV -> Ordering
$ccompare :: CV -> CV -> Ordering
Ord)

-- | A generalized CV allows for expressions involving infinite and epsilon values/intervals Used in optimization problems.
data GeneralizedCV = ExtendedCV ExtCV
                   | RegularCV  CV

-- | A simple expression type over extended values, covering infinity, epsilon and intervals.
data ExtCV = Infinite  Kind         -- infinity
           | Epsilon   Kind         -- epsilon
           | Interval  ExtCV ExtCV  -- closed interval
           | BoundedCV CV           -- a bounded value (i.e., neither infinity, nor epsilon). Note that this cannot appear at top, but can appear as a sub-expr.
           | AddExtCV  ExtCV ExtCV  -- addition
           | MulExtCV  ExtCV ExtCV  -- multiplication

-- | Kind instance for Extended CV
instance HasKind ExtCV where
  kindOf :: ExtCV -> Kind
kindOf (Infinite  Kind
k)   = Kind
k
  kindOf (Epsilon   Kind
k)   = Kind
k
  kindOf (Interval  ExtCV
l ExtCV
_) = forall a. HasKind a => a -> Kind
kindOf ExtCV
l
  kindOf (BoundedCV  CV
c)  = forall a. HasKind a => a -> Kind
kindOf CV
c
  kindOf (AddExtCV  ExtCV
l ExtCV
_) = forall a. HasKind a => a -> Kind
kindOf ExtCV
l
  kindOf (MulExtCV  ExtCV
l ExtCV
_) = forall a. HasKind a => a -> Kind
kindOf ExtCV
l

-- | Show instance, shows with the kind
instance Show ExtCV where
  show :: ExtCV -> String
show = Bool -> ExtCV -> String
showExtCV Bool
True

-- | Show an extended CV, with kind if required
showExtCV :: Bool -> ExtCV -> String
showExtCV :: Bool -> ExtCV -> String
showExtCV = Bool -> Bool -> ExtCV -> String
go Bool
False
  where go :: Bool -> Bool -> ExtCV -> String
go Bool
parens Bool
shk ExtCV
extCV = case ExtCV
extCV of
                                Infinite{}    -> Bool -> ShowS
withKind Bool
False String
"oo"
                                Epsilon{}     -> Bool -> ShowS
withKind Bool
False String
"epsilon"
                                Interval  ExtCV
l ExtCV
u -> Bool -> ShowS
withKind Bool
True  forall a b. (a -> b) -> a -> b
$ Char
'['  forall a. a -> [a] -> [a]
: Bool -> ExtCV -> String
showExtCV Bool
False ExtCV
l forall a. [a] -> [a] -> [a]
++ String
" .. " forall a. [a] -> [a] -> [a]
++ Bool -> ExtCV -> String
showExtCV Bool
False ExtCV
u forall a. [a] -> [a] -> [a]
++ String
"]"
                                BoundedCV CV
c   -> Bool -> CV -> String
showCV Bool
shk CV
c
                                AddExtCV ExtCV
l ExtCV
r  -> ShowS
par forall a b. (a -> b) -> a -> b
$ Bool -> ShowS
withKind Bool
False forall a b. (a -> b) -> a -> b
$ String -> ShowS
add (Bool -> Bool -> ExtCV -> String
go Bool
True Bool
False ExtCV
l) (Bool -> Bool -> ExtCV -> String
go Bool
True Bool
False ExtCV
r)

                                -- a few niceties here to grok -oo and -epsilon
                                MulExtCV (BoundedCV (CV Kind
KUnbounded (CInteger (-1)))) Infinite{} -> Bool -> ShowS
withKind Bool
False String
"-oo"
                                MulExtCV (BoundedCV (CV Kind
KReal      (CAlgReal (-1)))) Infinite{} -> Bool -> ShowS
withKind Bool
False String
"-oo"
                                MulExtCV (BoundedCV (CV Kind
KUnbounded (CInteger (-1)))) Epsilon{}  -> Bool -> ShowS
withKind Bool
False String
"-epsilon"
                                MulExtCV (BoundedCV (CV Kind
KReal      (CAlgReal (-1)))) Epsilon{}  -> Bool -> ShowS
withKind Bool
False String
"-epsilon"

                                MulExtCV ExtCV
l ExtCV
r  -> ShowS
par forall a b. (a -> b) -> a -> b
$ Bool -> ShowS
withKind Bool
False forall a b. (a -> b) -> a -> b
$ String -> ShowS
mul (Bool -> Bool -> ExtCV -> String
go Bool
True Bool
False ExtCV
l) (Bool -> Bool -> ExtCV -> String
go Bool
True Bool
False ExtCV
r)
           where par :: ShowS
par String
v | Bool
parens = Char
'(' forall a. a -> [a] -> [a]
: String
v forall a. [a] -> [a] -> [a]
++ String
")"
                       | Bool
True   = String
v
                 withKind :: Bool -> ShowS
withKind Bool
isInterval String
v | Bool -> Bool
not Bool
shk    = String
v
                                       | Bool
isInterval = String
v forall a. [a] -> [a] -> [a]
++ String
" :: [" forall a. [a] -> [a] -> [a]
++ Kind -> String
showBaseKind (forall a. HasKind a => a -> Kind
kindOf ExtCV
extCV) forall a. [a] -> [a] -> [a]
++ String
"]"
                                       | Bool
True       = String
v forall a. [a] -> [a] -> [a]
++ String
" :: "  forall a. [a] -> [a] -> [a]
++ Kind -> String
showBaseKind (forall a. HasKind a => a -> Kind
kindOf ExtCV
extCV)

                 add :: String -> String -> String
                 add :: String -> ShowS
add String
n String
v
                  | String
"-" forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
v = String
n forall a. [a] -> [a] -> [a]
++ String
" - " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [a]
tail String
v
                  | Bool
True               = String
n forall a. [a] -> [a] -> [a]
++ String
" + " forall a. [a] -> [a] -> [a]
++ String
v

                 mul :: String -> String -> String
                 mul :: String -> ShowS
mul String
n String
v = String
n forall a. [a] -> [a] -> [a]
++ String
" * " forall a. [a] -> [a] -> [a]
++ String
v

-- | Is this a regular CV?
isRegularCV :: GeneralizedCV -> Bool
isRegularCV :: GeneralizedCV -> Bool
isRegularCV RegularCV{}  = Bool
True
isRegularCV ExtendedCV{} = Bool
False

-- | 'Kind' instance for CV
instance HasKind CV where
  kindOf :: CV -> Kind
kindOf (CV Kind
k CVal
_) = Kind
k

-- | 'Kind' instance for generalized CV
instance HasKind GeneralizedCV where
  kindOf :: GeneralizedCV -> Kind
kindOf (ExtendedCV ExtCV
e) = forall a. HasKind a => a -> Kind
kindOf ExtCV
e
  kindOf (RegularCV  CV
c) = forall a. HasKind a => a -> Kind
kindOf CV
c

-- | Are two CV's of the same type?
cvSameType :: CV -> CV -> Bool
cvSameType :: CV -> CV -> Bool
cvSameType CV
x CV
y = forall a. HasKind a => a -> Kind
kindOf CV
x forall a. Eq a => a -> a -> Bool
== forall a. HasKind a => a -> Kind
kindOf CV
y

-- | Convert a CV to a Haskell boolean (NB. Assumes input is well-kinded)
cvToBool :: CV -> Bool
cvToBool :: CV -> Bool
cvToBool CV
x = CV -> CVal
cvVal CV
x forall a. Eq a => a -> a -> Bool
/= Integer -> CVal
CInteger Integer
0

-- | Normalize a CV. Essentially performs modular arithmetic to make sure the
-- value can fit in the given bit-size. Note that this is rather tricky for
-- negative values, due to asymmetry. (i.e., an 8-bit negative number represents
-- values in the range -128 to 127; thus we have to be careful on the negative side.)
normCV :: CV -> CV
normCV :: CV -> CV
normCV c :: CV
c@(CV (KBounded Bool
signed Int
sz) (CInteger Integer
v)) = CV
c { cvVal :: CVal
cvVal = Integer -> CVal
CInteger Integer
norm }
 where norm :: Integer
norm | Int
sz forall a. Eq a => a -> a -> Bool
== Int
0 = Integer
0

            | Bool
signed  = let rg :: Integer
rg = Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
sz forall a. Num a => a -> a -> a
- Int
1)
                        in case forall a. Integral a => a -> a -> (a, a)
divMod Integer
v Integer
rg of
                                  (Integer
a, Integer
b) | forall a. Integral a => a -> Bool
even Integer
a -> Integer
b
                                  (Integer
_, Integer
b)          -> Integer
b forall a. Num a => a -> a -> a
- Integer
rg

            | Bool
True    = {- We really want to do:

                                v `mod` (2 ^ sz)

                           Below is equivalent, and hopefully faster!
                        -}
                        Integer
v forall a. Bits a => a -> a -> a
.&. (((Integer
1 :: Integer) forall a. Bits a => a -> Int -> a
`shiftL` Int
sz) forall a. Num a => a -> a -> a
- Integer
1)
normCV c :: CV
c@(CV Kind
KBool (CInteger Integer
v)) = CV
c { cvVal :: CVal
cvVal = Integer -> CVal
CInteger (Integer
v forall a. Bits a => a -> a -> a
.&. Integer
1) }
normCV CV
c                         = CV
c
{-# INLINE normCV #-}

-- | Constant False as a 'CV'. We represent it using the integer value 0.
falseCV :: CV
falseCV :: CV
falseCV = Kind -> CVal -> CV
CV Kind
KBool (Integer -> CVal
CInteger Integer
0)

-- | Constant True as a 'CV'. We represent it using the integer value 1.
trueCV :: CV
trueCV :: CV
trueCV  = Kind -> CVal -> CV
CV Kind
KBool (Integer -> CVal
CInteger Integer
1)

-- | Lift a unary function through a 'CV'.
liftCV :: (AlgReal             -> b)
       -> (Integer             -> b)
       -> (Float               -> b)
       -> (Double              -> b)
       -> (FP                  -> b)
       -> (Rational            -> b)
       -> (Char                -> b)
       -> (String              -> b)
       -> ((Maybe Int, String) -> b)
       -> ([CVal]              -> b)
       -> (RCSet CVal          -> b)
       -> ([CVal]              -> b)
       -> (Maybe CVal          -> b)
       -> (Either CVal CVal    -> b)
       -> CV
       -> b
liftCV :: forall b.
(AlgReal -> b)
-> (Integer -> b)
-> (Float -> b)
-> (Double -> b)
-> (FP -> b)
-> (Rational -> b)
-> (Char -> b)
-> (String -> b)
-> ((Maybe Int, String) -> b)
-> ([CVal] -> b)
-> (RCSet CVal -> b)
-> ([CVal] -> b)
-> (Maybe CVal -> b)
-> (Either CVal CVal -> b)
-> CV
-> b
liftCV AlgReal -> b
f Integer -> b
_ Float -> b
_ Double -> b
_ FP -> b
_ Rational -> b
_ Char -> b
_ String -> b
_ (Maybe Int, String) -> b
_ [CVal] -> b
_ RCSet CVal -> b
_ [CVal] -> b
_ Maybe CVal -> b
_ Either CVal CVal -> b
_ (CV Kind
_ (CAlgReal  AlgReal
v)) = AlgReal -> b
f AlgReal
v
liftCV AlgReal -> b
_ Integer -> b
f Float -> b
_ Double -> b
_ FP -> b
_ Rational -> b
_ Char -> b
_ String -> b
_ (Maybe Int, String) -> b
_ [CVal] -> b
_ RCSet CVal -> b
_ [CVal] -> b
_ Maybe CVal -> b
_ Either CVal CVal -> b
_ (CV Kind
_ (CInteger  Integer
v)) = Integer -> b
f Integer
v
liftCV AlgReal -> b
_ Integer -> b
_ Float -> b
f Double -> b
_ FP -> b
_ Rational -> b
_ Char -> b
_ String -> b
_ (Maybe Int, String) -> b
_ [CVal] -> b
_ RCSet CVal -> b
_ [CVal] -> b
_ Maybe CVal -> b
_ Either CVal CVal -> b
_ (CV Kind
_ (CFloat    Float
v)) = Float -> b
f Float
v
liftCV AlgReal -> b
_ Integer -> b
_ Float -> b
_ Double -> b
f FP -> b
_ Rational -> b
_ Char -> b
_ String -> b
_ (Maybe Int, String) -> b
_ [CVal] -> b
_ RCSet CVal -> b
_ [CVal] -> b
_ Maybe CVal -> b
_ Either CVal CVal -> b
_ (CV Kind
_ (CDouble   Double
v)) = Double -> b
f Double
v
liftCV AlgReal -> b
_ Integer -> b
_ Float -> b
_ Double -> b
_ FP -> b
f Rational -> b
_ Char -> b
_ String -> b
_ (Maybe Int, String) -> b
_ [CVal] -> b
_ RCSet CVal -> b
_ [CVal] -> b
_ Maybe CVal -> b
_ Either CVal CVal -> b
_ (CV Kind
_ (CFP       FP
v)) = FP -> b
f FP
v
liftCV AlgReal -> b
_ Integer -> b
_ Float -> b
_ Double -> b
_ FP -> b
_ Rational -> b
f Char -> b
_ String -> b
_ (Maybe Int, String) -> b
_ [CVal] -> b
_ RCSet CVal -> b
_ [CVal] -> b
_ Maybe CVal -> b
_ Either CVal CVal -> b
_ (CV Kind
_ (CRational Rational
v)) = Rational -> b
f Rational
v
liftCV AlgReal -> b
_ Integer -> b
_ Float -> b
_ Double -> b
_ FP -> b
_ Rational -> b
_ Char -> b
f String -> b
_ (Maybe Int, String) -> b
_ [CVal] -> b
_ RCSet CVal -> b
_ [CVal] -> b
_ Maybe CVal -> b
_ Either CVal CVal -> b
_ (CV Kind
_ (CChar     Char
v)) = Char -> b
f Char
v
liftCV AlgReal -> b
_ Integer -> b
_ Float -> b
_ Double -> b
_ FP -> b
_ Rational -> b
_ Char -> b
_ String -> b
f (Maybe Int, String) -> b
_ [CVal] -> b
_ RCSet CVal -> b
_ [CVal] -> b
_ Maybe CVal -> b
_ Either CVal CVal -> b
_ (CV Kind
_ (CString   String
v)) = String -> b
f String
v
liftCV AlgReal -> b
_ Integer -> b
_ Float -> b
_ Double -> b
_ FP -> b
_ Rational -> b
_ Char -> b
_ String -> b
_ (Maybe Int, String) -> b
f [CVal] -> b
_ RCSet CVal -> b
_ [CVal] -> b
_ Maybe CVal -> b
_ Either CVal CVal -> b
_ (CV Kind
_ (CUserSort (Maybe Int, String)
v)) = (Maybe Int, String) -> b
f (Maybe Int, String)
v
liftCV AlgReal -> b
_ Integer -> b
_ Float -> b
_ Double -> b
_ FP -> b
_ Rational -> b
_ Char -> b
_ String -> b
_ (Maybe Int, String) -> b
_ [CVal] -> b
f RCSet CVal -> b
_ [CVal] -> b
_ Maybe CVal -> b
_ Either CVal CVal -> b
_ (CV Kind
_ (CList     [CVal]
v)) = [CVal] -> b
f [CVal]
v
liftCV AlgReal -> b
_ Integer -> b
_ Float -> b
_ Double -> b
_ FP -> b
_ Rational -> b
_ Char -> b
_ String -> b
_ (Maybe Int, String) -> b
_ [CVal] -> b
_ RCSet CVal -> b
f [CVal] -> b
_ Maybe CVal -> b
_ Either CVal CVal -> b
_ (CV Kind
_ (CSet      RCSet CVal
v)) = RCSet CVal -> b
f RCSet CVal
v
liftCV AlgReal -> b
_ Integer -> b
_ Float -> b
_ Double -> b
_ FP -> b
_ Rational -> b
_ Char -> b
_ String -> b
_ (Maybe Int, String) -> b
_ [CVal] -> b
_ RCSet CVal -> b
_ [CVal] -> b
f Maybe CVal -> b
_ Either CVal CVal -> b
_ (CV Kind
_ (CTuple    [CVal]
v)) = [CVal] -> b
f [CVal]
v
liftCV AlgReal -> b
_ Integer -> b
_ Float -> b
_ Double -> b
_ FP -> b
_ Rational -> b
_ Char -> b
_ String -> b
_ (Maybe Int, String) -> b
_ [CVal] -> b
_ RCSet CVal -> b
_ [CVal] -> b
_ Maybe CVal -> b
f Either CVal CVal -> b
_ (CV Kind
_ (CMaybe    Maybe CVal
v)) = Maybe CVal -> b
f Maybe CVal
v
liftCV AlgReal -> b
_ Integer -> b
_ Float -> b
_ Double -> b
_ FP -> b
_ Rational -> b
_ Char -> b
_ String -> b
_ (Maybe Int, String) -> b
_ [CVal] -> b
_ RCSet CVal -> b
_ [CVal] -> b
_ Maybe CVal -> b
_ Either CVal CVal -> b
f (CV Kind
_ (CEither   Either CVal CVal
v)) = Either CVal CVal -> b
f Either CVal CVal
v

-- | Lift a binary function through a 'CV'.
liftCV2 :: (AlgReal             -> AlgReal             -> b)
        -> (Integer             -> Integer             -> b)
        -> (Float               -> Float               -> b)
        -> (Double              -> Double              -> b)
        -> (FP                  -> FP                  -> b)
        -> (Rational            -> Rational            -> b)
        -> (Char                -> Char                -> b)
        -> (String              -> String              -> b)
        -> ([CVal]              -> [CVal]              -> b)
        -> ([CVal]              -> [CVal]              -> b)
        -> (Maybe CVal          -> Maybe CVal          -> b)
        -> (Either CVal CVal    -> Either CVal CVal    -> b)
        -> ((Maybe Int, String) -> (Maybe Int, String) -> b)
        -> CV                   -> CV                  -> b
liftCV2 :: forall b.
(AlgReal -> AlgReal -> b)
-> (Integer -> Integer -> b)
-> (Float -> Float -> b)
-> (Double -> Double -> b)
-> (FP -> FP -> b)
-> (Rational -> Rational -> b)
-> (Char -> Char -> b)
-> (String -> String -> b)
-> ([CVal] -> [CVal] -> b)
-> ([CVal] -> [CVal] -> b)
-> (Maybe CVal -> Maybe CVal -> b)
-> (Either CVal CVal -> Either CVal CVal -> b)
-> ((Maybe Int, String) -> (Maybe Int, String) -> b)
-> CV
-> CV
-> b
liftCV2 AlgReal -> AlgReal -> b
r Integer -> Integer -> b
i Float -> Float -> b
f Double -> Double -> b
d FP -> FP -> b
af Rational -> Rational -> b
ra Char -> Char -> b
c String -> String -> b
s [CVal] -> [CVal] -> b
u [CVal] -> [CVal] -> b
v Maybe CVal -> Maybe CVal -> b
m Either CVal CVal -> Either CVal CVal -> b
e (Maybe Int, String) -> (Maybe Int, String) -> b
w CV
x CV
y = case (CV -> CVal
cvVal CV
x, CV -> CVal
cvVal CV
y) of
                                           (CAlgReal   AlgReal
a, CAlgReal   AlgReal
b) -> AlgReal -> AlgReal -> b
r  AlgReal
a AlgReal
b
                                           (CInteger   Integer
a, CInteger   Integer
b) -> Integer -> Integer -> b
i  Integer
a Integer
b
                                           (CFloat     Float
a, CFloat     Float
b) -> Float -> Float -> b
f  Float
a Float
b
                                           (CDouble    Double
a, CDouble    Double
b) -> Double -> Double -> b
d  Double
a Double
b
                                           (CFP        FP
a, CFP        FP
b) -> FP -> FP -> b
af FP
a FP
b
                                           (CRational  Rational
a, CRational  Rational
b) -> Rational -> Rational -> b
ra Rational
a Rational
b
                                           (CChar      Char
a, CChar      Char
b) -> Char -> Char -> b
c  Char
a Char
b
                                           (CString    String
a, CString    String
b) -> String -> String -> b
s  String
a String
b
                                           (CList      [CVal]
a, CList      [CVal]
b) -> [CVal] -> [CVal] -> b
u  [CVal]
a [CVal]
b
                                           (CTuple     [CVal]
a, CTuple     [CVal]
b) -> [CVal] -> [CVal] -> b
v  [CVal]
a [CVal]
b
                                           (CMaybe     Maybe CVal
a, CMaybe     Maybe CVal
b) -> Maybe CVal -> Maybe CVal -> b
m  Maybe CVal
a Maybe CVal
b
                                           (CEither    Either CVal CVal
a, CEither    Either CVal CVal
b) -> Either CVal CVal -> Either CVal CVal -> b
e  Either CVal CVal
a Either CVal CVal
b
                                           (CUserSort  (Maybe Int, String)
a, CUserSort  (Maybe Int, String)
b) -> (Maybe Int, String) -> (Maybe Int, String) -> b
w  (Maybe Int, String)
a (Maybe Int, String)
b
                                           (CVal, CVal)
_                            -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.liftCV2: impossible, incompatible args received: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (CV
x, CV
y)

-- | Map a unary function through a 'CV'.
mapCV :: (AlgReal             -> AlgReal)
      -> (Integer             -> Integer)
      -> (Float               -> Float)
      -> (Double              -> Double)
      -> (FP                  -> FP)
      -> (Rational            -> Rational)
      -> (Char                -> Char)
      -> (String              -> String)
      -> ((Maybe Int, String) -> (Maybe Int, String))
      -> CV
      -> CV
mapCV :: (AlgReal -> AlgReal)
-> (Integer -> Integer)
-> (Float -> Float)
-> (Double -> Double)
-> (FP -> FP)
-> (Rational -> Rational)
-> (Char -> Char)
-> ShowS
-> ((Maybe Int, String) -> (Maybe Int, String))
-> CV
-> CV
mapCV AlgReal -> AlgReal
r Integer -> Integer
i Float -> Float
f Double -> Double
d FP -> FP
af Rational -> Rational
ra Char -> Char
c ShowS
s (Maybe Int, String) -> (Maybe Int, String)
u CV
x  = CV -> CV
normCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (forall a. HasKind a => a -> Kind
kindOf CV
x) forall a b. (a -> b) -> a -> b
$ case CV -> CVal
cvVal CV
x of
                                                          CAlgReal  AlgReal
a -> AlgReal -> CVal
CAlgReal  (AlgReal -> AlgReal
r  AlgReal
a)
                                                          CInteger  Integer
a -> Integer -> CVal
CInteger  (Integer -> Integer
i  Integer
a)
                                                          CFloat    Float
a -> Float -> CVal
CFloat    (Float -> Float
f  Float
a)
                                                          CDouble   Double
a -> Double -> CVal
CDouble   (Double -> Double
d  Double
a)
                                                          CFP       FP
a -> FP -> CVal
CFP       (FP -> FP
af FP
a)
                                                          CRational Rational
a -> Rational -> CVal
CRational (Rational -> Rational
ra Rational
a)
                                                          CChar     Char
a -> Char -> CVal
CChar     (Char -> Char
c  Char
a)
                                                          CString   String
a -> String -> CVal
CString   (ShowS
s  String
a)
                                                          CUserSort (Maybe Int, String)
a -> (Maybe Int, String) -> CVal
CUserSort ((Maybe Int, String) -> (Maybe Int, String)
u  (Maybe Int, String)
a)
                                                          CList{}     -> forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV: Unexpected call through mapCV with lists!"
                                                          CSet{}      -> forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV: Unexpected call through mapCV with sets!"
                                                          CTuple{}    -> forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV: Unexpected call through mapCV with tuples!"
                                                          CMaybe{}    -> forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV: Unexpected call through mapCV with maybe!"
                                                          CEither{}   -> forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV: Unexpected call through mapCV with either!"

-- | Map a binary function through a 'CV'.
mapCV2 :: (AlgReal             -> AlgReal             -> AlgReal)
       -> (Integer             -> Integer             -> Integer)
       -> (Float               -> Float               -> Float)
       -> (Double              -> Double              -> Double)
       -> (FP                  -> FP                  -> FP)
       -> (Rational            -> Rational            -> Rational)
       -> (Char                -> Char                -> Char)
       -> (String              -> String              -> String)
       -> ((Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String))
       -> CV
       -> CV
       -> CV
mapCV2 :: (AlgReal -> AlgReal -> AlgReal)
-> (Integer -> Integer -> Integer)
-> (Float -> Float -> Float)
-> (Double -> Double -> Double)
-> (FP -> FP -> FP)
-> (Rational -> Rational -> Rational)
-> (Char -> Char -> Char)
-> (String -> ShowS)
-> ((Maybe Int, String)
    -> (Maybe Int, String) -> (Maybe Int, String))
-> CV
-> CV
-> CV
mapCV2 AlgReal -> AlgReal -> AlgReal
r Integer -> Integer -> Integer
i Float -> Float -> Float
f Double -> Double -> Double
d FP -> FP -> FP
af Rational -> Rational -> Rational
ra Char -> Char -> Char
c String -> ShowS
s (Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String)
u CV
x CV
y = case (CV -> CV -> Bool
cvSameType CV
x CV
y, CV -> CVal
cvVal CV
x, CV -> CVal
cvVal CV
y) of
                                  (Bool
True, CAlgReal  AlgReal
a, CAlgReal  AlgReal
b) -> CV -> CV
normCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (forall a. HasKind a => a -> Kind
kindOf CV
x) (AlgReal -> CVal
CAlgReal  (AlgReal -> AlgReal -> AlgReal
r  AlgReal
a AlgReal
b))
                                  (Bool
True, CInteger  Integer
a, CInteger  Integer
b) -> CV -> CV
normCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (forall a. HasKind a => a -> Kind
kindOf CV
x) (Integer -> CVal
CInteger  (Integer -> Integer -> Integer
i  Integer
a Integer
b))
                                  (Bool
True, CFloat    Float
a, CFloat    Float
b) -> CV -> CV
normCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (forall a. HasKind a => a -> Kind
kindOf CV
x) (Float -> CVal
CFloat    (Float -> Float -> Float
f  Float
a Float
b))
                                  (Bool
True, CDouble   Double
a, CDouble   Double
b) -> CV -> CV
normCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (forall a. HasKind a => a -> Kind
kindOf CV
x) (Double -> CVal
CDouble   (Double -> Double -> Double
d  Double
a Double
b))
                                  (Bool
True, CFP       FP
a, CFP       FP
b) -> CV -> CV
normCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (forall a. HasKind a => a -> Kind
kindOf CV
x) (FP -> CVal
CFP       (FP -> FP -> FP
af FP
a FP
b))
                                  (Bool
True, CRational Rational
a, CRational Rational
b) -> CV -> CV
normCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (forall a. HasKind a => a -> Kind
kindOf CV
x) (Rational -> CVal
CRational (Rational -> Rational -> Rational
ra Rational
a Rational
b))
                                  (Bool
True, CChar     Char
a, CChar     Char
b) -> CV -> CV
normCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (forall a. HasKind a => a -> Kind
kindOf CV
x) (Char -> CVal
CChar     (Char -> Char -> Char
c  Char
a Char
b))
                                  (Bool
True, CString   String
a, CString   String
b) -> CV -> CV
normCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (forall a. HasKind a => a -> Kind
kindOf CV
x) (String -> CVal
CString   (String -> ShowS
s  String
a String
b))
                                  (Bool
True, CUserSort (Maybe Int, String)
a, CUserSort (Maybe Int, String)
b) -> CV -> CV
normCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (forall a. HasKind a => a -> Kind
kindOf CV
x) ((Maybe Int, String) -> CVal
CUserSort ((Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String)
u  (Maybe Int, String)
a (Maybe Int, String)
b))
                                  (Bool
True, CList{},     CList{})     -> forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV2: Unexpected call through mapCV2 with lists!"
                                  (Bool
True, CTuple{},    CTuple{})    -> forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV2: Unexpected call through mapCV2 with tuples!"
                                  (Bool
True, CMaybe{},    CMaybe{})    -> forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV2: Unexpected call through mapCV2 with maybes!"
                                  (Bool
True, CEither{},   CEither{})   -> forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV2: Unexpected call through mapCV2 with eithers!"
                                  (Bool, CVal, CVal)
_                                -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.mapCV2: impossible, incompatible args received: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (CV
x, CV
y)

-- | Show instance for 'CV'.
instance Show CV where
  show :: CV -> String
show = Bool -> CV -> String
showCV Bool
True

-- | Show instance for Generalized 'CV'
instance Show GeneralizedCV where
  show :: GeneralizedCV -> String
show (ExtendedCV ExtCV
k) = Bool -> ExtCV -> String
showExtCV Bool
True ExtCV
k
  show (RegularCV  CV
c) = Bool -> CV -> String
showCV    Bool
True CV
c

-- | Show a CV, with kind info if bool is True
showCV :: Bool -> CV -> String
showCV :: Bool -> CV -> String
showCV Bool
shk CV
w | forall a. HasKind a => a -> Bool
isBoolean CV
w = forall a. Show a => a -> String
show (CV -> Bool
cvToBool CV
w) forall a. [a] -> [a] -> [a]
++ (if Bool
shk then String
" :: Bool" else String
"")
showCV Bool
shk CV
w               = forall b.
(AlgReal -> b)
-> (Integer -> b)
-> (Float -> b)
-> (Double -> b)
-> (FP -> b)
-> (Rational -> b)
-> (Char -> b)
-> (String -> b)
-> ((Maybe Int, String) -> b)
-> ([CVal] -> b)
-> (RCSet CVal -> b)
-> ([CVal] -> b)
-> (Maybe CVal -> b)
-> (Either CVal CVal -> b)
-> CV
-> b
liftCV forall a. Show a => a -> String
show forall a. Show a => a -> String
show forall a. Show a => a -> String
show forall a. Show a => a -> String
show forall a. Show a => a -> String
show forall a. Show a => a -> String
show forall a. Show a => a -> String
show forall a. Show a => a -> String
show forall a b. (a, b) -> b
snd [CVal] -> String
shL RCSet CVal -> String
shS [CVal] -> String
shT Maybe CVal -> String
shMaybe Either CVal CVal -> String
shEither CV
w forall a. [a] -> [a] -> [a]
++ String
kInfo
      where kw :: Kind
kw = forall a. HasKind a => a -> Kind
kindOf CV
w

            kInfo :: String
kInfo | Bool
shk  = String
" :: " forall a. [a] -> [a] -> [a]
++ Kind -> String
showBaseKind Kind
kw
                  | Bool
True = String
""

            shL :: [CVal] -> String
shL [CVal]
xs = String
"[" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
"," (forall a b. (a -> b) -> [a] -> [b]
map (Bool -> CV -> String
showCV Bool
False forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
ke) [CVal]
xs) forall a. [a] -> [a] -> [a]
++ String
"]"
              where ke :: Kind
ke = case Kind
kw of
                           KList Kind
k -> Kind
k
                           Kind
_       -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.showCV: Impossible happened, expected list, got: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
kw

            -- we represent complements as @U - set@. This might be confusing, but is utterly cute!
            shS :: RCSet CVal -> String
            shS :: RCSet CVal -> String
shS RCSet CVal
eru = case RCSet CVal
eru of
                        RegularSet    Set CVal
e              -> Set CVal -> String
sh Set CVal
e
                        ComplementSet Set CVal
e | forall a. Set a -> Bool
Set.null Set CVal
e -> String
"U"
                                        | Bool
True       -> String
"U - " forall a. [a] -> [a] -> [a]
++ Set CVal -> String
sh Set CVal
e
              where sh :: Set CVal -> String
sh Set CVal
xs = String
"{" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
"," (forall a b. (a -> b) -> [a] -> [b]
map (Bool -> CV -> String
showCV Bool
False forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
ke) (forall a. Set a -> [a]
Set.toList Set CVal
xs)) forall a. [a] -> [a] -> [a]
++ String
"}"
                    ke :: Kind
ke = case Kind
kw of
                           KSet Kind
k -> Kind
k
                           Kind
_      -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.showCV: Impossible happened, expected set, got: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
kw

            shT :: [CVal] -> String
            shT :: [CVal] -> String
shT [CVal]
xs = String
"(" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
"," [String]
xs' forall a. [a] -> [a] -> [a]
++ String
")"
              where xs' :: [String]
xs' = case Kind
kw of
                            KTuple [Kind]
ks | forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
ks forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [CVal]
xs -> forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Kind
k CVal
x -> Bool -> CV -> String
showCV Bool
False (Kind -> CVal -> CV
CV Kind
k CVal
x)) [Kind]
ks [CVal]
xs
                            Kind
_   -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.showCV: Impossible happened, expected tuple (of length " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [CVal]
xs) forall a. [a] -> [a] -> [a]
++ String
"), got: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
kw

            shMaybe :: Maybe CVal -> String
            shMaybe :: Maybe CVal -> String
shMaybe Maybe CVal
c = case (Maybe CVal
c, Kind
kw) of
                          (Maybe CVal
Nothing, KMaybe{}) -> String
"Nothing"
                          (Just CVal
x,  KMaybe Kind
k) -> String
"Just " forall a. [a] -> [a] -> [a]
++ ShowS
paren (Bool -> CV -> String
showCV Bool
False (Kind -> CVal -> CV
CV Kind
k CVal
x))
                          (Maybe CVal, Kind)
_                   -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.showCV: Impossible happened, expected maybe, got: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
kw

            shEither :: Either CVal CVal -> String
            shEither :: Either CVal CVal -> String
shEither Either CVal CVal
val
              | KEither Kind
k1 Kind
k2 <- Kind
kw = case Either CVal CVal
val of
                                        Left  CVal
x -> String
"Left "  forall a. [a] -> [a] -> [a]
++ ShowS
paren (Bool -> CV -> String
showCV Bool
False (Kind -> CVal -> CV
CV Kind
k1 CVal
x))
                                        Right CVal
y -> String
"Right " forall a. [a] -> [a] -> [a]
++ ShowS
paren (Bool -> CV -> String
showCV Bool
False (Kind -> CVal -> CV
CV Kind
k2 CVal
y))
              | Bool
True                = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.showCV: Impossible happened, expected sum, got: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
kw

            -- kind of crude, but works ok
            paren :: ShowS
paren String
v
              | Bool
needsParen = Char
'(' forall a. a -> [a] -> [a]
: String
v forall a. [a] -> [a] -> [a]
++ String
")"
              | Bool
True       = String
v
              where needsParen :: Bool
needsParen = case forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace String
v of
                                   []         -> Bool
False
                                   rest :: String
rest@(Char
x:String
_) -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Char -> Bool
isSpace String
rest Bool -> Bool -> Bool
&& Char
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` String
"{[("

-- | Create a constant word from an integral.
mkConstCV :: Integral a => Kind -> a -> CV
mkConstCV :: forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
KBool           a
a = CV -> CV
normCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KBool      (Integer -> CVal
CInteger  (forall a. Integral a => a -> Integer
toInteger a
a))
mkConstCV k :: Kind
k@KBounded{}    a
a = CV -> CV
normCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k          (Integer -> CVal
CInteger  (forall a. Integral a => a -> Integer
toInteger a
a))
mkConstCV Kind
KUnbounded      a
a = CV -> CV
normCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KUnbounded (Integer -> CVal
CInteger  (forall a. Integral a => a -> Integer
toInteger a
a))
mkConstCV Kind
KReal           a
a = CV -> CV
normCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KReal      (AlgReal -> CVal
CAlgReal  (forall a. Num a => Integer -> a
fromInteger (forall a. Integral a => a -> Integer
toInteger a
a)))
mkConstCV Kind
KFloat          a
a = CV -> CV
normCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KFloat     (Float -> CVal
CFloat    (forall a. Num a => Integer -> a
fromInteger (forall a. Integral a => a -> Integer
toInteger a
a)))
mkConstCV Kind
KDouble         a
a = CV -> CV
normCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KDouble    (Double -> CVal
CDouble   (forall a. Num a => Integer -> a
fromInteger (forall a. Integral a => a -> Integer
toInteger a
a)))
mkConstCV k :: Kind
k@KFP{}         a
a = CV -> CV
normCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k          (FP -> CVal
CFP       (forall a. Num a => Integer -> a
fromInteger (forall a. Integral a => a -> Integer
toInteger a
a)))
mkConstCV Kind
KRational       a
a = CV -> CV
normCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KRational  (Rational -> CVal
CRational (forall a. Num a => Integer -> a
fromInteger (forall a. Integral a => a -> Integer
toInteger a
a)))
mkConstCV Kind
KChar           a
a = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to mkConstCV (Char) with value: "   forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Integral a => a -> Integer
toInteger a
a)
mkConstCV Kind
KString         a
a = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to mkConstCV (String) with value: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Integral a => a -> Integer
toInteger a
a)
mkConstCV (KUserSort String
s Maybe [String]
_) a
a = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to mkConstCV with user kind: " forall a. [a] -> [a] -> [a]
++ String
s forall a. [a] -> [a] -> [a]
++ String
" with value: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Integral a => a -> Integer
toInteger a
a)
mkConstCV k :: Kind
k@KList{}       a
a = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to mkConstCV (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
k forall a. [a] -> [a] -> [a]
++ String
") with value: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Integral a => a -> Integer
toInteger a
a)
mkConstCV k :: Kind
k@KSet{}        a
a = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to mkConstCV (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
k forall a. [a] -> [a] -> [a]
++ String
") with value: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Integral a => a -> Integer
toInteger a
a)
mkConstCV k :: Kind
k@KTuple{}      a
a = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to mkConstCV (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
k forall a. [a] -> [a] -> [a]
++ String
") with value: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Integral a => a -> Integer
toInteger a
a)
mkConstCV k :: Kind
k@KMaybe{}      a
a = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to mkConstCV (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
k forall a. [a] -> [a] -> [a]
++ String
") with value: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Integral a => a -> Integer
toInteger a
a)
mkConstCV k :: Kind
k@KEither{}     a
a = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to mkConstCV (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
k forall a. [a] -> [a] -> [a]
++ String
") with value: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Integral a => a -> Integer
toInteger a
a)

-- | Generate a random constant value ('CVal') of the correct kind.
randomCVal :: Kind -> IO CVal
randomCVal :: Kind -> IO CVal
randomCVal Kind
k =
  case Kind
k of
    Kind
KBool              -> Integer -> CVal
CInteger  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Integer
0, Integer
1)
    KBounded Bool
s Int
w       -> Integer -> CVal
CInteger  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Bool -> Int -> (Integer, Integer)
bounds Bool
s Int
w)
    Kind
KUnbounded         -> Integer -> CVal
CInteger  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO
    Kind
KReal              -> AlgReal -> CVal
CAlgReal  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO
    Kind
KFloat             -> Float -> CVal
CFloat    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO
    Kind
KDouble            -> Double -> CVal
CDouble   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO
    Kind
KRational          -> Rational -> CVal
CRational forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO

    -- Rather bad, but OK
    KFP Int
eb Int
sb          -> do Integer
sgn <- forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Integer
0 :: Integer, Integer
1)
                             let sign :: Bool
sign = Integer
sgn forall a. Eq a => a -> a -> Bool
== Integer
1
                             Integer
e   <- forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Integer
0 :: Integer, Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^Int
ebforall a. Num a => a -> a -> a
-Integer
1)
                             Integer
s   <- forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Integer
0 :: Integer, Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^Int
sbforall a. Num a => a -> a -> a
-Integer
1)
                             forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ FP -> CVal
CFP forall a b. (a -> b) -> a -> b
$ Bool -> (Integer, Int) -> (Integer, Int) -> FP
fpFromRawRep Bool
sign (Integer
e, Int
eb) (Integer
s, Int
sb)

    -- TODO: KString/KChar currently only go for 0..255; include unicode?
    Kind
KString            -> do Int
l <- forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Int
0, Int
100)
                             String -> CVal
CString forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
l (Int -> Char
chr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Int
0, Int
255))
    Kind
KChar              -> Char -> CVal
CChar forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Char
chr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Int
0, Int
255)
    KUserSort String
s Maybe [String]
_      -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to randomCVal with user kind: " forall a. [a] -> [a] -> [a]
++ String
s
    KList Kind
ek           -> do Int
l <- forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Int
0, Int
100)
                             [CVal] -> CVal
CList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
l (Kind -> IO CVal
randomCVal Kind
ek)
    KSet  Kind
ek           -> do Bool
i <- forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO                           -- regular or complement
                             Int
l <- forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Int
0, Int
100)                 -- some set upto 100 elements
                             Set CVal
vals <- forall a. Ord a => [a] -> Set a
Set.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
l (Kind -> IO CVal
randomCVal Kind
ek)
                             forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ RCSet CVal -> CVal
CSet forall a b. (a -> b) -> a -> b
$ if Bool
i then forall a. Set a -> RCSet a
RegularSet Set CVal
vals else forall a. Set a -> RCSet a
ComplementSet Set CVal
vals
    KTuple [Kind]
ks          -> [CVal] -> CVal
CTuple forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Kind -> IO CVal
randomCVal [Kind]
ks
    KMaybe Kind
ke          -> do Bool
i <- forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO
                             if Bool
i
                                then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Maybe CVal -> CVal
CMaybe forall a. Maybe a
Nothing
                                else Maybe CVal -> CVal
CMaybe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Kind -> IO CVal
randomCVal Kind
ke
    KEither Kind
k1 Kind
k2      -> do Bool
i <- forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO
                             if Bool
i
                                then Either CVal CVal -> CVal
CEither forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Kind -> IO CVal
randomCVal Kind
k1
                                else Either CVal CVal -> CVal
CEither forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Kind -> IO CVal
randomCVal Kind
k2
  where
    bounds :: Bool -> Int -> (Integer, Integer)
    bounds :: Bool -> Int -> (Integer, Integer)
bounds Bool
False Int
w = (Integer
0, Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^Int
w forall a. Num a => a -> a -> a
- Integer
1)
    bounds Bool
True  Int
w = (-Integer
x, Integer
xforall a. Num a => a -> a -> a
-Integer
1) where x :: Integer
x = Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
wforall a. Num a => a -> a -> a
-Int
1)

-- | Generate a random constant value ('CV') of the correct kind.
randomCV :: Kind -> IO CV
randomCV :: Kind -> IO CV
randomCV Kind
k = Kind -> CVal -> CV
CV Kind
k forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Kind -> IO CVal
randomCVal Kind
k

{-# ANN module ("HLint: ignore Redundant if" :: String) #-}