module Agda.Termination.Semiring
( HasZero(..)
, Semiring(..)
, integerSemiring
, intSemiring
, boolSemiring
) where
class Eq a => HasZero a where
zeroElement :: a
data Semiring a = Semiring
{ forall a. Semiring a -> a -> a -> a
add :: a -> a -> a
, forall a. Semiring a -> a -> a -> a
mul :: a -> a -> a
, forall a. Semiring a -> a
zero :: a
}
instance HasZero Integer where
zeroElement :: Integer
zeroElement = Integer
0
integerSemiring :: Semiring Integer
integerSemiring :: Semiring Integer
integerSemiring = Semiring { add :: Integer -> Integer -> Integer
add = Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+), mul :: Integer -> Integer -> Integer
mul = Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(*), zero :: Integer
zero = Integer
0 }
instance HasZero Int where
zeroElement :: Int
zeroElement = Int
0
intSemiring :: Semiring Int
intSemiring :: Semiring Int
intSemiring = Semiring { add :: Int -> Int -> Int
add = Int -> Int -> Int
forall a. Num a => a -> a -> a
(+), mul :: Int -> Int -> Int
mul = Int -> Int -> Int
forall a. Num a => a -> a -> a
(*), zero :: Int
zero = Int
0 }
boolSemiring :: Semiring Bool
boolSemiring :: Semiring Bool
boolSemiring =
Semiring { add :: Bool -> Bool -> Bool
add = Bool -> Bool -> Bool
(||), mul :: Bool -> Bool -> Bool
mul = Bool -> Bool -> Bool
(&&), zero :: Bool
zero = Bool
False }