module Data.Semigroup.Quantale where

import Data.Connection hiding (floor', ceiling')
import Data.Float
import Data.Group
import Data.Prd
import Data.Prd.Lattice
import Data.Word
import Data.Semigroup.Orphan ()
import Prelude hiding (negate, until)
import Test.Property.Util ((<==>),(==>))
import qualified Prelude as Pr

residuated :: Quantale a => a -> a -> a -> Bool
residuated x y z = x <> y <~ z <==> y <~ x \\ z <==> x <~ z // y

{-

In the interest of usability we abuse terminology slightly and use 'quantale' to describe any residuated, partially ordered semigroup. This admits instances of hoops and triangular (co)-norms.

There are several additional properties that apply when the poset structure is lattice-ordered (i.e. a residuated lattice) or when the semigroup is a monoid or semiring. See the associated 'Properties' module.


distributive_cross as bs = maybe True (~~ cross as bs) $ pjoin as <> pjoin bs
  where cross = join (liftA2 (<>) a b)

--lattice version
distributive_cross' as bs = cross as bs ~~ join as <> join bs
  where 
        cross = join (liftA2 (<>) a b)

join as \\ b ~~ meet (fmap (\\b) as)

a \\ meet bs ~~ meet (fmap (a\\) bs)

ideal_residuated :: (Quantale a, Ideal a, Functor (Rep a)) => a -> a -> Bool
ideal_residuated x y = x \\ y =~ join (fmap (x<>) (connl ideal $ y))

ideal_residuated' :: (Quantale a, Ideal a, Functor (Rep a)) => a -> a -> Bool
ideal_residuated' x y = x // y =~ join (fmap (<>x) (connl ideal $ y))

x \/ y = (x // y) <> y -- unit (minus_plus x) y -- (y // x) + x
x /\ y = x <> (x \\ y) -- (y + x) // x -- x \\ (x + y) 

minimal \\ x =~ maximal =~ x \\ maximal
mempty \\ x ~~ unit
 
-}

class (Semigroup a, Prd a) => Quantale a where
    residr :: a -> Conn a a
    residr x = Conn (x<>) (x\\)

    residl :: a -> Conn a a
    residl x = Conn (<>x) (//x)

    (\\) :: a -> a -> a
    x \\ y = connr (residr x) y

    (//) :: a -> a -> a
    x // y = connl (residl x) y

instance Quantale Float where
    x \\ y = y // x

    --x <> y <~ z iff y <~ x \\ z iff x <~ z // y.
    y // x | y =~ x = 0
           | otherwise = let z = y - x in if z + x <~ y then upper z (x<>) y else lower' z (x<>) y 

-- @'lower'' x@ is the least element /y/ in the descending
-- chain such that @not $ f y '<~' x@.
--
lower' z f x = until (\y -> f y <~ x) ge (shift $ -1) z

-- @'upper' y@ is the greatest element /x/ in the ascending
-- chain such that @g x '<~' y@.
--
upper z g y = while (\x -> g x <~ y) le (shift 1) z