{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE GADTs, StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}

-- |
-- Module      : OAlg.Entity.Diagram.Transformation
-- Description : natural transformations between diagrams
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- natural transformations between 'Diagram's.
module OAlg.Entity.Diagram.Transformation
  ( -- * Transformation
    Transformation(..), trfs

    -- * Duality
  , coTransformation
  ) where

import Data.Typeable
import Data.Array as A

import OAlg.Prelude

import OAlg.Structure.Exception
import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative as M
import OAlg.Structure.Fibred
import OAlg.Structure.Additive
import OAlg.Structure.Distributive
import OAlg.Structure.Vectorial as V
import OAlg.Structure.Algebraic

import OAlg.Entity.Natural
import OAlg.Entity.FinList

import OAlg.Entity.Diagram.Quiver
import OAlg.Entity.Diagram.Definition

--------------------------------------------------------------------------------
-- Transformation -

-- | natural transformations between two 'Diagram's.
--
-- __Property__ Let @'Transformation' a b t@ be in
-- @'Transformation' __t__ __n__ __m__ __a__@ for a 'Multiplicative' structure __@a@__,
-- then holds
--
-- (1) @'dgQuiver' a '==' 'dgQuiver' b@.
--
-- (2) For all @0 '<=' i '<' n@ holds: @'orientation' (t i) '==' p i ':>' q i@ where
-- @p = 'dgPoints' a@ and @q = 'dgPoints' b@.
--
-- (3) For all @0 '<=' j '<' m@ holds: @t (e j) 'M.*' f j '==' g j 'M.*' t (s j)@
-- where @f = 'dgArrows' a@, @g = 'dgArrows' b@, @s j@ is the index of the start point of
-- the @j@-th arrow and @e j@ is the index of the end point.
--
-- @
--                    t (s j)
--    s j     p (s j) --------> q (s j)
--     |         |                 |
--   j |     f j |                 | g j
--     |         |                 |
--     v         v                 v
--    e j     p (e j) --------> q (e j)
--                    t (e j)
-- @
data Transformation t n m a
  = Transformation (Diagram t n m a) (Diagram t n m a) (FinList n a)
  deriving (Int -> Transformation t n m a -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (t :: DiagramType) (n :: N') (m :: N') a.
Oriented a =>
Int -> Transformation t n m a -> ShowS
forall (t :: DiagramType) (n :: N') (m :: N') a.
Oriented a =>
[Transformation t n m a] -> ShowS
forall (t :: DiagramType) (n :: N') (m :: N') a.
Oriented a =>
Transformation t n m a -> String
showList :: [Transformation t n m a] -> ShowS
$cshowList :: forall (t :: DiagramType) (n :: N') (m :: N') a.
Oriented a =>
[Transformation t n m a] -> ShowS
show :: Transformation t n m a -> String
$cshow :: forall (t :: DiagramType) (n :: N') (m :: N') a.
Oriented a =>
Transformation t n m a -> String
showsPrec :: Int -> Transformation t n m a -> ShowS
$cshowsPrec :: forall (t :: DiagramType) (n :: N') (m :: N') a.
Oriented a =>
Int -> Transformation t n m a -> ShowS
Show,Transformation t n m a -> Transformation t n m a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (t :: DiagramType) (n :: N') (m :: N') a.
Oriented a =>
Transformation t n m a -> Transformation t n m a -> Bool
/= :: Transformation t n m a -> Transformation t n m a -> Bool
$c/= :: forall (t :: DiagramType) (n :: N') (m :: N') a.
Oriented a =>
Transformation t n m a -> Transformation t n m a -> Bool
== :: Transformation t n m a -> Transformation t n m a -> Bool
$c== :: forall (t :: DiagramType) (n :: N') (m :: N') a.
Oriented a =>
Transformation t n m a -> Transformation t n m a -> Bool
Eq)

--------------------------------------------------------------------------------
-- trfs -

-- | the underlying list of factors.
trfs :: Transformation t n m a -> FinList n a
trfs :: forall (t :: DiagramType) (n :: N') (m :: N') a.
Transformation t n m a -> FinList n a
trfs (Transformation Diagram t n m a
_ Diagram t n m a
_ FinList n a
fs) = FinList n a
fs

