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

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

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

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

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

-- | 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.
          | CUserSort !(Maybe Int, String)    -- ^ Value of an uninterpreted/user kind. The Maybe Int shows index position for enumerations
          | CTuple    ![CVal]                 -- ^ Tuple
          | CMaybe    !(Maybe CVal)           -- ^ Maybe
          | CEither   !(Either CVal CVal)     -- ^ Disjoint union
          | 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 CUserSort {} = Int
10
cvRank CTuple    {} = Int
11
cvRank CMaybe    {} = Int
12
cvRank CEither   {} = Int
13
cvRank CArray    {} = Int
14

-- | 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
  CUserSort (Maybe Int, String)
a == CUserSort (Maybe Int, String)
b = (Maybe Int, String)
a (Maybe Int, String) -> (Maybe Int, String) -> Bool
forall a. Eq a => a -> a -> Bool
== (Maybe Int, String)
b
  CTuple    [CVal]
a == CTuple    [CVal]
b = [CVal]
a [CVal] -> [CVal] -> Bool
forall a. Eq a => a -> a -> Bool
== [CVal]
b
  CMaybe    Maybe CVal
a == CMaybe    Maybe CVal
b = Maybe CVal
a Maybe CVal -> Maybe CVal -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe CVal
b
  CEither   Either CVal CVal
a == CEither   Either CVal CVal
b = Either CVal CVal
a Either CVal CVal -> Either CVal CVal -> Bool
forall a. Eq a => a -> a -> Bool
== Either CVal CVal
b

  -- 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
  CUserSort (Maybe Int, String)
a `compare` CUserSort (Maybe Int, String)
b = (Maybe Int, String)
a (Maybe Int, String) -> (Maybe Int, String) -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare`                  (Maybe Int, String)
b
  CTuple    [CVal]
a `compare` CTuple    [CVal]
b = [CVal]
a [CVal] -> [CVal] -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare`                  [CVal]
b
  CMaybe    Maybe CVal
a `compare` CMaybe    Maybe CVal
b = Maybe CVal
a Maybe CVal -> Maybe CVal -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare`                  Maybe CVal
b
  CEither   Either CVal CVal
a `compare` CEither   Either CVal CVal
b = Either CVal CVal
a Either CVal CVal -> Either CVal CVal -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare`                  Either CVal CVal
b

  -- 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]
++ Kind -> String
showBaseKind (ExtCV -> Kind
forall a. HasKind a => a -> Kind
kindOf ExtCV
extCV) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"
                                       | Bool
True       = String
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: "  String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
showBaseKind (ExtCV -> Kind
forall a. HasKind a => a -> Kind
kindOf ExtCV
extCV)

                 add :: String -> String -> String
                 add :: String -> ShowS
add String
n (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!"
                                                    CUserSort{} -> String -> CVal
forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV: Unexpected call through mapCV with uninterpreted sorts!"
                                                    CList{}     -> String -> CVal
forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV: Unexpected call through mapCV with lists!"
                                                    CSet{}      -> String -> CVal
forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV: Unexpected call through mapCV with sets!"
                                                    CTuple{}    -> String -> CVal
forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV: Unexpected call through mapCV with tuples!"
                                                    CMaybe{}    -> String -> CVal
forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV: Unexpected call through mapCV with maybe!"
                                                    CEither{}   -> String -> CVal
forall a. HasCallStack => String -> a
error String
"Data.SBV.mapCV: Unexpected call through mapCV with either!"
                                                    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 {b}. String -> b
unexpected String
"chars!"
                            (Bool
True, CString{},   CString{})   -> String -> CV
forall {b}. String -> b
unexpected String
"strings!"
                            (Bool
True, CUserSort{}, CUserSort{}) -> String -> CV
forall {b}. String -> b
unexpected String
"uninterpreted constants!"
                            (Bool
True, CList{},     CList{})     -> String -> CV
forall {b}. String -> b
unexpected String
"lists!"
                            (Bool
True, CTuple{},    CTuple{})    -> String -> CV
forall {b}. String -> b
unexpected String
"tuples!"
                            (Bool
True, CMaybe{},    CMaybe{})    -> String -> CV
forall {b}. String -> b
unexpected String
"maybes!"
                            (Bool
True, CEither{},   CEither{})   -> String -> CV
forall {b}. String -> b
unexpected String
"eithers!"
                            (Bool, CVal, CVal)
_                                -> String -> CV
forall {b}. String -> b
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 -> b
unexpected String
w = String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
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]
++ Kind -> String
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 (CUserSort (Maybe Int, String)
v) = (Maybe Int, String) -> String
forall a b. (a, b) -> b
snd  (Maybe Int, String)
v
        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 (CMaybe    Maybe CVal
v) = Maybe CVal -> String
shM  Maybe CVal
v
        sh (CEither   Either CVal CVal
v) = Either CVal CVal -> String
shE  Either CVal 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

        shM :: Maybe CVal -> String
        shM :: Maybe CVal -> String
