{-# LANGUAGE DeriveGeneric        #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Semiring.Generic
-- Copyright   :  (C) 2018 chessai
-- License     :  MIT (see the file LICENSE)
--
-- Maintainer  :  chessai <chessai1996@gmail.com>
-- Stability   :  provisional
-- Portability :  portable
--
-- This module provides generic deriving tools for semirings and rings for
-- product-like structures.
--
----------------------------------------------------------------------------

module Data.Semiring.Generic
  (
    GSemiring(..)
  , gzero
  , gone
  , gplus
  , gtimes
  , gfromNatural
  , GRing(..)
  , gnegate
  , GenericSemiring(..)
  ) where

import           Data.Semiring
import           GHC.Generics
import           Numeric.Natural (Natural)

import Prelude hiding (Num(..))

-- | An Identity-style wrapper with a 'Generic' interface
--   to be used with '-XDerivingVia'.
newtype GenericSemiring a = GenericSemiring a

instance (Generic a, GSemiring (Rep a)) => Semiring (GenericSemiring a) where
  zero :: GenericSemiring a
zero = a -> GenericSemiring a
forall a. a -> GenericSemiring a
GenericSemiring a
forall a. (Generic a, GSemiring (Rep a)) => a
gzero
  one :: GenericSemiring a
one = a -> GenericSemiring a
forall a. a -> GenericSemiring a
GenericSemiring a
forall a. (Generic a, GSemiring (Rep a)) => a
gone
  plus :: GenericSemiring a -> GenericSemiring a -> GenericSemiring a
plus (GenericSemiring a
x) (GenericSemiring a
y) = a -> GenericSemiring a
forall a. a -> GenericSemiring a
GenericSemiring (a -> a -> a
forall a. (Generic a, GSemiring (Rep a)) => a -> a -> a
gplus a
x a
y)
  times :: GenericSemiring a -> GenericSemiring a -> GenericSemiring a
times (GenericSemiring a
x) (GenericSemiring a
y) = a -> GenericSemiring a
forall a. a -> GenericSemiring a
GenericSemiring (a -> a -> a
forall a. (Generic a, GSemiring (Rep a)) => a -> a -> a
gtimes a
x a
y)
  fromNatural :: Natural -> GenericSemiring a
fromNatural Natural
x = a -> GenericSemiring a
forall a. a -> GenericSemiring a
GenericSemiring (Natural -> a
forall a. (Generic a, GSemiring (Rep a)) => Natural -> a
gfromNatural Natural
x)

{--------------------------------------------------------------------
  Generics
--------------------------------------------------------------------}

-- | Generic 'Semiring' class, used to implement 'plus', 'times', 'zero',
--   and 'one' for product-like types implementing 'Generic'.
class GSemiring f where
  {-# MINIMAL gplus', gzero', gtimes', gone', gfromNatural' #-}
  gzero'  :: f a
  gone'   :: f a
  gplus'  :: f a -> f a -> f a
  gtimes' :: f a -> f a -> f a
  gfromNatural' :: Natural -> f a

-- | Generic 'Ring' class, used to implement 'negate' for product-like
--   types implementing 'Generic'.
class GRing f where
  {-# MINIMAL gnegate' #-}
  gnegate' :: f a -> f a

-- | Generically generate a 'Semiring' 'zero' for any product-like type
-- implementing 'Generic'.
--
-- It is only defined for product types.
--
-- @
-- 'gplus' 'gzero' a = a = 'gplus' a 'gzero'
-- @
gzero :: (Generic a, GSemiring (Rep a)) => a
gzero :: forall a. (Generic a, GSemiring (Rep a)) => a
gzero = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to Rep a Any
forall a. Rep a a
forall (f :: * -> *) a. GSemiring f => f a
gzero'

-- | Generically generate a 'Semiring' 'one' for any product-like type
-- implementing 'Generic'.
--
-- It is only defined for product types.
--
-- @
-- 'gtimes' 'gone' a = a = 'gtimes' a 'gone'
-- @
gone :: (Generic a, GSemiring (Rep a)) => a
gone :: forall a. (Generic a, GSemiring (Rep a)) => a
gone  = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to Rep a Any
forall a. Rep a a
forall (f :: * -> *) a. GSemiring f => f a
gone'

-- | Generically generate a 'Semiring' 'plus' operation for any type
-- implementing 'Generic'. It is only defined for product types.
--
-- @
-- 'gplus' a b = 'gplus' b a
-- @
gplus :: (Generic a, GSemiring (Rep a)) => a -> a -> a
gplus :: forall a. (Generic a, GSemiring (Rep a)) => a -> a -> a
gplus a
x a
y = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a) -> Rep a Any -> a
forall a b. (a -> b) -> a -> b
$ a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
x Rep a Any -> Rep a Any -> Rep a Any
forall a. Rep a a -> Rep a a -> Rep a a
forall (f :: * -> *) a. GSemiring f => f a -> f a -> f a
`gplus'` a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
y

-- | Generically generate a 'Semiring' 'times' operation for any type
-- implementing 'Generic'. It is only defined for product types.
--
-- @
-- 'gtimes' a ('gtimes' b c) = 'gtimes' ('gtimes' a b) c
-- 'gtimes' a 'gzero' = 'gzero' = 'gtimes' 'gzero' a
-- @
gtimes :: (Generic a, GSemiring (Rep a)) => a -> a -> a
gtimes :: forall a. (Generic a, GSemiring (Rep a)) => a -> a -> a
gtimes a
x a
y = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a) -> Rep a Any -> a
forall a b. (a -> b) -> a -> b
$ a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
x Rep a Any -> Rep a Any -> Rep a Any
forall a. Rep a a -> Rep a a -> Rep a a
forall (f :: * -> *) a. GSemiring f => f a -> f a -> f a
`gtimes'` a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
y

-- | Generically generate a 'Semiring' 'fromNatural' for any product-like type
-- implementing 'Generic'.
--
-- It is only defined for product types.
gfromNatural :: (Generic a, GSemiring (Rep a)) => Natural -> a
gfromNatural :: forall a. (Generic a, GSemiring (Rep a)) => Natural -> a
gfromNatural = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a) -> (Natural -> Rep a Any) -> Natural -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Rep a Any
forall a. Natural -> Rep a a
forall (f :: * -> *) a. GSemiring f => Natural -> f a
gfromNatural'