--------------------------------------------------------------------------------
-- Transformaltion - Duality -

type instance Dual (Transformation t n m a) = Transformation (Dual t) n m (Op a)

-- | the dual transformation.
coTransformation :: Transformation t n m a -> Dual (Transformation t n m a)
coTransformation :: forall (t :: DiagramType) (n :: N') (m :: N') a.
Transformation t n m a -> Dual (Transformation t n m a)
coTransformation (Transformation Diagram t n m a
a Diagram t n m a
b FinList n a
ts)
  = forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a
-> Diagram t n m a -> FinList n a -> Transformation t n m a
Transformation (forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> Dual (Diagram t n m a)
coDiagram Diagram t n m a
b) (forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> Dual (Diagram t n m a)
coDiagram Diagram t n m a
a) (forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall x. x -> Op x
Op FinList n a
ts)

--------------------------------------------------------------------------------
-- Transformation - Entity -

l1, l2, l3 :: Label
l1 :: Label
l1 = String -> Label
Label String
"1"
l2 :: Label
l2 = String -> Label
Label String
"2"
l3 :: Label
l3 = String -> Label
Label String
"3"

vldTrDiscrete :: Oriented a
  => N -> FinList n (Point a) -> FinList n (Point a) -> FinList n a -> Statement
vldTrDiscrete :: forall a (n :: N').
Oriented a =>
N
-> FinList n (Point a)
-> FinList n (Point a)
-> FinList n a
-> Statement
vldTrDiscrete N
_ FinList n (Point a)
Nil FinList n (Point a)
Nil FinList n a
Nil = Statement
SValid
vldTrDiscrete N
i (Point a
p:|FinList n (Point a)
ps) (Point a
q:|FinList n (Point a)
qs) (a
t:|FinList n a
ts)
  = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
t
        , Label
l2 Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
t forall a. Eq a => a -> a -> Bool
== Point a
p forall p. p -> p -> Orientation p
:> Point a
q)
            Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(i,p,q,t)"String -> String -> Parameter
:=forall a. Show a => a -> String
show (N
i,Point a
p,Point a
q,a
t)]
        , forall a (n :: N').
Oriented a =>
N
-> FinList n (Point a)
-> FinList n (Point a)
-> FinList n a
-> Statement
vldTrDiscrete (forall a. Enum a => a -> a
succ N
i) FinList n (Point a)
ps FinList n (Point a)
qs FinList n a
ts
        ]

vldTrChainTo :: Multiplicative a
  => N -> (Point a,FinList m a) -> (Point a,FinList m a) -> FinList (m+1) a -> Statement
vldTrChainTo :: forall a (m :: N').
Multiplicative a =>
N
-> (Point a, FinList m a)
-> (Point a, FinList m a)
-> FinList (m + 1) a
-> Statement
vldTrChainTo N
i (Point a
p,FinList m a
fs) (Point a
q,FinList m a
gs) (a
t:|FinList n a
ts)
  = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
t
        , Label
l2 Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
t forall a. Eq a => a -> a -> Bool
== Point a
pforall p. p -> p -> Orientation p
:>Point a
q)
            Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(i,p,q,t)"String -> String -> Parameter
:=forall a. Show a => a -> String
show (N
i,Point a
p,Point a
q,a
t)]
        , forall a (m :: N').
Multiplicative a =>
N -> FinList m a -> FinList m a -> FinList (m + 1) a -> Statement
vldChTo N
i FinList m a
fs FinList m a
gs (a
tforall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:|FinList n a
ts)
        ] where
  vldChTo :: Multiplicative a
    => N -> FinList m a -> FinList m a -> FinList (m+1) a -> Statement
  vldChTo :: forall a (m :: N').
Multiplicative a =>
N -> FinList m a -> FinList m a -> FinList (m + 1) a -> Statement
vldChTo N
_ FinList m a
Nil FinList m a
Nil (a
_:|FinList n a
Nil) = Statement
SValid
  vldChTo N
i (a
f:|FinList n a
fs) (a
g:|FinList n a
gs) (a
r:|a
s:|FinList n a
ts)
    = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
s
          , Label
l2 Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
s forall a. Eq a => a -> a -> Bool
== Point a
p' forall p. p -> p -> Orientation p
:> Point a
q')
              Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(i,p',q',s)"String -> String -> Parameter
:=forall a. Show a => a -> String
show (N
i,Point a
p',Point a
q',a
s)]
          , Label
