{-|
Module      : Lattice
Description : Complemented complete lattice
Copyright   : (c) David Janin, 2015
License     : see the LICENSE file in the distribution
Maintainer  : janin@labri.fr
Stability   : experimental

Basic (complemented complete) lattice class. This does not intend to be a clever generic class for these lattices.

-}

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

{-# LANGUAGE MultiParamTypeClasses,
             FlexibleInstances #-}


module Duration.Lattice (POrd (..), Lattice (..), Complete (..)) where

import Duration.POrd

-- | Complemented complete lattices

class POrd d => Lattice d where
  -- | Least upper bound
  --
  -- prop> x pLeq y if, and only if, x = meet [x,y]
  --
  -- We also have, thanks to the instance of POrd [a]
  --
  -- prop> if l1 pLeq l2 then meet l1 pLeq l2
  --
  -- however, the converse may not hold.
    
  meet :: [d] -> d
  -- | Greatest lower bound
  --
  -- prop> x pLeq y if, and only if, y = join [x,y]  
  join ::  [d] -> d
  join = compl . meet . (map compl)
  -- | Complement, should satisfy the equations
  --
  -- prop> partialCompare x y == partialCompare (compl y) (compl x) 
  -- and
  -- 
  -- prop> join [l] == compl (meet [map compl l]), meet [l] == compl (join [map compl l])
  compl :: d -> d
  -- | Greatest value
  -- 
  -- prop> top == meet[]
  --
  -- and
  --
  -- prop> top == compl bot

  top :: d
  top = meet []
  -- | Least value
  -- 
  -- prop> bot == join []
  --
  -- and
  --
  -- prop> bot == compl top
  bot :: d
  bot = join [] 

-- | Without top and bot
instance Lattice Integer where
  meet = minimum
  compl = negate

-- | Without top and bot
instance Lattice Rational where
  meet = minimum
  compl = negate

-- | A rather adhoc completion of a partially ordered or an ordered type
data Complete a = Top | Bot | Value a deriving (Eq, Show)
                

-- | Extending Num (Yet all adhoc)
instance (Ord a, Num a) => Num (Complete a) where
  Bot + Top = error "Complete : undefined sum (Bot + Top)"
  Top + Bot = error "Complete : undefined sum (Top + Bot)"
  Bot + _ = Bot
  _ + Bot = Bot
  Top + _ = Top
  _ + Top = Top
  Value x +  Value y = Value $ x+y
  negate Bot = Top
  negate Top = Bot
  negate (Value x) = Value $ negate x
  signum = const $ Value 1
  abs = id
  fromInteger = Value . fromInteger
  (Value x) * (Value y) = Value $ x*y
  Top * Top = Top
  Top * Bot = Bot
  Bot * Top = Bot
  Bot * Bot = Top
  Top * (Value y)
      = case y of
          0 -> error "Complete :  undefined sum product (Top * 0)"
          _ -> Top
  Bot * (Value y) = Top * (Value (-y))
  (Value y) * Top = Top * (Value y)
  (Value y) * Bot = Top * (Value (-y))

-- | Extending Fractional (Yet all adhoc)
instance (Ord a, Fractional a) => Fractional (Complete a) where
    recip Bot = Value 0
    recip Top = Value 0
    recip (Value f) = Value (recip f)
    fromRational f = Value (fromRational f)
        
-- | Extending Ord
instance Ord a => Ord (Complete a) where
  (<=) Bot _ = True
  (<=) _ Top = True
  (<=) _ Bot = False
  (<=) Top _ = False
  (<=) (Value x) (Value y) = x <= y

instance POrd a => POrd (Complete a) where
    pLeq _ Top = True
    pLeq Top _ = False
    pLeq Bot _ = True
    pLeq _ Bot = False
    pLeq (Value a) (Value b) = pLeq a b


-- | Extending Lattice
instance (Num a, Ord a, POrd a) => Lattice (Complete a) where
  meet [] = Top
  meet (x:xs)
      = let rs = meet xs
        in case compare x rs of
             LT -> x
             _ -> rs
  compl = negate


-- |  Derived lattice for Product
instance (Lattice a,Lattice b) => Lattice (a,b) where
    meet l = (meet . fst . unzip $ l,meet . snd . unzip $ l)
    compl (a,b) = (compl a, compl b)


-- |  Derived lattice for Either
instance (Lattice a,Lattice b) => Lattice (Complete (Either a b)) where
    meet = meetCE
        where
          meetCE [] = Top
          meetCE (x:l)
              = case (x,meetCE l) of
                  (Top,r) -> r
                  (r,Top) -> r
                  (Value (Left a1),Value (Left a2))
                      -> Value (Left (meet [a1,a2]))
                  (Value (Right b1),Value (Right b2))
                      -> Value (Right (meet [b1,b2]))
                  _ -> Bot                       
    compl Top = Bot
    compl Bot = Top
    compl (Value (Left a)) = Value (Left $ compl a)
    compl (Value (Right b)) = Value (Right $ compl b)