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

{-# 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.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 rcs :: RCSet a
rcs = case RCSet a
rcs of
               ComplementSet s :: Set a
s | Set a -> Bool
forall a. Set a -> Bool
Set.null Set a
s -> "U"
                               | Bool
True       -> "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    s :: 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 xs :: [a]
xs = '{' Char -> ShowS
forall a. a -> [a] -> [a]
: String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "," ((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]
++ "}"

-- | 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    a :: Set a
a) (RegularSet    b :: Set a
b) = Set a
a Set a -> Set a -> Bool
forall a. Eq a => a -> a -> Bool
== Set a
b
eqRCSet (ComplementSet a :: Set a
a) (ComplementSet b :: Set a
b) = Set a
a Set a -> Set a -> Bool
forall a. Eq a => a -> a -> Bool
== Set a
b
eqRCSet _                 _                 = 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    a :: Set a
a) (RegularSet    b :: Set a
b) = Set a
a Set a -> Set a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Set a
b
compareRCSet (RegularSet    _) (ComplementSet _) = Ordering
LT
compareRCSet (ComplementSet _) (RegularSet    _) = Ordering
GT
compareRCSet (ComplementSet a :: Set a
a) (ComplementSet b :: 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 _ = 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
          | 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

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

-- | 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  a :: AlgReal
a == :: CVal -> CVal -> Bool
== CAlgReal  b :: AlgReal
b = AlgReal
a AlgReal -> AlgReal -> Bool
`algRealStructuralEqual` AlgReal
b
  CInteger  a :: Integer
a == CInteger  b :: Integer
b = Integer
a Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
b
  CFloat    a :: Float
a == CFloat    b :: 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   a :: Double
a == CDouble   b :: Double
b = Double
a Double -> Double -> Bool
forall a. RealFloat a => a -> a -> Bool
`fpIsEqualObjectH` Double
b   -- ditto
  CChar     a :: Char
a == CChar     b :: Char
b = Char
a Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
b
  CString   a :: String
a == CString   b :: String
b = String
a String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
b
  CList     a :: [CVal]
a == CList     b :: [CVal]
b = [CVal]
a [CVal] -> [CVal] -> Bool
forall a. Eq a => a -> a -> Bool
== [CVal]
b
  CSet      a :: RCSet CVal
a == CSet      b :: 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 a :: (Maybe Int, String)
a == CUserSort b :: (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    a :: [CVal]
a == CTuple    b :: [CVal]
b = [CVal]
a [CVal] -> [CVal] -> Bool
forall a. Eq a => a -> a -> Bool
== [CVal]
b
  CMaybe    a :: Maybe CVal
a == CMaybe    b :: Maybe CVal
b = Maybe CVal
a Maybe CVal -> Maybe CVal -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe CVal
b
  CEither   a :: Either CVal CVal
a == CEither   b :: 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
  a :: CVal
a           == b :: 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 [ ""
                                                       , "*** Data.SBV.Eq.CVal: Impossible happened: same rank in comparison fallthru"
                                                       , "***"
                                                       , "***   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)
                                                       , "***"
                                                       , "*** 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  a :: AlgReal
a compare :: CVal -> CVal -> Ordering
`compare` CAlgReal b :: AlgReal
b  = AlgReal
a        AlgReal -> AlgReal -> Ordering
`algRealStructuralCompare` AlgReal
b
  CInteger  a :: Integer
a `compare` CInteger b :: Integer
b  = Integer
a        Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare`                  Integer
b
  CFloat    a :: Float
a `compare` CFloat b :: Float
b    = Float
a        Float -> Float -> Ordering
forall a. RealFloat a => a -> a -> Ordering
`fpCompareObjectH`         Float
b
  CDouble   a :: Double
a `compare` CDouble b :: Double
b   = Double
a        Double -> Double -> Ordering
forall a. RealFloat a => a -> a -> Ordering
`fpCompareObjectH`         Double
b
  CChar     a :: Char
a `compare` CChar b :: Char
b     = Char
a        Char -> Char -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare`                  Char
b
  CString   a :: String
a `compare` CString b :: String
b   = String
a        String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare`                  String
b
  CList     a :: [CVal]
a `compare` CList   b :: [CVal]
b   = [CVal]
a        [CVal] -> [CVal] -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare`                  [CVal]
b
  CSet      a :: RCSet CVal
a `compare` CSet    b :: 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 a :: (Maybe Int, String)
a `compare` CUserSort b :: (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    a :: [CVal]
a `compare` CTuple    b :: [CVal]
b = [CVal]
a        [CVal] -> [CVal] -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare`                  [CVal]
b
  CMaybe    a :: Maybe CVal
a `compare` CMaybe    b :: Maybe CVal
b = Maybe CVal
a        Maybe CVal -> Maybe CVal -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare`                  Maybe CVal
b
  CEither   a :: Either CVal CVal
a `compare` CEither   b :: 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
  a :: CVal
a           `compare` b :: 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 [ ""
                                                                 , "*** Data.SBV.Ord.CVal: Impossible happened: same rank in comparison fallthru"
                                                                 , "***"
                                                                 , "***   Received: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall a. Show a => a -> String
show (Int
ra, Int
rb)
                                                                 , "***"
                                                                 , "*** 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 extendent 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  k :: Kind
k)   = Kind
k
  kindOf (Epsilon   k :: Kind
k)   = Kind
k
  kindOf (Interval  l :: ExtCV
l _) = ExtCV -> Kind
forall a. HasKind a => a -> Kind
kindOf ExtCV
l
  kindOf (BoundedCV  c :: CV
c)  = CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
c
  kindOf (AddExtCV  l :: ExtCV
l _) = ExtCV -> Kind
forall a. HasKind a => a -> Kind
kindOf ExtCV
l
  kindOf (MulExtCV  l :: ExtCV
l _) = 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 parens :: Bool
parens shk :: Bool
shk extCV :: ExtCV
extCV = case ExtCV
extCV of
                                Infinite{}    -> Bool -> ShowS
withKind Bool
False "oo"
                                Epsilon{}     -> Bool -> ShowS
withKind Bool
False "epsilon"
                                Interval  l :: ExtCV
l u :: ExtCV
u -> Bool -> ShowS
withKind Bool
True  ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ '['  Char -> ShowS
forall a. a -> [a] -> [a]
: Bool -> ExtCV -> String
showExtCV Bool
False ExtCV
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ " .. " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> ExtCV -> String
showExtCV Bool
False ExtCV
u String -> ShowS
forall a. [a] -> [a] -> [a]
++ "]"
                                BoundedCV c :: CV
c   -> Bool -> CV -> String
showCV Bool
shk CV
c
                                AddExtCV l :: ExtCV
l r :: 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 KUnbounded (CInteger (-1)))) Infinite{} -> Bool -> ShowS
withKind Bool
False "-oo"
                                MulExtCV (BoundedCV (CV KReal      (CAlgReal (-1)))) Infinite{} -> Bool -> ShowS
withKind Bool
False "-oo"
                                MulExtCV (BoundedCV (CV KUnbounded (CInteger (-1)))) Epsilon{}  -> Bool -> ShowS
withKind Bool
False "-epsilon"
                                MulExtCV (BoundedCV (CV KReal      (CAlgReal (-1)))) Epsilon{}  -> Bool -> ShowS
withKind Bool
False "-epsilon"

                                MulExtCV l :: ExtCV
l r :: 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 v :: String
v | Bool
parens = '(' Char -> ShowS
forall a. a -> [a] -> [a]
: String
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
                       | Bool
True   = String
v
                 withKind :: Bool -> ShowS
withKind isInterval :: Bool
isInterval v :: String
v | Bool -> Bool
not Bool
shk    = String
v
                                       | Bool
isInterval = String
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ " :: [" 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]
++ "]"
                                       | Bool
True       = String
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ " :: "  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 n :: String
n v :: String
v
                  | "-" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
v = String
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ " - " 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 -> ShowS
forall a. [a] -> [a] -> [a]
++ String
v

                 mul :: String -> String -> String
                 mul :: String -> ShowS
mul n :: String
n v :: String
v = String
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ " * " 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 k :: Kind
k _) = Kind
k

