{-# 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
data RCSet a = RegularSet (Set a)
| ComplementSet (Set a)
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]
++ "}"
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
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))
data CVal = CAlgReal !AlgReal
| CInteger !Integer
| CFloat !Float
| CDouble !Double
| CChar !Char
| CString !String
| CList ![CVal]
| CSet !(RCSet CVal)
| CUserSort !(Maybe Int, String)
| CTuple ![CVal]
| CMaybe !(Maybe CVal)
| CEither !(Either CVal CVal)
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
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
CDouble a :: Double
a == CDouble b :: Double
b = Double
a Double -> Double -> Bool
forall a. RealFloat a => a -> a -> Bool
`fpIsEqualObjectH` Double
b
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
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
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)
data GeneralizedCV = ExtendedCV ExtCV
| RegularCV CV
data ExtCV = Infinite Kind
| Epsilon Kind
| Interval ExtCV ExtCV
| BoundedCV CV
| AddExtCV ExtCV ExtCV
| MulExtCV ExtCV ExtCV
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
instance Show ExtCV where
show :: ExtCV -> String
show = Bool -> ExtCV -> String
showExtCV Bool
True
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)
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
isRegularCV :: GeneralizedCV -> Bool
isRegularCV :: GeneralizedCV -> Bool
isRegularCV RegularCV{} = Bool
True
isRegularCV ExtendedCV{} = Bool
False
instance HasKind CV where
kindOf :: CV -> Kind
kindOf (CV k :: Kind
k _) = Kind
k
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
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
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
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
falseCV :: CV
falseCV :: CV
falseCV = Kind -> CVal -> CV
CV Kind
KBool (Integer -> CVal
CInteger 0)
trueCV :: CV
trueCV :: CV
trueCV = Kind -> CVal -> CV
CV Kind
KBool (Integer -> CVal
CInteger 1)
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
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)
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!"
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)
instance Show CV where
show :: CV -> String
show = Bool -> CV -> String
showCV Bool
True
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
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
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
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` "{[("
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)
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
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
Int
l <- (Int, Int) -> IO Int
forall a. Random a => (a, a) -> IO a
randomRIO (0, 100)
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)
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) #-}