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

{-# LANGUAGE DeriveAnyClass      #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE DeriveGeneric       #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Core.Concrete where

import Control.Monad (replicateM)

import Control.DeepSeq (NFData)

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

import Data.Char (chr, isSpace)
import Data.List (intercalate)
import qualified Data.Text as T

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

import Data.Proxy

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

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

import qualified Data.Generics as G

import GHC.Generics

import Test.QuickCheck (Arbitrary(..))

-- | 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)
             deriving (RCSet a -> ()
(RCSet a -> ()) -> NFData (RCSet a)
forall a. NFData a => RCSet a -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall a. NFData a => RCSet a -> ()
rnf :: RCSet a -> ()
NFData, Typeable (RCSet a)
Typeable (RCSet a) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> RCSet a -> c (RCSet a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (RCSet a))
-> (RCSet a -> Constr)
-> (RCSet a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (RCSet a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RCSet a)))
-> ((forall b. Data b => b -> b) -> RCSet a -> RCSet a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> RCSet a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> RCSet a -> r)
-> (forall u. (forall d. Data d => d -> u) -> RCSet a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> RCSet a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> RCSet a -> m (RCSet a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RCSet a -> m (RCSet a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RCSet a -> m (RCSet a))
-> Data (RCSet a)
RCSet a -> Constr
RCSet a -> DataType
(forall b. Data b => b -> b) -> RCSet a -> RCSet a
forall a. (Data a, Ord a) => Typeable (RCSet a)
forall a. (Data a, Ord a) => RCSet a -> Constr
forall a. (Data a, Ord a) => RCSet a -> DataType
forall a.
(Data a, Ord a) =>
(forall b. Data b => b -> b) -> RCSet a -> RCSet a
forall a u.
(Data a, Ord a) =>
Int -> (forall d. Data d => d -> u) -> RCSet a -> u
forall a u.
(Data a, Ord a) =>
(forall d. Data d => d -> u) -> RCSet a -> [u]
forall a r r'.
(Data a, Ord a) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RCSet a -> r
forall a r r'.
(Data a, Ord a) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RCSet a -> r
forall a (m :: * -> *).
(Data a, Ord a, Monad m) =>
(forall d. Data d => d -> m d) -> RCSet a -> m (RCSet a)
forall a (m :: * -> *).
(Data a, Ord a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> RCSet a -> m (RCSet a)
forall a (c :: * -> *).
(Data a, Ord a) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (RCSet a)
forall a (c :: * -> *).
(Data a, Ord a) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RCSet a -> c (RCSet a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Ord a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (RCSet a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Ord a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RCSet a))
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> RCSet a -> u
forall u. (forall d. Data d => d -> u) -> RCSet a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RCSet a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RCSet a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RCSet a -> m (RCSet a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RCSet a -> m (RCSet a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (RCSet a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RCSet a -> c (RCSet a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (RCSet a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RCSet a))
$cgfoldl :: forall a (c :: * -> *).
(Data a, Ord a) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RCSet a -> c (RCSet a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RCSet a -> c (RCSet a)
$cgunfold :: forall a (c :: * -> *).
(Data a, Ord a) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (RCSet a)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (RCSet a)
$ctoConstr :: forall a. (Data a, Ord a) => RCSet a -> Constr
toConstr :: RCSet a -> Constr
$cdataTypeOf :: forall a. (Data a, Ord a) => RCSet a -> DataType
dataTypeOf :: RCSet a -> DataType
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Ord a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (RCSet a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (RCSet a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Ord a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RCSet a))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (RCSet a))
$cgmapT :: forall a.
(Data a, Ord a) =>
(forall b. Data b => b -> b) -> RCSet a -> RCSet a
gmapT :: (forall b. Data b => b -> b) -> RCSet a -> RCSet a
$cgmapQl :: forall a r r'.
(Data a, Ord a) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RCSet a -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RCSet a -> r
$cgmapQr :: forall a r r'.
(Data a, Ord a) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RCSet a -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RCSet a -> r
$cgmapQ :: forall a u.
(Data a, Ord a) =>
(forall d. Data d => d -> u) -> RCSet a -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> RCSet a -> [u]
$cgmapQi :: forall a u.
(Data a, Ord a) =>
Int -> (forall d. Data d => d -> u) -> RCSet a -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> RCSet a -> u
$cgmapM :: forall a (m :: * -> *).
(Data a, Ord a, Monad m) =>
(forall d. Data d => d -> m d) -> RCSet a -> m (RCSet a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RCSet a -> m (RCSet a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, Ord a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> RCSet a -> m (RCSet a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RCSet a -> m (RCSet a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, Ord a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> RCSet a -> m (RCSet a)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RCSet a -> m (RCSet a)
G.Data, (forall x. RCSet a -> Rep (RCSet a) x)
-> (forall x. Rep (RCSet a) x -> RCSet a) -> Generic (RCSet a)
forall x. Rep (RCSet a) x -> RCSet a
forall x. RCSet a -> Rep (RCSet a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (RCSet a) x -> RCSet a
forall a x. RCSet a -> Rep (RCSet a) x
$cfrom :: forall a x. RCSet a -> Rep (RCSet a) x
from :: forall x. RCSet a -> Rep (RCSet a) x
$cto :: forall a x. Rep (RCSet a) x -> RCSet a
to :: forall x. Rep (RCSet a) x -> RCSet a
Generic)

instance (Ord a, Arbitrary a) => Arbitrary (RCSet a) where
  arbitrary :: Gen (RCSet a)
arbitrary = do Bool
c :: Bool <- Gen Bool
forall a. Arbitrary a => Gen a
arbitrary
                 if Bool
c then Set a -> RCSet a
forall a. Set a -> RCSet a
RegularSet    (Set a -> RCSet a) -> Gen (Set a) -> Gen (RCSet a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Set a)
forall a. Arbitrary a => Gen a
arbitrary
                      else Set a -> RCSet a
forall a. Set a -> RCSet a
ComplementSet (Set a -> RCSet a) -> Gen (Set a) -> Gen (RCSet a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Set a)
forall a. Arbitrary a => Gen a
arbitrary

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

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

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

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

-- | Underlying type for SMTLib arrays, as a list of key-value pairs, with a default for unmapped
-- elements. Note that this type matches the typical models returned by SMT-solvers.
-- When we store the array, we do not bother removing earlier writes, so there might be duplicates.
-- That is, we store the history of the writes. The earlier a pair is in the list, the "later" it
-- is done, i.e., it takes precedence over the latter entries.
data ArrayModel a b = ArrayModel [(a, b)] b
                     deriving (Typeable (ArrayModel a b)
Typeable (ArrayModel a b) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> ArrayModel a b -> c (ArrayModel a b))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (ArrayModel a b))
-> (ArrayModel a b -> Constr)
-> (ArrayModel a b -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (ArrayModel a b)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (ArrayModel a b)))
-> ((forall b. Data b => b -> b)
    -> ArrayModel a b -> ArrayModel a b)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ArrayModel a b -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ArrayModel a b -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> ArrayModel a b -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> ArrayModel a b -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> ArrayModel a b -> m (ArrayModel a b))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> ArrayModel a b -> m (ArrayModel a b))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> ArrayModel a b -> m (ArrayModel a b))
-> Data (ArrayModel a b)
ArrayModel a b -> Constr
ArrayModel a b -> DataType
(forall b. Data b => b -> b) -> ArrayModel a b -> ArrayModel a b
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> ArrayModel a b -> u
forall u. (forall d. Data d => d -> u) -> ArrayModel a b -> [u]
forall a b. (Data a, Data b) => Typeable (ArrayModel a b)
forall a b. (Data a, Data b) => ArrayModel a b -> Constr
forall a b. (Data a, Data b) => ArrayModel a b -> DataType
forall a b.
(Data a, Data b) =>
(forall b. Data b => b -> b) -> ArrayModel a b -> ArrayModel a b
forall a b u.
(Data a, Data b) =>
Int -> (forall d. Data d => d -> u) -> ArrayModel a b -> u
forall a b u.
(Data a, Data b) =>
(forall d. Data d => d -> u) -> ArrayModel a b -> [u]
forall a b r r'.
(Data a, Data b) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ArrayModel a b -> r
forall a b r r'.
(Data a, Data b) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ArrayModel a b -> r
forall a b (m :: * -> *).
(Data a, Data b, Monad m) =>
(forall d. Data d => d -> m d)
-> ArrayModel a b -> m (ArrayModel a b)
forall a b (m :: * -> *).
(Data a, Data b, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> ArrayModel a b -> m (ArrayModel a b)
forall a b (c :: * -> *).
(Data a, Data b) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ArrayModel a b)
forall a b (c :: * -> *).
(Data a, Data b) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ArrayModel a b -> c (ArrayModel a b)
forall a b (t :: * -> *) (c :: * -> *).
(Data a, Data b, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (ArrayModel a b))
forall a b (t :: * -> * -> *) (c :: * -> *).
(Data a, Data b, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (ArrayModel a b))
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ArrayModel a b -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ArrayModel a b -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> ArrayModel a b -> m (ArrayModel a b)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ArrayModel a b -> m (ArrayModel a b)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ArrayModel a b)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ArrayModel a b -> c (ArrayModel a b)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (ArrayModel a b))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (ArrayModel a b))
$cgfoldl :: forall a b (c :: * -> *).
(Data a, Data b) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ArrayModel a b -> c (ArrayModel a b)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ArrayModel a b -> c (ArrayModel a b)
$cgunfold :: forall a b (c :: * -> *).
(Data a, Data b) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ArrayModel a b)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ArrayModel a b)
$ctoConstr :: forall a b. (Data a, Data b) => ArrayModel a b -> Constr
toConstr :: ArrayModel a b -> Constr
$cdataTypeOf :: forall a b. (Data a, Data b) => ArrayModel a b -> DataType
dataTypeOf :: ArrayModel a b -> DataType
$cdataCast1 :: forall a b (t :: * -> *) (c :: * -> *).
(Data a, Data b, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (ArrayModel a b))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (ArrayModel a b))
$cdataCast2 :: forall a b (t :: * -> * -> *) (c :: * -> *).
(Data a, Data b, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (ArrayModel a b))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (ArrayModel a b))
$cgmapT :: forall a b.
(Data a, Data b) =>
(forall b. Data b => b -> b) -> ArrayModel a b -> ArrayModel a b
gmapT :: (forall b. Data b => b -> b) -> ArrayModel a b -> ArrayModel a b
$cgmapQl :: forall a b r r'.
(Data a, Data b) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ArrayModel a b -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ArrayModel a b -> r
$cgmapQr :: forall a b r r'.
(Data a, Data b) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ArrayModel a b -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ArrayModel a b -> r
$cgmapQ :: forall a b u.
(Data a, Data b) =>
(forall d. Data d => d -> u) -> ArrayModel a b -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> ArrayModel a b -> [u]
$cgmapQi :: forall a b u.
(Data a, Data b) =>
Int -> (forall d. Data d => d -> u) -> ArrayModel a b -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> ArrayModel a b -> u
$cgmapM :: forall a b (m :: * -> *).
(Data a, Data b, Monad m) =>
(forall d. Data d => d -> m d)
-> ArrayModel a b -> m (ArrayModel a b)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> ArrayModel a b -> m (ArrayModel a b)
$cgmapMp :: forall a b (m :: * -> *).
(Data a, Data b, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> ArrayModel a b -> m (ArrayModel a b)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ArrayModel a b -> m (ArrayModel a b)
$cgmapMo :: forall a b (m :: * -> *).
(Data a, Data b, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> ArrayModel a b -> m (ArrayModel a b)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ArrayModel a b -> m (ArrayModel a b)
G.Data, (forall x. ArrayModel a b -> Rep (ArrayModel a b) x)
-> (forall x. Rep (ArrayModel a b) x -> ArrayModel a b)
-> Generic (ArrayModel a b)
forall x. Rep (ArrayModel a b) x -> ArrayModel a b
forall x. ArrayModel a b -> Rep (ArrayModel a b) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a b x. Rep (ArrayModel a b) x -> ArrayModel a b
forall a b x. ArrayModel a b -> Rep (ArrayModel a b) x
$cfrom :: forall a b x. ArrayModel a b -> Rep (ArrayModel a b) x
from :: forall x. ArrayModel a b -> Rep (ArrayModel a b) x
$cto :: forall a b x. Rep (ArrayModel a b) x -> ArrayModel a b
to :: forall x. Rep (ArrayModel a b) x -> ArrayModel a b
Generic, ArrayModel a b -> ()
(ArrayModel a b -> ()) -> NFData (ArrayModel a b)
forall a. (a -> ()) -> NFData a
forall a b. (NFData a, NFData b) => ArrayModel a b -> ()
$crnf :: forall a b. (NFData a, NFData b) => ArrayModel a b -> ()
rnf :: ArrayModel a b -> ()
NFData, Int -> ArrayModel a b -> ShowS
[ArrayModel a b] -> ShowS
ArrayModel a b -> String
(Int -> ArrayModel a b -> ShowS)
-> (ArrayModel a b -> String)
-> ([ArrayModel a b] -> ShowS)
-> Show (ArrayModel a b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. (Show a, Show b) => Int -> ArrayModel a b -> ShowS
forall a b. (Show a, Show b) => [ArrayModel a b] -> ShowS
forall a b. (Show a, Show b) => ArrayModel a b -> String
$cshowsPrec :: forall a b. (Show a, Show b) => Int -> ArrayModel a b -> ShowS
showsPrec :: Int -> ArrayModel a b -> ShowS
$cshow :: forall a b. (Show a, Show b) => ArrayModel a b -> String
show :: ArrayModel a b -> String
$cshowList :: forall a b. (Show a, Show b) => [ArrayModel a b] -> ShowS
showList :: [ArrayModel a b] -> ShowS
Show)

-- | The kind of an ArrayModel
instance (HasKind a, HasKind b) => HasKind (ArrayModel a b) where
   kindOf :: ArrayModel a b -> Kind
kindOf ArrayModel a b
_ = Kind -> Kind -> Kind
KArray (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) (Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b))

-- | A constant value.
-- Note: If you add a new constructor here, make sure you add the
-- corresponding equality in the instance "Eq CVal" and "Ord CVal"!
data CVal = CAlgReal  !AlgReal                 -- ^ Algebraic real
          | CInteger  !Integer                 -- ^ Bit-vector/unbounded integer
          | CFloat    !Float                   -- ^ Float
          | CDouble   !Double                  -- ^ Double
          | CFP       !FP                      -- ^ Arbitrary float
          | CRational Rational                 -- ^ Rational
          | CChar     !Char                    -- ^ Character
          | CString   !String                  -- ^ String
          | CList     ![CVal]                  -- ^ List
          | CSet      !(RCSet CVal)            -- ^ Set. Can be regular or complemented.
          | CADT      (String, [(Kind, CVal)]) -- ^ ADT: Constructor, and fields
          | CTuple    ![CVal]                  -- ^ Tuple
          | CArray    !(ArrayModel CVal CVal)  -- ^ Arrays are backed by look-up tables concretely
          deriving (Typeable CVal
Typeable CVal =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> CVal -> c CVal)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CVal)
-> (CVal -> Constr)
-> (CVal -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CVal))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CVal))
-> ((forall b. Data b => b -> b) -> CVal -> CVal)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CVal -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CVal -> r)
-> (forall u. (forall d. Data d => d -> u) -> CVal -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> CVal -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CVal -> m CVal)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CVal -> m CVal)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CVal -> m CVal)
-> Data CVal
CVal -> Constr
CVal -> DataType
(forall b. Data b => b -> b) -> CVal -> CVal
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> CVal -> u
forall u. (forall d. Data d => d -> u) -> CVal -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CVal -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CVal -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CVal -> m CVal
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CVal -> m CVal
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CVal
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CVal -> c CVal
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CVal)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CVal)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CVal -> c CVal
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CVal -> c CVal
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CVal
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CVal
$ctoConstr :: CVal -> Constr
toConstr :: CVal -> Constr
$cdataTypeOf :: CVal -> DataType
dataTypeOf :: CVal -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CVal)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CVal)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CVal)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CVal)
$cgmapT :: (forall b. Data b => b -> b) -> CVal -> CVal
gmapT :: (forall b. Data b => b -> b) -> CVal -> CVal
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CVal -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CVal -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CVal -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CVal -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> CVal -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> CVal -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CVal -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CVal -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CVal -> m CVal
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CVal -> m CVal
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CVal -> m CVal
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CVal -> m CVal
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CVal -> m CVal
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CVal -> m CVal
G.Data, (forall x. CVal -> Rep CVal x)
-> (forall x. Rep CVal x -> CVal) -> Generic CVal
forall x. Rep CVal x -> CVal
forall x. CVal -> Rep CVal x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CVal -> Rep CVal x
from :: forall x. CVal -> Rep CVal x
$cto :: forall x. Rep CVal x -> CVal
to :: forall x. Rep CVal x -> CVal
Generic, CVal -> ()
(CVal -> ()) -> NFData CVal
forall a. (a -> ()) -> NFData a
$crnf :: CVal -> ()
rnf :: CVal -> ()
NFData)

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

