{-# LANGUAGE RebindableSyntax #-}
module Algebra.Lattice (
      C(up, dn)
    , max, min, abs
    , propUpCommutative, propDnCommutative
    , propUpAssociative, propDnAssociative
    , propUpDnDistributive, propDnUpDistributive
) where

import qualified Algebra.PrincipalIdealDomain as PID
import qualified Algebra.Additive as Additive
import qualified Number.Ratio     as Ratio

import qualified Algebra.Laws as Laws

import NumericPrelude.Numeric hiding (abs)
import NumericPrelude.Base hiding (max, min)
import qualified Prelude as P

infixl 5 `up`, `dn`

class C a where
    up, dn :: a -> a -> a


{- * Properties -}

propUpCommutative, propDnCommutative ::
 (Eq a, C a) => a -> a -> Bool
propUpCommutative :: a -> a -> Bool
propUpCommutative  =  (a -> a -> a) -> a -> a -> Bool
forall a b. Eq a => (b -> b -> a) -> b -> b -> Bool
Laws.commutative a -> a -> a
forall a. C a => a -> a -> a
up
propDnCommutative :: a -> a -> Bool
propDnCommutative  =  (a -> a -> a) -> a -> a -> Bool
forall a b. Eq a => (b -> b -> a) -> b -> b -> Bool
Laws.commutative a -> a -> a
forall a. C a => a -> a -> a
dn

propUpAssociative, propDnAssociative ::
 (Eq a, C a) => a -> a -> a -> Bool
propUpAssociative :: a -> a -> a -> Bool
propUpAssociative  =  (a -> a -> a) -> a -> a -> a -> Bool
forall a. Eq a => (a -> a -> a) -> a -> a -> a -> Bool
Laws.associative a -> a -> a
forall a. C a => a -> a -> a
up
propDnAssociative :: a -> a -> a -> Bool
propDnAssociative  =  (a -> a -> a) -> a -> a -> a -> Bool
forall a. Eq a => (a -> a -> a) -> a -> a -> a -> Bool
Laws.associative a -> a -> a
forall a. C a => a -> a -> a
dn

propUpDnDistributive, propDnUpDistributive ::
 (Eq a, C a) => a -> a -> a -> Bool
propUpDnDistributive :: a -> a -> a -> Bool
propUpDnDistributive  =  (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool
forall a b.
Eq a =>
(a -> b -> a) -> (a -> a -> a) -> b -> a -> a -> Bool
Laws.leftDistributive a -> a -> a
forall a. C a => a -> a -> a
up a -> a -> a
forall a. C a => a -> a -> a
dn
propDnUpDistributive :: a -> a -> a -> Bool
propDnUpDistributive  =  (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool
forall a b.
Eq a =>
(a -> b -> a) -> (a -> a -> a) -> b -> a -> a -> Bool
Laws.leftDistributive a -> a -> a
forall a. C a => a -> a -> a
dn a -> a -> a
forall a. C a => a -> a -> a
up




-- With  @up == gcd@  and  @dn == lcm@  we have also a lattice.
instance C Integer where
    up :: Integer -> Integer -> Integer
up = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
P.max
    dn :: Integer -> Integer -> Integer
dn = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
P.min

instance (Ord a, PID.C a) => C (Ratio.T a) where
    up :: T a -> T a -> T a
up = T a -> T a -> T a
forall a. Ord a => a -> a -> a
P.max
    dn :: T a -> T a -> T a
dn = T a -> T a -> T a
forall a. Ord a => a -> a -> a
P.min

instance C Bool where
    up :: Bool -> Bool -> Bool
up = Bool -> Bool -> Bool
(P.||)
    dn :: Bool -> Bool -> Bool
dn = Bool -> Bool -> Bool
(P.&&)

instance (C a, C b) => C (a,b) where
    (a
x1,b
y1)up :: (a, b) -> (a, b) -> (a, b)
`up`(a
x2,b
y2) = (a
x1a -> a -> a
forall a. C a => a -> a -> a
`up`a
x2, b
y1b -> b -> b
forall a. C a => a -> a -> a
`up`b
y2)
    (a
x1,b
y1)dn :: (a, b) -> (a, b) -> (a, b)
`dn`(a
x2,b
y2) = (a
x1a -> a -> a
forall a. C a => a -> a -> a
`dn`a
x2, b
y1b -> b -> b
forall a. C a => a -> a -> a
`dn`b
y2)


max, min :: (C a) => a -> a -> a
max :: a -> a -> a
max = a -> a -> a
forall a. C a => a -> a -> a
up
min :: a -> a -> a
min = a -> a -> a
forall a. C a => a -> a -> a
dn

abs :: (C a, Additive.C a) => a -> a
abs :: a -> a
abs a
x = a
x a -> a -> a
forall a. C a => a -> a -> a
`up` a -> a
forall a. C a => a -> a
negate a
x