{-# 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
  (
    DiagramTrafo(..), dgts, dgtTypeRefl
  , dgtMapS, dgtMapCov, dgtMapCnt

  ) where

import Data.Typeable
import Data.Array as A

import OAlg.Prelude

import OAlg.Category.SDuality

import OAlg.Data.Either

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

import OAlg.Hom.Oriented
import OAlg.Hom.Multiplicative

import OAlg.Entity.Natural
import OAlg.Entity.FinList
import OAlg.Entity.Diagram.Quiver
import OAlg.Entity.Diagram.Definition

--------------------------------------------------------------------------------

-- DiagramTrafo -


-- | natural transformations between two 'Diagram's.

--

-- __Property__ Let @'DiagramTrafo' a b t@ be in

-- @'DiagramTrafo' __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 DiagramTrafo t n m a
  = DiagramTrafo (Diagram t n m a) (Diagram t n m a) (FinList n a)
  deriving (Int -> DiagramTrafo t n m a -> ShowS
[DiagramTrafo t n m a] -> ShowS
DiagramTrafo t n m a -> String
(Int -> DiagramTrafo t n m a -> ShowS)
-> (DiagramTrafo t n m a -> String)
-> ([DiagramTrafo t n m a] -> ShowS)
-> Show (DiagramTrafo t n m a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (t :: DiagramType) (n :: N') (m :: N') a.
(ShowPoint a, Show a) =>
Int -> DiagramTrafo t n m a -> ShowS
forall (t :: DiagramType) (n :: N') (m :: N') a.
(ShowPoint a, Show a) =>
[DiagramTrafo t n m a] -> ShowS
forall (t :: DiagramType) (n :: N') (m :: N') a.
(ShowPoint a, Show a) =>
DiagramTrafo t n m a -> String
$cshowsPrec :: forall (t :: DiagramType) (n :: N') (m :: N') a.
(ShowPoint a, Show a) =>
Int -> DiagramTrafo t n m a -> ShowS
showsPrec :: Int -> DiagramTrafo t n m a -> ShowS
$cshow :: forall (t :: DiagramType) (n :: N') (m :: N') a.
(ShowPoint a, Show a) =>
DiagramTrafo t n m a -> String
show :: DiagramTrafo t n m a -> String
$cshowList :: forall (t :: DiagramType) (n :: N') (m :: N') a.
(ShowPoint a, Show a) =>
[DiagramTrafo t n m a] -> ShowS
showList :: [DiagramTrafo t n m a] -> ShowS
Show,DiagramTrafo t n m a -> DiagramTrafo t n m a -> Bool
(DiagramTrafo t n m a -> DiagramTrafo t n m a -> Bool)
-> (DiagramTrafo t n m a -> DiagramTrafo t n m a -> Bool)
-> Eq (DiagramTrafo t n m a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (t :: DiagramType) (n :: N') (m :: N') a.
(EqPoint a, Eq a) =>
DiagramTrafo t n m a -> DiagramTrafo t n m a -> Bool
$c== :: forall (t :: DiagramType) (n :: N') (m :: N') a.
(EqPoint a, Eq a) =>
DiagramTrafo t n m a -> DiagramTrafo t n m a -> Bool
== :: DiagramTrafo t n m a -> DiagramTrafo t n m a -> Bool
$c/= :: forall (t :: DiagramType) (n :: N') (m :: N') a.
(EqPoint a, Eq a) =>
DiagramTrafo t n m a -> DiagramTrafo t n m a -> Bool
/= :: DiagramTrafo t n m a -> DiagramTrafo t n m a -> Bool
Eq)

--------------------------------------------------------------------------------

-- dgts -


-- | the underlying list of factors.

dgts :: DiagramTrafo t n m a -> FinList n a
dgts :: forall (t :: DiagramType) (n :: N') (m :: N') a.
DiagramTrafo t n m a -> FinList n a
dgts (DiagramTrafo Diagram t n m a
_ Diagram t n m a
_ FinList n a
fs) = FinList n a
fs

--------------------------------------------------------------------------------

-- dgtTypeRefl -


-- | reflexivity of @__t__@ for a diagram trafo.

dgtTypeRefl :: DiagramTrafo t n m a -> Dual (Dual t) :~: t
dgtTypeRefl :: forall (t :: DiagramType) (n :: N') (m :: N') a.
DiagramTrafo t n m a -> Dual (Dual t) :~: t
dgtTypeRefl (DiagramTrafo Diagram t n m a
a Diagram t n m a
_ FinList n a
_) = Diagram t n m a -> Dual (Dual t) :~: t
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> Dual (Dual t) :~: t
dgTypeRefl Diagram t n m a
a

--------------------------------------------------------------------------------

-- dgtMapCov -


-- | covariant mapping of 'DiagramTrafo'.

dgtMapCov :: HomMultiplicativeDisjunctive h
  => Variant2 Covariant h a b -> DiagramTrafo t n m a -> DiagramTrafo t n m b
dgtMapCov :: forall (h :: * -> * -> *) a b (t :: DiagramType) (n :: N')
       (m :: N').
HomMultiplicativeDisjunctive h =>
Variant2 'Covariant h a b
-> DiagramTrafo t n m a -> DiagramTrafo t n m b
dgtMapCov Variant2 'Covariant h a b
h (DiagramTrafo Diagram t n m a
a Diagram t n m a
b FinList n a
ts)
  = Diagram t n m b
-> Diagram t n m b -> FinList n b -> DiagramTrafo t n m b
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a
-> Diagram t n m a -> FinList n a -> DiagramTrafo t n m a
DiagramTrafo (Variant2 'Covariant h a b -> Diagram t n m a -> Diagram t n m b
forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedDisjunctive h =>
Variant2 'Covariant h x y -> Diagram t n m x -> Diagram t n m y
dgMapCov Variant2 'Covariant h a b
h Diagram t n m a
a) (Variant2 'Covariant h a b -> Diagram t n m a -> Diagram t n m b
forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedDisjunctive h =>
Variant2 'Covariant h x y -> Diagram t n m x -> Diagram t n m y
dgMapCov Variant2 'Covariant h a b
h Diagram t n m a
b) ((a -> b) -> FinList n a -> FinList n b
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (Variant2 'Covariant h a b -> a -> b
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap Variant2 'Covariant h a b
h) FinList n a
ts)

--------------------------------------------------------------------------------

-- dgtMapCnt -


-- | contravariant mapping of 'DiagramTrafo'.

dgtMapCnt :: HomMultiplicativeDisjunctive h
  => Variant2 Contravariant h a b -> DiagramTrafo t n m a -> DiagramTrafo (Dual t) n m b
dgtMapCnt :: forall (h :: * -> * -> *) a b (t :: DiagramType) (n :: N')
       (m :: N').
HomMultiplicativeDisjunctive h =>
Variant2 'Contravariant h a b
-> DiagramTrafo t n m a -> DiagramTrafo (Dual t) n m b
dgtMapCnt Variant2 'Contravariant h a b
h (DiagramTrafo Diagram t n m a
a Diagram t n m a
b FinList n a
ts)
  = Diagram (Dual t) n m b
-> Diagram (Dual t) n m b
-> FinList n b
-> DiagramTrafo (Dual t) n m b
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a
-> Diagram t n m a -> FinList n a -> DiagramTrafo t n m a
DiagramTrafo (Variant2 'Contravariant h a b
-> Diagram t n m a -> Dual1 (Diagram t n m) b
forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedDisjunctive h =>
Variant2 'Contravariant h x y
-> Diagram t n m x -> Dual1 (Diagram t n m) y
dgMapCnt Variant2 'Contravariant h a b
h Diagram t n m a
b) (Variant2 'Contravariant h a b
-> Diagram t n m a -> Dual1 (Diagram t n m) b
forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedDisjunctive h =>
Variant2 'Contravariant h x y
-> Diagram t n m x -> Dual1 (Diagram t n m) y
dgMapCnt Variant2 'Contravariant h a b
h Diagram t n m a
a) ((a -> b) -> FinList n a -> FinList n b
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (Variant2 'Contravariant h a b -> a -> b
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap Variant2 'Contravariant h a b
h) FinList n a
ts)

--------------------------------------------------------------------------------

-- Duality -


type instance Dual1 (DiagramTrafo t n m) = DiagramTrafo (Dual t) n m

instance (Show a, ShowPoint a) => ShowDual1 (DiagramTrafo t n m) a
instance (Eq a, EqPoint a) => EqDual1 (DiagramTrafo t n m) a

--------------------------------------------------------------------------------

-- dgtMapS -


-- | mapping of 'DiagramTrafo'

dgtMapS :: (HomMultiplicativeDisjunctive h, t ~ Dual (Dual t))
  => h x y -> SDualBi (DiagramTrafo t n m) x -> SDualBi (DiagramTrafo t n m) y
dgtMapS :: forall (h :: * -> * -> *) (t :: DiagramType) x y (n :: N')
       (m :: N').
(HomMultiplicativeDisjunctive h, t ~ Dual (Dual t)) =>
h x y
-> SDualBi (DiagramTrafo t n m) x -> SDualBi (DiagramTrafo t n m) y
dgtMapS = (Variant2 'Covariant h x y
 -> DiagramTrafo t n m x -> DiagramTrafo t n m y)
-> (Variant2 'Covariant h x y
    -> Dual1 (DiagramTrafo t n m) x -> Dual1 (DiagramTrafo t n m) y)
-> (Variant2 'Contravariant h x y
    -> DiagramTrafo t n m x -> Dual1 (DiagramTrafo t n m) y)
-> (Variant2 'Contravariant h x y
    -> Dual1 (DiagramTrafo t n m) x -> DiagramTrafo t n m y)
-> h x y
-> SDualBi (DiagramTrafo t n m) x
-> SDualBi (DiagramTrafo t n m) y
forall (h :: * -> * -> *) x y (d :: * -> *).
Disjunctive2 h =>
(Variant2 'Covariant h x y -> d x -> d y)
-> (Variant2 'Covariant h x y -> Dual1 d x -> Dual1 d y)
-> (Variant2 'Contravariant h x y -> d x -> Dual1 d y)
-> (Variant2 'Contravariant h x y -> Dual1 d x -> d y)
-> h x y
-> SDualBi d x
-> SDualBi d y
vmapBi Variant2 'Covariant h x y
-> DiagramTrafo t n m x -> DiagramTrafo t n m y
forall (h :: * -> * -> *) a b (t :: DiagramType) (n :: N')
       (m :: N').
HomMultiplicativeDisjunctive h =>
Variant2 'Covariant h a b
-> DiagramTrafo t n m a -> DiagramTrafo t n m b
dgtMapCov Variant2 'Covariant h x y
-> Dual1 (DiagramTrafo t n m) x -> Dual1 (DiagramTrafo t n m) y
Variant2 'Covariant h x y
-> DiagramTrafo (Dual t) n m x -> DiagramTrafo (Dual t) n m y
forall (h :: * -> * -> *) a b (t :: DiagramType) (n :: N')
       (m :: N').
HomMultiplicativeDisjunctive h =>
Variant2 'Covariant h a b
-> DiagramTrafo t n m a -> DiagramTrafo t n m b
dgtMapCov Variant2 'Contravariant h x y
-> DiagramTrafo t n m x -> Dual1 (DiagramTrafo t n m) y
Variant2 'Contravariant h x y
-> DiagramTrafo t n m x -> DiagramTrafo (Dual t) n m y
forall (h :: * -> * -> *) a b (t :: DiagramType) (n :: N')
       (m :: N').
HomMultiplicativeDisjunctive h =>
Variant2 'Contravariant h a b
-> DiagramTrafo t n m a -> DiagramTrafo (Dual t) n m b
dgtMapCnt Variant2 'Contravariant h x y
-> Dual1 (DiagramTrafo t n m) x -> DiagramTrafo t n m y
Variant2 'Contravariant h x y
-> DiagramTrafo (Dual t) n m x
-> DiagramTrafo (Dual (Dual t)) n m y
forall (h :: * -> * -> *) a b (t :: DiagramType) (n :: N')
       (m :: N').
HomMultiplicativeDisjunctive h =>
Variant2 'Contravariant h a b
-> DiagramTrafo t n m a -> DiagramTrafo (Dual t) n m b
dgtMapCnt

--------------------------------------------------------------------------------

-- FunctorialG -


instance (HomMultiplicativeDisjunctive h, t ~ Dual (Dual t))
  => ApplicativeG (SDualBi (DiagramTrafo t n m)) h (->) where
  amapG :: forall x y.
h x y
-> SDualBi (DiagramTrafo t n m) x -> SDualBi (DiagramTrafo t n m) y
amapG = h x y
-> SDualBi (DiagramTrafo t n m) x -> SDualBi (DiagramTrafo t n m) y
forall (h :: * -> * -> *) (t :: DiagramType) x y (n :: N')
       (m :: N').
(HomMultiplicativeDisjunctive h, t ~ Dual (Dual t)) =>
h x y
-> SDualBi (DiagramTrafo t n m) x -> SDualBi (DiagramTrafo t n m) y
dgtMapS

instance
  ( HomMultiplicativeDisjunctive h
  , FunctorialOriented h
  , t ~ Dual (Dual t)
  )
  => FunctorialG (SDualBi (DiagramTrafo t n m)) h (->)

--------------------------------------------------------------------------------

-- DiagramTrafo - 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 n1 (Point a)
ps) (Point a
q:|FinList n1 (Point a)
qs) (a
t:|FinList n1 a
ts)
  = [Statement] -> Statement
And [ a -> Statement
forall a. Validable a => a -> Statement
valid a
t
        , Label
l2 Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
t Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
p Point a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:> Point a
q)
            Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(i,p,q,t)"String -> String -> Parameter
:=(N, Point a, Point a, a) -> String
forall a. Show a => a -> String
show (N
i,Point a
p,Point a
q,a
t)]
        , N
-> FinList n1 (Point a)
-> FinList n1 (Point a)
-> FinList n1 a
-> Statement
forall a (n :: N').
Oriented a =>
N
-> FinList n (Point a)
-> FinList n (Point a)
-> FinList n a
-> Statement
vldTrDiscrete (N -> N
forall a. Enum a => a -> a
succ N
i) FinList n1 (Point a)
ps FinList n1 (Point a)
FinList n1 (Point a)
qs FinList n1 a
FinList n1 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 n1 a
ts)
  = [Statement] -> Statement
And [ a -> Statement
forall a. Validable a => a -> Statement
valid a
t
        , Label
l2 Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
t Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
pPoint a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:>Point a
q)
            Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(i,p,q,t)"String -> String -> Parameter
:=(N, Point a, Point a, a) -> String
forall a. Show a => a -> String
show (N
i,Point a
p,Point a
q,a
t)]
        , N -> FinList m a -> FinList m a -> FinList (m + 1) a -> Statement
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
ta -> FinList n1 a -> FinList (n1 + 1) a
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList n1 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 n1 a
Nil) = Statement
SValid
  vldChTo N
i (a
f:|FinList n1 a
fs) (a
g:|FinList n1 a
gs) (a
r:|a
s:|FinList n1 a
ts)
    = [Statement] -> Statement
And [ a -> Statement
forall a. Validable a => a -> Statement
valid a
s
          , Label
l2 Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
s Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
p' Point a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:> Point a
q')
              Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(i,p',q',s)"String -> String -> Parameter
:=(N, Point a, Point a, a) -> String
forall a. Show a => a -> String
show (N
i,Point a
p',Point a
q',a
s)]
          , Label
l3 Label -> Statement -> Statement
:<=>: (a
ra -> a -> a
forall c. Multiplicative c => c -> c -> c
*a
f a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
ga -> a -> a
forall c. Multiplicative c => c -> c -> c
*a
s)
              Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(i,r,f,g,s)"String -> String -> Parameter
:=(N, a, a, a, a) -> String
forall a. Show a => a -> String
show (N
i,a
r,a
f,a
g,a
s)]
          , N
-> FinList n1 a -> FinList n1 a -> FinList (n1 + 1) a -> Statement
forall a (m :: N').
Multiplicative a =>
N -> FinList m a -> FinList m a -> FinList (m + 1) a -> Statement
vldChTo (N -> N
forall a. Enum a => a -> a
succ N
i) FinList n1 a
fs FinList n1 a
FinList n1 a
gs (a
sa -> FinList n1 a -> FinList (n1 + 1) a
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList n1 a
ts)
          ] where
    p' :: Point a
p' = a -> Point a
forall q. Oriented q => q -> Point q
start a
f
    q' :: Point a
q' = a -> Point a
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 n1 a
Nil)
  = [Statement] -> Statement
And [ (a, a) -> Statement
forall a. Validable a => a -> Statement
valid (a
r,a
s)
        , Label
l2 Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
r Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
p Point a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:> Point a
q)
            Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(p,q,r)"String -> String -> Parameter
:=(Point a, Point a, a) -> String
forall a. Show a => a -> String
show (Point a
p,Point a
q,a
r)]
        , Label
l2 Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
s Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
p' Point a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:> Point a
q')
            Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(p',q',s)"String -> String -> Parameter
:=(Point a, Point a, a) -> String
forall a. Show a => a -> String
show (Point a
p',Point a
q',a
s)]
        , N -> a -> a -> FinList m a -> FinList m a -> Statement
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 n1 a
fs) (a
g:|FinList n1 a
gs)
    = [Statement] -> Statement
And [ (a, a) -> Statement
forall a. Validable a => a -> Statement
valid (a
f,a
g)
          , Label
l3 Label -> Statement -> Statement
:<=>: (a
sa -> a -> a
forall c. Multiplicative c => c -> c -> c
*a
f a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
ga -> a -> a
forall c. Multiplicative c => c -> c -> c
*a
r)
              Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(j,r,s,f,g)"String -> String -> Parameter
:=(N, a, a, a, a) -> String
forall a. Show a => a -> String
show (N
j,a
r,a
s,a
f,a
g)]
          , N -> a -> a -> FinList n1 a -> FinList n1 a -> Statement
forall a (m :: N').
Multiplicative a =>
N -> a -> a -> FinList m a -> FinList m a -> Statement
vld (N -> N
forall a. Enum a => a -> a
succ N
j) a
r a
s FinList n1 a
fs FinList n1 a
FinList n1 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 n1 a
ts)
  = [Statement] -> Statement
And [ a -> Statement
forall a. Validable a => a -> Statement
valid a
t
        , Label
l2 Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
t Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
p Point a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:> Point a
q)
            Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(j,t,p,q)"String -> String -> Parameter
:= (N, a, Point a, Point a) -> String
forall a. Show a => a -> String
show (N
0::N,a
t,Point a
p,Point a
q)]
        , N -> a -> FinList m a -> FinList m a -> FinList m a -> Statement
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 m a
FinList n1 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 n1 a
fs) (a
g:|FinList n1 a
gs) (a
t:|FinList n1 a
ts) 
    = [Statement] -> Statement
And [ (a, a, a) -> Statement
forall a. Validable a => a -> Statement
valid (a
f,a
g,a
t)
          , Label
l2 Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
t Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== a -> Point a
forall q. Oriented q => q -> Point q
start a
f Point a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:> a -> Point a
forall q. Oriented q => q -> Point q
start a
g)
              Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(j,f,g,t)"String -> String -> Parameter
:=(N, a, a, a) -> String
forall a. Show a => a -> String
show (N
j,a
f,a
g,a
t)]
          , Label
l3 Label -> Statement -> Statement
:<=>: (a
t0a -> a -> a
forall c. Multiplicative c => c -> c -> c
*a
f a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
ga -> a -> a
forall c. Multiplicative c => c -> c -> c
*a
t)
              Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(j,t0,f,g,t)"String -> String -> Parameter
:= (N, a, a, a, a) -> String
forall a. Show a => a -> String
show (N
j,a
t0,a
f,a
g,a
t)]
          , N -> a -> FinList n1 a -> FinList n1 a -> FinList n1 a -> Statement
forall a (m :: N').
Multiplicative a =>
N -> a -> FinList m a -> FinList m a -> FinList m a -> Statement
vld (N -> N
forall a. Enum a => a -> a
succ N
j) a
t0 FinList n1 a
fs FinList n1 a
FinList n1 a
gs FinList n1 a
FinList n1 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 Quiver n m -> Quiver n m -> Bool
forall a. Eq a => a -> a -> Bool
== Diagram t n m a -> Quiver n m
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented 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
:=(Diagram t n m a, Diagram t n m a) -> String
forall a. Show a => a -> String
show (Diagram t n m a
a,Diagram t n m a
b)]
        , N
-> FinList n (Point a)
-> FinList n (Point a)
-> FinList n a
-> Statement
forall a (n :: N').
Multiplicative a =>
N
-> FinList n (Point a)
-> FinList n (Point a)
-> FinList n a
-> Statement
vldTr N
0 (Diagram t n m a -> FinList n (Point 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
a) (Diagram t n m a -> FinList n (Point 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
        , N
-> FinList m (Orientation N)
-> FinList m a
-> FinList m a
-> Array N a
-> Statement
forall a (m :: N').
Multiplicative a =>
N
-> FinList m (Orientation N)
-> FinList m a
-> FinList m a
-> Array N a
-> Statement
vldCm N
0 (Quiver n m -> FinList m (Orientation N)
forall (n :: N') (m :: N'). Quiver n m -> FinList m (Orientation N)
qvOrientations Quiver n m
qa) (Diagram t n m a -> FinList m a
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> FinList m a
dgArrows Diagram t n m a
a) (Diagram t n m a -> FinList m a
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> FinList m a
dgArrows Diagram t n m a
b) (FinList n a -> Array N a
forall (n :: N') a. FinList n a -> Array N a
toArray FinList n a
ts) 
        ] where

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

vldTr :: Multiplicative a => DiagramTrafo t n m a -> Statement
vldTr :: forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
DiagramTrafo t n m a -> Statement
vldTr t :: DiagramTrafo t n m a
t@(DiagramTrafo 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)   -> N
-> FinList n (Point a)
-> FinList n (Point a)
-> FinList n a
-> Statement
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) -> N
-> (Point a, FinList m a)
-> (Point a, FinList m a)
-> FinList (m + 1) a
-> Statement
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
FinList (m + 1) a
ts
  (DiagramParallelLR Point a
p Point a
p' FinList m a
fs,DiagramParallelLR Point a
q Point a
q' FinList m a
gs)
    -> (Point a, Point a, FinList m a)
-> (Point a, Point a, FinList m a) -> FinList N2 a -> Statement
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
FinList N2 a
ts
  (DiagramSink Point a
p FinList m a
fs,DiagramSink Point a
q FinList m a
gs)       -> (Point a, FinList m a)
-> (Point a, FinList m a) -> FinList (m + 1) a -> Statement
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
FinList (m + 1) a
ts
  (DiagramGeneral FinList n (Point a)
_ FinList m (a, Orientation N)
_,DiagramGeneral FinList n (Point a)
_ FinList m (a, Orientation N)
_)   -> Diagram t n m a -> Diagram t n m a -> FinList n a -> Statement
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)
_                                         -> case DiagramTrafo t n m a -> Dual (Dual t) :~: t
forall (t :: DiagramType) (n :: N') (m :: N') a.
DiagramTrafo t n m a -> Dual (Dual t) :~: t
dgtTypeRefl DiagramTrafo t n m a
t of
    Dual (Dual t) :~: t
Refl -> DiagramTrafo (Dual t) n m (Op a) -> Statement
forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
DiagramTrafo t n m a -> Statement
vldTr Dual1 (DiagramTrafo t n m) (Op a)
DiagramTrafo (Dual t) n m (Op a)
t' where
      Contravariant2 IsoO Mlt Op a (Op a)
i   = Variant2 'Contravariant (Inv2 (HomDisjEmpty Mlt Op)) a (Op a)
forall x.
Multiplicative x =>
Variant2 'Contravariant (Inv2 (HomDisjEmpty Mlt Op)) x (Op x)
toDualOpMlt
      SDualBi (Left1 Dual1 (DiagramTrafo t n m) (Op a)
t') = IsoO Mlt Op a (Op a)
-> SDualBi (DiagramTrafo t n m) a
-> SDualBi (DiagramTrafo t n m) (Op a)
forall x y.
Inv2 (HomDisjEmpty Mlt Op) x y
-> SDualBi (DiagramTrafo t n m) x -> SDualBi (DiagramTrafo t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG IsoO Mlt Op a (Op a)
i (Either1 (Dual1 (DiagramTrafo t n m)) (DiagramTrafo t n m) a
-> SDualBi (DiagramTrafo t n m) a
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (DiagramTrafo t n m a
-> Either1 (DiagramTrafo (Dual t) n m) (DiagramTrafo t n m) a
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 DiagramTrafo t n m a
t))


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

--------------------------------------------------------------------------------

-- Multiplicative -


type instance Point (DiagramTrafo t n m a) = Diagram t n m a

instance (Show a, ShowPoint a) => ShowPoint (DiagramTrafo t n m a)
instance (Eq a, EqPoint a) => EqPoint (DiagramTrafo t n m a)
instance Oriented a => ValidablePoint (DiagramTrafo t n m a)
instance (Typeable a, Typeable t, Typeable n, Typeable m) => TypeablePoint (DiagramTrafo t n m a)

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

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

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

type instance Root (DiagramTrafo t n m a) = Orientation (Diagram t n m a)

instance (Show a, ShowPoint a) => ShowRoot (DiagramTrafo t n m a)
instance (Eq a, EqPoint a) => EqRoot (DiagramTrafo t n m a)
instance Oriented a => ValidableRoot (DiagramTrafo t n m a)
instance (Typeable a, Typeable t, Typeable n, Typeable m) => TypeableRoot (DiagramTrafo t n m a)

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

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

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

  ntimes :: N -> DiagramTrafo t n m a -> DiagramTrafo t n m a
ntimes N
n (DiagramTrafo 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 -> FinList n a -> DiagramTrafo t n m a
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a
-> Diagram t n m a -> FinList n a -> DiagramTrafo t n m a
DiagramTrafo Diagram t n m a
a Diagram t n m a
b ((a -> a) -> FinList n a -> FinList n a
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (N -> a -> a
forall a. Additive a => N -> a -> a
ntimes N
n) FinList n a
ts)

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

instance ( Distributive a, Abelian a
         , Typeable t, Typeable n, Typeable m
         )
  => Abelian (DiagramTrafo t n m a) where
  negate :: DiagramTrafo t n m a -> DiagramTrafo t n m a
negate (DiagramTrafo 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 -> FinList n a -> DiagramTrafo t n m a
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a
-> Diagram t n m a -> FinList n a -> DiagramTrafo t n m a
DiagramTrafo Diagram t n m a
a Diagram t n m a
b ((a -> a) -> FinList n a -> FinList n a
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 a -> a
forall a. Abelian a => a -> a
negate FinList n a
ts)
  ztimes :: Z -> DiagramTrafo t n m a -> DiagramTrafo t n m a
ztimes Z
z (DiagramTrafo 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 -> FinList n a -> DiagramTrafo t n m a
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a
-> Diagram t n m a -> FinList n a -> DiagramTrafo t n m a
DiagramTrafo Diagram t n m a
a Diagram t n m a
b ((a -> a) -> FinList n a -> FinList n a
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (Z -> a -> a
forall a. Abelian a => Z -> a -> a
ztimes Z
z) FinList n a
ts)

instance ( Algebraic a
         , Typeable t, Typeable n, Typeable m
         )
  => Vectorial (DiagramTrafo t n m a) where
  type Scalar (DiagramTrafo t n m a) = Scalar a
  Scalar (DiagramTrafo t n m a)
s ! :: Scalar (DiagramTrafo t n m a)
-> DiagramTrafo t n m a -> DiagramTrafo t n m a
! (DiagramTrafo 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 -> FinList n a -> DiagramTrafo t n m a
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a
-> Diagram t n m a -> FinList n a -> DiagramTrafo t n m a
DiagramTrafo Diagram t n m a
a Diagram t n m a
b ((a -> a) -> FinList n a -> FinList n a
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (Scalar a
Scalar (DiagramTrafo t n m a)
s Scalar a -> a -> a
forall v. Vectorial v => Scalar v -> v -> v
V.!) FinList n a
ts)

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