{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Tools.Diagrams.Dot where

import Data.Bifunctor (first)
import Data.Coerce (coerce)
import Data.List (cycle, repeat, sort)
import Data.Proxy (Proxy (..))
import GHC.TypeLits (KnownSymbol, Symbol, symbolVal)
import Prelude
  ( Bool (..)
  , Either (..)
  , Eq (..)
  , Foldable
  , Functor (..)
  , Int
  , Num (..)
  , Ord (..)
  , Show
  , String
  , Traversable (..)
  , const
  , either
  , foldMap
  , show
  , snd
  , splitAt
  , zip
  , zip3
  , (!!)
  , ($)
  , (++)
  )

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.Action (Costrong (..), MonoidalAction (..), Strong (..))
import Proarrow.Category.Monoidal.Strictified (IsList (..), SList (..), type (++))
import Proarrow.Core (CAT, CategoryOf (..), Is, Kind, Profunctor (..), Promonad (..), UN, dimapDefault, obj)
import Proarrow.Monoid (Comonoid (..), CopyDiscard, Monoid (..))
import Proarrow.Profunctor.Identity (Id (..))

type Port = String -- Basically a shown int, but may contain an additional direction (:n, :e, :s, :w)

newtype Vec as x = Vec {forall {k} (as :: k) x. Vec as x -> [x]
unVec :: [x]}
  deriving newtype (Int -> Vec as x -> ShowS
[Vec as x] -> ShowS
Vec as x -> String
(Int -> Vec as x -> ShowS)
-> (Vec as x -> String) -> ([Vec as x] -> ShowS) -> Show (Vec as x)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (as :: k) x. Show x => Int -> Vec as x -> ShowS
forall k (as :: k) x. Show x => [Vec as x] -> ShowS
forall k (as :: k) x. Show x => Vec as x -> String
$cshowsPrec :: forall k (as :: k) x. Show x => Int -> Vec as x -> ShowS
showsPrec :: Int -> Vec as x -> ShowS
$cshow :: forall k (as :: k) x. Show x => Vec as x -> String
show :: Vec as x -> String
$cshowList :: forall k (as :: k) x. Show x => [Vec as x] -> ShowS
showList :: [Vec as x] -> ShowS
Show, Vec as x -> Vec as x -> Bool
(Vec as x -> Vec as x -> Bool)
-> (Vec as x -> Vec as x -> Bool) -> Eq (Vec as x)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (as :: k) x. Eq x => Vec as x -> Vec as x -> Bool
$c== :: forall k (as :: k) x. Eq x => Vec as x -> Vec as x -> Bool
== :: Vec as x -> Vec as x -> Bool
$c/= :: forall k (as :: k) x. Eq x => Vec as x -> Vec as x -> Bool
/= :: Vec as x -> Vec as x -> Bool
Eq, (forall m. Monoid m => Vec as m -> m)
-> (forall m a. Monoid m => (a -> m) -> Vec as a -> m)
-> (forall m a. Monoid m => (a -> m) -> Vec as a -> m)
-> (forall a b. (a -> b -> b) -> b -> Vec as a -> b)
-> (forall a b. (a -> b -> b) -> b -> Vec as a -> b)
-> (forall b a. (b -> a -> b) -> b -> Vec as a -> b)
-> (forall b a. (b -> a -> b) -> b -> Vec as a -> b)
-> (forall a. (a -> a -> a) -> Vec as a -> a)
-> (forall a. (a -> a -> a) -> Vec as a -> a)
-> (forall a. Vec as a -> [a])
-> (forall a. Vec as a -> Bool)
-> (forall a. Vec as a -> Int)
-> (forall a. Eq a => a -> Vec as a -> Bool)
-> (forall a. Ord a => Vec as a -> a)
-> (forall a. Ord a => Vec as a -> a)
-> (forall a. Num a => Vec as a -> a)
-> (forall a. Num a => Vec as a -> a)
-> Foldable (Vec as)
forall a. Eq a => a -> Vec as a -> Bool
forall a. Num a => Vec as a -> a
forall a. Ord a => Vec as a -> a
forall m. Monoid m => Vec as m -> m
forall a. Vec as a -> Bool
forall a. Vec as a -> Int
forall a. Vec as a -> [a]
forall a. (a -> a -> a) -> Vec as a -> a
forall k (as :: k) a. Eq a => a -> Vec as a -> Bool
forall k (as :: k) a. Num a => Vec as a -> a
forall k (as :: k) a. Ord a => Vec as a -> a
forall k (as :: k) m. Monoid m => Vec as m -> m
forall k (as :: k) a. Vec as a -> Bool
forall k (as :: k) a. Vec as a -> Int
forall {k} (as :: k) x. Vec as x -> [x]
forall k (as :: k) a. (a -> a -> a) -> Vec as a -> a
forall k (as :: k) m a. Monoid m => (a -> m) -> Vec as a -> m
forall k (as :: k) b a. (b -> a -> b) -> b -> Vec as a -> b
forall k (as :: k) a b. (a -> b -> b) -> b -> Vec as a -> b
forall m a. Monoid m => (a -> m) -> Vec as a -> m
forall b a. (b -> a -> b) -> b -> Vec as a -> b
forall a b. (a -> b -> b) -> b -> Vec as a -> b
forall (t :: Type -> Type).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall k (as :: k) m. Monoid m => Vec as m -> m
fold :: forall m. Monoid m => Vec as m -> m
$cfoldMap :: forall k (as :: k) m a. Monoid m => (a -> m) -> Vec as a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Vec as a -> m
$cfoldMap' :: forall k (as :: k) m a. Monoid m => (a -> m) -> Vec as a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Vec as a -> m
$cfoldr :: forall k (as :: k) a b. (a -> b -> b) -> b -> Vec as a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Vec as a -> b
$cfoldr' :: forall k (as :: k) a b. (a -> b -> b) -> b -> Vec as a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Vec as a -> b
$cfoldl :: forall k (as :: k) b a. (b -> a -> b) -> b -> Vec as a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Vec as a -> b
$cfoldl' :: forall k (as :: k) b a. (b -> a -> b) -> b -> Vec as a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Vec as a -> b
$cfoldr1 :: forall k (as :: k) a. (a -> a -> a) -> Vec as a -> a
foldr1 :: forall a. (a -> a -> a) -> Vec as a -> a
$cfoldl1 :: forall k (as :: k) a. (a -> a -> a) -> Vec as a -> a
foldl1 :: forall a. (a -> a -> a) -> Vec as a -> a
$ctoList :: forall {k} (as :: k) x. Vec as x -> [x]
toList :: forall a. Vec as a -> [a]
$cnull :: forall k (as :: k) a. Vec as a -> Bool
null :: forall a. Vec as a -> Bool
$clength :: forall k (as :: k) a. Vec as a -> Int
length :: forall a. Vec as a -> Int
$celem :: forall k (as :: k) a. Eq a => a -> Vec as a -> Bool
elem :: forall a. Eq a => a -> Vec as a -> Bool
$cmaximum :: forall k (as :: k) a. Ord a => Vec as a -> a
maximum :: forall a. Ord a => Vec as a -> a
$cminimum :: forall k (as :: k) a. Ord a => Vec as a -> a
minimum :: forall a. Ord a => Vec as a -> a
$csum :: forall k (as :: k) a. Num a => Vec as a -> a
sum :: forall a. Num a => Vec as a -> a
$cproduct :: forall k (as :: k) a. Num a => Vec as a -> a
product :: forall a. Num a => Vec as a -> a
Foldable, (forall a b. (a -> b) -> Vec as a -> Vec as b)
-> (forall a b. a -> Vec as b -> Vec as a) -> Functor (Vec as)
forall k (as :: k) a b. a -> Vec as b -> Vec as a
forall k (as :: k) a b. (a -> b) -> Vec as a -> Vec as b
forall a b. a -> Vec as b -> Vec as a
forall a b. (a -> b) -> Vec as a -> Vec as b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall k (as :: k) a b. (a -> b) -> Vec as a -> Vec as b
fmap :: forall a b. (a -> b) -> Vec as a -> Vec as b
$c<$ :: forall k (as :: k) a b. a -> Vec as b -> Vec as a
<$ :: forall a b. a -> Vec as b -> Vec as a
Functor)
instance Traversable (Vec as) where
  traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vec as a -> f (Vec as b)
traverse a -> f b
f (Vec [a]
xs) = ([b] -> Vec as b) -> f [b] -> f (Vec as b)
forall a b. (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap [b] -> Vec as b
forall {k} (as :: k) x. [x] -> Vec as x
Vec ((a -> f b) -> [a] -> f [b]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> f b
f [a]
xs)
newtype Fin as = Fin {forall {k} (as :: k). Fin as -> Int
unFin :: Int}
  deriving newtype (Int -> Fin as -> ShowS
[Fin as] -> ShowS
Fin as -> String
(Int -> Fin as -> ShowS)
-> (Fin as -> String) -> ([Fin as] -> ShowS) -> Show (Fin as)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (as :: k). Int -> Fin as -> ShowS
forall k (as :: k). [Fin as] -> ShowS
forall k (as :: k). Fin as -> String
$cshowsPrec :: forall k (as :: k). Int -> Fin as -> ShowS
showsPrec :: Int -> Fin as -> ShowS
$cshow :: forall k (as :: k). Fin as -> String
show :: Fin as -> String
$cshowList :: forall k (as :: k). [Fin as] -> ShowS
showList :: [Fin as] -> ShowS
Show, Fin as -> Fin as -> Bool
(Fin as -> Fin as -> Bool)
-> (Fin as -> Fin as -> Bool) -> Eq (Fin as)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (as :: k). Fin as -> Fin as -> Bool
$c== :: forall k (as :: k). Fin as -> Fin as -> Bool
== :: Fin as -> Fin as -> Bool
$c/= :: forall k (as :: k). Fin as -> Fin as -> Bool
/= :: Fin as -> Fin as -> Bool
Eq, Integer -> Fin as
Fin as -> Fin as
Fin as -> Fin as -> Fin as
(Fin as -> Fin as -> Fin as)
-> (Fin as -> Fin as -> Fin as)
-> (Fin as -> Fin as -> Fin as)
-> (Fin as -> Fin as)
-> (Fin as -> Fin as)
-> (Fin as -> Fin as)
-> (Integer -> Fin as)
-> Num (Fin as)
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
forall k (as :: k). Integer -> Fin as
forall k (as :: k). Fin as -> Fin as
forall k (as :: k). Fin as -> Fin as -> Fin as
$c+ :: forall k (as :: k). Fin as -> Fin as -> Fin as
+ :: Fin as -> Fin as -> Fin as
$c- :: forall k (as :: k). Fin as -> Fin as -> Fin as
- :: Fin as -> Fin as -> Fin as
$c* :: forall k (as :: k). Fin as -> Fin as -> Fin as
* :: Fin as -> Fin as -> Fin as
$cnegate :: forall k (as :: k). Fin as -> Fin as
negate :: Fin as -> Fin as
$cabs :: forall k (as :: k). Fin as -> Fin as
abs :: Fin as -> Fin as
$csignum :: forall k (as :: k). Fin as -> Fin as
signum :: Fin as -> Fin as
$cfromInteger :: forall k (as :: k). Integer -> Fin as
fromInteger :: Integer -> Fin as
Num)
(!) :: Vec as x -> Fin as -> x
Vec [x]
xs ! :: forall {k} (as :: k) x. Vec as x -> Fin as -> x
! Fin Int
i = [x]
xs [x] -> Int -> x
forall a. HasCallStack => [a] -> Int -> a
!! Int
i

(+++) :: Vec as x -> Vec bs x -> Vec (as ++ bs) x
Vec [x]
xs +++ :: forall {k} (as :: [k]) x (bs :: [k]).
Vec as x -> Vec bs x -> Vec (as ++ bs) x
+++ Vec [x]
ys = [x] -> Vec (as ++ bs) x
forall {k} (as :: k) x. [x] -> Vec as x
Vec ([x]
xs [x] -> [x] -> [x]
forall a. [a] -> [a] -> [a]
++ [x]
ys)

split :: (IsList as) => Vec (as ++ bs) x -> (Vec as x, Vec bs x)
split :: forall {k} (as :: [k]) (bs :: [k]) x.
IsList as =>
Vec (as ++ bs) x -> (Vec as x, Vec bs x)
split @as (Vec [x]
xs) = case Int -> [x] -> ([x], [x])
forall a. Int -> [a] -> ([a], [a])
splitAt (forall (as :: [k]). IsList as => Int
forall {k} (as :: [k]). IsList as => Int
len @as) [x]
xs of ([x]
as, [x]
bs) -> ([x] -> Vec as x
forall {k} (as :: k) x. [x] -> Vec as x
Vec [x]
as, [x] -> Vec bs x
forall {k} (as :: k) x. [x] -> Vec as x
Vec [x]
bs)

len :: (IsList as) => Int
len :: forall {k} (as :: [k]). IsList as => Int
len @as = case forall (as :: [k]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
sList @as of
  SList as
SNil -> Int
0
  SList as
SSing -> Int
1
  SCons @_ @bs -> Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ forall (as :: [k]). IsList as => Int
forall {k} (as :: [k]). IsList as => Int
len @bs

ixs :: (IsList as) => Vec as (Fin as)
ixs :: forall {k} (as :: [k]). IsList as => Vec as (Fin as)
ixs @as = case forall (as :: [k]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
sList @as of
  SList as
SNil -> [Fin as] -> Vec as (Fin as)
forall {k} (as :: k) x. [x] -> Vec as x
Vec []
  SList as
SSing -> [Fin as] -> Vec as (Fin as)
forall {k} (as :: k) x. [x] -> Vec as x
Vec [Item [Fin as]
Fin '[a1]
0]
  SCons @_ @bs -> [Fin as1] -> Vec as (Fin as)
forall a b. Coercible a b => a -> b
coerce (Fin as1
0 Fin as1 -> [Fin as1] -> [Fin as1]
forall a. a -> [a] -> [a]
: (Fin as1 -> Fin as1) -> [Fin as1] -> [Fin as1]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Fin as1 -> Fin as1 -> Fin as1
forall a. Num a => a -> a -> a
+ Fin as1
1) (Vec as1 (Fin as1) -> [Fin as1]
forall {k} (as :: k) x. Vec as x -> [x]
unVec (forall (as :: [k]). IsList as => Vec as (Fin as)
forall {k} (as :: [k]). IsList as => Vec as (Fin as)
ixs @bs)))

ixed :: (IsList as) => Vec as x -> Vec as (Fin as, x)
ixed :: forall {k} (as :: [k]) x.
IsList as =>
Vec as x -> Vec as (Fin as, x)
ixed (Vec []) = [(Fin as, x)] -> Vec as (Fin as, x)
forall {k} (as :: k) x. [x] -> Vec as x
Vec []
ixed (Vec (x
x : [x]
xs)) = [(Fin as, x)] -> Vec as (Fin as, x)
forall {k} (as :: k) x. [x] -> Vec as x
Vec ([(Fin as, x)] -> Vec as (Fin as, x))
-> [(Fin as, x)] -> Vec as (Fin as, x)
forall a b. (a -> b) -> a -> b
$ (Fin as
0, x
x) (Fin as, x) -> [(Fin as, x)] -> [(Fin as, x)]
forall a. a -> [a] -> [a]
: ((Fin as, x) -> (Fin as, x)) -> [(Fin as, x)] -> [(Fin as, x)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Fin as
i, x
y) -> (Fin as
i Fin as -> Fin as -> Fin as
forall a. Num a => a -> a -> a
+ Fin as
1, x
y)) (Vec as (Fin as, x) -> [(Fin as, x)]
forall {k} (as :: k) x. Vec as x -> [x]
unVec (Vec as x -> Vec as (Fin as, x)
forall {k} (as :: [k]) x.
IsList as =>
Vec as x -> Vec as (Fin as, x)
ixed ([x] -> Vec as x
forall {k} (as :: k) x. [x] -> Vec as x
Vec [x]
xs)))

zipV3 :: Vec as x -> Vec as y -> Vec as z -> Vec as (x, y, z)
zipV3 :: forall {k} (as :: k) x y z.
Vec as x -> Vec as y -> Vec as z -> Vec as (x, y, z)
zipV3 (Vec [x]
xs) (Vec [y]
ys) (Vec [z]
zs) = [(x, y, z)] -> Vec as (x, y, z)
forall {k} (as :: k) x. [x] -> Vec as x
Vec ([x] -> [y] -> [z] -> [(x, y, z)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [x]
xs [y]
ys [z]
zs)

relax :: forall bs as. Fin as -> Fin (as ++ bs)
relax :: forall {k} (bs :: [k]) (as :: [k]). Fin as -> Fin (as ++ bs)
relax (Fin Int
i) = Int -> Fin (as ++ bs)
forall {k} (as :: k). Int -> Fin as
Fin Int
i

shift :: forall as bs. (IsList as) => Fin bs -> Fin (as ++ bs)
shift :: forall {k} (as :: [k]) (bs :: [k]).
IsList as =>
Fin bs -> Fin (as ++ bs)
shift (Fin Int
i) = Int -> Fin (as ++ bs)
forall {k} (as :: k). Int -> Fin as
Fin (forall (as :: [k]). IsList as => Int
forall {k} (as :: [k]). IsList as => Int
len @as Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i)

eitherF :: forall as bs r. (IsList as) => (Fin as -> r) -> (Fin bs -> r) -> Fin (as ++ bs) -> r
eitherF :: forall {k} (as :: [k]) (bs :: [k]) r.
IsList as =>
(Fin as -> r) -> (Fin bs -> r) -> Fin (as ++ bs) -> r
eitherF Fin as -> r
f Fin bs -> r
g (Fin Int
i)
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< forall (as :: [k]). IsList as => Int
forall {k} (as :: [k]). IsList as => Int
len @as = Fin as -> r
f (Int -> Fin as
forall {k} (as :: k). Int -> Fin as
Fin Int
i)
  | Bool
True = Fin bs -> r
g (Int -> Fin bs
forall {k} (as :: k). Int -> Fin as
Fin (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- forall (as :: [k]). IsList as => Int
forall {k} (as :: [k]). IsList as => Int
len @as))

names :: (IsList (as :: [Symbol])) => Vec as String
names :: forall (as :: [Symbol]). IsList as => Vec as String
names @as = case forall (as :: [Symbol]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
sList @as of
  SList as
SNil -> [String] -> Vec as String
forall {k} (as :: k) x. [x] -> Vec as x
Vec []
  SSing @s -> [String] -> Vec as String
forall {k} (as :: k) x. [x] -> Vec as x
Vec [Proxy a1 -> String
forall (n :: Symbol) (proxy :: Symbol -> Type).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @s)]
  SCons @s @ss -> [String] -> Vec as String
forall {k} (as :: k) x. [x] -> Vec as x
Vec (Proxy a1 -> String
forall (n :: Symbol) (proxy :: Symbol -> Type).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @s) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: Vec as1 String -> [String]
forall {k} (as :: k) x. Vec as x -> [x]
unVec (forall (as :: [Symbol]). IsList as => Vec as String
names @ss))

type SymRefl :: CAT Symbol
data SymRefl a b where
  SymRefl :: (KnownSymbol s) => SymRefl s s
instance Eq (SymRefl a b) where
  SymRefl a b
SymRefl == :: SymRefl a b -> SymRefl a b -> Bool
== SymRefl a b
SymRefl = Bool
True
instance Show (SymRefl a b) where
  show :: SymRefl a b -> String
show SymRefl a b
SymRefl = String
"SymRefl"
instance Profunctor SymRefl where
  dimap :: forall (c :: Symbol) (a :: Symbol) (b :: Symbol) (d :: Symbol).
(c ~> a) -> (b ~> d) -> SymRefl a b -> SymRefl c d
dimap = (c ~> a) -> (b ~> d) -> SymRefl a b -> SymRefl c d
SymRefl c a -> SymRefl b d -> SymRefl a b -> SymRefl c d
forall {k} (p :: k +-> k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: Symbol) (b :: Symbol) r.
((Ob a, Ob b) => r) -> SymRefl a b -> r
\\ SymRefl a b
SymRefl = r
(Ob a, Ob b) => r
r
instance Promonad SymRefl where
  id :: forall (a :: Symbol). Ob a => SymRefl a a
id = SymRefl a a
forall (s :: Symbol). KnownSymbol s => SymRefl s s
SymRefl
  SymRefl b c
SymRefl . :: forall (b :: Symbol) (c :: Symbol) (a :: Symbol).
SymRefl b c -> SymRefl a b -> SymRefl a c
. SymRefl a b
SymRefl = SymRefl a c
SymRefl a a
forall (s :: Symbol). KnownSymbol s => SymRefl s s
SymRefl
instance CategoryOf Symbol where
  type (~>) = SymRefl
  type Ob s = KnownSymbol s

type DOT :: Kind
type data DOT = D [Symbol]
type instance UN D (D ss) = ss

data DotData as bs = DotData
  { forall {k} {k} (as :: k) (bs :: k).
DotData as bs -> Vec as (Either (Fin bs) String)
inputs :: Vec as (Either (Fin bs) Port)
  , forall {k} {k} (as :: k) (bs :: k).
DotData as bs -> Vec bs (Either (Fin as) String)
outputs :: Vec bs (Either (Fin as) Port)
  , forall {k} {k} (as :: k) (bs :: k).
DotData as bs -> [(String, String, String)]
edges :: [(Port, String, Port)]
  , forall {k} {k} (as :: k) (bs :: k). DotData as bs -> [String]
nodeOpts :: [String]
  }
  deriving (Int -> DotData as bs -> ShowS
[DotData as bs] -> ShowS
DotData as bs -> String
(Int -> DotData as bs -> ShowS)
-> (DotData as bs -> String)
-> ([DotData as bs] -> ShowS)
-> Show (DotData as bs)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (as :: k) k (bs :: k). Int -> DotData as bs -> ShowS
forall k (as :: k) k (bs :: k). [DotData as bs] -> ShowS
forall k (as :: k) k (bs :: k). DotData as bs -> String
$cshowsPrec :: forall k (as :: k) k (bs :: k). Int -> DotData as bs -> ShowS
showsPrec :: Int -> DotData as bs -> ShowS
$cshow :: forall k (as :: k) k (bs :: k). DotData as bs -> String
show :: DotData as bs -> String
$cshowList :: forall k (as :: k) k (bs :: k). [DotData as bs] -> ShowS
showList :: [DotData as bs] -> ShowS
Show, DotData as bs -> DotData as bs -> Bool
(DotData as bs -> DotData as bs -> Bool)
-> (DotData as bs -> DotData as bs -> Bool) -> Eq (DotData as bs)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (as :: k) k (bs :: k).
DotData as bs -> DotData as bs -> Bool
$c== :: forall k (as :: k) k (bs :: k).
DotData as bs -> DotData as bs -> Bool
== :: DotData as bs -> DotData as bs -> Bool
$c/= :: forall k (as :: k) k (bs :: k).
DotData as bs -> DotData as bs -> Bool
/= :: DotData as bs -> DotData as bs -> Bool
Eq)

type Dot :: CAT DOT
data Dot a b where
  Dot :: (IsList as, IsList bs) => (Int -> (Int, DotData as bs)) -> Dot (D as) (D bs)

instance Eq (Dot a b) where
  Dot Int -> (Int, DotData as bs)
f == :: Dot a b -> Dot a b -> Bool
== Dot Int -> (Int, DotData as bs)
g = DotData as bs -> DotData as bs
forall {k} {k} (as :: k) (bs :: k). DotData as bs -> DotData as bs
normalize (Dot (D as) (D bs) -> DotData as bs
forall (as :: [Symbol]) (bs :: [Symbol]).
Dot (D as) (D bs) -> DotData as bs
getData ((Int -> (Int, DotData as bs)) -> Dot (D as) (D bs)
forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
(Int -> (Int, DotData as bs)) -> Dot (D as) (D bs)
Dot Int -> (Int, DotData as bs)
f)) DotData as bs -> DotData as bs -> Bool
forall a. Eq a => a -> a -> Bool
== DotData as bs -> DotData as bs
forall {k} {k} (as :: k) (bs :: k). DotData as bs -> DotData as bs
normalize (Dot (D as) (D bs) -> DotData as bs
forall (as :: [Symbol]) (bs :: [Symbol]).
Dot (D as) (D bs) -> DotData as bs
getData ((Int -> (Int, DotData as bs)) -> Dot (D as) (D bs)
forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
(Int -> (Int, DotData as bs)) -> Dot (D as) (D bs)
Dot Int -> (Int, DotData as bs)
Int -> (Int, DotData as bs)
g))
instance Show (Dot a b) where
  show :: Dot a b -> String
show (Dot Int -> (Int, DotData as bs)
f) = DotData as bs -> String
forall a. Show a => a -> String
show (Dot (D as) (D bs) -> DotData as bs
forall (as :: [Symbol]) (bs :: [Symbol]).
Dot (D as) (D bs) -> DotData as bs
getData ((Int -> (Int, DotData as bs)) -> Dot (D as) (D bs)
forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
(Int -> (Int, DotData as bs)) -> Dot (D as) (D bs)
Dot Int -> (Int, DotData as bs)
f))

instance Profunctor Dot where
  dimap :: forall (c :: DOT) (a :: DOT) (b :: DOT) (d :: DOT).
(c ~> a) -> (b ~> d) -> Dot a b -> Dot c d
dimap = (c ~> a) -> (b ~> d) -> Dot a b -> Dot c d
Dot c a -> Dot b d -> Dot a b -> Dot c d
forall {k} (p :: k +-> k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: DOT) (b :: DOT) r. ((Ob a, Ob b) => r) -> Dot a b -> r
\\ Dot{} = r
(Ob a, Ob b) => r
r
instance Promonad Dot where
  id :: forall (a :: DOT). Ob a => Dot a a
id @(D as) = (Int -> (Int, DotData (UN D a) (UN D a)))
-> Dot (D (UN D a)) (D (UN D a))
forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
(Int -> (Int, DotData as bs)) -> Dot (D as) (D bs)
Dot \Int
n ->
    ( Int
n
    , DotData
        { inputs :: Vec (UN D a) (Either (Fin (UN D a)) String)
inputs = (Fin (UN D a) -> Either (Fin (UN D a)) String)
-> Vec (UN D a) (Fin (UN D a))
-> Vec (UN D a) (Either (Fin (UN D a)) String)
forall a b. (a -> b) -> Vec (UN D a) a -> Vec (UN D a) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Fin (UN D a) -> Either (Fin (UN D a)) String
forall a b. a -> Either a b
Left (forall (as :: [Symbol]). IsList as => Vec as (Fin as)
forall {k} (as :: [k]). IsList as => Vec as (Fin as)
ixs @as)
        , outputs :: Vec (UN D a) (Either (Fin (UN D a)) String)
outputs = (Fin (UN D a) -> Either (Fin (UN D a)) String)
-> Vec (UN D a) (Fin (UN D a))
-> Vec (UN D a) (Either (Fin (UN D a)) String)
forall a b. (a -> b) -> Vec (UN D a) a -> Vec (UN D a) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Fin (UN D a) -> Either (Fin (UN D a)) String
forall a b. a -> Either a b
Left (forall (as :: [Symbol]). IsList as => Vec as (Fin as)
forall {k} (as :: [k]). IsList as => Vec as (Fin as)
ixs @as)
        , edges :: [(String, String, String)]
edges = []
        , nodeOpts :: [String]
nodeOpts = []
        }
    )
  Dot @bs Int -> (Int, DotData as bs)
l . :: forall (b :: DOT) (c :: DOT) (a :: DOT).
Dot b c -> Dot a b -> Dot a c
. Dot Int -> (Int, DotData as bs)
r = (Int -> (Int, DotData as bs)) -> Dot (D as) (D bs)
forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
(Int -> (Int, DotData as bs)) -> Dot (D as) (D bs)
Dot \Int
i ->
    let (Int
k, DotData Vec as (Either (Fin bs) String)
li Vec bs (Either (Fin as) String)
lo [(String, String, String)]
le [String]
ln) = Int -> (Int, DotData as bs)
l Int
j; (Int
j, DotData Vec as (Either (Fin bs) String)
ri Vec bs (Either (Fin as) String)
ro [(String, String, String)]
re [String]
rn) = Int -> (Int, DotData as bs)
r Int
i
    in ( Int
k
       , DotData
           { inputs :: Vec as (Either (Fin bs) String)
inputs = (Either (Fin as) String -> Either (Fin bs) String)
-> Vec as (Either (Fin as) String)
-> Vec as (Either (Fin bs) String)
forall a b. (a -> b) -> Vec as a -> Vec as b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Fin as -> Either (Fin bs) String)
-> (String -> Either (Fin bs) String)
-> Either (Fin as) String
-> Either (Fin bs) String
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Vec as (Either (Fin bs) String)
li Vec as (Either (Fin bs) String) -> Fin as -> Either (Fin bs) String
forall {k} (as :: k) x. Vec as x -> Fin as -> x
!) String -> Either (Fin bs) String
forall a b. b -> Either a b
Right) Vec as (Either (Fin as) String)
Vec as (Either (Fin bs) String)
ri
           , outputs :: Vec bs (Either (Fin as) String)
outputs = (Either (Fin bs) String -> Either (Fin as) String)
-> Vec bs (Either (Fin bs) String)
-> Vec bs (Either (Fin as) String)
forall a b. (a -> b) -> Vec bs a -> Vec bs b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Fin bs -> Either (Fin as) String)
-> (String -> Either (Fin as) String)
-> Either (Fin bs) String
-> Either (Fin as) String
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Vec bs (Either (Fin as) String)
ro Vec bs (Either (Fin as) String) -> Fin bs -> Either (Fin as) String
forall {k} (as :: k) x. Vec as x -> Fin as -> x
!) String -> Either (Fin as) String
forall a b. b -> Either a b
Right) Vec bs (Either (Fin as) String)
Vec bs (Either (Fin bs) String)
lo
           , edges :: [(String, String, String)]
