{-|
Module      : FuncTile
Description : Functions over tiles
Copyright   : (c) David Janin, 2016
License     : see the LICENSE file in the distribution
Maintainer  : janin@labri.fr
Stability   : experimental

Functions from tiles to tiles inherit from the rich algebraic structure of tiles. Then, defining 
/delay preserving functions/, we eventually get a monoidal cartesian closed category that is also a (weak) semiadditive category, with parallel product of functions as abelian, linear product in homsets (see "Tile.TCategories" for the various instances within "Control.Category"). 

-}

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

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


module Tile.Functile where

import Duration.Lattice

import Tile.Tile
import Tile.QList
-- import Tile.Atom
    
import Text.Show.Functions()

    

-- import Debug.Trace

------------------------------------------------------
-- * Functions over tiles and two subclasses
------------------------------------------------------

-- | Type functile is just a type synonym for functions from tile to tile. Yet, Functile d iv v1 v2
-- inherits from the inverse structure of its codomain and its extension to Num and Fractional.
--
type Functile d iv v1 v2 = Tile d iv v1 -> Tile d iv v2


-- ** Duration preserving functions

-- | A tile function is a /duration preserving/ tile function when
--
-- prop> durationT t == durationT (f t)
--
isDurationPreserving :: (Eq d, Num d, Lattice d, POrd v2) => Functile d iv v1 v2 -> Tile d iv v1 -> Bool
isDurationPreserving f t = durationT t == durationT (f t)

-- | Maps every tile function to a /duration preserving/ tile function.
-- 
-- @
-- forceDurP f t = re [f t] + delayT t
-- @
--
-- in such a way that
--
-- prop> re[forceDurP f t] == re[f t]

forceDurP :: (Eq d, Num d, POrd v1, Lattice d) => Functile d iv v1 v2 -> Functile d iv v1 v2
forceDurP f t = re [f t] + delayT t


-- ** Delay preserving functions

-- | A stronger notion: a tile function is a /delay preserving/ tile function when
--
-- prop> f (delayT t) == delayT (f t)

isDelayPreserving :: (Eq d, Num d, Lattice d, POrd v2) => Functile d iv v1 v2 -> Tile d iv v1 -> Bool
isDelayPreserving f t = f (delayT t) == delayT (f t)

-- | Maps every tile function to a /delay preserving/ tile function.
-- 
-- @
-- forceDelayP f t = re [f t] + delayT t
-- @
--
-- in such a way that
--
-- prop> (t /= delayT t) implies re[forceDelayP f t] == re[f t]
--
-- Clearly, we also have
--
-- prop> isDelayPreserving t => isDurationPreserving t

forceDelayP :: (Eq d, Num d, POrd v1, Lattice d) => Functile d iv v1 v2 -> Functile d iv v1 v2
forceDelayP f t = case (t == delayT t) of
                True -> delayT t
                False -> re [f t] + delayT t

------------------------------------------------------
-- * Terminal and (weak) initial objects
------------------------------------------------------


-- | The empty tile type is terminal and weak initial
-- restricting to duration preserving functions
-- with function 'delayT' as arrow from and to the empty tile type.
--
-- Restricting further to delay preserving functions makes
-- EmptyTile d iv truely initial (delayT is the unique arrow
-- from EmptyTile d iv into Tile d iv).
--
-- For all  f :: Tile d iv v -> Tile d iv Void
--
-- prop> isDurationPreserving f implies f t == delayT t
--
-- and for all  f :: Tile d iv Void -> Tile d iv v
--
-- prop> isDelayPreserving f implies f t == delayT t

type EmptyTile d iv = Tile d iv Void

-- | Our adhoc encoding of the empty type
data Void

instance Show (Void) where
    show _ = "<void>"

instance POrd (Void) where
    pLeq _ _ = True