l3 Label -> Statement -> Statement
:<=>: (a
rforall c. Multiplicative c => c -> c -> c
*a
f forall a. Eq a => a -> a -> Bool
== a
gforall c. Multiplicative c => c -> c -> c
*a
s)
              Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(i,r,f,g,s)"String -> String -> Parameter
:=forall a. Show a => a -> String
show (N
i,a
r,a
f,a
g,a
s)]
          , forall a (m :: N').
Multiplicative a =>
N -> FinList m a -> FinList m a -> FinList (m + 1) a -> Statement
vldChTo (forall a. Enum a => a -> a
succ N
i) FinList n a
fs FinList n a
gs (a
sforall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:|FinList n a
ts)
          ] where
    p' :: Point a
p' = forall q. Oriented q => q -> Point q
start a
f
    q' :: Point a
q' = forall q. Oriented q => q -> Point q
start a
g
  
vldTrPrlLR :: Multiplicative a
  => (Point a,Point a,FinList m a) -> (Point a,Point a,FinList m a)
  -> FinList N2 a -> Statement
vldTrPrlLR :: forall a (m :: N').
Multiplicative a =>
(Point a, Point a, FinList m a)
-> (Point a, Point a, FinList m a) -> FinList N2 a -> Statement
vldTrPrlLR (Point a
p,Point a
p',FinList m a
fs) (Point a
q,Point a
q',FinList m a
gs) (a
r:|a
s:|FinList n a
Nil)
  = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid (a
r,a
s)
        , Label
l2 Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
r forall a. Eq a => a -> a -> Bool
== Point a
p forall p. p -> p -> Orientation p
:> Point a
q)
            Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(p,q,r)"String -> String -> Parameter
:=forall a. Show a => a -> String
show (Point a
p,Point a
q,a
r)]
        , Label
l2 Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
s forall a. Eq a => a -> a -> Bool
== Point a
p' forall p. p -> p -> Orientation p
:> Point a
q')
            Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(p',q',s)"String -> String -> Parameter
:=forall a. Show a => a -> String
show (Point a
p',Point a
q',a
s)]
        , forall a (m :: N').
Multiplicative a =>
N -> a -> a -> FinList m a -> FinList m a -> Statement
vld N
0 a
r a
s FinList m a
fs FinList m a
gs
        ] where
  vld :: Multiplicative a => N -> a -> a -> FinList m a -> FinList m a -> Statement
  vld :: forall a (m :: N').
Multiplicative a =>
N -> a -> a -> FinList m a -> FinList m a -> Statement
vld N
_ a
_ a
_ FinList m a
Nil FinList m a
Nil = Statement
SValid
  vld N
j a
r a
s (a
f:|FinList n a
fs) (a
g:|FinList n a
gs)
    = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid (a
f,a
g)
          , Label
l3 Label -> Statement -> Statement
:<=>: (a
sforall c. Multiplicative c => c -> c -> c
*a
f forall a. Eq a => a -> a -> Bool
== a
gforall c. Multiplicative c => c -> c -> c
*a
r)
              Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(j,r,s,f,g)"String -> String -> Parameter
:=forall a. Show a => a -> String
show (N
j,a
r,a
s,a
f,a
g)]
          , forall a (m :: N').
Multiplicative a =>
N -> a -> a -> FinList m a -> FinList m a -> Statement
vld (forall a. Enum a => a -> a
succ N
j) a
r a
s FinList n a
fs FinList n a
gs
          ]

vldTrSink :: Multiplicative a
  => (Point a,FinList m a) -> (Point a,FinList m a) -> FinList (m+1) a -> Statement
vldTrSink :: forall a (m :: N').
Multiplicative a =>
(Point a, FinList m a)
-> (Point a, FinList m a) -> FinList (m + 1) a -> Statement
vldTrSink (Point a
p,FinList m a
fs) (Point a
q,FinList m a
gs) (a
t:|FinList n a
ts)
  = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
t
        , Label
l2 Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
t forall a. Eq a => a -> a -> Bool
== Point a
p forall p. p -> p -> Orientation p
:> Point a
q)
            Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(j,t,p,q)"String -> String -> Parameter