edges = [(String, String, String)]
re [(String, String, String)]
-> [(String, String, String)] -> [(String, String, String)]
forall a. [a] -> [a] -> [a]
++ ((Either (Fin as) String, String, Either (Fin bs) String)
 -> [(String, String, String)])
-> Vec bs (Either (Fin as) String, String, Either (Fin bs) String)
-> [(String, String, String)]
forall m a. Monoid m => (a -> m) -> Vec bs a -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\case (Right String
n1, String
n, Right String
n2) -> [(String
n1, String
n, String
n2)]; (Either (Fin as) String, String, Either (Fin bs) String)
_ -> []) (Vec bs (Either (Fin as) String)
-> Vec bs String
-> Vec bs (Either (Fin bs) String)
-> Vec bs (Either (Fin as) String, String, Either (Fin bs) String)
forall {k} (as :: k) x y z.
Vec as x -> Vec as y -> Vec as z -> Vec as (x, y, z)
zipV3 Vec bs (Either (Fin as) String)
ro (forall (as :: [Symbol]). IsList as => Vec as String
names @bs) Vec as (Either (Fin bs) String)
Vec bs (Either (Fin bs) String)
li) [(String, String, String)]
-> [(String, String, String)] -> [(String, String, String)]
forall a. [a] -> [a] -> [a]
++ [(String, String, String)]
le
           , nodeOpts :: [String]
