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

-- | String diagrams rendered to Graphviz: 'Dot' is a monoidal category of diagram fragments
-- ('node', 'line', the adjunction unit and counit 'unitAdj'\/'counitAdj', ...) indexed by their typed input and
-- output wires, and 'run' emits the composed diagram as dot source.
module Proarrow.Tools.Diagrams.Dot where

import Data.Bifunctor (first)
import Data.Char (digitToInt, isDigit)
import Data.Coerce (coerce)
import Data.List qualified as List
import Data.Proxy (Proxy (..))
import GHC.TypeLits (KnownSymbol, Symbol, symbolVal)
import Prelude hiding (Monoid (..), curry, id, (.))

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), Strictly (..), SymMonoidal (..), Tensor)
import Proarrow.Category.Monoidal.Closed (Closed (..))
import Proarrow.Category.Monoidal.CompactClosed (CompactClosed (..))
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard)
import Proarrow.Category.Monoidal.Hypergraph
  ( ExpHG
  , Frobenius
  , Hypergraph
  , applyHG
  , cap
  , cup
  , curryHG
  , dualHG
  , linDistHG
  , linDistInvHG
  )
import Proarrow.Category.Monoidal.StarAutonomous (StarAutonomous (..))
import Proarrow.Category.Monoidal.Strength (Costrong (..))
import Proarrow.Category.Monoidal.Strictified (IsList (..), SList (..), type (++))
import Proarrow.Core (CAT, CategoryOf (..), Is, Kind, Profunctor (..), Promonad (..), UN, dimapDefault)
import Proarrow.Monoid (CocommutativeComonoid, CommutativeMonoid, Comonoid (..), Monoid (..))

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
otherwise = 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 :: CAT 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

-- | The discrete category on type-level 'Symbol's, labelling the wires of a string diagram.
instance CategoryOf Symbol where
  type (~>) = SymRefl
  type Ob s = KnownSymbol s

type DOT :: Kind
type data DOT = D [Symbol]

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 -> [(NodeKind, String)]
nodes :: [(NodeKind, String)]
  -- ^ what each node means, and its Graphviz options
  }
  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)

