{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Entity.Diagram.Definition

-- Description : definition of diagrams on oriented structures

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- definition of 'Diagram's on 'Oriented' structures.

module OAlg.Entity.Diagram.Definition
  (
    -- * Diagram

    Diagram(..), DiagramType(..), rt'
  , dgType, dgTypeRefl, dgPoints, dgCenter, dgArrows, dgMap
  , dgQuiver

     -- ** Chain

  , chnToStart, chnFromStart

    -- ** Parallel

  , dgPrlAdjZero
  , dgPrlTail, dgPrlDiffHead
  , dgPrlDiffTail

    -- * Duality

  , dgToOp, dgFromOp, DiagramDuality(..)
  , coDiagram, coDiagramInv, dgFromOpOp
  
    -- * SomeDiagram

  , SomeDiagram(..), sdgMap, sdgFromOpOp
  , coSomeDiagram, coSomeDiagramInv
  
    -- * X

  , XDiagram(..)
  , xDiagram
  , xSomeDiagram, dstSomeDiagram
  , xSomeDiagramOrnt

  )
  where

import Control.Monad 

import Data.Typeable
import Data.Array as A hiding (range)

import OAlg.Prelude hiding (T)

import OAlg.Structure.Oriented
import OAlg.Structure.Additive
import OAlg.Structure.Distributive

import OAlg.Hom.Oriented
import OAlg.Hom.Definition

import OAlg.Entity.Natural as N hiding ((++))
import OAlg.Entity.FinList as S

import OAlg.Entity.Diagram.Quiver

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

-- DiagramType -


-- | the types of a 'Diagram'.

data DiagramType
  = Empty
  | Discrete
  | Chain Site
  | Parallel Direction
  | Star Site
  | General
  deriving (Int -> DiagramType -> ShowS
[DiagramType] -> ShowS
DiagramType -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DiagramType] -> ShowS
$cshowList :: [DiagramType] -> ShowS
show :: DiagramType -> String
$cshow :: DiagramType -> String
showsPrec :: Int -> DiagramType -> ShowS
$cshowsPrec :: Int -> DiagramType -> ShowS
Show,DiagramType -> DiagramType -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DiagramType -> DiagramType -> Bool
$c/= :: DiagramType -> DiagramType -> Bool
== :: DiagramType -> DiagramType -> Bool
$c== :: DiagramType -> DiagramType -> Bool
Eq,Eq DiagramType
DiagramType -> DiagramType -> Bool
DiagramType -> DiagramType -> Ordering
DiagramType -> DiagramType -> DiagramType
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: DiagramType -> DiagramType -> DiagramType
$cmin :: DiagramType -> DiagramType -> DiagramType
max :: DiagramType -> DiagramType -> DiagramType
$cmax :: DiagramType -> DiagramType -> DiagramType
>= :: DiagramType -> DiagramType -> Bool
$c>= :: DiagramType -> DiagramType -> Bool
> :: DiagramType -> DiagramType -> Bool
$c> :: DiagramType -> DiagramType -> Bool
<= :: DiagramType -> DiagramType -> Bool
$c<= :: DiagramType -> DiagramType -> Bool
< :: DiagramType -> DiagramType -> Bool
$c< :: DiagramType -> DiagramType -> Bool
compare :: DiagramType -> DiagramType -> Ordering
$ccompare :: DiagramType -> DiagramType -> Ordering
Ord)

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

-- DiagramType - Dual -


type instance Dual 'Empty                   = 'Empty
type instance Dual 'Discrete                = 'Discrete
type instance Dual ('Chain 'From)           = 'Chain 'To
type instance Dual ('Chain 'To)             = 'Chain 'From 
type instance Dual ('Parallel 'LeftToRight) = 'Parallel 'RightToLeft
type instance Dual ('Parallel 'RightToLeft) = 'Parallel 'LeftToRight
type instance Dual ('Star 'To)              = 'Star 'From
type instance Dual ('Star 'From)            = 'Star 'To
type instance Dual 'General                 = 'General


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

-- rt'


-- | 'Dual' is well defined on diagram types.

rt' :: forall (t :: DiagramType) . Dual (Dual t) :~: t -> Dual (Dual (Dual t)) :~: Dual t
rt' :: forall (t :: DiagramType).
(Dual (Dual t) :~: t) -> Dual (Dual (Dual t)) :~: Dual t
rt' Dual (Dual t) :~: t
Refl = forall {k} (a :: k). a :~: a
Refl

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

-- Diagram -


-- | diagram for a 'Oriented' structure __@a@__ of type __@t@__ having __@n@__ points

--   and __@m@__ arrows.

--

--   __Properties__ Let @d@ be in @'Diagram' __t__ __n__ __m__ __a__@ for a 'Oriented'

--   structure __@a@__, then holds:

--

--   (1) If @d@ matches @'DiagramChainTo' e as@ then holds: @e '==' 'end' a0@ and

--   @'start' ai '==' 'end' ai+1@ for all @i = 0..m-2@

--   where @a0':|'..':|'ai':|'..':|'am-1':|''Nil' = as@.

--

--   (2) If @d@ matches @'DiagramChainFrom' s as@ then holds: @s '==' 'start' a0@ and

--   @'end' ai '==' 'start' ai+1@ for all @i = 0..m-2@

--   where @a0':|'..':|'ai':|'..':|'am-1':|''Nil' = as@.

--

--   (3) If @d@ matches @'DiagramParallelLR' l r as@ then holds:

--   @'orientation' a '==' l':>'r@ for all @a@ in @as@.

--

--   (4) If @d@ matches @'DiagramParallelRL' l r as@ then holds:

--   @'orientation' a '==' r':>'l@ for all @a@ in @as@.

--

--   (5) If @d@ matches @'DiagramSink' e as@ then holds: @e '==' 'end' a@

--   for all @a@ in @as@.

--

--   (6) If @d@ matches @'DiagramSource' s as@ then holds: @s '==' 'start' a@

--   for all @a@ in @as@.

--

--   (7) If @d@ matches @'DiagramGeneral' ps aijs@ then holds@ @pi '==' 'start' aij@ and

--   @pj '==' 'end' aij@ for all @aij@ in @aijs@ and @ps = p0..pn-1@.

data Diagram t n m a where
  DiagramEmpty      :: Diagram 'Empty N0 N0 a
  DiagramDiscrete   :: FinList n (Point a) -> Diagram Discrete n N0 a  
  DiagramChainTo    :: Point a -> FinList m a -> Diagram (Chain To) (m+1) m a  
  DiagramChainFrom  :: Point a -> FinList m a -> Diagram (Chain From) (m+1) m a  
  DiagramParallelLR :: Point a -> Point a -> FinList m a
    -> Diagram (Parallel LeftToRight) N2 m a
  DiagramParallelRL :: Point a -> Point a -> FinList m a
    -> Diagram (Parallel RightToLeft) N2 m a
  DiagramSink       :: Point a -> FinList m a -> Diagram (Star To) (m+1) m a
  DiagramSource     :: Point a -> FinList m a -> Diagram (Star From) (m+1) m a  
  DiagramGeneral    :: FinList n (Point a) -> FinList m (a,Orientation N)
    -> Diagram General n m a

deriving instance Oriented a => Show (Diagram t n m a)
deriving instance Oriented a => Eq (Diagram t n m a)

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

-- dgPoints -


-- | the points of a diagram.

dgPoints :: Oriented a => Diagram t n m a -> FinList n (Point a)
dgPoints :: 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
d = case Diagram t n m a
d of
  Diagram t n m a
DiagramEmpty            -> forall a. FinList 'N0 a
Nil
  DiagramDiscrete FinList n (Point a)
ps      -> FinList n (Point a)
ps
  DiagramChainTo Point a
