-- | 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 { add :: Integer -> Integer -> Integer
add = forall a. Num a => a -> a -> a
(+), mul :: Integer -> Integer -> Integer
mul = 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 { add :: Int -> Int -> Int
add = forall a. Num a => a -> a -> a
(+), mul :: Int -> Int -> Int
mul = 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 { add :: Bool -> Bool -> Bool
add = Bool -> Bool -> Bool
(||), mul :: Bool -> Bool -> Bool
mul = Bool -> Bool -> Bool
(&&), zero :: Bool
zero = Bool
False } --, one = True }