    -- | Semirings.

    module Agda.Termination.Semiring
      ( HasZero(..)
      , Semiring(..)
      , integerSemiring
      , intSemiring
      , boolSemiring
      ) where

    -- | @HasZero@ is needed for sparse matrices, to tell which is the element
    --   that does not have to be stored.
    --   It is a cut-down version of @SemiRing@ which is definable
    --   without the implicit @?cutoff@.
    class Eq a => HasZero a where
      zeroElement :: a

    -- | Semirings.

    data Semiring a = Semiring
      { forall a. Semiring a -> a -> a -> a
    add  :: a -> a -> a  -- ^ Addition.
      , forall a. Semiring a -> a -> a -> a
    mul  :: a -> a -> a  -- ^ Multiplication.
      , forall a. Semiring a -> a
    zero :: a            -- ^ Zero.
      -- The one is never used in matrix multiplication
      -- , one  :: a            -- ^ One.
      }

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

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

    instance HasZero Integer where
      zeroElement :: Integer
    zeroElement = Integer
    0

    integerSemiring :: Semiring Integer
    integerSemiring :: Semiring Integer
    integerSemiring = Semiring :: forall a. (a -> a -> a) -> (a -> a -> a) -> a -> Semiring a
    Semiring { add :: Integer -> Integer -> Integer
    add = Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    (+), mul :: Integer -> Integer -> Integer
    mul = Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    (*), zero :: Integer
    zero = Integer
    0 } -- , one = 1 }

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

    instance HasZero Int where
      zeroElement :: Int
    zeroElement = Int
    0

    intSemiring :: Semiring Int
    intSemiring :: Semiring Int
    intSemiring = Semiring :: forall a. (a -> a -> a) -> (a -> a -> a) -> a -> Semiring a
    Semiring { add :: Int -> Int -> Int
    add = Int -> Int -> Int
    forall a. Num a => a -> a -> a
    (+), mul :: Int -> Int -> Int
    mul = Int -> Int -> Int
    forall a. Num a => a -> a -> a
    (*), zero :: Int
    zero = Int
    0 } -- , one = 1 }

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

    boolSemiring :: Semiring Bool
    boolSemiring :: Semiring Bool
    boolSemiring =
      Semiring :: forall a. (a -> a -> a) -> (a -> a -> a) -> a -> Semiring a
    Semiring { add :: Bool -> Bool -> Bool
    add = Bool -> Bool -> Bool
    (||), mul :: Bool -> Bool -> Bool
    mul = Bool -> Bool -> Bool
    (&&), zero :: Bool
    zero = Bool
    False } --, one = True }