Semiring.hs

{-# OPTIONS_GHC -Wunused-imports #-}

-- | 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
  { add  :: a -> a -> a  -- ^ Addition.
  , mul  :: a -> a -> a  -- ^ Multiplication.
  , 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 = 0

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

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

instance HasZero Int where
  zeroElement = 0

intSemiring :: Semiring Int
intSemiring = Semiring { add = (+), mul = (*), zero = 0 } -- , one = 1 }

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

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