{-|
Module      : MinMax
Description : Lattice completions of num data types
Copyright   : (c) David Janin, 2016
License     : see the LICENSE file in the distribution
Maintainer  : janin@labri.fr
Stability   : experimental

Embbeds Num data types into a complete lattice.

-}


{-# OPTIONS_GHC -Wall -fno-warn-name-shadowing #-}

{-# LANGUAGE TypeSynonymInstances
             , MultiParamTypeClasses
             , FlexibleInstances #-}

module Duration.MinMax where

       -- for a minMax (or maxMin) completion of partially order sets (aka POrd)
       -- no assumption that elements are (syntactically) ordered
       -- so most many implemented algorihtms are quadratic in time
       -- not to speak about exponential convertion of minMax to MaxMin
       -- abd vice versa

import Duration.Lattice

-- import qualified Data.List as L

---------------------------------------------------------------
-- * The Min and Max completions 
---------------------------------------------------------------

-- | Min l represents the least upper bound of elements of l
-- henceforth with Min[] as top element.
--
-- The mapping '\a -> Min [a]' is an embedding of a into Min a

data Min a = Min [a] deriving (Show)

           
-- | Min l represents the greates lower bound of elements of l
-- henceforth with Max[] as bottom.
--
-- The mapping '\a -> Max [a]' is an embedding of a into Max a
data Max a = Max [a] deriving (Show)

   ------------------------------------------------------------
   -- Min a and Max a are equipped with a partial order relation
   -- such that:
   --    1) Min a is a meet semi-lattice with Min[] as maximum
   --       Max a is a join semi-lattice with Max[] as minimum
   --    2) both \a -> Min [a] and \a -> Max [a] are embeddings
   -- In Maths, these constructions are known as
   -- order ideal completions
   ------------------------------------------------------------

---------------------------------------------------------------
-- ** The Min completion
---------------------------------------------------------------

-- | Inserts an element x into a list l of minimal elements
-- if l is an antichain then so is insertMin x l

insertMin :: (POrd a)=> a -> Min a -> Min a
   
insertMin x (Min []) = Min [x]
insertMin x m@(Min (y:ys))
  = case (partialCompare x y) of
    Just LT -> insertMin x (Min ys)
    Nothing -> let (Min ys1) = insertMin x (Min ys)
               in Min (y:ys1)
    _ -> m

-- | Reduces a Min list by removing greater comparable elements. The resulting list is an antichain.

reduceMin :: (POrd a) => Min a -> Min a
reduceMin (Min []) = Min []
reduceMin (Min (x:xs))
  = insertMin x (reduceMin (Min xs))

-- | Equals True when one element of its first arguement is smaller than or equal to its second arguement.
-- False otherwise

minCovered :: (POrd a) => Min a -> a -> Bool
  -- 
minCovered (Min []) _  = False
minCovered (Min (x:xs)) y 
  = case (partialCompare x y)  of 
    Just LT -> True
    Just EQ -> True
    _ -> minCovered (Min xs) y

-- | Induced partial order.
-- The boolean pMinLeq m1 m2 is True when every element of m2 is greater than or equal
-- to an element of m1, it is False otherwise

pMinLeq ::  (POrd a) => Min a -> Min a -> Bool
     -- 
pMinLeq _ (Min []) = True
pMinLeq m (Min (y:ys))
   = case (minCovered m y) of
     True -> pMinLeq m (Min ys)
     False -> False

-- | Min completion as a pOrd.
instance (POrd a) => POrd (Min a) where
  pLeq = pMinLeq
  
-- | For internal use (needed ?)
compareMin :: (POrd a) => Min a -> Min a -> Maybe Ordering
compareMin = partialCompare

-- | Natural embedding with the property that under (POrd a) hypothesis,
--
-- prop> partialCompare a b == partialCompare (toMin a) (toMin b)
--
-- that is to say, 'toMin' is a partial order embeding of a into Min a

toMin :: a -> Min a
toMin a = Min [a]

-- | Equality instance derived from the partial order
instance (POrd a) => Eq (Min a) where
  (==) = pOrdEq

---------------------------------------------------------------
-- ** The Max completion
---------------------------------------------------------------

-- | Inserts an element x into a list l of maximal elements;
-- if l is an antichain then so is insertMax x l.
        
insertMax :: (POrd a)=> a -> Max a -> Max a
   
insertMax x (Max []) = Max [x]
insertMax x m@(Max (y:ys))
  = case (partialCompare x y) of
    Just GT -> insertMax x (Max ys)
    Nothing -> let (Max ys1) = insertMax x (Max ys)
               in Max (y:ys1)
    _ -> m

-- | Reduces a Max list by removing smaller comparable elements. The resulting list is an antichain.

reduceMax :: (POrd a ) => Max a -> Max a
reduceMax (Max []) = Max []
reduceMax (Max (x:xs))
  = insertMax x (reduceMax (Max xs))

-- | Equals True when one element of its first arguement is greater than or equal to its second arguement.
-- False otherwise

