-----------------------------------------------------------------------------

-- Copyright 2019, Ideas project team. This file is distributed under the

-- terms of the Apache License 2.0. For more information, see the files

-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.

-----------------------------------------------------------------------------

-- |

-- Maintainer  :  bastiaan.heeren@ou.nl

-- Stability   :  provisional

-- Portability :  portable (depends on ghc)

--

-----------------------------------------------------------------------------


module Domain.Algebra.FieldLaws
   ( -- * Semi-ring laws

     leftDistributive, rightDistributive
   , distributiveLaws, semiRingLaws
     -- * Ring laws

   , leftNegateTimes, rightNegateTimes
   , negateTimesLaws, ringLaws, commutativeRingLaws
   , distributiveSubtractionLaws
     -- * Field laws

   , exchangeInverses, fieldLaws
     -- * Laws for additive monoid

   , fromAdditiveLaw
     -- * Laws for multiplicative monoid

   , fromMultiplicativeLaw
     -- * Properties

   , propsField
   ) where

import Domain.Algebra.Field
import Domain.Algebra.GroupLaws
import Domain.Algebra.Law
import Test.QuickCheck

--------------------------------------------------------

-- Semi-ring laws


leftDistributive :: SemiRing a => Law a
leftDistributive = leftDistributiveFor (|*|) (|+|)

rightDistributive :: SemiRing a => Law a
rightDistributive = rightDistributiveFor (|*|) (|+|)

distributiveLaws :: SemiRing a => [Law a]
distributiveLaws = [leftDistributive, rightDistributive]

semiRingLaws :: SemiRing a => [Law a]
semiRingLaws =
   map fromAdditiveLaw commutativeMonoidLaws ++
   map fromMultiplicativeLaw monoidZeroLaws ++
   distributiveLaws

--------------------------------------------------------

-- Ring laws


leftNegateTimes :: Ring a => Law a
leftNegateTimes = law "left-negate-times" $ \a b ->
   plusInverse a |*| b :==: plusInverse (a |*| b)

rightNegateTimes :: Ring a => Law a
rightNegateTimes = law "right-negate-times" $ \a b ->
   a |*| plusInverse b :==: plusInverse (a |*| b)

negateTimesLaws :: Ring a => [Law a]
negateTimesLaws = [leftNegateTimes, rightNegateTimes]

ringLaws :: Ring a => [Law a]
ringLaws =
   map fromAdditiveLaw abelianGroupLaws ++
   map fromMultiplicativeLaw monoidZeroLaws ++
   distributiveLaws ++ negateTimesLaws

commutativeRingLaws :: Ring a => [Law a]
commutativeRingLaws =
   fromMultiplicativeLaw commutative : ringLaws

distributiveSubtractionLaws :: Ring a => [Law a]
distributiveSubtractionLaws =
   [leftDistributiveFor (|*|) (|-|), rightDistributiveFor (|*|) (|-|)]

--------------------------------------------------------

-- Field laws


exchangeInverses :: Field a => Law a
exchangeInverses = law "exchange-inverses" $ \a ->
   timesInverse (plusInverse a) :==: plusInverse (timesInverse a)

fieldLaws :: Field a => [Law a]
fieldLaws =
   map fromAdditiveLaw abelianGroupLaws ++
   map fromMultiplicativeLaw abelianGroupLaws ++
   distributiveLaws ++ negateTimesLaws ++ [exchangeInverses]

--------------------------------------------------------

-- Laws for additive monoid


fromAdditiveLaw :: Law (Additive a) -> Law a
fromAdditiveLaw = mapLaw Additive fromAdditive

--------------------------------------------------------

-- Laws for multiplicative monoid


fromMultiplicativeLaw :: Law (Multiplicative a) -> Law a
fromMultiplicativeLaw = mapLaw Multiplicative fromMultiplicative

--------------------------------------------------------

-- Properties


propsField :: [Property]
propsField = map property (fieldLaws :: [Law (SafeNum Rational)])