{-|
Module      : Affine
Description : Linear polynoms with positive values of variable
Copyright   : (c) David Janin, 2016
License     : see the LICENSE file in the distribution
Maintainer  : janin@labri.fr
Stability   : experimental

An implementation of multi-variable linear polynoms. Associated partial order when variables are always assumed to have stricly positive values. This can also be seen as an algebra of (positive) delays with unknows.

Warning : the num and fractional instances are there for notational convinience. In order to stay within affine functions, the product fails over two non constant functions and teh inverse fails over a non constant function.
 
-}

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

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

module Duration.Affine (Affine(Affine), affineFromID, affineFromConst, shiftAffine, setToZeroAffine, evalAffine,getNextKnownDelay) where

import Duration.Lattice

import qualified Data.List as L

-- | Affine functions over a numeric space d and a set of variable index i.
data Affine d i = Affine !d ![(d,i)] deriving (Show)


---------------------------------------------------------------
--              Eq instance
---------------------------------------------------------------

-- | Semantical equality
instance (Num d, Ord d, Ord i) => Eq (Affine d i) where
  (==) = pOrdEq

---------------------------------------------------------------
--              Ord instance
---------------------------------------------------------------

-- | Total order with possible error
instance (Num d, Ord d, Ord i) => Ord (Affine d i) where
    compare d1 d2
        = case (partialCompare d1 d2) of
            Just EQ -> EQ
            Just LT -> LT
            Just GT -> GT
            Nothing -> error "Incomparable Affine: causality error ?"

---------------------------------------------------------------
--              Partial order instance
---------------------------------------------------------------

-- | Semantical partial order (with positive variables)
instance (Num d, Ord d, Ord i) => POrd (Affine d i) where
  partialCompare = compareAffine

---------------------------------------------------------------
--              Num instance
---------------------------------------------------------------

-- | For syntactic confort (with partially defined product)
instance (Num d, Eq d,Ord i) => Num (Affine d i) where
     (+) = plusAF
     -- | Fails when both components are non constants  
     (*) = multAF
     abs = \_ -> Affine (fromInteger 1) []
     signum = id
     fromInteger = \x -> Affine (fromInteger x) []
     negate = negateAF


---------------------------------------------------------------
--              Fractional instance
---------------------------------------------------------------

-- | For syntactic confort (with partially defined inverse)
instance (Fractional d, Eq d, Ord i) => Fractional (Affine d i) where
     recip = recipAF
     fromRational = \x -> Affine (fromRational x) []


---------------------------------------------------------------
-- * Primitive setters
---------------------------------------------------------------

-- | Creates the one variable affine function (X_i) from index i.

affineFromID :: Num d => i -> Affine d i
affineFromID i = Affine 0 [(1,i)]

-- | Creates the constant affine function (d) from value d.
affineFromConst :: d -> Affine d i
affineFromConst d = Affine d []

---------------------------------------------------------------
-- * Num and fractional non trivial functions
---------------------------------------------------------------

-- | Sum of two affine functions.
plusAF :: (Num d, Eq d,Ord i) => Affine d i -> Affine d i -> Affine d i 
plusAF (Affine d1 l1) (Affine d2 l2) = Affine (d1 + d2) (mergeL l1 l2)
   
-- | Product of two affine functions. Undefined with two non constant
-- functions in order to stay within affine functions.
multAF :: (Eq d, Num d) =>
                Affine d i -> Affine d i -> Affine d i
multAF (Affine 0 []) _ = (Affine 0 [])
multAF _ (Affine 0 []) = (Affine 0 [])
multAF (Affine d1 []) (Affine d2 l2) = Affine (d1*d2) (multL d1 l2)
multAF (Affine d1 l1) (Affine d2 []) = Affine (d1*d2) (multL d2 l1)
multAF _ _ = error "Affine product: at least one of the component in a product must be constant"
          -- this laste erroneous case allows to keep affine functions
          -- as values. Linear programing is then available for reasonning...
          -- In the more general case, this would lead to polynomials which
          -- comparison would remain decidable but at much much higher cost

multL :: Num d => d -> [(d, i)] -> [(d, i)]
multL _ [] = []
multL f ((d,e):l) = (f*d,e):(multL f l)

-- | Negates an affine functions 
negateAF :: Num d => Affine d i -> Affine d i
negateAF (Affine d l) = Affine (-d) (revL l) where
      revL [] = []
      revL ((d,i):l) = (-d,i):(revL l)

-- | Inverses an affine functions. Undefined over non constant functions in order
-- to stay within affine functions.
recipAF :: (Fractional d) => Affine d i -> Affine d i 
recipAF (Affine d []) = (Affine (1/d) [])
recipAF _ = error "Affine inverse: only defined for constant"
          -- this laste erroneous case allows to keep affine functions
          -- as values.
          -- In the more general case, this would lead to rational fractions
          -- that is, fractions of polynomials which comparison would remain
          -- decidable but at much much higher cost


---------------------------------------------------------------
-- * Various usefull low-level functions
---------------------------------------------------------------

-- | Normalizes representation
normalizeAffine :: (Eq d, Num d, Ord i) =>
                         Affine d i -> Affine d i