nodeOpts = [String]
rn [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
ln
           }
       )
instance CategoryOf DOT where
  type (~>) = Dot
  type Ob a = (Is D a, IsList (UN D a))

instance MonoidalProfunctor Dot where
  par0 :: Dot Unit Unit
par0 = (Int -> (Int, DotData '[] '[])) -> Dot (D '[]) (D '[])
forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
(Int -> (Int, DotData as bs)) -> Dot (D as) (D bs)
Dot \Int
i -> (Int
i, Vec '[] (Either (Fin '[]) String)
-> Vec '[] (Either (Fin '[]) String)
-> [(String, String, String)]
-> [String]
-> DotData '[] '[]
forall {k} {k} (as :: k) (bs :: k).
Vec as (Either (Fin bs) String)
-> Vec bs (Either (Fin as) String)
-> [(String, String, String)]
-> [String]
-> DotData as bs
DotData ([Either (Fin '[]) String] -> Vec '[] (Either (Fin '[]) String)
forall {k} (as :: k) x. [x] -> Vec as x
Vec []) ([Either (Fin '[]) String] -> Vec '[] (Either (Fin '[]) String)
forall {k} (as :: k) x. [x] -> Vec as x
Vec []) [] [])
  Dot @lis @los Int -> (Int, DotData as bs)
l par :: forall (x1 :: DOT) (x2 :: DOT) (y1 :: DOT) (y2 :: DOT).
Dot x1 x2 -> Dot y1 y2 -> Dot (x1 ** y1) (x2 ** y2)
`par` Dot @ris @ros Int -> (Int, DotData as bs)
r = forall (as :: [Symbol]) (bs :: [Symbol]) r.
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
forall {k} (as :: [k]) (bs :: [k]) r.
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
withIsList2 @lis @ris ((IsList (as ++ as) => Dot (x1 ** y1) (x2 ** y2))
 -> Dot (x1 ** y1) (x2 ** y2))
-> (IsList (as ++ as) => Dot (x1 ** y1) (x2 ** y2))
-> Dot (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$ forall (as :: [Symbol]) (bs :: [Symbol]) r.
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
forall {k} (as :: [k]) (bs :: [k]) r.
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
withIsList2 @los @ros ((IsList (bs ++ bs) => Dot (x1 ** y1) (x2 ** y2))
 -> Dot (x1 ** y1) (x2 ** y2))
-> (IsList (bs ++ bs) => Dot (x1 ** y1) (x2 ** y2))
-> Dot (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$ (Int -> (Int, DotData (as ++ as) (bs ++ bs)))
-> Dot (D (as ++ as)) (D (bs ++ bs))
forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
(Int -> (Int, DotData as bs)) -> Dot (D as) (D bs)
Dot \Int
i ->
    let (Int
k, DotData Vec as (Either (Fin bs) String)
li Vec bs (Either (Fin as) String)
lo [(String, String, String)]
le [String]
ln) = Int -> (Int, DotData as bs)
l Int
j; (Int
j, DotData Vec as (Either (Fin bs) String)
ri Vec bs (Either (Fin as) String)
ro [(String, String, String)]
re [String]
rn) = Int -> (Int, DotData as bs)
r Int
i
    in ( Int
k
       , DotData
           { inputs :: Vec (as ++ as) (Either (Fin (bs ++ bs)) String)
inputs = (Either (Fin bs) String -> Either (Fin (bs ++ bs)) String)
-> Vec as (Either (Fin bs) String)
-> Vec as (Either (Fin (bs ++ bs)) String)
forall a b. (a -> b) -> Vec as a -> Vec as b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Fin bs -> Fin (bs ++ bs))
-> Either (Fin bs) String -> Either (Fin (bs ++ bs)) String
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (forall (bs :: [Symbol]) (as :: [Symbol]). Fin as -> Fin (as ++ bs)
forall {k} (bs :: [k]) (as :: [k]). Fin as -> Fin (as ++ bs)
relax @ros)) Vec as (Either (Fin bs) String)
li Vec as (Either (Fin (bs ++ bs)) String)
-> Vec as (Either (Fin (bs ++ bs)) String)
-> Vec (as ++ as) (Either (Fin (bs ++ bs)) String)
forall {k} (as :: [k]) x (bs :: [k]).
Vec as x -> Vec bs x -> Vec (as ++ bs) x
+++ (Either (Fin bs) String -> Either (Fin (bs ++ bs)) String)
-> Vec as (Either (Fin bs) String)
-> Vec as (Either (Fin (bs ++ bs)) String)
forall a b. (a -> b) -> Vec as a -> Vec as b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Fin bs -> Fin (bs ++ bs))
-> Either (Fin bs) String -> Either (Fin (bs ++ bs)) String
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (forall (as :: [Symbol]) (bs :: [Symbol]).
IsList as =>
Fin bs -> Fin (as ++ bs)
forall {k} (as :: [k]) (bs :: [k]).
IsList as =>
Fin bs -> Fin (as ++ bs)
shift @los)) Vec as (Either (Fin bs) String)
ri
           , outputs :: Vec (bs ++ bs) (Either (Fin (as ++ as)) String)
outputs = (Either (Fin as) String -> Either (Fin (as ++ as)) String)
-> Vec bs (Either (Fin as) String)
-> Vec bs (Either (Fin (as ++ as)) String)
forall a b. (a -> b) -> Vec bs a -> Vec bs b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Fin as -> Fin (as ++ as))
-> Either (Fin as) String -> Either (Fin (as ++ as)) String
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (forall (bs :: [Symbol]) (as :: [Symbol]). Fin as -> Fin (as ++ bs)
forall {k} (bs :: [k]) (as :: [k]). Fin as -> Fin (as ++ bs)
relax @ris)) Vec bs (Either (Fin as) String)
lo Vec bs (Either (Fin (as ++ as)) String)
-> Vec bs (Either (Fin (as ++ as)) String)
-> Vec (bs ++ bs) (Either (Fin (as ++ as)) String)
forall {k} (as :: [k]) x (bs :: [k]).
Vec as x -> Vec bs x -> Vec (as ++ bs) x
+++ (Either (Fin as) String -> Either (Fin (as ++ as)) String)
-> Vec bs (Either (Fin as) String)
-> Vec bs (Either (Fin (as ++ as)) String)
forall a b. (a -> b) -> Vec bs a -> Vec bs b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Fin as -> Fin (as ++ as))
-> Either (Fin as) String -> Either (Fin (as ++ as)) String
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (forall (as :: [Symbol]) (bs :: [Symbol]).
IsList as =>
Fin bs -> Fin (as ++ bs)
forall {k} (as :: [k]) (bs :: [k]).
IsList as =>
Fin bs -> Fin (as ++ bs)
shift @lis)) Vec bs (Either (Fin as) String)
ro
           , edges :: [(String, String, String)]
edges = [(String, String, String)]
le [(String, String, String)]
-> [(String, String, String)] -> [(String, String, String)]
forall a. [a] -> [a] -> [a]
++ [(String, String, String)]
re
           , nodeOpts :: [String]
nodeOpts = [String]
ln [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
rn
           }
       )
instance Monoidal DOT where
  type Unit = D '[]
  type ls ** rs = D (UN D ls ++ UN D rs)
  withOb2 :: forall (a :: DOT) (b :: DOT) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @(D ls) @(D rs) Ob (a ** b) => r
r = forall (as :: [Symbol]) (bs :: [Symbol]) r.
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
forall {k} (as :: [k]) (bs :: [k]) r.
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
withIsList2 @ls @rs r
Ob (a ** b) => r
IsList (UN D a ++ UN D b) => r
r
  leftUnitor :: forall (a :: DOT). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ** a) ~> a
Dot (D (UN D a)) (D (UN D a))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: DOT). Ob a => Dot a a
id
  leftUnitorInv :: forall (a :: DOT). Ob a => a ~> (Unit ** a)
