-----------------------------------------------------------------------------
-- |
-- Module    : BenchSuite.Misc.SetAlgebra
-- Copyright : (c) Jeffrey Young
--                 Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Bench suite for Documentation.SBV.Examples.Misc.SetAlgebra
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

{-# LANGUAGE ScopedTypeVariables #-}

module BenchSuite.Misc.SetAlgebra(benchmarks) where

import Data.SBV hiding (complement)
import Data.SBV.Set
import Documentation.SBV.Examples.Misc.SetAlgebra

import BenchSuite.Bench.Bench


-- benchmark suite
benchmarks :: Runner
benchmarks =  rGroup $ fmap (`using` _prove)
              [ run "Commutivity.Union"           commutivityCup
              , run "Commutivity.Intersection"    commutivityCap
              , run "Associativity.Union"         assocCup
              , run "Associativity.Intersection"  assocCap
              , run "Distributivity.Union"        distribCup
              , run "Distributivity.Intersection" distribCap
              , run "Identity.Union"              identCup
              , run "Identity.Intersection"       identCap
              , run "Complement.Union"            compCup
              , run "Complement.Intersection"     compCap
              , run "Complement.Empty"            compEmpty
              , run "Complement.Complement"       compComp
              , run "Complement.Full"             compFull
              , run "Complement.Unique"           compUniq
              , run "Idempotency.Cup"             idempCup
              , run "Idempotency.Cap"             idempCap
              , run "Domination.Cup"              domCup
              , run "Domination.Cap"              domCap
              , run "Absorption.Cup"              absorbCup
              , run "Absorption.Cap"              absorbCap
              , run "Intersection.Difference"     intdiff
              , run "DeMorgans.Cup"               demorgCup
              , run "DeMorgans.Cap"               demorgCap
              , run "InclusionIsPO"               incPo
              , run "SubsetEquality"              subEq
              , run "SubsetEquality.Transitivity" subEqTrans
              , run "JoinMeet.1"                  joinMeet1
              , run "JoinMeet.2"                  joinMeet2
              , run "JoinMeet.3"                  joinMeet3
              , run "JoinMeet.4"                  joinMeet4
              , run "JoinMeet.5"                  joinMeet5
              , run "SubsetChar.Union"            subsetCharCup
              , run "SubsetChar.Intersection"     subsetCharCap
              , run "SubsetChar.Implication"      subsetCharImpl
              , run "SubsetChar.Complement"       subsetCharComp

              , run "RelativeComplements.Union"              relCompCup
              , run "RelativeComplements.Intersection"       relCompCap
              , run "RelativeComplements.UnionInters"        relCompCapCup
              , run "RelativeComplements.InterInters.1"      relCompCapCap
              , run "RelativeComplements.InterInters.2"      relCompCapCap2
              , run "RelativeComplements.UnionUnion"         relCompCupCup
              , run "RelativeComplements.Identity"           relCompIdent
              , run "RelativeComplements.UnitLeft"           relCompUnitL
              , run "RelativeComplements.UnitRight"          relCompUnitR
              , run "RelativeComplements.ComplementIdentity" relCompCompInt
              , run "RelativeComplements.ComplementUnion"    relCompCompUni
              , run "RelativeComplements.CompComp"           relCompComp
              , run "RelativeComplements.CompFull"           relCompFull
              , run "DistributionSubset.Union"               distSubset1
              , run "DistributionSubset.Intersection"        distSubset2
              ]
  where _prove = runner proveWith
        commutivityCup = \(a :: SI) b -> a `union` b .== b `union` a
        commutivityCap = \(a :: SI) b -> a `intersection` b .== b `intersection` a
        assocCup       = \(a :: SI) b c -> a `union` (b `union` c) .== (a `union` b) `union` c
        assocCap       = \(a :: SI) b c -> a `intersection` (b `intersection` c) .== (a `intersection` b) `intersection` c
        distribCup     = \(a :: SI) b c -> a `union` (b `intersection` c) .== (a `union` b) `intersection` (a `union` c)
        distribCap     = \(a :: SI) b c -> a `intersection` (b `union` c) .== (a `intersection` b) `union` (a `intersection` c)
        identCup       = \(a :: SI) -> a `union` empty .== a
        identCap       = \(a :: SI) -> a `intersection` full .== a
        compCup        = \(a :: SI) -> a `union` complement a .== full
        compCap        = \(a :: SI) -> a `intersection` complement a .== empty
        compEmpty      = complement (empty :: SI) .== full
        compComp       = \(a :: SI) -> complement (complement a) .== a
        compFull       = complement (full :: SI) .== empty
        compUniq       = \(a :: SI) b -> a `union` b .== full .&& a `intersection` b .== empty .<=> b .== complement a
        idempCup       = \(a :: SI) -> a `union` a .== a
        idempCap       = \(a :: SI) -> a `intersection` a .== a
        domCup         = \(a :: SI) -> a `union` full .== full
        domCap         = \(a :: SI) -> a `intersection` empty .== empty
        absorbCup      = \(a :: SI) b -> a `union` (a `intersection` b) .== a
        absorbCap      = \(a :: SI) b -> a `intersection` (a `union` b) .== a
        intdiff        = \(a :: SI) b -> a `intersection` b .== a `difference` (a `difference` b)
        demorgCup      = \(a :: SI) b -> complement (a `union` b) .== complement a `intersection` complement b
        demorgCap      = \(a :: SI) b -> complement (a `intersection` b) .== complement a `union` complement b
        incPo          = \(a :: SI) -> a `isSubsetOf` a
        subEq          = \(a :: SI) b -> a `isSubsetOf` b .&& b `isSubsetOf` a .<=> a .== b
        subEqTrans     = \(a :: SI) b c -> a `isSubsetOf` b .&& b `isSubsetOf` c .=> a `isSubsetOf` c
        joinMeet1      = \(a :: SI) b -> a `isSubsetOf` (a `union` b)
        joinMeet2      = \(a :: SI) b c -> a `isSubsetOf` c .&& b `isSubsetOf` c .=> (a `union` b) `isSubsetOf` c
        joinMeet3      = \(a :: SI) b -> (a `intersection` b) `isSubsetOf` a
        joinMeet4      = \(a :: SI) b -> (a `intersection` b) `isSubsetOf` b
        joinMeet5      = \(a :: SI) b c -> c `isSubsetOf` a .&& c `isSubsetOf` b .=> c `isSubsetOf` (a `intersection` b)
        subsetCharCup  = \(a :: SI) b -> a `isSubsetOf` b .<=> a `union` b .== b
        subsetCharCap  = \(a :: SI) b -> a `isSubsetOf` b .<=> a `intersection` b .== a
        subsetCharImpl = \(a :: SI) b -> a `isSubsetOf` b .<=> a `difference` b .== empty
        subsetCharComp = \(a :: SI) b -> a `isSubsetOf` b .<=> complement b `isSubsetOf` complement a
        relCompCup     = \(a :: SI) b c -> c \\ (a `union` b) .== (c \\ a) `intersection` (c \\ b)
        relCompCap     = \(a :: SI) b c -> c \\ (a `intersection` b) .== (c \\ a) `union` (c \\ b)
        relCompCapCup  = \(a :: SI) b c -> c \\ (b \\ a) .== (a `intersection` c) `union` (c \\ b)
        relCompCapCap  = \(a :: SI) b c -> (b \\ a) `intersection` c .== (b `intersection` c) \\ a
        relCompCapCap2 = \(a :: SI) b c -> (b \\ a) `intersection` c .== b `intersection` (c \\ a)
        relCompCupCup  = \(a :: SI) b c -> (b \\ a) `union` c .== (b `union` c) \\ (a \\ c)
        relCompIdent   = \(a :: SI) -> a \\ a .== empty
        relCompUnitL   = \(a :: SI) -> empty \\ a .== empty
        relCompUnitR   = \(a :: SI) -> empty \\ empty .== a
        relCompCompInt = \(a :: SI) b -> b \\ a .== complement a `intersection` b
        relCompCompUni = \(a :: SI) b -> complement (b \\ a) .== a `union` complement b
        relCompComp    = \(a :: SI) -> full \\ a .== complement a
        relCompFull    = \(a :: SI) -> a \\ full .== empty
        distSubset1    = \(a :: SI) b c -> a `isSubsetOf` (b `union` c) .=> a `isSubsetOf` b .&& a `isSubsetOf` c
        distSubset2    = \(a :: SI) b c -> (b `intersection` c) `isSubsetOf` a .=> b `isSubsetOf` a .&& c `isSubsetOf` a