normalizeAffine (Affine d []) = (Affine d [])
normalizeAffine (Affine d ((d1,i1):l)) = plusAF (Affine 0 [(d1,i1)]) (Affine d l)

-- | Merges ordered lists of monomials
mergeL:: (Num d,Eq d,Ord i) => [(d,i)] -> [(d,i)] -> [(d,i)] 
mergeL [] l = l
mergeL l [] = l
mergeL ((d1,e1):l1) ((d2,e2):l2)  = case (compare e1 e2) of
       LT -> (d1,e1):(mergeL l1 ((d2,e2):l2)) 
       EQ -> let d = (d1 + d2) in
             if (d == 0) then (mergeL l1 l2)
             else ((d1+d2),e1):(mergeL l1 l2)
       GT -> (d2,e2):(mergeL ((d1,e1):l1) l2) 

-----------------------------------
-- * Getters
-----------------------------------

-- | True when positive (or zero) for every positive values of variables, false otherwise.
isPosAffine :: (Num d, Ord d) => Affine d i -> Bool
isPosAffine (Affine d []) = 0<=d
isPosAffine (Affine d l) = if (d < 0) then False else isPosL l where
  isPosL :: (Num d, Ord d) => [(d,i)] -> Bool
  isPosL [] = True
  isPosL ((d,_):l) = if (d < 0) then False else isPosL l

-- | True when negative (or zero) for every positive values of variables, false otherwise.
isNegAffine ::  (Num d, Ord d) => Affine d i -> Bool
isNegAffine (Affine d []) = d <=0
isNegAffine (Affine d l) = if (d > 0) then False else isNegL l where
  isNegL :: (Num d, Ord d) => [(d,i)] -> Bool
  isNegL [] = True
  isNegL ((d,_):l) = if (d > 0) then False else isNegL l

-- | True on the contant zero affine function, false otherwise
isZeroAffine :: (Eq d, Num d) => Affine d i -> Bool
isZeroAffine (Affine 0 []) = True
isZeroAffine _  = False

-- | True on the contant affine functions, false otherwise
isConstAffine :: (Eq d, Num d,Ord i) => Affine d i -> Bool
isConstAffine a = let (Affine _ l) = normalizeAffine a
                  in case l of
                  [] -> True
                  _ -> False

-- | Induced partial order, with vaiable universally quantifified over positive values. 
compareAffine ::  (Ord d, Num d, Ord i) => (Affine d i) ->  (Affine d i) -> Maybe (Ordering)
compareAffine x y = let z = plusAF x (negateAF y) in
               case (isPosAffine z,isNegAffine z) of
               (True,True) -> Just EQ
               (True,False) -> Just GT
               (False,True) -> Just LT
               (False,False) -> Nothing


-----------------------------
-- * Update function
-----------------------------

-- | Gets the greatest stricly positive constant lower than an affine
-- returns Nothing if its 0
-- error if there is no such value
getNextKnownDelay :: (Eq d, Num d) => Affine d i -> Maybe d
getNextKnownDelay (Affine 0 []) = Nothing
getNextKnownDelay (Affine d []) = Just d
getNextKnownDelay _ = Nothing
                      
-- | Replaces any variable X by X + d 
shiftAffine :: (Eq d, Num d,Ord i) => d -> Affine d i -> Affine d i
shiftAffine _ (Affine dd []) = Affine dd []
shiftAffine d (Affine dd ((di,i):l))
  = (Affine (di*d) [(di,i)]) + shiftAffine d (Affine dd l)

-- | Sets variables Xi with i in the list to zero
setToZeroAffine :: (Num d,Ord i) => [i] -> Affine d i -> Affine d i
setToZeroAffine l (Affine dd ld)
    = Affine dd [(d,i) | (d,i) <- ld, L.notElem  i l]

{-
-- | For easy reading/debug purpose
instance (Show d, Num d,Eq d,Ord d,Show i) => Show (Affine d i) where
   show (Affine d l) =
        let showL [] = ""
            showL [(1,e)] = "X"++show e
            showL [(-1,e)] = "- X"++show e
            showL [(d,e)] = show d ++ "*" ++ "X" ++show e
            showL ((d1,e1):((d2,e2):l))
               = case (d2<0) of
                 True -> showL [(d1,e1)] ++ " - " ++ showL ((-d2,e2):l)
                 False -> showL [(d1,e1)] ++ " + " ++ showL ((d2,e2):l)
        in  case (d,l) of
             (0,[]) -> "(0)"
             (d,[]) -> "("++show d++")"
             (0,l) -> "("++showL l++")"
             (d,l) -> "("++show d ++ " + "  ++ showL l++")"
-}

{-
--------------------------------------------------------------
-- * Basic usage examples
--------------------------------------------------------------

-- | A test
test0 :: Affine Integer Integer
test0 = affineFromConst 3 + affineFromID 1
-}

-- | Evals an affine function on a point (for debug)
evalAffine :: (Eq d, Num d, Ord i) =>
                    d -> Affine d i -> Affine d i
evalAffine _ (Affine dd []) = Affine dd []
evalAffine d (Affine dd ((di,_):l))
    = Affine (di*d) [] + evalAffine d (Affine dd l)