:= forall a. Show a => a -> String
show (N
0::N,a
t,Point a
p,Point a
q)]
        , forall a (m :: N').
Multiplicative a =>
N -> a -> FinList m a -> FinList m a -> FinList m a -> Statement
vld N
1 a
t FinList m a
fs FinList m a
gs FinList n a
ts
        ] where
  vld :: Multiplicative a
    => N -> a -> FinList m a -> FinList m a -> FinList m a -> Statement
  vld :: forall a (m :: N').
Multiplicative a =>
N -> a -> FinList m a -> FinList m a -> FinList m a -> Statement
vld N
_ a
_ FinList m a
Nil FinList m a
Nil FinList m a
Nil = Statement
SValid
  vld N
j a
t0 (a
f:|FinList n a
fs) (a
g:|FinList n a
gs) (a
t:|FinList n a
ts) 
    = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid (a
f,a
g,a
t)
          , Label
l2 Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
t forall a. Eq a => a -> a -> Bool
== forall q. Oriented q => q -> Point q
start a
f forall p. p -> p -> Orientation p
:> forall q. Oriented q => q -> Point q
start a
g)
              Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(j,f,g,t)"String -> String -> Parameter
:=forall a. Show a => a -> String
show (N
j,a
f,a
g,a
t)]
          , Label
l3 Label -> Statement -> Statement
:<=>: (a
t0forall c. Multiplicative c => c -> c -> c
*a
f forall a. Eq a => a -> a -> Bool
== a
gforall c. Multiplicative c => c -> c -> c
*a
t)
              Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(j,t0,f,g,t)"String -> String -> Parameter
:= forall a. Show a => a -> String
show (N
j,a
t0,a
f,a
g,a
t)]
          , forall a (m :: N').
Multiplicative a =>
N -> a -> FinList m a -> FinList m a -> FinList m a -> Statement
vld (forall a. Enum a => a -> a
succ N
j) a
t0 FinList n a
fs FinList n a
gs FinList n a
ts
          ]

vldTrGen :: Multiplicative a
  => Diagram t n m a -> Diagram t n m a -> FinList n a -> Statement
vldTrGen :: forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a -> Diagram t n m a -> FinList n a -> Statement
vldTrGen Diagram t n m a
a Diagram t n m a
b FinList n a
ts
  = [Statement] -> Statement
