content: -----------------------------------------------------------------------------
  -- |
  -- Module    : BenchSuite.BitPrecise.BrokenSearch
  -- Copyright : (c) Jeffrey Young
  --                 Levent Erkok
  -- License   : BSD3
  -- Maintainer: erkokl@gmail.com
  -- Stability : experimental
  --
  -- Bench suite for Documentation.SBV.Examples.BitPrecise.BrokenSearch
  -----------------------------------------------------------------------------
  
  {-# OPTIONS_GHC -Wall -Werror #-}
  
  module BenchSuite.BitPrecise.BrokenSearch(benchmarks) where
  
  import Documentation.SBV.Examples.BitPrecise.BrokenSearch
  import BenchSuite.Bench.Bench as B
  
  import Data.SBV (proveWith,sInt32,(.>=),(.<=),(.==),sFromIntegral,SInt64,sDiv,constrain)
  
  -- benchmark suite
  benchmarks :: Runner
  benchmarks = rGroup
    [ B.run  "Arith.MidPointFixed"  (checkCorrect midPointFixed)        `using` runner Data.SBV.proveWith
    , B.run  "Arith-Overflow"       (checkCorrect midPointAlternative)  `using` runner Data.SBV.proveWith
    ]
  
    where checkCorrect f = do low  <- sInt32 "low"
                              high <- sInt32 "high"
  
                              constrain $ low .>= 0
                              constrain $ low .<= high
  
                              let low', high' :: SInt64
                                  low'  = sFromIntegral low
                                  high' = sFromIntegral high
                                  mid'  = (low' + high') `sDiv` 2
  
                                  mid   = f low high
  
                              return $ sFromIntegral mid .== mid'
  