module Agda.Termination.Semiring
( HasZero(..), SemiRing(..)
, Semiring(..)
, semiringInvariant
, integerSemiring
, boolSemiring
, Agda.Termination.Semiring.tests
) where
import Data.Monoid
import Agda.Utils.QuickCheck
import Agda.Utils.TestHelpers
class (Eq a, Monoid a) => SemiRing a where
multiply :: a -> a -> a
class Eq a => HasZero a where
zeroElement :: a
data Semiring a
= Semiring { add :: a -> a -> a
, mul :: a -> a -> a
, zero :: a
}
semiringInvariant :: (Arbitrary a, Eq a, Show a)
=> Semiring a
-> a -> a -> a -> Bool
semiringInvariant (Semiring { add = (+), mul = (*)
, zero = zero
}) = \x y z ->
associative (+) x y z &&
identity zero (+) x &&
commutative (+) x y &&
associative (*) x y z &&
leftDistributive (*) (+) x y z &&
rightDistributive (*) (+) x y z &&
isZero zero (*) x
instance HasZero Integer where
zeroElement = 0
instance Monoid Integer where
mempty = 0
mappend = (+)
instance SemiRing Integer where
multiply = (*)
integerSemiring :: Semiring Integer
integerSemiring = Semiring { add = (+), mul = (*), zero = 0 }
prop_integerSemiring = semiringInvariant integerSemiring
boolSemiring :: Semiring Bool
boolSemiring =
Semiring { add = (||), mul = (&&), zero = False }
prop_boolSemiring = semiringInvariant boolSemiring
tests :: IO Bool
tests = runTests "Agda.Termination.Semiring"
[ quickCheck' prop_integerSemiring
, quickCheck' prop_boolSemiring
]