-- | Eq instance for CVal. Note that we cannot simply derive Eq/Ord, since CVAlgReal doesn't have proper
-- instances for these when values are infinitely precise reals. However, we do
-- need a structural eq/ord for Map indexes; so define custom ones here:
instance Eq CVal where
  CAlgReal  AlgReal
a == :: CVal -> CVal -> Bool
== CAlgReal  AlgReal
b = AlgReal
a AlgReal -> AlgReal -> Bool
`algRealStructuralEqual` AlgReal
b
  CInteger  Integer
a == CInteger  Integer
b = Integer
a Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
b
  CFloat    Float
a == CFloat    Float
b = Float
a Float -> Float -> Bool
forall a. RealFloat a => a -> a -> Bool
`fpIsEqualObjectH` Float
b   -- We don't want +0/-0 to be confused; and also we want NaN = NaN here!
  CDouble   Double
a == CDouble   Double
b = Double
a Double -> Double -> Bool
forall a. RealFloat a => a -> a -> Bool
`fpIsEqualObjectH` Double
b   -- ditto
  CRational Rational
a == CRational Rational
b = Rational
a Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
b
  CFP       FP
a == CFP       FP
b = FP
a FP -> FP -> Bool
`arbFPIsEqualObjectH` FP
b
  CChar     Char
