module Agda.Utils.SemiRing where

-- | Semirings (<https://en.wikipedia.org/wiki/Semiring>).

class SemiRing a where
  ozero  :: a
  oone   :: a
  oplus  :: a -> a -> a
  otimes :: a -> a -> a

instance SemiRing () where
  ozero      = ()
  oone       = ()
  oplus  _ _ = ()
  otimes _ _ = ()

instance SemiRing a => SemiRing (Maybe a) where
  ozero = Nothing
  oone  = Just oone

  oplus Nothing y = y
  oplus x Nothing = x
  oplus (Just x) (Just y) = Just (oplus x y)

  otimes Nothing _ = Nothing
  otimes _ Nothing = Nothing
  otimes (Just x) (Just y) = Just (otimes x y)

-- | Star semirings
-- (<https://en.wikipedia.org/wiki/Semiring#Star_semirings>).

class SemiRing a => StarSemiRing a where
  ostar :: a -> a

instance StarSemiRing () where
  ostar _ = ()

instance StarSemiRing a => StarSemiRing (Maybe a) where
  ostar Nothing  = oone
  ostar (Just x) = Just (ostar x)