------------------------------------------------------
-- * Exponentiation
------------------------------------------------------

          
-- | Applies a tile of functions over tiles to a tile. This function is delay preserving in its second
-- arguement:
--
-- prop> delayT (applyT tf t) == delayT t
applyT ::  (Num d, Eq d, Lattice d) => Tile d iv (Functile d iv v1 v2)
     -> Tile d iv v1 -> Tile d iv v2
applyT (Tile _ _ QEnd) t = delayT t
applyT tf ta = evalT $ re [toLeftT tf] + (toRightT ta)

{-
applyT f t
  = let dfl = getAllFromAtomsT f
        df = delayToTailT f
        evalA [] _ = []
        evalA ((d1,f1):l) t@(Tile d ad q)
          = (f1 (Tile d ad (takeQ (d1-ad) q))): evalA l t
            -- f1 is applied to a tile with same duration as t
    in re (evalA dfl t) + df + recT applyT (tailT f) (dropD (durationT df) t)  -- version 1 (without meet)
--        dt = delayToTailT t
--        d = minDelayT df dt
--    in re (evalA dfl t) + d + applyT (df - d + tailT f) (dt - d + tailT t)  -- version 2 (with meet)
-}    


-- | Lifts a function over tiles into a tile of function of tile, in such a way that
--
-- prop> f t == applyT (fromFuncT f) t
--
-- Warning : for this, we truly need a greatest element (aka top) in the lattice d
fromFuncT :: (Num d, Eq d, Lattice d) => Functile d iv v1 v2 ->  Tile d iv (Functile d iv v1 v2)
fromFuncT f = fromValueT f


------------------------------------------------------
-- * Monoidal properties
------------------------------------------------------

-- | Evaluates the categorical product of a tile of functions and an argument tile.
-- Argument tile is cut according to the duration of functions to be applied.
evalT :: (Num d, Eq d, Lattice d) =>  Tile d iv (Either (Functile d iv v1 v2) v1) -> Tile d iv v2
evalT t = case unfoldNowT t of
 Tile _ _ QEnd -> 0                           
 _ -> let af = [(d,f) | (d,Left f) <- getAllFromAtomsT t]
      in re (map (\(d,f) -> f (takeD d (fromRightT t))) af) + delayToTailT t + recT (\_ t -> evalT t) () (tailT t)
-- evalT t = recT applyT (fromLeftT t) (fromRightT t)

-- | Currifies a function of tiles (duration/delay preservation properties yet to be checked)
curryT :: (Num d, Eq d, Lattice d) => Functile d iv (Either v1 v2) v3 ->  Functile d iv v1 (Functile d iv v2 v3)
curryT f t1 = let g t2 =  f (re[toRightT t2] + toLeftT t1)
              in fromFuncT g 
          
-- | Uncurrifies a function of tiles (duration/delay preservation properties yet to be checked)
uncurryT :: (Num d, Eq d, Lattice d) => Functile d iv v1 (Functile d iv v2 v3) -> Functile d iv (Either v1 v2) v3
uncurryT g t = let f = g (fromLeftT t)
               in applyT f (fromRightT t)


-- | Swaps left and right types in a biproduct type
swapT :: (Eq d, Num d, Lattice d) =>
               Tile d iv (Either v1 v2) -> Tile d iv (Either v2 v1)
swapT t = re[(toLeftT . fromRightT) t] + (toRightT  .fromLeftT) t
                  
------------------------------------------------------
-- * Categorical sum and product
------------------------------------------------------

-- ** Left and right projections

-- | Canonical left projection
fromLeftT :: (Num d, Eq d, Lattice d) => Functile d iv (Either v1 v2) v1
fromLeftT  (Tile d _ QEnd) = Tile d 0 QEnd
fromLeftT (Tile d ad q) = Tile d ad (fromLeftQ q)

-- | Canonical right projection
fromRightT :: (Num d, Eq d, Lattice d) => Functile d iv (Either v1 v2) v2
fromRightT (Tile d _ QEnd) = Tile d 0 QEnd
fromRightT (Tile d ad q) = Tile d ad (fromRightQ q)

-- ** Left and right injections