maxCovered :: (POrd a) => Max a -> a -> Bool
  -- maxCovered m y equals True when one element of m that is greater than or equal to y,
  -- it is False otherwise
maxCovered (Max []) _  = False
maxCovered (Max (x:xs)) y  
  = case (partialCompare x y)  of 
    Just GT -> True
    Just EQ -> True
    _ -> maxCovered (Max xs) y
    
-- | Induced partial order.
-- The boolean pMaxLeq m1 m2 is True when every element of m1 is smaller than or equal
-- to an element of m1, it is False otherwise

pMaxLeq ::  (POrd a) => Max a -> Max a -> Bool
  -- pMaxLeq m1 m2 equals
     -- True when every element of m1 is smaller than or equal to an element of m2
     -- False otherwise
pMaxLeq (Max []) _ = True
pMaxLeq (Max (x:xs)) m
   = case (maxCovered m x) of
     True -> pMaxLeq (Max xs) m
     False -> False

-- | Derived partial order
instance (POrd a) => POrd (Max a) where
  pLeq = pMaxLeq
  
-- | For internal use (needed ?)
compareMax :: (POrd a) => Max a -> Max a -> Maybe Ordering
compareMax = partialCompare

             
-- | Natural embedding with the property that under (POrd a) hypothesis,
--
-- prop> partialCompare a b == partialCompare (toMax a) (toMax b)
--
-- that is to say, 'toMax' is a partial order embeding of a into Max a
toMax :: a -> Max a
toMax a = Max [a]

-- | Derived equality instance
instance (POrd a) => Eq (Max a) where
  (==) m1 m2
    = case (compareMax m1 m2) of
      Just EQ -> True
      _ -> False

---------------------------------------------------------------
-- * The MinMax and MaxMin completion              -
---------------------------------------------------------------

-- | MinMax completion
type MinMax a = Min (Max a)
-- | MaxMin completion
--
-- MaxMin a and MinMax a are both equiped with a derived
-- order relation such that :
--      * both MinMax and MaxMin are (isomorphic) lattices
--      * both \a -> Min [Max a] and \a -> Max [Min a] are
--      partial order embeddings
--
-- Incidentaly:
-- Max[] and Max [Min []] are the least and the greatest
-- element of MaxMin, and Min[] and Min [Max []] are the
-- least and the greatest element in MinMax
   
type MaxMin a = Max (Min a)

   -- Then, Num a or Fractionnal a,  we can derive instances 
   -- Num (MinMax a) and Fractionnal (MinMax a). 



-- | The meet in Min completion
meetMin :: (POrd a) => Min a -> Min a -> Min a
       -- (R) the result is always reduced
meetMin (Min l1) (Min l2) = reduceMin (Min (l1++l2))

-- | The join in MinMax completion (with exponential blow up)
joinMin :: (POrd a) => MinMax a -> MinMax a -> MinMax a
       -- (R) the result is always reduced
joinMin (Min []) _ = Min []
joinMin _ (Min []) = Min[]
joinMin (Min[x]) (Min[y])
  = case (partialCompare x y) of
    Just LT -> Min[y]
    Nothing -> Min[joinMax x y]
    _ -> Min [x]
joinMin (Min (x:xs)) m = meetMin (joinMin m (Min[x])) (joinMin (Min xs) m)
    
-- | Corresponding list meet
meetMinL :: POrd a => [Min a] -> Min a
meetMinL [] = Min []
meetMinL (x:l) = meetMin x (meetMinL l)

-- | Corresponding list join
joinMinL :: POrd a => [MinMax a] -> Min (Max a)
joinMinL [] = Min [Max []]
joinMinL (x:l) = joinMin x (joinMinL l)

-- | The join in Max completion
joinMax :: (POrd a) => Max a -> Max a -> Max a
       -- (R) the result is always reduced
joinMax (Max l1) (Max l2) = reduceMax (Max (l1++l2))

-- | The meet in MaxMin completion (with exponential blow up)
meetMax :: (POrd a) => MaxMin a -> MaxMin a -> MaxMin a
       -- (R) the result is always reduced
meetMax (Max []) _ = Max[]
meetMax _ (Max []) = Max[]
meetMax (Max [x]) (Max [y])
  = case (partialCompare x y) of
    Just LT -> Max[x]
    Nothing -> Max[meetMin x y]
    _ -> Max [y]
meetMax (Max (x:xs)) m = joinMax (meetMax m (Max [x])) (meetMax (Max xs) m)
    
-- | Corresponding list meet
meetMaxL :: POrd a => [MaxMin a] -> Max (Min a)
meetMaxL [] = Max [Min[]]
meetMaxL (x:l) = meetMax x (meetMaxL l)

-- | Corresponding list join
joinMaxL :: POrd a => [Max a] -> Max a
joinMaxL [] = Max []
joinMaxL (x:l) = joinMax x (joinMaxL l)


-- | Emebedding of MaxMin into MinMax (warning : exponential blow up) 
maxMin2MinMax :: (POrd a) => MaxMin a -> MinMax a
       -- (R) the result is always doubly reduced, i.e. it is a reduced min or reduced max