a == CChar     Char
b = Char
a Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
b
  CString   String
a == CString   String
b = String
a String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
b
  CList     [CVal]
a == CList     [CVal]
b = [CVal]
a [CVal] -> [CVal] -> Bool
forall a. Eq a => a -> a -> Bool
== [CVal]
b
  CSet      RCSet CVal
a == CSet      RCSet CVal
b = RCSet CVal
a RCSet CVal -> RCSet CVal -> Bool
forall a. Eq a => RCSet a -> RCSet a -> Bool
`eqRCSet` RCSet CVal
b
  CTuple    [CVal]
a == CTuple    [CVal]
b = [CVal]
a [CVal] -> [CVal] -> Bool
forall a. Eq a => a -> a -> Bool
== [CVal]
b
  CADT      (String, [(Kind, CVal)])
a == CADT      (String, [(Kind, CVal)])
b = (String, [(Kind, CVal)])
a (String, [(Kind, CVal)]) -> (String, [(Kind, CVal)]) -> Bool
forall a. Eq a => a -> a -> Bool
== (String, [(Kind, CVal)])
b

  -- This is legit since we don't use this equality for actual semantic" equality, but rather as an index into maps
  CArray    (ArrayModel [(CVal, CVal)]
a1 CVal
d1) == CArray (ArrayModel [(CVal, CVal)]
a2 CVal
d2) = ([(CVal, CVal)]
a1, CVal
d1) ([(CVal, CVal)], CVal) -> ([(CVal, CVal)], CVal) -> Bool
forall a. Eq a => a -> a -> Bool
== ([(CVal, CVal)]
a2, CVal
d2)

  CVal
