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

    {-# OPTIONS_GHC -Wall -Werror #-}

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

    import Control.Monad (replicateM)

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

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

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

    import Data.Proxy

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

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

    -- | 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 rcs :: RCSet a
    rcs = case RCSet a
    rcs of
                   ComplementSet s :: Set a
    s | Set a -> Bool
    forall a. Set a -> Bool
    Set.null Set a
    s -> "U"
                                   | Bool
    True       -> "U - " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [a] -> String
    forall a. Show a => [a] -> String
    sh (Set a -> [a]
    forall a. Set a -> [a]
    Set.toAscList Set a
    s)
                   RegularSet    s :: Set a
    s              ->           [a] -> String
    forall a. Show a => [a] -> String
    sh (Set a -> [a]
    forall a. Set a -> [a]
    Set.toAscList Set a
    s)
       where sh :: [a] -> String
    sh xs :: [a]
    xs = '{' Char -> ShowS
    forall a. a -> [a] -> [a]
    : String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate "," ((a -> String) -> [a] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> String
    forall a. Show a => a -> String
    show [a]
    xs) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "}"

    -- | 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 :: RCSet a -> RCSet a -> Bool
    eqRCSet (RegularSet    a :: Set a
    a) (RegularSet    b :: Set a
    b) = Set a
    a Set a -> Set a -> Bool
    forall a. Eq a => a -> a -> Bool
    == Set a
    b
    eqRCSet (ComplementSet a :: Set a
    a) (ComplementSet b :: Set a
    b) = Set a
    a Set a -> Set a -> Bool
    forall a. Eq a => a -> a -> Bool
    == Set a
    b
    eqRCSet _                 _                 = Bool
    False

    -- | 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 :: RCSet a -> RCSet a -> Ordering
    compareRCSet (RegularSet    a :: Set a
    a) (RegularSet    b :: Set a
    b) = Set a
    a Set a -> Set a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare` Set a
    b
    compareRCSet (RegularSet    _) (ComplementSet _) = Ordering
    LT
    compareRCSet (ComplementSet _) (RegularSet    _) = Ordering
    GT
    compareRCSet (ComplementSet a :: Set a
    a) (ComplementSet b :: Set a
    b) = Set a
    a Set a -> Set a -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare` Set a
    b

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

    -- | A constant value
    data CVal = CAlgReal  !AlgReal              -- ^ Algebraic real
              | CInteger  !Integer              -- ^ Bit-vector/unbounded integer
              | CFloat    !Float                -- ^ Float
              | CDouble   !Double               -- ^ Double
              | 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

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

    -- | 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  a :: AlgReal
    a == :: CVal -> CVal -> Bool
    == CAlgReal  b :: AlgReal
    b = AlgReal
    a AlgReal -> AlgReal -> Bool
    `algRealStructuralEqual` AlgReal
    b
      CInteger  a :: Integer
    a == CInteger  b :: Integer
    b = Integer
    a Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    b
      CFloat    a :: Float
    a == CFloat    b :: Float
    b = Float
    a Float -> Float -> Bool
    forall a. RealFloat a => a -> a -> Bool
    `fpIsEqualObjectH` Float
    b   -- We don't want +0/-0 to be confused; and also we want NaN = NaN here!
      CDouble   a :: Double
    a == CDouble   b :: Double
    b = Double
    a Double -> Double -> Bool
    forall a. RealFloat a => a -> a -> Bool
    `fpIsEqualObjectH` Double
    b   -- ditto
      CChar     a :: Char
    a == CChar     b :: Char
    b = Char
    a Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    b
      CString   a :: String
    a == CString   b :: String
    b = String
    a String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    b
      CList     a :: [CVal]
    a == CList     b :: [CVal]
    b = [CVal]
    a [CVal] -> [CVal] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [CVal]
    b
      CSet      a :: RCSet CVal
    a == CSet      b :: RCSet CVal
    b = RCSet CVal
    a RCSet CVal -> RCSet CVal -> Bool
    forall a. Eq a => RCSet a -> RCSet a -> Bool
    `eqRCSet` RCSet CVal
    b
      CUserSort a :: (Maybe Int, String)
    a == CUserSort b :: (Maybe Int, String)
    b = (Maybe Int, String)
    a (Maybe Int, String) -> (Maybe Int, String) -> Bool
    forall a. Eq a => a -> a -> Bool
    == (Maybe Int, String)
    b
      CTuple    a :: [CVal]
    a == CTuple    b :: [CVal]
    b = [CVal]
    a [CVal] -> [CVal] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [CVal]
    b
      CMaybe    a :: Maybe CVal
    a == CMaybe    b :: Maybe CVal
    b = Maybe CVal
    a Maybe CVal -> Maybe CVal -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe CVal
    b
      CEither   a :: Either CVal CVal
    a == CEither   b :: Either CVal CVal
    b = Either CVal CVal
    a Either CVal CVal -> Either CVal CVal -> Bool
    forall a. Eq a => a -> a -> Bool
    == Either CVal CVal
    b
      a :: CVal
    a           == b :: CVal
    b           = if CVal -> Int
    cvRank CVal
    a Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == CVal -> Int
    cvRank CVal
    b
                                      then String -> Bool
    forall a. HasCallStack => String -> a
    error (String -> Bool) -> String -> Bool
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ ""
                                                           , "*** Data.SBV.Eq.CVal: Impossible happened: same rank in comparison fallthru"
                                                           , "***"
                                                           , "***   Received: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (Int, Int) -> String
    forall a. Show a => a -> String
    show (CVal -> Int
    cvRank CVal
    a, CVal -> Int
    cvRank CVal
    b)
                                                           , "***"
                                                           , "*** Please report this as a bug!"
                                                           ]
                                      else Bool
    False

    -- | Ord instance for VWVal. Same comments as the 'Eq' instance why this cannot be derived.
    instance Ord CVal where
      CAlgReal  a :: AlgReal
    a compare :: CVal -> CVal -> Ordering
    `compare` CAlgReal b :: AlgReal
    b  = AlgReal
    a        AlgReal -> AlgReal -> Ordering
    `algRealStructuralCompare` AlgReal
    b
      CInteger  a :: Integer
    a `compare` CInteger b :: Integer
    b  = Integer
    a        Integer -> Integer -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare`                  Integer
    b
      CFloat    a :: Float
    a `compare` CFloat b :: Float
    b    = Float
    a        Float -> Float -> Ordering
    forall a. RealFloat a => a -> a -> Ordering
    `fpCompareObjectH`         Float
    b
      CDouble   a :: Double
    a `compare` CDouble b :: Double
    b   = Double
    a        Double -> Double -> Ordering
    forall a. RealFloat a => a -> a -> Ordering
    `fpCompareObjectH`         Double
    b
      CChar     a :: Char
    a `compare` CChar b :: Char
    b     = Char
    a        Char -> Char -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare`                  Char
    b
      CString   a :: String
    a `compare` CString b :: String
    b   = String
    a        String -> String -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare`                  String
    b
      CList     a :: [CVal]
    a `compare` CList   b :: [CVal]
    b   = [CVal]
    a        [CVal] -> [CVal] -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare`                  [CVal]
    b
      CSet      a :: RCSet CVal
    a `compare` CSet    b :: RCSet CVal
    b   = RCSet CVal
    a        RCSet CVal -> RCSet CVal -> Ordering
    forall a. Ord a => RCSet a -> RCSet a -> Ordering
    `compareRCSet`             RCSet CVal
    b
      CUserSort a :: (Maybe Int, String)
    a `compare` CUserSort b :: (Maybe Int, String)
    b = (Maybe Int, String)
    a        (Maybe Int, String) -> (Maybe Int, String) -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare`                  (Maybe Int, String)
    b
      CTuple    a :: [CVal]
    a `compare` CTuple    b :: [CVal]
    b = [CVal]
    a        [CVal] -> [CVal] -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare`                  [CVal]
    b
      CMaybe    a :: Maybe CVal
    a `compare` CMaybe    b :: Maybe CVal
    b = Maybe CVal
    a        Maybe CVal -> Maybe CVal -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare`                  Maybe CVal
    b
      CEither   a :: Either CVal CVal
    a `compare` CEither   b :: Either CVal CVal
    b = Either CVal CVal
    a        Either CVal CVal -> Either CVal CVal -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare`                  Either CVal CVal
    b
      a :: CVal
    a           `compare` b :: CVal
    b           = let ra :: Int
    ra = CVal -> Int
    cvRank CVal
    a
                                              rb :: Int
    rb = CVal -> Int
    cvRank CVal
    b
                                          in if Int
    ra Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    rb
                                                then String -> Ordering
    forall a. HasCallStack => String -> a
    error (String -> Ordering) -> String -> Ordering
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unlines [ ""
                                                                     , "*** Data.SBV.Ord.CVal: Impossible happened: same rank in comparison fallthru"
                                                                     , "***"
                                                                     , "***   Received: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (Int, Int) -> String
    forall a. Show a => a -> String
    show (Int
    ra, Int
    rb)
                                                                     , "***"
                                                                     , "*** Please report this as a bug!"
                                                                     ]
                                                else CVal -> Int
    cvRank CVal
    a Int -> Int -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare` CVal -> Int
    cvRank CVal
    b

    -- | '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
    /= :: CV -> CV -> Bool
    $c/= :: CV -> CV -> Bool
    == :: CV -> CV -> Bool
    $c== :: CV -> CV -> Bool
    Eq, Eq CV
    Eq CV =>
    (CV -> CV -> Ordering)
    -> (CV -> CV -> Bool)
    -> (CV -> CV -> Bool)
    -> (CV -> CV -> Bool)
    -> (CV -> CV -> Bool)
    -> (CV -> CV -> CV)
    -> (CV -> CV -> CV)
    -> Ord CV
    CV -> CV -> Bool
    CV -> CV -> Ordering
    CV -> CV -> CV
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: CV -> CV -> CV
    $cmin :: CV -> CV -> CV
    max :: CV -> CV -> CV
    $cmax :: CV -> CV -> CV
    >= :: CV -> CV -> Bool
    $c>= :: CV -> CV -> Bool
    > :: CV -> CV -> Bool
    $c> :: CV -> CV -> Bool
    <= :: CV -> CV -> Bool
    $c<= :: CV -> CV -> Bool
    < :: CV -> CV -> Bool
    $c< :: CV -> CV -> Bool
    compare :: CV -> CV -> Ordering
    $ccompare :: CV -> CV -> Ordering
    $cp1Ord :: Eq CV
    Ord)

    -- | 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 extendent 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  k :: Kind
    k)   = Kind
    k
      kindOf (Epsilon   k :: Kind
    k)   = Kind
    k
      kindOf (Interval  l :: ExtCV
    l _) = ExtCV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf ExtCV
    l
      kindOf (BoundedCV  c :: CV
    c)  = CV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf CV
    c
      kindOf (AddExtCV  l :: ExtCV
    l _) = ExtCV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf ExtCV
    l
      kindOf (MulExtCV  l :: ExtCV
    l _) = ExtCV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf ExtCV
    l

    -- | 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 parens :: Bool
    parens shk :: Bool
    shk extCV :: ExtCV
    extCV = case ExtCV
    extCV of
                                    Infinite{}    -> Bool -> ShowS
    withKind Bool
    False "oo"
                                    Epsilon{}     -> Bool -> ShowS
    withKind Bool
    False "epsilon"
                                    Interval  l :: ExtCV
    l u :: ExtCV
    u -> Bool -> ShowS
    withKind Bool
    True  ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ '['  Char -> ShowS
    forall a. a -> [a] -> [a]
    : Bool -> ExtCV -> String
    showExtCV Bool
    False ExtCV
    l String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " .. " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Bool -> ExtCV -> String
    showExtCV Bool
    False ExtCV
    u String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "]"
                                    BoundedCV c :: CV
    c   -> Bool -> CV -> String
    showCV Bool
    shk CV
    c
                                    AddExtCV l :: ExtCV
    l r :: ExtCV
    r  -> ShowS
    par ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ Bool -> ShowS
    withKind Bool
    False ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ String -> ShowS
    add (Bool -> Bool -> ExtCV -> String
    go Bool
    True Bool
    False ExtCV
    l) (Bool -> Bool -> ExtCV -> String
    go Bool
    True Bool
    False ExtCV
    r)

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

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

                     add :: String -> String -> String
                     add :: String -> ShowS
    add n :: String
    n v :: String
    v
                      | "-" String -> String -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isPrefixOf` String
    v = String
    n String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " - " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. [a] -> [a]
    tail String
    v
                      | Bool
    True               = String
    n String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " + " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    v

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

    -- | 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 k :: Kind
    k _) = Kind
    k

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

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

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

    -- | 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 signed :: Bool
    signed sz :: Int
    sz) (CInteger v :: Integer
    v)) = CV
    c { cvVal :: CVal
    cvVal = Integer -> CVal
    CInteger Integer
    norm }
     where norm :: Integer
    norm | Int
    sz Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 0 = 0
                | Bool
    signed  = let rg :: Integer
    rg = 2 Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ (Int
    sz Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1)
                            in case Integer -> Integer -> (Integer, Integer)
    forall a. Integral a => a -> a -> (a, a)
    divMod Integer
    v Integer
    rg of
                                      (a :: Integer
    a, b :: Integer
    b) | Integer -> Bool
    forall a. Integral a => a -> Bool
    even Integer
    a -> Integer
    b
                                      (_, b :: Integer
    b)          -> Integer
    b Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    rg
                | Bool
    True    = Integer
    v Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` (2 Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Int
    sz)
    normCV c :: CV
    c@(CV KBool (CInteger v :: Integer
    v)) = CV
    c { cvVal :: CVal
    cvVal = Integer -> CVal
    CInteger (Integer
    v Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .&. 1) }
    normCV c :: CV
    c                         = CV
    c

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

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

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

    -- | Map a unary function through a 'CV'.
    mapCV :: (AlgReal             -> AlgReal)
          -> (Integer             -> Integer)
          -> (Float               -> Float)
          -> (Double              -> Double)
          -> (Char                -> Char)
          -> (String              -> String)
          -> ((Maybe Int, String) -> (Maybe Int, String))
          -> CV
          -> CV
    mapCV :: (AlgReal -> AlgReal)
    -> (Integer -> Integer)
    -> (Float -> Float)
    -> (Double -> Double)
    -> (Char -> Char)
    -> ShowS
    -> ((Maybe Int, String) -> (Maybe Int, String))
    -> CV
    -> CV
    mapCV r :: AlgReal -> AlgReal
    r i :: Integer -> Integer
    i f :: Float -> Float
    f d :: Double -> Double
    d c :: Char -> Char
    c s :: ShowS
    s u :: (Maybe Int, String) -> (Maybe Int, String)
    u x :: CV
    x  = CV -> CV
    normCV (CV -> CV) -> CV -> CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV (CV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf CV
    x) (CVal -> CV) -> CVal -> CV
    forall a b. (a -> b) -> a -> b
    $ case CV -> CVal
    cvVal CV
    x of
                                                        CAlgReal  a :: AlgReal
    a -> AlgReal -> CVal
    CAlgReal  (AlgReal -> AlgReal
    r AlgReal
    a)
                                                        CInteger  a :: Integer
    a -> Integer -> CVal
    CInteger  (Integer -> Integer
    i Integer
    a)
                                                        CFloat    a :: Float
    a -> Float -> CVal
    CFloat    (Float -> Float
    f Float
    a)
                                                        CDouble   a :: Double
    a -> Double -> CVal
    CDouble   (Double -> Double
    d Double
    a)
                                                        CChar     a :: Char
    a -> Char -> CVal
    CChar     (Char -> Char
    c Char
    a)
                                                        CString   a :: String
    a -> String -> CVal
    CString   (ShowS
    s String
    a)
                                                        CUserSort a :: (Maybe Int, String)
    a -> (Maybe Int, String) -> CVal
    CUserSort ((Maybe Int, String) -> (Maybe Int, String)
    u (Maybe Int, String)
    a)
                                                        CList{}     -> String -> CVal
    forall a. HasCallStack => String -> a
    error "Data.SBV.mapCV: Unexpected call through mapCV with lists!"
                                                        CSet{}      -> String -> CVal
    forall a. HasCallStack => String -> a
    error "Data.SBV.mapCV: Unexpected call through mapCV with sets!"
                                                        CTuple{}    -> String -> CVal
    forall a. HasCallStack => String -> a
    error "Data.SBV.mapCV: Unexpected call through mapCV with tuples!"
                                                        CMaybe{}    -> String -> CVal
    forall a. HasCallStack => String -> a
    error "Data.SBV.mapCV: Unexpected call through mapCV with maybe!"
                                                        CEither{}   -> String -> CVal
    forall a. HasCallStack => String -> a
    error "Data.SBV.mapCV: Unexpected call through mapCV with either!"

    -- | Map a binary function through a 'CV'.
    mapCV2 :: (AlgReal             -> AlgReal             -> AlgReal)
           -> (Integer             -> Integer             -> Integer)
           -> (Float               -> Float               -> Float)
           -> (Double              -> Double              -> Double)
           -> (Char                -> Char                -> Char)
           -> (String              -> String              -> String)
           -> ((Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String))
           -> CV
           -> CV
           -> CV
    mapCV2 :: (AlgReal -> AlgReal -> AlgReal)
    -> (Integer -> Integer -> Integer)
    -> (Float -> Float -> Float)
    -> (Double -> Double -> Double)
    -> (Char -> Char -> Char)
    -> (String -> ShowS)
    -> ((Maybe Int, String)
        -> (Maybe Int, String) -> (Maybe Int, String))
    -> CV
    -> CV
    -> CV
    mapCV2 r :: AlgReal -> AlgReal -> AlgReal
    r i :: Integer -> Integer -> Integer
    i f :: Float -> Float -> Float
    f d :: Double -> Double -> Double
    d c :: Char -> Char -> Char
    c s :: String -> ShowS
    s u :: (Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String)
    u x :: CV
    x y :: CV
    y = case (CV -> CV -> Bool
    cvSameType CV
    x CV
    y, CV -> CVal
    cvVal CV
    x, CV -> CVal
    cvVal CV
    y) of
                                (True, CAlgReal  a :: AlgReal
    a, CAlgReal  b :: AlgReal
    b) -> CV -> CV
    normCV (CV -> CV) -> CV -> CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV (CV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf CV
    x) (AlgReal -> CVal
    CAlgReal  (AlgReal -> AlgReal -> AlgReal
    r AlgReal
    a AlgReal
    b))
                                (True, CInteger  a :: Integer
    a, CInteger  b :: Integer
    b) -> CV -> CV
    normCV (CV -> CV) -> CV -> CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV (CV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf CV
    x) (Integer -> CVal
    CInteger  (Integer -> Integer -> Integer
    i Integer
    a Integer
    b))
                                (True, CFloat    a :: Float
    a, CFloat    b :: Float
    b) -> CV -> CV
    normCV (CV -> CV) -> CV -> CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV (CV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf CV
    x) (Float -> CVal
    CFloat    (Float -> Float -> Float
    f Float
    a Float
    b))
                                (True, CDouble   a :: Double
    a, CDouble   b :: Double
    b) -> CV -> CV
    normCV (CV -> CV) -> CV -> CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV (CV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf CV
    x) (Double -> CVal
    CDouble   (Double -> Double -> Double
    d Double
    a Double
    b))
                                (True, CChar     a :: Char
    a, CChar     b :: Char
    b) -> CV -> CV
    normCV (CV -> CV) -> CV -> CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV (CV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf CV
    x) (Char -> CVal
    CChar     (Char -> Char -> Char
    c Char
    a Char
    b))
                                (True, CString   a :: String
    a, CString   b :: String
    b) -> CV -> CV
    normCV (CV -> CV) -> CV -> CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV (CV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf CV
    x) (String -> CVal
    CString   (String -> ShowS
    s String
    a String
    b))
                                (True, CUserSort a :: (Maybe Int, String)
    a, CUserSort b :: (Maybe Int, String)
    b) -> CV -> CV
    normCV (CV -> CV) -> CV -> CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV (CV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf CV
    x) ((Maybe Int, String) -> CVal
    CUserSort ((Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String)
    u (Maybe Int, String)
    a (Maybe Int, String)
    b))
                                (True, CList{},     CList{})     -> String -> CV
    forall a. HasCallStack => String -> a
    error "Data.SBV.mapCV2: Unexpected call through mapCV2 with lists!"
                                (True, CTuple{},    CTuple{})    -> String -> CV
    forall a. HasCallStack => String -> a
    error "Data.SBV.mapCV2: Unexpected call through mapCV2 with tuples!"
                                (True, CMaybe{},    CMaybe{})    -> String -> CV
    forall a. HasCallStack => String -> a
    error "Data.SBV.mapCV2: Unexpected call through mapCV2 with maybes!"
                                (True, CEither{},   CEither{})   -> String -> CV
    forall a. HasCallStack => String -> a
    error "Data.SBV.mapCV2: Unexpected call through mapCV2 with eithers!"
                                _                                -> String -> CV
    forall a. HasCallStack => String -> a
    error (String -> CV) -> String -> CV
    forall a b. (a -> b) -> a -> b
    $ "SBV.mapCV2: impossible, incompatible args received: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (CV, CV) -> String
    forall a. Show a => a -> String
    show (CV
    x, CV
    y)

    -- | 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 k :: ExtCV
    k) = Bool -> ExtCV -> String
    showExtCV Bool
    True ExtCV
    k
      show (RegularCV  c :: 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 shk :: Bool
    shk w :: CV
    w | CV -> Bool
    forall a. HasKind a => a -> Bool
    isBoolean CV
    w = Bool -> String
    forall a. Show a => a -> String
    show (CV -> Bool
    cvToBool CV
    w) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (if Bool
    shk then " :: Bool" else "")
    showCV shk :: Bool
    shk w :: CV
    w               = (AlgReal -> String)
    -> (Integer -> String)
    -> (Float -> String)
    -> (Double -> String)
    -> (Char -> String)
    -> ShowS
    -> ((Maybe Int, String) -> String)
    -> ([CVal] -> String)
    -> (RCSet CVal -> String)
    -> ([CVal] -> String)
    -> (Maybe CVal -> String)
    -> (Either CVal CVal -> String)
    -> CV
    -> String
    forall b.
    (AlgReal -> b)
    -> (Integer -> b)
    -> (Float -> b)
    -> (Double -> b)
    -> (Char -> b)
    -> (String -> b)
    -> ((Maybe Int, String) -> b)
    -> ([CVal] -> b)
    -> (RCSet CVal -> b)
    -> ([CVal] -> b)
    -> (Maybe CVal -> b)
    -> (Either CVal CVal -> b)
    -> CV
    -> b
    liftCV AlgReal -> String
    forall a. Show a => a -> String
    show Integer -> String
    forall a. Show a => a -> String
    show Float -> String
    forall a. Show a => a -> String
    show Double -> String
    forall a. Show a => a -> String
    show Char -> String
    forall a. Show a => a -> String
    show ShowS
    forall a. Show a => a -> String
    show (Maybe Int, String) -> String
    forall a b. (a, b) -> b
    snd [CVal] -> String
    shL RCSet CVal -> String
    shS [CVal] -> String
    shT Maybe CVal -> String
    shMaybe Either CVal CVal -> String
    shEither CV
    w String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    kInfo
          where kw :: Kind
    kw = CV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf CV
    w

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

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

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

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

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

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

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

    -- | Create a constant word from an integral.
    mkConstCV :: Integral a => Kind -> a -> CV
    mkConstCV :: Kind -> a -> CV
    mkConstCV KBool                a :: a
    a = CV -> CV
    normCV (CV -> CV) -> CV -> CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    KBool      (Integer -> CVal
    CInteger (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    a))
    mkConstCV k :: Kind
    k@KBounded{}         a :: a
    a = CV -> CV
    normCV (CV -> CV) -> CV -> CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    k          (Integer -> CVal
    CInteger (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    a))
    mkConstCV KUnbounded           a :: a
    a = CV -> CV
    normCV (CV -> CV) -> CV -> CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    KUnbounded (Integer -> CVal
    CInteger (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    a))
    mkConstCV KReal                a :: a
    a = CV -> CV
    normCV (CV -> CV) -> CV -> CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    KReal      (AlgReal -> CVal
    CAlgReal (Integer -> AlgReal
    forall a. Num a => Integer -> a
    fromInteger (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    a)))
    mkConstCV KFloat               a :: a
    a = CV -> CV
    normCV (CV -> CV) -> CV -> CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    KFloat     (Float -> CVal
    CFloat   (Integer -> Float
    forall a. Num a => Integer -> a
    fromInteger (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    a)))
    mkConstCV KDouble              a :: a
    a = CV -> CV
    normCV (CV -> CV) -> CV -> CV
    forall a b. (a -> b) -> a -> b
    $ Kind -> CVal -> CV
    CV Kind
    KDouble    (Double -> CVal
    CDouble  (Integer -> Double
    forall a. Num a => Integer -> a
    fromInteger (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    a)))
    mkConstCV KChar                a :: a
    a = String -> CV
    forall a. HasCallStack => String -> a
    error (String -> CV) -> String -> CV
    forall a b. (a -> b) -> a -> b
    $ "Unexpected call to mkConstCV (Char) with value: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    a)
    mkConstCV KString              a :: a
    a = String -> CV
    forall a. HasCallStack => String -> a
    error (String -> CV) -> String -> CV
    forall a b. (a -> b) -> a -> b
    $ "Unexpected call to mkConstCV (String) with value: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    a)
    mkConstCV (KUninterpreted s :: String
    s _) a :: a
    a = String -> CV
    forall a. HasCallStack => String -> a
    error (String -> CV) -> String -> CV
    forall a b. (a -> b) -> a -> b
    $ "Unexpected call to mkConstCV with uninterpreted kind: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ " with value: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    a)
    mkConstCV k :: Kind
    k@KList{}            a :: a
    a = String -> CV
    forall a. HasCallStack => String -> a
    error (String -> CV) -> String -> CV
    forall a b. (a -> b) -> a -> b
    $ "Unexpected call to mkConstCV (" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ") with value: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    a)
    mkConstCV k :: Kind
    k@KSet{}             a :: a
    a = String -> CV
    forall a. HasCallStack => String -> a
    error (String -> CV) -> String -> CV
    forall a b. (a -> b) -> a -> b
    $ "Unexpected call to mkConstCV (" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ") with value: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    a)
    mkConstCV k :: Kind
    k@KTuple{}           a :: a
    a = String -> CV
    forall a. HasCallStack => String -> a
    error (String -> CV) -> String -> CV
    forall a b. (a -> b) -> a -> b
    $ "Unexpected call to mkConstCV (" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ") with value: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    a)
    mkConstCV k :: Kind
    k@KMaybe{}           a :: a
    a = String -> CV
    forall a. HasCallStack => String -> a
    error (String -> CV) -> String -> CV
    forall a b. (a -> b) -> a -> b
    $ "Unexpected call to mkConstCV (" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ") with value: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    a)
    mkConstCV k :: Kind
    k@KEither{}          a :: a
    a = String -> CV
    forall a. HasCallStack => String -> a
    error (String -> CV) -> String -> CV
    forall a b. (a -> b) -> a -> b
    $ "Unexpected call to mkConstCV (" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ") with value: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Integer -> String
    forall a. Show a => a -> String
    show (a -> Integer
    forall a. Integral a => a -> Integer
    toInteger a
    a)

    -- | Generate a random constant value ('CVal') of the correct kind.
    randomCVal :: Kind -> IO CVal
    randomCVal :: Kind -> IO CVal
    randomCVal k :: Kind
    k =
      case Kind
    k of
        KBool              -> Integer -> CVal
    CInteger (Integer -> CVal) -> IO Integer -> IO CVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Integer, Integer) -> IO Integer
    forall a. Random a => (a, a) -> IO a
    randomRIO (0, 1)
        KBounded s :: Bool
    s w :: Int
    w       -> Integer -> CVal
    CInteger (Integer -> CVal) -> IO Integer -> IO CVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Integer, Integer) -> IO Integer
    forall a. Random a => (a, a) -> IO a
    randomRIO (Bool -> Int -> (Integer, Integer)
    bounds Bool
    s Int
    w)
        KUnbounded         -> Integer -> CVal
    CInteger (Integer -> CVal) -> IO Integer -> IO CVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO Integer
    forall a. Random a => IO a
    randomIO
        KReal              -> AlgReal -> CVal
    CAlgReal (AlgReal -> CVal) -> IO AlgReal -> IO CVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO AlgReal
    forall a. Random a => IO a
    randomIO
        KFloat             -> Float -> CVal
    CFloat   (Float -> CVal) -> IO Float -> IO CVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO Float
    forall a. Random a => IO a
    randomIO
        KDouble            -> Double -> CVal
    CDouble  (Double -> CVal) -> IO Double -> IO CVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO Double
    forall a. Random a => IO a
    randomIO
        -- TODO: KString/KChar currently only go for 0..255; include unicode?
        KString            -> do Int
    l <- (Int, Int) -> IO Int
    forall a. Random a => (a, a) -> IO a
    randomRIO (0, 100)
                                 String -> CVal
    CString (String -> CVal) -> IO String -> IO CVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> IO Char -> IO String
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    replicateM Int
    l (Int -> Char
    chr (Int -> Char) -> IO Int -> IO Char
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Int, Int) -> IO Int
    forall a. Random a => (a, a) -> IO a
    randomRIO (0, 255))
        KChar              -> Char -> CVal
    CChar (Char -> CVal) -> (Int -> Char) -> Int -> CVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Char
    chr (Int -> CVal) -> IO Int -> IO CVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Int, Int) -> IO Int
    forall a. Random a => (a, a) -> IO a
    randomRIO (0, 255)
        KUninterpreted s :: String
    s _ -> String -> IO CVal
    forall a. HasCallStack => String -> a
    error (String -> IO CVal) -> String -> IO CVal
    forall a b. (a -> b) -> a -> b
    $ "Unexpected call to randomCVal with uninterpreted kind: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    s
        KList ek :: Kind
    ek           -> do Int
    l <- (Int, Int) -> IO Int
    forall a. Random a => (a, a) -> IO a
    randomRIO (0, 100)
                                 [CVal] -> CVal
    CList ([CVal] -> CVal) -> IO [CVal] -> IO CVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> IO CVal -> IO [CVal]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    replicateM Int
    l (Kind -> IO CVal
    randomCVal Kind
    ek)
        KSet  ek :: Kind
    ek           -> do Bool
    i <- IO Bool
    forall a. Random a => IO a
    randomIO                           -- regular or complement
                                 Int
    l <- (Int, Int) -> IO Int
    forall a. Random a => (a, a) -> IO a
    randomRIO (0, 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 (m :: * -> *) a. Monad m => a -> m a
    return (CVal -> IO CVal) -> CVal -> IO CVal
    forall a b. (a -> b) -> a -> b
    $ RCSet CVal -> CVal
    CSet (RCSet CVal -> CVal) -> RCSet CVal -> CVal
    forall a b. (a -> b) -> a -> b
    $ if Bool
    i then Set CVal -> RCSet CVal
    forall a. Set a -> RCSet a
    RegularSet Set CVal
    vals else Set CVal -> RCSet CVal
    forall a. Set a -> RCSet a
    ComplementSet Set CVal
    vals
        KTuple ks :: [Kind]
    ks          -> [CVal] -> CVal
    CTuple ([CVal] -> CVal) -> IO [CVal] -> IO CVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Kind -> IO CVal) -> [Kind] -> IO [CVal]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse Kind -> IO CVal
    randomCVal [Kind]
    ks
        KMaybe ke :: Kind
    ke          -> do Bool
    i <- IO Bool
    forall a. Random a => IO a
    randomIO
                                 if Bool
    i
                                    then CVal -> IO CVal
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CVal -> IO CVal) -> CVal -> IO CVal
    forall a b. (a -> b) -> a -> b
    $ Maybe CVal -> CVal
    CMaybe Maybe CVal
    forall a. Maybe a
    Nothing
                                    else Maybe CVal -> CVal
    CMaybe (Maybe CVal -> CVal) -> (CVal -> Maybe CVal) -> CVal -> CVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CVal -> Maybe CVal
    forall a. a -> Maybe a
    Just (CVal -> CVal) -> IO CVal -> IO CVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Kind -> IO CVal
    randomCVal Kind
    ke
        KEither k1 :: Kind
    k1 k2 :: Kind
    k2      -> do Bool
    i <- IO Bool
    forall a. Random a => IO a
    randomIO
                                 if Bool
    i
                                    then Either CVal CVal -> CVal
    CEither (Either CVal CVal -> CVal)
    -> (CVal -> Either CVal CVal) -> CVal -> CVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CVal -> Either CVal CVal
    forall a b. a -> Either a b
    Left  (CVal -> CVal) -> IO CVal -> IO CVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Kind -> IO CVal
    randomCVal Kind
    k1
                                    else Either CVal CVal -> CVal
    CEither (Either CVal CVal -> CVal)
    -> (CVal -> Either CVal CVal) -> CVal -> CVal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CVal -> Either CVal CVal
    forall a b. b -> Either a b
    Right (CVal -> CVal) -> IO CVal -> IO CVal
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Kind -> IO CVal
    randomCVal Kind
    k2
      where
        bounds :: Bool -> Int -> (Integer, Integer)
        bounds :: Bool -> Int -> (Integer, Integer)
    bounds False w :: Int
    w = (0, 2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Int
    w Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - 1)
        bounds True  w :: Int
    w = (-Integer
    x, Integer
    xInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -1) where x :: Integer
    x = 2Integer -> Int -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^(Int
    wInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -1)

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

    {-# ANN module ("HLint: ignore Redundant if" :: String) #-}