{-|
Module      : Docs.Additive
Description : Examples and properties of the tile algebra
Copyright   : (c) David Janin, 2016
License     : see the LICENSE file in the distribution
Maintainer  : janin@labri.fr
Stability   : experimental

Sum, negation and few axioms from inverse semigroup theory.

-}

module Docs.Additive where

import Tile.Tile

-- * The additive monoid of tiles
--
-- ** temporal values
-- | A basic atomic tile (temporal value):
--
-- @
-- b0 = fromDurationAndValueT 3 'a'
-- @
--
-- It can be depicted by
--
-- <<ex1.svg A basic temporal value>>
--
-- with duration d=3 and value v='a'.
b0 :: Tile Integer Char Char
b0 = fromDurationAndValueT 3 'a'

-- ** Delay
-- | A basic delay tile:
--
-- @
-- b1 = fromDurationT 3
-- @
--
-- It can be depicted by
--
-- <<ex2.svg A delay>>
--
-- with duration d=3. Forgeting values is handled by the /delayT/ functions with
--
-- prop> b1 == delayT b0
b1 :: Tile Integer Char Char
b1 = fromDurationT 3

-- ** Sum 
-- | The sum of two tiles amounts to merge the output root of the first one with the inoput root of the second.
--
-- @
-- b2 = x + y
-- @
--
-- It can be depicted by
--
-- <<ex3.svg A simple sum>>
--
-- with x = fromDurationAndValueT  3 'a' and y = fromDurationAndValueT  2 'b'.
--
-- Property: function delayT is functorial over sum:
--
-- prop> delayT (x+y) == delayT x + delayT y

b2 :: Tile Integer Char Char
b2 = fromDurationAndValueT 3 'a' + fromDurationAndValueT 2 'b'
   
-- ** Negation 
-- | The negation of a tile amounts to flip input and ouput roots.
--
-- @
-- b3 = -x
-- @
--
-- It can be depicted by
--
-- <<ex4.svg A negated tile>>
--
-- with x = fromDurationAndValueT  3 'a'.
--
-- Property: the negation distributes over sums reversing it.
--
-- prop> - (x+y) == - y - x

b3 :: Tile Integer Char Char
b3 = - fromDurationAndValueT 3 'a'

-- ** Difference
-- | The induced difference x - y defined as x + (-y).
--
-- @
-- b4 = x - y
-- @
--
-- It can be depicted by
--
-- <<ex5.svg A tile difference>>
--
-- Property : delayT is also functorial with respect to difference
--
-- prop> delayT (x - y) == delayT x - delayT y

b4 :: Tile Integer Char Char
b4 = fromDurationAndValueT 3 'a' - fromDurationAndValueT 2 'b'

-- ** Spatio-temporal resulting zigzags
-- | Temporal zigzag as a more general structure
--
-- @
-- b5 = x1 - x2 + x3 -x4 
-- @
--
-- It can be depicted by
--
-- <<ex6.svg A zigzag>>
--
-- with x1 = fromDurationAndValueT 3 'a', x2 = fromDurationAndValueT 5 'b',
-- x3 = fromDurationAndValueT 7 'c' and x4 = fromDurationAndValueT 3 'd'
b5 :: Tile Integer Char Char
b5 = fromDurationAndValueT 3 'a' - fromDurationAndValueT 5 'b'
     + fromDurationAndValueT 7 'c' - fromDurationAndValueT 3 'd'

-- ** Semigroup inverse 
-- | Merging parallel temporal values
--
-- @
-- b6 = x - x + x
-- @
--
-- Both x and x - x + x are depicted by
--
-- <<ex7.svg A negated tile>>
--
-- and we have
--
-- prop> x == x - x + x
b6 :: Tile Integer Char Char
b6 = fromDurationAndValueT 3 'a' - fromDurationAndValueT 3 'a' + fromDurationAndValueT 3 'a'
     

-- ** Idempotent tiles
-- | The coreset co[x] of a tile x is obtained by moving its input root to its ouput root. Dually,
-- the reset re[y] of a tile is otained by moving its ouput root to its input root.
-- 
--
-- @
-- b7 = co[x] + re[y]
-- @
--
-- When input and out roots coincides, as in co[x] or re[y], elements are idempotents.
--
-- <<ex8.svg A gneric idempotent>>
--
-- and we have:
--
-- prop> re[x] == x - x  and  x == re[x] + x
-- prop> co[y] == -y + y  and  y == y + co[y]
b7 :: Tile Integer Char Char
b7 = co [fromDurationAndValueT 3 'a'] + re[fromDurationAndValueT 2 'b']