e FinList m a
as     -> Point a
eforall a (t :: N'). a -> FinList t a -> FinList (t + 1) a
:|forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall q. Oriented q => q -> Point q
start FinList m a
as
  DiagramChainFrom Point a
s FinList m a
as   -> Point a
sforall a (t :: N'). a -> FinList t a -> FinList (t + 1) a
:|forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall q. Oriented q => q -> Point q
end FinList m a
as
  DiagramParallelLR Point a
p Point a
q FinList m a
_ -> Point a
p forall a (t :: N'). a -> FinList t a -> FinList (t + 1) a
:| Point a
q forall a (t :: N'). a -> FinList t a -> FinList (t + 1) a
:| forall a. FinList 'N0 a
Nil
  DiagramParallelRL Point a
p Point a
q FinList m a
_ -> Point a
p forall a (t :: N'). a -> FinList t a -> FinList (t + 1) a
:| Point a
q forall a (t :: N'). a -> FinList t a -> FinList (t + 1) a
:| forall a. FinList 'N0 a
Nil
  DiagramSink Point a
p FinList m a
as        -> Point a
p forall a (t :: N'). a -> FinList t a -> FinList (t + 1) a
:| forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall q. Oriented q => q -> Point q
start FinList m a
as
  DiagramSource Point a
p FinList m a
as      -> Point a
p forall a (t :: N'). a -> FinList t a -> FinList (t + 1) a
:| forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall q. Oriented q => q -> Point q
end FinList m a
as
  DiagramGeneral FinList n (Point a)
ps FinList m (a, Orientation N)
_     -> FinList n (Point a)
ps

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

-- dgArrows -


-- | the arrows of a diagram.

dgArrows :: Diagram t n m a -> FinList m a
dgArrows :: forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> FinList m a
dgArrows Diagram t n m a
d = case Diagram t n m a
d of
  Diagram t n m a
DiagramEmpty             -> forall a. FinList 'N0 a
Nil
  DiagramDiscrete FinList n (Point a)
_        -> forall a. FinList 'N0 a
Nil
  DiagramChainTo Point a
_ FinList m a
as      -> FinList m a
as
  DiagramChainFrom Point a
_ FinList m a
as    -> FinList m a
as
  DiagramParallelLR Point a
_ Point a
_ FinList m a
as -> FinList m a
as
  DiagramParallelRL Point a
_ Point a
_ FinList m a
as -> FinList m a
as
  DiagramSink Point a
_ FinList m a
as         -> FinList m a
as
  DiagramSource Point a
_ FinList m a
as       -> FinList m a
as
  DiagramGeneral FinList n (Point a)
_  FinList m (a, Orientation N)
as     -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst FinList m (a, Orientation N)
as

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

-- dgCenter -


-- | the center point of a 'Star'-diagram.

dgCenter :: Diagram (Star t) n m c -> Point c
dgCenter :: forall (t :: Site) (n :: N') (m :: N') c.
Diagram ('Star t) n m c -> Point c
dgCenter (DiagramSink Point c
c FinList m c
_)   = Point c
c
dgCenter (DiagramSource Point c
c FinList m c
_) = Point c
c

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

-- dgMap -


-- | mapping of a diagram via a homomorphism on 'Oriented' structures.

dgMap :: Hom Ort h => h a b -> Diagram t n m a -> Diagram t n m b
dgMap :: forall (h :: * -> * -> *) a b (t :: DiagramType) (n :: N')
       (m :: N').
Hom Ort h =>
h a b -> Diagram t n m a -> Diagram t n m b
dgMap h a b
h Diagram t n m a
d = case Diagram t n m a
d of
  Diagram t n m a
DiagramEmpty             -> forall a. Diagram 'Empty 'N0 'N0 a
DiagramEmpty
  DiagramDiscrete FinList n (Point a)
ps       -> forall (n :: N') a.
FinList n (Point a) -> Diagram 'Discrete n 'N0 a
DiagramDiscrete (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Point a -> Point b
fp FinList n (Point a)
ps)
  DiagramChainTo Point a
e FinList m a
as      -> forall a (m :: N').
Point a -> FinList m a -> Diagram ('Chain 'To) (m + 1) m a
DiagramChainTo (Point a -> Point b
fp Point a
e) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f FinList m a
as)
  DiagramChainFrom Point a
s FinList m a
as    -> forall a (m :: N').
Point a -> FinList m a -> Diagram ('Chain 'From) (m + 1) m a
DiagramChainFrom  (Point a -> Point b
fp Point a
s) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f FinList m a
as)
  DiagramParallelLR Point a
l Point a
r FinList m a
as -> forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) ('S N1) m a
DiagramParallelLR (Point a -> Point b
fp Point a
l) (Point a -> Point b
fp Point a
r) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f FinList m a
as)
  DiagramParallelRL Point a
l Point a
r FinList m a
as -> forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'RightToLeft) ('S N1) m a
DiagramParallelRL (Point a -> Point b
fp Point a
l) (Point a -> Point b
fp Point a
r) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f FinList m a
as)
  DiagramSink Point a
e FinList m a
as         -> forall a (m :: N').
Point a -> FinList m a -> Diagram ('Star 'To) (m + 1) m a
DiagramSink (Point a -> Point b
fp Point a
e) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f FinList m a
as)
  DiagramSource Point a
s FinList m a
as       -> forall a (m :: N').
Point a -> FinList m a -> Diagram ('Star 'From) (m + 1) m a
DiagramSource (Point a -> Point b
fp Point a
s) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f FinList m a
as)
  DiagramGeneral FinList n (Point a)
ps FinList m (a, Orientation N)
aijs   -> forall (n :: N') a (m :: N').
FinList n (Point a)
-> FinList m (a, Orientation N) -> Diagram 'General n m a
DiagramGeneral (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Point a -> Point b
fp FinList n (Point a)
ps)
                                (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(a
a,Orientation N
o) -> (a -> b
f a
a,Orientation N
o)) FinList m (a, Orientation N)
aijs)
  where fp :: Point a -> Point b
fp = forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap h a b
h
        f :: a -> b
f  = forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h a b
h

instance HomOriented h => Applicative1 h (Diagram t n m) where
  amap1 :: forall a b. h a b -> Diagram t n m a -> Diagram t n m b
amap1 = forall (h :: * -> * -> *) a b (t :: DiagramType) (n :: N')
       (m :: N').
Hom Ort h =>
h a b -> Diagram t n m a -> Diagram t n m b
dgMap

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

-- Diagram - Dual -


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

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

-- coDiagram -


-- | the co diagram with its inverse 'coDiagramInv'.

--

--   __Property__ Let @d@ be in @'Diagram' __t__ __n__ __m__ __a__@ for a 'Oriented'

--  structure __@a@__ then holds: @'dgPoints' ('coDiagram' d) '==' 'dgPoints' d@.

coDiagram :: Diagram t n m a -> Dual (Diagram t n m a)
coDiagram :: 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
d = case Diagram t n m a
d of
  Diagram t n m a
DiagramEmpty             -> forall a. Diagram 'Empty 'N0 'N0 a
DiagramEmpty
  DiagramDiscrete FinList n (Point a)
ps       -> forall (n :: N') a.
FinList n (Point a) -> Diagram 'Discrete n 'N0 a
DiagramDiscrete FinList n (Point a)
ps
  DiagramChainTo Point a
e FinList m a
as      -> forall a (m :: N').
Point a -> FinList m a -> Diagram ('Chain 'From) (m + 1) m a
DiagramChainFrom Point a
e (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. x -> Op x
Op FinList m a
as)
  DiagramChainFrom Point a
s FinList m a
as    -> forall a (m :: N').
Point a -> FinList m a -> Diagram ('Chain 'To) (m + 1) m a
DiagramChainTo Point a
s (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. x -> Op x
Op FinList m a
as)
  DiagramParallelLR Point a
l Point a
r FinList m a
as -> forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'RightToLeft) ('S N1) m a
DiagramParallelRL Point a
l Point a
r (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. x -> Op x
Op FinList m a
as)
  DiagramParallelRL Point a
l Point a
r FinList m a
as -> forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) ('S N1) m a
DiagramParallelLR Point a
l Point a
r (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. x -> Op x
Op FinList m a
as)
  DiagramSink Point a
e FinList m a
as         -> forall a (m :: N').
Point a -> FinList m a -> Diagram ('Star 'From) (m + 1) m a
DiagramSource Point a
e (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. x -> Op x
Op FinList m a
as)
  DiagramSource Point a
s FinList m a
as       -> forall a (m :: N').
Point a -> FinList m a -> Diagram ('Star 'To) (m + 1) m a
DiagramSink Point a
s (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. x -> Op x
Op FinList m a
as)
  DiagramGeneral FinList n (Point a)
ps FinList m (a, Orientation N)
aijs   -> forall (n :: N') a (m :: N').
FinList n (Point a)
-> FinList m (a, Orientation N) -> Diagram 'General n m a
DiagramGeneral FinList n (Point a)
ps (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(a
a,Orientation N
o) -> (forall x. x -> Op x
Op a
a,forall p. Orientation p -> Orientation p
opposite Orientation N
o)) FinList m (a, Orientation N)
aijs)

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

-- dgFromOpOp -


-- | from @'Op' '.' 'Op'@.

dgFromOpOp :: Oriented a => Diagram t n m (Op (Op a)) -> Diagram t n m a
dgFromOpOp :: forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m (Op (Op a)) -> Diagram t n m a
dgFromOpOp = forall (h :: * -> * -> *) a b (t :: DiagramType) (n :: N')
       (m :: N').
Hom Ort h =>
h a b -> Diagram t n m a -> Diagram t n m b
dgMap forall a. Oriented a => IsoOp Ort (Op (Op a)) a
isoFromOpOpOrt 

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

-- coDiagramInv -


-- | from the dual diagram, with inverse of 'coDiagram'.

coDiagramInv :: Oriented a => Dual (Dual t) :~: t
  -> Dual (Diagram t n m a) -> Diagram t n m a
coDiagramInv :: forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> Dual (Diagram t n m a) -> Diagram t n m a
coDiagramInv Dual (Dual t) :~: t
Refl = forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m (Op (Op a)) -> Diagram t n m a
dgFromOpOp forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> Dual (Diagram t n m a)
coDiagram

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

-- DiagramDuality -


-- | 'Op'-duality between diagrams.

data DiagramDuality f g a where
  DiagramDuality :: Oriented a
    => f a :~: Diagram t n m a
    -> g (Op a) :~: Dual (Diagram t n m a)
    -> Dual (Dual t) :~: t
    -> DiagramDuality f g a

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

-- dgToOp -


-- | to @__g__ ('Op' __a__)@.

dgToOp :: DiagramDuality f g a -> f a -> g (Op a)
dgToOp :: forall (f :: * -> *) (g :: * -> *) a.
DiagramDuality f g a -> f a -> g (Op a)
dgToOp (DiagramDuality f a :~: Diagram t n m a
Refl g (Op a) :~: Dual (Diagram t n m a)
Refl Dual (Dual t) :~: t
_) = forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> Dual (Diagram t n m a)
coDiagram

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

-- dgFromOp -


-- | from @__g__ ('Op' __a__)@.

dgFromOp :: DiagramDuality f g a -> g (Op a) -> f a 
dgFromOp :: forall (f :: * -> *) (g :: * -> *) a.
DiagramDuality f g a -> g (Op a) -> f a
dgFromOp (DiagramDuality f a :~: Diagram t n m a
Refl g (Op a) :~: Dual (Diagram t n m a)
Refl Dual (Dual t) :~: t
rt) = forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> Dual (Diagram t n m a) -> Diagram t n m a
coDiagramInv Dual (Dual t) :~: t
rt

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

-- Diagram - Validable -


instance Oriented a => Validable (Diagram t n m a) where
  valid :: Diagram t n m a -> Statement
valid Diagram t n m a
d = case Diagram t n m a
d of
    Diagram t n m a
DiagramEmpty -> Statement
SValid
    DiagramDiscrete FinList n (Point a)
ps -> forall a. Validable a => a -> Statement
valid FinList n (Point a)
ps
    DiagramChainTo Point a
e FinList m a
as -> forall a. Validable a => a -> Statement
valid Point a
e forall b. Boolean b => b -> b -> b
&& forall a (m :: N').
Oriented a =>
N -> Point a -> FinList m a -> Statement
vld N
0 Point a
e FinList m a
as where
      vld :: Oriented a => N -> Point a -> FinList m a -> Statement
      vld :: forall a (m :: N').
Oriented a =>
N -> Point a -> FinList m a -> Statement
vld N
_ Point a
_ FinList m a
Nil     = Statement
SValid
      vld N
i Point a
e (a
a:|FinList n a
as) = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
a
                            , Label
lC Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Point q
end a
a forall a. Eq a => a -> a -> Bool
== Point a
e)Bool -> Message -> Statement
:?>N -> Message
prm N
i
                            , forall a (m :: N').
Oriented a =>
N -> Point a -> FinList m a -> Statement
vld (forall a. Enum a => a -> a
succ N
i) (forall q. Oriented q => q -> Point q
start a
a) FinList n a
as
                            ]
                        
    DiagramParallelLR Point a
l Point a
r FinList m a
as -> forall a. Validable a => a -> Statement
valid Orientation (Point a)
o forall b. Boolean b => b -> b -> b
&& forall a (m :: N').
Oriented a =>
N -> Orientation (Point a) -> FinList m a -> Statement
vld N
0 Orientation (Point a)
o FinList m a
as where 
      o :: Orientation (Point a)
o = Point a
lforall p. p -> p -> Orientation p
:>Point a
r
      vld :: Oriented a => N -> Orientation (Point a) -> FinList m a -> Statement
      vld :: forall a (m :: N').
Oriented a =>
N -> Orientation (Point a) -> FinList m a -> Statement
vld N
_ Orientation (Point a)
_ FinList m a
Nil = Statement
SValid
      vld N
i Orientation (Point a)
o (a
a:|FinList n a
as)
        = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
a
              , Label
lO Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
a forall a. Eq a => a -> a -> Bool
== Orientation (Point a)
o)Bool -> Message -> Statement
:?>N -> Message
prm N
i
              , forall a (m :: N').
Oriented a =>
N -> Orientation (Point a) -> FinList m a -> Statement
vld (forall a. Enum a => a -> a
succ N
i) Orientation (Point a)
o FinList n a
as
              ]

    DiagramSink Point a
e FinList m a
as -> forall a. Validable a => a -> Statement
valid Point a
e forall b. Boolean b => b -> b -> b
&& forall a (m :: N').
Oriented a =>
N -> Point a -> FinList m a -> Statement
vld N
0 Point a
e FinList m a
as where
      vld :: Oriented a => N -> Point a -> FinList m a -> Statement
      vld :: forall a (m :: N').
Oriented a =>
N -> Point a -> FinList m a -> Statement
vld N
_ Point a
_ FinList m a
Nil     = Statement
SValid
      vld N
i Point a
e (a
a:|FinList n a
as)
        = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
a
              , Label
lE Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Point q
end a
a forall a. Eq a => a -> a -> Bool
== Point a
e)Bool -> Message -> Statement
:?>N -> Message
prm N
i
              , forall a (m :: N').
Oriented a =>
N -> Point a -> FinList m a -> Statement
vld (forall a. Enum a => a -> a
succ N
i) Point a
e FinList n a
as
              ]

    DiagramGeneral FinList n (Point a)
ps FinList m (a, Orientation N)
aijs -> [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid FinList n (Point a)
ps
                                  , forall a (m :: N').
Oriented a =>
N -> Array N (Point a) -> FinList m (a, Orientation N) -> Statement
vld N
0 (forall (n :: N') a. FinList n a -> Array N a
toArray FinList n (Point a)
ps) FinList m (a, Orientation N)
aijs
                                  ] where
      vld :: Oriented a
        => N -> Array N (Point a) -> FinList m (a,Orientation N) -> Statement
      vld :: forall a (m :: N').
Oriented a =>
N -> Array N (Point a) -> FinList m (a, Orientation N) -> Statement
vld N
_ Array N (Point a)
_ FinList m (a, Orientation N)
Nil = Statement
SValid
      vld N
l Array N (Point a)
ps ((a
a,N
i:>N
j):|FinList n (a, Orientation N)
aijs)
        = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
a
              , Label
lB Label -> Statement -> Statement
:<=>: (forall a. Ix a => (a, a) -> a -> Bool
inRange (forall i e. Array i e -> (i, i)
bounds Array N (Point a)
ps) N
i) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params[String
"l"String -> String -> Parameter
:=forall a. Show a => a -> String
show N
l,String
"i"String -> String -> Parameter
:=forall a. Show a => a -> String
show N
i]
              , Label
lB Label -> Statement -> Statement
:<=>: (forall a. Ix a => (a, a) -> a -> Bool
inRange (forall i e. Array i e -> (i, i)
bounds Array N (Point a)
ps) N
j) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params[String
"l"String -> String -> Parameter
:=forall a. Show a => a -> String
show N
l,String
"j"String -> String -> Parameter
:=forall a. Show a => a -> String
show N
j]
              , Label
lO Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
a forall a. Eq a => a -> a -> Bool
== (Array N (Point a)
psforall i e. Ix i => Array i e -> i -> e
!N
i)forall p. p -> p -> Orientation p
:>(Array N (Point a)
psforall i e. Ix i => Array i e -> i -> e
!N
j))
                         Bool -> Message -> Statement
:?>[Parameter] -> Message
Params[String
"l"String -> String -> Parameter
:=forall a. Show a => a -> String
show N
l,String
"(i,j)"String -> String -> Parameter
:=forall a. Show a => a -> String
show (N
i,N
j)]
              , forall a (m :: N').
Oriented a =>
N -> Array N (Point a) -> FinList m (a, Orientation N) -> Statement
vld (forall a. Enum a => a -> a
succ N
l) Array N (Point a)
ps FinList n (a, Orientation N)
aijs
              ]

    Diagram t n m a
_ -> forall a. Validable a => a -> Statement
valid forall (h :: * -> * -> *) a b. Applicative h => h a b -> 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
d

    where prm :: N -> Message
          prm :: N -> Message
prm N
i = [Parameter] -> Message
Params[String
"i"String -> String -> Parameter
:=forall a. Show a => a -> String
show N
i]
          lC :: Label
lC = String -> Label
Label String
"chain"
          lE :: Label
lE = String -> Label
Label String
"end"
          lO :: Label
lO = String -> Label
Label String
"orientation"
          lB :: Label
lB = String -> Label
Label String
"bound"
    

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

-- Diagram - Entity -


instance (Oriented a, Typeable t, Typeable n, Typeable m) => Entity (Diagram t n m a)

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

-- Diagram - Oriented -


instance (Oriented a, Typeable d, Typeable n, Typeable m)
  => Oriented (Diagram (Parallel d) n m a) where
  type Point (Diagram (Parallel d) n m a) = Point a
  orientation :: Diagram ('Parallel d) n m a
-> Orientation (Point (Diagram ('Parallel d) n m a))
orientation (DiagramParallelLR Point a
l Point a
r FinList m a
_) = Point a
lforall p. p -> p -> Orientation p
:>Point a
r
  orientation (DiagramParallelRL Point a
l Point a
r FinList m a
_) = Point a
rforall p. p -> p -> Orientation p
:>Point a
l
  
--------------------------------------------------------------------------------

-- dgQuiver -


-- | the underlying quiver of a diagram.

dgQuiver :: Diagram t n m a -> Quiver n m
dgQuiver :: forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> Quiver n m
dgQuiver Diagram t n m a
DiagramEmpty = forall (n :: N') (m :: N').
Any n -> FinList m (Orientation N) -> Quiver n m
Quiver W 'N0
W0 forall a. FinList 'N0 a
Nil
dgQuiver (DiagramDiscrete FinList n (Point a)
ps) = forall (n :: N') (m :: N').
Any n -> FinList m (Orientation N) -> Quiver n m
Quiver (forall (n :: N') a. FinList n a -> W n
toW FinList n (Point a)
ps) forall a. FinList 'N0 a
Nil
dgQuiver (DiagramChainTo Point a
_ FinList m a
as) = forall (n :: N') (m :: N').
Any n -> FinList m (Orientation N) -> Quiver n m
Quiver (forall (t :: N'). W t -> W (t + 1)
SW (forall (n :: N') a. FinList n a -> W n
toW FinList m (Orientation N)
os)) FinList m (Orientation N)
os where
  os :: FinList m (Orientation N)
os = forall (m :: N') x. N -> FinList m x -> FinList m (Orientation N)
chnTo N
0 FinList m a
as
  chnTo :: N -> FinList m x -> FinList m (Orientation N)
  chnTo :: forall (m :: N') x. N -> FinList m x -> FinList m (Orientation N)
chnTo N
_ FinList m x
Nil     = forall a. FinList 'N0 a
Nil
  chnTo N
j (x
_:|FinList n x
os) = (N
j' forall p. p -> p -> Orientation p
:> N
j)forall a (t :: N'). a -> FinList t a -> FinList (t + 1) a
:|forall (m :: N') x. N -> FinList m x -> FinList m (Orientation N)
chnTo N
j' FinList n x
os where j' :: N
j' = forall a. Enum a => a -> a
succ N
j
dgQuiver (DiagramParallelLR Point a
_ Point a
_ FinList m a
as) = forall (n :: N') (m :: N').
Any n -> FinList m (Orientation N) -> Quiver n m
Quiver forall (n :: N'). Attestable n => W n
attest (forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall b a. b -> a -> b
const (N
0forall p. p -> p -> Orientation p
:>N
1)) FinList m a
as)
dgQuiver (DiagramSink Point a
_ FinList m a
as) = forall (n :: N') (m :: N').
Any n -> FinList m (Orientation N) -> Quiver n m
Quiver (forall (t :: N'). W t -> W (t + 1)
SW (forall (n :: N') a. FinList n a -> W n
toW FinList m (Orientation N)
os)) FinList m (Orientation N)
os where
  os :: FinList m (Orientation N)
os = forall (m :: N') x. N -> FinList m x -> FinList m (Orientation N)
snk N
1 FinList m a
as
  snk :: N -> FinList m x -> FinList m (Orientation N)
  snk :: forall (m :: N') x. N -> FinList m x -> FinList m (Orientation N)
snk N
_ FinList m x
Nil     = forall a. FinList 'N0 a
Nil
  snk N
j (x
_:|FinList n x
os) = (N
jforall p. p -> p -> Orientation p
:>N
0)forall a (t :: N'). a -> FinList t a -> FinList (t + 1) a
:|forall (m :: N') x. N -> FinList m x -> FinList m (Orientation N)
snk (forall a. Enum a => a -> a
succ N
j) FinList n x
os
dgQuiver (DiagramGeneral FinList n (Point a)
ps FinList m (a, Orientation N)
os) = forall (n :: N') (m :: N').
Any n -> FinList m (Orientation N) -> Quiver n m
Quiver (forall (n :: N') a. FinList n a -> W n
toW FinList n (Point a)
ps) (forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall a b. (a, b) -> b
snd FinList m (a, Orientation N)
os)
dgQuiver Diagram t n m a
d = forall (n :: N') (m :: N'). Dual (Quiver n m) -> Quiver n m
coQuiverInv forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> Quiver n m
dgQuiver (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
d)

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

-- chnToStart -


-- | the last point of the chain.

chnToStart :: Oriented a => Diagram (Chain To) n m a -> Point a
chnToStart :: forall a (n :: N') (m :: N').
Oriented a =>
Diagram ('Chain 'To) n m a -> Point a
chnToStart (DiagramChainTo Point a
e FinList m a
as) = case FinList m a
as of
    FinList m a
Nil   -> Point a
e
    a
a:|FinList n a
as -> forall a (m :: N'). Oriented a => Point a -> FinList m a -> Point a
st (forall q. Oriented q => q -> Point q
start a
a) FinList n a
as where
      st :: Oriented a => Point a -> FinList m a -> Point a
      st :: forall a (m :: N'). Oriented a => Point a -> FinList m a -> Point a
st Point a
s FinList m a
Nil      = Point a
s
      st Point a
_ (a
a:|FinList n a
as)  = forall a (m :: N'). Oriented a => Point a -> FinList m a -> Point a
st (forall q. Oriented q => q -> Point q
start a
a) FinList n a
as

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

-- chnFromStart -


-- | the first point of the chain.

chnFromStart :: Diagram (Chain From) n m a -> Point a
chnFromStart :: forall (n :: N') (m :: N') a.
Diagram ('Chain 'From) n m a -> Point a
chnFromStart (DiagramChainFrom Point a
s FinList m a
_) = Point a
s

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

-- chnFromEnd -


chnFromEnd :: Oriented a => Diagram (Chain From) n m a -> Point a
chnFromEnd :: forall a (n :: N') (m :: N').
Oriented a =>
Diagram ('Chain 'From) n m a -> Point a
chnFromEnd d :: Diagram ('Chain 'From) n m a
d@(DiagramChainFrom Point a
_ FinList m a
_) = forall a (n :: N') (m :: N').
Oriented a =>
Diagram ('Chain 'To) n m a -> Point a
chnToStart forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> Dual (Diagram t n m a)
coDiagram Diagram ('Chain 'From) n m a
d

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

-- Diagram (Chain t) - Oriented -


instance (Oriented a, Typeable t, Typeable n, Typeable m) => Oriented (Diagram (Chain t) n m a) where
  type Point (Diagram (Chain t) n m a) = Point a
  start :: Diagram ('Chain t) n m a -> Point (Diagram ('Chain t) n m a)
start (DiagramChainFrom Point a
s FinList m a
_) = Point a
s
  start d :: Diagram ('Chain t) n m a
d@(DiagramChainTo Point a
_ FinList m a
_) = forall a (n :: N') (m :: N').
Oriented a =>
Diagram ('Chain 'To) n m a -> Point a
chnToStart Diagram ('Chain t) n m a
d

  end :: Diagram ('Chain t) n m a -> Point (Diagram ('Chain t) n m a)
end d :: Diagram ('Chain t) n m a
d@(DiagramChainFrom Point a
_ FinList m a
_) = forall a (n :: N') (m :: N').
Oriented a =>
Diagram ('Chain 'From) n m a -> Point a
chnFromEnd Diagram ('Chain t) n m a
d
  end (DiagramChainTo Point a
e FinList m a
_)     = Point a
e

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

-- dgPrlAdjZero -


-- | adjoins a 'zero' arrow as the first parallel arrow.

dgPrlAdjZero :: Distributive a
  => Diagram (Parallel LeftToRight) n m a -> Diagram (Parallel LeftToRight) n (m+1) a
dgPrlAdjZero :: forall a (n :: N') (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) n m a
-> Diagram ('Parallel 'LeftToRight) n (m + 1) a
dgPrlAdjZero (DiagramParallelLR Point a
l Point a
r FinList m a
as) = forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) ('S N1) m a
DiagramParallelLR Point a
l Point a
r (forall a. Additive a => Root a -> a
zero (Point a
lforall p. p -> p -> Orientation p
:>Point a
r)forall a (t :: N'). a -> FinList t a -> FinList (t + 1) a
:|FinList m a
as)

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

-- dgPrlTail -


-- | the _/tail/__ of a parallel diagram.

dgPrlTail :: Diagram (Parallel d) n (m+1) a -> Diagram (Parallel d) n m a
dgPrlTail :: forall (d :: Direction) (n :: N') (m :: N') a.
Diagram ('Parallel d) n (m + 1) a -> Diagram ('Parallel d) n m a
dgPrlTail (DiagramParallelLR Point a
l Point a
r FinList (m + 1) a
as) = forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) ('S N1) m a
DiagramParallelLR Point a
l Point a
r (forall (n :: N') a. FinList (n + 1) a -> FinList n a
tail FinList (m + 1) a
as)
dgPrlTail (DiagramParallelRL Point a
l Point a
r FinList (m + 1) a
as) = forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'RightToLeft) ('S N1) m a
DiagramParallelRL Point a
l Point a
r (forall (n :: N') a. FinList (n + 1) a -> FinList n a
tail FinList (m + 1) a
as)

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

-- dgPrlDiffTail -


-- | subtracts the first arrow to all the others an drops it.

dgPrlDiffTail :: Abelian a
  => Diagram (Parallel d) n (m+1) a -> Diagram (Parallel d) n m a
dgPrlDiffTail :: forall a (d :: Direction) (n :: N') (m :: N').
Abelian a =>
Diagram ('Parallel d) n (m + 1) a -> Diagram ('Parallel d) n m a
dgPrlDiffTail = forall (d :: Direction) (n :: N') (m :: N') a.
Diagram ('Parallel d) n (m + 1) a -> Diagram ('Parallel d) n m a
dgPrlTail forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall a (d :: Direction) (n :: N') (m :: N').
Abelian a =>
Diagram ('Parallel d) n (m + 1) a
-> Diagram ('Parallel d) n (m + 1) a
dgPrlDiffHead

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

-- dgPrlDiffHead -


-- | subtracts to every arrow of the parallel diagram the first arrow.

dgPrlDiffHead :: Abelian a
  => Diagram (Parallel d) n (m+1) a -> Diagram (Parallel d) n (m+1) a
dgPrlDiffHead :: forall a (d :: Direction) (n :: N') (m :: N').
Abelian a =>
Diagram ('Parallel d) n (m + 1) a
-> Diagram ('Parallel d) n (m + 1) a
dgPrlDiffHead Diagram ('Parallel d) n (m + 1) a
d = case Diagram ('Parallel d) n (m + 1) a
d of
  DiagramParallelLR Point a
l Point a
r FinList (m + 1) a
as -> forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) ('S N1) m a
DiagramParallelLR Point a
l Point a
r (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall {a}. Abelian a => a -> a -> a
diff forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (n :: N') a. FinList (n + 1) a -> a
head FinList (m + 1) a
as) FinList (m + 1) a
as)
  DiagramParallelRL Point a
l Point a
r FinList (m + 1) a
as -> forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'RightToLeft) ('S N1) m a
DiagramParallelRL Point a
l Point a
r (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall {a}. Abelian a => a -> a -> a
diff forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (n :: N') a. FinList (n + 1) a -> a
head FinList (m + 1) a
as) FinList (m + 1) a
as)
  where diff :: a -> a -> a
diff a
a a
x = a
x forall {a}. Abelian a => a -> a -> a
- a
a

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

-- dgType -


-- | the type of a diagram.

dgType :: Diagram t n m a -> DiagramType
dgType :: forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> DiagramType
dgType Diagram t n m a
d = case Diagram t n m a
d of
  Diagram t n m a
DiagramEmpty            -> DiagramType
Empty
  DiagramDiscrete FinList n (Point a)
_       -> DiagramType
Discrete
  DiagramChainTo Point a
_ FinList m a
_      -> Site -> DiagramType
Chain Site
To
  DiagramChainFrom Point a
_ FinList m a
_    -> Site -> DiagramType
Chain Site
From
  DiagramParallelLR Point a
_ Point a
_ FinList m a
_ -> Direction -> DiagramType
Parallel Direction
LeftToRight
  DiagramParallelRL Point a
_ Point a
_ FinList m a
_ -> Direction -> DiagramType
Parallel Direction
RightToLeft
  DiagramSink Point a
_ FinList m a
_         -> Site -> DiagramType
Star Site
To
  DiagramSource Point a
_ FinList m a
_       -> Site -> DiagramType
Star Site
From
  DiagramGeneral FinList n (Point a)
_ FinList m (a, Orientation N)
_      -> DiagramType
General

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

-- dgTypeRefl -


-- | reflexivity of the underlying diagram type.

dgTypeRefl :: Diagram t n m a -> Dual (Dual t) :~: t
dgTypeRefl :: forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> Dual (Dual t) :~: t
dgTypeRefl Diagram t n m a
d = case Diagram t n m a
d of
  Diagram t n m a
DiagramEmpty            -> forall {k} (a :: k). a :~: a
Refl
  DiagramDiscrete FinList n (Point a)
_       -> forall {k} (a :: k). a :~: a
Refl
  DiagramChainTo Point a
_ FinList m a
_      -> forall {k} (a :: k). a :~: a
Refl
  DiagramChainFrom Point a
_ FinList m a
_    -> forall {k} (a :: k). a :~: a
Refl
  DiagramParallelLR Point a
_ Point a
_ FinList m a
_ -> forall {k} (a :: k). a :~: a
Refl
  DiagramParallelRL Point a
_ Point a
_ FinList m a
_ -> forall {k} (a :: k). a :~: a
Refl
  DiagramSink Point a
_ FinList m a
_         -> forall {k} (a :: k). a :~: a
Refl
  DiagramSource Point a
_ FinList m a
_       -> forall {k} (a :: k). a :~: a
Refl
  DiagramGeneral FinList n (Point a)
_ FinList m (a, Orientation N)
_      -> forall {k} (a :: k). a :~: a
Refl

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

-- XDiagram -


-- | generator for random variables of diagrams.

data XDiagram t n m a where
  XDiagramEmpty      :: XDiagram 'Empty N0 N0 a
  XDiagramDiscrete   :: Any n -> X (Point a) -> XDiagram Discrete n N0 a
  XDiagramChainTo    :: Any m -> XOrtSite To a -> XDiagram (Chain To) (m+1) m a  
  XDiagramChainFrom  :: Any m -> XOrtSite From a -> XDiagram (Chain From) (m+1) m a
  XDiagramParallelLR :: Any m -> XOrtOrientation a
    -> XDiagram (Parallel LeftToRight) N2 m a
  XDiagramParallelRL :: Any m -> XOrtOrientation a
    -> XDiagram (Parallel RightToLeft) N2 m a
  XDiagramSink       :: Any m -> XOrtSite To a -> XDiagram (Star To) (m+1) m a
  XDiagramSource     :: Any m -> XOrtSite From a -> XDiagram (Star From) (m+1) m a

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

-- XDiagram - Dualisable -


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

-- | the co-'XDiagram'.

coXDiagram :: XDiagram t n m a -> Dual (XDiagram t n m a)
coXDiagram :: forall (t :: DiagramType) (n :: N') (m :: N') a.
XDiagram t n m a -> Dual (XDiagram t n m a)
coXDiagram XDiagram t n m a
xd = case XDiagram t n m a
xd of
  XDiagram t n m a
XDiagramEmpty           -> forall a. XDiagram 'Empty 'N0 'N0 a
XDiagramEmpty
  XDiagramDiscrete Any n
n X (Point a)
xp   -> forall (n :: N') a.
Any n -> X (Point a) -> XDiagram 'Discrete n 'N0 a
XDiagramDiscrete Any n
n X (Point a)
xp
  XDiagramChainTo Any m
m XOrtSite 'To a
xe    -> forall (m :: N') a.
Any m -> XOrtSite 'From a -> XDiagram ('Chain 'From) (m + 1) m a
XDiagramChainFrom Any m
m (forall (s :: Site) q. XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite XOrtSite 'To a
xe)
  XDiagramChainFrom Any m
m XOrtSite 'From a
xs  -> forall (m :: N') a.
Any m -> XOrtSite 'To a -> XDiagram ('Chain 'To) (m + 1) m a
XDiagramChainTo Any m
m (forall (s :: Site) q. XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite XOrtSite 'From a
xs)
  XDiagramParallelLR Any m
m XOrtOrientation a
xo -> forall (m :: N') a.
Any m
-> XOrtOrientation a
-> XDiagram ('Parallel 'RightToLeft) ('S N1) m a
XDiagramParallelRL Any m
m (forall q. XOrtOrientation q -> Dual (XOrtOrientation q)
coXOrtOrientation XOrtOrientation a
xo)
  XDiagramParallelRL Any m
m XOrtOrientation a
xo -> forall (m :: N') a.
Any m
-> XOrtOrientation a
-> XDiagram ('Parallel 'LeftToRight) ('S N1) m a
XDiagramParallelLR Any m
m (forall q. XOrtOrientation q -> Dual (XOrtOrientation q)
coXOrtOrientation XOrtOrientation a
xo)
  XDiagramSink Any m
m XOrtSite 'To a
xe       -> forall (m :: N') a.
Any m -> XOrtSite 'From a -> XDiagram ('Star 'From) (m + 1) m a
XDiagramSource Any m
m (forall (s :: Site) q. XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite XOrtSite 'To a
xe)
  XDiagramSource Any m
m XOrtSite 'From a
xs     -> forall (m :: N') a.
Any m -> XOrtSite 'To a -> XDiagram ('Star 'To) (m + 1) m a
XDiagramSink Any m
m (forall (s :: Site) q. XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite XOrtSite 'From a
xs)

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

-- xDiagram -


xDiscrete :: p a -> Any n -> X (Point a) -> X (Diagram Discrete n N0 a)
xDiscrete :: forall (p :: * -> *) a (n :: N').
p a -> Any n -> X (Point a) -> X (Diagram 'Discrete n 'N0 a)
xDiscrete p a
_ Any n
_ X (Point a)
XEmpty    = forall x. X x
XEmpty
xDiscrete p a
_ Any n
W0 X (Point a)
_        = forall (m :: * -> *) a. Monad m => a -> m a
return (forall (n :: N') a.
FinList n (Point a) -> Diagram 'Discrete n 'N0 a
DiagramDiscrete forall a. FinList 'N0 a
Nil)
xDiscrete p a
pa (SW W n
n') X (Point a)
xp = do
  DiagramDiscrete FinList n (Point a)
ps <- forall (p :: * -> *) a (n :: N').
p a -> Any n -> X (Point a) -> X (Diagram 'Discrete n 'N0 a)
xDiscrete p a
pa W n
n' X (Point a)
xp
  Point a
p <- X (Point a)
xp
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall (n :: N') a.
FinList n (Point a) -> Diagram 'Discrete n 'N0 a
DiagramDiscrete (Point a
pforall a (t :: N'). a -> FinList t a -> FinList (t + 1) a
:|FinList n (Point a)
ps))

xChain :: Oriented a => Any m -> XOrtSite To a -> X (Diagram (Chain To) (m+1) m a)
xChain :: forall a (m :: N').
Oriented a =>
Any m -> XOrtSite 'To a -> X (Diagram ('Chain 'To) (m + 1) m a)
xChain Any m
m xe :: XOrtSite 'To a
xe@(XEnd X (Point a)
xp Point a -> X a
_) = do
  Point a
e      <- X (Point a)
xp
  (Point a
_,FinList m a
as) <- forall a (m :: N').
Oriented a =>
Any m -> XOrtSite 'To a -> Point a -> X (Point a, FinList m a)
xchn Any m
m XOrtSite 'To a
xe Point a
e
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a (m :: N').
Point a -> FinList m a -> Diagram ('Chain 'To) (m + 1) m a
DiagramChainTo Point a
e FinList m a
as)
  where xchn :: Oriented a => Any m -> XOrtSite To a -> Point a -> X (Point a, FinList m a)
        xchn :: forall a (m :: N').
Oriented a =>
Any m -> XOrtSite 'To a -> Point a -> X (Point a, FinList m a)
xchn W m
W0 XOrtSite 'To a
_ Point a
e                    = forall (m :: * -> *) a. Monad m => a -> m a
return (Point a
e,forall a. FinList 'N0 a
Nil)
        xchn (SW W n
m') xe :: XOrtSite 'To a
xe@(XEnd X (Point a)
_ Point a -> X a
xea) Point a
e = do
          (Point a
s,FinList n a
as) <- forall a (m :: N').
Oriented a =>
Any m -> XOrtSite 'To a -> Point a -> X (Point a, FinList m a)
xchn W n
m' XOrtSite 'To a
xe Point a
e
          a
a <- Point a -> X a
xea Point a
s
          forall (m :: * -> *) a. Monad m => a -> m a
return (forall q. Oriented q => q -> Point q
start a
a,FinList n a
as forall (n :: N') a. FinList n a -> a -> FinList (n + 1) a
|: a
a)
          
xParallel :: Oriented a
  => Any m -> XOrtOrientation a -> X (Diagram (Parallel LeftToRight) N2 m a)
xParallel :: forall a (m :: N').
Oriented a =>
Any m
-> XOrtOrientation a
-> X (Diagram ('Parallel 'LeftToRight) ('S N1) m a)
xParallel W m
W0 XOrtOrientation a
xo = do
  Point a
l <- forall q. Oriented q => XOrtOrientation q -> X (Point q)
xoPoint XOrtOrientation a
xo
  Point a
r <- forall q. Oriented q => XOrtOrientation q -> X (Point q)
xoPoint XOrtOrientation a
xo
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) ('S N1) m a
DiagramParallelLR Point a
l Point a
r forall a. FinList 'N0 a
Nil)
xParallel (SW W n
m') XOrtOrientation a
xo = do
  DiagramParallelLR Point a
l Point a
r FinList n a
as <- forall a (m :: N').
Oriented a =>
Any m
-> XOrtOrientation a
-> X (Diagram ('Parallel 'LeftToRight) ('S N1) m a)
xParallel W n
m' XOrtOrientation a
xo
  a
a <- forall q. XOrtOrientation q -> Orientation (Point q) -> X q
xoArrow XOrtOrientation a
xo (Point a
lforall p. p -> p -> Orientation p
:>Point a
r)
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) ('S N1) m a
DiagramParallelLR Point a
l Point a
r (a
aforall a (t :: N'). a -> FinList t a -> FinList (t + 1) a
:|FinList n a
as))

xSink :: Oriented a
  => Any m -> XOrtSite To a -> X (Diagram (Star To) (m+1) m a)
xSink :: forall a (m :: N').
Oriented a =>
Any m -> XOrtSite 'To a -> X (Diagram ('Star 'To) (m + 1) m a)
xSink W m
W0 XOrtSite 'To a
xe = do
  Point a
e <- forall (s :: Site) q. XOrtSite s q -> X (Point q)
xosPoint XOrtSite 'To a
xe
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a (m :: N').
Point a -> FinList m a -> Diagram ('Star 'To) (m + 1) m a
DiagramSink Point a
e forall a. FinList 'N0 a
Nil)
xSink (SW W n
m') xe :: XOrtSite 'To a
xe@(XEnd X (Point a)
_ Point a -> X a
xea) = do
  DiagramSink Point a
e FinList n a
as <- forall a (m :: N').
Oriented a =>
Any m -> XOrtSite 'To a -> X (Diagram ('Star 'To) (m + 1) m a)
xSink W n
m' XOrtSite 'To a
xe
  a
a <- Point a -> X a
xea Point a
e
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a (m :: N').
Point a -> FinList m a -> Diagram ('Star 'To) (m + 1) m a
DiagramSink Point a
e (a
aforall a (t :: N'). a -> FinList t a -> FinList (t + 1) a
:|FinList n a
as))


-- | the induced random variables of diagrams.

xDiagram :: Oriented a => Dual (Dual t) :~: t
  -> XDiagram t n m a -> X (Diagram t n m a)
xDiagram :: forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> XDiagram t n m a -> X (Diagram t n m a)
xDiagram Dual (Dual t) :~: t
rt XDiagram t n m a
xd = case XDiagram t n m a
xd of
  XDiagram t n m a
XDiagramEmpty           -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Diagram 'Empty 'N0 'N0 a
DiagramEmpty
  XDiagramDiscrete Any n
n X (Point a)
xp   -> forall (p :: * -> *) a (n :: N').
p a -> Any n -> X (Point a) -> X (Diagram 'Discrete n 'N0 a)
xDiscrete XDiagram t n m a
xd Any n
n X (Point a)
xp
  XDiagramChainTo Any m
m XOrtSite 'To a
xs    -> forall a (m :: N').
Oriented a =>
Any m -> XOrtSite 'To a -> X (Diagram ('Chain 'To) (m + 1) m a)
xChain Any m
m XOrtSite 'To a
xs
  XDiagramParallelLR Any m
m XOrtOrientation a
xo -> forall a (m :: N').
Oriented a =>
Any m
-> XOrtOrientation a
-> X (Diagram ('Parallel 'LeftToRight) ('S N1) m a)
xParallel Any m
m XOrtOrientation a
xo
  XDiagramSink Any m
m XOrtSite 'To a
xe       -> forall a (m :: N').
Oriented a =>
Any m -> XOrtSite 'To a -> X (Diagram ('Star 'To) (m + 1) m a)
xSink Any m
m XOrtSite 'To a
xe
  XDiagram t n m a
_                       ->   forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> Dual (Diagram t n m a) -> Diagram t n m a
coDiagramInv Dual (Dual t) :~: t
rt)
                             forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> XDiagram t n m a -> X (Diagram t n m a)
xDiagram (forall (t :: DiagramType).
(Dual (Dual t) :~: t) -> Dual (Dual (Dual t)) :~: Dual t
rt' Dual (Dual t) :~: t
rt) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (t :: DiagramType) (n :: N') (m :: N') a.
XDiagram t n m a -> Dual (XDiagram t n m a)
coXDiagram XDiagram t n m a
xd

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

-- X (Diagram t n m OS) - Standard -


instance (Oriented a, n ~ N0, m ~ N0) => XStandard (Diagram 'Empty n m a) where
  xStandard :: X (Diagram 'Empty n m a)
xStandard = forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> XDiagram t n m a -> X (Diagram t n m a)
xDiagram forall {k} (a :: k). a :~: a
Refl forall a. XDiagram 'Empty 'N0 'N0 a
XDiagramEmpty


instance (Oriented a, m ~ N0, XStandardPoint a, Attestable n)
  => XStandard (Diagram Discrete n m a) where
  xStandard :: X (Diagram 'Discrete n m a)
xStandard = forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> XDiagram t n m a -> X (Diagram t n m a)
xDiagram forall {k} (a :: k). a :~: a
Refl (forall (n :: N') a.
Any n -> X (Point a) -> XDiagram 'Discrete n 'N0 a
XDiagramDiscrete W n
n forall x. XStandard x => X x
xStandard) where n :: W n
n = forall (n :: N'). Attestable n => W n
attest

instance (Oriented a, XStandardOrtSite To a, Attestable m)
  => XStandard (Diagram (Chain To) (S m) m a) where
  xStandard :: X (Diagram ('Chain 'To) ('S m) m a)
xStandard = forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> XDiagram t n m a -> X (Diagram t n m a)
xDiagram forall {k} (a :: k). a :~: a
Refl (forall (m :: N') a.
Any m -> XOrtSite 'To a -> XDiagram ('Chain 'To) (m + 1) m a
XDiagramChainTo W m
m forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite) where m :: W m
m = forall (n :: N'). Attestable n => W n
attest

instance (Oriented a, XStandardOrtSite From a, Attestable m)
  => XStandard (Diagram (Chain From) (S m) m a) where
  xStandard :: X (Diagram ('Chain 'From) ('S m) m a)
xStandard = forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> XDiagram t n m a -> X (Diagram t n m a)
xDiagram forall {k} (a :: k). a :~: a
Refl (forall (m :: N') a.
Any m -> XOrtSite 'From a -> XDiagram ('Chain 'From) (m + 1) m a
XDiagramChainFrom W m
m forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite) where m :: W m
m = forall (n :: N'). Attestable n => W n
attest

instance (Oriented a, n ~ N2, XStandardOrtOrientation a, Attestable m)
  => XStandard (Diagram (Parallel LeftToRight) n m a) where
  xStandard :: X (Diagram ('Parallel 'LeftToRight) n m a)
xStandard = forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> XDiagram t n m a -> X (Diagram t n m a)
xDiagram forall {k} (a :: k). a :~: a
Refl (forall (m :: N') a.
Any m
-> XOrtOrientation a
-> XDiagram ('Parallel 'LeftToRight) ('S N1) m a
XDiagramParallelLR W m
m forall q. XStandardOrtOrientation q => XOrtOrientation q
xStandardOrtOrientation) where
    m :: W m
m = forall (n :: N'). Attestable n => W n
attest

instance (Oriented a, n ~ N2, XStandardOrtOrientation a, Attestable m)
  => XStandard (Diagram (Parallel RightToLeft) n m a) where
  xStandard :: X (Diagram ('Parallel 'RightToLeft) n m a)
xStandard = forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> XDiagram t n m a -> X (Diagram t n m a)
xDiagram forall {k} (a :: k). a :~: a
Refl (forall (m :: N') a.
Any m
-> XOrtOrientation a
-> XDiagram ('Parallel 'RightToLeft) ('S N1) m a
XDiagramParallelRL W m
m forall q. XStandardOrtOrientation q => XOrtOrientation q
xStandardOrtOrientation) where
    m :: W m
m = forall (n :: N'). Attestable n => W n
attest

instance (Oriented a, XStandardOrtSite To a, Attestable m)
  => XStandard (Diagram (Star To) (S m) m a) where
  xStandard :: X (Diagram ('Star 'To) ('S m) m a)
xStandard = forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> XDiagram t n m a -> X (Diagram t n m a)
xDiagram forall {k} (a :: k). a :~: a
Refl (forall (m :: N') a.
Any m -> XOrtSite 'To a -> XDiagram ('Star 'To) (m + 1) m a
XDiagramSink W m
m forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite) where m :: W m
m = forall (n :: N'). Attestable n => W n
attest

instance (Oriented a, XStandardOrtSite From a, Attestable m)
  => XStandard (Diagram (Star From) (S m) m a) where
  xStandard :: X (Diagram ('Star 'From) ('S m) m a)
xStandard = forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> XDiagram t n m a -> X (Diagram t n m a)
xDiagram forall {k} (a :: k). a :~: a
Refl (forall (m :: N') a.
Any m -> XOrtSite 'From a -> XDiagram ('Star 'From) (m + 1) m a
XDiagramSource W m
m forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite) where m :: W m
m = forall (n :: N'). Attestable n => W n
attest

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

-- SomeDiagram -


-- | some diagram.

data SomeDiagram a where
  SomeDiagram :: Diagram t n m a -> SomeDiagram a

deriving instance Oriented a => Show (SomeDiagram a)

instance Oriented a => Validable (SomeDiagram a) where
  valid :: SomeDiagram a -> Statement
valid (SomeDiagram Diagram t n m a
d) = forall a. Validable a => a -> Statement
valid Diagram t n m a
d

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

-- sdgMap -


-- | mapping of some diagram via a homomorphism on 'Oriented' structures.

sdgMap :: Hom Ort h => h a b -> SomeDiagram a -> SomeDiagram b
sdgMap :: forall (h :: * -> * -> *) a b.
Hom Ort h =>
h a b -> SomeDiagram a -> SomeDiagram b
sdgMap h a b
h (SomeDiagram Diagram t n m a
a) = forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> SomeDiagram a
SomeDiagram (forall (h :: * -> * -> *) a b (t :: DiagramType) (n :: N')
       (m :: N').
Hom Ort h =>
h a b -> Diagram t n m a -> Diagram t n m b
dgMap h a b
h Diagram t n m a
a)

type instance Dual (SomeDiagram a) = SomeDiagram (Op a)

-- | the dual of some diagram, with inverse 'coSomeDiagramInv'.

coSomeDiagram :: SomeDiagram a -> Dual (SomeDiagram a)
coSomeDiagram :: forall a. SomeDiagram a -> Dual (SomeDiagram a)
coSomeDiagram (SomeDiagram Diagram t n m a
a) = forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> SomeDiagram a
SomeDiagram (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)

-- | from @'Op' '.' 'Op'@.

sdgFromOpOp :: Oriented a => SomeDiagram (Op (Op a)) -> SomeDiagram a
sdgFromOpOp :: forall a. Oriented a => SomeDiagram (Op (Op a)) -> SomeDiagram a
sdgFromOpOp (SomeDiagram Diagram t n m (Op (Op a))
a') = forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> SomeDiagram a
SomeDiagram (forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m (Op (Op a)) -> Diagram t n m a
dgFromOpOp Diagram t n m (Op (Op a))
a')

-- | from the dual of some diagram, with inverse 'coSomeDiagram'.

coSomeDiagramInv :: Oriented a => Dual (SomeDiagram a) -> SomeDiagram a
coSomeDiagramInv :: forall a. Oriented a => Dual (SomeDiagram a) -> SomeDiagram a
coSomeDiagramInv = forall a. Oriented a => SomeDiagram (Op (Op a)) -> SomeDiagram a
sdgFromOpOp forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall a. SomeDiagram a -> Dual (SomeDiagram a)
coSomeDiagram

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

-- xSomeDiagram -


-- | the induced random variable of some diagrams.

xSomeDiagram :: Oriented a
  => X SomeNatural
  -> XOrtSite To a -> XOrtSite From a
  -> XOrtOrientation a
  -> X (SomeDiagram a)
xSomeDiagram :: forall a.
Oriented a =>
X SomeNatural
-> XOrtSite 'To a
-> XOrtSite 'From a
-> XOrtOrientation a
-> X (SomeDiagram a)
xSomeDiagram X SomeNatural
xn XOrtSite 'To a
xTo XOrtSite 'From a
xFrom XOrtOrientation a
xO = do
  SomeNatural
n <- X SomeNatural
xn
  case SomeNatural
n of
    SomeNatural W n
W0 -> forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. [a] -> X a
xOneOf (forall a (x :: * -> *). Oriented a => x a -> X (SomeDiagram a)
xe XOrtSite 'To a
xToforall a. a -> [a] -> [a]
:forall a (n :: N').
Oriented a =>
Any n
-> XOrtSite 'To a
-> XOrtSite 'From a
-> XOrtOrientation a
-> [X (SomeDiagram a)]
xsd W 'N0
W0 XOrtSite 'To a
xTo XOrtSite 'From a
xFrom XOrtOrientation a
xO)
    SomeNatural W n
n  -> forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. [a] -> X a
xOneOf (forall a (n :: N').
Oriented a =>
Any n
-> XOrtSite 'To a
-> XOrtSite 'From a
-> XOrtOrientation a
-> [X (SomeDiagram a)]
xsd W n
n XOrtSite 'To a
xTo XOrtSite 'From a
xFrom XOrtOrientation a
xO)
  where

  xe :: Oriented a => x a -> X (SomeDiagram a)
  xe :: forall a (x :: * -> *). Oriented a => x a -> X (SomeDiagram a)
xe x a
_ = forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> XDiagram t n m a -> X (Diagram t n m a)
xDiagram forall {k} (a :: k). a :~: a
Refl (forall a. XDiagram 'Empty 'N0 'N0 a
XDiagramEmpty) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> SomeDiagram a
SomeDiagram

  xsd :: Oriented a
    => Any n
    -> XOrtSite To a -> XOrtSite From a
    -> XOrtOrientation a
    -> [X (SomeDiagram a)]
  xsd :: forall a (n :: N').
Oriented a =>
Any n
-> XOrtSite 'To a
-> XOrtSite 'From a
-> XOrtOrientation a
-> [X (SomeDiagram a)]
xsd Any n
n XOrtSite 'To a
xTo XOrtSite 'From a
xFrom XOrtOrientation a
xO
    = [ forall a (n :: N').
Oriented a =>
Any n -> X (Point a) -> X (SomeDiagram a)
xDiscrete Any n
n X (Point a)
xp
      , forall a (n :: N').
Oriented a =>
Any n -> XOrtSite 'To a -> X (SomeDiagram a)
xChainTo Any n
n XOrtSite 'To a
xTo
      , forall a (n :: N').
Oriented a =>
Any n -> XOrtSite 'From a -> X (SomeDiagram a)
xChainFrom Any n
n XOrtSite 'From a
xFrom
      , forall a (n :: N').
Oriented a =>
Any n -> XOrtOrientation a -> X (SomeDiagram a)
xParallelLR Any n
n XOrtOrientation a
xO
      , forall a (n :: N').
Oriented a =>
Any n -> XOrtOrientation a -> X (SomeDiagram a)
xParallelRL Any n
n XOrtOrientation a
xO
      , forall a (n :: N').
Oriented a =>
Any n -> XOrtSite 'To a -> X (SomeDiagram a)
xSink Any n
n XOrtSite 'To a
xTo
      , forall a (n :: N').
Oriented a =>
Any n -> XOrtSite 'From a -> X (SomeDiagram a)
xSource Any n
n XOrtSite 'From a
xFrom
      ]
    where xp :: X (Point a)
xp = forall q. Oriented q => XOrtOrientation q -> X (Point q)
xoPoint XOrtOrientation a
xO

  xDiscrete :: Oriented a => Any n -> X (Point a) -> X (SomeDiagram a)
  xDiscrete :: forall a (n :: N').
Oriented a =>
Any n -> X (Point a) -> X (SomeDiagram a)
xDiscrete Any n
n X (Point a)
xp
    = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> SomeDiagram a
SomeDiagram forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> XDiagram t n m a -> X (Diagram t n m a)
xDiagram forall {k} (a :: k). a :~: a
Refl (forall (n :: N') a.
Any n -> X (Point a) -> XDiagram 'Discrete n 'N0 a
XDiagramDiscrete Any n
n X (Point a)
xp)

  xChainTo :: Oriented a => Any n -> XOrtSite To a -> X (SomeDiagram a)
  xChainTo :: forall a (n :: N').
Oriented a =>
Any n -> XOrtSite 'To a -> X (SomeDiagram a)
xChainTo Any n
n XOrtSite 'To a
xTo
    = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> SomeDiagram a
SomeDiagram forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> XDiagram t n m a -> X (Diagram t n m a)
xDiagram forall {k} (a :: k). a :~: a
Refl (forall (m :: N') a.
Any m -> XOrtSite 'To a -> XDiagram ('Chain 'To) (m + 1) m a
XDiagramChainTo Any n
n XOrtSite 'To a
xTo)

  xChainFrom :: Oriented a => Any n -> XOrtSite From a -> X (SomeDiagram a)
  xChainFrom :: forall a (n :: N').
Oriented a =>
Any n -> XOrtSite 'From a -> X (SomeDiagram a)
xChainFrom Any n
n XOrtSite 'From a
xFrom = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall a. Oriented a => Dual (SomeDiagram a) -> SomeDiagram a
coSomeDiagramInv forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a (n :: N').
Oriented a =>
Any n -> XOrtSite 'To a -> X (SomeDiagram a)
xChainTo Any n
n (forall (s :: Site) q. XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite XOrtSite 'From a
xFrom)
          
  xParallelLR :: Oriented a => Any n -> XOrtOrientation a -> X (SomeDiagram a)
  xParallelLR :: forall a (n :: N').
Oriented a =>
Any n -> XOrtOrientation a -> X (SomeDiagram a)
xParallelLR Any n
n XOrtOrientation a
xO = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> SomeDiagram a
SomeDiagram forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> XDiagram t n m a -> X (Diagram t n m a)
xDiagram forall {k} (a :: k). a :~: a
Refl (forall (m :: N') a.
Any m
-> XOrtOrientation a
-> XDiagram ('Parallel 'LeftToRight) ('S N1) m a
XDiagramParallelLR Any n
n XOrtOrientation a
xO)
   
  xParallelRL :: Oriented a => Any n -> XOrtOrientation a -> X (SomeDiagram a)
  xParallelRL :: forall a (n :: N').
Oriented a =>
Any n -> XOrtOrientation a -> X (SomeDiagram a)
xParallelRL Any n
n XOrtOrientation a
xO = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall a. Oriented a => Dual (SomeDiagram a) -> SomeDiagram a
coSomeDiagramInv forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a (n :: N').
Oriented a =>
Any n -> XOrtOrientation a -> X (SomeDiagram a)
xParallelLR Any n
n (forall q. XOrtOrientation q -> Dual (XOrtOrientation q)
coXOrtOrientation XOrtOrientation a
xO)

  xSink :: Oriented a => Any n -> XOrtSite To a -> X (SomeDiagram a)
  xSink :: forall a (n :: N').
Oriented a =>
Any n -> XOrtSite 'To a -> X (SomeDiagram a)
xSink Any n
n XOrtSite 'To a
xTo = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> SomeDiagram a
SomeDiagram forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> XDiagram t n m a -> X (Diagram t n m a)
xDiagram forall {k} (a :: k). a :~: a
Refl (forall (m :: N') a.
Any m -> XOrtSite 'To a -> XDiagram ('Star 'To) (m + 1) m a
XDiagramSink Any n
n XOrtSite 'To a
xTo)

  xSource :: Oriented a => Any n -> XOrtSite From a -> X (SomeDiagram a)
  xSource :: forall a (n :: N').
Oriented a =>
Any n -> XOrtSite 'From a -> X (SomeDiagram a)
xSource Any n
n XOrtSite 'From a
xFrom = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall a. Oriented a => Dual (SomeDiagram a) -> SomeDiagram a
coSomeDiagramInv forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a (n :: N').
Oriented a =>
Any n -> XOrtSite 'To a -> X (SomeDiagram a)
xSink Any n
n (forall (s :: Site) q. XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite XOrtSite 'From a
xFrom)

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

-- dstSomeDiagram -


-- | distribution of a random variable of some diagrams.

dstSomeDiagram :: Oriented a => Int -> X (SomeDiagram a) -> IO ()
dstSomeDiagram :: forall a. Oriented a => Int -> X (SomeDiagram a) -> IO ()
dstSomeDiagram Int
n X (SomeDiagram a)
xd = forall x. (x -> [String]) -> Int -> X x -> IO ()
putDstr forall {a}. Oriented a => SomeDiagram a -> [String]
cnstr Int
n X (SomeDiagram a)
xd where
  cnstr :: SomeDiagram a -> [String]
cnstr (SomeDiagram Diagram t n m a
a) = [forall a. Show a => a -> String
aspCnstr Diagram t n m a
a]

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

-- xSomeDiagramOrnt -


-- | random variable of some diagram of @'Orientation' __p__@.

xSomeDiagramOrnt :: Entity p => X SomeNatural -> X p -> X (SomeDiagram (Orientation p))
xSomeDiagramOrnt :: forall p.
Entity p =>
X SomeNatural -> X p -> X (SomeDiagram (Orientation p))
xSomeDiagramOrnt X SomeNatural
xn X p
xp
  = forall a.
Oriented a =>
X SomeNatural
-> XOrtSite 'To a
-> XOrtSite 'From a
-> XOrtOrientation a
-> X (SomeDiagram a)
xSomeDiagram X SomeNatural
xn (forall p. X p -> XOrtSite 'To (Orientation p)
xEndOrnt X p
xp) (forall p. X p -> XOrtSite 'From (Orientation p)
xStartOrnt X p
xp) (forall p. X p -> XOrtOrientation (Orientation p)
xoOrnt X p
xp)