-- | Generically generate a 'Ring' 'negate' operation for any type
-- implementing 'Generic'. It is only defined for product types.
--
-- @
-- 'gplus' a ('gnegate' a) = 'zero'
-- @
gnegate :: (Generic a, GRing (Rep a)) => a -> a
gnegate :: forall a. (Generic a, GRing (Rep a)) => a -> a
gnegate a
x = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a) -> Rep a Any -> a
forall a b. (a -> b) -> a -> b
$ Rep a Any -> Rep a Any
forall a. Rep a a -> Rep a a
forall (f :: * -> *) a. GRing f => f a -> f a
gnegate' (Rep a Any -> Rep a Any) -> Rep a Any -> Rep a Any
forall a b. (a -> b) -> a -> b
$ a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
x

instance GSemiring U1 where
  gzero' :: forall a. U1 a
gzero' = U1 a
forall k (p :: k). U1 p
U1
  gone' :: forall a. U1 a
gone'  = U1 a
forall k (p :: k). U1 p
U1
  gplus' :: forall a. U1 a -> U1 a -> U1 a
gplus'  U1 a
_ U1 a
_ = U1 a
forall k (p :: k). U1 p
U1
  gtimes' :: forall a. U1 a -> U1 a -> U1 a
gtimes' U1 a
_ U1 a
_ = U1 a
forall k (p :: k). U1 p
U1
  gfromNatural' :: forall a. Natural -> U1 a
gfromNatural' Natural
_ = U1 a
forall k (p :: k). U1 p
U1

instance GRing U1 where
  gnegate' :: forall a. U1 a -> U1 a
gnegate' U1 a
_ = U1 a
forall k (p :: k). U1 p
U1

instance (GSemiring a, GSemiring b) => GSemiring (a :*: b) where
  gzero' :: forall a. (:*:) a b a
gzero' = a a
forall a. a a
forall (f :: * -> *) a. GSemiring f => f a
gzero' a a -> b a -> (:*:) a b a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b a
forall a. b a
forall (f :: * -> *) a. GSemiring f => f a
gzero'
  gone' :: forall a. (:*:) a b a
gone'  = a a
forall a. a a
forall (f :: * -> *) a. GSemiring f => f a
gone'  a a -> b a -> (:*:) a b a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b a
forall a. b a
forall (f :: * -> *) a. GSemiring f => f a
gone'
  gplus' :: forall a. (:*:) a b a -> (:*:) a b a -> (:*:) a b a
gplus'  (a a
a :*: b a
b) (a a
c :*: b a
d) = a a -> a a -> a a
forall a. a a -> a a -> a a
forall (f :: * -> *) a. GSemiring f => f a -> f a -> f a
gplus'  a a
a a a
c a a -> b a -> (:*:) a b a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b a -> b a -> b a
forall a. b a -> b a -> b a
forall (f :: * -> *) a. GSemiring f => f a -> f a -> f a
gplus' b a
b b a
d
  gtimes' :: forall a. (:*:) a b a -> (:*:) a b a -> (:*:) a b a
