{-|
Module      : QList
Description : Timed lists of temporal values 
Copyright   : (c) David Janin, Simon Archipoff, 2016
License     : see the LICENSE file in the distribution
Maintainer  : janin@labri.fr
Stability   : experimental

'QList's are timed sequences of bundles of temporal values, that is,
lists of 'Atom's synchronized on their starts, separated by (positive) delays.
'QList's are in one to one correspondance with zero duration tiles with no anticipation.

'QList's form the /back-end/ of our reactive machinery. Combining qlists 
can be directly made by using functions like 'mergeQ' or 'insertQ'. However,
the algebraic properties of these functions are not as nice as those acting over tiles (see "Docs.Additive").
So tiles can be seen as a handy algebraic /front-end/ for qlist manipulation.

<<ex12.svg>>

In the above picture of a tile, the underlying qlist is depicted in black. 
There is a semantic embedding of qlist into tile by the mapping

@
fromQList q = Tile 0 0 q
@

-}

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

{-# LANGUAGE MultiParamTypeClasses,
             GADTs,
             FlexibleContexts,
             FlexibleInstances #-}


module Tile.QList where

import Reactive.Updatable

import Tile.Tilable
-- import Duration.Lattice -- included in Tilable
import Tile.Atom

--------------------------------------------------------------------
-- * Timed "list" of temporal values
--------------------------------------------------------------------


-- | Queue lists (in short qlists) are built over duration type 'd', input value type 'iv' and ouput value type 'v'
data QList d iv v where
     QEnd :: QList d iv v
     QList :: [Atom d iv v] -> DQ d iv v -> QList d iv v
     QRec :: Updatable p d iv => d -> (p -> QList d iv v) -> p -> QList d iv v


size_qlist :: QList t t1 t2 -> Int
size_qlist QEnd = 0
size_qlist (QList _ (DQ _ ql)) = 1 + size_qlist ql
size_qlist (QRec _ _ _) = 1

width_qlist :: QList t t1 t2 -> Int
width_qlist QEnd = 0
width_qlist (QList l (DQ _ ql)) = length l + width_qlist ql
width_qlist (QRec _ _ _) = 0


-- | Show instance
instance (Show d, Num d, Show v) => Show (QList d iv v) where
  show QEnd = "QEnd"
  show (QList al dq) = "(QList "++ show al ++" ("++ show dq++"))"
  show (QRec _ _ _) = "<QRec>" -- show (stretchQ d (f p))

-- | Derived 'natural' partial order, possibly unfolding recursive definitions.
instance (Num d, Eq d, POrd d, POrd v) => POrd (QList d iv v) where
    pLeq q1 q2 = pLeqQ (reduceQ q1) (reduceQ q2) where
        pLeqQ _ QEnd = True    
        pLeqQ (QRec d f p) x = pLeqQ (stretchQ d (f p)) x 
        pLeqQ x (QRec d f p) = pLeqQ x (stretchQ d (f p))
        pLeqQ (QList al1 dq1) (QList al2 dq2)
            = case (pLeq al1 al2) of
                True -> pLeq dq1 dq2
                False -> False
        pLeqQ QEnd (QList [] (DQ _ q)) = pLeq QEnd q
        pLeqQ QEnd _ = False
                        
-- | Semantical equality, possibly unfolding recursive definitions.
instance  (Num d, Eq d, POrd d, POrd v) => Eq (QList d iv v) where
    (==) = pOrdEq
                   

-- | Delayed qlists, built over duration type 'd' and input value type 'iv'
-- with invariant property
--
-- prop> In every value (DQ d iv v) we should have (partialCompare 0 d) either equals Just LT or Just EQ
data DQ d iv v = DQ  d (QList d iv v)
         deriving (Show)

-- | Derived 'natural' partial order, possibly unfolding recursive definitions.
instance (Num d, Eq d, POrd d, POrd v) => POrd (DQ d iv v) where
    -- pLeq _ (DQ _ QEnd) = True
    -- pLeq (DQ _ QEnd) _ = False
    pLeq (DQ d1 q1) (DQ d2 q2)
        = case (partialCompare d1 d2) of
            Just EQ -> pLeq q1 q2
            Just LT -> pLeq (DQ 0 q1) (DQ 0 (QList [] (DQ (d2-d1) q2)))
            Just GT -> pLeq (DQ 0 (QList [] (DQ (d1-d2) q1))) (DQ 0 q2)
            Nothing -> error "Tile Partial Order : incomparable duration"
                       
         
--------------------------------------------------------------------
-- * Getters
--------------------------------------------------------------------

-- | True when empty
isEmptyQ :: (Num d, Eq d) => QList d iv v -> Bool
isEmptyQ QEnd = True
isEmptyQ (QList [] (DQ _ q)) = isEmptyQ q
isEmptyQ (QList _ _) = False
isEmptyQ (QRec _ f p) = isEmptyQ (f p)
                             
-- | gets atoms at date zero (may unfold recursive definition)
getAtomsQ :: (Num d,Eq d) => QList d iv v -> [Atom d iv v]
getAtomsQ QEnd = []
getAtomsQ (QList l (DQ 0 q)) = l++getAtomsQ q
getAtomsQ (QList l (DQ _ _)) = l
getAtomsQ (QRec d f p)
  = getAtomsQ $ stretchQ d (f p)

-- | keeps atoms at date zero dropping everything else
atomsQ :: (Num d,Eq d) => QList d iv v -> QList d iv v
atomsQ QEnd = QEnd
atomsQ q = QList (getAtomsQ q) (DQ 0 QEnd)
               
-- | gets delay to next atoms
delayToTailQ :: (Num d, Eq d) => QList d iv v -> d
delayToTailQ q 
    = case dropAtomsQ q of
        (QList [] (DQ d _)) -> d
        (QEnd) -> 0
        _ -> error "delayToTailQ : this should never happend"

-- | gets remainder of the qlist
--
-- prop> q == QList (getAtomsQ q) (DQ (delayToTailQ q) (tailQ q))
tailQ :: (Num d, Eq d) => QList d iv v -> QList d iv v
tailQ QEnd = QEnd
tailQ (QList _ (DQ 0 q)) = tailQ q
tailQ (QList _ (DQ _ q)) = q -- QList [] (DQ d q)
tailQ (QRec d f p)
  = tailQ $ stretchQ d (f p) -- QRec d (tailQ . f) p

-- | gets contents of atoms at date zero
getAllFromAtomsQ :: (Num d, Eq d) => QList d iv v -> [(d,v)]
getAllFromAtomsQ q = fmap getAllA (getAtomsQ q)

-- | drops atoms at date zero
--
-- prop> dropAtomsQ q == QList [] (DQ (delayToTailQ q) (tailQ q))
dropAtomsQ :: (Num d,Eq d) => QList d iv v -> QList d iv v
dropAtomsQ QEnd = QEnd
dropAtomsQ (QList _ (DQ 0 q)) = dropAtomsQ q
dropAtomsQ (QList _ (DQ d q)) = QList [] (DQ d q)
dropAtomsQ (QRec d f p) = dropAtomsQ $ stretchQ d (f p)

--------------------------------------------------------------------
-- * Setters
--------------------------------------------------------------------

-- ** Primitive setters

-- | Builds qlist from a tilable value (see "Tile.Tilable")
fromValueQ :: (Tilable d v) => v -> QList d iv v
fromValueQ v = QList [fromValueA v] (DQ 0 QEnd)

-- | Builds qlist from a duration and a value
fromDurationAndValueQ :: (Num d) => d -> v -> QList d iv v
fromDurationAndValueQ d v = QList [Atom d v] (DQ 0 QEnd)

-- ** Append atoms or delay
                            
-- | Appends a list of atoms to a q list
appendQ :: (Num d, Lattice d) =>
                 [Atom d iv v] -> QList d iv v -> QList d iv v
appendQ al q
    = mergeQ (QList al (DQ 0 QEnd),q)
      
-- | Delays a qlist by d unit of time (d must be positive)
addDelayQ :: (Num d, POrd d) => d -> QList d iv v -> QList d iv v
addDelayQ d q = case partialCompare 0 d of
               Just LT -> QList [] (DQ d q)
               Just EQ -> q
               _ -> error "addDelayQ : Illegal non strictly positive delay arguement"
                    
--------------------------------------------------------------------
-- ** Merge and delay
--------------------------------------------------------------------

-- | Merges two delayed qlists
mergeDQ :: (Num d, Lattice d) => (DQ d iv v,DQ d iv v) -> DQ d iv v
mergeDQ (DQ d1 q1,DQ _ QEnd) = DQ d1 q1
mergeDQ (DQ _ QEnd,DQ d2 q2) = DQ d2 q2
mergeDQ (DQ d1 q1, DQ d2 q2)
  = case (partialCompare d1 d2) of
    Just GT -> mergeDQ (DQ d2 q2, DQ d1 q1) 
    Just EQ -> DQ d1 $ mergeQ (q1,q2)
    -- Should we prefer: $ QRec 1 mergeQ (q1,q2)
    -- in the case d1 is strictly positive ?
    Just LT -> DQ d1 $ insertQ q1 (DQ (d2-d1) q2)
    -- Should we  prefer: $ QRec 1 (\(q,dq) -> insertQ q dq) (q1, DQ (d2-d1) q2)
    -- in the case d1 is strictly positive ?
    Nothing -> let d = meet [d1,d2]
               in DQ d $ QRec 1 (\(DQ d1 q1, DQ d2 q2) -> case partialCompare d1 d2 of
                                                            Just EQ -> mergeQ (q1,q2)
                                                            Just LT -> insertQ q1 (DQ (d2-d1) q2)
                                                            Just GT -> insertQ q2 (DQ (d1-d2) q1)
                                                            Nothing -> QEnd) -- adhoc debug
                                                                -- error "mergeDQ : non solvable merge")
                      (DQ d1 q1, DQ d2 q2)