-- | What a node means, as opposed to how it is drawn.
data NodeKind
  = -- | all its wires carry the same value: a (co)monoid point, a cup or a cap
    Spider
  | -- | 'swapNode'
    Crossing
  | -- | a generator, 'node'
    Box
  deriving (Int -> NodeKind -> ShowS
[NodeKind] -> ShowS
NodeKind -> String
(Int -> NodeKind -> ShowS)
-> (NodeKind -> String) -> ([NodeKind] -> ShowS) -> Show NodeKind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NodeKind -> ShowS
showsPrec :: Int -> NodeKind -> ShowS
$cshow :: NodeKind -> String
show :: NodeKind -> String
$cshowList :: [NodeKind] -> ShowS
showList :: [NodeKind] -> ShowS
Show, NodeKind -> NodeKind -> Bool
(NodeKind -> NodeKind -> Bool)
-> (NodeKind -> NodeKind -> Bool) -> Eq NodeKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NodeKind -> NodeKind -> Bool
== :: NodeKind -> NodeKind -> Bool
$c/= :: NodeKind -> NodeKind -> Bool
/= :: NodeKind -> NodeKind -> Bool
Eq, Eq NodeKind
Eq NodeKind =>
(NodeKind -> NodeKind -> Ordering)
-> (NodeKind -> NodeKind -> Bool)
-> (NodeKind -> NodeKind -> Bool)
-> (NodeKind -> NodeKind -> Bool)
-> (NodeKind -> NodeKind -> Bool)
-> (NodeKind -> NodeKind -> NodeKind)
-> (NodeKind -> NodeKind -> NodeKind)
-> Ord NodeKind
NodeKind -> NodeKind -> Bool
NodeKind -> NodeKind -> Ordering
NodeKind -> NodeKind -> NodeKind
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 :: NodeKind -> NodeKind -> Ordering
compare :: NodeKind -> NodeKind -> Ordering
$c< :: NodeKind -> NodeKind -> Bool
< :: NodeKind -> NodeKind -> Bool
$c<= :: NodeKind -> NodeKind -> Bool
<= :: NodeKind -> NodeKind -> Bool
$c> :: NodeKind -> NodeKind -> Bool
> :: NodeKind -> NodeKind -> Bool
$c>= :: NodeKind -> NodeKind -> Bool
>= :: NodeKind -> NodeKind -> Bool
$cmax :: NodeKind -> NodeKind -> NodeKind
max :: NodeKind -> NodeKind -> NodeKind
$cmin :: NodeKind -> NodeKind -> NodeKind
min :: NodeKind -> NodeKind -> NodeKind
Ord)

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 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 :: CAT 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
      (,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 = []
          , nodes :: [(NodeKind, String)]
nodes = []
          })
  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 [(NodeKind, 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 [(NodeKind, 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
           , nodes :: [(NodeKind, String)]
nodes = [(NodeKind, String)]
rn [(NodeKind, String)]
-> [(NodeKind, String)] -> [(NodeKind, String)]
forall a. [a] -> [a] -> [a]
++ [(NodeKind, String)]
ln
           }
       )

-- | The category string diagrams are built in: an object @'D' ws@ is the list of wire labels
-- along a boundary, and an arrow accumulates the Graphviz data connecting its input wires to its
-- output wires.
instance CategoryOf DOT where
  type (~>) = Dot
  type Ob a = (Is D a, IsList (UN D a))

instance MonoidalProfunctor Dot where
  one :: Dot Unit Unit
one = (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 (,Vec '[] (Either (Fin '[]) String)
-> Vec '[] (Either (Fin '[]) String)
-> [(String, String, String)]
-> [(NodeKind, String)]
-> DotData '[] '[]
forall {k} {k} (as :: k) (bs :: k).
Vec as (Either (Fin bs) String)
-> Vec bs (Either (Fin as) String)
-> [(String, String, String)]
-> [(NodeKind, 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 ** :: forall (x1 :: DOT) (x2 :: DOT) (y1 :: DOT) (y2 :: DOT).
Dot x1 x2 -> Dot y1 y2 -> Dot (x1 ** y1) (x2 ** y2)
** 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
j, DotData Vec as (Either (Fin bs) String)
li Vec bs (Either (Fin as) String)
lo [(String, String, String)]
le [(NodeKind, String)]
ln) = Int -> (Int, DotData as bs)
l Int
i; (Int
k, DotData Vec as (Either (Fin bs) String)
ri Vec bs (Either (Fin as) String)
ro [(String, String, String)]
re [(NodeKind, String)]
rn) = Int -> (Int, DotData as bs)
r Int
j
    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
           , nodes :: [(NodeKind, String)]
nodes = [(NodeKind, String)]
ln [(NodeKind, String)]
-> [(NodeKind, String)] -> [(NodeKind, String)]
forall a. [a] -> [a] -> [a]
++ [(NodeKind, 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
  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) (b :: k) (c :: k).
(Strictly a, Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
forall (a :: DOT) (b :: DOT) (c :: DOT).
(Strictly a, Monoidal DOT, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associatorDefault @as @bs @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) (b :: k) (c :: k).
(Strictly a, Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
forall (a :: DOT) (b :: DOT) (c :: DOT).
(Strictly a, Monoidal DOT, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associatorDefault @as @bs @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 = []
                 , nodes :: [(NodeKind, String)]
nodes = []
                 }
             )

-- | One point node for each wire of @as@. @inAt@ and @outAt@ say which wire's node each input and
-- output is attached to, and at which port. Drawing the (co)monoid on several wires as a single
-- point would not say which output continues which input.
pointsPerWire
  :: forall (as :: [Symbol]) xs ys
   . (IsList as, IsList xs, IsList ys)
  => (Fin xs -> (Int, String))
  -> (Fin ys -> (Int, String))
  -> String
  -> Dot (D xs) (D ys)
pointsPerWire :: forall (as :: [Symbol]) (xs :: [Symbol]) (ys :: [Symbol]).
(IsList as, IsList xs, IsList ys) =>
(Fin xs -> (Int, String))
-> (Fin ys -> (Int, String)) -> String -> Dot (D xs) (D ys)
pointsPerWire Fin xs -> (Int, String)
inAt Fin ys -> (Int, String)
outAt String
opts = (Int -> (Int, DotData xs ys)) -> Dot (D xs) (D ys)
forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
(Int -> (Int, DotData as bs)) -> Dot (D as) (D bs)
Dot \Int
n ->
  let at :: forall zs ws. (Fin zs -> (Int, String)) -> Fin zs -> Either (Fin ws) Port
      at :: forall {k} {k} (zs :: k) (ws :: k).
(Fin zs -> (Int, String)) -> Fin zs -> Either (Fin ws) String
at Fin zs -> (Int, String)
f Fin zs
i = let (Int
w, String
port) = Fin zs -> (Int, String)
f Fin zs
i in String -> Either (Fin ws) String
forall a b. b -> Either a b
Right (Int -> String
forall a. Show a => a -> String
show (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
w) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
port)
  in ( Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ forall (as :: [Symbol]). IsList as => Int
forall {k} (as :: [k]). IsList as => Int
len @as
     , DotData
         { inputs :: Vec xs (Either (Fin ys) String)
inputs = (Fin xs -> Either (Fin ys) String)
-> Vec xs (Fin xs) -> Vec xs (Either (Fin ys) String)
forall a b. (a -> b) -> Vec xs a -> Vec xs b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Fin xs -> (Int, String)) -> Fin xs -> Either (Fin ys) String
forall {k} {k} (zs :: k) (ws :: k).
(Fin zs -> (Int, String)) -> Fin zs -> Either (Fin ws) String
at Fin xs -> (Int, String)
inAt) (forall (as :: [Symbol]). IsList as => Vec as (Fin as)
forall {k} (as :: [k]). IsList as => Vec as (Fin as)
ixs @xs)
         , outputs :: Vec ys (Either (Fin xs) String)
outputs = (Fin ys -> Either (Fin xs) String)
-> Vec ys (Fin ys) -> Vec ys (Either (Fin xs) String)
forall a b. (a -> b) -> Vec ys a -> Vec ys b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Fin ys -> (Int, String)) -> Fin ys -> Either (Fin xs) String
forall {k} {k} (zs :: k) (ws :: k).
(Fin zs -> (Int, String)) -> Fin zs -> Either (Fin ws) String
at Fin ys -> (Int, String)
outAt) (forall (as :: [Symbol]). IsList as => Vec as (Fin as)
forall {k} (as :: [k]). IsList as => Vec as (Fin as)
ixs @ys)
         , edges :: [(String, String, String)]
edges = []
         , nodes :: [(NodeKind, String)]
nodes = Int -> (NodeKind, String) -> [(NodeKind, String)]
forall a. Int -> a -> [a]
replicate (forall (as :: [Symbol]). IsList as => Int
forall {k} (as :: [k]). IsList as => Int
len @as) (NodeKind
Spider, String
opts)
         }
     )