leftUnitorInv = a ~> (Unit ** a)
Dot (D (UN D a)) (D (UN D a))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: DOT). Ob a => Dot a a
id
  rightUnitor :: forall (a :: DOT). Ob a => (a ** Unit) ~> a
rightUnitor = (a ** Unit) ~> a
Dot (D (UN D a)) (D (UN D a))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: DOT). Ob a => Dot a a
id
  rightUnitorInv :: forall (a :: DOT). Ob a => a ~> (a ** Unit)
rightUnitorInv = a ~> (a ** Unit)
Dot (D (UN D a)) (D (UN D a))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: DOT). Ob a => Dot a a
id
  associator :: forall (a :: DOT) (b :: DOT) (c :: DOT).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @as @bs @cs = forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: DOT). (CategoryOf DOT, Ob a) => Obj a
obj @as Dot (D (UN D a)) (D (UN D a))
-> Dot (D (UN D b)) (D (UN D b))
-> Dot (D (UN D a) ** D (UN D b)) (D (UN D a) ** D (UN D b))
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: DOT) (x2 :: DOT) (y1 :: DOT) (y2 :: DOT).
Dot x1 x2 -> Dot y1 y2 -> Dot (x1 ** y1) (x2 ** y2)
`par` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: DOT). (CategoryOf DOT, Ob a) => Obj a
obj @bs Dot
  (D (UN D (D (UN D a)) ++ UN D (D (UN D b))))
  (D (UN D (D (UN D a)) ++ UN D (D (UN D b))))