-- | 'Kind' instance for generalized CV
instance HasKind GeneralizedCV where
  kindOf :: GeneralizedCV -> Kind
kindOf (ExtendedCV e :: ExtCV
e) = ExtCV -> Kind
forall a. HasKind a => a -> Kind
kindOf ExtCV
e
  kindOf (RegularCV  c :: 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 x :: CV
x y :: 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 x :: CV
x = CV -> CVal
cvVal CV
x CVal -> CVal -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer -> CVal
CInteger 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 signed :: Bool
signed sz :: Int
sz) (CInteger v :: 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
== 0 = 0
            | Bool
signed  = let rg :: Integer
rg = 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
- 1)
                        in case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod Integer
v Integer
rg of
                                  (a :: Integer
a, b :: Integer
b) | Integer -> Bool
forall a. Integral a => a -> Bool
even Integer
a -> Integer
b
                                  (_, b :: Integer
b)          -> Integer
b Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
rg
            | Bool
True    = Integer
v Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` (2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Int
sz)
normCV c :: CV
c@(CV KBool (CInteger v :: Integer
v)) = CV
c { cvVal :: CVal
cvVal = Integer -> CVal
CInteger (Integer
v Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. 1) }
normCV c :: CV
c                         = CV
c

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

-- | Lift a unary function through a 'CV'.
liftCV :: (AlgReal             -> b)
       -> (Integer             -> b)
       -> (Float               -> b)
       -> (Double              -> 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)
-> (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 f :: AlgReal -> b
f _ _ _ _ _ _ _ _ _ _ _ (CV _ (CAlgReal  v :: AlgReal
v)) = AlgReal -> b
f AlgReal
v
liftCV _ f :: Integer -> b
f _ _ _ _ _ _ _ _ _ _ (CV _ (CInteger  v :: Integer
v)) = Integer -> b
f Integer
v
liftCV _ _ f :: Float -> b
f _ _ _ _ _ _ _ _ _ (CV _ (CFloat    v :: Float
v)) = Float -> b
f Float
v
liftCV _ _ _ f :: Double -> b
f _ _ _ _ _ _ _ _ (CV _ (CDouble   v :: Double
v)) = Double -> b
f Double
v
liftCV _ _ _ _ f :: Char -> b
f _ _ _ _ _ _ _ (CV _ (CChar     v :: Char
v)) = Char -> b
f Char
v
liftCV _ _ _ _ _ f :: String -> b
f _ _ _ _ _ _ (CV _ (CString   v :: String
v)) = String -> b
f String
v
liftCV _ _ _ _ _ _ f :: (Maybe Int, String) -> b
f _ _ _ _ _ (CV _ (CUserSort v :: (Maybe Int, String)
v)) = (Maybe Int, String) -> b
f (Maybe Int, String)
v
liftCV _ _ _ _ _ _ _ f :: [CVal] -> b
f _ _ _ _ (CV _ (CList     v :: [CVal]
v)) = [CVal] -> b
f [CVal]
v
liftCV _ _ _ _ _ _ _ _ f :: RCSet CVal -> b
f _ _ _ (CV _ (CSet      v :: RCSet CVal
v)) = RCSet CVal -> b
f RCSet CVal
v
liftCV _ _ _ _ _ _ _ _ _ f :: [CVal] -> b
f _ _ (CV _ (CTuple    v :: [CVal]
v)) = [CVal] -> b
f [CVal]
v
liftCV _ _ _ _ _ _ _ _ _ _ f :: Maybe CVal -> b
f _ (CV _ (CMaybe    v :: Maybe CVal
v)) = Maybe CVal -> b
f Maybe CVal
v
liftCV _ _ _ _ _ _ _ _ _ _ _ f :: Either CVal CVal -> b
f (CV _ (CEither   v :: 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)
        -> (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)
-> (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 r :: AlgReal -> AlgReal -> b
r i :: Integer -> Integer -> b
i f :: Float -> Float -> b
f d :: Double -> Double -> b
d c :: Char -> Char -> b
c s :: String -> String -> b
s u :: [CVal] -> [CVal] -> b
u v :: [CVal] -> [CVal] -> b
v m :: Maybe CVal -> Maybe CVal -> b
m e :: Either CVal CVal -> Either CVal CVal -> b
e w :: (Maybe Int, String) -> (Maybe Int, String) -> b
w x :: CV
x y :: CV
y = case (CV -> CVal
cvVal CV
x, CV -> CVal
cvVal CV
y) of
                                      (CAlgReal   a :: AlgReal
a, CAlgReal   b :: AlgReal
b) -> AlgReal -> AlgReal -> b
r AlgReal
a AlgReal
b
                                      (CInteger   a :: Integer
a, CInteger   b :: Integer
b) -> Integer -> Integer -> b
i Integer
a Integer
b
                                      (CFloat     a :: Float
a, CFloat     b :: Float
b) -> Float -> Float -> b
f Float
a Float
b
                                      (CDouble    a :: Double
a, CDouble    b :: Double
b) -> Double -> Double -> b
d Double
a Double
b
                                      (CChar      a :: Char
a, CChar      b :: Char
b) -> Char -> Char -> b
c Char
a Char
b
                                      (CString    a :: String
a, CString    b :: String
b) -> String -> String -> b
s String
a String
b
                                      (CList      a :: [CVal]
a, CList      b :: [CVal]
b) -> [CVal] -> [CVal] -> b
u [CVal]
a [CVal]
b
                                      (CTuple     a :: [CVal]
a, CTuple     b :: [CVal]
b) -> [CVal] -> [CVal] -> b
v [CVal]
a [CVal]
b
                                      (CMaybe     a :: Maybe CVal
a, CMaybe     b :: Maybe CVal
b) -> Maybe CVal -> Maybe CVal -> b
m Maybe CVal
a Maybe CVal
b
                                      (CEither    a :: Either CVal CVal
a, CEither    b :: Either CVal CVal
b) -> Either CVal CVal -> Either CVal CVal -> b
e Either CVal CVal
a Either CVal CVal
b
                                      (CUserSort  a :: (Maybe Int, String)
a, CUserSort  b :: (Maybe Int, String)
b) -> (Maybe Int, String) -> (Maybe Int, String) -> b
w (Maybe Int, String)
a (Maybe Int, String)
b
                                      _                            -> String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
forall a b. (a -> b) -> a -> b
$ "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)
      -> (Char                -> Char)
      -> (String              -> String)
      -> ((Maybe Int, String) -> (Maybe Int, String))
      -> CV
      -> CV
mapCV :: (AlgReal -> AlgReal)
-> (Integer -> Integer)
-> (Float -> Float)
-> (Double -> Double)
-> (Char -> Char)
-> ShowS
-> ((Maybe Int, String) -> (Maybe Int, String))
-> CV
-> CV
mapCV r :: AlgReal -> AlgReal
r i :: Integer -> Integer
i f :: Float -> Float
f d :: Double -> Double
d c :: Char -> Char
c s :: ShowS
s u :: (Maybe Int, String) -> (Maybe Int, String)
u x :: 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  a :: AlgReal
a -> AlgReal -> CVal
CAlgReal  (AlgReal -> AlgReal
r AlgReal
a)
                                                    CInteger  a :: Integer
a -> Integer -> CVal
CInteger  (Integer -> Integer
i Integer
a)
                                                    CFloat    a :: Float
a -> Float -> CVal
CFloat    (Float -> Float
f Float
a)
                                                    CDouble   a :: Double
a -> Double -> CVal
CDouble   (Double -> Double
d Double
a)
                                                    CChar     a :: Char
a -> Char -> CVal
CChar     (Char -> Char
c Char
a)
                                                    CString   a :: String
a -> String -> CVal
CString   (ShowS
s String
a)
                                                    CUserSort a :: (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 "Data.SBV.mapCV: Unexpected call through mapCV with lists!"
                                                    CSet{}      -> String -> CVal
forall a. HasCallStack => String -> a
error "Data.SBV.mapCV: Unexpected call through mapCV with sets!"
                                                    CTuple{}    -> String -> CVal
forall a. HasCallStack => String -> a
error "Data.SBV.mapCV: Unexpected call through mapCV with tuples!"
                                                    CMaybe{}    -> String -> CVal
forall a. HasCallStack => String -> a
error "Data.SBV.mapCV: Unexpected call through mapCV with maybe!"
                                                    CEither{}   -> String -> CVal
forall a. HasCallStack => String -> a
error "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)
       -> (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)
-> (Char -> Char -> Char)
-> (String -> ShowS)
-> ((Maybe Int, String)
    -> (Maybe Int, String) -> (Maybe Int, String))
-> CV
-> CV
-> CV
mapCV2 r :: AlgReal -> AlgReal -> AlgReal
r i :: Integer -> Integer -> Integer
i f :: Float -> Float -> Float
f d :: Double -> Double -> Double
d c :: Char -> Char -> Char
c s :: String -> ShowS
s u :: (Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String)
u x :: CV
x y :: CV
y = case (CV -> CV -> Bool
cvSameType CV
x CV
y, CV -> CVal
cvVal CV
x, CV -> CVal
cvVal CV
y) of
                            (True, CAlgReal  a :: AlgReal
a, CAlgReal  b :: 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))
                            (True, CInteger  a :: Integer
a, CInteger  b :: 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))
                            (True, CFloat    a :: Float
a, CFloat    b :: 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))
                            (True, CDouble   a :: Double
a, CDouble   b :: 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))
                            (True, CChar     a :: Char
a, CChar     b :: 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))
                            (True, CString   a :: String
a, CString   b :: 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))
                            (True, CUserSort a :: (Maybe Int, String)
a, CUserSort b :: (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))
                            (True, CList{},     CList{})     -> String -> CV
forall a. HasCallStack => String -> a
error "Data.SBV.mapCV2: Unexpected call through mapCV2 with lists!"
                            (True, CTuple{},    CTuple{})    -> String -> CV
forall a. HasCallStack => String -> a
error "Data.SBV.mapCV2: Unexpected call through mapCV2 with tuples!"
                            (True, CMaybe{},    CMaybe{})    -> String -> CV
forall a. HasCallStack => String -> a
error "Data.SBV.mapCV2: Unexpected call through mapCV2 with maybes!"
                            (True, CEither{},   CEither{})   -> String -> CV
forall a. HasCallStack => String -> a
error "Data.SBV.mapCV2: Unexpected call through mapCV2 with eithers!"
                            _                                -> String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ "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 k :: ExtCV
k) = Bool -> ExtCV -> String
showExtCV Bool
True ExtCV
k
  show (RegularCV  c :: 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 shk :: Bool
shk w :: 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 " :: Bool" else "")
showCV shk :: Bool
shk w :: CV
w               = (AlgReal -> String)
-> (Integer -> String)
-> (Float -> String)
-> (Double -> 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)
-> (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 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 -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
showBaseKind Kind
kw
                  | Bool
True = ""

            shL :: [CVal] -> String
shL xs :: [CVal]
xs = "[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "," ((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]
++ "]"
              where ke :: Kind
ke = case Kind
kw of
                           KList k :: Kind
k -> Kind
k
                           _       -> String -> Kind
forall a. HasCallStack => String -> a
error (String -> Kind) -> String -> Kind
forall a b. (a -> b) -> a -> b
$ "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 eru :: RCSet CVal
eru = case RCSet CVal
eru of
                        RegularSet    e :: Set CVal
e              -> Set CVal -> String
sh Set CVal
e
                        ComplementSet e :: Set CVal
e | Set CVal -> Bool
forall a. Set a -> Bool
Set.null Set CVal
e -> "U"
                                        | Bool
True       -> "U - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set CVal -> String
sh Set CVal
e
              where sh :: Set CVal -> String
sh xs :: Set CVal
xs = "{" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "," ((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]
++ "}"
                    ke :: Kind
ke = case Kind
kw of
                           KSet k :: Kind
k -> Kind
k
                           _      -> String -> Kind
forall a. HasCallStack => String -> a
error (String -> Kind) -> String -> Kind
forall a b. (a -> b) -> a -> b
$ "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 xs :: [CVal]
xs = "(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "," [String]
xs' String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
              where xs' :: [String]
xs' = case Kind
kw of
                            KTuple ks :: [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 (\k :: Kind
k x :: CVal
x -> Bool -> CV -> String
showCV Bool
False (Kind -> CVal -> CV
CV Kind
k CVal
x)) [Kind]
ks [CVal]
xs
                            _   -> String -> [String]
forall a. HasCallStack => String -> a
error (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ "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]
++ "), 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 c :: Maybe CVal
c = case (Maybe CVal
c, Kind
kw) of
                          (Nothing, KMaybe{}) -> "Nothing"
                          (Just x :: CVal
x,  KMaybe k :: Kind
k) -> "Just " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
paren (Bool -> CV -> String
showCV Bool
False (Kind -> CVal -> CV
CV Kind
k CVal
x))
                          _                   -> ShowS
forall a. HasCallStack => String -> a
error ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ "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 val :: Either CVal CVal
val
              | KEither k1 :: Kind
k1 k2 :: Kind
k2 <- Kind
kw = case Either CVal CVal
val of
                                        Left  x :: CVal
x -> "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 y :: CVal
y -> "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
$ "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 v :: String
v
              | Bool
needsParen = '(' Char -> ShowS
forall a. a -> [a] -> [a]
: String
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
              | 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@(x :: Char
x:_) -> (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` "{[("

