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

    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeApplications    #-}
    {-# LANGUAGE Rank2Types          #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Core.Concrete
      ( module Data.SBV.Core.Concrete
      ) where

    import Control.Monad (replicateM)

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

    import Data.Char (chr, isSpace)
    import Data.List (isPrefixOf, intercalate)

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

    import Data.Proxy

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

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

    -- | A 'RCSet' is either a regular set or a set given by its complement from the corresponding universal set.
    data RCSet a = RegularSet    (Set a)
                 | ComplementSet (Set a)

    -- | Show instance. Regular sets are shown as usual.
    -- Complements are shown "U -" notation.
    instance Show a => Show (RCSet a) where
      show :: RCSet a -> String
    show 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))

    -- | A constant value
    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

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

    -- | Eq instance for CVVal. Note that we cannot simply derive Eq/Ord, since CVAlgReal doesn't have proper
    -- instances for these when values are infinitely precise reals. However, we do
    -- need a structural eq/ord for Map indexes; so define custom ones here:
    instance Eq CVal where
      CAlgReal  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
      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
      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 VWVal. 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
    `fprCompareObject`         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
      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

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

    -- | 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 String
    v
                      | String
    "-" String -> String -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isPrefixOf` String
    v = String
    n String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " - " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. HasCallStack => [a] -> [a]
    tail String
    v
                      | Bool
    True               = 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 :: CVal
    cvVal = Integer -> CVal
    CInteger Integer
    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 :: CVal
    cvVal = Integer -> CVal
    CInteger (Integer
    v Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .&. Integer
    1) }
    normCV CV
    c                         = CV
    c
    {-# INLINE normCV #-}

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

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

    -- | Lift a unary function through a 'CV'.
    liftCV :: (AlgReal             -> b)
           -> (Integer             -> b)
           -> (Float               -> b)
           -> (Double              -> b)
           -> (FP                  -> b)
           -> (Rational            -> b)
           -> (Char                -> b)
           -> (String              -> b)
           -> ((Maybe Int, String) -> b)
           -> ([CVal]              -> b)
           -> (RCSet CVal          -> b)
           -> ([CVal]              -> b)
           -> (Maybe CVal          -> b)
           -> (Either CVal CVal    -> b)
           -> CV
           -> b
    liftCV :: forall b.
    (AlgReal -> b)
    -> (Integer -> b)
    -> (Float -> b)
    -> (Double -> b)
    -> (FP -> b)
    -> (Rational -> b)
    -> (Char -> b)
    -> (String -> b)
    -> ((Maybe Int, String) -> b)
    -> ([CVal] -> b)
    -> (RCSet CVal -> b)
    -> ([CVal] -> b)
    -> (Maybe CVal -> b)
    -> (Either CVal CVal -> b)
    -> CV
    -> b
    liftCV AlgReal -> b
    f Integer -> b
    _ Float -> b
    _ Double -> b
    _ FP -> b
    _ Rational -> b
    _ Char -> b
    _ String -> b
    _ (Maybe Int, String) -> b
    _ [CVal] -> b
    _ RCSet CVal -> b
    _ [CVal] -> b
    _ Maybe CVal -> b
    _ Either CVal CVal -> b
    _ (CV Kind
    _ (CAlgReal  AlgReal
    v)) = AlgReal -> b
    f AlgReal
    v
    liftCV AlgReal -> b
    _ Integer -> b
    f Float -> b
    _ Double -> b
    _ FP -> b
    _ Rational -> b
    _ Char -> b
    _ String -> b
    _ (Maybe Int, String) -> b
    _ [CVal] -> b
    _ RCSet CVal -> b
    _ [CVal] -> b
    _ Maybe CVal -> b
    _ Either CVal CVal -> b
    _ (CV Kind
    _ (CInteger  Integer
    v)) = Integer -> b
    f Integer
    v
    liftCV AlgReal -> b
    _ Integer -> b
    _ Float -> b
    f Double -> b
    _ FP -> b
    _ Rational -> b
    _ Char -> b
    _ String -> b
    _ (Maybe Int, String) -> b
    _ [CVal] -> b
    _ RCSet CVal -> b
    _ [CVal] -> b
    _ Maybe CVal -> b
    _ Either CVal CVal -> b
    _ (CV Kind
    _ (CFloat    Float
    v)) = Float -> b
    f Float
    v
    liftCV AlgReal -> b
    _ Integer -> b
    _ Float -> b
    _ Double -> b
    f FP -> b
    _ Rational -> b
    _ Char -> b
    _ String -> b
    _ (Maybe Int, String) -> b
    _ [CVal] -> b
    _ RCSet CVal -> b
    _ [CVal] -> b
    _ Maybe CVal -> b
    _ Either CVal CVal -> b
    _ (CV Kind
    _ (CDouble   Double
    v)) = Double -> b
    f Double
    v
    liftCV AlgReal -> b
    _ Integer -> b
    _ Float -> b
    _ Double -> b
    _ FP -> b
    f Rational -> b
    _ Char -> b
    _ String -> b
    _ (Maybe Int, String) -> b
    _ [CVal] -> b
    _ RCSet CVal -> b
    _ [CVal] -> b
    _ Maybe CVal -> b
    _ Either CVal CVal -> b
    _ (CV Kind
    _ (CFP       FP
    v)) = FP -> b
    f FP
    v
    liftCV AlgReal -> b
    _ Integer -> b
    _ Float -> b
    _ Double -> b
    _ FP -> b
    _ Rational -> b
    f Char -> b
    _ String -> b
    _ (Maybe Int, String) -> b
    _ [CVal] -> b
    _ RCSet CVal -> b
    _ [CVal] -> b
    _ Maybe CVal -> b
    _ Either CVal CVal -> b
    _ (CV Kind
    _ (CRational Rational
    v)) = Rational -> b
    f Rational
    v
    liftCV AlgReal -> b
    _ Integer -> b
    _ Float -> b
    _ Double -> b
    _ FP -> b
    _ Rational -> b
    _ Char -> b
    f String -> b
    _ (Maybe Int, String) -> b
    _ [CVal] -> b
    _ RCSet CVal -> b
    _ [CVal] -> b
    _ Maybe CVal -> b
    _ Either CVal CVal -> b
    _ (CV Kind
    _ (CChar     Char
    v)) = Char -> b
    f Char
    v
    liftCV AlgReal -> b
    _ Integer -> b
    _ Float -> b
    _ Double -> b
    _ FP -> b
    _ Rational -> b
    _ Char -> b
    _ String -> b
    f (Maybe Int, String) -> b
    _ [CVal] -> b
    _ RCSet CVal -> b
    _ [CVal] -> b
    _ Maybe CVal -> b
    _ Either CVal CVal -> b
    _ (CV Kind
    _ (CString   String
    v)) = String -> b
    f String
    v
    liftCV AlgReal -> b
    _ Integer -> b
    _ Float -> b
    _ Double -> b
    _ FP -> b
    _ Rational -> b
    _ Char -> b
    _ String -> b
    _ (Maybe Int, String) -> b
    f [CVal] -> b
    _ RCSet CVal -> b
    _ [CVal] -> b
    _ Maybe CVal -> b
    _ Either CVal CVal -> b
    _ (CV Kind
    _ (CUserSort (Maybe Int, String)
    v)) = (Maybe Int, String) -> b
    f (Maybe Int, String)
    v
    liftCV AlgReal -> b
    _ Integer -> b
    _ Float -> b
    _ Double -> b
    _ FP -> b
    _ Rational -> b
    _ Char -> b
    _ String -> b
    _ (Maybe Int, String) -> b
    _ [CVal] -> b
    f RCSet CVal -> b
    _ [CVal] -> b
    _ Maybe CVal -> b
    _ Either CVal CVal -> b
    _ (CV Kind
    _ (CList     [CVal]
    v)) = [CVal] -> b
    f [CVal]
    v
    liftCV AlgReal -> b
    _ Integer -> b
    _ Float -> b
    _ Double -> b
    _ FP -> b
    _ Rational -> b
    _ Char -> b
    _ String -> b
    _ (Maybe Int, String) -> b
    _ [CVal] -> b
    _ RCSet CVal -> b
    f [CVal] -> b
    _ Maybe CVal -> b
    _ Either CVal CVal -> b
    _ (CV Kind
    _ (CSet      RCSet CVal
    v)) = RCSet CVal -> b
    f RCSet CVal
    v
    liftCV AlgReal -> b
    _ Integer -> b
    _ Float -> b
    _ Double -> b
    _ FP -> b
    _ Rational -> b
    _ Char -> b
    _ String -> b
    _ (Maybe Int, String) -> b
    _ [CVal] -> b
    _ RCSet CVal -> b
    _ [CVal] -> b
    f Maybe CVal -> b
    _ Either CVal CVal -> b
    _ (CV Kind
    _ (CTuple    [CVal]
    v)) = [CVal] -> b
    f [CVal]
    v
    liftCV AlgReal -> b
    _ Integer -> b
    _ Float -> b
    _ Double -> b
    _ FP -> b
    _ Rational -> b
    _ Char -> b
    _ String -> b
    _ (Maybe Int, String) -> b
    _ [CVal] -> b
    _ RCSet CVal -> b
    _ [CVal] -> b
    _ Maybe CVal -> b
    f Either CVal CVal -> b
    _ (CV Kind
    _ (CMaybe    Maybe CVal
    v)) = Maybe CVal -> b
    f Maybe CVal
    v
    liftCV AlgReal -> b
    _ Integer -> b
    _ Float -> b
    _ Double -> b
    _ FP -> b
    _ Rational -> b
    _ Char -> b
    _ String -> b
    _ (Maybe Int, String) -> b
    _ [CVal] -> b
    _ RCSet CVal -> b
    _ [CVal] -> b
    _ Maybe CVal -> b
    _ Either CVal CVal -> b
    f (CV Kind
    _ (CEither   Either CVal CVal
    v)) = Either CVal CVal -> b
    f Either CVal CVal
    v

    -- | Lift a binary function through a 'CV'.
    liftCV2 :: (AlgReal             -> AlgReal             -> b)
            -> (Integer             -> Integer             -> b)
            -> (Float               -> Float               -> b)
            -> (Double              -> Double              -> b)
            -> (FP                  -> FP                  -> b)
            -> (Rational            -> Rational            -> b)
            -> (Char                -> Char                -> b)
            -> (String              -> String              -> b)
            -> ([CVal]              -> [CVal]              -> b)
            -> ([CVal]              -> [CVal]              -> b)
            -> (Maybe CVal          -> Maybe CVal          -> b)
            -> (Either CVal CVal    -> Either CVal CVal    -> b)
            -> ((Maybe Int, String) -> (Maybe Int, String) -> b)
            -> CV                   -> CV                  -> b
    liftCV2 :: forall b.
    (AlgReal -> AlgReal -> b)
    -> (Integer -> Integer -> b)
    -> (Float -> Float -> b)
    -> (Double -> Double -> b)
    -> (FP -> FP -> b)
    -> (Rational -> Rational -> b)
    -> (Char -> Char -> b)
    -> (String -> String -> b)
    -> ([CVal] -> [CVal] -> b)
    -> ([CVal] -> [CVal] -> b)
    -> (Maybe CVal -> Maybe CVal -> b)
    -> (Either CVal CVal -> Either CVal CVal -> b)
    -> ((Maybe Int, String) -> (Maybe Int, String) -> b)
    -> CV
    -> CV
    -> b
    liftCV2 AlgReal -> AlgReal -> b
    r Integer -> Integer -> b
    i Float -> Float -> b
    f Double -> Double -> b
    d FP -> FP -> b
    af Rational -> Rational -> b
    ra Char -> Char -> b
    c String -> String -> b
    s [CVal] -> [CVal] -> b
    u [CVal] -> [CVal] -> b
    v Maybe CVal -> Maybe CVal -> b
    m Either CVal CVal -> Either CVal CVal -> b
    e (Maybe Int, String) -> (Maybe Int, String) -> b
    w CV
    x CV
    y = case (CV -> CVal
    cvVal CV
    x, CV -> CVal
    cvVal CV
    y) of
                                               (CAlgReal   AlgReal
    a, CAlgReal   AlgReal
    b) -> AlgReal -> AlgReal -> b
    r  AlgReal
    a AlgReal
    b
                                               (CInteger   Integer
    a, CInteger   Integer
    b) -> Integer -> Integer -> b
    i  Integer
    a Integer
    b
                                               (CFloat     Float
    a, CFloat     Float
    b) -> Float -> Float -> b
    f  Float
    a Float
    b
                                               (CDouble    Double
    a, CDouble    Double
    b) -> Double -> Double -> b
    d  Double
    a Double
    b
                                               (CFP        FP
    a, CFP        FP
    b) -> FP -> FP -> b
    af FP
    a FP
    b
                                               (CRational  Rational
    a, CRational  Rational
    b) -> Rational -> Rational -> b
    ra Rational
    a Rational
    b
                                               (CChar      Char
    a, CChar      Char
    b) -> Char -> Char -> b
    c  Char
    a Char
    b
                                               (CString    String
    a, CString    String
    b) -> String -> String -> b
    s  String
    a String
    b
                                               (CList      [CVal]
    a, CList      [CVal]
    b) -> [CVal] -> [CVal] -> b
    u  [CVal]
    a [CVal]
    b
                                               (CTuple     [CVal]
    a, CTuple     [CVal]
    b) -> [CVal] -> [CVal] -> b
    v  [CVal]
    a [CVal]
    b
                                               (CMaybe     Maybe CVal
    a, CMaybe     Maybe CVal
    b) -> Maybe CVal -> Maybe CVal -> b
    m  Maybe CVal
    a Maybe CVal
    b
                                               (CEither    Either CVal CVal
    a, CEither    Either CVal CVal
    b) -> Either CVal CVal -> Either CVal CVal -> b
    e  Either CVal CVal
    a Either CVal CVal
    b
                                               (CUserSort  (Maybe Int, String)
    a, CUserSort  (Maybe Int, String)
    b) -> (Maybe Int, String) -> (Maybe Int, String) -> b
    w  (Maybe Int, String)
    a (Maybe Int, String)
    b
                                               (CVal, CVal)
    _                            -> String -> b
    forall a. HasCallStack => String -> a
    error (String -> b) -> String -> b
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.liftCV2: impossible, incompatible args received: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (CV, CV) -> String
    forall a. Show a => a -> String
    show (CV
    x, CV
    y)

    -- | Map a unary function through a 'CV'.
    mapCV :: (AlgReal             -> AlgReal)
          -> (Integer             -> Integer)
          -> (Float               -> Float)
          -> (Double              -> Double)
          -> (FP                  -> FP)
          -> (Rational            -> Rational)
          -> (Char                -> Char)
          -> (String              -> String)
          -> ((Maybe Int, String) -> (Maybe Int, String))
          -> CV
          -> CV
    mapCV :: (AlgReal -> AlgReal)
    -> (Integer -> Integer)
    -> (Float -> Float)
    -> (Double -> Double)
    -> (FP -> FP)
    -> (Rational -> Rational)
    -> (Char -> Char)
    -> ShowS
    -> ((Maybe Int, String) -> (Maybe Int, String))
    -> CV
    -> CV
    mapCV AlgReal -> AlgReal
    r Integer -> Integer
    i Float -> Float
    f Double -> Double
    d FP -> FP
    af Rational -> Rational
    ra Char -> Char
    c ShowS
    s (Maybe Int, String) -> (Maybe Int, String)
    u 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     Char
    a -> Char -> CVal
    CChar     (Char -> Char
    c  Char
    a)
                                                              CString   String
    a -> String -> CVal
    CString   (ShowS
    s  String
    a)
                                                              CUserSort (Maybe Int, String)
    a -> (Maybe Int, String) -> CVal
    CUserSort ((Maybe Int, String) -> (Maybe Int, String)
    u  (Maybe Int, String)
    a)
                                                              CList{}     -> String -> CVal
    forall a. HasCallStack => String -> a
    error 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!"

    -- | Map a binary function through a 'CV'.
    mapCV2 :: (AlgReal             -> AlgReal             -> AlgReal)
           -> (Integer             -> Integer             -> Integer)
           -> (Float               -> Float               -> Float)
           -> (Double              -> Double              -> Double)
           -> (FP                  -> FP                  -> FP)
           -> (Rational            -> Rational            -> Rational)
           -> (Char                -> Char                -> Char)
           -> (String              -> String              -> String)
           -> ((Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String))
           -> CV
           -> CV
           -> CV
    mapCV2 :: (AlgReal -> AlgReal -> AlgReal)
    -> (Integer -> Integer -> Integer)
    -> (Float -> Float -> Float)
    -> (Double -> Double -> Double)
    -> (FP -> FP -> FP)
    -> (Rational -> Rational -> Rational)
    -> (Char -> Char -> Char)
    -> (String -> ShowS)
    -> ((Maybe Int, String)
        -> (Maybe Int, String) -> (Maybe Int, String))
    -> 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 Char -> Char -> Char
    c String -> ShowS
    s (Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String)
    u 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     Char
    a, CChar     Char
    b) -> CV -> CV
    normCV (CV -> CV) -> CV -> CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV (CV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf CV
    x) (Char -> CVal
    CChar     (Char -> Char -> Char
    c  Char
    a Char
    b))
                                      (Bool
    True, CString   String
    a, CString   String
    b) -> CV -> CV
    normCV (CV -> CV) -> CV -> CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV (CV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf CV
    x) (String -> CVal
    CString   (String -> ShowS
    s  String
    a String
    b))
                                      (Bool
    True, CUserSort (Maybe Int, String)
    a, CUserSort (Maybe Int, String)
    b) -> CV -> CV
    normCV (CV -> CV) -> CV -> CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV (CV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf CV
    x) ((Maybe Int, String) -> CVal
    CUserSort ((Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String)
    u  (Maybe Int, String)
    a (Maybe Int, String)
    b))
                                      (Bool
    True, CList{},     CList{})     -> String -> CV
    forall a. HasCallStack => String -> a
    error String
    "Data.SBV.mapCV2: Unexpected call through mapCV2 with lists!"
                                      (Bool
    True, CTuple{},    CTuple{})    -> String -> CV
    forall a. HasCallStack => String -> a
    error String
    "Data.SBV.mapCV2: Unexpected call through mapCV2 with tuples!"
                                      (Bool
    True, CMaybe{},    CMaybe{})    -> String -> CV
    forall a. HasCallStack => String -> a
    error String
    "Data.SBV.mapCV2: Unexpected call through mapCV2 with maybes!"
                                      (Bool
    True, CEither{},   CEither{})   -> String -> CV
    forall a. HasCallStack => String -> a
    error String
    "Data.SBV.mapCV2: Unexpected call through mapCV2 with eithers!"
                                      (Bool, CVal, CVal)
    _                                -> String -> CV
    forall a. HasCallStack => String -> a
    error (String -> CV) -> String -> CV
    forall a b. (a -> b) -> a -> b
    $ String
    "Data.SBV.mapCV2: impossible, incompatible args received: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (CV, CV) -> String
    forall a. Show a => a -> String
    show (CV
    x, CV
    y)

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

    -- | Show instance for Generalized 'CV'
    instance Show GeneralizedCV where
      show :: GeneralizedCV -> String
    show (ExtendedCV 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               = (AlgReal -> String)
    -> (Integer -> String)
    -> (Float -> String)
    -> (Double -> String)
    -> (FP -> String)
    -> (Rational -> String)
    -> (Char -> String)
    -> ShowS
    -> ((Maybe Int, String) -> String)
    -> ([CVal] -> String)
    -> (RCSet CVal -> String)
    -> ([CVal] -> String)
    -> (Maybe CVal -> String)
    -> (Either CVal CVal -> String)
    -> CV
    -> String
    forall b.
    (AlgReal -> b)
    -> (Integer -> b)
    -> (Float -> b)
    -> (Double -> b)
    -> (FP -> b)
    -> (Rational -> b)
    -> (Char -> b)
    -> (String -> b)
    -> ((Maybe Int, String) -> b)
    -> ([CVal] -> b)
    -> (RCSet CVal -> b)
    -> ([CVal] -> b)
    -> (Maybe CVal -> b)
    -> (Either CVal CVal -> b)
    -> CV
    -> b
    liftCV AlgReal -> String
    forall a. Show a => a -> String
    show Integer -> String
    forall a. Show a => a -> String
    show Float -> String
    forall a. Show a => a -> String
    show Double -> String
    forall a. Show a => a -> String
    show FP -> String
    forall a. Show a => a -> String
    show Rational -> String
    forall a. Show a => a -> String
    show Char -> String
    forall a. Show a => a -> String
    show ShowS
    forall a. Show a => a -> String
    show (Maybe Int, String) -> String
    forall a b. (a, b) -> b
    snd [CVal] -> String
    shL RCSet CVal -> String
    shS [CVal] -> String
    shT Maybe CVal -> String
    shMaybe Either CVal CVal -> String
    shEither CV
    w String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    kInfo
          where kw :: Kind
    kw = CV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf CV
    w

                kInfo :: String
    kInfo | Bool
    shk  = String
    " :: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    showBaseKind Kind
    kw
                      | Bool
    True = String
    ""

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

                -- 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
    sh 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
    sh Set CVal
    e
                  where sh :: Set CVal -> String
    sh 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
    kw 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
    kw

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

                shMaybe :: Maybe CVal -> String
                shMaybe :: Maybe CVal -> String
    shMaybe Maybe CVal
    c = case (Maybe CVal
    c, Kind
    kw) 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
    kw

                shEither :: Either CVal CVal -> String
                shEither :: Either CVal CVal -> String
    shEither Either CVal CVal
    val
                  | KEither Kind
    k1 Kind
    k2 <- Kind
    kw = 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
    kw

                -- 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 -> 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{}         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       (Integer -> FP
    forall a. Num a => Integer -> a
    fromInteger (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)

    -- | Generate a random constant value ('CVal') of the correct kind.
    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 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)
        KUserSort String
    s 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
    "Unexpected call to randomCVal with user kind: " 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
        KMaybe Kind
    ke          -> do Bool
    i <- IO Bool
    forall a (m :: * -> *). (Random a, MonadIO m) => m a
    randomIO
                                 if Bool
    i
                                    then 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
    $ Maybe CVal -> CVal
    CMaybe Maybe CVal
    forall a. Maybe a
    Nothing
                                    else Maybe CVal -> CVal
    CMaybe (Maybe CVal -> CVal) -> (CVal -> Maybe CVal) -> CVal -> CVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CVal -> Maybe CVal
    forall a. a -> Maybe a
    Just (CVal -> CVal) -> IO CVal -> IO CVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Kind -> IO CVal
    randomCVal Kind
    ke
        KEither Kind
    k1 Kind
    k2      -> do Bool
    i <- IO Bool
    forall a (m :: * -> *). (Random a, MonadIO m) => m a
    randomIO
                                 if Bool
    i
                                    then Either CVal CVal -> CVal
    CEither (Either CVal CVal -> CVal)
    -> (CVal -> Either CVal CVal) -> CVal -> CVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CVal -> Either CVal CVal
    forall a b. a -> Either a b
    Left  (CVal -> CVal) -> IO CVal -> IO CVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Kind -> IO CVal
    randomCVal Kind
    k1
                                    else Either CVal CVal -> CVal
    CEither (Either CVal CVal -> CVal)
    -> (CVal -> Either CVal CVal) -> CVal -> CVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CVal -> Either CVal CVal
    forall a b. b -> Either a b
    Right (CVal -> CVal) -> IO CVal -> IO CVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Kind -> IO CVal
    randomCVal Kind
    k2
      where
        bounds :: Bool -> Int -> (Integer, Integer)
        bounds :: Bool -> Int -> (Integer, Integer)
    bounds 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 ('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" -}