maxMin2MinMax (Max []) = Min [Max []]
maxMin2MinMax (Max ((Min []):_)) = Min []
maxMin2MinMax (Max ((Min l):xs)) = joinMin (Min (fmap toMax l)) (maxMin2MinMax (Max xs))


-- | Emebedding of MinMax into MaxMin (warning : exponential blow up) 
minMax2MaxMin :: (POrd a) => MinMax a -> MaxMin a
       -- (R) the result is always doubly reduced, i.e. it is a reduced max or reduced min
minMax2MaxMin (Min []) = Max [Min []]
minMax2MaxMin (Min ((Max []):_)) = Max []
minMax2MaxMin (Min ((Max l):xs)) = meetMax (Max (fmap toMin l)) (minMax2MaxMin (Min xs))


---------------------------------------------------------------
-- * Functor like functions
---------------------------------------------------------------


-- | Unary (covariant) lift for Min
fmap1Min :: (POrd a) => (a -> a) -> Min a -> Min a
fmap1Min f (Min l) 
  = reduceMin $ Min (map f l)  

-- | Unary (covariant) lift for Max
fmap1Max :: (POrd a) => (a -> a) -> Max a -> Max a
fmap1Max f (Max l) 
  = reduceMax $ Max (map f l)  

-- | Unary (covariant) lift for MinMax
fmap1MinMax :: (POrd a) => (a -> a) -> MinMax a -> MinMax a
fmap1MinMax f = fmap1Min (fmap1Max f)

-- | Unary (covariant) lift for MaxMin
fmap1MaxMin :: (POrd a) => (a -> a) -> MaxMin a -> MaxMin a
fmap1MaxMin f = fmap1Max (fmap1Min f)

-- | Binary lift for Min 
fmap2Min :: (POrd a) => (a -> a -> a) -> Min a -> Min a -> Min a 
fmap2Min f (Min l1) (Min l2)
  = reduceMin $ Min (concatMap (\y -> (map (\x -> f x y) l1)) l2)

-- | Binary lift for Max 
fmap2Max :: (POrd a) => (a -> a -> a) -> Max a -> Max a -> Max a 
fmap2Max f (Max l1) (Max l2)
  = reduceMax $ Max (concatMap (\y -> (map (\x -> f x y) l1)) l2)

-- | Binary lift for MinMax 
fmap2MinMax :: (POrd a) => (a -> a -> a) -> MinMax a -> MinMax a -> MinMax a 
fmap2MinMax f = fmap2Min (fmap2Max f)

-- | Binary lift for MaxMin 
fmap2MaxMin :: (POrd a) => (a -> a -> a) -> MaxMin a -> MaxMin a -> MaxMin a 
fmap2MaxMin f = fmap2Max (fmap2Min f)

-- | Unary contravariant lift for Min
fmapRMin :: (POrd a) => (a -> b) -> Min a -> Max b
fmapRMin f (Min l) = Max (fmap f l)
-- | Unary contravariant lift for Max
fmapRMax :: (POrd a) => (a -> b) -> Max a -> Min b
fmapRMax f (Max l) = Min (fmap f l)

-- | Unary contravariant lift for MinMax
fmapRMinMax :: (POrd a) => (a -> a) -> MinMax a -> MaxMin a
fmapRMinMax f = fmapRMin (fmapRMax f)

-- | Unary contravariant lift for MaxMin
fmapRMaxMin :: (POrd a) => (a -> a) -> MaxMin a -> MinMax a
fmapRMaxMin f = fmapRMax (fmapRMin f)


-- | Derived Num instance (to be checked)
instance (Num a,POrd a) => Num (MinMax a) where
  fromInteger d = Min [Max [fromInteger d]]
  (+) = fmap2MinMax (+)
  (*) = fmap2MinMax (*)
  abs = const $ fromInteger 1
  signum = id
  negate d = maxMin2MinMax (fmapRMinMax negate d)

-- | Derived Fractional instance (to be checked)
instance (Fractional a,POrd a) => Fractional (MinMax a) where
  fromRational r = Min [Max [fromRational r]]
  recip d = maxMin2MinMax (fmapRMinMax recip d)

-- | Derived Lattice instance
instance (POrd a, Num a) => Lattice (MinMax a) where
  meet = meetMinL
  compl = negate


-- | for exports (to be cleaned)
meetM :: (POrd a) => [MinMax a] -> MinMax a
meetM = meetMinL

-- | for exports (to be cleaned)
joinM :: (POrd a) => [MinMax a] -> MinMax a
joinM = joinMinL

       
-- | Derived total order with possible errors; 
-- to be used either with care, or as syntactic sugar..
instance (POrd d) => Ord (Min (Max d)) where
    compare d1 d2
        = case (partialCompare d1 d2) of
            Just EQ -> EQ
            Just LT -> LT
            Just GT -> GT
            Nothing -> error "Incomparable MinMax: causality error ?"

reduceMM :: (POrd a) => MinMax a -> MinMax a
reduceMM (Min l) = reduceMin (Min (map reduceMax l))

justMM :: a -> Min (Max a)
justMM d = Min[Max [d]]