--                  QRec 1 (\(DQ d1 q1, DQ d2 q2) -> QList [] (mergeDQ (DQ (d1-d) q1 , DQ (d2-d) q2)))
--                          (DQ d1 q1, DQ d2 q2)
                          
-- | Merges two qlists. This function relates with operation over tiles
-- as follows:
--
-- prop> Tile 0 0 (mergeQ q1 q2) = Tile 0 0 q1 + Tile 0 0 q2
mergeQ :: (Num d, Lattice d) => (QList d iv v,QList d iv v) -> (QList d iv v)  
mergeQ (QEnd,q) = q
mergeQ (q,QEnd) = q
mergeQ (QList l1 dq1,QList l2 dq2)
  = QList (l1++l2) $ mergeDQ (dq1, dq2) 
mergeQ (QRec d1 f1 p1,QRec d2 f2 p2)
  = QRec 1 (\(p1,p2) -> mergeQ (stretchQ d1 (f1 p1),stretchQ d2 (f2 p2))) (p1,p2)
mergeQ (qr@(QRec _ _ _),q)
  = QRec 1 (\(QRec d f p,q) -> mergeQ (stretchQ d (f p),q)) (qr,q)
mergeQ (q,qr@(QRec _ _ _)) = mergeQ (qr,q)

-- | Merges a qlist and a delayed qlist into a qlist.
insertQ :: (Num d, Lattice d) => QList d iv v -> DQ d iv v -> QList d iv v
insertQ QEnd (DQ d q) = QList [] (DQ d q)
insertQ (QList l (DQ d1 q1)) (DQ d2 q2) = QList l (mergeDQ (DQ d1 q1, DQ d2 q2))
insertQ qr@(QRec _ _ _) dq@(DQ _ _)
  = QRec 1 (\(QRec df f p,dq) -> insertQ (stretchQ df (f p)) dq) (qr,dq) 