a           == CVal
b           = if CVal -> Int
cvRank CVal
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== CVal -> Int
cvRank CVal
b
                                  then String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                                       , String
"*** Data.SBV.Eq.CVal: Impossible happened: same rank in comparison fallthru"
                                                       , String
"***"
                                                       , String
"***   Received: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall a. Show a => a -> String
show (CVal -> Int
cvRank CVal
a, CVal -> Int
cvRank CVal
b)
                                                       , String
"***"
                                                       , String
"*** Please report this as a bug!"
                                                       ]
                                  else Bool
False

-- | Ord instance for CVal. Same comments as the 'Eq' instance why this cannot be derived.
instance Ord CVal where
  CAlgReal  AlgReal
a compare :: CVal -> CVal -> Ordering
`compare` CAlgReal  AlgReal
b = AlgReal
a AlgReal -> AlgReal -> Ordering
`algRealStructuralCompare` AlgReal
b
  CInteger  Integer
a `compare` CInteger  Integer
b = Integer
a Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare`                  Integer
b
  CFloat    Float
a `compare` CFloat    Float
b = Float
a Float -> Float -> Ordering
forall a. RealFloat a => a -> a -> Ordering
`fpCompareObjectH`         Float
b
  CDouble   Double
a `compare` CDouble   Double
b = Double
a Double -> Double -> Ordering
forall a. RealFloat a => a -> a -> Ordering
`fpCompareObjectH`         Double
b
  CRational Rational
a `compare` CRational Rational
b = Rational
a Rational -> Rational -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare`                  Rational
b
  CFP       FP
a `compare` CFP       FP
b = FP
a FP -> FP -> Ordering
`arbFPCompareObjectH`      FP
b
  CChar     Char