-- | Create a constant word from an integral.
mkConstCV :: Integral a => Kind -> a -> CV
mkConstCV :: Kind -> a -> CV
mkConstCV KBool                a :: 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
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 KUnbounded           a :: 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 KReal                a :: 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 KFloat               a :: 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 KDouble              a :: 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 KChar                a :: a
a = String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ "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 KString              a :: a
a = String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ "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 (KUninterpreted s :: String
s _) a :: a
a = String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ "Unexpected call to mkConstCV with uninterpreted kind: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ " 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
a = String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ "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]
++ ") 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
a = String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ "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]
++ ") 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
a = String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ "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]
++ ") 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
a = String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ "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]
++ ") 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
a = String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ "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]
++ ") 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 k :: Kind
k =
  case Kind
k of
    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. Random a => (a, a) -> IO a
randomRIO (0, 1)
    KBounded s :: Bool
s w :: 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. Random a => (a, a) -> IO a
randomRIO (Bool -> Int -> (Integer, Integer)
bounds Bool
s Int
w)
    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. Random a => IO a
randomIO
    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. Random a => IO a
randomIO
    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. Random a => IO a
randomIO
    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. Random a => IO a
randomIO
    -- TODO: KString/KChar currently only go for 0..255; include unicode?
    KString            -> do Int