And [ Label
l1 Label -> Statement -> Statement
:<=>: (Quiver n m
qa forall a. Eq a => a -> a -> Bool
== forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> Quiver n m
dgQuiver Diagram t n m a
b)
            Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(a,b)"String -> String -> Parameter
:=forall a. Show a => a -> String
show (Diagram t n m a
a,Diagram t n m a
b)]
        , forall a (n :: N').
Multiplicative a =>
N
-> FinList n (Point a)
-> FinList n (Point a)
-> FinList n a
-> Statement
vldTr N
0 (forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints Diagram t n m a
a) (forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints Diagram t n m a
b) FinList n a
ts
        , forall a (m :: N').
Multiplicative a =>
N
-> FinList m (Orientation N)
-> FinList m a
-> FinList m a
-> Array N a
-> Statement
vldCm N
0 (forall (n :: N') (m :: N'). Quiver n m -> FinList m (Orientation N)
qvOrientations Quiver n m
qa) (forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> FinList m a
dgArrows Diagram t n m a
a) (forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> FinList m a
dgArrows Diagram t n m a
b) (forall (n :: N') a. FinList n a -> Array N a
toArray FinList n a
ts) 
        ] where

  qa :: Quiver n m
qa = forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> Quiver n m
dgQuiver Diagram t n m a
a
  
  vldTr :: Multiplicative a
    => N -> FinList n (Point a) -> FinList n (Point a) -> FinList n a -> Statement
  vldTr :: forall a (n :: N').
Multiplicative a =>
N
-> FinList n (Point a)
-> FinList n (Point a)
-> FinList n a
-> Statement
vldTr N
_ FinList n (Point a)
Nil FinList n (Point a)
Nil FinList n a
Nil = Statement
SValid
  vldTr N
i (Point a
p:|FinList n (Point a)
ps) (Point a
q:|FinList n (Point a)
qs) (a
t:|FinList n a
ts)
    = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
t
          , Label
l1 Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
t forall a. Eq a => a -> a -> Bool
== Point a
p forall p. p -> p -> Orientation p
:> Point a
q)
              Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(i,p,q,t)"String -> String -> Parameter
:= forall a. Show a => a -> String
show (N
i,Point a
p,Point a
q,a
t)]
          , forall a (n :: N').
Multiplicative a =>
N
-> FinList n (Point a)
-> FinList n (Point a)
-> FinList n a
-> Statement
vldTr (forall a. Enum a => a -> a
succ N
i) FinList n (Point a)
ps FinList n (Point a)
qs FinList n a
ts
          ]
  vldCm :: Multiplicative a
    => N 
    -> FinList m (Orientation N) -> FinList m a -> FinList m a
    -> Array N a
    -> Statement
  vldCm :: forall a (m :: N').
Multiplicative a =>
N
-> FinList m (Orientation N)
-> FinList m a
-> FinList m a
-> Array N a
-> Statement
vldCm N
_ FinList m (Orientation N)
Nil FinList m a
Nil FinList m a
Nil Array N a
_ = Statement
SValid
  vldCm N
j ((N
s:>N
e):|FinList n (Orientation N)
os) (a
f:|FinList n a
fs) (a
g:|FinList n a
gs) Array N a
t
    = [Statement] -> Statement
And [ Label
l3 Label -> Statement -> Statement
:<=>: let {ts :: a
ts = Array N a
t forall i e. Ix i => Array i e -> i -> e
A.! N
s;te :: a
te = Array N a
t forall i e. Ix i => Array i e -> i -> e
A.! N
e} in (a
te forall c. Multiplicative c => c -> c -> c
* a
f forall a. Eq a => a -> a -> Bool
== a
g forall c. Multiplicative c => c -> c -> c
* a
ts)
              Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(j,s,e,f,g,ts,te)"String -> String -> Parameter
:= forall a. Show a => a -> String
show (N
j,N
s,N
e,a
f,a
g,a
ts,a
te)]
          , forall a (m :: N').
Multiplicative a =>
N
-> FinList m (Orientation N)
-> FinList m a
-> FinList m a
-> Array N a
-> Statement
vldCm (forall a. Enum a => a -> a
succ N
j) FinList n (Orientation N)
os FinList n a
fs FinList n a
gs Array N a
t
          ]

vldTr :: Multiplicative a => Transformation t n m a -> Statement
vldTr :: forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Transformation t n m a -> Statement
vldTr t :: Transformation t n m a
t@(Transformation Diagram t n m a
a Diagram t n m a
b FinList n a
ts) = case (Diagram t n m a
a,Diagram t n m a
b) of
  (Diagram t n m a
DiagramEmpty, Diagram t n m a
DiagramEmpty)              -> Statement
SValid
  (DiagramDiscrete FinList n (Point a)
ps,DiagramDiscrete FinList n (Point a)
qs)   -> forall a (n :: N').
Oriented a =>
N
-> FinList n (Point a)
-> FinList n (Point a)
-> FinList n a
-> Statement
vldTrDiscrete N
0 FinList n (Point a)
ps FinList n (Point a)
qs FinList n a
ts
  (DiagramChainTo Point a
p FinList m a
fs,DiagramChainTo Point a
q FinList m a
gs) -> forall a (m :: N').
Multiplicative a =>
N
-> (Point a, FinList m a)
-> (Point a, FinList m a)
-> FinList (m + 1) a
-> Statement
vldTrChainTo N
0 (Point a
p,FinList m a
fs) (Point a
q,FinList m a
gs) FinList n a
ts
  (DiagramParallelLR Point a
p Point a
p' FinList m a
fs,DiagramParallelLR Point a
q Point a
q' FinList m a
gs)
    -> forall a (m :: N').
Multiplicative a =>
(Point a, Point a, FinList m a)
-> (Point a, Point a, FinList m a) -> FinList N2 a -> Statement
vldTrPrlLR (Point a
p,Point a
p',FinList m a
fs) (Point a
q,Point a
q',FinList m a
gs) FinList n a
ts
  (DiagramSink Point a
p FinList m a
fs,DiagramSink Point a
q FinList m a
gs)       -> forall a (m :: N').
Multiplicative a =>
(Point a, FinList m a)
-> (Point a, FinList m a) -> FinList (m + 1) a -> Statement
vldTrSink (Point a
p,FinList m a
fs) (Point a
q,FinList m a
gs) FinList n a
ts
  (DiagramGeneral FinList n (Point a)
_ FinList m (a, Orientation N)
_,DiagramGeneral FinList n (Point a)
_ FinList m (a, Orientation N)
_)   -> forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a -> Diagram t n m a -> FinList n a -> Statement
vldTrGen Diagram t n m a
a Diagram t n m a
b FinList n a
ts
  (Diagram t n m a, Diagram t n m a)
_                                         -> forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Transformation t n m a -> Statement
vldTr (forall (t :: DiagramType) (n :: N') (m :: N') a.
Transformation t n m a -> Dual (Transformation t n m a)
coTransformation Transformation t n m a
t)

instance Multiplicative a => Validable (Transformation t n m a) where
  valid :: Transformation t n m a -> Statement
valid t :: Transformation t n m a
t@(Transformation Diagram t n m a
a Diagram t n m a
b FinList n a
_) = String -> Label
Label String
"Transformation" Label -> Statement -> Statement
:<=>:
    [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid (Diagram t n m a
a,Diagram t n m a
b) 
        , forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Transformation t n m a -> Statement
vldTr Transformation t n m a
t
        ]

instance ( Multiplicative a
         , Typeable t, Typeable n, Typeable m
         )
  => Entity (Transformation t n m a)

--------------------------------------------------------------------------------
-- Multiplicative -

instance ( Multiplicative a
         , Typeable t, Typeable n, Typeable m
         )
  => Oriented (Transformation t n m a) where
  type Point (Transformation t n m a) = Diagram t n m a
  orientation :: Transformation t n m a
-> Orientation (Point (Transformation t n m a))
orientation (Transformation Diagram t n m a
a Diagram t n m a
b FinList n a
_) = Diagram t n m a
aforall p. p -> p -> Orientation p
:>Diagram t n m a
b

instance ( Multiplicative a
         , Typeable t, Typeable n, Typeable m
         )
  => Multiplicative (Transformation t n m a) where
  one :: Point (Transformation t n m a) -> Transformation t n m a
one Point (Transformation t n m a)
d = forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a
-> Diagram t n m a -> FinList n a -> Transformation t n m a
Transformation Point (Transformation t n m a)
d Point (Transformation t n m a)
d FinList n a
ts where
    ts :: FinList n a
ts = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall c. Multiplicative c => Point c -> c
one forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints Point (Transformation t n m a)
d
    
  Transformation Diagram t n m a
a Diagram t n m a
b FinList n a
fs * :: Transformation t n m a
-> Transformation t n m a -> Transformation t n m a
* Transformation Diagram t n m a
c Diagram t n m a
d FinList n a
gs
    | Diagram t n m a
d forall a. Eq a => a -> a -> Bool
== Diagram t n m a
a    = forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a
-> Diagram t n m a -> FinList n a -> Transformation t n m a
Transformation Diagram t n m a
c Diagram t n m a
b (forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall c. Multiplicative c => c -> c -> c
(*)) (FinList n a
fs forall (n :: N') a b.
FinList n a -> FinList n b -> FinList n (a, b)
`zip` FinList n a
gs))
    | Bool
otherwise = forall a e. Exception e => e -> a
throw ArithmeticException
NotMultiplicable

  npower :: Transformation t n m a -> N -> Transformation t n m a
npower Transformation t n m a
t N
1                       = Transformation t n m a
t
  npower Transformation t n m a
t N
_ | forall b. Boolean b => b -> b
not (forall q. Oriented q => q -> Bool
isEndo Transformation t n m a
t)      = forall a e. Exception e => e -> a
throw ArithmeticException
NotExponential
  npower (Transformation Diagram t n m a
a Diagram t n m a
_ FinList n a
ts) N
n = forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a
-> Diagram t n m a -> FinList n a -> Transformation t n m a
Transformation Diagram t n m a
a Diagram t n m a
a (forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall c. Multiplicative c => c -> N -> c
`npower` N
n) FinList n a
ts)

instance ( Distributive a
         , Typeable t, Typeable n, Typeable m
         )
  => Fibred (Transformation t n m a) where
  type Root (Transformation t n m a) = Orientation (Diagram t n m a)
  
instance ( Distributive a
         , Typeable t, Typeable n, Typeable m
         )
  => FibredOriented (Transformation t n m a)

instance ( Distributive a
         , Typeable t, Typeable n, Typeable m
         )
  => Additive (Transformation t n m a) where
  zero :: Root (Transformation t n m a) -> Transformation t n m a
zero (Diagram t n m a
a:>Diagram t n m a
b) = forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a
-> Diagram t n m a -> FinList n a -> Transformation t n m a
Transformation Diagram t n m a
a Diagram t n m a
b FinList n a
zs where
    zs :: FinList n a
zs = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall a. Additive a => Root a -> a
zero forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall p. p -> p -> Orientation p
(:>)) (forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints Diagram t n m a
a forall (n :: N') a b.
FinList n a -> FinList n b -> FinList n (a, b)
`zip` forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints Diagram t n m a
b)
    
  Transformation Diagram t n m a
a Diagram t n m a
b FinList n a
fs + :: Transformation t n m a
-> Transformation t n m a -> Transformation t n m a
+ Transformation Diagram t n m a
c Diagram t n m a
d FinList n a
gs
    | Diagram t n m a
aforall p. p -> p -> Orientation p
:>Diagram t n m a
b forall a. Eq a => a -> a -> Bool
== Diagram t n m a
cforall p. p -> p -> Orientation p
:>Diagram t n m a
d = forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a
-> Diagram t n m a -> FinList n a -> Transformation t n m a
Transformation Diagram t n m a
a Diagram t n m a
b (forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Additive a => a -> a -> a
(+)) (FinList n a
fs forall (n :: N') a b.
FinList n a -> FinList n b -> FinList n (a, b)
`zip` FinList n a
gs))
    | Bool
otherwise    = forall a e. Exception e => e -> a
throw ArithmeticException
NotAddable

  ntimes :: N -> Transformation t n m a -> Transformation t n m a
ntimes N
n (Transformation Diagram t n m a
a Diagram t n m a
b FinList n a
ts) = forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a
-> Diagram t n m a -> FinList n a -> Transformation t n m a
Transformation Diagram t n m a
a Diagram t n m a
b (forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall a. Additive a => N -> a -> a
ntimes N
n) FinList n a
ts)

instance ( Distributive a
         , Typeable t, Typeable n, Typeable m
         )
  => Distributive (Transformation t n m a)

instance ( Distributive a, Abelian a
         , Typeable t, Typeable n, Typeable m
         )
  => Abelian (Transformation t n m a) where
  negate :: Transformation t n m a -> Transformation t n m a
negate (Transformation Diagram t n m a
a Diagram t n m a
b FinList n a
ts) = forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a
-> Diagram t n m a -> FinList n a -> Transformation t n m a
Transformation Diagram t n m a
a Diagram t n m a
b (forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall a. Abelian a => a -> a
negate FinList n a
ts)
  ztimes :: Z -> Transformation t n m a -> Transformation t n m a
ztimes Z
z (Transformation Diagram t n m a
a Diagram t n m a
b FinList n a
ts) = forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a
-> Diagram t n m a -> FinList n a -> Transformation t n m a
Transformation Diagram t n m a
a Diagram t n m a
b (forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall a. Abelian a => Z -> a -> a
ztimes Z
z) FinList n a
ts)

instance ( Distributive a, Vectorial a
         , Typeable t, Typeable n, Typeable m
         )
  => Vectorial (Transformation t n m a) where
  type Scalar (Transformation t n m a) = Scalar a
  Scalar (Transformation t n m a)
s ! :: Scalar (Transformation t n m a)
-> Transformation t n m a -> Transformation t n m a
! (Transformation Diagram t n m a
a Diagram t n m a
b FinList n a
ts) = forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a
-> Diagram t n m a -> FinList n a -> Transformation t n m a
Transformation Diagram t n m a
a Diagram t n m a
b (forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (Scalar (Transformation t n m a)
s forall v. Vectorial v => Scalar v -> v -> v
V.!) FinList n a
ts)

instance ( Algebraic a
         , Typeable t, Typeable n, Typeable m
         )
  => Algebraic (Transformation t n m a)