content: -----------------------------------------------------------------------------
  -- |
  -- Module    : BenchSuite.WeakestPreconditions.Basics
  -- Copyright : (c) Jeffrey Young
  --                 Levent Erkok
  -- License   : BSD3
  -- Maintainer: erkokl@gmail.com
  -- Stability : experimental
  --
  -- Bench suite for Documentation.SBV.Examples.WeakestPreconditions.Basics
  -----------------------------------------------------------------------------
  
  {-# OPTIONS_GHC -fno-warn-orphans #-}
  {-# LANGUAGE NamedFieldPuns #-}
  
  module BenchSuite.WeakestPreconditions.Basics(benchmarks) where
  
  import Documentation.SBV.Examples.WeakestPreconditions.Basics
  import Data.SBV
  import Data.SBV.Tools.WeakestPreconditions
  
  import Control.DeepSeq
  import BenchSuite.Bench.Bench
  import BenchSuite.WeakestPreconditions.Instances()
  
  instance NFData a => NFData (IncS a)
  
  
  benchmarks :: Runner
  benchmarks = rGroup
    [ runIO "Correctness.Basics skip"        $ correctness Skip Skip
    , runIO "Correctness.Basics y+1"         $ correctness Skip $ Assign $ \st@IncS{y} -> st{y = y+1}
    , runIO "Correctness.Basics x>0"         $ correctness (assert "x > 0" (\IncS{x} -> x .> 0)) Skip
    , runIO "Correctness.Basics x>-5"        $ correctness (assert "x > -5" (\IncS{x} -> x .> -5)) Skip
    , runIO "Correctness.Basics y is even"   $ correctness Skip (assert "y is even" (\IncS{y} -> y `sMod` 2 .== 0))
    , runIO "Correctness.Basics y > x"       $ correctness Skip (assert "y > x" (\IncS{x, y} -> y .> x))
    , runIO "Correctness.Basics skip-assign" $ correctness Skip (Assign $ \st -> st{x = 10, y = 11})
    ]
  