-- | Canonical left injection
toLeftT :: (Num d, Eq d, Lattice d) => Functile d iv v1 (Either v1 v2)
toLeftT (Tile d _ QEnd) = Tile d 0 QEnd
toLeftT (Tile d ad q) = Tile d ad (fmapQ Left q)
{-
toLeftT t    
    = let h1 = map (fmapT Left) (atomsT t)
          d1 = delayToTailT t
      in re h1 + d1
      + recT (\_ -> \t -> toLeftT t) () (tailT t)
-}

-- | Canonical right injection
--
-- With combination properties
--
-- prop> id==fromLeftT . toLeftT and id == fromRightT . toRightT
--
-- prop> delayT==fromLeftT . toRightT and delayT == fromRightT . toLeftT

toRightT :: (Num d, Eq d, Lattice d) => Functile d iv v2 (Either v1 v2)
toRightT  (Tile d _ QEnd) = Tile d 0 QEnd
toRightT (Tile d ad q) = Tile d ad (fmapQ Right q)
{- toRightT t                    
  = let h1 = map (fmapT Right) (atomsT t)
        d1 = delayToTailT t     
    in re h1 + d1
       + recT (\_ -> \t -> toRightT t) () (tailT t)
-}

-- ** Factorization through product

-- | Factorizes tile functions through product, that is, for all /duration preserving/ functions, 
-- the following properties are satisfied:
--
-- prop> fromLeftT (factorProductT f1 f2 t) ==  f1 t
--
-- prop> fromRightT (factorProductT f1 f2 t) ==  f2 t
--
-- In other words, provided unicity of such a factorization, Tile d iv (Either v1 v2) is the categorical product of Tile d iv v1 and Tile d iv v1.

factorProductT :: (Eq d, Num d,Lattice d) =>
           (Functile  d iv v v1) -> (Functile d iv v v2)
              -> Functile d iv v  (Either v1 v2) 
factorProductT f1 f2 = \t -> parForkT (toLeftT (f1 t)) (toRightT (f2 t))


-- ** Factorization through sum (not unique)

-- | Factorizes tile functions through sum, that is, for all /delay preserving/ functions,
-- the following properties are satisfied:
--
-- prop> factorSumT f1 f2 (toLeftT t) ==  f1 t
--
-- prop> factorSumT f1 f2 (toRightT t) ==  f2 t
--
-- In other words, provided unicity of such a factorization, Tile d iv (Either v1 v2) is the categorical sum of Tile d iv v1 and Tile d iv v1

factorSumT :: (Eq d, Num d,Lattice d) =>
           (Functile  d iv v1 v) -> (Functile d iv v2 v)
              -> Functile d iv (Either v1 v2) v
factorSumT f1 f2 = \t -> parForkT (f1 (fromLeftT t)) (f2 (fromRightT t))


------------------------------------------------------
-- * More on the resulting weak semiadditive category
------------------------------------------------------

-- ** Routing primitives

-- | Mixes two tiles almost without loss of information.
muxT :: (Eq d, Num d, Lattice d) =>
              (Tile d iv v1,Tile d iv v2) -> Tile d iv (Either v1 v2)
muxT (t1,t2) = re[toLeftT t1] + toRightT t2

-- | Demixes a mixed tile without loss of information.
-- The property
--
-- prop> muxT . demuxT t == t
--
-- holds for every tile /t/ of Tile d iv (Either v1 v2),
-- and the property
--
-- prop> demuxT . muxT (t1,t2) == (t1,t2)
--
-- holds whenever |duration t1 == duration t2|.

demuxT :: (Eq d, Num d, Lattice d) =>
                Tile d iv (Either v1 v2) -> (Tile d iv v1, Tile d iv v2)
demuxT t = (fromLeftT t, fromRightT t)

-- ** Parallel application of tile functions

-- | Applies in a list of functions over the same arguement and return the parallel merge of their results.
-- This parallel product of functions is defined by:
--
-- @
-- parFT [] t = delayT t
-- parFT (f:fs) t = re [f t] + parFT fs t
-- @
--
-- Remark : with zero object and finite products and sums that coincides, the category of delay preserving tile functions
-- is a 'semiadditive category'. The binary version of the parallel composition is the induced abelian monoid product inside homsets.
 