-- ** Stretch

-- | Stretchs qlist by a given factor. This function relates with operation over tiles
-- as follows:
--
-- prop> Tile 0 0 (stretchQ d q) = fromDurationT d * Tile 0 0 q
stretchQ :: Num d =>
                    d -> QList d iv v -> QList d iv v
stretchQ _ QEnd = QEnd
stretchQ df (QList al dq) = QList (fmap (stretchA df) al) (stretchDQ df dq)
stretchQ df (QRec d f p) = QRec (df*d) f p


-- | Stretchs dqlist by a given factor
stretchDQ :: Num d =>
                    d -> DQ d iv v -> DQ d iv v
stretchDQ _ (DQ _ QEnd) = DQ 0 QEnd
stretchDQ dd (DQ d q) = DQ (dd*d) (stretchQ dd q)


-- ** Reduce

-- | Reduces the head of a qlist by gluing all atom lists at zero delay from "now".
-- This function may unfold immediate recursive definitions. The resulting 'head reduced qlist' is of
-- any of one the following form:
--
-- prop> QEnd (the empty list)
-- prop> or QList al (DQ 0 QEnd) with non empty al (the non empty list of atoms)
-- prop> or QList al (DQ d q) with stricly positive d
reduceQ :: (Num d,POrd d) => QList d iv v -> QList d iv v
reduceQ QEnd = QEnd
reduceQ (QRec d f p) = reduceQ (stretchQ d (f p))
reduceQ (QList [] (DQ d q))
  = case partialCompare 0 d of
      Just LT -> QList [] (DQ d q)
      Just EQ -> reduceQ q
      _  -> error "reduceQ : invalid duration in QList (1)"
