module Agda.Utils.SemiRing where
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)
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)