-> Dot (D (UN D c)) (D (UN D c))
-> Dot
     (D (UN D (D (UN D a)) ++ UN D (D (UN D b))) ** D (UN D c))
     (D (UN D (D (UN D a)) ++ UN D (D (UN D b))) ** D (UN D c))
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: DOT) (x2 :: DOT) (y1 :: DOT) (y2 :: DOT).
Dot x1 x2 -> Dot y1 y2 -> Dot (x1 ** y1) (x2 ** y2)
`par` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: DOT). (CategoryOf DOT, Ob a) => Obj a
obj @cs
  associatorInv :: forall (a :: DOT) (b :: DOT) (c :: DOT).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @as @bs @cs = forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: DOT). (CategoryOf DOT, Ob a) => Obj a
obj @as Dot (D (UN D a)) (D (UN D a))
-> Dot (D (UN D b)) (D (UN D b))
-> Dot (D (UN D a) ** D (UN D b)) (D (UN D a) ** D (UN D b))
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: DOT) (x2 :: DOT) (y1 :: DOT) (y2 :: DOT).
Dot x1 x2 -> Dot y1 y2 -> Dot (x1 ** y1) (x2 ** y2)
`par` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: DOT). (CategoryOf DOT, Ob a) => Obj a
obj @bs Dot
  (D (UN D (D (UN D a)) ++ UN D (D (UN D b))))
  (D (UN D (D (UN D a)) ++ UN D (D (UN D b))))
-> Dot (D (UN D c)) (D (UN D c))
-> Dot
     (D (UN D (D (UN D a)) ++ UN D (D (UN D b))) ** D (UN D c))
     (D (UN D (D (UN D a)) ++ UN D (D (UN D b))) ** D (UN D c))
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: DOT) (x2 :: DOT) (y1 :: DOT) (y2 :: DOT).
Dot x1 x2 -> Dot y1 y2 -> Dot (x1 ** y1) (x2 ** y2)
`par` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: DOT). (CategoryOf DOT, Ob a) => Obj a
obj @cs
instance SymMonoidal DOT where
  swap :: forall (a :: DOT) (b :: DOT). (Ob a, Ob b) => (a ** b) ~> (b ** a)
swap @(D as) @(D bs) =
    forall (as :: [Symbol]) (bs :: [Symbol]) r.
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
forall {k} (as :: [k]) (bs :: [k]) r.
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
withIsList2 @as @bs ((IsList (UN D a ++ UN D b) => (a ** b) ~> (b ** a))
 -> (a ** b) ~> (b ** a))
-> (IsList (UN D a ++ UN D b) => (a ** b) ~> (b ** a))
-> (a ** b) ~> (b ** a)
forall a b. (a -> b) -> a -> b
$
      forall (as :: [Symbol]) (bs :: [Symbol]) r.
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
forall {k} (as :: [k]) (bs :: [k]) r.
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
withIsList2 @bs @as ((IsList (UN D b ++ UN D a) => (a ** b) ~> (b ** a))
 -> (a ** b) ~> (b ** a))
-> (IsList (UN D b ++ UN D a) => (a ** b) ~> (b ** a))
-> (a ** b) ~> (b ** a)
forall a b. (a -> b) -> a -> b
$
        (Int -> (Int, DotData (UN D a ++ UN D b) (UN D b ++ UN D a)))
-> Dot (D (UN D a ++ UN D b)) (D (UN D b ++ UN D a))
forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
(Int -> (Int, DotData as bs)) -> Dot (D as) (D bs)
Dot \Int
n ->
          let as :: Vec (UN D a) (Fin (UN D a))
as = forall (as :: [Symbol]). IsList as => Vec as (Fin as)
forall {k} (as :: [k]). IsList as => Vec as (Fin as)
ixs @as; bs :: Vec (UN D b) (Fin (UN D b))
bs = forall (as :: [Symbol]). IsList as => Vec as (Fin as)
forall {k} (as :: [k]). IsList as => Vec as (Fin as)
ixs @bs
          in ( Int
n
             , DotData
                 { inputs :: Vec (UN D a ++ UN D b) (Either (Fin (UN D b ++ UN D a)) String)
inputs = (Fin (UN D b ++ UN D a) -> Either (Fin (UN D b ++ UN D a)) String)
-> Vec (UN D a ++ UN D b) (Fin (UN D b ++ UN D a))
-> Vec (UN D a ++ UN D b) (Either (Fin (UN D b ++ UN D a)) String)
forall a b.
(a -> b) -> Vec (UN D a ++ UN D b) a -> Vec (UN D a ++ UN D b) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Fin (UN D b ++ UN D a) -> Either (Fin (UN D b ++ UN D a)) String
forall a b. a -> Either a b
Left ((Fin (UN D a) -> Fin (UN D b ++ UN D a))
-> Vec (UN D a) (Fin (UN D a))
-> Vec (UN D a) (Fin (UN D b ++ UN D a))
forall a b. (a -> b) -> Vec (UN D a) a -> Vec (UN D a) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (as :: [Symbol]) (bs :: [Symbol]).
IsList as =>
Fin bs -> Fin (as ++ bs)
forall {k} (as :: [k]) (bs :: [k]).
IsList as =>
Fin bs -> Fin (as ++ bs)
shift @bs) Vec (UN D a) (Fin (UN D a))
as Vec (UN D a) (Fin (UN D b ++ UN D a))
-> Vec (UN D b) (Fin (UN D b ++ UN D a))
-> Vec (UN D a ++ UN D b) (Fin (UN D b ++ UN D a))
forall {k} (as :: [k]) x (bs :: [k]).
Vec as x -> Vec bs x -> Vec (as ++ bs) x
+++ (Fin (UN D b) -> Fin (UN D b ++ UN D a))
-> Vec (UN D b) (Fin (UN D b))
-> Vec (UN D b) (Fin (UN D b ++ UN D a))
forall a b. (a -> b) -> Vec (UN D b) a -> Vec (UN D b) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (bs :: [Symbol]) (as :: [Symbol]). Fin as -> Fin (as ++ bs)
forall {k} (bs :: [k]) (as :: [k]). Fin as -> Fin (as ++ bs)
relax @as) Vec (UN D b) (Fin (UN D b))
bs)
                 , outputs :: Vec (UN D b ++ UN D a) (Either (Fin (UN D a ++ UN D b)) String)