reduceQ (QList al (DQ d q))
  = case partialCompare 0 d of
      Just LT -> QList al (DQ d q)
      Just EQ -> case reduceQ q of
                   QEnd -> QList al (DQ 0 QEnd)
                   QList al1 dq1 -> QList (al++al1) dq1
                   _ -> error "reduceQ : This should never happen"
      _  -> error "reduceQ : invalid duration in QList (2)"
                 
{-
-- | Reduces a QList by gluing all atom lists occuring at zero delay from "now".
reduceDQ :: (Num d,POrd d) => DQ d iv v -> DQ d iv v
reduceDQ (DQ d q)
    = case (partialCompare 0 d) of
        Just EQ -> DQ 0 $ reduceQ q
        Just LT -> DQ d q
        Just GT -> error "reduceDQ : Negative delay in qlist"
        Nothing -> error "reduceDQ : Unknown delay in qlist"
-}

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

-- | Applies a function over values. This function relates with operation over tiles
-- as follows:
--
-- prop> Tile 0 0 (fmapQ f q) = fmap f (Tile 0 0 q)
fmapQ :: Num d => (v1 -> v2) -> QList d iv v1 -> QList d iv v2
fmapQ _ QEnd = QEnd
fmapQ f (QList al (DQ d q)) = QList (fmap (fmapA f) al) (DQ d (fmapQ f q))
fmapQ f (QRec d g p) = QRec d (\p -> fmapQ f (g p)) p

instance (Num d) => Functor (QList d iv) where
    fmap = fmapQ

-- | Changes duration (same type).
fmapDQ :: (Num d) => (d -> d) -> QList d iv v -> QList d iv v
fmapDQ _ QEnd = QEnd
fmapDQ f (QList al (DQ d q)) = QList (fmap (fmapDA f) al) (DQ (f d) $ fmapDQ f q)
fmapDQ f (QRec d g p) = QRec (f d) (\p -> fmapDQ f (g p)) p

--------------------------------------------------------------------
-- * Projections
--------------------------------------------------------------------

-- ** Category based projection (Either acts as a categorical product)

-- | Gets from Left
fromLeftQ :: QList d iv (Either v1 v2) -> QList d iv v1
fromLeftQ QEnd = QEnd
fromLeftQ (QList al (DQ d q)) = QList [Atom d v | Atom d (Left v) <- al] (DQ d (fromLeftQ q))
fromLeftQ (QRec d f p) = QRec d (\p -> fromLeftQ (f p)) p

-- | Gets from Right
fromRightQ :: QList d iv (Either v1 v2) -> QList d iv v2
fromRightQ QEnd = QEnd
fromRightQ (QList al (DQ d q)) = QList [Atom d v | Atom d (Right v) <- al] (DQ d (fromRightQ q))
fromRightQ (QRec d f p) = QRec d (\p -> fromRightQ (f p)) p

-- ** Duration based projections

-- | Keeps all atoms starting stricly before some duration d measured from the begining of the qlist
-- and cut the qlist accordingly.
takeQ :: (Num d, Lattice d) => d -> QList d iv v -> QList d iv v
takeQ _ QEnd = QEnd
takeQ d q
    = case (partialCompare 0 d) of
        Just LT -> case q of
                     (QList al (DQ d1 q1)) -> QList al (DQ d1 $ QRec 1 (\(DQ d q) -> takeQ d q) (DQ (d-d1) q1))
                                              -- QRec protected : 01/17
                     (QRec dd f p) -> takeQ d (stretchQ dd (f p))
                     _ -> error "takeQ : this should never happend"
        _ -> QEnd
--        Just GT -> QEnd
--        Just EQ -> QEnd
--        Nothing -> error "takeQ : unknown duration"
                   -- QRec 1 (\(DQ d q) -> takeQ d q) (DQ d q)

                        