l <- (Int, Int) -> IO Int
forall a. Random a => (a, a) -> IO a
randomRIO (0, 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. Random a => (a, a) -> IO a
randomRIO (0, 255))
    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. Random a => (a, a) -> IO a
randomRIO (0, 255)
    KUninterpreted s :: String
s _ -> String -> IO CVal
forall a. HasCallStack => String -> a
error (String -> IO CVal) -> String -> IO CVal
forall a b. (a -> b) -> a -> b
$ "Unexpected call to randomCVal with uninterpreted kind: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
    KList ek :: Kind
ek           -> do Int
l <- (Int, Int) -> IO Int
forall a. Random a => (a, a) -> IO a
randomRIO (0, 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  ek :: Kind
ek           -> do Bool
i <- IO Bool
forall a. Random a => IO a
randomIO                           -- regular or complement
                             Int
l <- (Int, Int) -> IO Int
forall a. Random a => (a, a) -> IO a
randomRIO (0, 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 ks :: [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 ke :: Kind
ke          -> do Bool
i <- IO Bool
forall a. Random a => IO 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 k1 :: Kind
k1 k2 :: Kind
k2      -> do Bool
i <- IO Bool
forall a. Random a => IO 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 False w :: Int
w = (0, 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
- 1)
    bounds True  w :: Int
w = (-Integer
x, Integer
xInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-1) where x :: Integer
x = 2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-1)

-- | Generate a random constant value ('CV') of the correct kind.
randomCV :: Kind -> IO CV
randomCV :: Kind -> IO CV
randomCV k :: 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) #-}