-----------------------------------------------------------------------------
-- |
-- 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 | Set a -> Bool
forall a. Set a -> Bool
Set.null Set a
s -> String
"U"
                               | Bool
True       -> String
"U - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [a] -> String
forall a. Show a => [a] -> String
sh (Set a -> [a]
forall a. Set a -> [a]
Set.toAscList Set a
s)
               RegularSet    Set a
s              ->           [a] -> String
forall a. Show a => [a] -> String
sh (Set a -> [a]
forall a. Set a -> [a]
Set.toAscList Set a
s)
   where sh :: [a] -> String
sh [a]
xs = Char
'{' Char -> ShowS
forall a. a -> [a] -> [a]
: String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map a -> String
forall a. Show a => a -> String
show [a]
xs) String -> ShowS
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 :: RCSet a -> RCSet a -> Bool
eqRCSet (RegularSet    Set a
a) (RegularSet    Set a
b) = Set a
a Set a -> Set a -> Bool
forall a. Eq a => a -> a -> Bool
== Set a
b
eqRCSet (ComplementSet Set a
a) (ComplementSet Set a
b) = Set a
a Set a -> Set a -> Bool
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 :: RCSet a -> RCSet a -> Ordering
compareRCSet (RegularSet    Set a
a) (RegularSet    Set a
b) = Set a
a Set a -> Set a -> Ordering
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 Set a -> Set a -> Ordering
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 (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
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 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
b
  CFloat    Float
a == CFloat    Float
b = Float
a Float -> Float -> Bool
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 Double -> Double -> Bool
forall a. RealFloat a => a -> a -> Bool
`fpIsEqualObjectH` Double
b   -- ditto
  CRational Rational
a == CRational Rational
b = Rational
a Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
b
  CChar     Char
a == CChar     Char
b = Char
a Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
b
  CString   String
a == CString   String
b = String
a String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
b
  CList     [CVal]
a == CList     [CVal]
b = [CVal]
a [CVal] -> [CVal] -> Bool
forall a. Eq a => a -> a -> Bool
== [CVal]
b
  CSet      RCSet CVal
a == CSet      RCSet CVal
b = RCSet CVal
a RCSet CVal -> RCSet CVal -> Bool
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 (Maybe Int, String) -> (Maybe Int, String) -> Bool
forall a. Eq a => a -> a -> Bool
== (Maybe Int, String)
b
  CTuple    [CVal]
a == CTuple    [CVal]
b = [CVal]
a [CVal] -> [CVal] -> Bool
forall a. Eq a => a -> a -> Bool
== [CVal]
b
  CMaybe    Maybe CVal
a == CMaybe    Maybe CVal
b = Maybe CVal
a Maybe CVal -> Maybe CVal -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe CVal
b
  CEither   Either CVal CVal
a == CEither   Either CVal CVal
b = Either CVal CVal
a Either CVal CVal -> Either CVal CVal -> Bool
forall a. Eq a => a -> a -> Bool
== Either CVal CVal
b
  CVal
a           == CVal
b           = if CVal -> Int
cvRank CVal
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== CVal -> Int
cvRank CVal
b
                                  then String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
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: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
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 Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare`                  Integer
b
  CFloat    Float
a `compare` CFloat    Float
b = Float
a Float -> Float -> Ordering
forall a. RealFloat a => a -> a -> Ordering
`fpCompareObjectH`         Float
b
  CDouble   Double
a `compare` CDouble   Double
b = Double
a Double -> Double -> Ordering
forall a. RealFloat a => a -> a -> Ordering
`fpCompareObjectH`         Double
b
  CRational Rational
a `compare` CRational Rational
b = Rational
a Rational -> Rational -> Ordering
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 Char -> Char -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare`                  Char
b
  CString   String
a `compare` CString   String
b = String
a String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare`                  String
b
  CList     [CVal]
a `compare` CList     [CVal]
b = [CVal]
a [CVal] -> [CVal] -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare`                  [CVal]
b
  CSet      RCSet CVal
a `compare` CSet      RCSet CVal
b = RCSet CVal
a RCSet CVal -> RCSet CVal -> Ordering
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 (Maybe Int, String) -> (Maybe Int, String) -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare`                  (Maybe Int, String)
b
  CTuple    [CVal]
a `compare` CTuple    [CVal]
b = [CVal]
a [CVal] -> [CVal] -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare`                  [CVal]
b
  CMaybe    Maybe CVal
a `compare` CMaybe    Maybe CVal
b = Maybe CVal
a Maybe CVal -> Maybe CVal -> Ordering
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 Either CVal CVal -> Either CVal CVal -> Ordering
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
rb
                                            then String -> Ordering
forall a. HasCallStack => String -> a
error (String -> Ordering) -> String -> Ordering
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: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
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 Int -> Int -> Ordering
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
(CV -> CV -> Bool) -> (CV -> CV -> Bool) -> Eq CV
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
Eq CV
-> (CV -> CV -> Ordering)
-> (CV -> CV -> Bool)
-> (CV -> CV -> Bool)
-> (CV -> CV -> Bool)
-> (CV -> CV -> Bool)
-> (CV -> CV -> CV)
-> (CV -> CV -> CV)
-> Ord 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
$cp1Ord :: Eq CV
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
_) = ExtCV -> Kind
forall a. HasKind a => a -> Kind
kindOf ExtCV
l
  kindOf (BoundedCV  CV
c)  = CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
c
  kindOf (AddExtCV  ExtCV
l ExtCV
_) = ExtCV -> Kind
forall a. HasKind a => a -> Kind
kindOf ExtCV
l
  kindOf (MulExtCV  ExtCV
l ExtCV
_) = ExtCV -> Kind
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  ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Char
'['  Char -> ShowS
forall a. a -> [a] -> [a]
: Bool -> ExtCV -> String
showExtCV Bool
False ExtCV
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" .. " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> ExtCV -> String
showExtCV Bool
False ExtCV
u String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"
                                BoundedCV CV