-- | Drops all atoms starting stricly before some duration d measured from the begining of the qlist
-- and cut the qlist accordingly.
dropQ :: (Num d, Lattice d) => d -> QList d iv v -> QList d iv v
dropQ _ QEnd = QEnd
dropQ d q
  = case partialCompare 0 d of
      Just LT
          -> case q of
               (QList _ (DQ d1 q1))
                   -> case partialCompare d d1 of
                        Just GT -> QRec 1 (\(DQ d q) -> dropQ d q) (DQ (d-d1) q1)
                        Just EQ -> q1
                        _ -> QList [] (DQ (d1 - d) q1)
                        -- _ ->  error "dropQ : unknown duration (2)"
               (QRec dd f p) -> dropQ d (stretchQ dd (f p))
               _ -> error "dropQ : this should never happend"
      _ -> q
      -- Just GT -> q
      -- Just EQ -> q
      -- Nothing -> error "dropQ : unknown duration"
                 -- QRec 1 (\(DQ d q) -> dropQ d q) (DQ d q0)

-- | Splits a qlist with a boolean function
split :: Functor f =>
               (b -> Bool) -> f b -> f (Either b b)
split f q = fmap
             (\v -> case (f v) of
                     True -> Left v
                     False -> Right v)
                              q
                                              
-- * Reverse

-- | Returns the time symetric of a qlist, with symmetric point a fixed distance from its begining,
-- and the distance from the beggining of that new list to the same fixed point.
reverseQ :: (Num d,Lattice d) => d -> QList d iv v -> (d,QList d iv v)
reverseQ dd q = timedListToQList . reverseTimedList $ qlistToTimedList dd q

-- | Transforms a qlist into a list of pairs (d,Atom d iv v) where d marks the distance from the beggining
-- of each atoms to a fixed zero in time
qlistToTimedList :: (Num d) => d -> QList d iv v -> [(d,Atom d iv v)]
qlistToTimedList _ QEnd = []
qlistToTimedList dd (QRec d f p) = qlistToTimedList dd (stretchQ d (f p))
qlistToTimedList dd (QList l (DQ d q)) = (map (\a -> (dd,a)) l) ++ qlistToTimedList (dd + d) q

-- | Reverses timed lists, now taking distance from ends of atoms to the zero point. 
reverseTimedList :: Num d => [(d, Atom d iv v)] -> [(d, Atom d iv v)]
reverseTimedList [] = []
reverseTimedList ((dd,(Atom d v)):l) = (-dd,(Atom d v)):reverseTimedList l
                                       -- this version keeps
                                      -- (-d-dd,(Atom d v)):reverseTimedList l

-- | Transform a timed list into a qlist keeping the distance of the begining of the first atom to the zero
timedListToQList :: (Num d, Lattice d) => [(d, Atom d iv v)] -> (d, QList d iv v)
timedListToQList [] = (0,QEnd)
timedListToQList ((dd,a):l)
  = let (d,q) = timedListToQList l
    in case partialCompare dd d of
         Just LT -> (dd,insertQ (QList [a] (DQ 0 QEnd)) (DQ (d - dd) q))
         Just EQ -> (dd,mergeQ (QList [a] (DQ 0 QEnd),q))
         Just GT -> (d,insertQ q (DQ (dd - d)  (QList [a] (DQ 0 QEnd))))
         Nothing -> error "timedListToQList/Reverse tile : non comparable duration"

-- * Other functions


-- | Unfold all recursive definitions in a qlist (for debug purpose) 
unfoldQ :: Num d => QList d iv v -> QList d iv v
unfoldQ QEnd = QEnd
unfoldQ (QList al (DQ d q)) = QList al (DQ d (unfoldQ q))
unfoldQ (QRec d f p) = stretchQ d (unfoldQ $ (f p))


-- | For on-the fly updates of outputs
instance Updatable (DQ d iv v) d iv  where
     update (f,nq) (DQ d q) = DQ (f d) $ update (f,nq) q

-- | For on-the fly updates of outputs
instance Updatable (QList d iv v) d iv where
  update _ QEnd = QEnd
  update (f,nq) (QList al (DQ d q)) = QList (update (f,nq) al) (DQ (f d) $ update (f,nq) q)
  update (f,nq) (QRec d g p) = QRec (f d) g (update (f,nq) p)


-- | Some functions over qlists

copyAndReplayQ :: (Num d, Lattice d) => d
                                 -> (QList d iv v -> QList d iv v) -> QList d iv v -> QList d iv v
copyAndReplayQ  _ _ QEnd = QEnd
copyAndReplayQ  d f (QRec dd g p) = QRec dd ((copyAndReplayQ  d f).g) p
copyAndReplayQ  d f q
    = mergeQ (takeQ d q,QList [] (DQ d (QRec 1 (\q-> mergeQ (f (takeQ d q), copyAndReplayQ d f $ dropQ d q)) q)))