shM Maybe CVal
c = case (Maybe CVal
c, Kind
wk) of
                  (Maybe CVal
Nothing, KMaybe{}) -> String
"Nothing"
                  (Just CVal
x,  KMaybe Kind
k) -> String
"Just " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
paren (Bool -> CV -> String
showCV Bool
False (Kind -> CVal -> CV
CV Kind
k CVal
x))
                  (Maybe CVal, Kind)
_                   -> ShowS
forall a. HasCallStack => String -> a
error ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.showCV: Impossible happened, expected maybe, got: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
wk

        shE :: Either CVal CVal -> String
        shE :: Either CVal CVal -> String
shE Either CVal CVal
val
          | KEither Kind
k1 Kind
k2 <- Kind
wk = case Either CVal CVal
val of
                                    Left  CVal
x -> String
"Left "  String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
paren (Bool -> CV -> String
showCV Bool
False (Kind -> CVal -> CV
CV Kind
k1 CVal
x))
                                    Right CVal
y -> String
"Right " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
paren (Bool -> CV -> String
showCV Bool
False (Kind -> CVal -> CV
CV Kind
k2 CVal
y))
          | Bool
True                = ShowS
forall a. HasCallStack => String -> a
error ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.showCV: Impossible happened, expected sum, got: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
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

        -- kind of crude, but works ok
        paren :: ShowS
paren String
v
          | Bool
needsParen = Char
'(' Char -> ShowS
forall a. a -> [a] -> [a]
: String
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
          | Bool
True       = String
v
          where needsParen :: Bool
