{-# OPTIONS_GHC -Wunused-imports #-}
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 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)
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)