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 Maybe a
Nothing Maybe a
y = Maybe a
y
  oplus Maybe a
x Maybe a
Nothing = Maybe a
x
  oplus (Just a
x) (Just 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 Maybe a
Nothing Maybe a
_ = Maybe a
forall a. Maybe a
Nothing
  otimes Maybe a
_ Maybe a
Nothing = Maybe a
forall a. Maybe a
Nothing
  otimes (Just a
x) (Just 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 Maybe a
Nothing  = Maybe a
forall a. SemiRing a => a
oone
  ostar (Just a
x) = a -> Maybe a
forall a. a -> Maybe a
Just (a -> a
forall a. StarSemiRing a => a -> a
ostar a
x)