c   -> Bool -> CV -> String
showCV Bool
shk CV
c
                                AddExtCV ExtCV
l ExtCV
r  -> ShowS
par ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Bool -> ShowS
withKind Bool
False ShowS -> ShowS
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 ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Bool -> ShowS
withKind Bool
False ShowS -> ShowS
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
'(' Char -> ShowS
forall a. a -> [a] -> [a]
: String
v String -> ShowS
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 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: [" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
showBaseKind (ExtCV -> Kind
forall a. HasKind a => a -> Kind
kindOf ExtCV
extCV) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"
                                       | Bool
True       = String
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: "  String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
showBaseKind (ExtCV -> Kind
forall a. HasKind a => a -> Kind
kindOf ExtCV
extCV)

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

                 mul :: String -> String -> String
                 mul :: String -> ShowS
mul String
n String
v = String
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" * " String -> ShowS
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) = ExtCV -> Kind
forall a. HasKind a => a -> Kind
kindOf ExtCV
e
  kindOf (RegularCV  CV
c) = CV -> Kind
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 = CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
x Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== CV -> Kind
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 CVal -> CVal -> Bool
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = Integer
0

            | Bool
signed  = let rg :: Integer
rg = Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
sz Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
                        in case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod Integer
v Integer
rg of
                                  (Integer
a, Integer
b) | Integer -> Bool
forall a. Integral a => a -> Bool
even Integer
a -> Integer
b
                                  (Integer
_, Integer
b)          -> Integer
b Integer -> Integer -> Integer
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 Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. (((Integer
1 :: Integer) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
sz) Integer -> Integer -> Integer
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 Integer -> Integer -> Integer
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 :: (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)
        -> (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)
-> (Integer -> Integer -> b)
-> (Float -> Float -> b)
-> (Double -> Double -> b)
-> (FP -> FP -> 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 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
                                         (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)
_                            -> String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
forall a b. (a -> b) -> a -> b
$ String
"SBV.liftCV2: impossible, incompatible args received: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (CV, CV) -> String
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 (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
x) (CVal -> CV) -> CVal -> CV
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{}     -> String -> CVal
forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV: Unexpected call through mapCV with lists!"
                                                          CSet{}      -> String -> CVal
forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV: Unexpected call through mapCV with sets!"
                                                          CTuple{}    -> String -> CVal
forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV: Unexpected call through mapCV with tuples!"
                                                          CMaybe{}    -> String -> CVal
forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV: Unexpected call through mapCV with maybe!"
                                                          CEither{}   -> String -> CVal
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 (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (CV -> Kind
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 (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (CV -> Kind
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 (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (CV -> Kind
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 (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (CV -> Kind
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 (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (CV -> Kind
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 (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (CV -> Kind
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 (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (CV -> Kind
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 (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (CV -> Kind
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 (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (CV -> Kind
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{})     -> String -> CV
forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV2: Unexpected call through mapCV2 with lists!"
                                  (Bool
True, CTuple{},    CTuple{})    -> String -> CV
forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV2: Unexpected call through mapCV2 with tuples!"
                                  (Bool
True, CMaybe{},    CMaybe{})    -> String -> CV
forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV2: Unexpected call through mapCV2 with maybes!"
                                  (Bool
True, CEither{},   CEither{})   -> String -> CV
forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV2: Unexpected call through mapCV2 with eithers!"
                                  (Bool, CVal, CVal)
_                                -> String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.mapCV2: impossible, incompatible args received: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (CV, CV) -> String
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 | CV -> Bool
forall a. HasKind a => a -> Bool
isBoolean CV
w = Bool -> String
forall a. Show a => a -> String
show (CV -> Bool
cvToBool CV
w) String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if Bool
shk then String
" :: Bool" else String
"")
showCV Bool
shk CV
w               = (AlgReal -> String)
-> (Integer -> String)
-> (Float -> String)
-> (Double -> String)
-> (FP -> String)
-> (Rational -> String)
-> (Char -> String)
-> ShowS
-> ((Maybe Int, String) -> String)
-> ([CVal] -> String)
-> (RCSet CVal -> String)
-> ([CVal] -> String)
-> (Maybe CVal -> String)
-> (Either CVal CVal -> String)
-> CV
-> String
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 -> String
forall a. Show a => a -> String
show Integer -> String
forall a. Show a => a -> String
show Float -> String
forall a. Show a => a -> String
show Double -> String
forall a. Show a => a -> String
show FP -> String
forall a. Show a => a -> String
show Rational -> String
forall a. Show a => a -> String
show Char -> String
forall a. Show a => a -> String
show ShowS
forall a. Show a => a -> String
show (Maybe Int, String) -> String
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 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
kInfo
      where kw :: Kind
kw = CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
w

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

            shL :: [CVal] -> String
shL [CVal]
xs = String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((CVal -> String) -> [CVal] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> CV -> String
showCV Bool
False (CV -> String) -> (CVal -> CV) -> CVal -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
ke) [CVal]
xs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"
              where ke :: Kind
ke = case Kind
kw of
                           KList Kind
k -> Kind
k
                           Kind
_       -> String -> Kind
forall a. HasCallStack => String -> a
error (String -> Kind) -> String -> Kind
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.showCV: Impossible happened, expected list, got: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
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 | Set CVal -> Bool
forall a. Set a -> Bool
Set.null Set CVal
e -> String
"U"
                                        | Bool
True       -> String
"U - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set CVal -> String
sh Set CVal
e
              where sh :: Set CVal -> String
sh Set CVal
xs = String
"{" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((CVal -> String) -> [CVal] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> CV -> String
showCV Bool
False (CV -> String) -> (CVal -> CV) -> CVal -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
ke) (Set CVal -> [CVal]
forall a. Set a -> [a]
Set.toList Set CVal
xs)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
                    ke :: Kind
ke = case Kind
kw of
                           KSet Kind
k -> Kind
k
                           Kind
_      -> String -> Kind
forall a. HasCallStack => String -> a
error (String -> Kind) -> String -> Kind
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.showCV: Impossible happened, expected set, got: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
kw

            shT :: [CVal] -> String
            shT :: [CVal] -> String
shT [CVal]
xs = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," [String]
xs' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
              where xs' :: [String]
xs' = case Kind
kw of
                            KTuple [Kind]
ks | [Kind] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
ks Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [CVal] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [CVal]
xs -> (Kind -> CVal -> String) -> [Kind] -> [CVal] -> [String]
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
_   -> String -> [String]
forall a. HasCallStack => String -> a
error (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.showCV: Impossible happened, expected tuple (of length " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([CVal] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [CVal]
xs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"), got: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
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 " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
paren (Bool -> CV -> String
showCV Bool
False (Kind -> CVal -> CV
CV Kind
k CVal
x))
                          (Maybe CVal, Kind)
_                   -> ShowS
forall a. HasCallStack => String -> a
error ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.showCV: Impossible happened, expected maybe, got: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
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 "  String -> ShowS
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 " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
paren (Bool -> CV -> String
showCV Bool
False (Kind -> CVal -> CV
CV Kind
k2 CVal
y))
              | Bool
True                = ShowS
forall a. HasCallStack => String -> a
error ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.showCV: Impossible happened, expected sum, got: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
kw

            -- kind of crude, but works ok
            paren :: ShowS
paren String
v
              | Bool
needsParen = Char
'(' Char -> ShowS
forall a. a -> [a] -> [a]
: String
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
              | Bool
True       = String
v
              where needsParen :: Bool
needsParen = case (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace String
v of
                                   []         -> Bool
False
                                   rest :: String
rest@(Char
x:String
_) -> (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Char -> Bool
isSpace String
rest Bool -> Bool -> Bool
&& Char
x Char -> String -> Bool
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 :: Kind -> a -> CV
mkConstCV Kind
KBool           a
a = CV -> CV
normCV (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KBool      (Integer -> CVal
CInteger  (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a))
mkConstCV k :: Kind
k@KBounded{}    a
a = CV -> CV
normCV (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k          (Integer -> CVal
CInteger  (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a))
mkConstCV Kind
KUnbounded      a
a = CV -> CV
normCV (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KUnbounded (Integer -> CVal
CInteger  (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a))
mkConstCV Kind
KReal           a
a = CV -> CV
normCV (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KReal      (AlgReal -> CVal
CAlgReal  (Integer -> AlgReal
forall a. Num a => Integer -> a
fromInteger (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a)))
mkConstCV Kind
KFloat          a
a = CV -> CV
normCV (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KFloat     (Float -> CVal
CFloat    (Integer -> Float
forall a. Num a => Integer -> a
fromInteger (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a)))
mkConstCV Kind
KDouble         a
a = CV -> CV
normCV (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KDouble    (Double -> CVal
CDouble   (Integer -> Double
forall a. Num a => Integer -> a
fromInteger (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a)))
mkConstCV k :: Kind
k@KFP{}         a
a = CV -> CV
normCV (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k          (FP -> CVal
CFP       (Integer -> FP
forall a. Num a => Integer -> a
fromInteger (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a)))
mkConstCV Kind
KRational       a
a = CV -> CV
normCV (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KRational  (Rational -> CVal
CRational (Integer -> Rational
forall a. Num a => Integer -> a
fromInteger (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a)))
mkConstCV Kind
KChar           a
a = String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to mkConstCV (Char) with value: "   String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a)
mkConstCV Kind
KString         a
a = String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to mkConstCV (String) with value: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a)
mkConstCV (KUserSort String
s Maybe [String]
_) a
a = String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to mkConstCV with user kind: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" with value: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a)
mkConstCV k :: Kind
k@KList{}       a
a = String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to mkConstCV (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") with value: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a)
mkConstCV k :: Kind
k@KSet{}        a
a = String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to mkConstCV (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") with value: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a)
mkConstCV k :: Kind
k@KTuple{}      a
a = String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to mkConstCV (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") with value: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a)
mkConstCV k :: Kind
k@KMaybe{}      a
a = String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to mkConstCV (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") with value: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a)
mkConstCV k :: Kind
k@KEither{}     a
a = String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to mkConstCV (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") with value: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (a -> Integer
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  (Integer -> CVal) -> IO Integer -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> IO Integer
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Integer
0, Integer
1)
    KBounded Bool
s Int
w       -> Integer -> CVal
CInteger  (Integer -> CVal) -> IO Integer -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> IO Integer
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  (Integer -> CVal) -> IO Integer -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO Integer
forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO
    Kind
KReal              -> AlgReal -> CVal
CAlgReal  (AlgReal -> CVal) -> IO AlgReal -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO AlgReal
forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO
    Kind
KFloat             -> Float -> CVal
CFloat    (Float -> CVal) -> IO Float -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO Float
forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO
    Kind
KDouble            -> Double -> CVal
CDouble   (Double -> CVal) -> IO Double -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO Double
forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO
    Kind
KRational          -> Rational -> CVal
CRational (Rational -> CVal) -> IO Rational -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO Rational
forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO

    -- Rather bad, but OK
    KFP Int
eb Int
sb          -> do Integer
sgn <- (Integer, Integer) -> IO Integer
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Integer
0 :: Integer, Integer
1)
                             let sign :: Bool
sign = Integer
sgn Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1
                             Integer
e   <- (Integer, Integer) -> IO Integer
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Integer
0 :: Integer, Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
ebInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)
                             Integer
s   <- (Integer, Integer) -> IO Integer
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Integer
0 :: Integer, Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
sbInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)
                             CVal -> IO CVal
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CVal -> IO CVal) -> CVal -> IO CVal
forall a b. (a -> b) -> a -> b
$ FP -> CVal
CFP (FP -> CVal) -> FP -> CVal
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 <- (Int, Int) -> IO Int
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Int
0, Int
100)
                             String -> CVal
CString (String -> CVal) -> IO String -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> IO Char -> IO String
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
l (Int -> Char
chr (Int -> Char) -> IO Int -> IO Char
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int, Int) -> IO Int
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Int
0, Int
255))
    Kind
KChar              -> Char -> CVal
CChar (Char -> CVal) -> (Int -> Char) -> Int -> CVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Char
chr (Int -> CVal) -> IO Int -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int, Int) -> IO Int
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Int
0, Int
255)
    KUserSort String
s Maybe [String]
_      -> String -> IO CVal
forall a. HasCallStack => String -> a
error (String -> IO CVal) -> String -> IO CVal
forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to randomCVal with user kind: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
    KList Kind
ek           -> do Int
l <- (Int, Int) -> IO Int
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Int
0, Int
100)
                             [CVal] -> CVal
CList ([CVal] -> CVal) -> IO [CVal] -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> IO CVal -> IO [CVal]
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 <- IO Bool
forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO                           -- regular or complement
                             Int
l <- (Int, Int) -> IO Int
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Int
0, Int
100)                 -- some set upto 100 elements
                             Set CVal
vals <- [CVal] -> Set CVal
forall a. Ord a => [a] -> Set a
Set.fromList ([CVal] -> Set CVal) -> IO [CVal] -> IO (Set CVal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> IO CVal -> IO [CVal]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
l (Kind -> IO CVal
randomCVal Kind
ek)
                             CVal -> IO CVal
forall (m :: * -> *) a. Monad m => a -> m a
return (CVal -> IO CVal) -> CVal -> IO CVal
forall a b. (a -> b) -> a -> b
$ RCSet CVal -> CVal
CSet (RCSet CVal -> CVal) -> RCSet CVal -> CVal
forall a b. (a -> b) -> a -> b
$ if Bool
i then Set CVal -> RCSet CVal
forall a. Set a -> RCSet a
RegularSet Set CVal
vals else Set CVal -> RCSet CVal
forall a. Set a -> RCSet a
ComplementSet Set CVal
vals
    KTuple [Kind]
ks          -> [CVal] -> CVal
CTuple ([CVal] -> CVal) -> IO [CVal] -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Kind -> IO CVal) -> [Kind] -> IO [CVal]
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 <- IO Bool
forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO
                             if Bool
i
                                then CVal -> IO CVal
forall (m :: * -> *) a. Monad m => a -> m a
return (CVal -> IO CVal) -> CVal -> IO CVal
forall a b. (a -> b) -> a -> b
$ Maybe CVal -> CVal
CMaybe Maybe CVal
forall a. Maybe a
Nothing
                                else Maybe CVal -> CVal
CMaybe (Maybe CVal -> CVal) -> (CVal -> Maybe CVal) -> CVal -> CVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> CVal) -> IO CVal -> IO CVal
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 <- IO Bool
forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO
                             if Bool
i
                                then Either CVal CVal -> CVal
CEither (Either CVal CVal -> CVal)
-> (CVal -> Either CVal CVal) -> CVal -> CVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CVal -> Either CVal CVal
forall a b. a -> Either a b
Left  (CVal -> CVal) -> IO CVal -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Kind -> IO CVal
randomCVal Kind
k1
                                else Either CVal CVal -> CVal
CEither (Either CVal CVal -> CVal)
-> (CVal -> Either CVal CVal) -> CVal -> CVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CVal -> Either CVal CVal
forall a b. b -> Either a b
Right (CVal -> CVal) -> IO CVal -> IO CVal
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
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
    bounds Bool
True  Int
w = (-Integer
x, Integer
xInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) where x :: Integer
x = Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
wInt -> Int -> Int
forall 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 (CVal -> CV) -> IO CVal -> IO CV
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) #-}