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 :: ()
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)
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)