outputs = (Fin (UN D a ++ UN D b) -> Either (Fin (UN D a ++ UN D b)) String)
-> Vec (UN D b ++ UN D a) (Fin (UN D a ++ UN D b))
-> Vec (UN D b ++ UN D a) (Either (Fin (UN D a ++ UN D b)) String)
forall a b.
(a -> b) -> Vec (UN D b ++ UN D a) a -> Vec (UN D b ++ UN D a) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Fin (UN D a ++ UN D b) -> Either (Fin (UN D a ++ UN D b)) String
forall a b. a -> Either a b
Left ((Fin (UN D b) -> Fin (UN D a ++ UN D b))
-> Vec (UN D b) (Fin (UN D b))
-> Vec (UN D b) (Fin (UN D a ++ UN D b))
forall a b. (a -> b) -> Vec (UN D b) a -> Vec (UN D b) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (as :: [Symbol]) (bs :: [Symbol]).
IsList as =>
Fin bs -> Fin (as ++ bs)
forall {k} (as :: [k]) (bs :: [k]).
IsList as =>
Fin bs -> Fin (as ++ bs)
shift @as) Vec (UN D b) (Fin (UN D b))
bs Vec (UN D b) (Fin (UN D a ++ UN D b))
-> Vec (UN D a) (Fin (UN D a ++ UN D b))
-> Vec (UN D b ++ UN D a) (Fin (UN D a ++ UN D b))
forall {k} (as :: [k]) x (bs :: [k]).
Vec as x -> Vec bs x -> Vec (as ++ bs) x
+++ (Fin (UN D a) -> Fin (UN D a ++ UN D b))
-> Vec (UN D a) (Fin (UN D a))
-> Vec (UN D a) (Fin (UN D a ++ UN D b))
forall a b. (a -> b) -> Vec (UN D a) a -> Vec (UN D a) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (bs :: [Symbol]) (as :: [Symbol]). Fin as -> Fin (as ++ bs)
forall {k} (bs :: [k]) (as :: [k]). Fin as -> Fin (as ++ bs)
relax @bs) Vec (UN D a) (Fin (UN D a))
as)
                 , edges :: [(String, String, String)]
edges = []
                 , nodeOpts :: [String]
nodeOpts = []
                 }
             )
instance (Ob as) => Monoid (D as) where
  mempty :: Unit ~> D as
mempty = Vec '[] String -> Vec as String -> String -> Dot (D '[]) (D as)
forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
Vec as String -> Vec bs String -> String -> Dot (D as) (D bs)
node' ([String] -> Vec '[] String
forall {k} (as :: k) x. [x] -> Vec as x
Vec []) ([String] -> Vec as String
forall {k} (as :: k) x. [x] -> Vec as x
Vec ([String] -> [String]
forall a. HasCallStack => [a] -> [a]
cycle [String
Item [String]
":s"])) String
"shape=point; width=0.07; fillcolor=white"
  mappend :: (D as ** D as) ~> D as
mappend =
    forall (as :: [Symbol]) (bs :: [Symbol]) r.
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
forall {k} (as :: [k]) (bs :: [k]) r.
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
withIsList2 @as @as ((IsList (as ++ as) => (D as ** D as) ~> D as)
 -> (D as ** D as) ~> D as)
-> (IsList (as ++ as) => (D as ** D as) ~> D as)
-> (D as ** D as) ~> D as
forall a b. (a -> b) -> a -> b
$ Vec (as ++ as) String
-> Vec as String -> String -> Dot (D (as ++ as)) (D as)
forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
Vec as String -> Vec bs String -> String -> Dot (D as) (D bs)
node' ([String] -> Vec (as ++ as) String
forall {k} (as :: k) x. [x] -> Vec as x
Vec ([String] -> [String]
forall a. HasCallStack => [a] -> [a]
cycle [String
Item [String]
":nw", String
Item [String]
":ne"])) ([String] -> Vec as String
forall {k} (as :: k) x. [x] -> Vec as x
Vec ([String] -> [String]
forall a. HasCallStack => [a] -> [a]
cycle [String
Item [String]
":s"])) String
"shape=point; width=0.07; fillcolor=white"
instance (Ob as) => Comonoid (D as) where
  counit :: D as ~> Unit
counit = Vec as String -> Vec '[] String -> String -> Dot (D as) (D '[])
forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
Vec as String -> Vec bs String -> String -> Dot (D as) (D bs)
node' ([String] -> Vec as String
forall {k} (as :: k) x. [x] -> Vec as x
Vec ([String] -> [String]
forall a. HasCallStack => [a] -> [a]
cycle [String
Item [String]
":n"])) ([String] -> Vec '[] String
forall {k} (as :: k) x. [x] -> Vec as x
Vec []) String
"shape=point; width=0.07"
  comult :: D as ~> (D as ** D as)
comult = forall (as :: [Symbol]) (bs :: [Symbol]) r.
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
forall {k} (as :: [k]) (bs :: [k]) r.
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
withIsList2 @as @as ((IsList (as ++ as) => D as ~> (D as ** D as))
 -> D as ~> (D as ** D as))
-> (IsList (as ++ as) => D as ~> (D as ** D as))
-> D as ~> (D as ** D as)
forall a b. (a -> b) -> a -> b
$ Vec as String
-> Vec (as ++ as) String -> String -> Dot (D as) (D (as ++ as))
forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
Vec as String -> Vec bs String -> String -> Dot (D as) (D bs)
node' ([String] -> Vec as String
forall {k} (as :: k) x. [x] -> Vec as x
Vec ([String] -> [String]
forall a. HasCallStack => [a] -> [a]
cycle [String
Item [String]
":n"])) ([String] -> Vec (as ++ as) String
forall {k} (as :: k) x. [x] -> Vec as x
Vec ([String] -> [String]
forall a. HasCallStack => [a] -> [a]
cycle [String
Item [String]
":sw", String
Item [String]
":se"])) String
"shape=point; width=0.07"
instance CopyDiscard DOT
instance Strong DOT (Id :: CAT DOT) where
  act :: forall (a :: DOT) (b :: DOT) (x :: DOT) (y :: DOT).
(a ~> b) -> Id x y -> Id (Act a x) (Act b y)
act a ~> b
f (Id x ~> y
g) = (D (UN D a ++ UN D x) ~> D (UN D b ++ UN D y))
-> Id (D (UN D a ++ UN D x)) (D (UN D b ++ UN D y))
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (a ~> b
Dot a b
f Dot a b -> Dot x y -> Dot (a ** x) (b ** y)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: DOT) (x2 :: DOT) (y1 :: DOT) (y2 :: DOT).
Dot x1 x2 -> Dot y1 y2 -> Dot (x1 ** y1) (x2 ** y2)
`par` x ~> y
Dot x y
g)
instance Costrong DOT Dot where
  coact :: forall (a :: DOT) (x :: DOT) (y :: DOT).
(Ob a, Ob x, Ob y) =>
Dot (Act a x) (Act a y) -> Dot x y
coact @(D as) @(D xs) @(D ys) (Dot Int -> (Int, DotData as bs)
f) = (Int -> (Int, DotData (UN D x) (UN D y)))
-> Dot (D (UN D x)) (D (UN D y))
forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
(Int -> (Int, DotData as bs)) -> Dot (D as) (D bs)
Dot \Int
n ->
    case Int -> (Int, DotData as bs)
f Int
n of
      (Int
n', DotData Vec as (Either (Fin bs) String)
is Vec bs (Either (Fin as) String)
os [(String, String, String)]
es [String]
ns) ->
        let
          inps :: Vec as (Either (Fin (UN D y)) String)
inps = (Either (Fin bs) String -> Either (Fin (UN D y)) String)
-> Vec as (Either (Fin bs) String)
-> Vec as (Either (Fin (UN D y)) String)
forall a b. (a -> b) -> Vec as a -> Vec as b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Either (Fin bs) String -> Either (Fin (UN D y)) String
fromI Vec as (Either (Fin bs) String)
is
          outs :: Vec bs (Either (Fin (UN D x)) String)
outs = (Either (Fin as) String -> Either (Fin (UN D x)) String)
-> Vec bs (Either (Fin as) String)
-> Vec bs (Either (Fin (UN D x)) String)
forall a b. (a -> b) -> Vec bs a -> Vec bs b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Either (Fin as) String -> Either (Fin (UN D x)) String
fromO Vec bs (Either (Fin as) String)
os
          (Vec (UN D a) (Either (Fin (UN D y)) String)
ais, Vec (UN D x) (Either (Fin (UN D y)) String)
xs) = forall (as :: [Symbol]) (bs :: [Symbol]) x.
IsList as =>
Vec (as ++ bs) x -> (Vec as x, Vec bs x)
forall {k} (as :: [k]) (bs :: [k]) x.
IsList as =>
Vec (as ++ bs) x -> (Vec as x, Vec bs x)
split @as @xs Vec as (Either (Fin (UN D y)) String)
Vec (UN D a ++ UN D x) (Either (Fin (UN D y)) String)
inps
          (Vec (UN D a) (Either (Fin (UN D x)) String)
aos, Vec (UN D y) (Either (Fin (UN D x)) String)
ys) = forall (as :: [Symbol]) (bs :: [Symbol]) x.
IsList as =>
Vec (as ++ bs) x -> (Vec as x, Vec bs x)
forall {k} (as :: [k]) (bs :: [k]) x.
IsList as =>
Vec (as ++ bs) x -> (Vec as x, Vec bs x)
split @as @ys Vec bs (Either (Fin (UN D x)) String)
Vec (UN D a ++ UN D y) (Either (Fin (UN D x)) String)
outs
          fromI :: Either (Fin bs) String -> Either (Fin (UN D y)) String
