    -- | Semirings.

    module Agda.Termination.Semiring
      ( Semiring(..)
      , semiringInvariant
      , integerSemiring
      , boolSemiring
      , Agda.Termination.Semiring.tests
      ) where

    import Agda.Utils.QuickCheck
    import Agda.Utils.TestHelpers

    -- | Semirings.

    data Semiring a
      = Semiring { add  :: a -> a -> a  -- ^ Addition.
                 , mul  :: a -> a -> a  -- ^ Multiplication.
                 , zero :: a            -- ^ Zero.
                 , one  :: a            -- ^ One.
                 }

    -- | Semiring invariant.

    -- I think it's OK to use the same x, y, z triple for all the
    -- properties below.

    semiringInvariant :: (Arbitrary a, Eq a, Show a)
                      => Semiring a
                      -> a -> a -> a -> Bool
    semiringInvariant (Semiring { add = (+), mul = (*)
                                , zero = zero, one = one}) = \x y z ->
      associative (+)           x y z &&
      identity zero (+)         x     &&
      commutative (+)           x y   &&
      associative (*)           x y z &&
      identity one (*)          x     &&
      leftDistributive (*) (+)  x y z &&
      rightDistributive (*) (+) x y z &&
      isZero zero (*)           x

    ------------------------------------------------------------------------
    -- Specific semirings

    -- | The standard semiring on 'Integer's.

    integerSemiring :: Semiring Integer
    integerSemiring = Semiring { add = (+), mul = (*), zero = 0, one = 1 }

    prop_integerSemiring = semiringInvariant integerSemiring

    -- | The standard semiring on 'Bool's.

    boolSemiring :: Semiring Bool
    boolSemiring =
      Semiring { add = (||), mul = (&&), zero = False, one = True }

    prop_boolSemiring = semiringInvariant boolSemiring

    ------------------------------------------------------------------------
    -- All tests

    tests :: IO Bool
    tests = runTests "Agda.Termination.Semiring"
      [ quickCheck' prop_integerSemiring
      , quickCheck' prop_boolSemiring
      ]