{-# 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.

--

-- __Duality__#Duality# Each diagram admits a co-diagram just by /reversing/ the arrows and leaving

-- the points untouched. In the following it will be demonstrated how to work - respectively -

-- how to switch between a diagram and its co-diagram and how this duality-concept is

-- implemented.

--

-- Let @d@ be a diagram in @'Diagram' __t n m x__@ over a 'Oriented' structure @__x__@. To get

-- the co-diagram @d'@ of @d@ just use the code:

--

-- @

-- Contravariant2 i   = toDualOpOrt

-- SDualBi (Left1 d') = amapF i (SDualBi (Right1 d))

-- @

--

-- where 'toDualOpOrt' is the duality operator with type @'IsoO' 'Ort' 'Op' __x__ ('Op' __x__)@

-- which can be applied to 'SDualBi'.

--

-- And to get the diagram @d@ of a given co-diagram @d'@ just use the code:

--

-- @

-- Contravariant2 i   = toDualOpOrt

-- SDualBi (Right1 d) = amapF (inv2 i) (SDualBi (Left1 d'))

-- @

--

-- where @'inv2' i@ is the inverse of @i@. As the application of @'IsoO' 'Ort' 'Op'@ on 'SDualBi'

-- is functorial, the two mappings @'amapF' i@ and @'amapF' ('inv2' i)@ are inverse to each other.

--

-- To implement this behavior, follow the following steps:

--

-- First implement two functions on @'Diagram' __t n m x__@, where the one maps it to

-- @'Diagram' __t n m y__@ according to a covariant homomorphism on 'Oriented' structures

-- (see 'dgMapCov') and the other maps it to @'Diagram' ('Dual' t) n m y@ (see 'dgMapCnt').

-- 

-- Now define the duality on the types according

--

-- @

-- type instance Dual1 (Diagram t n m) = Diagram (Dual t) n m

-- @

--

-- With this definitions you can implement the mapping 'dgMapS' on 'SDualBi' by

--

-- @

-- dgMapS = vmapBi dgMapCov dgMapCov dgMapCnt dgMapCnt

-- @

--

-- where 'vmapBi' implements the duality mapping on 'SDualBi'.

--

-- Finally on can declare the

--

-- @

-- instance (HomDisjunctiveOriented h, t ~ Dual (Dual t))

--   => ApplicativeG (SDualBi (Diagram t n m)) h (->) where

--   amapG = dgMapS

-- @

--

-- and because of the given implementation of 'dgMapCov', 'dgMapCnt' and the property of 'vmapBi'

-- on can declare: 

--

-- @

-- instance

--   ( HomOrientedDisjunctive h

--   , FunctorialOriented h

--   , t ~ Dual (Dual t)

--   )

--   => FunctorialG (SDualBi (Diagram t n m)) h (->)

-- @

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

    Diagram(..), DiagramType(..), rt'
  , dgType, dgTypeRefl, dgPoints, dgCenter, dgArrows
  , dgQuiver
  
    -- * Duality

  , dgMapS, dgMapCov, dgMapCnt, dgMap


     -- ** Chain

  , chnToStart, chnFromStart

    -- ** Parallel

  , dgPrlAdjZero
  , dgPrlTail, dgPrlDiffHead
  , dgPrlDiffTail

    -- * SomeDiagram

  , SomeDiagram(..), sdgMap

    -- * X

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

  )
  where

import Control.Monad 

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

import OAlg.Prelude hiding (T)

import OAlg.Category.SDuality

import OAlg.Data.Either

import OAlg.Structure.Oriented
import OAlg.Structure.Additive
import OAlg.Structure.Distributive
import OAlg.Hom.Definition
import OAlg.Hom.Oriented

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
(Int -> DiagramType -> ShowS)
-> (DiagramType -> String)
-> ([DiagramType] -> ShowS)
-> Show DiagramType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DiagramType -> ShowS
showsPrec :: Int -> DiagramType -> ShowS
$cshow :: DiagramType -> String
show :: DiagramType -> String
$cshowList :: [DiagramType] -> ShowS
showList :: [DiagramType] -> ShowS
Show,DiagramType -> DiagramType -> Bool
(DiagramType -> DiagramType -> Bool)
-> (DiagramType -> DiagramType -> Bool) -> Eq DiagramType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DiagramType -> DiagramType -> Bool
== :: DiagramType -> DiagramType -> Bool
$c/= :: DiagramType -> DiagramType -> Bool
/= :: DiagramType -> DiagramType -> Bool
Eq,Eq DiagramType
Eq DiagramType =>
(DiagramType -> DiagramType -> Ordering)
-> (DiagramType -> DiagramType -> Bool)
-> (DiagramType -> DiagramType -> Bool)
-> (DiagramType -> DiagramType -> Bool)
-> (DiagramType -> DiagramType -> Bool)
-> (DiagramType -> DiagramType -> DiagramType)
-> (DiagramType -> DiagramType -> DiagramType)
-> Ord 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
$ccompare :: DiagramType -> DiagramType -> Ordering
compare :: DiagramType -> DiagramType -> Ordering
$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
>= :: DiagramType -> DiagramType -> Bool
$cmax :: DiagramType -> DiagramType -> DiagramType
max :: DiagramType -> DiagramType -> DiagramType
$cmin :: DiagramType -> DiagramType -> DiagramType
min :: DiagramType -> DiagramType -> DiagramType
Ord)

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

-- DiagramType - Dual -


type instance Dual 'Empty        = 'Empty
type instance Dual 'Discrete     = 'Discrete
type instance Dual ('Chain t)    = 'Chain (Dual t)
type instance Dual ('Parallel t) = 'Parallel (Dual t)
type instance Dual ('Star t)     = 'Star (Dual t)
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 = Dual t :~: Dual t
Dual (Dual (Dual t)) :~: Dual t
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 (Show a, ShowPoint a) => Show (Diagram t n m a)
deriving instance (Eq a, EqPoint a) => Eq (Diagram t n m 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            -> t :~: t
Dual (Dual t) :~: t
forall {k} (a :: k). a :~: a
Refl
  DiagramDiscrete FinList n (Point a)
_       -> t :~: t
Dual (Dual t) :~: t
forall {k} (a :: k). a :~: a
Refl
  DiagramChainTo Point a
_ FinList m a
_      -> t :~: t
Dual (Dual t) :~: t
forall {k} (a :: k). a :~: a
Refl
  DiagramChainFrom Point a
_ FinList m a
_    -> t :~: t
Dual (Dual t) :~: t
forall {k} (a :: k). a :~: a
Refl
  DiagramParallelLR Point a
_ Point a
_ FinList m a
_ -> t :~: t
Dual (Dual t) :~: t
forall {k} (a :: k). a :~: a
Refl
  DiagramParallelRL Point a
_ Point a
_ FinList m a
_ -> t :~: t
Dual (Dual t) :~: t
forall {k} (a :: k). a :~: a
Refl
  DiagramSink Point a
_ FinList m a
_         -> t :~: t
Dual (Dual t) :~: t
forall {k} (a :: k). a :~: a
Refl
  DiagramSource Point a
_ FinList m a
_       -> t :~: t
Dual (Dual t) :~: t
forall {k} (a :: k). a :~: a
Refl
  DiagramGeneral FinList n (Point a)
_ FinList m (a, Orientation N)
_      -> t :~: t
Dual (Dual t) :~: t
forall {k} (a :: k). a :~: a
Refl

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

-- 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            -> FinList n (Point a)
FinList 'N0 (Point a)
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
ePoint a -> FinList m (Point a) -> FinList (m + 1) (Point a)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|(a -> Point a) -> FinList m a -> FinList m (Point a)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 a -> Point a
forall q. Oriented q => q -> Point q
start FinList m a
as
  DiagramChainFrom Point a
s FinList m a
as   -> Point a
sPoint a -> FinList m (Point a) -> FinList (m + 1) (Point a)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|(a -> Point a) -> FinList m a -> FinList m (Point a)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 a -> Point a
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 Point a -> FinList N1 (Point a) -> FinList (N1 + 1) (Point a)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:| Point a
q Point a -> FinList 'N0 (Point a) -> FinList ('N0 + 1) (Point a)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:| FinList 'N0 (Point a)
forall a. FinList 'N0 a
Nil
  DiagramParallelRL Point a
p Point a
q FinList m a
_ -> Point a
p Point a -> FinList N1 (Point a) -> FinList (N1 + 1) (Point a)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:| Point a
q Point a -> FinList 'N0 (Point a) -> FinList ('N0 + 1) (Point a)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:| FinList 'N0 (Point a)
forall a. FinList 'N0 a
Nil
  DiagramSink Point a
p FinList m a
as        -> Point a
p Point a -> FinList m (Point a) -> FinList (m + 1) (Point a)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:| (a -> Point a) -> FinList m a -> FinList m (Point a)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 a -> Point a
forall q. Oriented q => q -> Point q
start FinList m a
as
  DiagramSource Point a
p FinList m a
as      -> Point a
p Point a -> FinList m (Point a) -> FinList (m + 1) (Point a)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:| (a -> Point a) -> FinList m a -> FinList m (Point a)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 a -> Point a
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             -> FinList m a
FinList 'N0 a
forall a. FinList 'N0 a
Nil
  DiagramDiscrete FinList n (Point a)
_        -> FinList m a
FinList 'N0 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     -> ((a, Orientation N) -> a)
-> FinList m (a, Orientation N) -> FinList m a
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (a, Orientation N) -> a
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

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

-- Diagram - Duality -


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

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

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

-- dgMap -


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

--

-- __Properties__ Let @d@ be in @'Diagram __t n m a__@ and

-- @'Covariant2' h@ in @'Variant2' 'Covariant' __h a b__@ with

-- @'HomOrientedDisjunctive' __s o h__@, then holds:

--

-- (1) @'dgArrows' ('dgMapCov' q h d) '==' 'amap1' ('amap' h) ('dgArrows' d)@.

--

-- (2) @'dgPoints' ('dgMapCov' q h d) '==' 'amap1' ('pmap' h) ('dgPoints' d)@.

--

-- where @q@ is any proxy in @__q s o__@.

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

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

-- dgMapCov -


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

dgMapCov :: HomOrientedDisjunctive h
  => Variant2 Covariant h x y -> Diagram t n m x -> Diagram t n m y
dgMapCov :: 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 x y -> Diagram t n m x -> Diagram t n m y
forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOriented h =>
h x y -> Diagram t n m x -> Diagram t n m y
dgMap

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

-- dgMapCnt -


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

--

-- __Properties__ Let @d@ be in @'Diagram __t n m a__@ and

-- @'Contravariant2' h@ in @'Variant2' 'Contravariant' __h a b__@ with

-- @'HomOrientedDisjunctive' __s o h__@, then holds:

--

-- (1) @'dgArrows' ('dgMapCov' q h d) '==' 'amap1' ('amap' h) ('dgArrows' d)@.

--

-- (2) @'dgPoints' ('dgMapCov' q h d) '==' 'amap1' ('pmap' h) ('dgPoints' d)@.

--

-- where @q@ is any proxy in @__q s o__@.

dgMapCnt :: HomOrientedDisjunctive h
  => Variant2 Contravariant h x y -> Diagram t n m x -> Dual1 (Diagram t n m) y
dgMapCnt :: 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 (Contravariant2 h x y
h) Diagram t n m x
d = case Diagram t n m x
d of
  Diagram t n m x
DiagramEmpty             -> Dual1 (Diagram t n m) y
Diagram 'Empty 'N0 'N0 y
forall a. Diagram 'Empty 'N0 'N0 a
DiagramEmpty
  DiagramDiscrete FinList n (Point x)
ps       -> FinList n (Point y) -> Diagram 'Discrete n 'N0 y
forall (n :: N') a.
FinList n (Point a) -> Diagram 'Discrete n 'N0 a
DiagramDiscrete ((Point x -> Point y) -> FinList n (Point x) -> FinList n (Point y)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Point x -> Point y
hPnt FinList n (Point x)
ps)
  DiagramChainTo Point x
e FinList m x
as      -> Point y -> FinList m y -> Diagram ('Chain 'From) (m + 1) m y
forall a (m :: N').
Point a -> FinList m a -> Diagram ('Chain 'From) (m + 1) m a
DiagramChainFrom (Point x -> Point y
hPnt Point x
e) ((x -> y) -> FinList m x -> FinList m y
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 x -> y
hArw FinList m x
as)
  DiagramChainFrom Point x
s FinList m x
as    -> Point y -> FinList m y -> Diagram ('Chain 'To) (m + 1) m y
forall a (m :: N').
Point a -> FinList m a -> Diagram ('Chain 'To) (m + 1) m a
DiagramChainTo (Point x -> Point y
hPnt Point x
s) ((x -> y) -> FinList m x -> FinList m y
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 x -> y
hArw FinList m x
as)
  DiagramParallelLR Point x
l Point x
r FinList m x
as -> Point y
-> Point y
-> FinList m y
-> Diagram ('Parallel 'RightToLeft) ('S N1) m y
forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'RightToLeft) ('S N1) m a
DiagramParallelRL (Point x -> Point y
hPnt Point x
l) (Point x -> Point y
hPnt Point x
r) ((x -> y) -> FinList m x -> FinList m y
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 x -> y
hArw FinList m x
as)
  DiagramParallelRL Point x
l Point x
r FinList m x
as -> Point y
-> Point y
-> FinList m y
-> Diagram ('Parallel 'LeftToRight) ('S N1) m y
forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) ('S N1) m a
DiagramParallelLR (Point x -> Point y
hPnt Point x
l) (Point x -> Point y
hPnt Point x
r) ((x -> y) -> FinList m x -> FinList m y
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 x -> y
hArw FinList m x
as)
  DiagramSink Point x
e FinList m x
as         -> Point y -> FinList m y -> Diagram ('Star 'From) (m + 1) m y
forall a (m :: N').
Point a -> FinList m a -> Diagram ('Star 'From) (m + 1) m a
DiagramSource (Point x -> Point y
hPnt Point x
e) ((x -> y) -> FinList m x -> FinList m y
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 x -> y
hArw FinList m x
as)
  DiagramSource Point x
s FinList m x
as       -> Point y -> FinList m y -> Diagram ('Star 'To) (m + 1) m y
forall a (m :: N').
Point a -> FinList m a -> Diagram ('Star 'To) (m + 1) m a
DiagramSink (Point x -> Point y
hPnt Point x
s) ((x -> y) -> FinList m x -> FinList m y
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 x -> y
hArw FinList m x
as)
  DiagramGeneral FinList n (Point x)
ps FinList m (x, Orientation N)
aijs   -> FinList n (Point y)
-> FinList m (y, Orientation N) -> Diagram 'General n m y
forall (n :: N') a (m :: N').
FinList n (Point a)
-> FinList m (a, Orientation N) -> Diagram 'General n m a
DiagramGeneral
                                ((Point x -> Point y) -> FinList n (Point x) -> FinList n (Point y)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Point x -> Point y
hPnt FinList n (Point x)
ps)
                                (((x, Orientation N) -> (y, Orientation N))
-> FinList m (x, Orientation N) -> FinList m (y, Orientation N)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(x
a,Orientation N
o) -> (x -> y
hArw x
a,Orientation N -> Orientation N
forall p. Orientation p -> Orientation p
opposite Orientation N
o)) FinList m (x, Orientation N)
aijs)
  where hPnt :: Point x -> Point y
hPnt = h x y -> Point x -> Point y
forall (h :: * -> * -> *) x y.
ApplicativePoint h =>
h x y -> Point x -> Point y
pmap h x y
h
        hArw :: x -> y
hArw = h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h x y
h

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

-- dgMapS -


-- | the canonically induced application given by 'dgMap' and 'dgMapCnt'.

dgMapS :: (HomOrientedDisjunctive h, t ~ Dual (Dual t))
  => h x y -> SDualBi (Diagram t n m) x -> SDualBi (Diagram t n m) y
dgMapS :: forall (h :: * -> * -> *) (t :: DiagramType) x y (n :: N')
       (m :: N').
(HomOrientedDisjunctive h, t ~ Dual (Dual t)) =>
h x y -> SDualBi (Diagram t n m) x -> SDualBi (Diagram t n m) y
dgMapS = (Variant2 'Covariant h x y -> Diagram t n m x -> Diagram t n m y)
-> (Variant2 'Covariant h x y
    -> Dual1 (Diagram t n m) x -> Dual1 (Diagram t n m) y)
-> (Variant2 'Contravariant h x y
    -> Diagram t n m x -> Dual1 (Diagram t n m) y)
-> (Variant2 'Contravariant h x y
    -> Dual1 (Diagram t n m) x -> Diagram t n m y)
-> h x y
-> SDualBi (Diagram t n m) x
-> SDualBi (Diagram 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 -> Diagram t n m x -> Diagram t n m y
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 x y
-> Dual1 (Diagram t n m) x -> Dual1 (Diagram t n m) y
Variant2 'Covariant h x y
-> Diagram (Dual t) n m x -> Diagram (Dual t) n m y
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 'Contravariant h x y
-> Diagram t n m x -> Dual1 (Diagram t n m) y
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 x y
-> Dual1 (Diagram t n m) x -> Diagram t n m y
Variant2 'Contravariant h x y
-> Diagram (Dual t) n m x -> Dual1 (Diagram (Dual t) n m) y
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

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

-- Diagram - FunctorialG -


instance HomOriented h
  => ApplicativeG (Diagram t n m) h (->) where amapG :: forall x y. h x y -> Diagram t n m x -> Diagram t n m y
amapG = h x y -> Diagram t n m x -> Diagram t n m y
forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOriented h =>
h x y -> Diagram t n m x -> Diagram t n m y
dgMap

instance (HomOriented h, FunctorialOriented h)
  => FunctorialG (Diagram t n m) h (->)

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

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

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

-- 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 -> FinList n (Point a) -> Statement
forall a. Validable a => a -> Statement
valid FinList n (Point a)
ps
    DiagramChainTo Point a
e FinList m a
as -> Point a -> Statement
forall a. Validable a => a -> Statement
valid Point a
e Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& N -> Point a -> FinList m a -> Statement
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 n1 a
as) = [Statement] -> Statement
And [ a -> Statement
forall a. Validable a => a -> Statement
valid a
a
                            , Label
lC Label -> Statement -> Statement
:<=>: (a -> Point a
forall q. Oriented q => q -> Point q
end a
a Point a -> Point a -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
e)Bool -> Message -> Statement
:?>N -> Message
prm N
i
                            , N -> Point a -> FinList n1 a -> Statement
forall a (m :: N').
Oriented a =>
N -> Point a -> FinList m a -> Statement
vld (N -> N
forall a. Enum a => a -> a
succ N
i) (a -> Point a
forall q. Oriented q => q -> Point q
start a
a) FinList n1 a
as
                            ]
                        
    DiagramParallelLR Point a
l Point a
r FinList m a
as -> Orientation (Point a) -> Statement
forall a. Validable a => a -> Statement
valid Orientation (Point a)
o Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& N -> Orientation (Point a) -> FinList m a -> Statement
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
lPoint a -> Point a -> Orientation (Point a)
forall 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 n1 a
as)
        = [Statement] -> Statement
And [ a -> Statement
forall a. Validable a => a -> Statement
valid a
a
              , Label
lO Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
a Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Orientation (Point a)
o)Bool -> Message -> Statement
:?>N -> Message
prm N
i
              , N -> Orientation (Point a) -> FinList n1 a -> Statement
forall a (m :: N').
Oriented a =>
N -> Orientation (Point a) -> FinList m a -> Statement
vld (N -> N
forall a. Enum a => a -> a
succ N
i) Orientation (Point a)
o FinList n1 a
as
              ]

    DiagramSink Point a
e FinList m a
as -> Point a -> Statement
forall a. Validable a => a -> Statement
valid Point a
e Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& N -> Point a -> FinList m a -> Statement
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 n1 a
as)
        = [Statement] -> Statement
And [ a -> Statement
forall a. Validable a => a -> Statement
valid a
a
              , Label
lE Label -> Statement -> Statement
:<=>: (a -> Point a
forall q. Oriented q => q -> Point q
end a
a Point a -> Point a -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
e)Bool -> Message -> Statement
:?>N -> Message
prm N
i
              , N -> Point a -> FinList n1 a -> Statement
forall a (m :: N').
Oriented a =>
N -> Point a -> FinList m a -> Statement
vld (N -> N
forall a. Enum a => a -> a
succ N
i) Point a
e FinList n1 a
as
              ]

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

    Diagram t n m a
_ -> case 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
d of
      Dual (Dual t) :~: t
Refl -> Diagram (Dual t) n m (Op a) -> Statement
forall a. Validable a => a -> Statement
valid Dual1 (Diagram t n m) (Op a)
Diagram (Dual t) n m (Op a)
d' where
        SDualBi (Left1 Dual1 (Diagram t n m) (Op a)
d')          = HomDisj Ort Op (HomEmpty Ort) a (Op a)
-> SDualBi (Diagram t n m) a -> SDualBi (Diagram t n m) (Op a)
forall x y.
HomDisj Ort Op (HomEmpty Ort) x y
-> SDualBi (Diagram t n m) x -> SDualBi (Diagram t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG HomDisj Ort Op (HomEmpty Ort) a (Op a)
toOp (Either1 (Dual1 (Diagram t n m)) (Diagram t n m) a
-> SDualBi (Diagram t n m) a
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Diagram t n m a -> Either1 (Diagram (Dual t) n m) (Diagram t n m) a
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Diagram t n m a
d))
        Contravariant2 (Inv2 HomDisj Ort Op (HomEmpty Ort) a (Op a)
toOp HomDisjEmpty Ort Op (Op a) a
_) = Variant2 'Contravariant (IsoO Ort Op) a (Op a)
forall x.
Oriented x =>
Variant2 'Contravariant (IsoO Ort Op) x (Op x)
toDualOpOrt
    where prm :: N -> Message
          prm :: N -> Message
prm N
i = [Parameter] -> Message
Params[String
"i"String -> String -> Parameter
:=N -> String
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"


instance Oriented a => ValidableDual1 (Diagram t n m) a

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

-- Diagram - Oriented -


type instance Point (Diagram (Parallel d) n m a) = Point a
instance ShowPoint a => ShowPoint (Diagram (Parallel d) n m a)
instance EqPoint a => EqPoint (Diagram (Parallel d) n m a)
instance Oriented a => ValidablePoint (Diagram (Parallel d) n m a)
instance TypeablePoint a => TypeablePoint (Diagram (Parallel d) n m a)
instance (Oriented a, Typeable d, Typeable n, Typeable m)
  => Oriented (Diagram (Parallel d) n m a) where
  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
lPoint a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:>Point a
r
  orientation (DiagramParallelRL Point a
l Point a
r FinList m a
_) = Point a
rPoint a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:>Point a
l

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

-- dgQuiver -


-- | the underlying quiver of a diagram.

dgQuiver :: Oriented a => Diagram t n m a -> Quiver n m
dgQuiver :: forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> Quiver n m
dgQuiver Diagram t n m a
DiagramEmpty = Any n -> FinList m (Orientation N) -> Quiver n m
forall (n :: N') (m :: N').
Any n -> FinList m (Orientation N) -> Quiver n m
Quiver Any n
W 'N0
W0 FinList m (Orientation N)
FinList 'N0 (Orientation N)
forall a. FinList 'N0 a
Nil
dgQuiver (DiagramDiscrete FinList n (Point a)
ps) = Any n -> FinList m (Orientation N) -> Quiver n m
forall (n :: N') (m :: N').
Any n -> FinList m (Orientation N) -> Quiver n m
Quiver (FinList n (Point a) -> Any n
forall (n :: N') a. FinList n a -> W n
toW FinList n (Point a)
ps) FinList m (Orientation N)
FinList 'N0 (Orientation N)
forall a. FinList 'N0 a
Nil
dgQuiver (DiagramChainTo Point a
_ FinList m a
as) = Any n -> FinList m (Orientation N) -> Quiver n m
forall (n :: N') (m :: N').
Any n -> FinList m (Orientation N) -> Quiver n m
Quiver (W m -> W (m + 1)
forall (n1 :: N'). W n1 -> W (n1 + 1)
SW (FinList m (Orientation N) -> W m
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 = N -> FinList m a -> FinList m (Orientation N)
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     = FinList m (Orientation N)
FinList 'N0 (Orientation N)
forall a. FinList 'N0 a
Nil
  chnTo N
j (x
_:|FinList n1 x
os) = (N
j' N -> N -> Orientation N
forall p. p -> p -> Orientation p
:> N
j)Orientation N
-> FinList n1 (Orientation N) -> FinList (n1 + 1) (Orientation N)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|N -> FinList n1 x -> FinList n1 (Orientation N)
forall (m :: N') x. N -> FinList m x -> FinList m (Orientation N)
chnTo N
j' FinList n1 x
os where j' :: N
j' = N -> N
forall a. Enum a => a -> a
succ N
j
dgQuiver (DiagramParallelLR Point a
_ Point a
_ FinList m a
as) = Any n -> FinList m (Orientation N) -> Quiver n m
forall (n :: N') (m :: N').
Any n -> FinList m (Orientation N) -> Quiver n m
Quiver Any n
forall (n :: N'). Attestable n => W n
attest ((a -> Orientation N) -> FinList m a -> FinList m (Orientation N)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (Orientation N -> a -> Orientation N
forall b a. b -> a -> b
const (N
0N -> N -> Orientation N
forall p. p -> p -> Orientation p
:>N
1)) FinList m a
as)
dgQuiver (DiagramSink Point a
_ FinList m a
as) = Any n -> FinList m (Orientation N) -> Quiver n m
forall (n :: N') (m :: N').
Any n -> FinList m (Orientation N) -> Quiver n m
Quiver (W m -> W (m + 1)
forall (n1 :: N'). W n1 -> W (n1 + 1)
SW (FinList m (Orientation N) -> W m
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 = N -> FinList m a -> FinList m (Orientation N)
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     = FinList m (Orientation N)
FinList 'N0 (Orientation N)
forall a. FinList 'N0 a
Nil
  snk N
j (x
_:|FinList n1 x
os) = (N
jN -> N -> Orientation N
forall p. p -> p -> Orientation p
:>N
0)Orientation N
-> FinList n1 (Orientation N) -> FinList (n1 + 1) (Orientation N)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|N -> FinList n1 x -> FinList n1 (Orientation N)
forall (m :: N') x. N -> FinList m x -> FinList m (Orientation N)
snk (N -> N
forall a. Enum a => a -> a
succ N
j) FinList n1 x
os
dgQuiver (DiagramGeneral FinList n (Point a)
ps FinList m (a, Orientation N)
os) = Any n -> FinList m (Orientation N) -> Quiver n m
forall (n :: N') (m :: N').
Any n -> FinList m (Orientation N) -> Quiver n m
Quiver (FinList n (Point a) -> Any n
forall (n :: N') a. FinList n a -> W n
toW FinList n (Point a)
ps) (((a, Orientation N) -> Orientation N)
-> FinList m (a, Orientation N) -> FinList m (Orientation N)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (a, Orientation N) -> Orientation N
forall a b. (a, b) -> b
snd FinList m (a, Orientation N)
os)
dgQuiver Diagram t n m a
d = case 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
d of
  Dual (Dual t) :~: t
Refl -> Dual (Quiver n m) -> Quiver n m
Quiver n m -> Quiver n m
forall (n :: N') (m :: N'). Dual (Quiver n m) -> Quiver n m
coQuiverInv (Quiver n m -> Quiver n m) -> Quiver n m -> Quiver n m
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Diagram (Dual t) n m (Op a) -> Quiver n m
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> Quiver n m
dgQuiver Dual1 (Diagram t n m) (Op a)
Diagram (Dual t) n m (Op a)
d' where
    SDualBi (Left1 Dual1 (Diagram t n m) (Op a)
d') = HomDisj Ort Op (HomEmpty Ort) a (Op a)
-> SDualBi (Diagram t n m) a -> SDualBi (Diagram t n m) (Op a)
forall x y.
HomDisj Ort Op (HomEmpty Ort) x y
-> SDualBi (Diagram t n m) x -> SDualBi (Diagram t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG HomDisj Ort Op (HomEmpty Ort) a (Op a)
toOp (Either1 (Dual1 (Diagram t n m)) (Diagram t n m) a
-> SDualBi (Diagram t n m) a
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Diagram t n m a -> Either1 (Diagram (Dual t) n m) (Diagram t n m) a
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Diagram t n m a
d))
    Contravariant2 (Inv2 HomDisj Ort Op (HomEmpty Ort) a (Op a)
toOp HomDisjEmpty Ort Op (Op a) a
_) = Variant2 'Contravariant (IsoO Ort Op) a (Op a)
forall x.
Oriented x =>
Variant2 'Contravariant (IsoO Ort Op) x (Op x)
toDualOpOrt

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

-- 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 n1 a
as -> Point a -> FinList n1 a -> Point a
forall a (m :: N'). Oriented a => Point a -> FinList m a -> Point a
st (a -> Point a
forall q. Oriented q => q -> Point q
start a
a) FinList n1 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 n1 a
as)  = Point a -> FinList n1 a -> Point a
forall a (m :: N'). Oriented a => Point a -> FinList m a -> Point a
st (a -> Point a
forall q. Oriented q => q -> Point q
start a
a) FinList n1 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
_) = Diagram ('Chain 'To) ('S m) m (Op a) -> Point (Op a)
forall a (n :: N') (m :: N').
Oriented a =>
Diagram ('Chain 'To) n m a -> Point a
chnToStart Dual1 (Diagram ('Chain 'From) ('S m) m) (Op a)
Diagram ('Chain 'To) ('S m) m (Op a)
d' where
  SDualBi (Left1 Dual1 (Diagram ('Chain 'From) ('S m) m) (Op a)
d') = HomDisj Ort Op (HomEmpty Ort) a (Op a)
-> SDualBi (Diagram ('Chain 'From) ('S m) m) a
-> SDualBi (Diagram ('Chain 'From) ('S m) m) (Op a)
forall x y.
HomDisj Ort Op (HomEmpty Ort) x y
-> SDualBi (Diagram ('Chain 'From) ('S m) m) x
-> SDualBi (Diagram ('Chain 'From) ('S m) m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG HomDisj Ort Op (HomEmpty Ort) a (Op a)
toOp (Either1
  (Dual1 (Diagram ('Chain 'From) n m)) (Diagram ('Chain 'From) n m) a
-> SDualBi (Diagram ('Chain 'From) n m) a
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Diagram ('Chain 'From) n m a
-> Either1
     (Diagram ('Chain 'To) ('S m) m) (Diagram ('Chain 'From) n m) a
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Diagram ('Chain 'From) n m a
d))
  Contravariant2 (Inv2 HomDisj Ort Op (HomEmpty Ort) a (Op a)
toOp HomDisjEmpty Ort Op (Op a) a
_) = Variant2 'Contravariant (IsoO Ort Op) a (Op a)
forall x.
Oriented x =>
Variant2 'Contravariant (IsoO Ort Op) x (Op x)
toDualOpOrt

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

-- Diagram (Chain t) - Oriented -


type instance Point (Diagram (Chain t) n m a) = Point a
instance ShowPoint a => ShowPoint (Diagram (Chain t) n m a)
instance EqPoint a => EqPoint (Diagram (Chain t) n m a)
instance Oriented a => ValidablePoint (Diagram (Chain t) n m a)
instance TypeablePoint a => TypeablePoint (Diagram (Chain t) n m a)
instance (Oriented a, Typeable t, Typeable n, Typeable m) => Oriented (Diagram (Chain t) n m a) where
  
  start :: Diagram ('Chain t) n m a -> Point (Diagram ('Chain t) n m a)
start (DiagramChainFrom Point a
s FinList m a
_) = Point a
Point (Diagram ('Chain t) n m a)
s
  start d :: Diagram ('Chain t) n m a
d@(DiagramChainTo Point a
_ FinList m a
_) = Diagram ('Chain 'To) n m a -> Point a
forall a (n :: N') (m :: N').
Oriented a =>
Diagram ('Chain 'To) n m a -> Point a
chnToStart Diagram ('Chain t) n m a
Diagram ('Chain 'To) 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
_) = Diagram ('Chain 'From) n m a -> Point a
forall a (n :: N') (m :: N').
Oriented a =>
Diagram ('Chain 'From) n m a -> Point a
chnFromEnd Diagram ('Chain t) n m a
Diagram ('Chain 'From) n m a
d
  end (DiagramChainTo Point a
e FinList m a
_)     = Point a
Point (Diagram ('Chain t) n m 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) = Point a
-> Point a
-> FinList ('S m) a
-> Diagram ('Parallel 'LeftToRight) ('S N1) ('S m) a
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 (Root a -> a
forall a. Additive a => Root a -> a
zero (Point a
lPoint a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:>Point a
r)a -> FinList m a -> FinList (m + 1) a
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 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) = Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) ('S N1) m a
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 (FinList (m + 1) a -> FinList m a
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) = Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'RightToLeft) ('S N1) m a
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 (FinList (m + 1) a -> FinList m a
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 = Diagram ('Parallel d) n (m + 1) a -> Diagram ('Parallel d) n m a
Diagram ('Parallel d) n ('S m) a -> Diagram ('Parallel d) n m a
forall (d :: Direction) (n :: N') (m :: N') a.
Diagram ('Parallel d) n (m + 1) a -> Diagram ('Parallel d) n m a
dgPrlTail (Diagram ('Parallel d) n ('S m) a -> Diagram ('Parallel d) n m a)
-> (Diagram ('Parallel d) n ('S m) a
    -> Diagram ('Parallel d) n ('S m) a)
-> Diagram ('Parallel d) n ('S m) a
-> Diagram ('Parallel d) n m 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
. Diagram ('Parallel d) n (m + 1) a
-> Diagram ('Parallel d) n (m + 1) a
Diagram ('Parallel d) n ('S m) a
-> Diagram ('Parallel d) n ('S m) a
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 -> Point a
-> Point a
-> FinList ('S m) a
-> Diagram ('Parallel 'LeftToRight) ('S N1) ('S m) a
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 -> a) -> FinList ('S m) a -> FinList ('S m) a
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (a -> a -> a
forall {a}. Abelian a => a -> a -> a
diff (a -> a -> a) -> a -> a -> a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ FinList (m + 1) a -> a
forall (n :: N') a. FinList (n + 1) a -> a
head FinList (m + 1) a
as) FinList (m + 1) a
FinList ('S m) a
as)
  DiagramParallelRL Point a
l Point a
r FinList (m + 1) a
as -> Point a
-> Point a
-> FinList ('S m) a
-> Diagram ('Parallel 'RightToLeft) ('S N1) ('S m) a
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 ((a -> a) -> FinList ('S m) a -> FinList ('S m) a
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (a -> a -> a
forall {a}. Abelian a => a -> a -> a
diff (a -> a -> a) -> a -> a -> a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ FinList (m + 1) a -> a
forall (n :: N') a. FinList (n + 1) a -> a
head FinList (m + 1) a
as) FinList (m + 1) a
FinList ('S m) a
as)
  where diff :: a -> a -> a
diff a
a a
x = a
x a -> a -> a
forall {a}. Abelian a => a -> a -> a
- a
a

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

-- 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 Dual1 (XDiagram t n m) = XDiagram (Dual t) n m
type instance Dual (XDiagram t n m a) = Dual1 (XDiagram 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           -> Dual (XDiagram t n m a)
XDiagram 'Empty 'N0 'N0 (Op a)
forall a. XDiagram 'Empty 'N0 'N0 a
XDiagramEmpty
  XDiagramDiscrete Any n
n X (Point a)
xp   -> Any n -> X (Point (Op a)) -> XDiagram 'Discrete n 'N0 (Op a)
forall (n :: N') a.
Any n -> X (Point a) -> XDiagram 'Discrete n 'N0 a
XDiagramDiscrete Any n
n X (Point a)
X (Point (Op a))
xp
  XDiagramChainTo Any m
m XOrtSite 'To a
xe    -> Any m
-> XOrtSite 'From (Op a)
-> XDiagram ('Chain 'From) (m + 1) m (Op a)
forall (m :: N') a.
Any m -> XOrtSite 'From a -> XDiagram ('Chain 'From) (m + 1) m a
XDiagramChainFrom Any m
m (XOrtSite 'To a -> Dual (XOrtSite 'To a)
forall (s :: Site) q. XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite XOrtSite 'To a
xe)
  XDiagramChainFrom Any m
m XOrtSite 'From a
xs  -> Any m
-> XOrtSite 'To (Op a) -> XDiagram ('Chain 'To) (m + 1) m (Op a)
forall (m :: N') a.
Any m -> XOrtSite 'To a -> XDiagram ('Chain 'To) (m + 1) m a
XDiagramChainTo Any m
m (XOrtSite 'From a -> Dual (XOrtSite 'From a)
forall (s :: Site) q. XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite XOrtSite 'From a
xs)
  XDiagramParallelLR Any m
m XOrtOrientation a
xo -> Any m
-> XOrtOrientation (Op a)
-> XDiagram ('Parallel 'RightToLeft) ('S N1) m (Op a)
forall (m :: N') a.
Any m
-> XOrtOrientation a
-> XDiagram ('Parallel 'RightToLeft) ('S N1) m a
XDiagramParallelRL Any m
m (XOrtOrientation a -> Dual (XOrtOrientation a)
forall q. XOrtOrientation q -> Dual (XOrtOrientation q)
coXOrtOrientation XOrtOrientation a
xo)
  XDiagramParallelRL Any m
m XOrtOrientation a
xo -> Any m
-> XOrtOrientation (Op a)
-> XDiagram ('Parallel 'LeftToRight) ('S N1) m (Op a)
forall (m :: N') a.
Any m
-> XOrtOrientation a
-> XDiagram ('Parallel 'LeftToRight) ('S N1) m a
XDiagramParallelLR Any m
m (XOrtOrientation a -> Dual (XOrtOrientation a)
forall q. XOrtOrientation q -> Dual (XOrtOrientation q)
coXOrtOrientation XOrtOrientation a
xo)
  XDiagramSink Any m
m XOrtSite 'To a
xe       -> Any m
-> XOrtSite 'From (Op a) -> XDiagram ('Star 'From) (m + 1) m (Op a)
forall (m :: N') a.
Any m -> XOrtSite 'From a -> XDiagram ('Star 'From) (m + 1) m a
XDiagramSource Any m
m (XOrtSite 'To a -> Dual (XOrtSite 'To a)
forall (s :: Site) q. XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite XOrtSite 'To a
xe)
  XDiagramSource Any m
m XOrtSite 'From a
xs     -> Any m
-> XOrtSite 'To (Op a) -> XDiagram ('Star 'To) (m + 1) m (Op a)
forall (m :: N') a.
Any m -> XOrtSite 'To a -> XDiagram ('Star 'To) (m + 1) m a
XDiagramSink Any m
m (XOrtSite 'From a -> Dual (XOrtSite 'From a)
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    = X (Diagram 'Discrete n 'N0 a)
forall x. X x
XEmpty
xDiscrete p a
_ Any n
W0 X (Point a)
_        = Diagram 'Discrete n 'N0 a -> X (Diagram 'Discrete n 'N0 a)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (FinList n (Point a) -> Diagram 'Discrete n 'N0 a
forall (n :: N') a.
FinList n (Point a) -> Diagram 'Discrete n 'N0 a
DiagramDiscrete FinList n (Point a)
FinList 'N0 (Point a)
forall a. FinList 'N0 a
Nil)
xDiscrete p a
pa (SW W n1
n') X (Point a)
xp = do
  DiagramDiscrete FinList n1 (Point a)
ps <- p a -> W n1 -> X (Point a) -> X (Diagram 'Discrete n1 'N0 a)
forall (p :: * -> *) a (n :: N').
p a -> Any n -> X (Point a) -> X (Diagram 'Discrete n 'N0 a)
xDiscrete p a
pa W n1
n' X (Point a)
xp
  Point a
p <- X (Point a)
xp
  Diagram 'Discrete n 'N0 a -> X (Diagram 'Discrete n 'N0 a)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (FinList n (Point a) -> Diagram 'Discrete n 'N0 a
forall (n :: N') a.
FinList n (Point a) -> Diagram 'Discrete n 'N0 a
DiagramDiscrete (Point a
pPoint a -> FinList n1 (Point a) -> FinList (n1 + 1) (Point a)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList n1 (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) <- Any m -> XOrtSite 'To a -> Point a -> X (Point a, FinList m a)
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
  Diagram ('Chain 'To) ('S m) m a
-> X (Diagram ('Chain 'To) ('S m) m a)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Point a -> FinList m a -> Diagram ('Chain 'To) (m + 1) m a
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                    = (Point a, FinList 'N0 a) -> X (Point a, FinList 'N0 a)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Point a
e,FinList 'N0 a
forall a. FinList 'N0 a
Nil)
        xchn (SW W n1
m') xe :: XOrtSite 'To a
xe@(XEnd X (Point a)
_ Point a -> X a
xea) Point a
e = do
          (Point a
s,FinList n1 a
as) <- W n1 -> XOrtSite 'To a -> Point a -> X (Point a, FinList n1 a)
forall a (m :: N').
Oriented a =>
Any m -> XOrtSite 'To a -> Point a -> X (Point a, FinList m a)
xchn W n1
m' XOrtSite 'To a
xe Point a
e
          a
a <- Point a -> X a
xea Point a
s
          (Point a, FinList m a) -> X (Point a, FinList m a)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Point a
forall q. Oriented q => q -> Point q
start a
a,FinList n1 a
as FinList n1 a -> a -> FinList (n1 + 1) a
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 <- XOrtOrientation a -> X (Point a)
forall q. Oriented q => XOrtOrientation q -> X (Point q)
xoPoint XOrtOrientation a
xo
  Point a
r <- XOrtOrientation a -> X (Point a)
forall q. Oriented q => XOrtOrientation q -> X (Point q)
xoPoint XOrtOrientation a
xo
  Diagram ('Parallel 'LeftToRight) ('S N1) m a
-> X (Diagram ('Parallel 'LeftToRight) ('S N1) m a)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) ('S N1) m a
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 FinList m a
FinList 'N0 a
forall a. FinList 'N0 a
Nil)
xParallel (SW W n1
m') XOrtOrientation a
xo = do
  DiagramParallelLR Point a
l Point a
r FinList n1 a
as <- W n1
-> XOrtOrientation a
-> X (Diagram ('Parallel 'LeftToRight) ('S N1) n1 a)
forall a (m :: N').
Oriented a =>
Any m
-> XOrtOrientation a
-> X (Diagram ('Parallel 'LeftToRight) ('S N1) m a)
xParallel W n1
m' XOrtOrientation a
xo
  a
a <- XOrtOrientation a -> Orientation (Point a) -> X a
forall q. XOrtOrientation q -> Orientation (Point q) -> X q
xoArrow XOrtOrientation a
xo (Point a
lPoint a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:>Point a
r)
  Diagram ('Parallel 'LeftToRight) ('S N1) m a
-> X (Diagram ('Parallel 'LeftToRight) ('S N1) m a)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) ('S N1) m a
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
aa -> FinList n1 a -> FinList (n1 + 1) a
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList n1 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 <- XOrtSite 'To a -> X (Point a)
forall (s :: Site) q. XOrtSite s q -> X (Point q)
xosPoint XOrtSite 'To a
xe
  Diagram ('Star 'To) N1 'N0 a -> X (Diagram ('Star 'To) N1 'N0 a)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Point a -> FinList 'N0 a -> Diagram ('Star 'To) ('N0 + 1) 'N0 a
forall a (m :: N').
Point a -> FinList m a -> Diagram ('Star 'To) (m + 1) m a
DiagramSink Point a
e FinList 'N0 a
forall a. FinList 'N0 a
Nil)
xSink (SW W n1
m') xe :: XOrtSite 'To a
xe@(XEnd X (Point a)
_ Point a -> X a
xea) = do
  DiagramSink Point a
e FinList n1 a
as <- W n1 -> XOrtSite 'To a -> X (Diagram ('Star 'To) (n1 + 1) n1 a)
forall a (m :: N').
Oriented a =>
Any m -> XOrtSite 'To a -> X (Diagram ('Star 'To) (m + 1) m a)
xSink W n1
m' XOrtSite 'To a
xe
  a
a <- Point a -> X a
xea Point a
e
  Diagram ('Star 'To) ('S ('S n1)) ('S n1) a
-> X (Diagram ('Star 'To) ('S ('S n1)) ('S n1) a)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Point a
-> FinList ('S n1) a -> Diagram ('Star 'To) ('S n1 + 1) ('S n1) a
forall a (m :: N').
Point a -> FinList m a -> Diagram ('Star 'To) (m + 1) m a
DiagramSink Point a
e (a
aa -> FinList n1 a -> FinList (n1 + 1) a
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList n1 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 rt :: Dual (Dual t) :~: t
rt@Dual (Dual t) :~: t
Refl XDiagram t n m a
xd = case XDiagram t n m a
xd of
  XDiagram t n m a
XDiagramEmpty           -> Diagram t n m a -> X (Diagram t n m a)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return Diagram t n m a
Diagram 'Empty 'N0 'N0 a
forall a. Diagram 'Empty 'N0 'N0 a
DiagramEmpty
  XDiagramDiscrete Any n
n X (Point a)
xp   -> XDiagram t n m a
-> Any n -> X (Point a) -> X (Diagram 'Discrete n 'N0 a)
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    -> Any m -> XOrtSite 'To a -> X (Diagram ('Chain 'To) (m + 1) m a)
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 -> Any m
-> XOrtOrientation a
-> X (Diagram ('Parallel 'LeftToRight) ('S N1) m a)
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       -> Any m -> XOrtSite 'To a -> X (Diagram ('Star 'To) (m + 1) m a)
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
_                       ->   (Diagram (Dual t) n m (Op a) -> Diagram t n m a)
-> X (Diagram (Dual t) n m (Op a)) -> X (Diagram t n m a)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\Dual1 (Diagram t n m) (Op a)
d' -> let SDualBi (Right1 Diagram t n m a
d)
                                                   = HomDisj Ort Op (HomEmpty Ort) (Op a) a
-> SDualBi (Diagram t n m) (Op a) -> SDualBi (Diagram t n m) a
forall x y.
HomDisj Ort Op (HomEmpty Ort) x y
-> SDualBi (Diagram t n m) x -> SDualBi (Diagram t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG HomDisj Ort Op (HomEmpty Ort) (Op a) a
fromOp (Either1 (Dual1 (Diagram t n m)) (Diagram t n m) (Op a)
-> SDualBi (Diagram t n m) (Op a)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Dual1 (Diagram t n m) (Op a)
-> Either1 (Dual1 (Diagram t n m)) (Diagram t n m) (Op a)
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 Dual1 (Diagram t n m) (Op a)
d'))
                                                 Contravariant2 (Inv2 HomDisjEmpty Ort Op a (Op a)
_ HomDisj Ort Op (HomEmpty Ort) (Op a) a
fromOp) = Variant2 'Contravariant (IsoO Ort Op) a (Op a)
forall x.
Oriented x =>
Variant2 'Contravariant (IsoO Ort Op) x (Op x)
toDualOpOrt
                                             in Diagram t n m a
d)
                             (X (Diagram (Dual t) n m (Op a)) -> X (Diagram t n m a))
-> X (Diagram (Dual t) n m (Op a)) -> X (Diagram t n m a)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (Dual (Dual (Dual t)) :~: Dual t)
-> XDiagram (Dual t) n m (Op a) -> X (Diagram (Dual t) n m (Op 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 ((Dual (Dual t) :~: t) -> Dual (Dual (Dual t)) :~: Dual t
forall (t :: DiagramType).
(Dual (Dual t) :~: t) -> Dual (Dual (Dual t)) :~: Dual t
rt' Dual (Dual t) :~: t
rt) (XDiagram (Dual t) n m (Op a) -> X (Diagram (Dual t) n m (Op a)))
-> XDiagram (Dual t) n m (Op a) -> X (Diagram (Dual t) n m (Op a))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XDiagram t n m a -> Dual (XDiagram t n m a)
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

-- | random variable for 'Chain's.

xDiagramChain :: (Oriented x, Attestable m, n ~ m + 1)
  => XOrtSite t x -> X (Diagram (Chain t) n m x)
xDiagramChain :: forall x (m :: N') (n :: N') (t :: Site).
(Oriented x, Attestable m, n ~ (m + 1)) =>
XOrtSite t x -> X (Diagram ('Chain t) n m x)
xDiagramChain xo :: XOrtSite t x
xo@(XStart X (Point x)
_ Point x -> X x
_) = (Dual (Dual ('Chain t)) :~: 'Chain t)
-> XDiagram ('Chain t) n m x -> X (Diagram ('Chain t) n m x)
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 ('Chain t)) :~: 'Chain t
'Chain t :~: 'Chain t
forall {k} (a :: k). a :~: a
Refl (Any m -> XOrtSite 'From x -> XDiagram ('Chain 'From) (m + 1) m x
forall (m :: N') a.
Any m -> XOrtSite 'From a -> XDiagram ('Chain 'From) (m + 1) m a
XDiagramChainFrom Any m
m XOrtSite t x
XOrtSite 'From x
xo) where m :: Any m
m = Any m
forall (n :: N'). Attestable n => W n
attest
xDiagramChain xo :: XOrtSite t x
xo@(XEnd X (Point x)
_ Point x -> X x
_)   = (Dual (Dual ('Chain t)) :~: 'Chain t)
-> XDiagram ('Chain t) n m x -> X (Diagram ('Chain t) n m x)
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 ('Chain t)) :~: 'Chain t
'Chain t :~: 'Chain t
forall {k} (a :: k). a :~: a
Refl (Any m -> XOrtSite 'To x -> XDiagram ('Chain 'To) (m + 1) m x
forall (m :: N') a.
Any m -> XOrtSite 'To a -> XDiagram ('Chain 'To) (m + 1) m a
XDiagramChainTo Any m
m XOrtSite t x
XOrtSite 'To x
xo) where m :: Any m
m = Any m
forall (n :: N'). Attestable n => W n
attest

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

-- 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 = (Dual (Dual 'Empty) :~: 'Empty)
-> XDiagram 'Empty n m a -> X (Diagram 'Empty n m 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 Dual (Dual 'Empty) :~: 'Empty
'Empty :~: 'Empty
forall {k} (a :: k). a :~: a
Refl XDiagram 'Empty n m a
XDiagram 'Empty 'N0 'N0 a
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 = (Dual (Dual 'Discrete) :~: 'Discrete)
-> XDiagram 'Discrete n m a -> X (Diagram 'Discrete n m 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 Dual (Dual 'Discrete) :~: 'Discrete
'Discrete :~: 'Discrete
forall {k} (a :: k). a :~: a
Refl (Any n -> X (Point a) -> XDiagram 'Discrete n 'N0 a
forall (n :: N') a.
Any n -> X (Point a) -> XDiagram 'Discrete n 'N0 a
XDiagramDiscrete Any n
n X (Point a)
forall x. XStandard x => X x
xStandard) where n :: Any n
n = Any n
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 = (Dual (Dual ('Parallel 'LeftToRight)) :~: 'Parallel 'LeftToRight)
-> XDiagram ('Parallel 'LeftToRight) n m a
-> X (Diagram ('Parallel 'LeftToRight) n m 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 Dual (Dual ('Parallel 'LeftToRight)) :~: 'Parallel 'LeftToRight
'Parallel 'LeftToRight :~: 'Parallel 'LeftToRight
forall {k} (a :: k). a :~: a
Refl (Any m
-> XOrtOrientation a
-> XDiagram ('Parallel 'LeftToRight) ('S N1) m a
forall (m :: N') a.
Any m
-> XOrtOrientation a
-> XDiagram ('Parallel 'LeftToRight) ('S N1) m a
XDiagramParallelLR Any m
m XOrtOrientation a
forall q. XStandardOrtOrientation q => XOrtOrientation q
xStandardOrtOrientation) where
    m :: Any m
m = Any 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 = (Dual (Dual ('Parallel 'RightToLeft)) :~: 'Parallel 'RightToLeft)
-> XDiagram ('Parallel 'RightToLeft) n m a
-> X (Diagram ('Parallel 'RightToLeft) n m 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 Dual (Dual ('Parallel 'RightToLeft)) :~: 'Parallel 'RightToLeft
'Parallel 'RightToLeft :~: 'Parallel 'RightToLeft
forall {k} (a :: k). a :~: a
Refl (Any m
-> XOrtOrientation a
-> XDiagram ('Parallel 'RightToLeft) ('S N1) m a
forall (m :: N') a.
Any m
-> XOrtOrientation a
-> XDiagram ('Parallel 'RightToLeft) ('S N1) m a
XDiagramParallelRL Any m
m XOrtOrientation a
forall q. XStandardOrtOrientation q => XOrtOrientation q
xStandardOrtOrientation) where
    m :: Any m
m = Any 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 = (Dual (Dual ('Star 'To)) :~: 'Star 'To)
-> XDiagram ('Star 'To) ('S m) m a
-> X (Diagram ('Star 'To) ('S m) m 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 Dual (Dual ('Star 'To)) :~: 'Star 'To
'Star 'To :~: 'Star 'To
forall {k} (a :: k). a :~: a
Refl (Any m -> XOrtSite 'To a -> XDiagram ('Star 'To) (m + 1) m a
forall (m :: N') a.
Any m -> XOrtSite 'To a -> XDiagram ('Star 'To) (m + 1) m a
XDiagramSink Any m
m XOrtSite 'To a
forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite) where m :: Any m
m = Any 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 = (Dual (Dual ('Star 'From)) :~: 'Star 'From)
-> XDiagram ('Star 'From) ('S m) m a
-> X (Diagram ('Star 'From) ('S m) m 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 Dual (Dual ('Star 'From)) :~: 'Star 'From
'Star 'From :~: 'Star 'From
forall {k} (a :: k). a :~: a
Refl (Any m -> XOrtSite 'From a -> XDiagram ('Star 'From) (m + 1) m a
forall (m :: N') a.
Any m -> XOrtSite 'From a -> XDiagram ('Star 'From) (m + 1) m a
XDiagramSource Any m
m XOrtSite 'From a
forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite) where m :: Any m
m = Any m
forall (n :: N'). Attestable n => W n
attest

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

-- X (Diagram (Chain t) (m+1) m -


instance (Oriented a, XStandardOrtSite t a, Attestable m, n ~ m + 1)
  => XStandard (Diagram (Chain t) n m a) where
  xStandard :: X (Diagram ('Chain t) n m a)
xStandard = XOrtSite t a -> X (Diagram ('Chain t) n m a)
forall x (m :: N') (n :: N') (t :: Site).
(Oriented x, Attestable m, n ~ (m + 1)) =>
XOrtSite t x -> X (Diagram ('Chain t) n m x)
xDiagramChain XOrtSite t a
forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite

instance (Oriented x, XStandardOrtSite To x, XStandardOrtSite From x, Attestable m, n ~ m+1)
  => XStandardDual1 (SDualBi (Diagram (Chain To) n m)) x

instance (Oriented x, XStandardOrtSite From x, Attestable m, n ~ m+1)
  => XStandardDual1 (Diagram (Chain To) n m) x

instance (Attestable m, n ~ m+1)
  => TransformableG (SDualBi (Diagram (Chain To) n m)) OrtSiteX EqE where
  tauG :: forall x.
Struct OrtSiteX x
-> Struct EqE (SDualBi (Diagram ('Chain 'To) n m) x)
tauG Struct OrtSiteX x
Struct = Struct EqE (SDualBi (Diagram ('Chain 'To) n m) x)
forall s x. Structure s x => Struct s x
Struct

instance (Oriented x, XStandardOrtSite To x, XStandardOrtSite From x, Attestable m, n ~ m+1)
  => XStandardDual1 (SDualBi (Diagram (Chain From) n m)) x

instance (Oriented x, XStandardOrtSite To x, Attestable m, n ~ m+1)
  => XStandardDual1 (Diagram (Chain From) n m) x
  
instance (Attestable m, n ~ m+1)
  => TransformableG (SDualBi (Diagram (Chain From) n m)) OrtSiteX EqE where
  tauG :: forall x.
Struct OrtSiteX x
-> Struct EqE (SDualBi (Diagram ('Chain 'From) n m) x)
tauG Struct OrtSiteX x
Struct = Struct EqE (SDualBi (Diagram ('Chain 'From) n m) x)
forall s x. Structure s x => Struct s x
Struct

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

-- 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 => Eq (SomeDiagram a) where
  SomeDiagram Diagram t n m a
a == :: SomeDiagram a -> SomeDiagram a -> Bool
== SomeDiagram Diagram t n m a
b
    = [Bool] -> Bool
forall b. Boolean b => [b] -> b
and [ Diagram t n m a -> DiagramType
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> DiagramType
dgType Diagram t n m a
a DiagramType -> DiagramType -> Bool
forall a. Eq a => a -> a -> Bool
== Diagram t n m a -> DiagramType
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> DiagramType
dgType Diagram t n m a
b
          , Diagram t n m a -> Diagram t n m a -> Bool
forall x (t :: DiagramType) (n :: N') (m :: N') (t' :: DiagramType)
       (n' :: N') (m' :: N').
Oriented x =>
Diagram t n m x -> Diagram t' n' m' x -> Bool
eqPnts Diagram t n m a
a Diagram t n m a
b
          , Diagram t n m a -> Diagram t n m a -> Bool
forall x (t :: DiagramType) (n :: N') (m :: N') (t' :: DiagramType)
       (n' :: N') (m' :: N').
Oriented x =>
Diagram t n m x -> Diagram t' n' m' x -> Bool
eqArws Diagram t n m a
a Diagram t n m a
b
          , Diagram t n m a -> Diagram t n m a -> Bool
forall (t :: DiagramType) (n :: N') (m :: N') x (t' :: DiagramType)
       (n' :: N') (m' :: N').
Diagram t n m x -> Diagram t' n' m' x -> Bool
eqOrnt Diagram t n m a
a Diagram t n m a
b
          ]
    where
      eqPnts :: Oriented x => Diagram t n m x -> Diagram t' n' m' x -> Bool
      eqPnts :: forall x (t :: DiagramType) (n :: N') (m :: N') (t' :: DiagramType)
       (n' :: N') (m' :: N').
Oriented x =>
Diagram t n m x -> Diagram t' n' m' x -> Bool
eqPnts Diagram t n m x
a Diagram t' n' m' x
b = (FinList n (Point x) -> [Point x]
forall a. FinList n a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (FinList n (Point x) -> [Point x])
-> FinList n (Point x) -> [Point x]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Diagram t n m x -> FinList n (Point x)
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints Diagram t n m x
a) [Point x] -> [Point x] -> Bool
forall a. Eq a => a -> a -> Bool
== (FinList n' (Point x) -> [Point x]
forall a. FinList n' a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (FinList n' (Point x) -> [Point x])
-> FinList n' (Point x) -> [Point x]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Diagram t' n' m' x -> FinList n' (Point x)
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints Diagram t' n' m' x
b)

      eqArws :: Oriented x => Diagram t n m x -> Diagram t' n' m' x -> Bool
      eqArws :: forall x (t :: DiagramType) (n :: N') (m :: N') (t' :: DiagramType)
       (n' :: N') (m' :: N').
Oriented x =>
Diagram t n m x -> Diagram t' n' m' x -> Bool
eqArws Diagram t n m x
a Diagram t' n' m' x
b = (FinList m x -> [x]
forall a. FinList m a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (FinList m x -> [x]) -> FinList m x -> [x]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Diagram t n m x -> FinList m x
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> FinList m a
dgArrows Diagram t n m x
a) [x] -> [x] -> Bool
forall a. Eq a => a -> a -> Bool
== (FinList m' x -> [x]
forall a. FinList m' a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (FinList m' x -> [x]) -> FinList m' x -> [x]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Diagram t' n' m' x -> FinList m' x
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> FinList m a
dgArrows Diagram t' n' m' x
b)

      eqOrnt :: Diagram t n m x -> Diagram t' n' m' x -> Bool
      eqOrnt :: forall (t :: DiagramType) (n :: N') (m :: N') x (t' :: DiagramType)
       (n' :: N') (m' :: N').
Diagram t n m x -> Diagram t' n' m' x -> Bool
eqOrnt (DiagramGeneral FinList n (Point x)
_ FinList m (x, Orientation N)
o) (DiagramGeneral FinList n' (Point x)
_ FinList m' (x, Orientation N)
o')
        = (FinList m (Orientation N) -> [Orientation N]
forall a. FinList m a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (FinList m (Orientation N) -> [Orientation N])
-> FinList m (Orientation N) -> [Orientation N]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((x, Orientation N) -> Orientation N)
-> FinList m (x, Orientation N) -> FinList m (Orientation N)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (x, Orientation N) -> Orientation N
forall a b. (a, b) -> b
snd FinList m (x, Orientation N)
o) [Orientation N] -> [Orientation N] -> Bool
forall a. Eq a => a -> a -> Bool
== (FinList m' (Orientation N) -> [Orientation N]
forall a. FinList m' a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (FinList m' (Orientation N) -> [Orientation N])
-> FinList m' (Orientation N) -> [Orientation N]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((x, Orientation N) -> Orientation N)
-> FinList m' (x, Orientation N) -> FinList m' (Orientation N)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (x, Orientation N) -> Orientation N
forall a b. (a, b) -> b
snd FinList m' (x, Orientation N)
o')
      eqOrnt Diagram t n m x
_ Diagram t' n' m' x
_ = Bool
True

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

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

-- sdgMap -


-- | mapping of some diagram.

sdgMap :: (HomOriented h, DualisableOriented s o)
  => HomDisj s o h x y -> SomeDiagram x -> SomeDiagram y
sdgMap :: forall (h :: * -> * -> *) s (o :: * -> *) x y.
(HomOriented h, DualisableOriented s o) =>
HomDisj s o h x y -> SomeDiagram x -> SomeDiagram y
sdgMap HomDisj s o h x y
h (SomeDiagram Diagram t n m x
d)   = case Diagram t n m x -> 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 x
d of
  Dual (Dual t) :~: t
Refl                    -> case HomDisj s o h x y
-> SDualBi (Diagram t n m) x -> SDualBi (Diagram t n m) y
forall x y.
HomDisj s o h x y
-> SDualBi (Diagram t n m) x -> SDualBi (Diagram t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG HomDisj s o h x y
h (Either1 (Dual1 (Diagram t n m)) (Diagram t n m) x
-> SDualBi (Diagram t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Diagram t n m x -> Either1 (Diagram (Dual t) n m) (Diagram t n m) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Diagram t n m x
d)) of
    SDualBi (Right1 Diagram t n m y
d')  -> Diagram t n m y -> SomeDiagram y
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> SomeDiagram a
SomeDiagram Diagram t n m y
d'
    SDualBi (Left1 Dual1 (Diagram t n m) y
d')   -> Diagram (Dual t) n m y -> SomeDiagram y
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> SomeDiagram a
SomeDiagram Dual1 (Diagram t n m) y
Diagram (Dual t) n m y
d'
  
instance (HomOriented h, DualisableOriented s o)
  => ApplicativeG SomeDiagram (HomDisj s o h) (->) where
  amapG :: forall x y. HomDisj s o h x y -> SomeDiagram x -> SomeDiagram y
amapG = HomDisj s o h x y -> SomeDiagram x -> SomeDiagram y
forall (h :: * -> * -> *) s (o :: * -> *) x y.
(HomOriented h, DualisableOriented s o) =>
HomDisj s o h x y -> SomeDiagram x -> SomeDiagram y
sdgMap

instance (HomOriented h, DualisableOriented s o)
  => FunctorialG SomeDiagram (HomDisj s o h) (->)

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

-- 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 -> X (X (SomeDiagram a)) -> X (SomeDiagram a)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (X (X (SomeDiagram a)) -> X (SomeDiagram a))
-> X (X (SomeDiagram a)) -> X (SomeDiagram a)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [X (SomeDiagram a)] -> X (X (SomeDiagram a))
forall a. [a] -> X a
xOneOf (XOrtSite 'To a -> X (SomeDiagram a)
forall a (x :: * -> *). Oriented a => x a -> X (SomeDiagram a)
xe XOrtSite 'To a
xToX (SomeDiagram a) -> [X (SomeDiagram a)] -> [X (SomeDiagram a)]
forall a. a -> [a] -> [a]
:W 'N0
-> XOrtSite 'To a
-> XOrtSite 'From a
-> XOrtOrientation a
-> [X (SomeDiagram 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  -> X (X (SomeDiagram a)) -> X (SomeDiagram a)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (X (X (SomeDiagram a)) -> X (SomeDiagram a))
-> X (X (SomeDiagram a)) -> X (SomeDiagram a)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [X (SomeDiagram a)] -> X (X (SomeDiagram a))
forall a. [a] -> X a
xOneOf (W n
-> XOrtSite 'To a
-> XOrtSite 'From a
-> XOrtOrientation a
-> [X (SomeDiagram a)]
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
_ = (Dual (Dual 'Empty) :~: 'Empty)
-> XDiagram 'Empty 'N0 'N0 a -> X (Diagram 'Empty 'N0 'N0 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 Dual (Dual 'Empty) :~: 'Empty
'Empty :~: 'Empty
forall {k} (a :: k). a :~: a
Refl (XDiagram 'Empty 'N0 'N0 a
forall a. XDiagram 'Empty 'N0 'N0 a
XDiagramEmpty) X (Diagram 'Empty 'N0 'N0 a)
-> (Diagram 'Empty 'N0 'N0 a -> X (SomeDiagram a))
-> X (SomeDiagram a)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SomeDiagram a -> X (SomeDiagram a)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (SomeDiagram a -> X (SomeDiagram a))
-> (Diagram 'Empty 'N0 'N0 a -> SomeDiagram a)
-> Diagram 'Empty 'N0 'N0 a
-> X (SomeDiagram 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
. Diagram 'Empty 'N0 'N0 a -> SomeDiagram a
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
    = [ Any n -> X (Point a) -> X (SomeDiagram a)
forall a (n :: N').
Oriented a =>
Any n -> X (Point a) -> X (SomeDiagram a)
xDiscrete Any n
n X (Point a)
xp
      , Any n -> XOrtSite 'To a -> X (SomeDiagram a)
forall a (n :: N').
Oriented a =>
Any n -> XOrtSite 'To a -> X (SomeDiagram a)
xChainTo Any n
n XOrtSite 'To a
xTo
      , Any n -> XOrtSite 'From a -> X (SomeDiagram a)
forall a (n :: N').
Oriented a =>
Any n -> XOrtSite 'From a -> X (SomeDiagram a)
xChainFrom Any n
n XOrtSite 'From a
xFrom
      , Any n -> XOrtOrientation a -> X (SomeDiagram a)
forall a (n :: N').
Oriented a =>
Any n -> XOrtOrientation a -> X (SomeDiagram a)
xParallelLR Any n
n XOrtOrientation a
xO
      , Any n -> XOrtOrientation a -> X (SomeDiagram a)
forall a (n :: N').
Oriented a =>
Any n -> XOrtOrientation a -> X (SomeDiagram a)
xParallelRL Any n
n XOrtOrientation a
xO
      , Any n -> XOrtSite 'To a -> X (SomeDiagram a)
forall a (n :: N').
Oriented a =>
Any n -> XOrtSite 'To a -> X (SomeDiagram a)
xSink Any n
n XOrtSite 'To a
xTo
      , Any n -> XOrtSite 'From a -> X (SomeDiagram a)
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 = XOrtOrientation a -> X (Point a)
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
    = (Diagram 'Discrete n 'N0 a -> SomeDiagram a)
-> X (Diagram 'Discrete n 'N0 a) -> X (SomeDiagram a)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Diagram 'Discrete n 'N0 a -> SomeDiagram a
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> SomeDiagram a
SomeDiagram (X (Diagram 'Discrete n 'N0 a) -> X (SomeDiagram a))
-> X (Diagram 'Discrete n 'N0 a) -> X (SomeDiagram a)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (Dual (Dual 'Discrete) :~: 'Discrete)
-> XDiagram 'Discrete n 'N0 a -> X (Diagram 'Discrete n 'N0 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 Dual (Dual 'Discrete) :~: 'Discrete
'Discrete :~: 'Discrete
forall {k} (a :: k). a :~: a
Refl (Any n -> X (Point a) -> XDiagram 'Discrete n 'N0 a
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
    = (Diagram ('Chain 'To) ('S n) n a -> SomeDiagram a)
-> X (Diagram ('Chain 'To) ('S n) n a) -> X (SomeDiagram a)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Diagram ('Chain 'To) ('S n) n a -> SomeDiagram a
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> SomeDiagram a
SomeDiagram (X (Diagram ('Chain 'To) ('S n) n a) -> X (SomeDiagram a))
-> X (Diagram ('Chain 'To) ('S n) n a) -> X (SomeDiagram a)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (Dual (Dual ('Chain 'To)) :~: 'Chain 'To)
-> XDiagram ('Chain 'To) ('S n) n a
-> X (Diagram ('Chain 'To) ('S n) n 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 Dual (Dual ('Chain 'To)) :~: 'Chain 'To
'Chain 'To :~: 'Chain 'To
forall {k} (a :: k). a :~: a
Refl (Any n -> XOrtSite 'To a -> XDiagram ('Chain 'To) (n + 1) n a
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 = (SomeDiagram (Op a) -> SomeDiagram a)
-> X (SomeDiagram (Op a)) -> X (SomeDiagram a)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (HomDisj Ort Op (HomEmpty Ort) (Op a) a
-> SomeDiagram (Op a) -> SomeDiagram a
forall (h :: * -> * -> *) s (o :: * -> *) x y.
(HomOriented h, DualisableOriented s o) =>
HomDisj s o h x y -> SomeDiagram x -> SomeDiagram y
sdgMap HomDisj Ort Op (HomEmpty Ort) (Op a) a
f) (X (SomeDiagram (Op a)) -> X (SomeDiagram a))
-> X (SomeDiagram (Op a)) -> X (SomeDiagram a)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Any n -> XOrtSite 'To (Op a) -> X (SomeDiagram (Op a))
forall a (n :: N').
Oriented a =>
Any n -> XOrtSite 'To a -> X (SomeDiagram a)
xChainTo Any n
n (XOrtSite 'From a -> Dual (XOrtSite 'From a)
forall (s :: Site) q. XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite XOrtSite 'From a
xFrom) where
    Contravariant2 (Inv2 HomDisjEmpty Ort Op a (Op a)
_ HomDisj Ort Op (HomEmpty Ort) (Op a) a
f) = Variant2 'Contravariant (IsoO Ort Op) a (Op a)
forall x.
Oriented x =>
Variant2 'Contravariant (IsoO Ort Op) x (Op x)
toDualOpOrt
  
  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 = (Diagram ('Parallel 'LeftToRight) ('S N1) n a -> SomeDiagram a)
-> X (Diagram ('Parallel 'LeftToRight) ('S N1) n a)
-> X (SomeDiagram a)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Diagram ('Parallel 'LeftToRight) ('S N1) n a -> SomeDiagram a
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> SomeDiagram a
SomeDiagram (X (Diagram ('Parallel 'LeftToRight) ('S N1) n a)
 -> X (SomeDiagram a))
-> X (Diagram ('Parallel 'LeftToRight) ('S N1) n a)
-> X (SomeDiagram a)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (Dual (Dual ('Parallel 'LeftToRight)) :~: 'Parallel 'LeftToRight)
-> XDiagram ('Parallel 'LeftToRight) ('S N1) n a
-> X (Diagram ('Parallel 'LeftToRight) ('S N1) n 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 Dual (Dual ('Parallel 'LeftToRight)) :~: 'Parallel 'LeftToRight
'Parallel 'LeftToRight :~: 'Parallel 'LeftToRight
forall {k} (a :: k). a :~: a
Refl (Any n
-> XOrtOrientation a
-> XDiagram ('Parallel 'LeftToRight) ('S N1) n a
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 = (SomeDiagram (Op a) -> SomeDiagram a)
-> X (SomeDiagram (Op a)) -> X (SomeDiagram a)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (HomDisj Ort Op (HomEmpty Ort) (Op a) a
-> SomeDiagram (Op a) -> SomeDiagram a
forall (h :: * -> * -> *) s (o :: * -> *) x y.
(HomOriented h, DualisableOriented s o) =>
HomDisj s o h x y -> SomeDiagram x -> SomeDiagram y
sdgMap HomDisj Ort Op (HomEmpty Ort) (Op a) a
f) (X (SomeDiagram (Op a)) -> X (SomeDiagram a))
-> X (SomeDiagram (Op a)) -> X (SomeDiagram a)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Any n -> XOrtOrientation (Op a) -> X (SomeDiagram (Op a))
forall a (n :: N').
Oriented a =>
Any n -> XOrtOrientation a -> X (SomeDiagram a)
xParallelLR Any n
n (XOrtOrientation a -> Dual (XOrtOrientation a)
forall q. XOrtOrientation q -> Dual (XOrtOrientation q)
coXOrtOrientation XOrtOrientation a
xO) where
    Contravariant2 (Inv2 HomDisjEmpty Ort Op a (Op a)
_ HomDisj Ort Op (HomEmpty Ort) (Op a) a
f) = Variant2 'Contravariant (IsoO Ort Op) a (Op a)
forall x.
Oriented x =>
Variant2 'Contravariant (IsoO Ort Op) x (Op x)
toDualOpOrt
    
  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 = (Diagram ('Star 'To) ('S n) n a -> SomeDiagram a)
-> X (Diagram ('Star 'To) ('S n) n a) -> X (SomeDiagram a)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Diagram ('Star 'To) ('S n) n a -> SomeDiagram a
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> SomeDiagram a
SomeDiagram (X (Diagram ('Star 'To) ('S n) n a) -> X (SomeDiagram a))
-> X (Diagram ('Star 'To) ('S n) n a) -> X (SomeDiagram a)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (Dual (Dual ('Star 'To)) :~: 'Star 'To)
-> XDiagram ('Star 'To) ('S n) n a
-> X (Diagram ('Star 'To) ('S n) n 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 Dual (Dual ('Star 'To)) :~: 'Star 'To
'Star 'To :~: 'Star 'To
forall {k} (a :: k). a :~: a
Refl (Any n -> XOrtSite 'To a -> XDiagram ('Star 'To) (n + 1) n a
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 = (SomeDiagram (Op a) -> SomeDiagram a)
-> X (SomeDiagram (Op a)) -> X (SomeDiagram a)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (HomDisj Ort Op (HomEmpty Ort) (Op a) a
-> SomeDiagram (Op a) -> SomeDiagram a
forall (h :: * -> * -> *) s (o :: * -> *) x y.
(HomOriented h, DualisableOriented s o) =>
HomDisj s o h x y -> SomeDiagram x -> SomeDiagram y
sdgMap HomDisj Ort Op (HomEmpty Ort) (Op a) a
f) (X (SomeDiagram (Op a)) -> X (SomeDiagram a))
-> X (SomeDiagram (Op a)) -> X (SomeDiagram a)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Any n -> XOrtSite 'To (Op a) -> X (SomeDiagram (Op a))
forall a (n :: N').
Oriented a =>
Any n -> XOrtSite 'To a -> X (SomeDiagram a)
xSink Any n
n (XOrtSite 'From a -> Dual (XOrtSite 'From a)
forall (s :: Site) q. XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite XOrtSite 'From a
xFrom) where
    Contravariant2 (Inv2 HomDisjEmpty Ort Op a (Op a)
_ HomDisj Ort Op (HomEmpty Ort) (Op a) a
f) = Variant2 'Contravariant (IsoO Ort Op) a (Op a)
forall x.
Oriented x =>
Variant2 'Contravariant (IsoO Ort Op) x (Op x)
toDualOpOrt

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

-- 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 = (SomeDiagram a -> [String]) -> Int -> X (SomeDiagram a) -> IO ()
forall x. (x -> [String]) -> Int -> X x -> IO ()
putDstr SomeDiagram a -> [String]
forall {a}. (ShowPoint a, Show a) => SomeDiagram a -> [String]
cnstr Int
n X (SomeDiagram a)
xd where
  cnstr :: SomeDiagram a -> [String]
cnstr (SomeDiagram Diagram t n m a
a) = [Diagram t n m a -> String
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
  = X SomeNatural
-> XOrtSite 'To (Orientation p)
-> XOrtSite 'From (Orientation p)
-> XOrtOrientation (Orientation p)
-> X (SomeDiagram (Orientation p))
forall a.
Oriented a =>
X SomeNatural
-> XOrtSite 'To a
-> XOrtSite 'From a
-> XOrtOrientation a
-> X (SomeDiagram a)
xSomeDiagram X SomeNatural
xn (X p -> XOrtSite 'To (Orientation p)
forall p. X p -> XOrtSite 'To (Orientation p)
xEndOrnt X p
xp) (X p -> XOrtSite 'From (Orientation p)
forall p. X p -> XOrtSite 'From (Orientation p)
xStartOrnt X p
xp) (X p -> XOrtOrientation (Orientation p)
forall p. X p -> XOrtOrientation (Orientation p)
xoOrnt X p
xp)

xsd :: X (SomeDiagram OS)
xsd :: X (SomeDiagram OS)
xsd = X SomeNatural -> X Symbol -> X (SomeDiagram OS)
forall p.
Entity p =>
X SomeNatural -> X p -> X (SomeDiagram (Orientation p))
xSomeDiagramOrnt X SomeNatural
xn X Symbol
forall x. XStandard x => X x
xStandard where xn :: X SomeNatural
xn = (N -> SomeNatural) -> X N -> X SomeNatural
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 N -> SomeNatural
someNatural (X N -> X SomeNatural) -> X N -> X SomeNatural
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> N -> X N
xNB N
0 N
20