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 :: ()
ozero      = ()
  oone :: ()
oone       = ()
  oplus :: () -> () -> ()
oplus  _ _ = ()
  otimes :: () -> () -> ()
otimes _ _ = ()

instance SemiRing a => SemiRing (Maybe a) where
  ozero :: Maybe a
ozero = Maybe a
forall a. Maybe a
Nothing
  oone :: Maybe a
oone  = a -> Maybe a
forall a. a -> Maybe a
Just a
forall a. SemiRing a => a
oone

  oplus :: Maybe a -> Maybe a -> Maybe a
oplus Nothing y :: Maybe a
y = Maybe a
y
  oplus x :: Maybe a
x Nothing = Maybe a
x
  oplus (Just x :: a
x) (Just y :: a
y) = a -> Maybe a
forall a. a -> Maybe a
Just (a -> a -> a
forall a. SemiRing a => a -> a -> a
oplus a
x a
y)

  otimes :: Maybe a -> Maybe a -> Maybe a
otimes Nothing _ = Maybe a
forall a. Maybe a
Nothing
  otimes _ Nothing = Maybe a
forall a. Maybe a
Nothing
  otimes (Just x :: a
x) (Just y :: a
y) = a -> Maybe a
forall a. a -> Maybe a
Just (a -> a -> a
forall a. SemiRing a => a -> a -> a
otimes a
x a
y)

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

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

instance StarSemiRing () where
  ostar :: () -> ()
ostar _ = ()

instance StarSemiRing a => StarSemiRing (Maybe a) where
  ostar :: Maybe a -> Maybe a
ostar Nothing  = Maybe a
forall a. SemiRing a => a
oone
  ostar (Just x :: a
x) = a -> Maybe a
forall a. a -> Maybe a
Just (a -> a
forall a. StarSemiRing a => a -> a
ostar a
x)