a `compare` CChar     Char
b = Char
a Char -> Char -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare`                  Char
b
  CString   String
a `compare` CString   String
b = String
a String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare`                  String
b
  CList     [CVal]
a `compare` CList     [CVal]
b = [CVal]
a [CVal] -> [CVal] -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare`                  [CVal]
b
  CSet      RCSet CVal
a `compare` CSet      RCSet CVal
b = RCSet CVal
a RCSet CVal -> RCSet CVal -> Ordering
forall a. Ord a => RCSet a -> RCSet a -> Ordering
`compareRCSet`             RCSet CVal
b
  CTuple    [CVal]
a `compare` CTuple    [CVal]
b = [CVal]
a [CVal] -> [CVal] -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare`                  [CVal]
b
  CADT      (String, [(Kind, CVal)])
a `compare` CADT      (String, [(Kind, CVal)])
b = (String, [(Kind, CVal)])
a (String, [(Kind, CVal)]) -> (String, [(Kind, CVal)]) -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare`                  (String, [(Kind, CVal)])
b

  -- This is legit since we don't use this equality for actual semantic order, but rather as an index into maps
  CArray    (ArrayModel [(CVal, CVal)]
a1 CVal
d1) `compare` CArray (ArrayModel [(CVal, CVal)]
a2 CVal
d2) = ([(CVal, CVal)]
a1, CVal
d1) ([(CVal, CVal)], CVal) -> ([(CVal, CVal)], CVal) -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` ([(CVal, CVal)]
a2, CVal
d2)

  CVal
a           `compare` CVal
b           = let ra :: Int
ra = CVal -> Int
cvRank CVal
a
                                          rb :: Int
rb = CVal -> Int
cvRank CVal
b
                                      in if Int
ra Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
rb
                                            then String -> Ordering
forall a. HasCallStack => String -> a
error (String -> Ordering) -> String -> Ordering
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                                                 , String
"*** Data.SBV.Ord.CVal: Impossible happened: same rank in comparison fallthru"
                                                                 , String
"***"
                                                                 , String
"***   Received: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall a. Show a => a -> String
show (Int
ra, Int
rb)
                                                                 , String
"***"
                                                                 , String
"*** Please report this as a bug!"
                                                                 ]
                                            else CVal -> Int
