{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
--module TestTemplate where

module Main where

import Control.Exception
import Control.Monad ((<=<), unless)
import Control.Monad.IO.Class (liftIO)
import           Control.Monad.Trans.Maybe
import Data.Bits
import Data.Parameterized.Map (MapF)
import qualified Data.Parameterized.Map as MapF
import Data.Parameterized.Nonce
import Data.Parameterized.Pair
import Data.Parameterized.Some
import Data.String
import Numeric (showHex)
import System.Exit (exitFailure)
-- import System.IO

import LibBF
import qualified Data.BitVector.Sized as BV

import What4.BaseTypes
import What4.Config
import What4.Interface

import           What4.Protocol.SMTWriter ((.==), mkSMTTerm)
import qualified What4.Protocol.SMTWriter as SMT
import qualified What4.Protocol.SMTLib2 as SMT2
import qualified What4.Protocol.Online as Online
import           What4.Protocol.Online (SolverProcess(..), OnlineSolver(..))
import qualified What4.Solver.CVC4 as CVC4

import What4.Expr
import What4.Expr.App (reduceApp)
import What4.Expr.Builder
import What4.Expr.GroundEval
import What4.SatResult

import What4.Utils.Arithmetic
import What4.Utils.FloatHelpers

import           Hedgehog
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Gen
import GHC.Stack

--import Debug.Trace (trace)



main :: IO ()
main =
  do let fpp = knownRepr :: FloatPrecisionRepr Prec32

     let xs = castTemplates RNE <>
              (Some <$> floatTestTemplates [] 0 fpp) <>
              (do r <- roundingModes
                  (Some <$> floatTemplates [r] 1 fpp))

     sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState globalNonceGenerator

     extendConfig CVC4.cvc4Options (getConfiguration sym)
     proc <- Online.startSolverProcess @(SMT2.Writer CVC4.CVC4) CVC4.cvc4Features Nothing sym

     let testnum = 500

     tests <- sequence [ do p <- templateGroundEvalTestAlt sym proc t testnum
                            --p <- templateGroundEvalTest sym proc t testnum
                            --p <- templateConstantFoldTest sym t testnum
                            pure (fromString (show t), p)
                       | Some t <- xs
                       ]
     testsPassed <- checkSequential $ Group "Float tests" tests
     unless testsPassed exitFailure


data FUnOp
  = FNeg
  | FAbs
  | FSqrt RoundingMode
  | FRound RoundingMode
 deriving (Show)

data FBinOp
  = FAdd RoundingMode
  | FSub RoundingMode
  | FMul RoundingMode
  | FDiv RoundingMode
  | FRem
  | FMin
  | FMax
 deriving (Show)

data FTestOp
  = FIsNaN
  | FIsInf
  | FIsZero
  | FIsPos
  | FIsNeg
  | FIsSubnorm
  | FIsNorm
 deriving Show

data FRelOp
  = FLogicEq
  | FLogicNeq
  | FEq
  | FApart
  | FUnordered
  | FLe
  | FLt
  | FGe
  | FGt
 deriving Show

-- | This datatype essentially mirrors the public API of the
--   What4 interface.  There should (eventually) be one element
--   of this datatype per syntax former method in "What4.Interface".
--   Each template represents a fragment of syntax that could be
--   generated.  We use these templates to test constant folding,
--   ground evaluation, term simplifications, fidelity
--   WRT solver term semantics and soundness of abstract domains.
--
--   The overall idea is that we want to enumerate all small
--   templates and use each template to generate a collection of test
--   cases.  Hopefully we can achieve high code path coverages with
--   a relatively small depth of templates, which should keep this process
--   managable.  We also have the option to manually generate templates
--   if necessary to increase test coverage.
data TestTemplate tp where
  TVar :: BaseTypeRepr tp -> TestTemplate tp

  TFloatPZero :: FloatPrecisionRepr fpp -> TestTemplate (BaseFloatType fpp)
  TFloatNZero :: FloatPrecisionRepr fpp -> TestTemplate (BaseFloatType fpp)
  TFloatNaN   :: FloatPrecisionRepr fpp -> TestTemplate (BaseFloatType fpp)

  TFloatUnOp ::
    FUnOp ->
    TestTemplate (BaseFloatType fpp) ->
    TestTemplate (BaseFloatType fpp)

  TFloatBinOp ::
    FBinOp ->
    TestTemplate (BaseFloatType fpp) ->
    TestTemplate (BaseFloatType fpp) ->
    TestTemplate (BaseFloatType fpp)

  TFloatTest ::
    FTestOp ->
    TestTemplate (BaseFloatType fpp) ->
    TestTemplate BaseBoolType

  TFloatRel ::
    FRelOp ->
    TestTemplate (BaseFloatType fpp) ->
    TestTemplate (BaseFloatType fpp) ->
    TestTemplate BaseBoolType

  TFloatFromBits :: (2 <= eb, 2 <= sb) =>
    FloatPrecisionRepr (FloatingPointPrecision eb sb) ->
    TestTemplate (BaseBVType (eb + sb)) ->
    TestTemplate (BaseFloatType (FloatingPointPrecision eb sb))

  TFloatToBits :: (2 <= eb, 2 <= sb) =>
    TestTemplate (BaseFloatType (FloatingPointPrecision eb sb)) ->
    TestTemplate (BaseBVType (eb + sb))

  TBVToFloat :: (1 <= w) =>
    FloatPrecisionRepr fpp ->
    RoundingMode ->
    Bool {- False = unsigned -} ->
    TestTemplate (BaseBVType w) ->
    TestTemplate (BaseFloatType fpp)

  TFloatToBV :: (1 <= w) =>
    NatRepr w ->
    RoundingMode ->
    Bool {- False = unsigned -} ->
    TestTemplate (BaseFloatType fpp) ->
    TestTemplate (BaseBVType w)

  TFloatCast ::
    FloatPrecisionRepr fpp ->
    RoundingMode ->
    TestTemplate (BaseFloatType fpp') ->
    TestTemplate (BaseFloatType fpp)

  TFloatToReal ::
    TestTemplate (BaseFloatType fpp) ->
    TestTemplate BaseRealType

  TRealToFloat ::
    FloatPrecisionRepr fpp ->
    RoundingMode ->
    TestTemplate BaseRealType ->
    TestTemplate (BaseFloatType fpp)

  TFloatFMA ::
    RoundingMode ->
    TestTemplate (BaseFloatType fpp) ->
    TestTemplate (BaseFloatType fpp) ->
    TestTemplate (BaseFloatType fpp) ->
    TestTemplate (BaseFloatType fpp)



instance Show (TestTemplate tp) where
  showsPrec d tt = case tt of
    TVar{}        -> showString "<var>"
    TFloatPZero{} -> showString "+0.0"
    TFloatNZero{} -> showString "-0.0"
    TFloatNaN{}   -> showString "NaN"
    TFloatUnOp op x -> showParen (d > 0) $
       shows op . showString " " . showsPrec 10 x
    TFloatBinOp op x y -> showParen (d > 0) $
       shows op . showString " " . showsPrec 10 x . showString " " . showsPrec 10 y
    TFloatTest op x -> showParen (d > 0) $
       shows op . showString " " . showsPrec 10 x
    TFloatRel op x y ->  showParen (d > 0) $
       shows op . showString " " . showsPrec 10 x . showString " " . showsPrec 10 y
    TFloatFMA r x y z -> showParen (d > 0) $
       showString "FMA" . showString " " . shows r . showString " " .
       showsPrec 10 x . showString " " . showsPrec 10 y . showString " " . showsPrec 10 z
    TFloatFromBits _fpp x -> showParen (d > 0) $
       showString "FloatFromBits " . showsPrec 10 x
    TFloatToBits x -> showParen (d > 0) $
       showString "FloatToBits " . showsPrec 10 x
    TFloatCast fpp r x -> showParen (d > 0) $
       showString "FloatCast " . shows fpp . showString " " . shows r . showString " " . showsPrec 10 x
    TFloatToReal x -> showParen (d > 0) $
       showString "FloatToReal " . showsPrec 10 x
    TRealToFloat fpp r x -> showParen (d > 0) $
       showString "RealToFloat " . shows fpp . showString " " . shows r . showString " " . showsPrec 10 x
    TBVToFloat fpp r sgn x ->
       showString (if sgn then "SBVToFloat " else "BVToFloat ") .
       shows fpp . showString " " .
       shows r . showString " " .
       showsPrec 10 x
    TFloatToBV w r sgn x ->
       showString (if sgn then "FloatToSBV" else "FloatToBV ") .
       shows w . showString " " .
       shows r . showString " " .
       showsPrec 10 x

-- | Compute the maximum depth of the given test template
templateDepth :: TestTemplate tp -> Integer
templateDepth = f
  where
  f :: TestTemplate tp -> Integer
  f t = case t of
          TVar{} -> 0

          TFloatPZero{} -> 0
          TFloatNZero{} -> 0
          TFloatNaN{}  -> 0

          TFloatUnOp _op x    -> 1 + (f x)
          TFloatBinOp _op x y -> 1 + max (f x) (f y)
          TFloatTest _op x    -> 1 + (f x)
          TFloatRel _op x y   -> 1 + max (f x) (f y)
          TFloatFMA _ x y z   -> 1 + max (f x) (max (f y) (f z))
          TFloatFromBits _ x  -> 1 + f x
          TFloatToBits x      -> 1 + f x
          TFloatCast _ _ x    -> 1 + f x
          TFloatToReal x      -> 1 + f x
          TRealToFloat _ _ x  -> 1 + f x
          TBVToFloat _ _ _ x  -> 1 + f x
          TFloatToBV _ _ _ x  -> 1 + f x


-- | A manually provided collection test templates that test coercions between types.
castTemplates :: RoundingMode -> [Some TestTemplate]
castTemplates r =
  [ Some (TFloatFromBits (knownRepr :: FloatPrecisionRepr Prec32) (TVar (BaseBVRepr (knownNat @32))))
  , Some (TFloatToBits (TVar (knownRepr :: BaseTypeRepr (BaseFloatType Prec32))))
  , Some (TFloatCast (knownRepr :: FloatPrecisionRepr Prec32) r
              (TVar (knownRepr :: BaseTypeRepr (BaseFloatType Prec64))))
  , Some (TFloatCast (knownRepr :: FloatPrecisionRepr Prec64) r
              (TVar (knownRepr :: BaseTypeRepr (BaseFloatType Prec32))))
  , Some (TFloatToReal (TVar (knownRepr :: BaseTypeRepr (BaseFloatType Prec32))))
  , Some (TRealToFloat (knownRepr :: FloatPrecisionRepr Prec32) r (TVar knownRepr))

  , Some (TBVToFloat (knownRepr :: FloatPrecisionRepr Prec32) r False
              (TVar (knownRepr :: BaseTypeRepr (BaseBVType 32))))
  , Some (TBVToFloat (knownRepr :: FloatPrecisionRepr Prec32) r True
              (TVar (knownRepr :: BaseTypeRepr (BaseBVType 32))))

  , Some (TFloatToBV (knownNat :: NatRepr 32) r False
              (TVar (knownRepr :: BaseTypeRepr (BaseFloatType Prec32))))
  , Some (TFloatToBV (knownNat :: NatRepr 32) r True
              (TVar (knownRepr :: BaseTypeRepr (BaseFloatType Prec32))))
  ]


-- | Generate test templates for all predicates and relations
--   on folating point values, whose subterms are generated
--   by calling @floatTemplates.  With the given inputs.
--
--   CAUTION! This function blows up very quickly!
floatTestTemplates ::
  [RoundingMode] ->
  Integer ->
  FloatPrecisionRepr fpp ->
  [TestTemplate BaseBoolType]
floatTestTemplates rs n fpp = tops <> relops
 where
   subterms = floatTemplates rs n fpp
   tops   = [ TFloatTest op x | op <- fTestOps, x <- subterms ]
   relops = [ TFloatRel op x y | op <- fRelOps, x <- subterms, y <- subterms ]

-- | Generate floating-point test templates of the given
--   depth, iterating through each of the given rounding
--   modes for operations that require rounding.
--
--   CAUTION! This function blows up very quickly!
floatTemplates ::
  [RoundingMode] ->
  Integer ->
  FloatPrecisionRepr fpp ->
  [TestTemplate (BaseFloatType fpp)]
floatTemplates rs n fpp
  | n <= 0 = base
  | n == 1 = base <> floatOps fpp rs base
  | otherwise = f n

  where
   base = [ TVar (BaseFloatRepr fpp), TFloatPZero fpp, TFloatNZero fpp, TFloatNaN fpp ]

   f d | d < 1 = [ TVar (BaseFloatRepr fpp) ]
   f d = [ TVar (BaseFloatRepr fpp) ] <> floatOps fpp rs (f (d-1))

floatOps ::
  FloatPrecisionRepr fpp ->
  [RoundingMode] ->
  [TestTemplate (BaseFloatType fpp)] ->
  [TestTemplate (BaseFloatType fpp)]
floatOps fpp@(FloatingPointPrecisionRepr eb sb) rs subterms = casts <> uops <> bops <> fma
  where
    uops  = [ TFloatUnOp op x | op <- fUnOps rs, x <- subterms ]
    bops  = [ TFloatBinOp op x y | op <- fBinOps rs, x <- subterms, y <- subterms ]
    fma   = [ TFloatFMA r x y z | r <- rs, x <- subterms, y <- subterms, z <- subterms ]
    casts = [ case isPosNat (addNat eb sb) of
                Just LeqProof -> TFloatFromBits fpp (TVar (BaseBVRepr (addNat eb sb)))
                Nothing -> error $ unwords ["floatOps", "bad fpp", show fpp]
            ]

roundingModes :: [RoundingMode]
roundingModes = [ RNE, RNA, RTP, RTN, RTZ ]

fBinOps :: [RoundingMode] -> [FBinOp]
fBinOps rs =
  (FAdd <$> rs) <>
  (FSub <$> rs) <>
  (FMul <$> rs) <>
  (FDiv <$> rs) <>
  [ FRem, FMin, FMax ]

fUnOps :: [RoundingMode] -> [FUnOp]
fUnOps rs =
  [ FNeg, FAbs ] <>
  (FSqrt <$> rs) <>
  (FRound <$> rs)

fTestOps :: [FTestOp]
fTestOps = [ FIsNaN, FIsInf, FIsZero, FIsPos, FIsNeg, FIsSubnorm, FIsNorm ]

fRelOps :: [FRelOp]
fRelOps = [ FLogicEq, FLogicNeq, FEq, FApart, FUnordered, FLe, FLt, FGe, FGt ]



generateByType :: BaseTypeRepr tp -> Gen (GroundValue tp)
generateByType BaseBoolRepr = Gen.bool
generateByType (BaseFloatRepr fpp) = genFloat fpp
generateByType (BaseBVRepr w) = genBV w
generateByType BaseRealRepr  = genReal
generateByType tp = error ("generateByType! TODO " ++ show tp)

genReal :: Gen Rational
genReal = Gen.realFrac_ (Gen.linearFracFrom 0 (negate mx) mx)
  where mx = 1 ^^ (200::Integer)

genBV :: (1 <= w) => NatRepr w -> Gen (BV.BV w)
genBV w =
  do val <- Gen.integral (Gen.linearFrom 0 (minSigned w) (maxSigned w))
     pure (BV.mkBV w val)

-- | A random generator for floating-point values that tries to
--   get good coverage for all the various special and normal values.
genFloat :: FloatPrecisionRepr fpp -> Gen BigFloat
genFloat (FloatingPointPrecisionRepr eb sb) =
    Gen.frequency
        [ ( 1, pure bfPosZero)
        , ( 1, pure bfNegZero)
        , ( 1, pure bfPosInf)
        , ( 1, pure bfNegInf)
        , ( 1, pure bfNaN)
        , (50, genNormal)
        , ( 5, genSubnormal)
        , (45, genBinary)
        ]
 where
  emax = bit (fromInteger (intValue eb - 1)) - 1
  smax = bit (fromInteger (intValue sb)) - 1
  opts = fpOpts (intValue eb) (intValue sb) Away
  numBits = intValue eb + intValue sb

  -- generates non-shrinkable floats uniformly chosen from among all bitpatterns
  genBinary =
    do bits <- Gen.integral_ (Gen.linear 0 (bit (fromInteger numBits) - 1))
       pure (bfFromBits opts bits)

  -- generates non-shrinkable floats corresponding to subnormal values.  These are
  -- values with 0 biased exponent and nonzero mantissa.
  genSubnormal =
    do sgn  <- Gen.bool
       bits <- Gen.integral_ (Gen.linear 1 (bit (fromInteger (intValue sb)) - 1))
       let x0 = bfFromBits opts bits
       let x  = if sgn then bfNeg x0 else x0
       pure $! x

  -- tries to generate shrinkable floats, prefering "smaller" values
  genNormal =
    do sgn <- Gen.bool
       ex  <- Gen.integral (Gen.linearFrom 0 (1-emax) emax)
       mag <- Gen.integral (Gen.linear 1 smax)
       let x0 = bfStatus (bfMul2Exp opts (bfFromInteger mag) (ex - fromIntegral (lgCeil mag)))
       let x  = if sgn then bfNeg x0 else x0
       pure $! x

-- | Use the given map to bind the values in an expression and compute the value
--   of the expression, if it can be computed.
mapGroundEval :: MapF (Expr t) GroundValueWrapper -> Expr t tp -> MaybeT IO (GroundValue tp)
mapGroundEval m x =
  case MapF.lookup x m of
    Just v -> pure (unGVW v)
    Nothing -> tryEvalGroundExpr (mapGroundEval m) x

-- | Inject ground values into expressions based on their type.
groundLit ::  ExprBuilder t st fs -> BaseTypeRepr tp -> GroundValue tp -> IO (Expr t tp)
groundLit sym tp v =
  case tp of
    BaseFloatRepr fpp -> floatLit sym fpp v
    BaseBVRepr w      -> bvLit sym w v
    BaseBoolRepr      -> pure (backendPred sym v)
    BaseRealRepr      -> realLit sym v
    _ -> error $ unwords ["groundLit TODO", show tp]

-- | Given a map binding varables to expressions, rebuild the given expression by reapplying
--   the expression formers appearing in it.  This is used to test the constant-folding
--   rules of the expression builder.
reduceEval :: ExprBuilder t st fs -> MapF (Expr t) GroundValueWrapper -> Expr t tp -> IO (Expr t tp)
reduceEval sym m e
  | Just v <- MapF.lookup e m = groundLit sym (exprType e) (unGVW v)
  | Just a <- asApp e = reduceApp sym bvUnary =<< traverseApp (reduceEval sym m) a
  | otherwise = pure e

-- | Use the given solver process as an evaluation oracle to
--   verify that a given expression must have the given
--   value when the variables in it are bound via the
--   given map.
--
--   A value as computed via @solverEval@ may nonetheless fail
--   this test if functions appearing in it are underconstrained.
verifySolverEval :: forall t st fs solver tp.
  OnlineSolver solver =>
  ExprBuilder t st fs ->
  SolverProcess t solver ->
  MapF (Expr t) GroundValueWrapper ->
  Expr t tp ->
  GroundValue tp ->
  IO Bool
verifySolverEval _sym proc gmap expr val =
  do let c = Online.solverConn proc
     let f :: Pair (Expr t) GroundValueWrapper -> IO (SMT.Term solver)
         f (Pair e (GVW v)) =
            case exprType e of
              BaseFloatRepr fpp ->
                do e' <- mkSMTTerm c e
                   return (e' .== SMT.floatTerm fpp v)
              BaseBVRepr w ->
                do e' <- mkSMTTerm c e
                   return (e' .== SMT.bvTerm w v)
              BaseBoolRepr ->
                do e' <- mkSMTTerm c e
                   return (e' .== SMT.boolExpr v)
              BaseRealRepr ->
                do e' <- mkSMTTerm c e
                   return (e' .== SMT.rationalTerm v)

              tp -> fail ("verifySolverEval: TODO " ++ show tp)

     Online.inNewFrame proc do
       mapM_ (SMT.assumeFormula c <=< f) (MapF.toList gmap)

       gl <- f (Pair expr (GVW val))
       SMT.assumeFormula c (SMT.notExpr gl)

       res <- Online.check proc "eval"
       case res of
         Unknown -> fail "Expected UNSAT, but got UNKNOWN"
         Unsat _ -> pure True
         Sat _   -> pure False

-- | Use the given solver process as an evaluation oracle to
--   compute the a value of the given expression when given
--   a binding of variables that appear in the expression.
--   Return the value computed by the solver.
--
--   In principle, the solver might return one of several
--   different values for the expression if any of the
--   functions appearing in it are partial or underspecified.
solverEval :: forall t st fs solver tp.
  OnlineSolver solver =>
  ExprBuilder t st fs ->
  SolverProcess t solver ->
  MapF (Expr t) GroundValueWrapper ->
  Expr t tp ->
  IO (GroundValue tp)
solverEval _sym proc gmap expr =
  do let c = Online.solverConn proc
     let f :: Pair (Expr t) GroundValueWrapper -> IO (SMT.Term solver)
         f (Pair e (GVW v)) =
            case exprType e of
              BaseFloatRepr fpp ->
                do e' <- mkSMTTerm c e
                   return (e' .== SMT.floatTerm fpp v)
              BaseBVRepr w ->
                do e' <- mkSMTTerm c e
                   return (e' .== SMT.bvTerm w v)
              BaseBoolRepr ->
                do e' <- mkSMTTerm c e
                   return (e' .== SMT.boolExpr v)
              BaseRealRepr ->
                do e' <- mkSMTTerm c e
                   return (e' .== SMT.rationalTerm v)

              tp -> fail ("solverEval: TODO " ++ show tp)

     Online.inNewFrame proc do
       mapM_ (SMT.assumeFormula c <=< f) (MapF.toList gmap)
       e' <- mkSMTTerm c expr
       res <- Online.check proc "eval"
       case res of
         Unsat _ -> fail "Expected SAT, but got UNSAT"
         Unknown -> fail "Expected SAT, but got UNKNOWN"
         Sat _ ->
           case exprType expr of
             BaseFloatRepr fpp ->
               do bv <- SMT.smtEvalFloat (Online.solverEvalFuns proc) fpp e'
                  return (bfFromBits (fppOpts fpp RNE) (BV.asUnsigned bv))
             BaseBVRepr w ->
               SMT.smtEvalBV (Online.solverEvalFuns proc) w e'
             BaseRealRepr ->
               SMT.smtEvalReal (Online.solverEvalFuns proc) e'
             BaseBoolRepr ->
               SMT.smtEvalBool (Online.solverEvalFuns proc) e'

             tp -> fail ("solverEval: TODO2 " ++ show tp)

showMap :: MapF (Expr t) GroundValueWrapper -> String
showMap gmap = unlines (map f (MapF.toList gmap))
  where
    f :: Pair (Expr t) (GroundValueWrapper) -> String
    f (Pair e (GVW v)) = show (printSymExpr e) <> " |-> " <> showGroundVal (exprType e) v

showGroundVal :: HasCallStack => BaseTypeRepr tp -> GroundValue tp -> String
showGroundVal tp v =
  case tp of
    BaseFloatRepr fpp ->
      let i = bfToBits (fppOpts fpp RNE) v in
        show v <> " 0x" <> showHex i ""
    BaseBVRepr w -> BV.ppHex w v
    BaseRealRepr -> show v
    BaseBoolRepr -> show v
    _ -> "showGroundVal: TODO " <> show tp

-- | This property generator takes a template and uses it to
--   compare our Haskell-side ground evaulation code against
--   the computations performed by an online solver, which
--   is used as a computational oracle.  Random values are
--   chosen for the free variables, and the expression is evaluated
--   by the ground evaluator using the generated values for
--   the variables.  Next, in the solver, we assert the equality of
--   the same variables to their concrete values and ask for a satisfying
--   model; then we ask the solver for the value of the expression in
--   that model and check that the two computations agree.
--
--   Some expressions are underspecified, which means their output is
--   unconstrained for some inputs (e.g, division by 0). In these cases
--   the ground evaluator may compute no value at all; these cases
--   are considered successful tests.
templateGroundEvalTest ::
  OnlineSolver solver =>
  ExprBuilder t st fs ->
  SolverProcess t solver ->
  TestTemplate tp ->
  Int ->
  IO Property
templateGroundEvalTest sym proc t numTests =
  do (sz, gmapGen, expr) <- templateGen sym t
     pure $ withTests (fromIntegral (max 1 (numTests * sz))) $ property $
       do annotateShow (printSymExpr expr)
          gmap <- forAllWith showMap gmapGen
          v  <- liftIO (runMaybeT (mapGroundEval gmap expr))
          annotate (maybe "Nothing" (showGroundVal (exprType expr)) v)
          res <- liftIO (try (solverEval sym proc gmap expr))
          case res of
            Left (ex :: IOError) -> footnote (show ex) >> failure
            Right v' ->
              do annotate (showGroundVal (exprType expr) v')
                 case v of
                   Just v_ -> Just True === groundEq (exprType expr) v_ v'
                   Nothing -> success

-- | This property generator takes a template and uses it to
--   compare our Haskell-side ground evaulation code against
--   the computations performed by an online solver, which
--   is used as a computational oracle.  Random values are
--   chosen for the free variables, and the expression is evaluated
--   by the ground evaluator using the generated values for
--   the variables.  Next, in the solver, we assert the equality of
--   the same variables to their concrete values, and ask the solver
--   to prove that it has the same value as we computed in the
--   ground evaluator.  This complements the above test; together
--   they demonstrate that the ground evaluator, when it computes a
--   value at all, computes the unique value that a solver may assign to it.
templateGroundEvalTestAlt ::
  OnlineSolver solver =>
  ExprBuilder t st fs ->
  SolverProcess t solver ->
  TestTemplate tp ->
  Int ->
  IO Property
templateGroundEvalTestAlt sym proc t numTests =
  do (sz, gmapGen, expr) <- templateGen sym t
     pure $ withTests (fromIntegral (max 1 (numTests * sz))) $ property $
       do annotateShow (printSymExpr expr)
          gmap <- forAllWith showMap gmapGen
          v  <- liftIO (runMaybeT (mapGroundEval gmap expr))
          case v of
            Nothing -> success
            Just v_ ->
              do annotate (showGroundVal (exprType expr) v_)
                 res <- liftIO (try (verifySolverEval sym proc gmap expr v_))
                 case res of
                   Left (ex :: IOError) -> footnote (show ex) >> failure
                   Right b -> if b then success else failure


-- | This property generator takes a template and uses it to
--   compare the ground evaluation code against the constant-folding
--   rules used when constructing terms.  Similar to the test above,
--   we compute an expression and then use ground evaluation to
--   compute a value for randomly-chosen values of the variables.
--   Next, we \"reduce\" the expression by reapplying the syntactic
--   constructors, replacing the variables with literal expressions.
--   Finally, we check that the expression has constant-folded to
--   a literal expression that agrees with the ground value computed
--   before. Moreover, ground evaluation should fail to compute a value
--   iff the reduced expression does not constant-fold to a literal.
templateConstantFoldTest ::
  ExprBuilder t st fs ->
  TestTemplate tp ->
  Int ->
  IO Property
templateConstantFoldTest sym t numTests =
  do (sz, gmapGen, expr) <- templateGen sym t
     pure $ withTests (fromIntegral (max 1 (numTests * sz))) $ property $
       do annotateShow (printSymExpr expr)
          gmap <- forAllWith showMap gmapGen

          v  <- liftIO (runMaybeT (mapGroundEval gmap expr))
          annotate (maybe "Nothing" (showGroundVal (exprType expr)) v)

          v' <- liftIO (reduceEval sym gmap expr)
          annotateShow (printSymExpr v')

          case v of
            Just v_ ->
              do p <- liftIO (isEq sym v' =<< groundLit sym (exprType expr) v_)
                 Just True === asConstantPred p
            Nothing -> False === baseIsConcrete v'

-- | Given a test template, compute data that can be used to drive one of the
--   test predicates above.  We return an @Int@ that counts how many variables
--   appear in the template, a generator action that computes ground values
--   for the variables appearing in the template, and an expression over
--   those variables according to the template.
templateGen :: forall t st fs tp.
  ExprBuilder t st fs -> TestTemplate tp -> IO (Int, Gen (MapF (Expr t) GroundValueWrapper), Expr t tp)
templateGen sym = f
  where
    f :: forall tp'. TestTemplate tp' -> IO (Int, Gen (MapF (Expr t) GroundValueWrapper), Expr t tp')
    f (TVar bt) =
       do v <- freshConstant sym emptySymbol bt
          return (1, MapF.singleton v . GVW <$> generateByType bt, v)

    f (TFloatPZero fpp) =
       do e <- floatPZero sym fpp
          return (0, pure MapF.empty, e)

    f (TFloatNZero fpp) =
       do e <- floatNZero sym fpp
          return (0, pure MapF.empty, e)

    f (TFloatNaN fpp) =
        do e <- floatNaN sym fpp
           return (0, pure MapF.empty, e)

    f (TFloatUnOp op x) =
        do (xn,xg,xe) <- f x
           e <- case op of
                  FNeg     -> floatNeg sym xe
                  FAbs     -> floatAbs sym xe
                  FSqrt  r -> floatSqrt sym r xe
                  FRound r -> floatRound sym r xe
           return (xn,xg, e)

    f (TFloatBinOp op x y) =
        do (xn,xg,xe) <- f x
           (yn,yg,ye) <- f y
           e <- case op of
                  FAdd r -> floatAdd sym r xe ye
                  FSub r -> floatSub sym r xe ye
                  FMul r -> floatMul sym r xe ye
                  FDiv r -> floatDiv sym r xe ye
                  FRem   -> floatRem sym xe ye
                  FMin   -> floatMin sym xe ye
                  FMax   -> floatMax sym xe ye

           return (xn+yn, MapF.union <$> xg <*> yg, e)

    f (TFloatTest op x) =
        do (xn,xg,xe) <- f x
           e <- case op of
                  FIsNaN  -> floatIsNaN sym xe
                  FIsInf  -> floatIsInf sym xe
                  FIsZero -> floatIsZero sym xe
                  FIsPos  -> floatIsPos sym xe
                  FIsNeg  -> floatIsNeg sym xe
                  FIsSubnorm -> floatIsSubnorm sym xe
                  FIsNorm -> floatIsNorm sym xe
           return (xn, xg, e)

    f (TFloatRel op x y) =
        do (xn,xg,xe) <- f x
           (yn,yg,ye) <- f y
           e <- case op of
                  FLogicEq   -> floatEq sym xe ye
                  FLogicNeq  -> floatNe sym xe ye
                  FEq        -> floatFpEq sym xe ye
                  FApart     -> floatFpApart sym xe ye
                  FUnordered -> floatFpUnordered sym xe ye
                  FLe        -> floatLe sym xe ye
                  FLt        -> floatLt sym xe ye
                  FGe        -> floatGe sym xe ye
                  FGt        -> floatGt sym xe ye

           return (xn+yn, MapF.union <$> xg <*> yg, e)

    f (TFloatFMA r x y z) =
        do (xn,xg,xe) <- f x
           (yn,yg,ye) <- f y
           (zn,zg,ze) <- f z
           e <- floatFMA sym r xe ye ze
           return (xn+yn+zn, foldr MapF.union MapF.empty <$> sequence [xg,yg,zg], e)

    f (TFloatFromBits fpp x) =
        do (xn,xg,xe) <- f x
           e <- floatFromBinary sym fpp xe
           return (xn,xg,e)

    f (TFloatToBits x) =
        do (xn,xg,xe) <- f x
           e <- floatToBinary sym xe
           return (xn,xg,e)

    f (TFloatCast fpp r x) =
        do (xn,xg,xe) <- f x
           e <- floatCast sym fpp r xe
           return (xn,xg,e)

    f (TFloatToReal x) =
        do (xn,xg,xe) <- f x
           e <- floatToReal sym xe
           return (xn,xg,e)

    f (TRealToFloat fpp r x) =
        do (xn,xg,xe) <- f x
           e <- realToFloat sym fpp r xe
           return (xn,xg,e)

    f (TBVToFloat fpp r sgn x) =
        do (xn,xg,xe) <- f x
           e <- case sgn of
                  False -> bvToFloat sym fpp r xe
                  True  -> sbvToFloat sym fpp r xe
           return (xn,xg,e)

    f (TFloatToBV w r sgn x) =
        do (xn,xg,xe) <- f x
           e <- case sgn of
                  False -> floatToBV sym w r xe
                  True  -> floatToSBV sym w r xe
           return (xn,xg,e)