content: -----------------------------------------------------------------------------
  -- |
  -- Module    : BenchSuite.WeakestPreconditions.Sum
  -- Copyright : (c) Jeffrey Young
  --                 Levent Erkok
  -- License   : BSD3
  -- Maintainer: erkokl@gmail.com
  -- Stability : experimental
  --
  -- Bench suite for Documentation.SBV.Examples.WeakestPreconditions.Sum
  -----------------------------------------------------------------------------
  
  {-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}
  {-# LANGUAGE NamedFieldPuns #-}
  
  module BenchSuite.WeakestPreconditions.Sum(benchmarks) where
  
  import Documentation.SBV.Examples.WeakestPreconditions.Sum
  import Data.SBV
  
  import Control.DeepSeq
  import BenchSuite.Bench.Bench
  import BenchSuite.WeakestPreconditions.Instances()
  
  instance NFData a => NFData (SumS a)
  
  
  benchmarks :: Runner
  benchmarks = rGroup [ runIO "Correctness.Sum.correctInvariant"     $ correctness correctInvariant (Just measure)
                      , runIO "Correctness.Sum.alwaysFalseInvariant" $ correctness alwaysFalseInvariant Nothing
                      , runIO "Correctness.Sum.alwaysTrueInvariant"  $ correctness alwaysTrueInvariant Nothing
                      , runIO "Correctness.Sum.loopInvariant"        $ correctness loopInvariant Nothing
                      , runIO "Correctness.Sum.badMeasure1"          $ correctness badMeasure1Invariant (Just badMeasure1)
                      , runIO "Correctness.Sum.badMeasure2"          $ correctness badMeasure2Invariant (Just badMeasure2)
                      ]
               where
                 correctInvariant     SumS{n, i, s} = s .== (i*(i+1)) `sDiv` 2 .&& i .<= n
                 measure              SumS{n, i}    = [n - i]
                 alwaysFalseInvariant _             = sFalse
                 alwaysTrueInvariant  _             =  sTrue
                 loopInvariant        SumS{n, i, s} = s .<= i .&& s .== (i*(i+1)) `sDiv` 2 .&& i .<= n
                 badMeasure1Invariant SumS{n, i, s} = s .== (i*(i+1)) `sDiv` 2 .&& i .<= n
                 badMeasure1          SumS{i}       = [- i]
                 badMeasure2Invariant SumS{n, i, s} = s .== (i*(i+1)) `sDiv` 2 .&& i .<= n
                 badMeasure2          SumS{n, i}    = [n + i]
  