fromI = (Fin bs -> Either (Fin (UN D y)) String)
-> (String -> Either (Fin (UN D y)) String)
-> Either (Fin bs) String
-> Either (Fin (UN D y)) String
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall (as :: [Symbol]) (bs :: [Symbol]) r.
IsList as =>
(Fin as -> r) -> (Fin bs -> r) -> Fin (as ++ bs) -> r
forall {k} (as :: [k]) (bs :: [k]) r.
IsList as =>
(Fin as -> r) -> (Fin bs -> r) -> Fin (as ++ bs) -> r
eitherF @as @ys (Vec (UN D a) (Either (Fin (UN D y)) String)
ais Vec (UN D a) (Either (Fin (UN D y)) String)
-> Fin (UN D a) -> Either (Fin (UN D y)) String
forall {k} (as :: k) x. Vec as x -> Fin as -> x
!) Fin (UN D y) -> Either (Fin (UN D y)) String
forall a b. a -> Either a b
Left) String -> Either (Fin (UN D y)) String
forall a b. b -> Either a b
Right
          fromO :: Either (Fin as) String -> Either (Fin (UN D x)) String
fromO = (Fin as -> Either (Fin (UN D x)) String)
-> (String -> Either (Fin (UN D x)) String)
-> Either (Fin as) String
-> Either (Fin (UN D x)) String
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall (as :: [Symbol]) (bs :: [Symbol]) r.
IsList as =>
(Fin as -> r) -> (Fin bs -> r) -> Fin (as ++ bs) -> r
forall {k} (as :: [k]) (bs :: [k]) r.
IsList as =>
(Fin as -> r) -> (Fin bs -> r) -> Fin (as ++ bs) -> r
eitherF @as @xs (Vec (UN D a) (Either (Fin (UN D x)) String)
aos Vec (UN D a) (Either (Fin (UN D x)) String)
-> Fin (UN D a) -> Either (Fin (UN D x)) String
forall {k} (as :: k) x. Vec as x -> Fin as -> x
!) Fin (UN D x) -> Either (Fin (UN D x)) String
forall a b. a -> Either a b
Left) String -> Either (Fin (UN D x)) String
forall a b. b -> Either a b
Right
        in
          ( Int
n'
          , DotData
              { inputs :: Vec (UN D x) (Either (Fin (UN D y)) String)
inputs = Vec (UN D x) (Either (Fin (UN D y)) String)
xs
              , outputs :: Vec (UN D y) (Either (Fin (UN D x)) String)
outputs = Vec (UN D y) (Either (Fin (UN D x)) String)
ys
              , edges :: [(String, String, String)]
edges =
                  [(String, String, String)]
es [(String, String, String)]
-> [(String, String, String)] -> [(String, String, String)]
forall a. [a] -> [a] -> [a]
++ ((Either (Fin (UN D x)) String, String,
  Either (Fin (UN D y)) String)
 -> [(String, String, String)])
-> Vec
     (UN D a)
     (Either (Fin (UN D x)) String, String,
      Either (Fin (UN D y)) String)
-> [(String, String, String)]
forall m a. Monoid m => (a -> m) -> Vec (UN D a) a -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\case (Right String
n1, String
nm, Right String
n2) -> [(String
n1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":sw", String
nm, String
n2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":nw")]; (Either (Fin (UN D x)) String, String,
 Either (Fin (UN D y)) String)
_ -> []) (Vec (UN D a) (Either (Fin (UN D x)) String)
-> Vec (UN D a) String
-> Vec (UN D a) (Either (Fin (UN D y)) String)
-> Vec
     (UN D a)
     (Either (Fin (UN D x)) String, String,
      Either (Fin (UN D y)) String)
forall {k} (as :: k) x y z.
Vec as x -> Vec as y -> Vec as z -> Vec as (x, y, z)
zipV3 Vec (UN D a) (Either (Fin (UN D x)) String)
aos (forall (as :: [Symbol]). IsList as => Vec as String
names @as) Vec (UN D a) (Either (Fin (UN D y)) String)
ais)
              , nodeOpts :: [String]
nodeOpts = [String]
ns
              }
          )
instance MonoidalAction DOT DOT where
  type Act a x = a ** x
  withObAct :: forall (a :: DOT) (x :: DOT) r.
(Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct @a @x Ob (Act a x) => r
r = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @x r
Ob (a ** x) => r
Ob (Act a x) => r
r
  unitor :: forall (x :: DOT). Ob x => Act Unit x ~> x
unitor = Act Unit x ~> x
Dot (D (UN D x)) (D (UN D x))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: DOT). Ob a => Dot a a
id
  unitorInv :: forall (x :: DOT). Ob x => x ~> Act Unit x
unitorInv = x ~> Act Unit x
Dot (D (UN D x)) (D (UN D x))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: DOT). Ob a => Dot a a
id
  multiplicator :: forall (a :: DOT) (b :: DOT) (x :: DOT).
(Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator @as @bs @cs = forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: DOT). (CategoryOf DOT, Ob a) => Obj a
obj @as Dot (D (UN D a)) (D (UN D a))
-> Dot (D (UN D b)) (D (UN D b))
-> Dot (D (UN D a) ** D (UN D b)) (D (UN D a) ** D (UN D b))
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: DOT) (x2 :: DOT) (y1 :: DOT) (y2 :: DOT).
Dot x1 x2 -> Dot y1 y2 -> Dot (x1 ** y1) (x2 ** y2)
`par` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: DOT). (CategoryOf DOT, Ob a) => Obj a
obj @bs Dot
  (D (UN D (D (UN D a)) ++ UN D (D (UN D b))))
  (D (UN D (D (UN D a)) ++ UN D (D (UN D b))))
-> Dot (D (UN D x)) (D (UN D x))
-> Dot
     (D (UN D (D (UN D a)) ++ UN D (D (UN D b))) ** D (UN D x))
     (D (UN D (D (UN D a)) ++ UN D (D (UN D b))) ** D (UN D x))
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: DOT) (x2 :: DOT) (y1 :: DOT) (y2 :: DOT).
Dot x1 x2 -> Dot y1 y2 -> Dot (x1 ** y1) (x2 ** y2)
`par` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: DOT). (CategoryOf DOT, Ob a) => Obj a
obj @cs
  multiplicatorInv :: forall (a :: DOT) (b :: DOT) (x :: DOT).
(Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv @as @bs @cs = forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: DOT). (CategoryOf DOT, Ob a) => Obj a
obj @as Dot (D (UN D a)) (D (UN D a))
-> Dot (D (UN D b)) (D (UN D b))
-> Dot (D (UN D a) ** D (UN D b)) (D (UN D a) ** D (UN D b))
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: DOT) (x2 :: DOT) (y1 :: DOT) (y2 :: DOT).
Dot x1 x2 -> Dot y1 y2 -> Dot (x1 ** y1) (x2 ** y2)
`par` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: DOT). (CategoryOf DOT, Ob a) => Obj a
obj @bs Dot
  (D (UN D (D (UN D a)) ++ UN D (D (UN D b))))
  (D (UN D (D (UN D a)) ++ UN D (D (UN D b))))
-> Dot (D (UN D x)) (D (UN D x))
-> Dot
     (D (UN D (D (UN D a)) ++ UN D (D (UN D b))) ** D (UN D x))
     (D (UN D (D (UN D a)) ++ UN D (D (UN D b))) ** D (UN D x))
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: DOT) (x2 :: DOT) (y1 :: DOT) (y2 :: DOT).
Dot x1 x2 -> Dot y1 y2 -> Dot (x1 ** y1) (x2 ** y2)
`par` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: DOT). (CategoryOf DOT, Ob a) => Obj a
obj @cs

swap2 :: (Ob a, Ob b) => Dot (D [a, b]) (D [b, a])
swap2 :: forall (a :: Symbol) (b :: Symbol).
(Ob a, Ob b) =>
Dot (D '[a, b]) (D '[b, a])
swap2 @a @b = forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @(D '[a]) @(D '[b])

-- Regular swap won't render a crossing, since dot can freely move the edges around.
-- This version forces a crossing by adding an invisible node.
swapNode :: (Ob a, Ob b) => Dot (D [a, b]) (D [b, a])
swapNode :: forall (a :: Symbol) (b :: Symbol).
(Ob a, Ob b) =>
Dot (D '[a, b]) (D '[b, a])
swapNode @a @b =
  forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
Vec as String -> Vec bs String -> String -> Dot (D as) (D bs)
node' @[a, b] @[b, a]
    ([String] -> Vec '[a, b] String
forall {k} (as :: k) x. [x] -> Vec as x
Vec [String
Item [String]
":nw", String
Item [String]
":ne"])
    ([String] -> Vec '[b, a] String
forall {k} (as :: k) x. [x] -> Vec as x
Vec [String
Item [String]
":sw", String
Item [String]
":se"])
    String
"shape=point; style=invis; height=0; width=0"

node' :: (IsList as, IsList bs) => Vec as String -> Vec bs String -> String -> Dot (D as) (D bs)
node' :: forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
Vec as String -> Vec bs String -> String -> Dot (D as) (D bs)
node' @as @bs Vec as String
as Vec bs String
bs String
s = (Int -> (Int, DotData as bs)) -> Dot (D as) (D bs)
forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
(Int -> (Int, DotData as bs)) -> Dot (D as) (D bs)
Dot \Int
n ->
  ( Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
  , DotData
      { inputs :: Vec as (Either (Fin bs) String)
inputs = (Fin as -> Either (Fin bs) String)
-> Vec as (Fin as) -> Vec as (Either (Fin bs) String)
forall a b. (a -> b) -> Vec as a -> Vec as b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Fin as
i -> String -> Either (Fin bs) String
forall a b. b -> Either a b
Right (Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Vec as String
as Vec as String -> Fin as -> String
forall {k} (as :: k) x. Vec as x -> Fin as -> x
! Fin as
i))) (forall (as :: [Symbol]). IsList as => Vec as (Fin as)
forall {k} (as :: [k]). IsList as => Vec as (Fin as)
ixs @as)
      , outputs :: Vec bs (Either (Fin as) String)
