{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

{-|
Module      : GenWhat4Expr
Copyright   : (c) Galois Inc, 2020
License     : BSD3
Maintainer  : kquick@galois.com

This module provides Hedgehog generators for What4 expression values
that have associated Haskell counterparts; the Haskell value predicts
the What4 value on evaluation.

The What4 expression is often generated from a Haskell value
evaluation, so the "distance" between the tests and the implementation
might be seen as fairly small.  However, there is a lot of
simplification and subterm-elimination that is attempted in What4
expressions; this testing can verify the expected *functional*
behavior of the expressions as various simplifications and
implementation adjustments are made.

Because these are generated expressions, they don't tend to shrink as
much one would expect (e.g.  @(5 + 1)@ will not be shrunk to @6@)
because that requires domain-specific expression evaluation.  When
failures occur, it can be helpful to temporarily edit out portions of
these generators to attempt simplification.
-}

module GenWhat4Expr where

import           Data.Bits
import qualified Data.BitVector.Sized as BV
import           Data.Maybe ( fromMaybe, isJust )
import           Data.Word
import           GHC.Natural
import           GHC.TypeNats ( KnownNat )
import           Hedgehog
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Internal.Gen as IGen
import qualified Hedgehog.Range as Range
import           Test.Tasty.HUnit
import           What4.Interface


-- | A convenience class to extract the description string and haskell
-- value (and type) for any type of TestExpr.
class IsTestExpr x where
  type HaskellTy x
  desc :: x -> String
  testval :: x -> HaskellTy x

  -- n.b. cannot ad What4BTy, because the target (SymExpr) is a type
  -- synonym for a type family and type family instances cannot
  -- specify a type synonym as a target.
  --
  -- data What4BTy x :: BaseType -- -> Type
  -- type What4BTy x :: Type -> Type

  -- testexpr :: forall sym. (IsExprBuilder sym) => x -> sym -> IO (What4BTy x sym)

pdesc :: IsTestExpr x => x -> String
pdesc s = "(" <> desc s <> ")"

----------------------------------------------------------------------

-- Somewhat awkward, but when using Gen.subtermN for Gen.recursive,
-- each of the subterms is required to have the same type as the
-- result of the recursive term.  This is fine for uniform values
-- (e.g. simply-typed lambda calculi) but for a DSL like the What4
-- IsExprBuilder this means that even though there are separate
-- generators here for each subtype the results must be wrapped in a
-- common type that can hold all the 't' results from 'SymExpr sym
-- t'... the 'TestExpr' type here.  There's a lot of expectation of
-- which value is present when unwrapping (this is just test code),
-- and there various uses of Hedgehog 'Gen.filter' to ensure the right
-- value is returned even in the face of shrinking: when shrinking a
-- recursive term (e.g. "natEq x y") the result is a 'Pred sym', but
-- shrinking will try to eliminate the 'natEq' wrapper and end up
-- trying to return 'x' or 'y', which is a 'SymNat sym' instead.

data TestExpr = TE_Bool PredTestExpr
              | TE_Int  IntTestExpr
              | TE_BV8  BV8TestExpr
              | TE_BV16 BV16TestExpr
              | TE_BV32 BV32TestExpr
              | TE_BV64 BV64TestExpr

-- Projection functions that return Nothing if there is a constructor mismatch.

boolTestExprMaybe :: TestExpr -> Maybe PredTestExpr
boolTestExprMaybe = \case
  TE_Bool p -> Just p
  _ -> Nothing

intTestExprMaybe :: TestExpr -> Maybe IntTestExpr
intTestExprMaybe = \case
  TE_Int i -> Just i
  _ -> Nothing

bv8TestExprMaybe :: TestExpr -> Maybe BV8TestExpr
bv8TestExprMaybe = \case
  TE_BV8 bv8 -> Just bv8
  _ -> Nothing

bv16TestExprMaybe :: TestExpr -> Maybe BV16TestExpr
bv16TestExprMaybe = \case
  TE_BV16 bv16 -> Just bv16
  _ -> Nothing

bv32TestExprMaybe :: TestExpr -> Maybe BV32TestExpr
bv32TestExprMaybe = \case
  TE_BV32 bv32 -> Just bv32
  _ -> Nothing

bv64TestExprMaybe :: TestExpr -> Maybe BV64TestExpr
bv64TestExprMaybe = \case
  TE_BV64 bv64 -> Just bv64
  _ -> Nothing

-- Projection functions that `error` if there is a constructor mismatch.
-- Use these with caution.

fromBoolTestExpr :: HasCallStack => TestExpr -> PredTestExpr
fromBoolTestExpr = fromMaybe (error "Expected TE_Bool") . boolTestExprMaybe

fromIntTestExpr :: HasCallStack => TestExpr -> IntTestExpr
fromIntTestExpr = fromMaybe (error "Expected TE_Int") . intTestExprMaybe

fromBV8TestExpr :: HasCallStack => TestExpr -> BV8TestExpr
fromBV8TestExpr = fromMaybe (error "Expected TE_BV8") . bv8TestExprMaybe

fromBV16TestExpr :: HasCallStack => TestExpr -> BV16TestExpr
fromBV16TestExpr = fromMaybe (error "Expected TE_BV16") . bv16TestExprMaybe

fromBV32TestExpr :: HasCallStack => TestExpr -> BV32TestExpr
fromBV32TestExpr = fromMaybe (error "Expected TE_BV32") . bv32TestExprMaybe

fromBV64TestExpr :: HasCallStack => TestExpr -> BV64TestExpr
fromBV64TestExpr = fromMaybe (error "Expected TE_BV64") . bv64TestExprMaybe

-- Constructor predicates

isBoolTestExpr, isIntTestExpr,
  isBV8TestExpr, isBV16TestExpr, isBV32TestExpr, isBV64TestExpr
  :: TestExpr -> Bool

isBoolTestExpr = isJust . boolTestExprMaybe
isIntTestExpr = isJust . intTestExprMaybe
isBV8TestExpr = isJust . bv8TestExprMaybe
isBV16TestExpr = isJust . bv16TestExprMaybe
isBV32TestExpr = isJust . bv32TestExprMaybe
isBV64TestExpr = isJust . bv64TestExprMaybe


----------------------------------------------------------------------

data PredTestExpr =
  PredTest { preddsc :: String
           , predval :: Bool
           , predexp :: forall sym. (IsExprBuilder sym) => sym -> IO (Pred sym)
           }

instance IsTestExpr PredTestExpr where
  type HaskellTy PredTestExpr = Bool
  desc = preddsc
  testval = predval


genBoolCond :: (HasCallStack, Monad m) => GenT m TestExpr
genBoolCond = Gen.recursive Gen.choice
  [
    return $ TE_Bool $ PredTest "true" True $ return . truePred
  , return $ TE_Bool $ PredTest "false" False $ return . falsePred
  ]
  $
  let boolTerm = IGen.filterT isBoolTestExpr genBoolCond
      intTerm = IGen.filterT isIntTestExpr genIntTestExpr
      bv8Term = IGen.filterT isBV8TestExpr genBV8TestExpr
      bv16Term = IGen.filterT isBV16TestExpr genBV16TestExpr
      bv32Term = IGen.filterT isBV32TestExpr genBV32TestExpr
      bv64Term = IGen.filterT isBV64TestExpr genBV64TestExpr
      subBoolTerm2 gen = Gen.subterm2 boolTerm boolTerm
                         (\xt yt -> let x = fromBoolTestExpr xt
                                        y = fromBoolTestExpr yt in
                                    TE_Bool $ gen x y)
      subBoolTerm3 gen = Gen.subterm3 boolTerm boolTerm boolTerm
                         (\xt yt zt -> let x = fromBoolTestExpr xt
                                           y = fromBoolTestExpr yt
                                           z = fromBoolTestExpr zt in
                                       TE_Bool $ gen x y z)
      subIntTerms2 gen = Gen.subterm2 intTerm intTerm (\xt yt -> let x = fromIntTestExpr xt
                                                                     y = fromIntTestExpr yt in
                                                                 TE_Bool $ gen x y)
      -- subBV16Terms2 gen = Gen.subterm2 bv16Term bv16Term (\xt yt -> let x = fromBV16TestExpr xt
      --                                                                   y = fromBV16TestExpr yt in
      --                                                               TE_Bool $ gen x y)
      -- subBV8Terms2 gen = Gen.subterm2 bv8Term bv8Term (\xt yt -> let x = fromBV8TestExpr xt
      --                                                                y = fromBV8TestExpr yt in
      --                                                            TE_Bool $ gen x y)
  in
  [
    Gen.subterm genBoolCond
    (\itct -> let itc = fromBoolTestExpr itct in
              TE_Bool $ PredTest ("not " <> pdesc itc)
              (not $ testval itc)
              (\sym -> notPred sym =<< predexp itc sym))

  , subBoolTerm2
    (\x y ->
       PredTest ("and " <> pdesc x <> " " <> pdesc y)
       (testval x && testval y)
       (\sym -> do x' <- predexp x sym
                   y' <- predexp y sym
                   andPred sym x' y'
       ))

  , subBoolTerm2
    (\x y ->
       PredTest ("or " <> pdesc x <> " " <> pdesc y)
       (testval x || testval y)
       (\sym -> do x' <- predexp x sym
                   y' <- predexp y sym
                   orPred sym x' y'
       ))

  , subBoolTerm2
    (\x y ->
       PredTest ("eq " <> pdesc x <> " " <> pdesc y)
       (testval x == testval y)
       (\sym -> do x' <- predexp x sym
                   y' <- predexp y sym
                   eqPred sym x' y'
       ))

  , subBoolTerm2
    (\x y ->
       PredTest ("xor " <> pdesc x <> " " <> pdesc y)
       (testval x `xor` testval y)
       (\sym -> do x' <- predexp x sym
                   y' <- predexp y sym
                   xorPred sym x' y'
       ))

  , subBoolTerm3
    (\c x y ->
       PredTest ("ite " <> pdesc c <> " " <> pdesc x <> " " <> pdesc y)
       (if testval c then testval x else testval y)
       (\sym -> do c' <- predexp c sym
                   x' <- predexp x sym
                   y' <- predexp y sym
                   itePred sym c' x' y'
       ))

  , subIntTerms2
    (\x y ->
        PredTest ("intEq " <> pdesc x <> " " <> pdesc y)
        (testval x == testval y)
        (\sym -> do x' <- intexpr x sym
                    y' <- intexpr y sym
                    intEq sym x' y'
        ))

  , subIntTerms2
    (\x y ->
        PredTest (pdesc x <> " int.<= " <> pdesc y)
        (testval x <= testval y)
        (\sym -> do x' <- intexpr x sym
                    y' <- intexpr y sym
                    intLe sym x' y'
        ))

  , subIntTerms2
    (\x y ->
        PredTest (pdesc x <> " int.< " <> pdesc y)
        (testval x < testval y)
        (\sym -> do x' <- intexpr x sym
                    y' <- intexpr y sym
                    intLt sym x' y'
        ))

  , Gen.subterm2 intTerm bv16Term
    -- Note [natTerm]: natTerm is used as the index into
    -- bv16term. This is somewhat inefficient, but saves the
    -- administrative overhead of another TestExpr member.  However,
    -- the NatExpr could be greater than the bit range, so mod the
    -- result if necessary.  Also note that the testBitBV uses an
    -- actual Natural, not a What4 Nat, so the natval is used and the
    -- natexpr is ignored.
    (\it vt -> TE_Bool $  -- KWQ: bvsized
      let i = fromIntTestExpr it
          v = fromBV16TestExpr vt
          ival = fromInteger (testval i `mod` 16) in
      PredTest
      (pdesc v <> "[" <> show ival <> "]")
      (testBit (testval v) (fromEnum ival))
      (\sym -> testBitBV sym ival =<< bvexpr v sym))

  ]
  ++ bvPredExprs bv8Term fromBV8TestExpr bv8expr 8
  ++ bvPredExprs bv16Term fromBV16TestExpr bvexpr 16
  ++ bvPredExprs bv32Term fromBV32TestExpr bv32expr 32
  ++ bvPredExprs bv64Term fromBV64TestExpr bv64expr 64


bvPredExprs :: ( Monad m
               , HaskellTy bvtestexpr ~ Integer
               , IsTestExpr bvtestexpr
               , 1 <= w
               )
            => GenT m TestExpr
            -> (TestExpr -> bvtestexpr)
            -> (bvtestexpr
                -> (forall sym. (IsExprBuilder sym) => sym -> IO (SymBV sym w)))
            -> Natural
            -> [GenT m TestExpr]
bvPredExprs bvTerm projTE expr width =
  let subBVTerms2 gen = Gen.subterm2 bvTerm bvTerm
                        (\x y -> TE_Bool $ gen (projTE x) (projTE y))
      mask = (.&.) (2^width - 1)
      uBV v = if v >= 0 then v else 2^width + v
      sBV v = let norm = if v >= 0 then v else mask (v - 2^width)
              in if norm >= (2^(width-1)) then norm - 2^width else norm
      pfx o = "bv" <> show width <> "." <> o
  in
  [
    subBVTerms2
    (\x y ->
        PredTest (unwords [pdesc x, pfx "bvEq", pdesc y])
        (uBV (testval x) == uBV (testval y))
        (\sym -> do x' <- expr x sym
                    y' <- expr y sym
                    bvEq sym x' y'
        ))

  , subBVTerms2
    (\x y ->
        PredTest (unwords [pdesc x, pfx "bvNe", pdesc y])
        (uBV (testval x) /= uBV (testval y))
        (\sym -> do x' <- expr x sym
                    y' <- expr y sym
                    bvNe sym x' y'
        ))

  , subBVTerms2
    (\x y ->
        PredTest (unwords [pdesc x, pfx "bvUlt", pdesc y])
        (uBV (testval x) < uBV (testval y))
        (\sym -> do x' <- expr x sym
                    y' <- expr y sym
                    bvUlt sym x' y'
        ))

  , subBVTerms2
    (\x y ->
        PredTest (unwords [pdesc x, pfx "bvUle", pdesc y])
        (uBV (testval x) <= uBV (testval y))
        (\sym -> do x' <- expr x sym
                    y' <- expr y sym
                    bvUle sym x' y'
        ))

  , subBVTerms2
    (\x y ->
        PredTest (unwords [pdesc x, pfx "bvUge", pdesc y])
        (uBV (testval x) >= uBV (testval y))
        (\sym -> do x' <- expr x sym
                    y' <- expr y sym
                    bvUge sym x' y'
        ))

  , subBVTerms2
    (\x y ->
        PredTest (unwords [pdesc x, pfx "bvUgt", pdesc y])
        (uBV (testval x) > uBV (testval y))
        (\sym -> do x' <- expr x sym
                    y' <- expr y sym
                    bvUgt sym x' y'
        ))

  , subBVTerms2
    (\x y ->
        PredTest (unwords [pdesc x, pfx "bvSlt", pdesc y])
        (sBV (testval x) < sBV (testval y))
        (\sym -> do x' <- expr x sym
                    y' <- expr y sym
                    bvSlt sym x' y'
        ))

  , subBVTerms2
    (\x y ->
        PredTest (unwords [pdesc x, pfx "bvSle", pdesc y])
        (sBV (testval x) <= sBV (testval y))
        (\sym -> do x' <- expr x sym
                    y' <- expr y sym
                    bvSle sym x' y'
        ))

  , subBVTerms2
    (\x y ->
        PredTest (unwords [pdesc x, pfx "bvSge", pdesc y])
        (sBV (testval x) >= sBV (testval y))
        (\sym -> do x' <- expr x sym
                    y' <- expr y sym
                    bvSge sym x' y'
        ))

  , subBVTerms2
    (\x y ->
        PredTest (unwords [pdesc x, pfx "bvSgt", pdesc y])
        (sBV (testval x) > sBV (testval y))
        (\sym -> do x' <- expr x sym
                    y' <- expr y sym
                    bvSgt sym x' y'
        ))

  , Gen.subterm bvTerm
    (\vt -> TE_Bool $ let v = projTE vt in
        PredTest
        (pfx "isneg? " <> pdesc v)
        (mask (testval v) < 0 || mask (testval v) >= 2^(width-1))
        (\sym -> bvIsNeg sym =<< expr v sym))

  , Gen.subterm bvTerm
    (\vt -> TE_Bool $ let v = projTE vt in
        PredTest
        (pfx "isNonZero? " <> pdesc v)
        (testval v /= 0)
        (\sym -> bvIsNonzero sym =<< expr v sym))

  ]


----------------------------------------------------------------------

data IntTestExpr = IntTestExpr { intdesc :: String
                               , intval  :: Integer
                               , intexpr :: forall sym. (IsExprBuilder sym) => sym -> IO (SymInteger sym)
                               }

instance IsTestExpr IntTestExpr where
  type HaskellTy IntTestExpr = Integer
  desc = intdesc
  testval = intval

genIntTestExpr :: Monad m => GenT m TestExpr
genIntTestExpr = Gen.recursive Gen.choice
  [
    do n <- Gen.integral $ Range.constant (-3) 3  -- keep the range small, or will never see dup values for natEq
       return $ TE_Int $ IntTestExpr (show n) n $ \sym -> intLit sym n
  ]
  $
  let intTerm = IGen.filterT isIntTestExpr genIntTestExpr
      intTermNZ = IGen.filterT isIntNZTestExpr genIntTestExpr
      isIntNZTestExpr = \case
        TE_Int n -> testval n /= 0
        _ -> False
      subIntTerms2 gen = Gen.subterm2 intTerm intTerm
                           (\xt yt -> let x = fromIntTestExpr xt
                                          y = fromIntTestExpr yt in
                                      TE_Int $ gen x y)
      subIntTerms2nz gen = Gen.subterm2 intTerm intTermNZ
                           (\xt yt -> let x = fromIntTestExpr xt
                                          y = fromIntTestExpr yt in
                                      TE_Int $ gen x y)
  in
  [
    subIntTerms2 (\x y -> IntTestExpr (pdesc x <> " int.+ " <> pdesc y)
                          (testval x + testval y)
                          (\sym -> do x' <- intexpr x sym
                                      y' <- intexpr y sym
                                      intAdd sym x' y'
                          ))
  , subIntTerms2
    (\x y -> IntTestExpr (pdesc x <> " int.- " <> pdesc y)
             (testval x - testval y)
             (\sym -> do x' <- intexpr x sym
                         y' <- intexpr y sym
                         intSub sym x' y'
             ))
  , subIntTerms2
    (\x y -> IntTestExpr (pdesc x <> " int.* " <> pdesc y)
             (testval x * testval y)
             (\sym -> do x' <- intexpr x sym
                         y' <- intexpr y sym
                         intMul sym x' y'
             ))
  , subIntTerms2nz  -- nz on 2nd to avoid divide-by-zero
    (\x y -> IntTestExpr (pdesc x <> " int./ " <> pdesc y)
             (if testval y >= 0 then
                 testval x `div` testval y
              else
                 negate (testval x `div` negate (testval y)))
             (\sym -> do x' <- intexpr x sym
                         y' <- intexpr y sym
                         intDiv sym x' y'
             ))
  , subIntTerms2nz  -- nz on 2nd to avoid divide-by-zero
    (\x y -> IntTestExpr (pdesc x <> " int.mod " <> pdesc y)
             (testval x `mod` abs (testval y))
             (\sym -> do x' <- intexpr x sym
                         y' <- intexpr y sym
                         intMod sym x' y'
             ))
  , Gen.subterm3
    (IGen.filterT isBoolTestExpr genBoolCond)
    intTerm intTerm
    (\ct xt yt ->
      let c = fromBoolTestExpr ct
          x = fromIntTestExpr xt
          y = fromIntTestExpr yt in
      TE_Int $ IntTestExpr
      (pdesc c <> " int.? " <> pdesc x <> " : " <> pdesc y)
      (if testval c then testval x else testval y)
      (\sym -> do c' <- predexp c sym
                  x' <- intexpr x sym
                  y' <- intexpr y sym
                  intIte sym c' x' y'
      ))
  ]

----------------------------------------------------------------------

-- TBD: genIntTestExpr :: Monad m => GenT m TestExpr


----------------------------------------------------------------------

allbits8, allbits16, allbits32, allbits64 :: Integer
allbits8  = (2 :: Integer) ^ (8 :: Integer) - 1
allbits16 = (2 :: Integer) ^ (16 :: Integer) - 1
allbits32 = (2 :: Integer) ^ (32 :: Integer) - 1
allbits64 = (2 :: Integer) ^ (64 :: Integer) - 1


genBV8val :: Monad m => GenT m Integer
genBV8val = Gen.choice
            [
              -- keep the range small, or will never see dup values
              Gen.integral $ Range.constantFrom 0 (-10) 10
            , Gen.integral $ Range.constant (128-1) (128+1)
            , Gen.integral $ Range.constant (allbits8-2) allbits8
            ]

data BV8TestExpr = BV8TestExpr
  { bv8desc :: String
  , bv8val  :: Integer
  , bv8expr :: forall sym. (IsExprBuilder sym) => sym -> IO (SymBV sym 8)
  }

instance IsTestExpr BV8TestExpr where
  type HaskellTy BV8TestExpr = Integer
  desc = bv8desc
  testval = bv8val

genBV8TestExpr :: Monad m => GenT m TestExpr
genBV8TestExpr = let ret8 = return . TE_BV8 in
  Gen.recursive Gen.choice
  [
    do n <- genBV8val
       ret8 $ BV8TestExpr (show n <> "`8") n $ \sym -> bvLit sym knownRepr (BV.mkBV knownNat n)
  , ret8 $ BV8TestExpr ("0`8") 0 $ \sym -> minUnsignedBV sym knownRepr
  , let n = allbits8
    in ret8 $ BV8TestExpr (show n <> "`8") n $ \sym -> maxUnsignedBV sym knownRepr
  , let n = allbits8 `shiftR` 1
    in ret8 $ BV8TestExpr (show n <> "`8") n $ \sym -> maxSignedBV sym knownRepr
  , let n = allbits8 `xor` (allbits8 `shiftR` 1)
    in ret8 $ BV8TestExpr (show n <> "`8") n $ \sym -> minSignedBV sym knownRepr
  ]
  $
  bvTGExprs (tgen8 bvTermGens)
  ++
  bvTGMixedExprs bvTermGens 8


genBV16val :: Monad m => GenT m Integer
genBV16val = Gen.choice
             [
               -- keep the range small, or will never see dup values
               Gen.integral $ Range.constantFrom 0 (-10) 10
             , Gen.integral $ Range.constant (allbits8-1) (allbits8+2)
             , Gen.integral $ Range.constant ((-1) * (allbits8+2)) ((-1) * (allbits8-1))
             , Gen.integral $ Range.constant (allbits16-2) allbits16
             ]

data BV16TestExpr =
  BV16TestExpr { bvdesc :: String
               , bvval  :: Integer
               , bvexpr :: forall sym. (IsExprBuilder sym) => sym -> IO (SymBV sym 16)
               }

instance IsTestExpr BV16TestExpr where
  type HaskellTy BV16TestExpr = Integer
  desc = bvdesc
  testval = bvval

genBV16TestExpr :: Monad m => GenT m TestExpr
genBV16TestExpr = let ret16 = return . TE_BV16 in
  Gen.recursive Gen.choice
  [
    do n <- genBV16val
       ret16 $ BV16TestExpr (show n <> "`16") n $ \sym -> bvLit sym knownRepr (BV.mkBV knownNat n)
  , ret16 $ BV16TestExpr ("0`16") 0 $ \sym -> minUnsignedBV sym knownRepr
  , let n = allbits16
    in ret16 $ BV16TestExpr (show n <> "`16") n $ \sym -> maxUnsignedBV sym knownRepr
  , let n = allbits16 `shiftR` 1
    in ret16 $ BV16TestExpr (show n <> "`16") n $ \sym -> maxSignedBV sym knownRepr
  , let n = allbits16 `xor` (allbits16 `shiftR` 1)
    in ret16 $ BV16TestExpr (show n <> "`16") n $ \sym -> minSignedBV sym knownRepr
  ]
  $
  bvTGExprs (tgen16 bvTermGens)
  ++
  bvTGMixedExprs bvTermGens 16


genBV32val :: Monad m => GenT m Integer
genBV32val = Gen.choice
             [
               -- keep the range small, or will never see dup values
               Gen.integral $ Range.constantFrom 0 (-10) 10
             , Gen.integral $ Range.constant (allbits8-1) (allbits8+2)
             , Gen.integral $ Range.constant (allbits16-1) (allbits16+2)
             , Gen.integral $ Range.constant ((-1) * (allbits16+2)) ((-1) * (allbits16-1))
             , Gen.integral $ Range.constant (allbits32-2) allbits32
             ]


data BV32TestExpr =
  BV32TestExpr { bv32desc :: String
               , bv32val  :: Integer
               , bv32expr :: forall sym. (IsExprBuilder sym) => sym -> IO (SymBV sym 32)
               }

instance IsTestExpr BV32TestExpr where
  type HaskellTy BV32TestExpr = Integer
  desc = bv32desc
  testval = bv32val

genBV32TestExpr :: Monad m => GenT m TestExpr
genBV32TestExpr = let ret32 = return . TE_BV32 in
  Gen.recursive Gen.choice
  [
    do n <- genBV32val
       ret32 $ BV32TestExpr (show n <> "`32") n $ \sym -> bvLit sym knownRepr (BV.mkBV knownNat n)
  , ret32 $ BV32TestExpr ("0`32") 0 $ \sym -> minUnsignedBV sym knownRepr
  , let n = allbits32
    in ret32 $ BV32TestExpr (show n <> "`32") n $ \sym -> maxUnsignedBV sym knownRepr
  , let n = allbits32 `shiftR` 1
    in ret32 $ BV32TestExpr (show n <> "`32") n $ \sym -> maxSignedBV sym knownRepr
  , let n = allbits32 `xor` (allbits32 `shiftR` 1)
    in ret32 $ BV32TestExpr (show n <> "`32") n $ \sym -> minSignedBV sym knownRepr
  ]
  $
  bvTGExprs (tgen32 bvTermGens)
  ++
  bvTGMixedExprs bvTermGens 32


genBV64val :: Monad m => GenT m Integer
genBV64val = Gen.choice
             [
               -- keep the range small, or will never see dup values
               Gen.integral $ Range.constantFrom 0 (-10) 10
             , Gen.integral $ Range.constant (allbits8-1) (allbits8+2)
             , Gen.integral $ Range.constant (allbits16-1) (allbits16+2)
             , Gen.integral $ Range.constant (allbits32-1) (allbits32+2)
             , Gen.integral $ Range.constant ((-1) * (allbits32+2)) ((-1) * (allbits32-1))
             , Gen.integral $ Range.constant (allbits64-2) allbits64
             ]


data BV64TestExpr =
  BV64TestExpr { bv64desc :: String
               , bv64val  :: Integer
               , bv64expr :: forall sym. (IsExprBuilder sym) => sym -> IO (SymBV sym 64)
               }

instance IsTestExpr BV64TestExpr where
  type HaskellTy BV64TestExpr = Integer
  desc = bv64desc
  testval = bv64val

genBV64TestExpr :: Monad m => GenT m TestExpr
genBV64TestExpr = let ret64 = return . TE_BV64 in
  Gen.recursive Gen.choice
  [
    do n <- genBV64val
       ret64 $ BV64TestExpr (show n <> "`64") n $ \sym -> bvLit sym knownRepr (BV.mkBV knownNat n)
  , ret64 $ BV64TestExpr ("0`64") 0 $ \sym -> minUnsignedBV sym knownRepr
  , let n = allbits64
    in ret64 $ BV64TestExpr (show n <> "`64") n $ \sym -> maxUnsignedBV sym knownRepr
  , let n = allbits64 `shiftR` 1
    in ret64 $ BV64TestExpr (show n <> "`64") n $ \sym -> maxSignedBV sym knownRepr
  , let n = allbits64 `xor` (allbits64 `shiftR` 1)
    in ret64 $ BV64TestExpr (show n <> "`64") n $ \sym -> minSignedBV sym knownRepr
  ]
  $
  bvTGExprs (tgen64 bvTermGens)
  ++
  bvTGMixedExprs bvTermGens 64


-- | For a particular bitwidth, the BVTermGen structure provides the
-- various definitions of term generators, constructors and
-- projectors, What4 expression extractors, and width designations.
data BVTermGen m bvtestexpr w word = BVTermGen
  {
    genTerm :: GenT m TestExpr
  , conBVT :: bvtestexpr -> TestExpr
  , projBVT :: TestExpr -> bvtestexpr
  , subBVTCon :: String -> Integer
              -> (forall sym. (IsExprBuilder sym) => sym -> IO (SymBV sym w))
              -> bvtestexpr
  , symExpr :: bvtestexpr
            -> (forall sym. (IsExprBuilder sym) => sym -> IO (SymBV sym w))
  , bitWidth :: Natural
  , toBVWord :: (Integer -> word)
  }

-- | This combines the information about BVTermGen for all of the
-- standard widths
data BVTermsGen m = BVTermsGen
  {
    tgen8 :: BVTermGen m BV8TestExpr 8 Word8
  , tgen16 :: BVTermGen m BV16TestExpr 16 Word16
  , tgen32 :: BVTermGen m BV32TestExpr 32 Word32
  , tgen64 :: BVTermGen m BV64TestExpr 64 Word64
  }

bvTermGens :: Monad m => BVTermsGen m
bvTermGens =
  let g8 = BVTermGen
           (IGen.filterT isBV8TestExpr genBV8TestExpr)
           TE_BV8
           fromBV8TestExpr
           BV8TestExpr
           bv8expr
           8
           fromIntegral
      g16 = BVTermGen
            (IGen.filterT isBV16TestExpr genBV16TestExpr)
            TE_BV16
            fromBV16TestExpr
            BV16TestExpr
            bvexpr
            16
            fromIntegral
      g32 = BVTermGen
            (IGen.filterT isBV32TestExpr genBV32TestExpr)
            TE_BV32
            fromBV32TestExpr
            BV32TestExpr
            bv32expr
            32
            fromIntegral
      g64 = BVTermGen
            (IGen.filterT isBV64TestExpr genBV64TestExpr)
            TE_BV64
            fromBV64TestExpr
            BV64TestExpr
            bv64expr
            64
            fromIntegral
            -- n.b. toEnum . fromEnum doesn't work for very large
            -- Word64 values (-1, -2, high-bit set?), so use
            -- fromIntegral instead (probably faster?)
  in BVTermsGen g8 g16 g32 g64


bvTGExprs :: ( Monad m
             , HaskellTy bvtestexpr ~ Integer
             , IsTestExpr bvtestexpr
             , 1 <= w
             , KnownNat w
             , Integral word
             , FiniteBits word
             )
          => BVTermGen m bvtestexpr w word
          -> [GenT m TestExpr]
bvTGExprs gt = bvExprs (genTerm gt) (conBVT gt) (projBVT gt) (subBVTCon gt)
                       (symExpr gt) (bitWidth gt) (toBVWord gt)

bvExprs :: ( Monad m
           , HaskellTy bvtestexpr ~ Integer
           , IsTestExpr bvtestexpr
           , 1 <= w
           , KnownNat w
           , Integral word
           , Bits word
           , FiniteBits word
           )
        => GenT m TestExpr
        -> (bvtestexpr -> TestExpr)
        -> (TestExpr -> bvtestexpr)
        -> (String -> Integer
            -> (forall sym. (IsExprBuilder sym) => sym -> IO (SymBV sym w))
            -> bvtestexpr)
        -> (bvtestexpr
            -> (forall sym. (IsExprBuilder sym) => sym -> IO (SymBV sym w)))
        -> Natural
        -> (HaskellTy bvtestexpr -> word)
        -> [GenT m TestExpr]
bvExprs bvTerm conTE projTE teSubCon expr width toWord =
  let subBVTerms1 gen = Gen.subterm bvTerm (conTE . gen . projTE)
      subBVTerms2 gen = Gen.subterm2 bvTerm bvTerm
                        (\x y -> conTE $ gen (projTE x) (projTE y))
      subBVTerms2nz gen = Gen.subterm2 bvTerm bvTermNZ
                          (\x y -> conTE $ gen (projTE x) (projTE y))
      bvTermNZ = do t <- projTE <$> bvTerm
                    -- adjust 0 to +1 to avoid divide-by-zero.  A
                    -- Gen.filterT tends to lead to non-termination
                    -- here
                    return $ if testval t == 0
                             then conTE $ teSubCon
                                  (pdesc t <> " +1")
                                  (testval t + 1)
                                  (\sym -> do lit1 <- bvLit sym knownRepr (BV.one knownNat)

                                              orig <- expr t sym
                                              bvAdd sym orig lit1)
                             else conTE t
      mask = (.&.) (2^width - 1)
      uBV v = if v >= 0 then v else 2^width + v
      sBV v = let norm = if v >= 0 then v else mask (v - 2^width)
              in if norm >= (2^(width-1)) then norm - 2^width else norm
      pfx o = "bv" <> show width <> "." <> o
  in
  [
    subBVTerms1
    (\x -> teSubCon (pfx "neg " <> pdesc x)
           (mask ((-1) * testval x))
           (\sym -> bvNeg sym =<< expr x sym))

  , subBVTerms1
    (\x -> teSubCon (pfx "not " <> pdesc x)
           (mask (complement $ testval x))
           (\sym -> bvNotBits sym =<< expr x sym))

  , subBVTerms2
    (\x y -> teSubCon (pdesc x <> " " <> pfx "+ " <> pdesc y)
             (mask (testval x + testval y))
             (\sym -> do x' <- expr x sym
                         y' <- expr y sym
                         bvAdd sym x' y'))

  , subBVTerms2
    (\x y -> teSubCon (unwords [pdesc x, pfx "-", pdesc y])
             (mask (testval x - testval y))
             (\sym -> do x' <- expr x sym
                         y' <- expr y sym
                         bvSub sym x' y'))

  , subBVTerms2
    (\x y -> teSubCon (unwords [pdesc x, pfx "*", pdesc y])
             (mask (testval x * testval y))
             (\sym -> do x' <- expr x sym
                         y' <- expr y sym
                         bvMul sym x' y'))

  , subBVTerms2nz
    (\x y -> teSubCon (unwords [pdesc x, pfx "u/", pdesc y])
             (mask (uBV (testval x) `quot` uBV (testval y)))
             (\sym -> do x' <- expr x sym
                         y' <- expr y sym
                         bvUdiv sym x' y'))

  , subBVTerms2nz
    (\x y -> teSubCon (unwords [pdesc x, pfx "urem", pdesc y])
             (mask (uBV (testval x) `rem` uBV (testval y)))
             (\sym -> do x' <- expr x sym
                         y' <- expr y sym
                         bvUrem sym x' y'))

  , subBVTerms2nz
    (\x y -> teSubCon (unwords [pdesc x, pfx "s/", pdesc y])
             (let x' = sBV $ testval x
                  y' = sBV $ testval y
              in mask (x' `quot` y'))
             (\sym -> do x' <- expr x sym
                         y' <- expr y sym
                         bvSdiv sym x' y'))

  , subBVTerms2nz
    (\x y -> teSubCon (unwords [pdesc x, pfx "srem", pdesc y])
             (let x' = sBV $ testval x
                  y' = sBV $ testval y
              in mask (x' `rem` y'))
             (\sym -> do x' <- expr x sym
                         y' <- expr y sym
                         bvSrem sym x' y'))

  , Gen.subterm3
    (IGen.filterT isBoolTestExpr genBoolCond)
    bvTerm bvTerm
    (\ct lt rt -> conTE $
    let c = fromBoolTestExpr ct
        l = projTE lt
        r = projTE rt
    in teSubCon
       (unwords [pdesc c, pfx "?", pdesc l, ":", pdesc r])
       (if testval c then testval l else testval r)
       (\sym -> do c' <- predexp c sym
                   l' <- expr l sym
                   r' <- expr r sym
                   bvIte sym c' l' r'))

  , subBVTerms2
    (\x y -> teSubCon (unwords [pdesc x, pfx "rol", pdesc y])
             (let x' = toWord $ uBV $ testval x
                  y' = fromEnum $ uBV $ testval y
              in mask (toInteger (x' `rotateL` y')))
             (\sym -> do x' <- expr x sym
                         y' <- expr y sym
                         bvRol sym x' y'))

  , subBVTerms2
    (\x y -> teSubCon (unwords [pdesc x, pfx "ror", pdesc y])
             (let x' = toWord $ uBV $ testval x
                  y' = fromEnum $ uBV $ testval y
              in mask (toInteger (x' `rotateR` y')))
             (\sym -> do x' <- expr x sym
                         y' <- expr y sym
                         bvRor sym x' y'))

  , subBVTerms2
    (\x y -> teSubCon (unwords [pdesc x, pfx "&", pdesc y])
             (mask (testval x .&. testval y))
             (\sym -> do x' <- expr x sym
                         y' <- expr y sym
                         bvAndBits sym x' y'))

  , subBVTerms2
    (\x y -> teSubCon (unwords [pdesc x, pfx "|", pdesc y])
             (mask (testval x .|. testval y))
             (\sym -> do x' <- expr x sym
                         y' <- expr y sym
                         bvOrBits sym x' y'))

  , subBVTerms2
    (\x y -> teSubCon (unwords [pdesc x, pfx "xor", pdesc y])
             (mask (testval x `xor` testval y))
             (\sym -> do x' <- expr x sym
                         y' <- expr y sym
                         bvXorBits sym x' y'))

  , let intTerm = IGen.filterT isIntTestExpr genIntTestExpr
        boolTerm = IGen.filterT isBoolTestExpr genBoolCond
    in
      Gen.subterm3 bvTerm intTerm boolTerm $
      -- see Note [natTerm]
      \bvt nt bt ->
        let bv = projTE bvt
            n = fromIntTestExpr nt
            b = fromBoolTestExpr bt
            nval = fromInteger (testval n `mod` toInteger width)
            ival = fromIntegral nval :: Int
        in conTE $ teSubCon
           (pdesc bv <> "[" <> show nval <> "]" <> pfx ":=" <> pdesc b)
           (if testval b
            then setBit (testval bv) ival
            else clearBit (testval bv) ival)
           (\sym -> do bv' <- expr bv sym
                       b' <- predexp b sym
                       bvSet sym bv' nval b')

  , let boolTerm = IGen.filterT isBoolTestExpr genBoolCond
    in
      Gen.subterm boolTerm $
      \bt ->
        let b = fromBoolTestExpr bt in
        -- technically bvFill also takes a NatRepr for the output
        -- width, but due to the arrangement of these expression
        -- generators, it will just generate the size specified for
        -- the current width
        conTE $ teSubCon
        (pfx "=" <> pdesc b <> "..")
        (if testval b then mask (-1) else mask 0)
        (\sym -> bvFill sym knownRepr =<< predexp b sym)

  , subBVTerms1
    (\x -> teSubCon (pfx "bvPopCount " <> pdesc x)
           (fromIntegral $ popCount $ mask $ testval x)
           (\sym -> bvPopcount sym =<< expr x sym))

  , subBVTerms1
    (\x -> teSubCon (pfx "bvCountLeadingZeros " <> pdesc x)
           (fromIntegral $ countLeadingZeros $ toWord $ uBV $ mask $ testval x)
           (\sym -> bvCountLeadingZeros sym =<< expr x sym))

  , subBVTerms1
    (\x -> teSubCon (pfx "bvCountTrailingZeros " <> pdesc x)
           (fromIntegral $ countTrailingZeros $ toWord $ uBV $ mask $ testval x)
           (\sym -> bvCountTrailingZeros sym =<< expr x sym))

  -- TBD: carrylessMultiply

  , subBVTerms1
    (\x -> teSubCon
           (pfx "bvSelect @0[" <> pdesc x <> "]")
           (mask (testval x))
           (\sym -> do x' <- expr x sym
                       bvSelect sym (knownRepr :: NatRepr 0) knownRepr x'))

  -- TODO: bvTrunc doesn't allow the no-op/same-size operation
  -- , subBVTerms1
  --   (\x -> teSubCon
  --          (pfx "bvTrunc " <> pdesc x)
  --          (mask (testval x))
  --          (\sym -> do x' <- expr x sym
  --                      bvTrunc sym knownRepr x'))

  -- TODO: bvZext doesn't allow the no-op/same-size operation
  -- , subBVTerms1
  --   (\x -> teSubCon
  --          (pfx "bvZext " <> pdesc x)
  --          (mask (testval x))
  --          (\sym -> do x' <- expr x sym
  --                      bvZext sym knownRepr x'))

  -- TODO: bvSext doesn't allow the no-op/same-size operation
  -- , subBVTerms1
  --   (\x -> teSubCon
  --          (pfx "bvSext " <> pdesc x)
  --          (mask (testval x))
  --          (\sym -> do x' <- expr x sym
  --                      bvSext sym knownRepr x'))


  , subBVTerms2
    (\x y -> teSubCon (unwords [pdesc x, pfx "<<", pdesc y])
             (mask (uBV (testval x) `shiftL` (fromEnum $ min (toInteger width) $ uBV $ testval y)))
             (\sym -> do x' <- expr x sym
                         y' <- expr y sym
                         bvShl sym x' y'))

  , subBVTerms2
    (\x y -> teSubCon (unwords [pdesc x, pfx "lsr", pdesc y])
             (let s = fromEnum $ min (toInteger width) $ uBV $ testval y
              in mask (uBV (testval x) `shiftR` s))
             (\sym -> do x' <- expr x sym
                         y' <- expr y sym
                         bvLshr sym x' y'))

  , subBVTerms2
    (\x y -> teSubCon (unwords [pdesc x, pfx "asr", pdesc y])
             (let s = fromEnum $ min (toInteger width) $ uBV $ testval y
              in mask (sBV (testval x) `shiftR` s))
             (\sym -> do x' <- expr x sym
                         y' <- expr y sym
                         bvAshr sym x' y'))

  ]


bvTGMixedExprs :: Monad m => BVTermsGen m -> Natural -> [GenT m TestExpr]
bvTGMixedExprs termGens tgtWidth =
  case tgtWidth of
    8 -> bvTGMixedExprs_Double (tgen8 termGens) (tgen16 termGens) ++
         bvTGMixedExprs_Quadruple (tgen8 termGens) (tgen32 termGens)
    16 -> bvTGMixedExprs_Half (tgen16 termGens) (tgen8 termGens) ++
          bvTGMixedExprs_Double (tgen16 termGens) (tgen32 termGens) ++
          bvTGMixedExprs_Quadruple (tgen16 termGens) (tgen64 termGens)
    32 -> bvTGMixedExprs_Half (tgen32 termGens) (tgen16 termGens) ++
          bvTGMixedExprs_QuarterHalf (tgen32 termGens) (tgen16 termGens) (tgen8 termGens) ++
          bvTGMixedExprs_Double (tgen32 termGens) (tgen64 termGens)
    64 -> bvTGMixedExprs_Half (tgen64 termGens) (tgen32 termGens) ++
          bvTGMixedExprs_QuarterHalf (tgen64 termGens) (tgen32 termGens) (tgen16 termGens)
    _ -> error $ "Unsupported width for mixed BV expressions: " <> show tgtWidth


bvTGMixedExprs_Half :: ( Monad m
                       , 1 <= w
                       , w + 1 <= w + w
                       , KnownNat (w + w)
                       , HaskellTy bvtestexpr ~ Integer
                       , IsTestExpr bvtestexpr
                       , HaskellTy bvtestexpr_h ~ Integer
                       , IsTestExpr bvtestexpr_h
                       )
                    => BVTermGen m bvtestexpr (w + w) word
                    -> BVTermGen m bvtestexpr_h w word_h
                    -> [GenT m TestExpr]
bvTGMixedExprs_Half thisTG halfTG =
  let pfx o = "bv" <> (show $ bitWidth thisTG) <> "." <> o
      halfWidth = bitWidth halfTG
      halfMask = (.&.) (2^halfWidth - 1)
      width = bitWidth thisTG
      mask = (.&.) (2^width - 1)
      halfHiBit = (.&.) (2^(halfWidth - 1))
  in
    -- output size must match the size of thisTG
    [
      Gen.subterm2 (genTerm halfTG) (genTerm halfTG) $
      (\gen x y -> conBVT thisTG $ gen (projBVT halfTG x) (projBVT halfTG y)) $
      (\x y -> subBVTCon thisTG
               (pfx "bvConcat " <> pdesc x <> " " <> pdesc y)
               (let x' = halfMask (testval x)
                    y' = halfMask (testval y)
                in (x' `shiftL` (fromEnum halfWidth)) .|. y')
               (\sym -> do x' <- symExpr halfTG x sym
                           y' <- symExpr halfTG y sym
                           bvConcat sym x' y'))

    , Gen.subterm (genTerm halfTG)
      (\x -> conBVT thisTG $
             subBVTCon thisTG
             (pfx "bvZext " <> pdesc (projBVT halfTG x))
             (let x' = testval (projBVT halfTG x)
               in (halfMask x'))
             (\sym -> do x' <- symExpr halfTG (projBVT halfTG x) sym
                         bvZext sym knownRepr x'))

    , Gen.subterm (genTerm halfTG)
      (\x -> conBVT thisTG $
             subBVTCon thisTG
             (pfx "bvSext " <> pdesc (projBVT halfTG x))
             (let x' = halfMask $ testval (projBVT halfTG x)
                  hiBits = mask (-1) `xor` halfMask (-1)
              in if halfHiBit x' == 0 then x' else (hiBits .|. x'))
             (\sym -> do x' <- symExpr halfTG (projBVT halfTG x) sym
                         bvSext sym knownRepr x'))
    ]

bvTGMixedExprs_QuarterHalf :: ( Monad m
                              , 1 <= w
                              , 1 <= w + w
                              , 1 <= w + w + w + w
                              , (w + (w + w)) ~ ((w + w) + w)
                              , 1 <= ((w + w) + w)
                              , (w + 1) <= w + w + w + w
                              , KnownNat (w + w + w + w)
                              , HaskellTy bvtestexpr ~ Integer
                              , IsTestExpr bvtestexpr
                              , HaskellTy bvtestexpr_h ~ Integer
                              , IsTestExpr bvtestexpr_h
                              , HaskellTy bvtestexpr_q ~ Integer
                              , IsTestExpr bvtestexpr_q
                              )
                           => BVTermGen m bvtestexpr (w + w + w + w) word
                           -> BVTermGen m bvtestexpr_h (w + w) word_h
                           -> BVTermGen m bvtestexpr_q w word_q
                           -> [GenT m TestExpr]
bvTGMixedExprs_QuarterHalf thisTG halfTG quarterTG =
  let pfx o = "bv" <> (show $ bitWidth thisTG) <> "." <> o
      halfWidth = bitWidth halfTG
      halfMask = (.&.) (2^halfWidth - 1)
      quarterWidth = bitWidth quarterTG
      quarterMask = (.&.) (2^quarterWidth - 1)
      quarterHiBit = (.&.) (2^(quarterWidth - 1))
      width = bitWidth thisTG
      mask = (.&.) (2^width - 1)
  in
    [
      Gen.subterm3 (genTerm quarterTG) (genTerm halfTG) (genTerm quarterTG) $
      (\gen x y z -> conBVT thisTG $
                     gen (projBVT quarterTG x)
                         (projBVT halfTG y)
                         (projBVT quarterTG z)) $
      (\x y z -> subBVTCon thisTG
                 (pfx "bvConcat " <> pdesc x <> " " <>
                  pfx "bvConcat " <> pdesc y <> " " <> pdesc z)
                 (let x' = quarterMask (testval x)
                      y' = halfMask (testval y)
                      z' = quarterMask (testval z)
                      s1 = fromEnum halfWidth
                      s2 = fromEnum quarterWidth
                  in ((((x' `shiftL` s1) .|. y') `shiftL` s2) .|. z'))
                 (\sym -> do x' <- symExpr quarterTG x sym
                             y' <- symExpr halfTG y sym
                             z' <- symExpr quarterTG z sym
                             xy <- bvConcat sym x' y'
                             bvConcat sym xy z'))

    -- already did bvZext and bvSext with half-size in
    -- bvTGMixedExprs_Half, so just test extensions from quarter size
    -- here.

    , Gen.subterm (genTerm quarterTG)
      (\x -> conBVT thisTG $
             subBVTCon thisTG
             (pfx "bvZext " <> pdesc (projBVT quarterTG x))
             (let x' = testval (projBVT quarterTG x)
               in (quarterMask x'))
             (\sym -> do x' <- symExpr quarterTG (projBVT quarterTG x) sym
                         bvZext sym knownRepr x'))

    , Gen.subterm (genTerm quarterTG)
      (\x -> conBVT thisTG $
             subBVTCon thisTG
             (pfx "bvSext " <> pdesc (projBVT quarterTG x))
             (let x' = quarterMask $ testval (projBVT quarterTG x)
                  hiBits = mask (-1) `xor` quarterMask (-1)
              in if quarterHiBit x' == 0 then x' else (hiBits .|. x'))
             (\sym -> do x' <- symExpr quarterTG (projBVT quarterTG x) sym
                         bvSext sym knownRepr x'))
    ]


bvTGMixedExprs_Double :: ( Monad m
                         , 1 <= w
                         , 0 + w <= w + w
                         , 1 + w <= w + w  -- bvSelect --v
                         , w + 1 <= w + w  -- bvTrunc ---^
                         , 2 + w <= w + w
                         , 7 + w <= w + w
                         , KnownNat w
                         , HaskellTy bvtestexpr ~ Integer
                         , IsTestExpr bvtestexpr
                         , HaskellTy bvtestexpr_d ~ Integer
                         , IsTestExpr bvtestexpr_d
                         )
                      => BVTermGen m bvtestexpr w word
                      -> BVTermGen m bvtestexpr_d (w + w) word_d
                      -> [GenT m TestExpr]
bvTGMixedExprs_Double thisTG dblTG =
  let pfx o = "bv" <> (show $ bitWidth thisTG) <> "." <> o
      mask = (.&.) (2^(bitWidth thisTG) - 1)
  in
    [

      -- The bvSelect offset and size are NatReprs, so the type must
      -- be known at compile time, thus these values cannot be
      -- generated via hedgehog property generation functions.  The
      -- size must be the size of the current conBVT result, and
      -- bvSelect requres that offset + size < width of input
      -- value. There are a few hard-coded offsets used here that
      -- should be valid for all input BV sizes >= 16 and output BV
      -- sizes >= 8:
      --
      --   0, 1, 2, 7

      Gen.subterm (genTerm dblTG)
      (\x -> conBVT thisTG $
             subBVTCon thisTG
             (pfx "bvSelect @0[" <> pdesc (projBVT dblTG x) <> "]")
             (mask ((testval (projBVT dblTG x)) `shiftR` 0))
             (\sym -> do x' <- symExpr dblTG (projBVT dblTG x) sym
                         bvSelect sym (knownRepr :: NatRepr 0) knownRepr x'))

    , Gen.subterm (genTerm dblTG)
      (\x -> conBVT thisTG $
             subBVTCon thisTG
             (pfx "bvSelect @1[" <> pdesc (projBVT dblTG x) <> "]")
             (mask ((testval (projBVT dblTG x)) `shiftR` 1))
             (\sym -> do x' <- symExpr dblTG (projBVT dblTG x) sym
                         bvSelect sym (knownRepr :: NatRepr 1) knownRepr x'))

    , Gen.subterm (genTerm dblTG)
      (\x -> conBVT thisTG $
             subBVTCon thisTG
             (pfx "bvSelect @2[" <> pdesc (projBVT dblTG x) <> "]")
             (mask ((testval (projBVT dblTG x)) `shiftR` 2))
             (\sym -> do x' <- symExpr dblTG (projBVT dblTG x) sym
                         bvSelect sym (knownRepr :: NatRepr 2) knownRepr x'))

    , Gen.subterm (genTerm dblTG)
      (\x -> conBVT thisTG $
             subBVTCon thisTG
             (pfx "bvSelect @7[" <> pdesc (projBVT dblTG x) <> "]")
             (mask ((testval (projBVT dblTG x)) `shiftR` 7))
             (\sym -> do x' <- symExpr dblTG (projBVT dblTG x) sym
                         bvSelect sym (knownRepr :: NatRepr 7) knownRepr x'))

    , Gen.subterm (genTerm dblTG)
      (\x -> conBVT thisTG $
             subBVTCon thisTG
             (pfx "bvTrunc " <> pdesc (projBVT dblTG x))
             (mask (testval (projBVT dblTG x)))
             (\sym -> do x' <- symExpr dblTG (projBVT dblTG x) sym
                         bvTrunc sym knownRepr x'))
    ]

bvTGMixedExprs_Quadruple :: ( Monad m
                         , 1 <= w
                         , 0 + w <= w + w + w + w
                         , 1 + w <= w + w + w + w  -- bvSelect --v
                         , w + 1 <= w + w + w + w  -- bvTrunc ---^
                         , 2 + w <= w + w + w + w
                         , 7 + w <= w + w + w + w
                         , 12 + w <= w + w + w + w
                         , 19 + w <= w + w + w + w
                         , KnownNat w
                         , HaskellTy bvtestexpr ~ Integer
                         , IsTestExpr bvtestexpr
                         , HaskellTy bvtestexpr_d ~ Integer
                         , IsTestExpr bvtestexpr_d
                         )
                      => BVTermGen m bvtestexpr w word
                      -> BVTermGen m bvtestexpr_d (w + w + w + w) word_d
                      -> [GenT m TestExpr]
bvTGMixedExprs_Quadruple thisTG quadTG =
  let pfx o = "bv" <> (show $ bitWidth thisTG) <> "." <> o
      mask = (.&.) (2^(bitWidth thisTG) - 1)
  in
    [
      -- The bvSelect offset and size are NatReprs, so the type must
      -- be known at compile time, thus these values cannot be
      -- generated via hedgehog property generation functions.  The
      -- size must be the size of the current conBVT result, and there
      -- are a few hard-coded offsets used here that should be valid
      -- for all BV sizes >= 32:
      --
      --   0, 1, 2, 7, 12, 19

      Gen.subterm (genTerm quadTG)
      (\x -> conBVT thisTG $
             subBVTCon thisTG
             (pfx "bvSelect @0[" <> pdesc (projBVT quadTG x) <> "]")
             (mask ((testval (projBVT quadTG x)) `shiftR` 0))
             (\sym -> do x' <- symExpr quadTG (projBVT quadTG x) sym
                         bvSelect sym (knownRepr :: NatRepr 0) knownRepr x'))

    , Gen.subterm (genTerm quadTG)
      (\x -> conBVT thisTG $
             subBVTCon thisTG
             (pfx "bvSelect @1[" <> pdesc (projBVT quadTG x) <> "]")
             (mask ((testval (projBVT quadTG x)) `shiftR` 1))
             (\sym -> do x' <- symExpr quadTG (projBVT quadTG x) sym
                         bvSelect sym (knownRepr :: NatRepr 1) knownRepr x'))

    , Gen.subterm (genTerm quadTG)
      (\x -> conBVT thisTG $
             subBVTCon thisTG
             (pfx "bvSelect @2[" <> pdesc (projBVT quadTG x) <> "]")
             (mask ((testval (projBVT quadTG x)) `shiftR` 2))
             (\sym -> do x' <- symExpr quadTG (projBVT quadTG x) sym
                         bvSelect sym (knownRepr :: NatRepr 2) knownRepr x'))

    , Gen.subterm (genTerm quadTG)
      (\x -> conBVT thisTG $
             subBVTCon thisTG
             (pfx "bvSelect @7[" <> pdesc (projBVT quadTG x) <> "]")
             (mask ((testval (projBVT quadTG x)) `shiftR` 7))
             (\sym -> do x' <- symExpr quadTG (projBVT quadTG x) sym
                         bvSelect sym (knownRepr :: NatRepr 7) knownRepr x'))

    , Gen.subterm (genTerm quadTG)
      (\x -> conBVT thisTG $
             subBVTCon thisTG
             (pfx "bvSelect @12[" <> pdesc (projBVT quadTG x) <> "]")
             (mask ((testval (projBVT quadTG x)) `shiftR` 12))
             (\sym -> do x' <- symExpr quadTG (projBVT quadTG x) sym
                         bvSelect sym (knownRepr :: NatRepr 12) knownRepr x'))

    , Gen.subterm (genTerm quadTG)
      (\x -> conBVT thisTG $
             subBVTCon thisTG
             (pfx "bvSelect @19[" <> pdesc (projBVT quadTG x) <> "]")
             (mask ((testval (projBVT quadTG x)) `shiftR` 19))
             (\sym -> do x' <- symExpr quadTG (projBVT quadTG x) sym
                         bvSelect sym (knownRepr :: NatRepr 19) knownRepr x'))

    -- bvTrunc output size must match the size of thisTG

    , Gen.subterm (genTerm quadTG)
      (\x -> conBVT thisTG $
             subBVTCon thisTG
             (pfx "bvTrunc " <> pdesc (projBVT quadTG x))
             (mask (testval (projBVT quadTG x)))
             (\sym -> do x' <- symExpr quadTG (projBVT quadTG x) sym
                         bvTrunc sym knownRepr x'))
    ]



-- TBD: BV operations returning a (Pred,BV) pair will need another TestExpr
-- representation: addUnsignedOF, addSignedOF, subUnsignedOF,
-- subSignedOF, mulUnsignedOF, mulSignedOF

-- TBD: BV operations returning a (BV,BV) pair will need another
-- TestExpr representation: unsignedWideMultiplyBV, signedWideMultiplyBV

-- TBD: struct operations
-- TBD: array operations
-- TBD: Lossless conversions
-- TBD: Lossless combinators
-- TBD: Lossy conversions
-- TBD: Lossy (non-injective) combinators
-- TBD: Bitvector operations (intSetWidth, uintSetWidth, intToUInt)
-- TBD: string operations
-- TBD: real operations
-- TBD: IEEE-754 floating-point operations
-- TBD: Cplx operations
-- TBD: misc functions in Interface.hs