gtimes' (a a
a :*: b a
b) (a a
c :*: b a
d) = a a -> a a -> a a
forall a. a a -> a a -> a a
forall (f :: * -> *) a. GSemiring f => f a -> f a -> f a
gtimes' a a
a a a
c a a -> b a -> (:*:) a b a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b a -> b a -> b a
forall a. b a -> b a -> b a
forall (f :: * -> *) a. GSemiring f => f a -> f a -> f a
gtimes' b a
b b a
d
  gfromNatural' :: forall a. Natural -> (:*:) a b a
gfromNatural' Natural
n = Natural -> a a
forall a. Natural -> a a
forall (f :: * -> *) a. GSemiring f => Natural -> f a
gfromNatural' Natural
n a a -> b a -> (:*:) a b a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Natural -> b a
forall a. Natural -> b a
forall (f :: * -> *) a. GSemiring f => Natural -> f a
gfromNatural' Natural
n

instance (GRing a, GRing b) => GRing (a :*: b) where
  gnegate' :: forall a. (:*:) a b a -> (:*:) a b a
gnegate' (a a
a :*: b a
b) = a a -> a a
forall a. a a -> a a
forall (f :: * -> *) a. GRing f => f a -> f a
gnegate' a a
a a a -> b a -> (:*:) a b a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b a -> b a
forall a. b a -> b a
forall (f :: * -> *) a. GRing f => f a -> f a
gnegate' b a
b

instance (GSemiring a) => GSemiring (M1 i c a) where
  gzero' :: forall a. M1 i c a a
gzero' = a a -> M1 i c a a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 a a
forall a. a a
forall (f :: * -> *) a. GSemiring f => f a
gzero'
  gone' :: forall a. M1 i c a a
gone'  = a a -> M1 i c a a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 a a
forall a. a a
forall (f :: * -> *) a. GSemiring f => f a
gone'
  gplus' :: forall a. M1 i c a a -> M1 i c a a -> M1 i c a a
gplus'  (M1 a a
x) (M1 a a
y) = a a -> M1 i c a a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (a a -> M1 i c a a) -> a a -> M1 i c a a
forall a b. (a -> b) -> a -> b
$ a a -> a a -> a a
forall a. a a -> a a -> a a
forall (f :: * -> *) a. GSemiring f => f a -> f a -> f a
gplus'  a a
x a a
y
  gtimes' :: forall a. M1 i c a a -> M1 i c a a -> M1 i c a a
gtimes' (M1 a a
x) (M1 a a
y) = a a -> M1 i c a a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (a a -> M1 i c a a) -> a a -> M1 i c a a
forall a b. (a -> b) -> a -> b
$ a a -> a a -> a a
forall a. a a -> a a -> a a
forall (f :: * -> *) a. GSemiring f => f a -> f a -> f a
gtimes' a a
x a a
y
  gfromNatural' :: forall a. Natural -> M1 i c a a
gfromNatural' = a a -> M1 i c a a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (a a -> M1 i c a a) -> (Natural -> a a) -> Natural -> M1 i c a a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> a a
forall a. Natural -> a a
forall (f :: * -> *) a. GSemiring f => Natural -> f a
gfromNatural'

instance (GRing a) => GRing (M1 i c a) where
  gnegate' :: forall a. M1 i c a a -> M1 i c a a
gnegate' (M1 a a
x) = a a -> M1 i c a a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (a a -> M1 i c a a) -> a a -> M1 i c a a
forall a b. (a -> b) -> a -> b
$ a a -> a a
forall a. a a -> a a
forall (f :: * -> *) a. GRing f => f a -> f a
gnegate' a a
x

instance (Semiring a) => GSemiring (K1 i a) where
  gzero' :: forall a. K1 i a a
gzero' = a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 a
forall a. Semiring a => a
zero
  gone' :: forall a. K1 i a a
gone'  = a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 a
forall a. Semiring a => a
one
  gplus' :: forall a. K1 i a a -> K1 i a a -> K1 i a a
gplus'  (K1 a
x) (K1 a
y) = a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (a -> K1 i a a) -> a -> K1 i a a
forall a b. (a -> b) -> a -> b
$ a -> a -> a
forall a. Semiring a => a -> a -> a
plus  a
x a
y
  gtimes' :: forall a. K1 i a a -> K1 i a a -> K1 i a a
gtimes' (K1 a
x) (K1 a
y) = a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (a -> K1 i a a) -> a -> K1 i a a
forall a b. (a -> b) -> a -> b
$ a -> a -> a
forall a. Semiring a => a -> a -> a
times a
x a
y
  gfromNatural' :: forall a. Natural -> K1 i a a
gfromNatural' = a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (a -> K1 i a a) -> (Natural -> a) -> Natural -> K1 i a a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> a
forall a. Semiring a => Natural -> a
fromNatural

instance (Ring a) => GRing (K1 i a) where
  gnegate' :: forall a. K1 i a a -> K1 i a a
gnegate' (K1 a
x) = a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (a -> K1 i a a) -> a -> K1 i a a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Ring a => a -> a
negate a
x