parFT :: (Eq d, Num d, Lattice d) =>
                       [Functile d iv v1 v2] ->  (Functile d iv v1 v2)
parFT [] t = delayT t
parFT (f:fs) t = re [f t] + parFT fs t

infixl 9 |+|
(|+|) :: (Eq d, Num d, Lattice d) => Functile d iv v1 v2 -> Functile d iv v1 v2 -> Functile d iv v1 v2
f1 |+|  f2 = parFT [f1,f2]
-- ^ Derived binary parallel product defined by
--
-- prop> f1 |+| f2 = parFT [f1,f2]
--
-- Properties of the binary parallel product:
--
-- * Neutral element:
--
-- prop> f |+| delayT == forceDurP f, delayT |+| f  == forceDurP f
--
-- * Associativity:
--
-- prop> f1 |+| (f2 |+| f3) == (f1 |+| f2) |+| f3
--
-- * Commutativity:
--
-- prop> f1 |+| f2 == f2 |+| f1
--
-- * Idempotence
--
-- prop> (f |+| f) == f
--
-- * Distributivity
--
-- prop> (f1 |+| f2) . g == (f1 . g) |+| (f2 . g)
--
-- The following property would hold in an additive category...
--
-- prop> g . (f1 |+| f2) /= (g . f1) |+| (g . f2) for some g

-- ** Sequential application of tile functions

-- | Applies in a list of functions over the same arguement and return the sequential merge of their results.
-- This sequential product is defined by:
--
-- @
-- seqFT [] t = delayT t
-- seqFT (f:fs) t = re[f t + seqFT fs t] + delayT t
-- @
seqFT :: (Eq d, Num d, Lattice d) =>
               [Functile d iv v1 v2] -> Functile d iv v1 v2
seqFT [] t = delayT t
seqFT (f:fs) t = re[f t + seqFT fs t] + delayT t

infixl 8 |*|
(|*|) :: (Eq d, Num d, Lattice d) => Functile d iv v1 v2 -> Functile d iv v1 v2 -> Functile d iv v1 v2
f1 |*|  f2 = seqFT [f1,f2]
-- ^ Derived binary sequential composition defined by
--
-- prop> f1 |*| f2 = seqFT [f1,f2]
--
-- Properties of the binary sequential product:
--
-- prop> yet to be discovered....

------------------------------------------------------
-- * Function examples
------------------------------------------------------


-- | Records slices of the input tile of some duration and replay them applying some function parameter.
--
-- @
-- recordAndReplay d f t
--    = let recordD = takeD d t
--      in recordD + re [f recordD] + recT (recordAndReplayD d) f (dropD d t)
-- @
--
-- This is a typical example of a pull reactive function where the clock structure of the output is governed
-- by itself.
recordAndReplayD :: (Eq d, Num d, Lattice d) =>
                       d -> (Functile d iv v v) -> Functile d iv v v
recordAndReplayD _ _ (Tile d _ QEnd) = Tile d 0 QEnd
recordAndReplayD 0 _ t = t
recordAndReplayD d f t
    = let recordD = recT (\_ -> \t -> takeD d t) () t
      in recordD + re [f recordD] + recT (recordAndReplayD d) f (dropD d t)

-- Num instance
instance  (Eq d, Num d, Lattice d) => Num (Functile d iv v1 v2) where
    (+) f1 f2 t = (f1 t) + (f2 t)
    (*) f1 f2 t = (f1 t) * (f2 t)
    negate f t = negate (f t) 
    fromInteger n = const $ (fromInteger n)
    abs = const $ const (fromInteger 1) 
    signum = id

-- Fractional instance
instance (Eq d, Fractional d, Lattice d) => Fractional (Functile d iv v1 v2) where
    fromRational n = const $ (fromRational n)
    recip f t = recip (f t)