needsParen = case (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace String
v of
                               []         -> Bool
False
                               rest :: String
rest@(Char
x:String
_) -> Char
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'-' Bool -> Bool -> Bool
|| ((Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Char -> Bool
isSpace String
rest Bool -> Bool -> Bool
&& Char
x Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` String
"{[(")

-- | Create a constant word from an integral.
mkConstCV :: Integral a => Kind -> a -> CV
mkConstCV :: forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
KBool           a
a = CV -> CV
normCV (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KBool      (Integer -> CVal
CInteger  (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a))
mkConstCV k :: Kind
k@KBounded{}    a
a = CV -> CV
normCV (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k          (Integer -> CVal
CInteger  (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a))
mkConstCV Kind
KUnbounded      a
a = CV -> CV
normCV (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KUnbounded (Integer -> CVal
CInteger  (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a))
mkConstCV Kind
KReal           a
a = CV -> CV
normCV (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KReal      (AlgReal -> CVal
CAlgReal  (Integer -> AlgReal
forall a. Num a => Integer -> a
fromInteger (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a)))
mkConstCV Kind
KFloat          a
a = CV -> CV
normCV (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KFloat     (Float -> CVal
CFloat    (Integer -> Float
forall a. Num a => Integer -> a
fromInteger (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a)))
mkConstCV Kind
KDouble         a
a = CV -> CV
normCV (CV -> CV) -> CV -> CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KDouble    (Double -> CVal
CDouble   (Integer -> Double
forall a. Num a => Integer -> a
fromInteger (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a)))
mkConstCV k :: Kind
k@(KFP 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 (KUserSort String
s Maybe [String]
_) a
a = String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to mkConstCV with user kind: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" with value: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a)
mkConstCV k :: Kind
k@KList{}       a
a = String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to mkConstCV (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") with value: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a)
mkConstCV k :: Kind
k@KSet{}        a
a = String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to mkConstCV (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") with value: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a)
mkConstCV k :: Kind
k@KTuple{}      a
a = String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to mkConstCV (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") with value: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a)
mkConstCV k :: Kind
k@KMaybe{}      a
a = String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to mkConstCV (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") with value: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a)
mkConstCV k :: Kind
k@KEither{}     a
a = String -> CV
forall a. HasCallStack => String -> a
error (String -> CV) -> String -> CV
forall a b. (a -> b) -> a -> b
$ String
"Unexpected call to mkConstCV (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") with value: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a)
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
    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 sgn <- (Integer, Integer) -> IO Integer
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Integer
0 :: Integer, Integer
1)
                             let sign = Integer
sgn Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1
                             e   <- randomRIO (0 :: Integer, 2^eb-1)
                             s   <- randomRIO (0 :: Integer, 2^sb-1)
                             pure $ CFP $ fpFromRawRep sign (e, eb) (s, sb)

    -- TODO: KString/KChar currently only go for 0..255; include unicode?
    Kind
KString            -> do l <- (Int, Int) -> IO Int
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Int
0, Int
100)
                             CString <$> replicateM l (chr <$> randomRIO (0, 255))
    Kind
KChar              -> Char -> CVal
CChar (Char -> CVal) -> (Int -> Char) -> Int -> CVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Char
chr (Int -> CVal) -> IO Int -> IO CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int, Int) -> IO Int
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Int
0, Int
255)
    KUserSort String
s Maybe [String]
es     -> case Maybe [String]
es of
                            Just vs :: [String]
vs@(String
_:[String]
_) -> do i <- (Int, Int) -> IO Int
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Int
0, [String] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
vs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
                                                pure $ CUserSort (Just i, vs !! i)
                            Maybe [String]
_             -> String -> IO CVal
forall a. HasCallStack => String -> a
error (String -> IO CVal) -> String -> IO CVal
forall a b. (a -> b) -> a -> b
$ String
"randomCVal: Not supported for completely uninterpreted type: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
    KList Kind
ek           -> do l <- (Int, Int) -> IO Int
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Int
0, Int
100)
                             CList <$> replicateM l (randomCVal ek)
    KSet  Kind
ek           -> do i <- IO Bool
forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO                           -- regular or complement
                             l <- randomRIO (0, 100)                 -- some set upto 100 elements
                             vals <- Set.fromList <$> replicateM l (randomCVal ek)
                             return $ CSet $ if i then RegularSet vals else ComplementSet 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
    KMaybe Kind
ke          -> do i <- IO Bool
forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO
                             if i
                                then return $ CMaybe Nothing
                                else CMaybe . Just <$> randomCVal ke
    KEither Kind
k1 Kind
k2      -> do i <- IO Bool
forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO
                             if i
                                then CEither . Left  <$> randomCVal k1
                                else CEither . Right <$> randomCVal k2
    KArray Kind
k1 Kind
k2       -> do l   <- (Int, Int) -> IO Int
forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
randomRIO (Int
0, Int
100)
                             ks  <- replicateM l (randomCVal k1)
                             vs  <- replicateM l (randomCVal k2)
                             def <- randomCVal k2
                             return $ CArray $ ArrayModel (zip ks vs) 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" -}