-- | 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
  ]