-- | Attaches at the given port of wire @i@'s point.
wireAt :: String -> Fin as -> (Int, String)
wireAt :: forall {k} (as :: k). String -> Fin as -> (Int, String)
wireAt String
port (Fin Int
i) = (Int
i, String
port)

-- | Attaches wire @i@ of either copy in @as ++ as@ to wire @i@'s point, the first copy at the
-- first port and the second at the second.
eitherCopy :: forall (as :: [Symbol]). (IsList as) => String -> String -> Fin (as ++ as) -> (Int, String)
eitherCopy :: forall (as :: [Symbol]).
IsList as =>
String -> String -> Fin (as ++ as) -> (Int, String)
eitherCopy String
l String
r = 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 @as (String -> Fin as -> (Int, String)
forall {k} (as :: k). String -> Fin as -> (Int, String)
wireAt String
l) (String -> Fin as -> (Int, String)
forall {k} (as :: k). String -> Fin as -> (Int, String)
wireAt String
r)

instance (Ob as) => Monoid (D as) where
  mempty :: Unit ~> D as
mempty = forall (as :: [Symbol]) (xs :: [Symbol]) (ys :: [Symbol]).
(IsList as, IsList xs, IsList ys) =>
(Fin xs -> (Int, String))
-> (Fin ys -> (Int, String)) -> String -> Dot (D xs) (D ys)
pointsPerWire @as (String -> Fin '[] -> (Int, String)
forall {k} (as :: k). String -> Fin as -> (Int, String)
wireAt String
"") (String -> Fin as -> (Int, String)
forall {k} (as :: k). String -> Fin as -> (Int, String)
wireAt 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
$
      forall (as :: [Symbol]) (xs :: [Symbol]) (ys :: [Symbol]).
(IsList as, IsList xs, IsList ys) =>
(Fin xs -> (Int, String))
-> (Fin ys -> (Int, String)) -> String -> Dot (D xs) (D ys)
pointsPerWire @as (forall (as :: [Symbol]).
IsList as =>
String -> String -> Fin (as ++ as) -> (Int, String)
eitherCopy @as String
":nw" String
":ne") (String -> Fin as -> (Int, String)
forall {k} (as :: k). String -> Fin as -> (Int, String)
wireAt String
":s") String
"shape=point; width=0.07; fillcolor=white"
instance (Ob as) => Comonoid (D as) where
  counit :: D as ~> Unit
counit = forall (as :: [Symbol]) (xs :: [Symbol]) (ys :: [Symbol]).
(IsList as, IsList xs, IsList ys) =>
(Fin xs -> (Int, String))
-> (Fin ys -> (Int, String)) -> String -> Dot (D xs) (D ys)
pointsPerWire @as (String -> Fin as -> (Int, String)
forall {k} (as :: k). String -> Fin as -> (Int, String)
wireAt String
":n") (String -> Fin '[] -> (Int, String)
forall {k} (as :: k). String -> Fin as -> (Int, String)
wireAt String
"") 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
$
      forall (as :: [Symbol]) (xs :: [Symbol]) (ys :: [Symbol]).
(IsList as, IsList xs, IsList ys) =>
(Fin xs -> (Int, String))
-> (Fin ys -> (Int, String)) -> String -> Dot (D xs) (D ys)
pointsPerWire @as (String -> Fin as -> (Int, String)
forall {k} (as :: k). String -> Fin as -> (Int, String)
wireAt String
":n") (forall (as :: [Symbol]).
IsList as =>
String -> String -> Fin (as ++ as) -> (Int, String)
eitherCopy @as String
":sw" String
":se") String
"shape=point; width=0.07"
instance (Ob as) => CocommutativeComonoid (D as)
instance (Ob as) => CommutativeMonoid (D as)

-- | The points are spiders: on each wire, merging and copying are the special commutative
-- Frobenius structure.
instance (Ob as) => Frobenius (D as)

instance CopyDiscard DOT

-- | The points make every object a special commutative Frobenius object, so a diagram's wires can
-- be bent: each object is its own dual, with cups and caps drawn as a copy or merge point next to
-- a unit or counit point.
instance Hypergraph DOT

instance Closed DOT where
  type a ~~> b = ExpHG a b
  withObExp :: forall (a :: DOT) (b :: DOT) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @a @b Ob (a ~~> b) => r
r = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @DOT @a @b r
Ob (a ** b) => r
Ob (a ~~> b) => r
r
  curry :: forall (a :: DOT) (b :: DOT) (c :: DOT).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @a @b = forall {k} (a :: k) (b :: k) (c :: k).
(Hypergraph k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> ExpHG b c
forall (a :: DOT) (b :: DOT) (c :: DOT).
(Hypergraph DOT, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> ExpHG b c
curryHG @a @b
  apply :: forall (a :: DOT) (b :: DOT). (Ob a, Ob b) => ((a ~~> b) ** a) ~> b
apply @b @c = forall {k} (b :: k) (c :: k).
(Hypergraph k, Ob b, Ob c) =>
(ExpHG b c ** b) ~> c
forall (b :: DOT) (c :: DOT).
(Hypergraph DOT, Ob b, Ob c) =>
(ExpHG b c ** b) ~> c
applyHG @b @c

instance StarAutonomous DOT where
  type Dual a = a
  withObDual :: forall (a :: DOT) r. Ob a => (Ob (Dual a) => r) -> r
withObDual Ob (Dual a) => r
r = r
Ob (Dual a) => r
r
  dual :: forall (a :: DOT) (b :: DOT). (a ~> b) -> Dual b ~> Dual a
dual = (a ~> b) -> b ~> a
(a ~> b) -> Dual b ~> Dual a
forall {k} (a :: k) (b :: k). Hypergraph k => (a ~> b) -> b ~> a
dualHG
  dualInv :: forall (a :: DOT) (b :: DOT).
(Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv = (Dual a ~> Dual b) -> b ~> a
(D (UN D a) ~> D (UN D b)) -> D (UN D b) ~> D (UN D a)
forall {k} (a :: k) (b :: k). Hypergraph k => (a ~> b) -> b ~> a
dualHG
  linDist :: forall (a :: DOT) (b :: DOT) (c :: DOT).
(Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist @a @b @c = forall {k} (a :: k) (b :: k) (c :: k).
(Hypergraph k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> ExpHG b c
forall (a :: DOT) (b :: DOT) (c :: DOT).
(Hypergraph DOT, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> ExpHG b c
linDistHG @a @b @c
  linDistInv :: forall (a :: DOT) (b :: DOT) (c :: DOT).
(Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @a @b @c = forall {k} (a :: k) (b :: k) (c :: k).
(Hypergraph k, Ob b, Ob c) =>
(a ~> (b ** c)) -> (a ** b) ~> c
forall (a :: DOT) (b :: DOT) (c :: DOT).
(Hypergraph DOT, Ob b, Ob c) =>
(a ~> (b ** c)) -> (a ** b) ~> c
linDistInvHG @a @b @c
  doubleNeg :: forall (a :: DOT). Ob a => Dual (Dual a) ~> a
doubleNeg = Dual (Dual a) ~> a
Dot (D (UN D a)) (D (UN D a))
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: DOT). Ob a => Dot a a
id
  doubleNegInv :: forall (a :: DOT). Ob a => a ~> Dual (Dual a)
doubleNegInv = a ~> Dual (Dual a)
Dot (D (UN D a)) (D (UN D a))
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: DOT). Ob a => Dot a a
id

instance CompactClosed DOT where
  distribDual :: forall (a :: DOT) (b :: DOT).
(Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual @a @b = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @DOT @a @b Dot (D (UN D a ++ UN D b)) (D (UN D a ++ UN D b))
Ob (a ** b) => Dot (D (UN D a ++ UN D b)) (D (UN D a ++ UN D b))
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: DOT). Ob a => Dot a a
id
  dualUnit :: Dual Unit ~> Unit
dualUnit = Dual Unit ~> Unit
Dot (D '[]) (D '[])
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: DOT). Ob a => Dot a a
id
  dualityUnit :: forall (a :: DOT). Ob a => Unit ~> (a ** Dual a)
dualityUnit @a = forall {k} (a :: k). Frobenius a => Unit ~> (a ** a)
forall (a :: DOT). Frobenius a => Unit ~> (a ** a)
cup @a
  dualityCounit :: forall (a :: DOT). Ob a => (Dual a ** a) ~> Unit
dualityCounit @a = forall {k} (a :: k). Frobenius a => (a ** a) ~> Unit
forall (a :: DOT). Frobenius a => (a ** a) ~> Unit
cap @a
instance Costrong Tensor Dot where
  coact :: forall (a :: DOT) (x :: DOT) (y :: DOT).
(Ob a, Ob x, Ob y) =>
Dot (Act Tensor a x) (Act Tensor 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 [(NodeKind, 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 -> String -> String -> (String, String, String)
feedback String
n1 String
nm String
n2]; (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)
              , nodes :: [(NodeKind, String)]
nodes = [(NodeKind, String)]
ns
              }
          )

-- | A fed-back wire. One that returns to the node it leaves is attached at corners of its ports, so
-- that Graphviz draws the loop beside the node and not across it; one between two nodes attaches
-- as any other wire does.
feedback :: Port -> String -> Port -> (Port, String, Port)
feedback :: String -> String -> String -> (String, String, String)
feedback String
from String
nm String
to
  | String -> Int
nodeOf String
from Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Int
nodeOf String
to = (String -> ShowS
bend String
":sw" String
from, String
nm, String -> ShowS
bend String
":nw" String
to)
  | Bool
otherwise = (String
from, String
nm, String
to)

-- | A port with the side it is drawn at replaced by the given corner.
bend :: String -> Port -> Port
bend :: String -> ShowS
bend String
corner String
p = case (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
':') (ShowS
forall a. [a] -> [a]
reverse String
p) of
  (String
side, Char
':' : String
rest) | ShowS
forall a. [a] -> [a]
reverse String
side String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` ([String
Item [String]
"n", String
Item [String]
"ne", String
Item [String]
"e", String
Item [String]
"se", String
Item [String]
"s", String
Item [String]
"sw", String
Item [String]
"w", String
Item [String]
"nw", String
Item [String]
"c"] :: [String]) -> ShowS
forall a. [a] -> [a]
reverse String
rest String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
corner
  (String, String)
_ -> String
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
corner

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])

-- | A crossing drawn through an invisible node, which pins the crossing point. A plain 'swap'
-- also renders as a crossing, since 'run' fixes the order of the boundary wires and 'node' the
-- order of its ports, but Graphviz is then free to place it.
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) =>
NodeKind
-> Vec as String -> Vec bs String -> String -> Dot (D as) (D bs)
node' @[a, b] @[b, a]
    NodeKind
Crossing
    ([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) => NodeKind -> Vec as String -> Vec bs String -> String -> Dot (D as) (D bs)
node' :: forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
NodeKind
-> Vec as String -> Vec bs String -> String -> Dot (D as) (D bs)
node' @as @bs NodeKind
k 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 = []
      , nodes :: [(NodeKind, String)]
nodes = [(NodeKind
k, String
s)]
      }
  )

-- | A node with the given name, with a port for each input along the top and each output along
-- the bottom, in order, so that Graphviz draws the wires into it in order.
node :: forall as bs. (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 =
  NodeKind
-> Vec as String -> Vec bs String -> String -> Dot (D as) (D bs)
forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
NodeKind
-> Vec as String -> Vec bs String -> String -> Dot (D as) (D bs)
node'
    NodeKind
Box
    ((Fin as -> String) -> Vec as (Fin as) -> Vec as 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 Int
i) -> String
":i" 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
":n") (forall (as :: [Symbol]). IsList as => Vec as (Fin as)
forall {k} (as :: [k]). IsList as => Vec as (Fin as)
ixs @as))
    ((Fin bs -> String) -> Vec bs (Fin bs) -> Vec bs 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 Int
j) -> String
":o" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
j String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":s") (forall (as :: [Symbol]). IsList as => Vec as (Fin as)
forall {k} (as :: [k]). IsList as => Vec as (Fin as)
ixs @bs))
    (Int -> Int -> ShowS
portedLabel (forall (as :: [Symbol]). IsList as => Int
forall {k} (as :: [k]). IsList as => Int
len @as) (forall (as :: [Symbol]). IsList as => Int
forall {k} (as :: [k]). IsList as => Int
len @bs) String
s)

-- | An HTML-like label drawing the node as a rounded box: the name in the middle, with a row of
-- empty cells along the top edge for the inputs and along the bottom edge for the outputs, named
-- by the ports 'node' attaches the wires to. The wires end at the box's edge.
portedLabel :: Int -> Int -> String -> String
portedLabel :: Int -> Int -> ShowS
portedLabel Int
ins Int
outs String
s =
  String
"shape=plain; label=<<table border=\"1\" style=\"rounded\" cellborder=\"0\" cellspacing=\"0\" cellpadding=\"0\">"
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"<tr><td>"
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> Int -> String
ports String
"i" Int
ins
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"</td></tr><tr><td cellpadding=\"2\">"
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
htmlEscape String
s
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"</td></tr><tr><td>"
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> Int -> String
ports String
"o" Int
outs
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"</td></tr></table>>"
  where
    ports :: String -> Int -> String
    ports :: String -> Int -> String
ports String
port Int
n =
      String
"<table border=\"0\" cellborder=\"0\" cellspacing=\"0\" cellpadding=\"0\"><tr>"
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"<td width=\"6\" height=\"6\"></td>"
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate
          String
"<td width=\"4\"></td>"
          [String
"<td port=\"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
port 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
"\" width=\"10\"></td>" | Int
i <- [Int
Item [Int]
0 .. Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 :: Int]]
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"<td width=\"6\"></td></tr></table>"

-- | The nodes in the order they are reached from the inputs, going along the wires, followed by
-- any that no input reaches.
nodeOrder :: [Either x Port] -> [(Port, String, Port)] -> Int -> [Int]
nodeOrder :: forall x.
[Either x String] -> [(String, String, String)] -> Int -> [Int]
nodeOrder [Either x String]
ins [(String, String, String)]
es Int
count = [Int]
reached [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int
n | Int
n <- [Int
Item [Int]
0 .. Int
count Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1], Int
n Int -> [Int] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`notElem` [Int]
reached]
  where
    reached :: [Int]
reached = [Int] -> [Int] -> [Int]
go [] [String -> Int
nodeOf String
p | Right String
p <- [Either x String]
ins]
    go :: [Int] -> [Int] -> [Int]
go [Int]
seen [] = [Int] -> [Int]
forall a. [a] -> [a]
reverse [Int]
seen
    go [Int]
seen (Int
n : [Int]
queue)
      | Int
n Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` [Int]
seen = [Int] -> [Int] -> [Int]
go [Int]
seen [Int]
queue
      | Bool
otherwise = [Int] -> [Int] -> [Int]
go (Int
n Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
seen) ([Int]
queue [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [String -> Int
nodeOf String
q | (String
p, String
_, String
q) <- [(String, String, String)]
es, String -> Int
nodeOf String
p Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n])

-- | The node a port belongs to.
nodeOf :: Port -> Int
nodeOf :: String -> Int
nodeOf = (Int -> Char -> Int) -> Int -> String -> Int
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (\Int
n Char
c -> Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
10 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Char -> Int
digitToInt Char
c) Int
0 (String -> Int) -> ShowS -> String -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
takeWhile Char -> Bool
isDigit

-- | A port without its node and without the side it is drawn at (@3:o0:s@ is @:o0@); a port that
-- is only a side keeps it (@3:nw@ is @:nw@).
portOf :: Port -> String
portOf :: ShowS
portOf String
p = case (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
':') (Int -> ShowS
forall a. Int -> [a] -> [a]
drop Int
1 ((Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isDigit String
p)) of
  (String
name, Char
':' : String
_) -> Char
':' Char -> ShowS
forall a. a -> [a] -> [a]
: String
name
  (String, String)
_ -> (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isDigit String
p

htmlEscape :: String -> String
htmlEscape :: ShowS
htmlEscape = (Char -> String) -> ShowS
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 (\case Char
'<' -> String
"&lt;"; Char
'>' -> String
"&gt;"; Char
'&' -> String
"&amp;"; Char
c -> [Char
Item String
c])

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 :: CAT 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)

run :: Dot (D as) (D bs) -> String
run :: forall (as :: [Symbol]) (bs :: [Symbol]).
Dot (D as) (D bs) -> String
run @as @bs d :: Dot (D as) (D bs)
d@Dot{} =
  String
header
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ Dot (D as) (D bs) -> String
forall (as :: [Symbol]) (bs :: [Symbol]).
Dot (D as) (D bs) -> String
statements Dot (D as) (D bs)
d
    -- the inputs at the top and the outputs at the bottom
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> String -> Int -> String
onRank String
"source" String
"i" (forall (as :: [Symbol]). IsList as => Int
forall {k} (as :: [k]). IsList as => Int
len @as)
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> String -> Int -> String
onRank String
"sink" String
"o" (forall (as :: [Symbol]). IsList as => Int
forall {k} (as :: [k]). IsList as => Int
len @bs)
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n}\n"

-- | A boundary node on the given rank, when its boundary has any wires.
onRank :: String -> String -> Int -> String
onRank :: String -> String -> Int -> String
onRank String
rank String
n Int
wires = if Int
wires Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then String
"" else String
"\n  { rank=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
rank 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
"; }"

-- | The start of a Graphviz graph, with the fonts and wire style of every diagram.
header :: String
header :: String
header =
  String
"digraph G { ranksep=0.3; node [fontname=\"Times-Italic\"; shape=circle; margin=0]; edge [fontname=\"Times-Italic\"; dir=none];"

-- | The statements drawing a diagram. Each boundary is one node, @i@ or @o@, with a port per
-- wire, so that Graphviz keeps the wires in order, and is left out when it has no wires.
statements :: Dot (D as) (D bs) -> String
statements :: forall (as :: [Symbol]) (bs :: [Symbol]).
Dot (D as) (D bs) -> String
statements @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 [(NodeKind, String)]
ns) = Int -> (Int, DotData as bs)
f Int
0
      ins :: [String]
ins = Vec as String -> [String]
forall {k} (as :: k) x. Vec as x -> [x]
unVec (forall (as :: [Symbol]). IsList as => Vec as String
names @as)
      outs :: [String]
outs = Vec bs String -> [String]
forall {k} (as :: k) x. Vec as x -> [x]
unVec (forall (as :: [Symbol]). IsList as => Vec as String
names @bs)
  in String -> [String] -> String
boundary String
"i" [String]
ins
       String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
boundary String
"o" [String]
outs
       -- node configuration, in the order the nodes are reached from the inputs: Graphviz breaks
       -- the cycles of a trace by searching in the order nodes are listed, so this makes the wires
       -- run forward from the first input
       String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int -> String) -> [Int] -> 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 -> 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]
++ (NodeKind, String) -> String
forall a b. (a, b) -> b
snd ([(NodeKind, String)]
ns [(NodeKind, String)] -> Int -> (NodeKind, String)
forall a. HasCallStack => [a] -> Int -> a
!! Int
i) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"];") ([Either (Fin bs) String]
-> [(String, String, String)] -> Int -> [Int]
forall x.
[Either x String] -> [(String, String, String)] -> Int -> [Int]
nodeOrder (Vec as (Either (Fin bs) String) -> [Either (Fin bs) String]
forall {k} (as :: k) x. Vec as x -> [x]
unVec Vec as (Either (Fin bs) String)
is) [(String, String, String)]
es ([(NodeKind, String)] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [(NodeKind, 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:p" 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:p" 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 :: CAT 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:p" 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
  where
    boundary :: String -> [String] -> String
boundary String
name [String]
ws
      | [String] -> Bool
forall a. [a] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [String]
ws = String
""
      | Bool
otherwise =
          String
"\n  "
            String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
name
            String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" [shape=plain; label=<<table border=\"0\" cellborder=\"0\" cellspacing=\"8\" cellpadding=\"0\"><tr>"
            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
"<td port=\"p" 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
"\" width=\"24\">" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
htmlEscape String
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"</td>") ([Int] -> [String] -> [(Int, String)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] [String]
ws)
            String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"</tr></table>>];"

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 = NodeKind
-> Vec '[] String
-> Vec '[l, r] String
-> String
-> Dot (D '[]) (D '[l, r])
forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
NodeKind
-> Vec as String -> Vec bs String -> String -> Dot (D as) (D bs)
node' NodeKind
Box ([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 = NodeKind
-> Vec '[r, l] String
-> Vec '[] String
-> String
-> Dot (D '[r, l]) (D '[])
forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
NodeKind
-> Vec as String -> Vec bs String -> String -> Dot (D as) (D bs)
node' NodeKind
Box ([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=ϵ"