outputs = (Fin bs -> Either (Fin as) String)
-> Vec bs (Fin bs) -> Vec bs (Either (Fin as) String)
forall a b. (a -> b) -> Vec bs a -> Vec bs b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Fin bs
i -> String -> Either (Fin as) String
forall a b. b -> Either a b
Right (Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Vec bs String
bs Vec bs String -> Fin bs -> String
forall {k} (as :: k) x. Vec as x -> Fin as -> x
! Fin bs
i))) (forall (as :: [Symbol]). IsList as => Vec as (Fin as)
forall {k} (as :: [k]). IsList as => Vec as (Fin as)
ixs @bs)
      , edges :: [(String, String, String)]
edges = []
      , nodeOpts :: [String]
nodeOpts = [String
Item [String]
s]
      }
  )

node :: (IsList as, IsList bs) => String -> Dot (D as) (D bs)
node :: forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
String -> Dot (D as) (D bs)
node String
s = Vec as String -> Vec bs String -> String -> Dot (D as) (D bs)
forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
Vec as String -> Vec bs String -> String -> Dot (D as) (D bs)
node' ([String] -> Vec as String
forall {k} (as :: k) x. [x] -> Vec as x
Vec (String -> [String]
forall a. a -> [a]
repeat String
"")) ([String] -> Vec bs String
forall {k} (as :: k) x. [x] -> Vec as x
Vec (String -> [String]
forall a. a -> [a]
repeat String
"")) (String
"label=\"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\"")

line :: (Ob a) => Dot (D '[a]) (D '[a])
line :: forall (a :: Symbol). Ob a => Dot (D '[a]) (D '[a])
line = Dot (D '[a]) (D '[a])
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: DOT). Ob a => Dot a a
id

getData :: Dot (D as) (D bs) -> DotData as bs
getData :: forall (as :: [Symbol]) (bs :: [Symbol]).
Dot (D as) (D bs) -> DotData as bs
getData (Dot Int -> (Int, DotData as bs)
f) = (Int, DotData as bs) -> DotData as bs
forall a b. (a, b) -> b
snd (Int -> (Int, DotData as bs)
f Int
0)

normalize :: DotData as bs -> DotData as bs
normalize :: forall {k} {k} (as :: k) (bs :: k). DotData as bs -> DotData as bs
normalize (DotData Vec as (Either (Fin bs) String)
is Vec bs (Either (Fin as) String)
os [(String, String, String)]
es [String]
ns) =
  Vec as (Either (Fin bs) String)
-> Vec bs (Either (Fin as) String)
-> [(String, String, String)]
-> [String]
-> DotData as bs
forall {k} {k} (as :: k) (bs :: k).
Vec as (Either (Fin bs) String)
-> Vec bs (Either (Fin as) String)
-> [(String, String, String)]
-> [String]
-> DotData as bs
DotData Vec as (Either (Fin bs) String)
is Vec bs (Either (Fin as) String)
os ([(String, String, String)] -> [(String, String, String)]
forall a. Ord a => [a] -> [a]
sort [(String, String, String)]
es) ([String] -> [String]
forall a. Ord a => [a] -> [a]
sort [String]
ns)

run :: Dot (D as) (D bs) -> String
run :: forall (as :: [Symbol]) (bs :: [Symbol]).
Dot (D as) (D bs) -> String
run @as @bs (Dot Int -> (Int, DotData as bs)
f) =
  let (Int
_, DotData Vec as (Either (Fin bs) String)
is Vec bs (Either (Fin as) String)
os [(String, String, String)]
es [String]
ns) = Int -> (Int, DotData as bs)
f Int
0; as :: Vec as (Fin as, String)
as = Vec as String -> Vec as (Fin as, String)
forall {k} (as :: [k]) x.
IsList as =>
Vec as x -> Vec as (Fin as, x)
ixed (forall (as :: [Symbol]). IsList as => Vec as String
names @as); bs :: Vec bs (Fin bs, String)
bs = Vec bs String -> Vec bs (Fin bs, String)
forall {k} (as :: [k]) x.
IsList as =>
Vec as x -> Vec as (Fin as, x)
ixed (forall (as :: [Symbol]). IsList as => Vec as String
names @bs)
  in String
"digraph G { ranksep=1; node [fontname=\"Times-Italic\"; shape=circle; margin=0]; edge [fontname=\"Times-Italic\"; dir=none];"
       -- fix inputs at the top
       String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n  { rank=source; "
       String -> ShowS
forall a. [a] -> [a] -> [a]
++ ((Fin as, String) -> String) -> Vec as (Fin as, String) -> String
forall m a. Monoid m => (a -> m) -> Vec as a -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap
         (\(Fin as
i, String
n) -> String
"\n    i" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Fin as -> String
forall a. Show a => a -> String
show Fin as
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" [label=\"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\"; shape=plain];")
         Vec as (Fin as, String)
as
       String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
       -- fix outputs at the bottom
       String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n  { rank=sink; "
       String -> ShowS
forall a. [a] -> [a] -> [a]
++ ((Fin bs, String) -> String) -> Vec bs (Fin bs, String) -> String
forall m a. Monoid m => (a -> m) -> Vec bs a -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap
         (\(Fin bs
i, String
n) -> String
"\n    o" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Fin bs -> String
forall a. Show a => a -> String
show Fin bs
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" [label=\"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\"; shape=plain];")
         Vec bs (Fin bs, String)
bs
       String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
       -- node configuration
       String -> ShowS
forall a. [a] -> [a] -> [a]
++ ((Int, String) -> String) -> [(Int, String)] -> String
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\(Int
i, String
n) -> String
"\n  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" [" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"];") ([Int] -> [String] -> [(Int, String)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] [String]
ns)
       -- edges from inputs
       String -> ShowS
forall a. [a] -> [a] -> [a]
++ ((Fin as, Either (Fin bs) String) -> String)
-> Vec as (Fin as, Either (Fin bs) String) -> String
forall m a. Monoid m => (a -> m) -> Vec as a -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\(Fin as
i, Either (Fin bs) String
n) -> String
"\n  i" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Fin as -> String
forall a. Show a => a -> String
show Fin as
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":s -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Fin bs -> String) -> ShowS -> Either (Fin bs) String -> String
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (\Fin bs
j -> String
"o" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Fin bs -> String
forall a. Show a => a -> String
show Fin bs
j String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":n") ShowS
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id Either (Fin bs) String
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
";") (Vec as (Either (Fin bs) String)
-> Vec as (Fin as, Either (Fin bs) String)
forall {k} (as :: [k]) x.
IsList as =>
Vec as x -> Vec as (Fin as, x)
ixed Vec as (Either (Fin bs) String)
is)
       -- edges from outputs
       String -> ShowS
forall a. [a] -> [a] -> [a]
++ ((Fin bs, Either (Fin as) String) -> String)
-> Vec bs (Fin bs, Either (Fin as) String) -> String
forall m a. Monoid m => (a -> m) -> Vec bs a -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\(Fin bs
i, Either (Fin as) String
n) -> (Fin as -> String) -> ShowS -> Either (Fin as) String -> String
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (String -> Fin as -> String
forall a b. a -> b -> a
const String
"") (\String
n' -> String
"\n  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
n' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> o" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Fin bs -> String
forall a. Show a => a -> String
show Fin bs
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":n;") Either (Fin as) String
n) (Vec bs (Either (Fin as) String)
-> Vec bs (Fin bs, Either (Fin as) String)
forall {k} (as :: [k]) x.
IsList as =>
Vec as x -> Vec as (Fin as, x)
ixed Vec bs (Either (Fin as) String)
os)
       -- internal edges
       String -> ShowS
forall a. [a] -> [a] -> [a]
++ ((String, String, String) -> String)
-> [(String, String, String)] -> String
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\(String
i, String
s, String
j) -> String
"\n  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
j String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" [label=\"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\"];") [(String, String, String)]
es
       String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n}\n"

unitAdj :: (Ob l, Ob r) => Dot (D '[]) (D '[l, r])
unitAdj :: forall (l :: Symbol) (r :: Symbol).
(Ob l, Ob r) =>
Dot (D '[]) (D '[l, r])
unitAdj = Vec '[] String
-> Vec '[l, r] String -> String -> Dot (D '[]) (D '[l, r])
forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
Vec as String -> Vec bs String -> String -> Dot (D as) (D bs)
node' ([String] -> Vec '[] String
forall {k} (as :: k) x. [x] -> Vec as x
Vec []) ([String] -> Vec '[l, r] String
forall {k} (as :: k) x. [x] -> Vec as x
Vec [String
Item [String]
":sw", String
Item [String]
":se"]) String
"label=η"

counitAdj :: (Ob l, Ob r) => Dot (D '[r, l]) (D '[])
counitAdj :: forall (l :: Symbol) (r :: Symbol).
(Ob l, Ob r) =>
Dot (D '[r, l]) (D '[])
counitAdj = Vec '[r, l] String
-> Vec '[] String -> String -> Dot (D '[r, l]) (D '[])
forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
Vec as String -> Vec bs String -> String -> Dot (D as) (D bs)
node' ([String] -> Vec '[r, l] String
forall {k} (as :: k) x. [x] -> Vec as x
Vec [String
Item [String]
":nw", String
Item [String]
":ne"]) ([String] -> Vec '[] String
forall {k} (as :: k) x. [x] -> Vec as x
Vec []) String
"label=ϵ"