cvRank CVal
a Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` CVal -> Int
cvRank CVal
b

-- | A t'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
$c== :: CV -> CV -> Bool
== :: CV -> CV -> Bool
$c/= :: CV -> CV -> Bool
/= :: 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
$ccompare :: CV -> CV -> Ordering
compare :: CV -> CV -> Ordering
$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
>= :: CV -> CV -> Bool
$cmax :: CV -> CV -> CV
max :: CV -> CV -> CV
$cmin :: CV -> CV -> CV
min :: CV -> CV -> CV
Ord, Typeable CV
Typeable CV =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> CV -> c CV)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CV)
-> (CV -> Constr)
-> (CV -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CV))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CV))
-> ((forall b. Data b => b -> b) -> CV -> CV)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CV -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CV -> r)
-> (forall u. (forall d. Data d => d -> u) -> CV -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> CV -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CV -> m CV)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CV -> m CV)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CV -> m CV)
-> Data CV
CV -> Constr
CV -> DataType
(forall b. Data b => b -> b) -> CV -> CV
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> CV -> u
forall u. (forall d. Data d => d -> u) -> CV -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CV -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CV -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CV -> m CV
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CV -> m CV
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CV
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CV -> c CV
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CV)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CV)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CV -> c CV
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CV -> c CV
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CV
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CV
$ctoConstr :: CV -> Constr
toConstr :: CV -> Constr
$cdataTypeOf :: CV -> DataType
dataTypeOf :: CV -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CV)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CV)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CV)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CV)
$cgmapT :: (forall b. Data b => b -> b) -> CV -> CV
gmapT :: (forall b. Data b => b -> b) -> CV -> CV
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CV -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CV -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CV -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CV -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> CV -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> CV -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CV -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CV -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CV -> m CV
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CV -> m CV
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CV -> m CV
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CV -> m CV
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CV -> m CV
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CV -> m CV
G.Data, CV -> ()
(CV -> ()) -> NFData CV
forall a. (a -> ()) -> NFData a
$crnf :: CV -> ()
rnf :: CV -> ()
NFData, (forall x. CV -> Rep CV x)
-> (forall x. Rep CV x -> CV) -> Generic CV
forall x. Rep CV x -> CV
forall x. CV -> Rep CV x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CV -> Rep CV x
from :: forall x. CV -> Rep CV x
$cto :: forall x. Rep CV x -> CV
to :: forall x. Rep CV x -> CV
Generic)

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

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

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

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

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

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

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

                 add :: String -> String -> String
                 add :: String -> ShowS
add String
n (Char
'-':String
v) = String
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
v
                 add String
n String
v       = String
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" + " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
v

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

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

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

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

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

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

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

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

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

                                v `mod` (2 ^ sz)

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

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

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

-- | Map a unary function through a t'CV'.
mapCV :: (AlgReal             -> AlgReal)
      -> (Integer             -> Integer)
      -> (Float               -> Float)
      -> (Double              -> Double)
      -> (FP                  -> FP)
      -> (Rational            -> Rational)
      -> CV                   -> CV
mapCV :: (AlgReal -> AlgReal)
-> (Integer -> Integer)
-> (Float -> Float)
-> (Double -> Double)
-> (FP -> FP)
-> (Rational -> Rational)
-> CV
-> CV
mapCV AlgReal -> AlgReal
r Integer -> Integer
i Float -> Float
f Double -> Double
d FP -> FP
af Rational -> Rational
ra CV
x  = CV -> CV
normCV (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
x) (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ case CV -> CVal
cvVal CV
x of
                                                    CAlgReal  AlgReal
a -> AlgReal -> CVal
CAlgReal  (AlgReal -> AlgReal
r  AlgReal
a)
                                                    CInteger  Integer
a -> Integer -> CVal
CInteger  (Integer -> Integer
i  Integer
a)
                                                    CFloat    Float
a -> Float -> CVal
CFloat    (Float -> Float
f  Float
a)
                                                    CDouble   Double
a -> Double -> CVal
CDouble   (Double -> Double
d  Double
a)
                                                    CFP       FP
a -> FP -> CVal
CFP       (FP -> FP
af FP
a)
                                                    CRational Rational
a -> Rational -> CVal
CRational (Rational -> Rational
ra Rational
a)
                                                    CChar{}     -> String -> CVal
forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV: Unexpected call through mapCV with chars!"
                                                    CString{}   -> String -> CVal
forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV: Unexpected call through mapCV with strings!"
                                                    CADT{}      -> String -> CVal
forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV: Unexpected call through mapCV with ADTs!"
                                                    CList{}     -> String -> CVal
forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV: Unexpected call through mapCV with lists!"
                                                    CSet{}      -> String -> CVal
forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV: Unexpected call through mapCV with sets!"
                                                    CTuple{}    -> String -> CVal
forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV: Unexpected call through mapCV with tuples!"
                                                    CArray{}    -> String -> CVal
forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV: Unexpected call through mapCV with arrays!"

-- | Map a binary function through a t'CV'.
mapCV2 :: (AlgReal             -> AlgReal             -> AlgReal)
       -> (Integer             -> Integer             -> Integer)
       -> (Float               -> Float               -> Float)
       -> (Double              -> Double              -> Double)
       -> (FP                  -> FP                  -> FP)
       -> (Rational            -> Rational            -> Rational)
       -> CV                   -> CV                  -> CV
mapCV2 :: (AlgReal -> AlgReal -> AlgReal)
-> (Integer -> Integer -> Integer)
-> (Float -> Float -> Float)
-> (Double -> Double -> Double)
-> (FP -> FP -> FP)
-> (Rational -> Rational -> Rational)
-> CV
-> CV
-> CV
mapCV2 AlgReal -> AlgReal -> AlgReal
r Integer -> Integer -> Integer
i Float -> Float -> Float
f Double -> Double -> Double
d FP -> FP -> FP
af Rational -> Rational -> Rational
ra CV
x CV
y = case (CV -> CV -> Bool
cvSameType CV
x CV
y, CV -> CVal
cvVal CV
x, CV -> CVal
cvVal CV
y) of
                            (Bool
True, CAlgReal  AlgReal
a, CAlgReal  AlgReal
b) -> CV -> CV
normCV (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
x) (AlgReal -> CVal
CAlgReal  (AlgReal -> AlgReal -> AlgReal
r  AlgReal
a AlgReal
b))
                            (Bool
True, CInteger  Integer
a, CInteger  Integer
b) -> CV -> CV
normCV (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
x) (Integer -> CVal
CInteger  (Integer -> Integer -> Integer
i  Integer
a Integer
b))
                            (Bool
True, CFloat    Float
a, CFloat    Float
b) -> CV -> CV
normCV (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
x) (Float -> CVal
CFloat    (Float -> Float -> Float
f  Float
a Float
b))
                            (Bool
True, CDouble   Double
a, CDouble   Double
b) -> CV -> CV
normCV (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
x) (Double -> CVal
CDouble   (Double -> Double -> Double
d  Double
a Double
b))
                            (Bool
True, CFP       FP
a, CFP       FP
b) -> CV -> CV
normCV (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
x) (FP -> CVal
CFP       (FP -> FP -> FP
af FP
a FP
b))
                            (Bool
True, CRational Rational
a, CRational Rational
b) -> CV -> CV
normCV (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
x) (Rational -> CVal
CRational (Rational -> Rational -> Rational
ra Rational
a Rational
b))
                            (Bool
True, CChar{},     CChar{})     -> String -> CV
forall {a}. String -> a
unexpected String
"chars!"
                            (Bool
True, CString{},   CString{})   -> String -> CV
forall {a}. String -> a
unexpected String
"strings!"
                            (Bool
True, CList{},     CList{})     -> String -> CV
forall {a}. String -> a
unexpected String
"lists!"
                            (Bool
True, CTuple{},    CTuple{})    -> String -> CV
forall {a}. String -> a
unexpected String
"tuples!"
                            (Bool, CVal, CVal)
_                                -> String -> CV
forall {a}. String -> a
unexpected (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ String
"incompatible args: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (CV, CV) -> String
forall a. Show a => a -> String
show (CV
x, CV
y)
   where unexpected :: String -> a
unexpected String
w = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                        , String
"*** Data.SBV.mapCV2: Unexpected call through mapCV2 with " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
w
                                        , String
"*** Please report this as a bug!"
                                        ]

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

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

-- | Show a CV, with kind info if bool is True
showCV :: Bool -> CV -> String
showCV :: Bool -> CV -> String
showCV Bool
shk CV
w | CV -> Bool
forall a. HasKind a => a -> Bool
isBoolean CV
w = Bool -> String
forall a. Show a => a -> String
show (CV -> Bool
cvToBool CV
w) String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if Bool
shk then String
" :: Bool" else String
"")
showCV Bool
shk CV
w = CVal -> String
sh (CV -> CVal
cvVal CV
w) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
kInfo
  where kInfo :: String
kInfo | Bool
shk  = String
" :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
T.unpack (Kind -> Text
showBaseKind Kind
wk)
              | Bool
True = String
""

        wk :: Kind
wk = CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
w

        sh :: CVal -> String
sh (CAlgReal  AlgReal
v) = AlgReal -> String
forall a. Show a => a -> String
show  AlgReal
v
        sh (CInteger  Integer
v) = Integer -> String
forall a. Show a => a -> String
show  Integer
v
        sh (CFloat    Float
v) = Float -> String
forall a. Show a => a -> String
show  Float
v
        sh (CDouble   Double
v) = Double -> String
forall a. Show a => a -> String
show  Double
v
        sh (CFP       FP
v) = FP -> String
forall a. Show a => a -> String
show  FP
v
        sh (CRational Rational
v) = Rational -> String
forall a. Show a => a -> String
show  Rational
v
        sh (CChar     Char
v) = Char -> String
forall a. Show a => a -> String
show  Char
v
        sh (CString   String
v) = ShowS
forall a. Show a => a -> String
show  String
v
        sh (CADT      (String, [(Kind, CVal)])
c) = (String, [(Kind, CVal)]) -> String
shADT (String, [(Kind, CVal)])
c
        sh (CList     [CVal]
v) = [CVal] -> String
shL   [CVal]
v
        sh (CSet      RCSet CVal
v) = RCSet CVal -> String
shS   RCSet CVal
v
        sh (CTuple    [CVal]
v) = [CVal] -> String
shT   [CVal]
v
        sh (CArray    ArrayModel CVal CVal
v) = ArrayModel CVal CVal -> String
shA   ArrayModel CVal CVal
v

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

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

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

        shA :: ArrayModel CVal CVal -> String
        shA :: ArrayModel CVal CVal -> String
shA (ArrayModel [(CVal, CVal)]
assocs CVal
def)
          | KArray Kind
k1 Kind
k2 <- Kind
wk = String
"([" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," [Bool -> CV -> String
showCV Bool
False (Kind -> CVal -> CV
CV ([Kind] -> Kind
KTuple [Kind
k1, Kind
k2]) ([CVal] -> CVal
CTuple [CVal
a, CVal
b])) | (CVal
a, CVal
b) <- [(CVal, CVal)]
assocs] String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"], " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> CV -> String
showCV Bool
False (Kind -> CVal -> CV
CV Kind
k2 CVal
def) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
          | Bool
True               = ShowS
forall a. HasCallStack => String -> a
error ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.showCV: Impossible happened, expected array, got: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
wk

        shADT :: (String, [(Kind, CVal)]) -> String
shADT (String
c, [(Kind, CVal)]
kvs)
          | forall (t :: * -> *) a. Foldable t => t a -> Bool
null @[] [String]
flds = String
c
          | Bool
True          = [String] -> String
unwords (String
c String -> [String] -> [String]
forall a. a -> [a] -> [a]
: ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ShowS
wrap [String]
flds)
          where wrap :: ShowS
wrap String
v
                 | Int -> ShowS
forall a. Int -> [a] -> [a]
take Int
1 String
v String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
"(", String
"[", String
"{"]  = String
v
                 | (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Char -> Bool
isSpace String
v Bool -> Bool -> Bool
|| Int -> ShowS
forall a. Int -> [a] -> [a]
take Int
1 String
v String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"-" = Char
'(' Char -> ShowS
forall a. a -> [a] -> [a]
: String
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
                 | Bool
True                             = String
v

                flds :: [String]
flds = ((Kind, CVal) -> String) -> [(Kind, CVal)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\(Kind
k, CVal
v) -> Bool -> CV -> String
showCV Bool
False (Kind -> CVal -> CV
CV Kind
k CVal
v)) [(Kind, CVal)]
kvs

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

-- | Generate a random constant value ('CVal') of the correct kind. We error out for a completely uninterpreted type.
randomCVal :: Kind -> IO CVal
randomCVal :: Kind -> IO CVal
randomCVal Kind
k =
  case Kind
k of
    KVar{}             -> String -> IO CVal
forall a. HasCallStack => String -> a
error (String -> IO CVal) -> String -> IO CVal
forall a b. (a -> b) -> a -> b
$ String
"randomCVal: Unexpected kind: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k
    Kind
KBool              -> Integer -> CVal
CInteger  (Integer -> CVal) -> IO Integer -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> IO Integer
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Integer
0, Integer
1)
    KBounded Bool
s Int
w       -> Integer -> CVal
CInteger  (Integer -> CVal) -> IO Integer -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> IO Integer
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Bool -> Int -> (Integer, Integer)
bounds Bool
s Int
w)
    Kind
KUnbounded         -> Integer -> CVal
CInteger  (Integer -> CVal) -> IO Integer -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO Integer
forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO
    Kind
KReal              -> AlgReal -> CVal
CAlgReal  (AlgReal -> CVal) -> IO AlgReal -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO AlgReal
forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO
    Kind
KFloat             -> Float -> CVal
CFloat    (Float -> CVal) -> IO Float -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO Float
forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO
    Kind
KDouble            -> Double -> CVal
CDouble   (Double -> CVal) -> IO Double -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO Double
forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO
    Kind
KRational          -> Rational -> CVal
CRational (Rational -> CVal) -> IO Rational -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO Rational
forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO

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

    -- TODO: KString/KChar currently only go for 0..255; include unicode?
    Kind
KString            -> do Int
l <- (Int, Int) -> IO Int
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Int
0, Int
100)
                             String -> CVal
CString (String -> CVal) -> IO String -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> IO Char -> IO String
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
l (Int -> Char
chr (Int -> Char) -> IO Int -> IO Char
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int, Int) -> IO Int
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Int
0, Int
255))
    Kind
KChar              -> Char -> CVal
CChar (Char -> CVal) -> (Int -> Char) -> Int -> CVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Char
chr (Int -> CVal) -> IO Int -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int, Int) -> IO Int
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Int
0, Int
255)

    -- TODO: Can we do something here?
    KApp String
s [Kind]
_           -> String -> IO CVal
forall a. HasCallStack => String -> a
error (String -> IO CVal) -> String -> IO CVal
forall a b. (a -> b) -> a -> b
$ String
"randomCVal: Not supported for KApp: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s

    KADT String
_ [(String, Kind)]
_ cstrs :: [(String, [Kind])]
cstrs@((String, [Kind])
_:[(String, [Kind])]
_) -> do Int
i <- (Int, Int) -> IO Int
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Int
0, [(String, [Kind])] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(String, [Kind])]
cstrs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
                               let (String
c, [Kind]
fks) = [(String, [Kind])]
cstrs [(String, [Kind])] -> Int -> (String, [Kind])
forall a. HasCallStack => [a] -> Int -> a
!! Int
i
                               [CVal]
vs <- (Kind -> IO CVal) -> [Kind] -> IO [CVal]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Kind -> IO CVal
randomCVal [Kind]
fks
                               CVal -> IO CVal
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CVal -> IO CVal) -> CVal -> IO CVal
forall a b. (a -> b) -> a -> b
$ (String, [(Kind, CVal)]) -> CVal
CADT (String
c, [Kind] -> [CVal] -> [(Kind, CVal)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Kind]
fks [CVal]
vs)
    KADT String
s [(String, Kind)]
_ [(String, [Kind])]
_         -> String -> IO CVal
forall a. HasCallStack => String -> a
error (String -> IO CVal) -> String -> IO CVal
forall a b. (a -> b) -> a -> b
$ String
"randomCVal: Not supported for ADT:  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s

    KList Kind
ek           -> do Int
l <- (Int, Int) -> IO Int
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Int
0, Int
100)
                             [CVal] -> CVal
CList ([CVal] -> CVal) -> IO [CVal] -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> IO CVal -> IO [CVal]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
l (Kind -> IO CVal
randomCVal Kind
ek)

    KSet  Kind
ek           -> do Bool
i <- IO Bool
forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO                           -- regular or complement
                             Int
l <- (Int, Int) -> IO Int
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Int
0, Int
100)                 -- some set upto 100 elements
                             Set CVal
vals <- [CVal] -> Set CVal
forall a. Ord a => [a] -> Set a
Set.fromList ([CVal] -> Set CVal) -> IO [CVal] -> IO (Set CVal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> IO CVal -> IO [CVal]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
l (Kind -> IO CVal
randomCVal Kind
ek)
                             CVal -> IO CVal
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CVal -> IO CVal) -> CVal -> IO CVal
forall a b. (a -> b) -> a -> b
$ RCSet CVal -> CVal
CSet (RCSet CVal -> CVal) -> RCSet CVal -> CVal
forall a b. (a -> b) -> a -> b
$ if Bool
i then Set CVal -> RCSet CVal
forall a. Set a -> RCSet a
RegularSet Set CVal
vals else Set CVal -> RCSet CVal
forall a. Set a -> RCSet a
ComplementSet Set CVal
vals

    KTuple [Kind]
ks          -> [CVal] -> CVal
CTuple ([CVal] -> CVal) -> IO [CVal] -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Kind -> IO CVal) -> [Kind] -> IO [CVal]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Kind -> IO CVal
randomCVal [Kind]
ks

    KArray Kind
k1 Kind
k2       -> do Int
l   <- (Int, Int) -> IO Int
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Int
0, Int
100)
                             [CVal]
ks  <- Int -> IO CVal -> IO [CVal]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
l (Kind -> IO CVal
randomCVal Kind
k1)
                             [CVal]
vs  <- Int -> IO CVal -> IO [CVal]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
l (Kind -> IO CVal
randomCVal Kind
k2)
                             CVal
def <- Kind -> IO CVal
randomCVal Kind
k2
                             CVal -> IO CVal
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CVal -> IO CVal) -> CVal -> IO CVal
forall a b. (a -> b) -> a -> b
$ ArrayModel CVal CVal -> CVal
CArray (ArrayModel CVal CVal -> CVal) -> ArrayModel CVal CVal -> CVal
forall a b. (a -> b) -> a -> b
$ [(CVal, CVal)] -> CVal -> ArrayModel CVal CVal
forall a b. [(a, b)] -> b -> ArrayModel a b
ArrayModel ([CVal] -> [CVal] -> [(CVal, CVal)]
forall a b. [a] -> [b] -> [(a, b)]
zip [CVal]
ks [CVal]
vs) CVal
def
  where
    bounds :: Bool -> Int -> (Integer, Integer)
    bounds :: Bool -> Int -> (Integer, Integer)
bounds Bool
False Int
w = (Integer
0, Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
    bounds Bool
True  Int
w = (-Integer
x, Integer
xInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) where x :: Integer
x = Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)

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

{- HLint ignore module "Redundant if" -}