{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
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)
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 rcs = case rcs of
ComplementSet s | Set.null s -> "U"
| True -> "U - " ++ sh (Set.toAscList s)
RegularSet s -> sh (Set.toAscList s)
where sh xs = '{' : intercalate "," (map show xs) ++ "}"
eqRCSet :: Eq a => RCSet a -> RCSet a -> Bool
eqRCSet (RegularSet a) (RegularSet b) = a == b
eqRCSet (ComplementSet a) (ComplementSet b) = a == b
eqRCSet _ _ = False
compareRCSet :: Ord a => RCSet a -> RCSet a -> Ordering
compareRCSet (RegularSet a) (RegularSet b) = a `compare` b
compareRCSet (RegularSet _) (ComplementSet _) = LT
compareRCSet (ComplementSet _) (RegularSet _) = GT
compareRCSet (ComplementSet a) (ComplementSet b) = a `compare` b
instance HasKind a => HasKind (RCSet a) where
kindOf _ = KSet (kindOf (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 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 == CAlgReal b = a `algRealStructuralEqual` b
CInteger a == CInteger b = a == b
CFloat a == CFloat b = a `fpIsEqualObjectH` b
CDouble a == CDouble b = a `fpIsEqualObjectH` b
CChar a == CChar b = a == b
CString a == CString b = a == b
CList a == CList b = a == b
CSet a == CSet b = a `eqRCSet` b
CUserSort a == CUserSort b = a == b
CTuple a == CTuple b = a == b
CMaybe a == CMaybe b = a == b
CEither a == CEither b = a == b
a == b = if cvRank a == cvRank b
then error $ unlines [ ""
, "*** Data.SBV.Eq.CVal: Impossible happened: same rank in comparison fallthru"
, "***"
, "*** Received: " ++ show (cvRank a, cvRank b)
, "***"
, "*** Please report this as a bug!"
]
else False
instance Ord CVal where
CAlgReal a `compare` CAlgReal b = a `algRealStructuralCompare` b
CInteger a `compare` CInteger b = a `compare` b
CFloat a `compare` CFloat b = a `fpCompareObjectH` b
CDouble a `compare` CDouble b = a `fpCompareObjectH` b
CChar a `compare` CChar b = a `compare` b
CString a `compare` CString b = a `compare` b
CList a `compare` CList b = a `compare` b
CSet a `compare` CSet b = a `compareRCSet` b
CUserSort a `compare` CUserSort b = a `compare` b
CTuple a `compare` CTuple b = a `compare` b
CMaybe a `compare` CMaybe b = a `compare` b
CEither a `compare` CEither b = a `compare` b
a `compare` b = let ra = cvRank a
rb = cvRank b
in if ra == rb
then error $ unlines [ ""
, "*** Data.SBV.Ord.CVal: Impossible happened: same rank in comparison fallthru"
, "***"
, "*** Received: " ++ show (ra, rb)
, "***"
, "*** Please report this as a bug!"
]
else cvRank a `compare` cvRank b
data CV = CV { _cvKind :: !Kind
, cvVal :: !CVal
}
deriving (Eq, 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 (Infinite k) = k
kindOf (Epsilon k) = k
kindOf (Interval l _) = kindOf l
kindOf (BoundedCV c) = kindOf c
kindOf (AddExtCV l _) = kindOf l
kindOf (MulExtCV l _) = kindOf l
instance Show ExtCV where
show = showExtCV True
showExtCV :: Bool -> ExtCV -> String
showExtCV = go False
where go parens shk extCV = case extCV of
Infinite{} -> withKind False "oo"
Epsilon{} -> withKind False "epsilon"
Interval l u -> withKind True $ '[' : showExtCV False l ++ " .. " ++ showExtCV False u ++ "]"
BoundedCV c -> showCV shk c
AddExtCV l r -> par $ withKind False $ add (go True False l) (go True False r)
MulExtCV (BoundedCV (CV KUnbounded (CInteger (-1)))) Infinite{} -> withKind False "-oo"
MulExtCV (BoundedCV (CV KReal (CAlgReal (-1)))) Infinite{} -> withKind False "-oo"
MulExtCV (BoundedCV (CV KUnbounded (CInteger (-1)))) Epsilon{} -> withKind False "-epsilon"
MulExtCV (BoundedCV (CV KReal (CAlgReal (-1)))) Epsilon{} -> withKind False "-epsilon"
MulExtCV l r -> par $ withKind False $ mul (go True False l) (go True False r)
where par v | parens = '(' : v ++ ")"
| True = v
withKind isInterval v | not shk = v
| isInterval = v ++ " :: [" ++ showBaseKind (kindOf extCV) ++ "]"
| True = v ++ " :: " ++ showBaseKind (kindOf extCV)
add :: String -> String -> String
add n v
| "-" `isPrefixOf` v = n ++ " - " ++ tail v
| True = n ++ " + " ++ v
mul :: String -> String -> String
mul n v = n ++ " * " ++ v
isRegularCV :: GeneralizedCV -> Bool
isRegularCV RegularCV{} = True
isRegularCV ExtendedCV{} = False
instance HasKind CV where
kindOf (CV k _) = k
instance HasKind GeneralizedCV where
kindOf (ExtendedCV e) = kindOf e
kindOf (RegularCV c) = kindOf c
cvSameType :: CV -> CV -> Bool
cvSameType x y = kindOf x == kindOf y
cvToBool :: CV -> Bool
cvToBool x = cvVal x /= CInteger 0
normCV :: CV -> CV
normCV c@(CV (KBounded signed sz) (CInteger v)) = c { cvVal = CInteger norm }
where norm | sz == 0 = 0
| signed = let rg = 2 ^ (sz - 1)
in case divMod v rg of
(a, b) | even a -> b
(_, b) -> b - rg
| True = v `mod` (2 ^ sz)
normCV c@(CV KBool (CInteger v)) = c { cvVal = CInteger (v .&. 1) }
normCV c = c
falseCV :: CV
falseCV = CV KBool (CInteger 0)
trueCV :: CV
trueCV = CV KBool (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 f _ _ _ _ _ _ _ _ _ _ _ (CV _ (CAlgReal v)) = f v
liftCV _ f _ _ _ _ _ _ _ _ _ _ (CV _ (CInteger v)) = f v
liftCV _ _ f _ _ _ _ _ _ _ _ _ (CV _ (CFloat v)) = f v
liftCV _ _ _ f _ _ _ _ _ _ _ _ (CV _ (CDouble v)) = f v
liftCV _ _ _ _ f _ _ _ _ _ _ _ (CV _ (CChar v)) = f v
liftCV _ _ _ _ _ f _ _ _ _ _ _ (CV _ (CString v)) = f v
liftCV _ _ _ _ _ _ f _ _ _ _ _ (CV _ (CUserSort v)) = f v
liftCV _ _ _ _ _ _ _ f _ _ _ _ (CV _ (CList v)) = f v
liftCV _ _ _ _ _ _ _ _ f _ _ _ (CV _ (CSet v)) = f v
liftCV _ _ _ _ _ _ _ _ _ f _ _ (CV _ (CTuple v)) = f v
liftCV _ _ _ _ _ _ _ _ _ _ f _ (CV _ (CMaybe v)) = f v
liftCV _ _ _ _ _ _ _ _ _ _ _ f (CV _ (CEither v)) = f 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 r i f d c s u v m e w x y = case (cvVal x, cvVal y) of
(CAlgReal a, CAlgReal b) -> r a b
(CInteger a, CInteger b) -> i a b
(CFloat a, CFloat b) -> f a b
(CDouble a, CDouble b) -> d a b
(CChar a, CChar b) -> c a b
(CString a, CString b) -> s a b
(CList a, CList b) -> u a b
(CTuple a, CTuple b) -> v a b
(CMaybe a, CMaybe b) -> m a b
(CEither a, CEither b) -> e a b
(CUserSort a, CUserSort b) -> w a b
_ -> error $ "SBV.liftCV2: impossible, incompatible args received: " ++ show (x, y)
mapCV :: (AlgReal -> AlgReal)
-> (Integer -> Integer)
-> (Float -> Float)
-> (Double -> Double)
-> (Char -> Char)
-> (String -> String)
-> ((Maybe Int, String) -> (Maybe Int, String))
-> CV
-> CV
mapCV r i f d c s u x = normCV $ CV (kindOf x) $ case cvVal x of
CAlgReal a -> CAlgReal (r a)
CInteger a -> CInteger (i a)
CFloat a -> CFloat (f a)
CDouble a -> CDouble (d a)
CChar a -> CChar (c a)
CString a -> CString (s a)
CUserSort a -> CUserSort (u a)
CList{} -> error "Data.SBV.mapCV: Unexpected call through mapCV with lists!"
CSet{} -> error "Data.SBV.mapCV: Unexpected call through mapCV with sets!"
CTuple{} -> error "Data.SBV.mapCV: Unexpected call through mapCV with tuples!"
CMaybe{} -> error "Data.SBV.mapCV: Unexpected call through mapCV with maybe!"
CEither{} -> 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 r i f d c s u x y = case (cvSameType x y, cvVal x, cvVal y) of
(True, CAlgReal a, CAlgReal b) -> normCV $ CV (kindOf x) (CAlgReal (r a b))
(True, CInteger a, CInteger b) -> normCV $ CV (kindOf x) (CInteger (i a b))
(True, CFloat a, CFloat b) -> normCV $ CV (kindOf x) (CFloat (f a b))
(True, CDouble a, CDouble b) -> normCV $ CV (kindOf x) (CDouble (d a b))
(True, CChar a, CChar b) -> normCV $ CV (kindOf x) (CChar (c a b))
(True, CString a, CString b) -> normCV $ CV (kindOf x) (CString (s a b))
(True, CUserSort a, CUserSort b) -> normCV $ CV (kindOf x) (CUserSort (u a b))
(True, CList{}, CList{}) -> error "Data.SBV.mapCV2: Unexpected call through mapCV2 with lists!"
(True, CTuple{}, CTuple{}) -> error "Data.SBV.mapCV2: Unexpected call through mapCV2 with tuples!"
(True, CMaybe{}, CMaybe{}) -> error "Data.SBV.mapCV2: Unexpected call through mapCV2 with maybes!"
(True, CEither{}, CEither{}) -> error "Data.SBV.mapCV2: Unexpected call through mapCV2 with eithers!"
_ -> error $ "SBV.mapCV2: impossible, incompatible args received: " ++ show (x, y)
instance Show CV where
show = showCV True
instance Show GeneralizedCV where
show (ExtendedCV k) = showExtCV True k
show (RegularCV c) = showCV True c
showCV :: Bool -> CV -> String
showCV shk w | isBoolean w = show (cvToBool w) ++ (if shk then " :: Bool" else "")
showCV shk w = liftCV show show show show show show snd shL shS shT shMaybe shEither w ++ kInfo
where kw = kindOf w
kInfo | shk = " :: " ++ showBaseKind kw
| True = ""
shL xs = "[" ++ intercalate "," (map (showCV False . CV ke) xs) ++ "]"
where ke = case kw of
KList k -> k
_ -> error $ "Data.SBV.showCV: Impossible happened, expected list, got: " ++ show kw
shS :: RCSet CVal -> String
shS eru = case eru of
RegularSet e -> sh e
ComplementSet e | Set.null e -> "U"
| True -> "U - " ++ sh e
where sh xs = "{" ++ intercalate "," (map (showCV False . CV ke) (Set.toList xs)) ++ "}"
ke = case kw of
KSet k -> k
_ -> error $ "Data.SBV.showCV: Impossible happened, expected set, got: " ++ show kw
shT :: [CVal] -> String
shT xs = "(" ++ intercalate "," xs' ++ ")"
where xs' = case kw of
KTuple ks | length ks == length xs -> zipWith (\k x -> showCV False (CV k x)) ks xs
_ -> error $ "Data.SBV.showCV: Impossible happened, expected tuple (of length " ++ show (length xs) ++ "), got: " ++ show kw
shMaybe :: Maybe CVal -> String
shMaybe c = case (c, kw) of
(Nothing, KMaybe{}) -> "Nothing"
(Just x, KMaybe k) -> "Just " ++ showCV False (CV k x)
_ -> error $ "Data.SBV.showCV: Impossible happened, expected maybe, got: " ++ show kw
shEither :: Either CVal CVal -> String
shEither val
| KEither k1 k2 <- kw = case val of
Left x -> "Left " ++ showCV False (CV k1 x)
Right y -> "Right " ++ showCV False (CV k2 y)
| True = error $ "Data.SBV.showCV: Impossible happened, expected sum, got: " ++ show kw
mkConstCV :: Integral a => Kind -> a -> CV
mkConstCV KBool a = normCV $ CV KBool (CInteger (toInteger a))
mkConstCV k@KBounded{} a = normCV $ CV k (CInteger (toInteger a))
mkConstCV KUnbounded a = normCV $ CV KUnbounded (CInteger (toInteger a))
mkConstCV KReal a = normCV $ CV KReal (CAlgReal (fromInteger (toInteger a)))
mkConstCV KFloat a = normCV $ CV KFloat (CFloat (fromInteger (toInteger a)))
mkConstCV KDouble a = normCV $ CV KDouble (CDouble (fromInteger (toInteger a)))
mkConstCV KChar a = error $ "Unexpected call to mkConstCV (Char) with value: " ++ show (toInteger a)
mkConstCV KString a = error $ "Unexpected call to mkConstCV (String) with value: " ++ show (toInteger a)
mkConstCV (KUninterpreted s _) a = error $ "Unexpected call to mkConstCV with uninterpreted kind: " ++ s ++ " with value: " ++ show (toInteger a)
mkConstCV k@KList{} a = error $ "Unexpected call to mkConstCV (" ++ show k ++ ") with value: " ++ show (toInteger a)
mkConstCV k@KSet{} a = error $ "Unexpected call to mkConstCV (" ++ show k ++ ") with value: " ++ show (toInteger a)
mkConstCV k@KTuple{} a = error $ "Unexpected call to mkConstCV (" ++ show k ++ ") with value: " ++ show (toInteger a)
mkConstCV k@KMaybe{} a = error $ "Unexpected call to mkConstCV (" ++ show k ++ ") with value: " ++ show (toInteger a)
mkConstCV k@KEither{} a = error $ "Unexpected call to mkConstCV (" ++ show k ++ ") with value: " ++ show (toInteger a)
randomCVal :: Kind -> IO CVal
randomCVal k =
case k of
KBool -> CInteger <$> randomRIO (0, 1)
KBounded s w -> CInteger <$> randomRIO (bounds s w)
KUnbounded -> CInteger <$> randomIO
KReal -> CAlgReal <$> randomIO
KFloat -> CFloat <$> randomIO
KDouble -> CDouble <$> randomIO
KString -> do l <- randomRIO (0, 100)
CString <$> replicateM l (chr <$> randomRIO (0, 255))
KChar -> CChar . chr <$> randomRIO (0, 255)
KUninterpreted s _ -> error $ "Unexpected call to randomCVal with uninterpreted kind: " ++ s
KList ek -> do l <- randomRIO (0, 100)
CList <$> replicateM l (randomCVal ek)
KSet ek -> do i <- randomIO
l <- randomRIO (0, 100)
vals <- Set.fromList <$> replicateM l (randomCVal ek)
return $ CSet $ if i then RegularSet vals else ComplementSet vals
KTuple ks -> CTuple <$> traverse randomCVal ks
KMaybe ke -> do i <- randomIO
if i
then return $ CMaybe Nothing
else CMaybe . Just <$> randomCVal ke
KEither k1 k2 -> do i <- randomIO
if i
then CEither . Left <$> randomCVal k1
else CEither . Right <$> randomCVal k2
where
bounds :: Bool -> Int -> (Integer, Integer)
bounds False w = (0, 2^w - 1)
bounds True w = (-x, x-1) where x = 2^(w-1)
randomCV :: Kind -> IO CV
randomCV k = CV k <$> randomCVal k
{-# ANN module ("HLint: ignore Redundant if" :: String) #-}