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

-- | String diagrams drawn as SVG. 'Svg' is the category of diagrams of
-- "Proarrow.Tools.Diagrams.Dot", with the same meaning, but a diagram is laid out from how it is
-- built instead of by Graphviz: a tensor puts its two sides next to each other, a composite stacks
-- them with a band of curved wires in between, and a trace draws its loops around the side. Every
-- coordinate is computed here, so every choice can be tweaked.
--
-- Unlike 'DOT', 'SVG' is not strict about its unit: the unit is a wire of its own, 'I', so the
-- unitors are arrows that can be drawn, a dotted wire ending on or leaving another wire. With
-- 'explicitCoherence' off, unit wires take up no room and are not drawn at all.
--
-- Nor is 'SVG' self-dual on the nose: the dual of a wire @'Wire' s@ is the wire @'Co' s@, shown
-- with a superscript ⁻¹ and drawn as a hollow line. The arrows between a wire and its dual only
-- relabel.
--
-- Both are only drawn: an arrow means the 'Dot' diagram on the wires with the unit wires left out
-- and the duals forgotten ('Erase').
module Proarrow.Tools.Diagrams.Svg where

import Data.Functor.Identity (Identity (..))
import Data.Kind (Constraint)
import Data.List qualified as List
import Data.List.NonEmpty (NonEmpty (..))
import Data.List.NonEmpty qualified as NE
import Data.Maybe (fromMaybe)
import Data.Proxy (Proxy (..))
import GHC.TypeLits (KnownSymbol, Symbol, symbolVal)
import Numeric (showFFloat)
import Prelude hiding (Monoid (..), curry, id, (**), (.))

import Proarrow.Category.Instance.Free (All)
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..), Tensor)
import Proarrow.Category.Monoidal qualified as M
import Proarrow.Category.Monoidal.Closed (Closed (..))
import Proarrow.Category.Monoidal.CompactClosed (CompactClosed (..))
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard)
import Proarrow.Category.Monoidal.Hypergraph (Frobenius, Hypergraph, cap, cup)
import Proarrow.Category.Monoidal.StarAutonomous (ExpSA, StarAutonomous (..), applySA, currySA, expSA)
import Proarrow.Category.Monoidal.Strength (Costrong (..))
import Proarrow.Category.Monoidal.Strictified
  ( IsList (..)
  , SList (..)
  , Strictified (..)
  , obj1
  , singleton
  , swap2
  , type (++)
  )
import Proarrow.Core (CAT, CategoryOf (..), Is, Kind, Profunctor (..), Promonad (..), UN, dimapDefault, obj)
import Proarrow.Monoid (CocommutativeComonoid, CommutativeMonoid, Comonoid (..), Monoid (..))
import Proarrow.Tools.Diagrams.Dot (DOT, Dot)
import Proarrow.Tools.Diagrams.Dot qualified as Dot
import Proarrow.Tools.Laws (Labelled (..), Law (..), Laws (..), lawName, withSides)

-- * Wires

-- | A wire: a labelled wire, the dual of one, or the unit wire.
type W :: Kind
type data W = Wire Symbol | Co Symbol | I

-- | The dual of a wire. The unit wire is its own dual.
type DualW :: W -> W
type family DualW w where
  DualW (Wire s) = Co s
  DualW (Co s) = Wire s
  DualW I = I

-- | The duals of the wires.
type DualList :: [W] -> [W]
type family DualList ws where
  DualList '[] = '[]
  DualList (w ': ws) = DualW w ': DualList ws

-- | The labels of the wires that carry something: the unit wires left out, and a dual wire
-- labelled as the wire it is the dual of.
type Erase :: [W] -> [Symbol]
type family Erase ws where
  Erase '[] = '[]
  Erase (Wire s ': ws) = s ': Erase ws
  Erase (Co s ': ws) = s ': Erase ws
  Erase (I ': ws) = Erase ws

-- | A wire whose label is known. The methods are facts about 'DualW' and 'Erase' that hold for
-- each kind of wire, from which 'withIsListDual', 'withIsListErase', 'withEraseAppend',
-- 'withDualDual' and 'withEraseDual' prove them for lists by induction.
type KnownWire :: W -> Constraint
class KnownWire w where
  -- | The label of the wire as it is shown, and its kind.
  wireInfo :: (String, WireKind)

  withKnownDualW :: ((KnownWire (DualW w)) => r) -> r
  withIsListEraseCons :: forall (ws :: [W]) r. (IsList (Erase ws)) => ((IsList (Erase (w ': ws))) => r) -> r
  withEraseAppendCons
    :: forall (as :: [W]) (bs :: [W]) r
     . (Erase (as ++ bs) ~ (Erase as ++ Erase bs))
    => ((Erase (w ': (as ++ bs)) ~ (Erase (w ': as) ++ Erase bs)) => r)
    -> r
  withDualDualW :: ((DualW (DualW w) ~ w) => r) -> r
  withEraseDualCons
    :: forall (ws :: [W]) r. (Erase (DualList ws) ~ Erase ws) => ((Erase (DualList (w ': ws)) ~ Erase (w ': ws)) => r) -> r

instance (KnownSymbol s) => KnownWire (Wire s) where
  wireInfo :: (String, WireKind)
wireInfo = (Proxy s -> 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), WireKind
Plain)
  withKnownDualW :: forall r. (KnownWire (DualW (Wire s)) => r) -> r
withKnownDualW KnownWire (DualW (Wire s)) => r
r = r
KnownWire (DualW (Wire s)) => r
r
  withIsListEraseCons :: forall (ws :: [W]) r.
IsList (Erase ws) =>
(IsList (Erase (Wire s : ws)) => r) -> r
withIsListEraseCons @ws IsList (Erase (Wire s : ws)) => 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 @'[s] @(Erase ws) r
IsList ('[s] ++ Erase ws) => r
IsList (Erase (Wire s : ws)) => r
r
  withEraseAppendCons :: forall (as :: [W]) (bs :: [W]) r.
(Erase (as ++ bs) ~ (Erase as ++ Erase bs)) =>
((Erase (Wire s : (as ++ bs))
  ~ (Erase (Wire s : as) ++ Erase bs)) =>
 r)
-> r
withEraseAppendCons (Erase (Wire s : (as ++ bs))
 ~ (Erase (Wire s : as) ++ Erase bs)) =>
r
r = r
(Erase (Wire s : (as ++ bs))
 ~ (Erase (Wire s : as) ++ Erase bs)) =>
r
r
  withDualDualW :: forall r. ((DualW (DualW (Wire s)) ~ Wire s) => r) -> r
withDualDualW (DualW (DualW (Wire s)) ~ Wire s) => r
r = r
(DualW (DualW (Wire s)) ~ Wire s) => r
r
  withEraseDualCons :: forall (ws :: [W]) r.
(Erase (DualList ws) ~ Erase ws) =>
((Erase (DualList (Wire s : ws)) ~ Erase (Wire s : ws)) => r) -> r
withEraseDualCons (Erase (DualList (Wire s : ws)) ~ Erase (Wire s : ws)) => r
r = r
(Erase (DualList (Wire s : ws)) ~ Erase (Wire s : ws)) => r
r

instance (KnownSymbol s) => KnownWire (Co s) where
  wireInfo :: (String, WireKind)
wireInfo = (Proxy s -> 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]
++ String
"⁻¹", WireKind
DualWire)
  withKnownDualW :: forall r. (KnownWire (DualW (Co s)) => r) -> r
withKnownDualW KnownWire (DualW (Co s)) => r
r = r
KnownWire (DualW (Co s)) => r
r
  withIsListEraseCons :: forall (ws :: [W]) r.
IsList (Erase ws) =>
(IsList (Erase (Co s : ws)) => r) -> r
withIsListEraseCons @ws IsList (Erase (Co s : ws)) => 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 @'[s] @(Erase ws) r
IsList ('[s] ++ Erase ws) => r
IsList (Erase (Co s : ws)) => r
r
  withEraseAppendCons :: forall (as :: [W]) (bs :: [W]) r.
(Erase (as ++ bs) ~ (Erase as ++ Erase bs)) =>
((Erase (Co s : (as ++ bs)) ~ (Erase (Co s : as) ++ Erase bs)) =>
 r)
-> r
withEraseAppendCons (Erase (Co s : (as ++ bs)) ~ (Erase (Co s : as) ++ Erase bs)) => r
r = r
(Erase (Co s : (as ++ bs)) ~ (Erase (Co s : as) ++ Erase bs)) => r
r
  withDualDualW :: forall r. ((DualW (DualW (Co s)) ~ Co s) => r) -> r
withDualDualW (DualW (DualW (Co s)) ~ Co s) => r
r = r
(DualW (DualW (Co s)) ~ Co s) => r
r
  withEraseDualCons :: forall (ws :: [W]) r.
(Erase (DualList ws) ~ Erase ws) =>
((Erase (DualList (Co s : ws)) ~ Erase (Co s : ws)) => r) -> r
withEraseDualCons (Erase (DualList (Co s : ws)) ~ Erase (Co s : ws)) => r
r = r
(Erase (DualList (Co s : ws)) ~ Erase (Co s : ws)) => r
r

instance KnownWire I where
  wireInfo :: (String, WireKind)
wireInfo = (String
"𝐈", WireKind
UnitWire)
  withKnownDualW :: forall r. (KnownWire (DualW I) => r) -> r
withKnownDualW KnownWire (DualW I) => r
r = r
KnownWire (DualW I) => r
r
  withIsListEraseCons :: forall (ws :: [W]) r.
IsList (Erase ws) =>
(IsList (Erase (I : ws)) => r) -> r
withIsListEraseCons IsList (Erase (I : ws)) => r
r = r
IsList (Erase (I : ws)) => r
r
  withEraseAppendCons :: forall (as :: [W]) (bs :: [W]) r.
(Erase (as ++ bs) ~ (Erase as ++ Erase bs)) =>
((Erase (I : (as ++ bs)) ~ (Erase (I : as) ++ Erase bs)) => r) -> r
withEraseAppendCons (Erase (I : (as ++ bs)) ~ (Erase (I : as) ++ Erase bs)) => r
r = r
(Erase (I : (as ++ bs)) ~ (Erase (I : as) ++ Erase bs)) => r
r
  withDualDualW :: forall r. ((DualW (DualW I) ~ I) => r) -> r
withDualDualW (DualW (DualW I) ~ I) => r
r = r
(DualW (DualW I) ~ I) => r
r
  withEraseDualCons :: forall (ws :: [W]) r.
(Erase (DualList ws) ~ Erase ws) =>
((Erase (DualList (I : ws)) ~ Erase (I : ws)) => r) -> r
withEraseDualCons (Erase (DualList (I : ws)) ~ Erase (I : ws)) => r
r = r
(Erase (DualList (I : ws)) ~ Erase (I : ws)) => r
r

type WireId :: CAT W
data WireId a b where
  WireId :: (KnownWire w) => WireId w w
instance Profunctor WireId where
  dimap :: forall (c :: W) (a :: W) (b :: W) (d :: W).
(c ~> a) -> (b ~> d) -> WireId a b -> WireId c d
dimap = (c ~> a) -> (b ~> d) -> WireId a b -> WireId c d
WireId c a -> WireId b d -> WireId a b -> WireId 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 :: W) (b :: W) r. ((Ob a, Ob b) => r) -> WireId a b -> r
\\ WireId a b
WireId = r
(Ob a, Ob b) => r
r
instance Promonad WireId where
  id :: forall (a :: W). Ob a => WireId a a
id = WireId a a
forall (w :: W). KnownWire w => WireId w w
WireId
  WireId b c
WireId . :: forall (b :: W) (c :: W) (a :: W).
WireId b c -> WireId a b -> WireId a c
. WireId a b
WireId = WireId a c
WireId a a
forall (w :: W). KnownWire w => WireId w w
WireId

-- | The discrete category on wires, so that lists of wires are objects of 'Strictified'.
instance CategoryOf W where
  type (~>) = WireId
  type Ob w = KnownWire w

-- | The duals of a list of wires are a list of wires.
withIsListDual :: forall (ws :: [W]) r. (IsList ws) => ((IsList (DualList ws)) => r) -> r
withIsListDual :: forall (ws :: [W]) r. IsList ws => (IsList (DualList ws) => r) -> r
withIsListDual IsList (DualList ws) => r
r =
  forall (as :: [W]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: W). (Ob a, as ~ '[a]) => r)
-> (forall (b :: W) (bs :: [W]) (c :: W) (cs :: [W]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
forall {k} (as :: [k]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
listCase @ws
    r
(ws ~ '[]) => r
IsList (DualList ws) => r
r
    (\ @w -> forall (w :: W) r. KnownWire w => (KnownWire (DualW w) => r) -> r
withKnownDualW @w r
IsList (DualList ws) => r
KnownWire (DualW a) => r
r)
    (\ @b @bs @c @cs -> forall (w :: W) r. KnownWire w => (KnownWire (DualW w) => r) -> r
withKnownDualW @b (forall (w :: W) r. KnownWire w => (KnownWire (DualW w) => r) -> r
withKnownDualW @c (forall (ws :: [W]) r. IsList ws => (IsList (DualList ws) => r) -> r
withIsListDual @cs (forall (ws :: [W]) r. IsList ws => (IsList (DualList ws) => r) -> r
withIsListDual @bs r
IsList (DualList ws) => r
IsList (DualList bs) => r
r))))

-- | The erased wires of a list of wires are a list of labels.
withIsListErase :: forall (ws :: [W]) r. (IsList ws) => ((IsList (Erase ws)) => r) -> r
withIsListErase :: forall (ws :: [W]) r. IsList ws => (IsList (Erase ws) => r) -> r
withIsListErase IsList (Erase ws) => r
r =
  forall (as :: [W]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: W). (Ob a, as ~ '[a]) => r)
-> (forall (b :: W) (bs :: [W]) (c :: W) (cs :: [W]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
forall {k} (as :: [k]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
listCase @ws
    r
(ws ~ '[]) => r
IsList (Erase ws) => r
r
    (\ @w -> forall (w :: W) (ws :: [W]) r.
(KnownWire w, IsList (Erase ws)) =>
(IsList (Erase (w : ws)) => r) -> r
withIsListEraseCons @w @'[] r
IsList (Erase ws) => r
IsList (Erase '[a]) => r
r)
    (\ @w @ws' -> forall (ws :: [W]) r. IsList ws => (IsList (Erase ws) => r) -> r
withIsListErase @ws' (forall (w :: W) (ws :: [W]) r.
(KnownWire w, IsList (Erase ws)) =>
(IsList (Erase (w : ws)) => r) -> r
withIsListEraseCons @w @ws' r
IsList (Erase ws) => r
IsList (Erase (b : bs)) => r
r))

-- | Erasing commutes with appending.
withEraseAppend
  :: forall (as :: [W]) (bs :: [W]) r. (IsList as) => ((Erase (as ++ bs) ~ (Erase as ++ Erase bs)) => r) -> r
withEraseAppend :: forall (as :: [W]) (bs :: [W]) r.
IsList as =>
((Erase (as ++ bs) ~ (Erase as ++ Erase bs)) => r) -> r
withEraseAppend (Erase (as ++ bs) ~ (Erase as ++ Erase bs)) => r
r =
  forall (as :: [W]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: W). (Ob a, as ~ '[a]) => r)
-> (forall (b :: W) (bs :: [W]) (c :: W) (cs :: [W]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
forall {k} (as :: [k]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
listCase @as
    r
(Erase (as ++ bs) ~ (Erase as ++ Erase bs)) => r
(as ~ '[]) => r
r
    (\ @w -> forall (w :: W) (as :: [W]) (bs :: [W]) r.
(KnownWire w, Erase (as ++ bs) ~ (Erase as ++ Erase bs)) =>
((Erase (w : (as ++ bs)) ~ (Erase (w : as) ++ Erase bs)) => r) -> r
withEraseAppendCons @w @'[] @bs r
(Erase (a : ('[] ++ bs)) ~ (Erase '[a] ++ Erase bs)) => r
(Erase (as ++ bs) ~ (Erase as ++ Erase bs)) => r
r)
    (\ @w @as' -> forall (as :: [W]) (bs :: [W]) r.
IsList as =>
((Erase (as ++ bs) ~ (Erase as ++ Erase bs)) => r) -> r
withEraseAppend @as' @bs (forall (w :: W) (as :: [W]) (bs :: [W]) r.
(KnownWire w, Erase (as ++ bs) ~ (Erase as ++ Erase bs)) =>
((Erase (w : (as ++ bs)) ~ (Erase (w : as) ++ Erase bs)) => r) -> r
withEraseAppendCons @w @as' @bs r
(Erase (b : (bs ++ bs)) ~ (Erase (b : bs) ++ Erase bs)) => r
(Erase (as ++ bs) ~ (Erase as ++ Erase bs)) => r
r))

-- | Dualising twice gives the wires back.
withDualDual :: forall (ws :: [W]) r. (IsList ws) => ((DualList (DualList ws) ~ ws) => r) -> r
withDualDual :: forall (ws :: [W]) r.
IsList ws =>
((DualList (DualList ws) ~ ws) => r) -> r
withDualDual (DualList (DualList ws) ~ ws) => r
r =
  forall (as :: [W]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: W). (Ob a, as ~ '[a]) => r)
-> (forall (b :: W) (bs :: [W]) (c :: W) (cs :: [W]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
forall {k} (as :: [k]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
listCase @ws
    r
(ws ~ '[]) => r
(DualList (DualList ws) ~ ws) => r
r
    (\ @w -> forall (w :: W) r. KnownWire w => ((DualW (DualW w) ~ w) => r) -> r
withDualDualW @w r
(DualList (DualList ws) ~ ws) => r
(DualW (DualW a) ~ a) => r
r)
    (\ @w @ws' -> forall (ws :: [W]) r.
IsList ws =>
((DualList (DualList ws) ~ ws) => r) -> r
withDualDual @ws' (forall (w :: W) r. KnownWire w => ((DualW (DualW w) ~ w) => r) -> r
withDualDualW @w r
(DualList (DualList ws) ~ ws) => r
(DualW (DualW b) ~ b) => r
r))

-- | Dualising commutes with appending.
withDualAppend
  :: forall (as :: [W]) (bs :: [W]) r. (IsList as) => ((DualList (as ++ bs) ~ (DualList as ++ DualList bs)) => r) -> r
withDualAppend :: forall (as :: [W]) (bs :: [W]) r.
IsList as =>
((DualList (as ++ bs) ~ (DualList as ++ DualList bs)) => r) -> r
withDualAppend (DualList (as ++ bs) ~ (DualList as ++ DualList bs)) => r
r = forall (as :: [W]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: W). (Ob a, as ~ '[a]) => r)
-> (forall (b :: W) (bs :: [W]) (c :: W) (cs :: [W]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
forall {k} (as :: [k]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
listCase @as r
(as ~ '[]) => r
(DualList (as ++ bs) ~ (DualList as ++ DualList bs)) => r
r r
(DualList (as ++ bs) ~ (DualList as ++ DualList bs)) => r
forall (a :: W). (Ob a, as ~ '[a]) => r
r (\ @_ @as' -> forall (as :: [W]) (bs :: [W]) r.
IsList as =>
((DualList (as ++ bs) ~ (DualList as ++ DualList bs)) => r) -> r
withDualAppend @as' @bs r
(DualList (as ++ bs) ~ (DualList as ++ DualList bs)) => r
(DualList (bs ++ bs) ~ (DualList bs ++ DualList bs)) => r
r)

-- | The duals of wires erase to the same labels as the wires.
withEraseDual :: forall (ws :: [W]) r. (IsList ws) => ((Erase (DualList ws) ~ Erase ws) => r) -> r
withEraseDual :: forall (ws :: [W]) r.
IsList ws =>
((Erase (DualList ws) ~ Erase ws) => r) -> r
withEraseDual (Erase (DualList ws) ~ Erase ws) => r
r =
  forall (as :: [W]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: W). (Ob a, as ~ '[a]) => r)
-> (forall (b :: W) (bs :: [W]) (c :: W) (cs :: [W]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
forall {k} (as :: [k]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
listCase @ws
    r
(Erase (DualList ws) ~ Erase ws) => r
(ws ~ '[]) => r
r
    (\ @w -> forall (w :: W) (ws :: [W]) r.
(KnownWire w, Erase (DualList ws) ~ Erase ws) =>
((Erase (DualList (w : ws)) ~ Erase (w : ws)) => r) -> r
withEraseDualCons @w @'[] r
(Erase (DualList ws) ~ Erase ws) => r
(Erase (DualList '[a]) ~ Erase '[a]) => r
r)
    (\ @w @ws' -> forall (ws :: [W]) r.
IsList ws =>
((Erase (DualList ws) ~ Erase ws) => r) -> r
withEraseDual @ws' (forall (w :: W) (ws :: [W]) r.
(KnownWire w, Erase (DualList ws) ~ Erase ws) =>
((Erase (DualList (w : ws)) ~ Erase (w : ws)) => r) -> r
withEraseDualCons @w @ws' r
(Erase (DualList ws) ~ Erase ws) => r
(Erase (DualList (b : bs)) ~ Erase (b : bs)) => r
r))

-- | The labels of the wires of @ws@ as they are shown, and their kinds.
wires :: forall (ws :: [W]). (IsList ws) => [(String, WireKind)]
wires :: forall (ws :: [W]). IsList ws => [(String, WireKind)]
wires = case forall (as :: [W]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
sList @ws of
  SList ws
SNil -> []
  SSing @w -> [forall (w :: W). KnownWire w => (String, WireKind)
wireInfo @w]
  SCons @w @ws' -> forall (w :: W). KnownWire w => (String, WireKind)
wireInfo @w (String, WireKind) -> [(String, WireKind)] -> [(String, WireKind)]
forall a. a -> [a] -> [a]
: forall (ws :: [W]). IsList ws => [(String, WireKind)]
wires @ws'

wireKinds :: forall (ws :: [W]). (IsList ws) => [WireKind]
wireKinds :: forall (ws :: [W]). IsList ws => [WireKind]
wireKinds = ((String, WireKind) -> WireKind)
-> [(String, WireKind)] -> [WireKind]
forall a b. (a -> b) -> [a] -> [b]
map (String, WireKind) -> WireKind
forall a b. (a, b) -> b
snd (forall (ws :: [W]). IsList ws => [(String, WireKind)]
wires @ws)

-- * The category

type SVG :: Kind
type data SVG = S [W]

-- | A diagram: its meaning, as a 'Dot' diagram on the erased wires, and how it was built, which
-- is drawn when it is rendered.
type Svg :: CAT SVG
data Svg a b where
  Svg :: (IsList as, IsList bs) => Dot (Dot.D (Erase as)) (Dot.D (Erase bs)) -> Diagram -> Svg (S as) (S bs)

-- | A diagram from its meaning, which may use that the erased wires are lists, and how it is
-- drawn.
svg
  :: forall (as :: [W]) (bs :: [W])
   . (IsList as, IsList bs)
  => ((IsList (Erase as), IsList (Erase bs)) => Dot (Dot.D (Erase as)) (Dot.D (Erase bs)))
  -> Diagram
  -> Svg (S as) (S bs)
svg :: forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs) =>
((IsList (Erase as), IsList (Erase bs)) =>
 Dot (D (Erase as)) (D (Erase bs)))
-> Diagram -> Svg (S as) (S bs)
svg (IsList (Erase as), IsList (Erase bs)) =>
Dot (D (Erase as)) (D (Erase bs))
d = forall (ws :: [W]) r. IsList ws => (IsList (Erase ws) => r) -> r
withIsListErase @as (forall (ws :: [W]) r. IsList ws => (IsList (Erase ws) => r) -> r
withIsListErase @bs (Dot (D (Erase as)) (D (Erase bs)) -> Diagram -> Svg (S as) (S bs)
forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs) =>
Dot (D (Erase as)) (D (Erase bs)) -> Diagram -> Svg (S as) (S bs)
Svg Dot (D (Erase as)) (D (Erase bs))
(IsList (Erase as), IsList (Erase bs)) =>
Dot (D (Erase as)) (D (Erase bs))
d))

-- | A diagram that means the identity on the erased wires, drawn as given.
drawnAs :: forall (as :: [W]) (bs :: [W]). (IsList as, IsList bs, Erase as ~ Erase bs) => Diagram -> Svg (S as) (S bs)
drawnAs :: forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs, Erase as ~ Erase bs) =>
Diagram -> Svg (S as) (S bs)
drawnAs = forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs) =>
((IsList (Erase as), IsList (Erase bs)) =>
 Dot (D (Erase as)) (D (Erase bs)))
-> Diagram -> Svg (S as) (S bs)
svg @as @bs (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: DOT). (CategoryOf DOT, Ob a) => Obj a
obj @(Dot.D (Erase as)))

-- | An arrow between wires that erase to the same labels, a wire and its dual for example: in
-- meaning the identity. It is drawn as nothing, the wires carrying on in the style of their new
-- kinds.
relabel :: forall (a :: SVG) (b :: SVG). (Ob a, Ob b, Erase (UN S a) ~ Erase (UN S b)) => a ~> b
relabel :: forall (a :: SVG) (b :: SVG).
(Ob a, Ob b, Erase (UN S a) ~ Erase (UN S b)) =>
a ~> b
relabel = Diagram -> Svg (S (UN S a)) (S (UN S b))
forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs, Erase as ~ Erase bs) =>
Diagram -> Svg (S as) (S bs)
drawnAs ([WireKind] -> [WireKind] -> Diagram
Straight (forall (ws :: [W]). IsList ws => [WireKind]
wireKinds @(UN S a)) (forall (ws :: [W]). IsList ws => [WireKind]
wireKinds @(UN S b)))

-- | Choices about what to draw.
data Options = Options
  { Options -> Bool
explicitIdentities :: Bool
  -- ^ draw each identity, 'line' included, as a wire in a dashed frame; otherwise an identity is
  -- not drawn at all
  , Options -> Bool
explicitCoherence :: Bool
  -- ^ draw the unit wires dotted, the unitors as a unit wire running into another wire or out of
  -- it, and the associators with brackets for the groupings they go between; otherwise none of
  -- these are drawn, and unit wires take up no room
  , Options -> Bool
explicitSwaps :: Bool
  -- ^ draw each 'swap' as a crossing of its own; otherwise its crossing is drawn in the band
  -- where the wires next change position
  , Options -> Bool
fixedSpiders :: Bool
  -- ^ keep the two legs of a copy or merge point in the order they are listed; otherwise they
  -- may trade places to avoid a crossing, which the points being commutative allows
  }
  deriving (Int -> Options -> String -> String
[Options] -> String -> String
Options -> String
(Int -> Options -> String -> String)
-> (Options -> String)
-> ([Options] -> String -> String)
-> Show Options
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Options -> String -> String
showsPrec :: Int -> Options -> String -> String
$cshow :: Options -> String
show :: Options -> String
$cshowList :: [Options] -> String -> String
showList :: [Options] -> String -> String
Show)

-- | Nothing drawn that the meaning does not need, legs in order.
defaultOptions :: Options
defaultOptions :: Options
defaultOptions = Options{explicitIdentities :: Bool
explicitIdentities = Bool
False, explicitCoherence :: Bool
explicitCoherence = Bool
False, explicitSwaps :: Bool
explicitSwaps = Bool
False, fixedSpiders :: Bool
fixedSpiders = Bool
True}

-- | The meaning of a diagram, forgetting how it is drawn.
meaningOf :: Svg (S as) (S bs) -> Dot (Dot.D (Erase as)) (Dot.D (Erase bs))
meaningOf :: forall (as :: [W]) (bs :: [W]).
Svg (S as) (S bs) -> Dot (D (Erase as)) (D (Erase bs))
meaningOf (Svg Dot (D (Erase as)) (D (Erase bs))
d Diagram
_) = Dot (D (Erase as)) (D (Erase bs))
Dot (D (Erase as)) (D (Erase bs))
d

instance Show (Svg a b) where
  show :: Svg a b -> String
show (Svg Dot (D (Erase as)) (D (Erase bs))
d Diagram
_) = Dot (D (Erase as)) (D (Erase bs)) -> String
forall a. Show a => a -> String
show Dot (D (Erase as)) (D (Erase bs))
d

instance Profunctor Svg where
  dimap :: forall (c :: SVG) (a :: SVG) (b :: SVG) (d :: SVG).
(c ~> a) -> (b ~> d) -> Svg a b -> Svg c d
dimap = (c ~> a) -> (b ~> d) -> Svg a b -> Svg c d
Svg c a -> Svg b d -> Svg a b -> Svg 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 :: SVG) (b :: SVG) r. ((Ob a, Ob b) => r) -> Svg a b -> r
\\ Svg{} = r
(Ob a, Ob b) => r
r
instance Promonad Svg where
  id :: forall (a :: SVG). Ob a => Svg a a
id @(S as) = forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs, Erase as ~ Erase bs) =>
Diagram -> Svg (S as) (S bs)
drawnAs @as @as ([WireKind] -> Diagram
Ident (forall (ws :: [W]). IsList ws => [WireKind]
wireKinds @as))
  Svg Dot (D (Erase as)) (D (Erase bs))
f Diagram
l . :: forall (b :: SVG) (c :: SVG) (a :: SVG).
Svg b c -> Svg a b -> Svg a c
. Svg Dot (D (Erase as)) (D (Erase bs))
g Diagram
m = Dot (D (Erase as)) (D (Erase bs)) -> Diagram -> Svg (S as) (S bs)
forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs) =>
Dot (D (Erase as)) (D (Erase bs)) -> Diagram -> Svg (S as) (S bs)
Svg (Dot (D (Erase as)) (D (Erase bs))
f Dot (D (Erase as)) (D (Erase bs))
-> Dot (D (Erase as)) (D (Erase as))
-> Dot (D (Erase as)) (D (Erase bs))
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: DOT) (c :: DOT) (a :: DOT).
Dot b c -> Dot a b -> Dot a c
. Dot (D (Erase as)) (D (Erase as))
Dot (D (Erase as)) (D (Erase bs))
g) (Diagram -> Diagram -> Diagram
Seq Diagram
m Diagram
l)

-- | The category string diagrams are drawn in: an object @'S' ws@ is the list of wires along a
-- boundary.
instance CategoryOf SVG where
  type (~>) = Svg
  type Ob a = (Is S a, IsList (UN S a))

instance MonoidalProfunctor Svg where
  one :: Svg Unit Unit
one = Diagram -> Svg (S '[I]) (S '[I])
forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs, Erase as ~ Erase bs) =>
Diagram -> Svg (S as) (S bs)
drawnAs ([WireKind] -> Diagram
Ident [WireKind
UnitWire])
  Svg @lis @los Dot (D (Erase as)) (D (Erase bs))
f Diagram
l ** :: forall (x1 :: SVG) (x2 :: SVG) (y1 :: SVG) (y2 :: SVG).
Svg x1 x2 -> Svg y1 y2 -> Svg (x1 ** y1) (x2 ** y2)
** Svg @ris @ros Dot (D (Erase as)) (D (Erase bs))
g Diagram
m =
    forall (as :: [W]) (bs :: [W]) 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) => Svg (x1 ** y1) (x2 ** y2))
 -> Svg (x1 ** y1) (x2 ** y2))
-> (IsList (as ++ as) => Svg (x1 ** y1) (x2 ** y2))
-> Svg (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$
      forall (as :: [W]) (bs :: [W]) 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) => Svg (x1 ** y1) (x2 ** y2))
 -> Svg (x1 ** y1) (x2 ** y2))
-> (IsList (bs ++ bs) => Svg (x1 ** y1) (x2 ** y2))
-> Svg (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$
        forall (as :: [W]) (bs :: [W]) r.
IsList as =>
((Erase (as ++ bs) ~ (Erase as ++ Erase bs)) => r) -> r
withEraseAppend @lis @ris (((Erase (as ++ as) ~ (Erase as ++ Erase as)) =>
  Svg (x1 ** y1) (x2 ** y2))
 -> Svg (x1 ** y1) (x2 ** y2))
-> ((Erase (as ++ as) ~ (Erase as ++ Erase as)) =>
    Svg (x1 ** y1) (x2 ** y2))
-> Svg (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$
          forall (as :: [W]) (bs :: [W]) r.
IsList as =>
((Erase (as ++ bs) ~ (Erase as ++ Erase bs)) => r) -> r
withEraseAppend @los @ros (((Erase (bs ++ bs) ~ (Erase bs ++ Erase bs)) =>
  Svg (x1 ** y1) (x2 ** y2))
 -> Svg (x1 ** y1) (x2 ** y2))
-> ((Erase (bs ++ bs) ~ (Erase bs ++ Erase bs)) =>
    Svg (x1 ** y1) (x2 ** y2))
-> Svg (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$
            Dot (D (Erase (as ++ as))) (D (Erase (bs ++ bs)))
-> Diagram -> Svg (S (as ++ as)) (S (bs ++ bs))
forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs) =>
Dot (D (Erase as)) (D (Erase bs)) -> Diagram -> Svg (S as) (S bs)
Svg (Dot (D (Erase as)) (D (Erase bs))
f Dot (D (Erase as)) (D (Erase bs))
-> Dot (D (Erase as)) (D (Erase bs))
-> Dot
     (D (Erase as) ** D (Erase as)) (D (Erase bs) ** D (Erase bs))
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)
** Dot (D (Erase as)) (D (Erase bs))
g) (Diagram -> Diagram -> Diagram
Beside Diagram
l Diagram
m)

-- | The unit is the unit wire, and the unitors absorb or create it.
instance Monoidal SVG where
  type Unit = S '[I]
  type ls ** rs = S (UN S ls ++ UN S rs)
  withOb2 :: forall (a :: SVG) (b :: SVG) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @(S ls) @(S rs) Ob (a ** b) => r
r = forall (as :: [W]) (bs :: [W]) 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 S a ++ UN S b) => r
r
  leftUnitor :: forall (a :: SVG). Ob a => (Unit ** a) ~> a
leftUnitor @(S as) = forall (as :: [W]) (bs :: [W]) 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 @'[I] @as ((IsList ('[I] ++ UN S a) => (Unit ** a) ~> a) -> (Unit ** a) ~> a)
-> (IsList ('[I] ++ UN S a) => (Unit ** a) ~> a)
-> (Unit ** a) ~> a
forall a b. (a -> b) -> a -> b
$ Diagram -> Svg (S (I : UN S a)) (S (UN S a))
forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs, Erase as ~ Erase bs) =>
Diagram -> Svg (S as) (S bs)
drawnAs (Side -> Direction -> [WireKind] -> Diagram
Unitor Side
OnLeft Direction
Absorb (forall (ws :: [W]). IsList ws => [WireKind]
wireKinds @as))
  leftUnitorInv :: forall (a :: SVG). Ob a => a ~> (Unit ** a)
leftUnitorInv @(S as) = forall (as :: [W]) (bs :: [W]) 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 @'[I] @as ((IsList ('[I] ++ UN S a) => a ~> (Unit ** a)) -> a ~> (Unit ** a))
-> (IsList ('[I] ++ UN S a) => a ~> (Unit ** a))
-> a ~> (Unit ** a)
forall a b. (a -> b) -> a -> b
$ Diagram -> Svg (S (UN S a)) (S (I : UN S a))
forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs, Erase as ~ Erase bs) =>
Diagram -> Svg (S as) (S bs)
drawnAs (Side -> Direction -> [WireKind] -> Diagram
Unitor Side
OnLeft Direction
Create (forall (ws :: [W]). IsList ws => [WireKind]
wireKinds @as))
  rightUnitor :: forall (a :: SVG). Ob a => (a ** Unit) ~> a
rightUnitor @(S as) = forall (as :: [W]) r.
IsList as =>
((IsList (as ++ '[I]), Erase (as ++ '[I]) ~ Erase as) => r) -> r
withRightUnit @as (((IsList (UN S a ++ '[I]),
   Erase (UN S a ++ '[I]) ~ Erase (UN S a)) =>
  (a ** Unit) ~> a)
 -> (a ** Unit) ~> a)
-> ((IsList (UN S a ++ '[I]),
     Erase (UN S a ++ '[I]) ~ Erase (UN S a)) =>
    (a ** Unit) ~> a)
-> (a ** Unit) ~> a
forall a b. (a -> b) -> a -> b
$ Diagram -> Svg (S (UN S a ++ '[I])) (S (UN S a))
forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs, Erase as ~ Erase bs) =>
Diagram -> Svg (S as) (S bs)
drawnAs (Side -> Direction -> [WireKind] -> Diagram
Unitor Side
OnRight Direction
Absorb (forall (ws :: [W]). IsList ws => [WireKind]
wireKinds @as))
  rightUnitorInv :: forall (a :: SVG). Ob a => a ~> (a ** Unit)
rightUnitorInv @(S as) = forall (as :: [W]) r.
IsList as =>
((IsList (as ++ '[I]), Erase (as ++ '[I]) ~ Erase as) => r) -> r
withRightUnit @as (((IsList (UN S a ++ '[I]),
   Erase (UN S a ++ '[I]) ~ Erase (UN S a)) =>
  a ~> (a ** Unit))
 -> a ~> (a ** Unit))
-> ((IsList (UN S a ++ '[I]),
     Erase (UN S a ++ '[I]) ~ Erase (UN S a)) =>
    a ~> (a ** Unit))
-> a ~> (a ** Unit)
forall a b. (a -> b) -> a -> b
$ Diagram -> Svg (S (UN S a)) (S (UN S a ++ '[I]))
forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs, Erase as ~ Erase bs) =>
Diagram -> Svg (S as) (S bs)
drawnAs (Side -> Direction -> [WireKind] -> Diagram
Unitor Side
OnRight Direction
Create (forall (ws :: [W]). IsList ws => [WireKind]
wireKinds @as))
  associator :: forall (a :: SVG) (b :: SVG) (c :: SVG).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @(S as) @(S bs) @(S cs) = forall (as :: [W]) (bs :: [W]) (cs :: [W]).
(IsList as, IsList bs, IsList cs) =>
Grouping -> Svg (S (as ++ (bs ++ cs))) (S (as ++ (bs ++ cs)))
rebracketed @as @bs @cs Grouping
LeftFirst
  associatorInv :: forall (a :: SVG) (b :: SVG) (c :: SVG).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @(S as) @(S bs) @(S cs) = forall (as :: [W]) (bs :: [W]) (cs :: [W]).
(IsList as, IsList bs, IsList cs) =>
Grouping -> Svg (S (as ++ (bs ++ cs))) (S (as ++ (bs ++ cs)))
rebracketed @as @bs @cs Grouping
RightFirst

-- | Wires with a unit wire on the right are a list, and erase to the same labels.
withRightUnit :: forall (as :: [W]) r. (IsList as) => ((IsList (as ++ '[I]), Erase (as ++ '[I]) ~ Erase as) => r) -> r
withRightUnit :: forall (as :: [W]) r.
IsList as =>
((IsList (as ++ '[I]), Erase (as ++ '[I]) ~ Erase as) => r) -> r
withRightUnit (IsList (as ++ '[I]), Erase (as ++ '[I]) ~ Erase as) => r
r = forall (as :: [W]) (bs :: [W]) 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 @'[I] ((IsList (as ++ '[I]) => r) -> r)
-> (IsList (as ++ '[I]) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall (as :: [W]) (bs :: [W]) r.
IsList as =>
((Erase (as ++ bs) ~ (Erase as ++ Erase bs)) => r) -> r
withEraseAppend @as @'[I] (((Erase (as ++ '[I]) ~ (Erase as ++ Erase '[I])) => r) -> r)
-> ((Erase (as ++ '[I]) ~ (Erase as ++ Erase '[I])) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall (ws :: [W]) r. IsList ws => (IsList (Erase ws) => r) -> r
withIsListErase @as r
IsList (Erase as) => r
(IsList (as ++ '[I]), Erase (as ++ '[I]) ~ Erase as) => r
r

-- | An associator, from the given grouping to the other one.
rebracketed
  :: forall (as :: [W]) (bs :: [W]) (cs :: [W])
   . (IsList as, IsList bs, IsList cs)
  => Grouping
  -> Svg (S (as ++ (bs ++ cs))) (S (as ++ (bs ++ cs)))
rebracketed :: forall (as :: [W]) (bs :: [W]) (cs :: [W]).
(IsList as, IsList bs, IsList cs) =>
Grouping -> Svg (S (as ++ (bs ++ cs))) (S (as ++ (bs ++ cs)))
rebracketed Grouping
g =
  forall (as :: [W]) (bs :: [W]) 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 @cs ((IsList (bs ++ cs) =>
  Svg (S (as ++ (bs ++ cs))) (S (as ++ (bs ++ cs))))
 -> Svg (S (as ++ (bs ++ cs))) (S (as ++ (bs ++ cs))))
-> (IsList (bs ++ cs) =>
    Svg (S (as ++ (bs ++ cs))) (S (as ++ (bs ++ cs))))
-> Svg (S (as ++ (bs ++ cs))) (S (as ++ (bs ++ cs)))
forall a b. (a -> b) -> a -> b
$
    forall (as :: [W]) (bs :: [W]) 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 ++ cs) ((IsList (as ++ (bs ++ cs)) =>
  Svg (S (as ++ (bs ++ cs))) (S (as ++ (bs ++ cs))))
 -> Svg (S (as ++ (bs ++ cs))) (S (as ++ (bs ++ cs))))
-> (IsList (as ++ (bs ++ cs)) =>
    Svg (S (as ++ (bs ++ cs))) (S (as ++ (bs ++ cs))))
-> Svg (S (as ++ (bs ++ cs))) (S (as ++ (bs ++ cs)))
forall a b. (a -> b) -> a -> b
$
      Diagram -> Svg (S (as ++ (bs ++ cs))) (S (as ++ (bs ++ cs)))
forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs, Erase as ~ Erase bs) =>
Diagram -> Svg (S as) (S bs)
drawnAs (Grouping -> [WireKind] -> [WireKind] -> [WireKind] -> Diagram
Rebracket Grouping
g (forall (ws :: [W]). IsList ws => [WireKind]
wireKinds @as) (forall (ws :: [W]). IsList ws => [WireKind]
wireKinds @bs) (forall (ws :: [W]). IsList ws => [WireKind]
wireKinds @cs))

instance SymMonoidal SVG where
  swap :: forall (a :: SVG) (b :: SVG). (Ob a, Ob b) => (a ** b) ~> (b ** a)
swap @(S as) @(S bs) =
    forall (as :: [W]) (bs :: [W]) 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 S a ++ UN S b) => (a ** b) ~> (b ** a))
 -> (a ** b) ~> (b ** a))
-> (IsList (UN S a ++ UN S b) => (a ** b) ~> (b ** a))
-> (a ** b) ~> (b ** a)
forall a b. (a -> b) -> a -> b
$
      forall (as :: [W]) (bs :: [W]) 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 S b ++ UN S a) => (a ** b) ~> (b ** a))
 -> (a ** b) ~> (b ** a))
-> (IsList (UN S b ++ UN S a) => (a ** b) ~> (b ** a))
-> (a ** b) ~> (b ** a)
forall a b. (a -> b) -> a -> b
$
        forall (as :: [W]) (bs :: [W]) r.
IsList as =>
((Erase (as ++ bs) ~ (Erase as ++ Erase bs)) => r) -> r
withEraseAppend @as @bs (((Erase (UN S a ++ UN S b)
   ~ (Erase (UN S a) ++ Erase (UN S b))) =>
  (a ** b) ~> (b ** a))
 -> (a ** b) ~> (b ** a))
-> ((Erase (UN S a ++ UN S b)
     ~ (Erase (UN S a) ++ Erase (UN S b))) =>
    (a ** b) ~> (b ** a))
-> (a ** b) ~> (b ** a)
forall a b. (a -> b) -> a -> b
$
          forall (as :: [W]) (bs :: [W]) r.
IsList as =>
((Erase (as ++ bs) ~ (Erase as ++ Erase bs)) => r) -> r
withEraseAppend @bs @as (((Erase (UN S b ++ UN S a)
   ~ (Erase (UN S b) ++ Erase (UN S a))) =>
  (a ** b) ~> (b ** a))
 -> (a ** b) ~> (b ** a))
-> ((Erase (UN S b ++ UN S a)
     ~ (Erase (UN S b) ++ Erase (UN S a))) =>
    (a ** b) ~> (b ** a))
-> (a ** b) ~> (b ** a)
forall a b. (a -> b) -> a -> b
$
            forall (ws :: [W]) r. IsList ws => (IsList (Erase ws) => r) -> r
withIsListErase @as ((IsList (Erase (UN S a)) => (a ** b) ~> (b ** a))
 -> (a ** b) ~> (b ** a))
-> (IsList (Erase (UN S a)) => (a ** b) ~> (b ** a))
-> (a ** b) ~> (b ** a)
forall a b. (a -> b) -> a -> b
$
              forall (ws :: [W]) r. IsList ws => (IsList (Erase ws) => r) -> r
withIsListErase @bs ((IsList (Erase (UN S b)) => (a ** b) ~> (b ** a))
 -> (a ** b) ~> (b ** a))
-> (IsList (Erase (UN S b)) => (a ** b) ~> (b ** a))
-> (a ** b) ~> (b ** a)
forall a b. (a -> b) -> a -> b
$
                ((IsList (Erase (UN S a ++ UN S b)),
  IsList (Erase (UN S b ++ UN S a))) =>
 Dot (D (Erase (UN S a ++ UN S b))) (D (Erase (UN S b ++ UN S a))))
-> Diagram -> Svg (S (UN S a ++ UN S b)) (S (UN S b ++ UN S a))
forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs) =>
((IsList (Erase as), IsList (Erase bs)) =>
 Dot (D (Erase as)) (D (Erase bs)))
-> Diagram -> Svg (S as) (S bs)
svg (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @DOT @(Dot.D (Erase as)) @(Dot.D (Erase bs))) (Diagram -> Svg (S (UN S a ++ UN S b)) (S (UN S b ++ UN S a)))
-> Diagram -> Svg (S (UN S a ++ UN S b)) (S (UN S b ++ UN S a))
forall a b. (a -> b) -> a -> b
$
                  Bool -> [WireKind] -> [Int] -> Diagram
Permute Bool
False (forall (ws :: [W]). IsList ws => [WireKind]
wireKinds @(as ++ bs)) ([forall (as :: [W]). IsList as => Int
forall {k} (as :: [k]). IsList as => Int
Dot.len @as .. forall (as :: [W]). IsList as => Int
forall {k} (as :: [k]). IsList as => Int
Dot.len @as Int -> Int -> Int
forall a. Num a => a -> a -> a
+ forall (as :: [W]). IsList as => Int
forall {k} (as :: [k]). IsList as => Int
Dot.len @bs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1] [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int
0 .. forall (as :: [W]). IsList as => Int
forall {k} (as :: [k]). IsList as => Int
Dot.len @as Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1])

-- | The unit point takes the unit wire in, and the discard point gives it out.
instance (Ob as) => Monoid (S as) where
  mempty :: Unit ~> S as
mempty = ((IsList (Erase '[I]), IsList (Erase as)) =>
 Dot (D (Erase '[I])) (D (Erase as)))
-> Diagram -> Svg (S '[I]) (S as)
forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs) =>
((IsList (Erase as), IsList (Erase bs)) =>
 Dot (D (Erase as)) (D (Erase bs)))
-> Diagram -> Svg (S as) (S bs)
svg (forall {k} (m :: k). Monoid m => Unit ~> m
forall (m :: DOT). Monoid m => Unit ~> m
mempty @(Dot.D (Erase as))) (Diagram -> Diagram -> Diagram
Seq Diagram
UnitEnd (PointKind -> [WireKind] -> Diagram
Points PointKind
UnitPoint (forall (ws :: [W]). IsList ws => [WireKind]
wireKinds @as)))
  mappend :: (S as ** S as) ~> S as
mappend = forall (as :: [W]) (bs :: [W]) 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) => (S as ** S as) ~> S as)
 -> (S as ** S as) ~> S as)
-> (IsList (as ++ as) => (S as ** S as) ~> S as)
-> (S as ** S as) ~> S as
forall a b. (a -> b) -> a -> b
$ forall (as :: [W]) (bs :: [W]) r.
IsList as =>
((Erase (as ++ bs) ~ (Erase as ++ Erase bs)) => r) -> r
withEraseAppend @as @as (((Erase (as ++ as) ~ (Erase as ++ Erase as)) =>
  (S as ** S as) ~> S as)
 -> (S as ** S as) ~> S as)
-> ((Erase (as ++ as) ~ (Erase as ++ Erase as)) =>
    (S as ** S as) ~> S as)
-> (S as ** S as) ~> S as
forall a b. (a -> b) -> a -> b
$ ((IsList (Erase (as ++ as)), IsList (Erase as)) =>
 Dot (D (Erase (as ++ as))) (D (Erase as)))
-> Diagram -> Svg (S (as ++ as)) (S as)
forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs) =>
((IsList (Erase as), IsList (Erase bs)) =>
 Dot (D (Erase as)) (D (Erase bs)))
-> Diagram -> Svg (S as) (S bs)
svg (forall {k} (m :: k). Monoid m => (m ** m) ~> m
forall (m :: DOT). Monoid m => (m ** m) ~> m
mappend @(Dot.D (Erase as))) (PointKind -> [WireKind] -> Diagram
Points PointKind
MergePoint (forall (ws :: [W]). IsList ws => [WireKind]
wireKinds @as))

instance (Ob as) => Comonoid (S as) where
  counit :: S as ~> Unit
counit = ((IsList (Erase as), IsList (Erase '[I])) =>
 Dot (D (Erase as)) (D (Erase '[I])))
-> Diagram -> Svg (S as) (S '[I])
forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs) =>
((IsList (Erase as), IsList (Erase bs)) =>
 Dot (D (Erase as)) (D (Erase bs)))
-> Diagram -> Svg (S as) (S bs)
svg (forall {k} (c :: k). Comonoid c => c ~> Unit
forall (c :: DOT). Comonoid c => c ~> Unit
counit @(Dot.D (Erase as))) (Diagram -> Diagram -> Diagram
Seq (PointKind -> [WireKind] -> Diagram
Points PointKind
DiscardPoint (forall (ws :: [W]). IsList ws => [WireKind]
wireKinds @as)) Diagram
UnitStart)
  comult :: S as ~> (S as ** S as)
comult = forall (as :: [W]) (bs :: [W]) 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) => S as ~> (S as ** S as))
 -> S as ~> (S as ** S as))
-> (IsList (as ++ as) => S as ~> (S as ** S as))
-> S as ~> (S as ** S as)
forall a b. (a -> b) -> a -> b
$ forall (as :: [W]) (bs :: [W]) r.
IsList as =>
((Erase (as ++ bs) ~ (Erase as ++ Erase bs)) => r) -> r
withEraseAppend @as @as (((Erase (as ++ as) ~ (Erase as ++ Erase as)) =>
  S as ~> (S as ** S as))
 -> S as ~> (S as ** S as))
-> ((Erase (as ++ as) ~ (Erase as ++ Erase as)) =>
    S as ~> (S as ** S as))
-> S as ~> (S as ** S as)
forall a b. (a -> b) -> a -> b
$ ((IsList (Erase as), IsList (Erase (as ++ as))) =>
 Dot (D (Erase as)) (D (Erase (as ++ as))))
-> Diagram -> Svg (S as) (S (as ++ as))
forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs) =>
((IsList (Erase as), IsList (Erase bs)) =>
 Dot (D (Erase as)) (D (Erase bs)))
-> Diagram -> Svg (S as) (S bs)
svg (forall {k} (c :: k). Comonoid c => c ~> (c ** c)
forall (c :: DOT). Comonoid c => c ~> (c ** c)
comult @(Dot.D (Erase as))) (PointKind -> [WireKind] -> Diagram
Points PointKind
CopyPoint (forall (ws :: [W]). IsList ws => [WireKind]
wireKinds @as))
instance (Ob as) => CocommutativeComonoid (S as)
instance (Ob as) => CommutativeMonoid (S as)
instance (Ob as) => Frobenius (S as)
instance CopyDiscard SVG
instance Hypergraph SVG

-- | The exponential is the *-autonomous one, @'Dual' (a '**' 'Dual' b)@, so curried wires show as
-- duals.
instance Closed SVG where
  type a ~~> b = ExpSA a b
  withObExp :: forall (a :: SVG) (b :: SVG) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @a @b Ob (a ~~> b) => r
r = forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @SVG @b ((Ob (Dual b) => r) -> r) -> (Ob (Dual b) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @SVG @a @(Dual b) ((Ob (a ** Dual b) => r) -> r) -> (Ob (a ** Dual b) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @SVG @(a ** Dual b) r
Ob (a ~~> b) => r
Ob (Dual (a ** Dual b)) => r
r
  curry :: forall (a :: SVG) (b :: SVG) (c :: SVG).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @a @b @c = forall {k} (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> ExpSA b c
forall (a :: SVG) (b :: SVG) (c :: SVG).
(StarAutonomous SVG, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> ExpSA b c
currySA @a @b @c
  apply :: forall (a :: SVG) (b :: SVG). (Ob a, Ob b) => ((a ~~> b) ** a) ~> b
apply @b @c = forall {k} (b :: k) (c :: k).
(StarAutonomous k, Ob b, Ob c) =>
(ExpSA b c ** b) ~> c
forall (b :: SVG) (c :: SVG).
(StarAutonomous SVG, Ob b, Ob c) =>
(ExpSA b c ** b) ~> c
applySA @b @c
  ^^^ :: forall (a :: SVG) (b :: SVG) (x :: SVG) (y :: SVG).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
(^^^) = (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
(b ~> y) -> (x ~> a) -> ExpSA a b ~> ExpSA x y
forall {k} (a :: k) (b :: k) (x :: k) (y :: k).
StarAutonomous k =>
(b ~> y) -> (x ~> a) -> ExpSA a b ~> ExpSA x y
expSA

-- | The dual of a wire is its 'Co' wire. Duals come from 'dualCup' and 'dualCap', which mean a cup
-- or cap and are drawn as a bend, so a dual wire is drawn hollow wherever it runs.
instance StarAutonomous SVG where
  type Dual a = S (DualList (UN S a))
  withObDual :: forall (a :: SVG) r. Ob a => (Ob (Dual a) => r) -> r
withObDual @a Ob (Dual a) => r
r = forall (ws :: [W]) r. IsList ws => (IsList (DualList ws) => r) -> r
withIsListDual @(UN S a) r
Ob (Dual a) => r
IsList (DualList (UN S a)) => r
r
  dual :: forall (a :: SVG) (b :: SVG). (a ~> b) -> Dual b ~> Dual a
dual @a @b a ~> b
f =
    ( forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @SVG @a ((Ob (Dual a) => Fold '[Dual b] ~> Fold '[Dual a])
 -> Fold '[Dual b] ~> Fold '[Dual a])
-> (Ob (Dual a) => Fold '[Dual b] ~> Fold '[Dual a])
-> Fold '[Dual b] ~> Fold '[Dual a]
forall a b. (a -> b) -> a -> b
$
        forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @SVG @b ((Ob (Dual b) => Fold '[Dual b] ~> Fold '[Dual a])
 -> Fold '[Dual b] ~> Fold '[Dual a])
-> (Ob (Dual b) => Fold '[Dual b] ~> Fold '[Dual a])
-> Fold '[Dual b] ~> Fold '[Dual a]
forall a b. (a -> b) -> a -> b
$
          forall (as :: [SVG]) (bs :: [SVG]).
Strictified as bs -> Fold as ~> Fold bs
forall {k} (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
unStr @'[Dual b] @'[Dual a] (Strictified '[Dual b] '[Dual a]
 -> Fold '[Dual b] ~> Fold '[Dual a])
-> Strictified '[Dual b] '[Dual a]
-> Fold '[Dual b] ~> Fold '[Dual a]
forall a b. (a -> b) -> a -> b
$
            Obj '[S (DualList (UN S b))]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 Obj '[S (DualList (UN S b))]
-> ('[] ~> '[S (UN S a), S (DualList (UN S a))])
-> ('[S (DualList (UN S b))] ** '[])
   ~> ('[S (DualList (UN S b))]
       ** '[S (UN S a), S (DualList (UN S a))])
forall (x1 :: [SVG]) (x2 :: [SVG]) (y1 :: [SVG]) (y2 :: [SVG]).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
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 (a :: SVG). Ob a => '[] ~> '[a, Dual a]
dualCupS @a
              (('[S (DualList (UN S b))] ** '[])
 ~> ('[S (DualList (UN S b))]
     ** '[S (UN S a), S (DualList (UN S a))]))
-> (('[S (DualList (UN S b))]
     ** '[S (UN S a), S (DualList (UN S a))])
    ~> (('[S (DualList (UN S b))] ++ '[S (UN S b)])
        ++ '[S (DualList (UN S a))]))
-> ('[S (DualList (UN S b))] ** '[])
   ~> (('[S (DualList (UN S b))] ++ '[S (UN S b)])
       ++ '[S (DualList (UN S a))])
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
M.== Obj '[S (DualList (UN S b))]
Strictified '[S (DualList (UN S b))] '[S (DualList (UN S b))]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 Strictified '[S (DualList (UN S b))] '[S (DualList (UN S b))]
-> Strictified '[S (UN S a)] '[S (UN S b)]
-> Strictified
     ('[S (DualList (UN S b))] ** '[S (UN S a)])
     ('[S (DualList (UN S b))] ** '[S (UN S b)])
forall (x1 :: [SVG]) (x2 :: [SVG]) (y1 :: [SVG]) (y2 :: [SVG]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
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)
** (S (UN S a) ~> S (UN S b)) -> '[S (UN S a)] ~> '[S (UN S b)]
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> '[a] ~> '[b]
singleton a ~> b
S (UN S a) ~> S (UN S b)
f Strictified
  ('[S (DualList (UN S b))] ++ '[S (UN S a)])
  ('[S (DualList (UN S b))] ++ '[S (UN S b)])
-> Strictified '[S (DualList (UN S a))] '[S (DualList (UN S a))]
-> Strictified
     (('[S (DualList (UN S b))] ++ '[S (UN S a)])
      ** '[S (DualList (UN S a))])
     (('[S (DualList (UN S b))] ++ '[S (UN S b)])
      ** '[S (DualList (UN S a))])
forall (x1 :: [SVG]) (x2 :: [SVG]) (y1 :: [SVG]) (y2 :: [SVG]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
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)
** Obj '[S (DualList (UN S a))]
Strictified '[S (DualList (UN S a))] '[S (DualList (UN S a))]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1
              (('[S (DualList (UN S b))] ** '[])
 ~> (('[S (DualList (UN S b))] ++ '[S (UN S b)])
     ++ '[S (DualList (UN S a))]))
-> ((('[S (DualList (UN S b))] ++ '[S (UN S b)])
     ++ '[S (DualList (UN S a))])
    ~> ('[] ++ '[S (DualList (UN S a))]))
-> ('[S (DualList (UN S b))] ** '[])
   ~> ('[] ++ '[S (DualList (UN S a))])
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
M.== forall (a :: SVG). Ob a => '[Dual a, a] ~> '[]
dualCapS @b Strictified '[S (DualList (UN S b)), S (UN S b)] '[]
-> Strictified '[S (DualList (UN S a))] '[S (DualList (UN S a))]
-> Strictified
     ('[S (DualList (UN S b)), S (UN S b)] ** '[S (DualList (UN S a))])
     ('[] ** '[S (DualList (UN S a))])
forall (x1 :: [SVG]) (x2 :: [SVG]) (y1 :: [SVG]) (y2 :: [SVG]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
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)
** Obj '[S (DualList (UN S a))]
Strictified '[S (DualList (UN S a))] '[S (DualList (UN S a))]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1
    )
      ((Ob a, Ob b) => Fold '[Dual b] ~> Fold '[Dual a])
-> Svg a b -> Fold '[Dual b] ~> Fold '[Dual a]
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: SVG) (b :: SVG) r. ((Ob a, Ob b) => r) -> Svg a b -> r
\\ a ~> b
Svg a b
f
  dualInv :: forall (a :: SVG) (b :: SVG).
(Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv @a @b Dual a ~> Dual b
g =
    forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @SVG @a ((Ob (Dual a) => b ~> a) -> b ~> a)
-> (Ob (Dual a) => b ~> a) -> b ~> a
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @SVG @b ((Ob (Dual b) => b ~> a) -> b ~> a)
-> (Ob (Dual b) => b ~> a) -> b ~> a
forall a b. (a -> b) -> a -> b
$
        forall (as :: [SVG]) (bs :: [SVG]).
Strictified as bs -> Fold as ~> Fold bs
forall {k} (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
unStr @'[b] @'[a] (Strictified '[b] '[a] -> Fold '[b] ~> Fold '[a])
-> Strictified '[b] '[a] -> Fold '[b] ~> Fold '[a]
forall a b. (a -> b) -> a -> b
$
          forall (a :: SVG). Ob a => '[] ~> '[a, Dual a]
dualCupS @a ('[] ~> '[S (UN S a), S (DualList (UN S a))])
-> ('[S (UN S b)] ~> '[S (UN S b)])
-> ('[] ** '[S (UN S b)])
   ~> ('[S (UN S a), S (DualList (UN S a))] ** '[S (UN S b)])
forall (x1 :: [SVG]) (x2 :: [SVG]) (y1 :: [SVG]) (y2 :: [SVG]).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
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)
** '[S (UN S b)] ~> '[S (UN S b)]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1
            (('[] ** '[S (UN S b)])
 ~> ('[S (UN S a), S (DualList (UN S a))] ** '[S (UN S b)]))
-> (('[S (UN S a), S (DualList (UN S a))] ** '[S (UN S b)])
    ~> (('[S (UN S a)] ++ '[S (DualList (UN S b))]) ++ '[S (UN S b)]))
-> ('[] ** '[S (UN S b)])
   ~> (('[S (UN S a)] ++ '[S (DualList (UN S b))]) ++ '[S (UN S b)])
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
M.== Obj '[S (UN S a)]
Strictified '[S (UN S a)] '[S (UN S a)]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 Strictified '[S (UN S a)] '[S (UN S a)]
-> Strictified '[S (DualList (UN S a))] '[S (DualList (UN S b))]
-> Strictified
     ('[S (UN S a)] ** '[S (DualList (UN S a))])
     ('[S (UN S a)] ** '[S (DualList (UN S b))])
forall (x1 :: [SVG]) (x2 :: [SVG]) (y1 :: [SVG]) (y2 :: [SVG]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
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)
** (S (DualList (UN S a)) ~> S (DualList (UN S b)))
-> '[S (DualList (UN S a))] ~> '[S (DualList (UN S b))]
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> '[a] ~> '[b]
singleton Dual a ~> Dual b
S (DualList (UN S a)) ~> S (DualList (UN S b))
g Strictified
  ('[S (UN S a)] ++ '[S (DualList (UN S a))])
  ('[S (UN S a)] ++ '[S (DualList (UN S b))])
-> Strictified '[S (UN S b)] '[S (UN S b)]
-> Strictified
     (('[S (UN S a)] ++ '[S (DualList (UN S a))]) ** '[S (UN S b)])
     (('[S (UN S a)] ++ '[S (DualList (UN S b))]) ** '[S (UN S b)])
forall (x1 :: [SVG]) (x2 :: [SVG]) (y1 :: [SVG]) (y2 :: [SVG]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
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)
** '[S (UN S b)] ~> '[S (UN S b)]
Strictified '[S (UN S b)] '[S (UN S b)]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1
            (('[] ** '[S (UN S b)])
 ~> (('[S (UN S a)] ++ '[S (DualList (UN S b))]) ++ '[S (UN S b)]))
-> ((('[S (UN S a)] ++ '[S (DualList (UN S b))]) ++ '[S (UN S b)])
    ~> ('[S (UN S a)] ++ '[]))
-> ('[] ** '[S (UN S b)]) ~> ('[S (UN S a)] ++ '[])
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
M.== Obj '[S (UN S a)]
Strictified '[S (UN S a)] '[S (UN S a)]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 Strictified '[S (UN S a)] '[S (UN S a)]
-> Strictified '[S (DualList (UN S b)), S (UN S b)] '[]
-> Strictified
     ('[S (UN S a)] ** '[S (DualList (UN S b)), S (UN S b)])
     ('[S (UN S a)] ** '[])
forall (x1 :: [SVG]) (x2 :: [SVG]) (y1 :: [SVG]) (y2 :: [SVG]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
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 (a :: SVG). Ob a => '[Dual a, a] ~> '[]
dualCapS @b
  linDist :: forall (a :: SVG) (b :: SVG) (c :: SVG).
(Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist @a @b @c (a ** b) ~> Dual c
f =
    forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @SVG @b ((Ob (Dual b) => a ~> Dual (b ** c)) -> a ~> Dual (b ** c))
-> (Ob (Dual b) => a ~> Dual (b ** c)) -> a ~> Dual (b ** c)
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @SVG @c ((Ob (Dual c) => a ~> Dual (b ** c)) -> a ~> Dual (b ** c))
-> (Ob (Dual c) => a ~> Dual (b ** c)) -> a ~> Dual (b ** c)
forall a b. (a -> b) -> a -> b
$
        forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @SVG @b @c ((Ob (b ** c) => a ~> Dual (b ** c)) -> a ~> Dual (b ** c))
-> (Ob (b ** c) => a ~> Dual (b ** c)) -> a ~> Dual (b ** c)
forall a b. (a -> b) -> a -> b
$
          forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @SVG @(b ** c) ((Ob (Dual (b ** c)) => a ~> Dual (b ** c)) -> a ~> Dual (b ** c))
-> (Ob (Dual (b ** c)) => a ~> Dual (b ** c)) -> a ~> Dual (b ** c)
forall a b. (a -> b) -> a -> b
$
            forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @SVG @(Dual b) @(Dual c) ((Ob (Dual b ** Dual c) => a ~> Dual (b ** c))
 -> a ~> Dual (b ** c))
-> (Ob (Dual b ** Dual c) => a ~> Dual (b ** c))
-> a ~> Dual (b ** c)
forall a b. (a -> b) -> a -> b
$
              forall (as :: [W]) (bs :: [W]) r.
IsList as =>
((DualList (as ++ bs) ~ (DualList as ++ DualList bs)) => r) -> r
withDualAppend @(UN S b) @(UN S c) (((DualList (UN S b ++ UN S c)
   ~ (DualList (UN S b) ++ DualList (UN S c))) =>
  a ~> Dual (b ** c))
 -> a ~> Dual (b ** c))
-> ((DualList (UN S b ++ UN S c)
     ~ (DualList (UN S b) ++ DualList (UN S c))) =>
    a ~> Dual (b ** c))
-> a ~> Dual (b ** c)
forall a b. (a -> b) -> a -> b
$
                forall (a :: SVG) (b :: SVG).
(Ob a, Ob b, Erase (UN S a) ~ Erase (UN S b)) =>
a ~> b
relabel @(Dual b ** Dual c) @(Dual (b ** c))
                  Svg
  (S (DualList (UN S b ++ UN S c))) (S (DualList (UN S b ++ UN S c)))
-> Svg (S (UN S a)) (S (DualList (UN S b ++ UN S c)))
-> Svg (S (UN S a)) (S (DualList (UN S b ++ UN S c)))
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: SVG) (c :: SVG) (a :: SVG).
Svg b c -> Svg a b -> Svg a c
. forall (as :: [SVG]) (bs :: [SVG]).
Strictified as bs -> Fold as ~> Fold bs
forall {k} (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
unStr @'[a] @[Dual b, Dual c]
                    ( Obj '[S (UN S a)]
Strictified '[S (UN S a)] '[S (UN S a)]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 Strictified '[S (UN S a)] '[S (UN S a)]
-> Strictified '[] '[S (UN S b), S (DualList (UN S b))]
-> Strictified
     ('[S (UN S a)] ** '[])
     ('[S (UN S a)] ** '[S (UN S b), S (DualList (UN S b))])
forall (x1 :: [SVG]) (x2 :: [SVG]) (y1 :: [SVG]) (y2 :: [SVG]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
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 (a :: SVG). Ob a => '[] ~> '[a, Dual a]
dualCupS @b
                        ('[S (UN S a)]
 ~> ('[S (UN S a)] ++ '[S (UN S b), S (DualList (UN S b))]))
-> (('[S (UN S a)] ++ '[S (UN S b), S (DualList (UN S b))])
    ~> ('[S (DualList (UN S c))] ++ '[S (DualList (UN S b))]))
-> '[S (UN S a)]
   ~> ('[S (DualList (UN S c))] ++ '[S (DualList (UN S b))])
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
M.== forall (as :: [SVG]) (bs :: [SVG]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str @[a, b] @'[Dual c] (a ** b) ~> Dual c
Fold '[a, b] ~> Fold '[Dual c]
f Strictified '[a, b] '[S (DualList (UN S c))]
-> Strictified '[S (DualList (UN S b))] '[S (DualList (UN S b))]
-> Strictified
     ('[a, b] ** '[S (DualList (UN S b))])
     ('[S (DualList (UN S c))] ** '[S (DualList (UN S b))])
forall (x1 :: [SVG]) (x2 :: [SVG]) (y1 :: [SVG]) (y2 :: [SVG]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
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)
** Obj '[S (DualList (UN S b))]
Strictified '[S (DualList (UN S b))] '[S (DualList (UN S b))]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1
                        ('[S (UN S a)]
 ~> ('[S (DualList (UN S c))] ++ '[S (DualList (UN S b))]))
-> (('[S (DualList (UN S c))] ++ '[S (DualList (UN S b))])
    ~> '[S (DualList (UN S b)), S (DualList (UN S c))])
-> '[S (UN S a)] ~> '[S (DualList (UN S b)), S (DualList (UN S c))]
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
M.== '[S (DualList (UN S c)), S (DualList (UN S b))]
~> '[S (DualList (UN S b)), S (DualList (UN S c))]
('[S (DualList (UN S c))] ++ '[S (DualList (UN S b))])
~> '[S (DualList (UN S b)), S (DualList (UN S c))]
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
'[a, b] ~> '[b, a]
swap2
                    )
  linDistInv :: forall (a :: SVG) (b :: SVG) (c :: SVG).
(Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @a @b @c a ~> Dual (b ** c)
g =
    forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @SVG @b ((Ob (Dual b) => (a ** b) ~> Dual c) -> (a ** b) ~> Dual c)
-> (Ob (Dual b) => (a ** b) ~> Dual c) -> (a ** b) ~> Dual c
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @SVG @c ((Ob (Dual c) => (a ** b) ~> Dual c) -> (a ** b) ~> Dual c)
-> (Ob (Dual c) => (a ** b) ~> Dual c) -> (a ** b) ~> Dual c
forall a b. (a -> b) -> a -> b
$
        forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @SVG @b @c ((Ob (b ** c) => (a ** b) ~> Dual c) -> (a ** b) ~> Dual c)
-> (Ob (b ** c) => (a ** b) ~> Dual c) -> (a ** b) ~> Dual c
forall a b. (a -> b) -> a -> b
$
          forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @SVG @(b ** c) ((Ob (Dual (b ** c)) => (a ** b) ~> Dual c) -> (a ** b) ~> Dual c)
-> (Ob (Dual (b ** c)) => (a ** b) ~> Dual c) -> (a ** b) ~> Dual c
forall a b. (a -> b) -> a -> b
$
            forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @SVG @(Dual b) @(Dual c) ((Ob (Dual b ** Dual c) => (a ** b) ~> Dual c)
 -> (a ** b) ~> Dual c)
-> (Ob (Dual b ** Dual c) => (a ** b) ~> Dual c)
-> (a ** b) ~> Dual c
forall a b. (a -> b) -> a -> b
$
              forall (as :: [W]) (bs :: [W]) r.
IsList as =>
((DualList (as ++ bs) ~ (DualList as ++ DualList bs)) => r) -> r
withDualAppend @(UN S b) @(UN S c) (((DualList (UN S b ++ UN S c)
   ~ (DualList (UN S b) ++ DualList (UN S c))) =>
  (a ** b) ~> Dual c)
 -> (a ** b) ~> Dual c)
-> ((DualList (UN S b ++ UN S c)
     ~ (DualList (UN S b) ++ DualList (UN S c))) =>
    (a ** b) ~> Dual c)
-> (a ** b) ~> Dual c
forall a b. (a -> b) -> a -> b
$
                forall (as :: [SVG]) (bs :: [SVG]).
Strictified as bs -> Fold as ~> Fold bs
forall {k} (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
unStr @[a, b] @'[Dual c] (Strictified '[a, b] '[Dual c] -> Fold '[a, b] ~> Fold '[Dual c])
-> Strictified '[a, b] '[Dual c] -> Fold '[a, b] ~> Fold '[Dual c]
forall a b. (a -> b) -> a -> b
$
                  forall (as :: [SVG]) (bs :: [SVG]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str @'[a] @[Dual b, Dual c] (forall (a :: SVG) (b :: SVG).
(Ob a, Ob b, Erase (UN S a) ~ Erase (UN S b)) =>
a ~> b
relabel @(Dual (b ** c)) @(Dual b ** Dual c) Svg
  (S (DualList (UN S b ++ UN S c))) (S (DualList (UN S b ++ UN S c)))
-> Svg (S (UN S a)) (S (DualList (UN S b ++ UN S c)))
-> Svg (S (UN S a)) (S (DualList (UN S b ++ UN S c)))
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: SVG) (c :: SVG) (a :: SVG).
Svg b c -> Svg a b -> Svg a c
. a ~> Dual (b ** c)
Svg (S (UN S a)) (S (DualList (UN S b ++ UN S c)))
g) Strictified '[a] '[S (DualList (UN S b)), S (DualList (UN S c))]
-> Strictified '[S (UN S b)] '[S (UN S b)]
-> Strictified
     ('[a] ** '[S (UN S b)])
     ('[S (DualList (UN S b)), S (DualList (UN S c))] ** '[S (UN S b)])
forall (x1 :: [SVG]) (x2 :: [SVG]) (y1 :: [SVG]) (y2 :: [SVG]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
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)
** Obj '[S (UN S b)]
Strictified '[S (UN S b)] '[S (UN S b)]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1
                    ('[S (UN S a), S (UN S b)]
 ~> ('[S (DualList (UN S b)), S (DualList (UN S c))]
     ++ '[S (UN S b)]))
-> (('[S (DualList (UN S b)), S (DualList (UN S c))]
     ++ '[S (UN S b)])
    ~> ('[S (DualList (UN S b))]
        ++ '[S (UN S b), S (DualList (UN S c))]))
-> '[S (UN S a), S (UN S b)]
   ~> ('[S (DualList (UN S b))]
       ++ '[S (UN S b), S (DualList (UN S c))])
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
M.== Obj '[S (DualList (UN S b))]
Strictified '[S (DualList (UN S b))] '[S (DualList (UN S b))]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 Strictified '[S (DualList (UN S b))] '[S (DualList (UN S b))]
-> Strictified
     '[S (DualList (UN S c)), S (UN S b)]
     '[S (UN S b), S (DualList (UN S c))]
-> Strictified
     ('[S (DualList (UN S b))] ** '[S (DualList (UN S c)), S (UN S b)])
     ('[S (DualList (UN S b))] ** '[S (UN S b), S (DualList (UN S c))])
forall (x1 :: [SVG]) (x2 :: [SVG]) (y1 :: [SVG]) (y2 :: [SVG]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
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)
** '[S (DualList (UN S c)), S (UN S b)]
~> '[S (UN S b), S (DualList (UN S c))]
Strictified
  '[S (DualList (UN S c)), S (UN S b)]
  '[S (UN S b), S (DualList (UN S c))]
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
'[a, b] ~> '[b, a]
swap2
                    ('[S (UN S a), S (UN S b)]
 ~> ('[S (DualList (UN S b))]
     ++ '[S (UN S b), S (DualList (UN S c))]))
-> (('[S (DualList (UN S b))]
     ++ '[S (UN S b), S (DualList (UN S c))])
    ~> ('[] ++ '[S (DualList (UN S c))]))
-> '[S (UN S a), S (UN S b)] ~> ('[] ++ '[S (DualList (UN S c))])
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
M.== forall (a :: SVG). Ob a => '[Dual a, a] ~> '[]
dualCapS @b Strictified '[S (DualList (UN S b)), S (UN S b)] '[]
-> Strictified '[S (DualList (UN S c))] '[S (DualList (UN S c))]
-> Strictified
     ('[S (DualList (UN S b)), S (UN S b)] ** '[S (DualList (UN S c))])
     ('[] ** '[S (DualList (UN S c))])
forall (x1 :: [SVG]) (x2 :: [SVG]) (y1 :: [SVG]) (y2 :: [SVG]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
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)
** Obj '[S (DualList (UN S c))]
Strictified '[S (DualList (UN S c))] '[S (DualList (UN S c))]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1
  doubleNeg :: forall (a :: SVG). Ob a => Dual (Dual a) ~> a
doubleNeg @a = forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @SVG @a ((Ob (Dual a) => Dual (Dual a) ~> a) -> Dual (Dual a) ~> a)
-> (Ob (Dual a) => Dual (Dual a) ~> a) -> Dual (Dual a) ~> a
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @SVG @(Dual a) ((Ob (Dual (Dual a)) => Dual (Dual a) ~> a) -> Dual (Dual a) ~> a)
-> (Ob (Dual (Dual a)) => Dual (Dual a) ~> a) -> Dual (Dual a) ~> a
forall a b. (a -> b) -> a -> b
$ forall (ws :: [W]) r.
IsList ws =>
((DualList (DualList ws) ~ ws) => r) -> r
withDualDual @(UN S a) (((DualList (DualList (UN S a)) ~ UN S a) => Dual (Dual a) ~> a)
 -> Dual (Dual a) ~> a)
-> ((DualList (DualList (UN S a)) ~ UN S a) => Dual (Dual a) ~> a)
-> Dual (Dual a) ~> a
forall a b. (a -> b) -> a -> b
$ forall (a :: SVG) (b :: SVG).
(Ob a, Ob b, Erase (UN S a) ~ Erase (UN S b)) =>
a ~> b
relabel @(Dual (Dual a)) @a
  doubleNegInv :: forall (a :: SVG). Ob a => a ~> Dual (Dual a)
doubleNegInv @a = forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @SVG @a ((Ob (Dual a) => a ~> Dual (Dual a)) -> a ~> Dual (Dual a))
-> (Ob (Dual a) => a ~> Dual (Dual a)) -> a ~> Dual (Dual a)
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @SVG @(Dual a) ((Ob (Dual (Dual a)) => a ~> Dual (Dual a)) -> a ~> Dual (Dual a))
-> (Ob (Dual (Dual a)) => a ~> Dual (Dual a)) -> a ~> Dual (Dual a)
forall a b. (a -> b) -> a -> b
$ forall (ws :: [W]) r.
IsList ws =>
((DualList (DualList ws) ~ ws) => r) -> r
withDualDual @(UN S a) (((DualList (DualList (UN S a)) ~ UN S a) => a ~> Dual (Dual a))
 -> a ~> Dual (Dual a))
-> ((DualList (DualList (UN S a)) ~ UN S a) => a ~> Dual (Dual a))
-> a ~> Dual (Dual a)
forall a b. (a -> b) -> a -> b
$ forall (a :: SVG) (b :: SVG).
(Ob a, Ob b, Erase (UN S a) ~ Erase (UN S b)) =>
a ~> b
relabel @a @(Dual (Dual a))

-- | A wire bent upwards, @a@ on the left and its dual on the right. It means 'cup', and is drawn
-- as one bend that turns into the dual at its apex.
dualCup :: forall (a :: SVG). (Ob a) => Unit ~> a ** Dual a
dualCup :: forall (a :: SVG). Ob a => Unit ~> (a ** Dual a)
dualCup = forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @SVG @a ((Ob (Dual a) => Unit ~> (a ** Dual a)) -> Unit ~> (a ** Dual a))
-> (Ob (Dual a) => Unit ~> (a ** Dual a)) -> Unit ~> (a ** Dual a)
forall a b. (a -> b) -> a -> b
$
  forall (ws :: [W]) r.
IsList ws =>
((Erase (DualList ws) ~ Erase ws) => r) -> r
withEraseDual @(UN S a) (((Erase (DualList (UN S a)) ~ Erase (UN S a)) =>
  Unit ~> (a ** Dual a))
 -> Unit ~> (a ** Dual a))
-> ((Erase (DualList (UN S a)) ~ Erase (UN S a)) =>
    Unit ~> (a ** Dual a))
-> Unit ~> (a ** Dual a)
forall a b. (a -> b) -> a -> b
$
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @SVG @a @a ((Ob (a ** a) => Unit ~> (a ** Dual a)) -> Unit ~> (a ** Dual a))
-> (Ob (a ** a) => Unit ~> (a ** Dual a)) -> Unit ~> (a ** Dual a)
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @SVG @a @(Dual a) ((Ob (a ** Dual a) => Unit ~> (a ** Dual a))
 -> Unit ~> (a ** Dual a))
-> (Ob (a ** Dual a) => Unit ~> (a ** Dual a))
-> Unit ~> (a ** Dual a)
forall a b. (a -> b) -> a -> b
$
        case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: SVG). (CategoryOf SVG, Ob a) => Obj a
obj @a Svg (S (UN S a)) (S (UN S a))
-> Svg (S (UN S a)) (S (DualList (UN S a)))
-> Svg
     (S (UN S a) ** S (UN S a)) (S (UN S a) ** S (DualList (UN S a)))
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 :: SVG) (x2 :: SVG) (y1 :: SVG) (y2 :: SVG).
Svg x1 x2 -> Svg y1 y2 -> Svg (x1 ** y1) (x2 ** y2)
** forall (a :: SVG) (b :: SVG).
(Ob a, Ob b, Erase (UN S a) ~ Erase (UN S b)) =>
a ~> b
relabel @a @(Dual a)) Svg
  (S (UN S (S (UN S a)) ++ UN S (S (UN S a))))
  (S (UN S (S (UN S a)) ++ UN S (S (DualList (UN S a)))))
-> Svg (S '[I]) (S (UN S (S (UN S a)) ++ UN S (S (UN S a))))
-> Svg
     (S '[I]) (S (UN S (S (UN S a)) ++ UN S (S (DualList (UN S a)))))
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: SVG) (c :: SVG) (a :: SVG).
Svg b c -> Svg a b -> Svg a c
. forall {k} (a :: k). Frobenius a => Unit ~> (a ** a)
forall (a :: SVG). Frobenius a => Unit ~> (a ** a)
cup @a of
          Svg Dot (D (Erase as)) (D (Erase bs))
d Diagram
_ -> Dot (D (Erase '[I])) (D (Erase bs))
-> Diagram -> Svg (S '[I]) (S bs)
forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs) =>
Dot (D (Erase as)) (D (Erase bs)) -> Diagram -> Svg (S as) (S bs)
Svg Dot (D (Erase as)) (D (Erase bs))
Dot (D (Erase '[I])) (D (Erase bs))
d (Diagram -> Diagram -> Diagram
Seq Diagram
UnitEnd (BendKind -> [WireKind] -> [WireKind] -> Diagram
Bend BendKind
Cup (forall (ws :: [W]). IsList ws => [WireKind]
wireKinds @(UN S a)) (forall (ws :: [W]). IsList ws => [WireKind]
wireKinds @(UN S (Dual a)))))

-- | A wire bent downwards, the dual of @a@ on the left and @a@ on the right. It means 'cap', and is
-- drawn as one bend that turns into the dual at its apex.
dualCap :: forall (a :: SVG). (Ob a) => Dual a ** a ~> Unit
dualCap :: forall (a :: SVG). Ob a => (Dual a ** a) ~> Unit
dualCap = forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @SVG @a ((Ob (Dual a) => (Dual a ** a) ~> Unit) -> (Dual a ** a) ~> Unit)
-> (Ob (Dual a) => (Dual a ** a) ~> Unit) -> (Dual a ** a) ~> Unit
forall a b. (a -> b) -> a -> b
$
  forall (ws :: [W]) r.
IsList ws =>
((Erase (DualList ws) ~ Erase ws) => r) -> r
withEraseDual @(UN S a) (((Erase (DualList (UN S a)) ~ Erase (UN S a)) =>
  (Dual a ** a) ~> Unit)
 -> (Dual a ** a) ~> Unit)
-> ((Erase (DualList (UN S a)) ~ Erase (UN S a)) =>
    (Dual a ** a) ~> Unit)
-> (Dual a ** a) ~> Unit
forall a b. (a -> b) -> a -> b
$
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @SVG @a @a ((Ob (a ** a) => (Dual a ** a) ~> Unit) -> (Dual a ** a) ~> Unit)
-> (Ob (a ** a) => (Dual a ** a) ~> Unit) -> (Dual a ** a) ~> Unit
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @SVG @(Dual a) @a ((Ob (Dual a ** a) => (Dual a ** a) ~> Unit)
 -> (Dual a ** a) ~> Unit)
-> (Ob (Dual a ** a) => (Dual a ** a) ~> Unit)
-> (Dual a ** a) ~> Unit
forall a b. (a -> b) -> a -> b
$
        case forall {k} (a :: k). Frobenius a => (a ** a) ~> Unit
forall (a :: SVG). Frobenius a => (a ** a) ~> Unit
cap @a Svg (S (UN S a ++ UN S a)) (S '[I])
-> Svg
     (S (UN S (S (DualList (UN S a))) ++ UN S (S (UN S a))))
     (S (UN S a ++ UN S a))
-> Svg
     (S (UN S (S (DualList (UN S a))) ++ UN S (S (UN S a)))) (S '[I])
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: SVG) (c :: SVG) (a :: SVG).
Svg b c -> Svg a b -> Svg a c
. (forall (a :: SVG) (b :: SVG).
(Ob a, Ob b, Erase (UN S a) ~ Erase (UN S b)) =>
a ~> b
relabel @(Dual a) @a Svg (S (DualList (UN S a))) (S (UN S a))
-> Svg (S (UN S a)) (S (UN S a))
-> Svg
     (S (DualList (UN S a)) ** S (UN S a)) (S (UN S a) ** S (UN S a))
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 :: SVG) (x2 :: SVG) (y1 :: SVG) (y2 :: SVG).
Svg x1 x2 -> Svg y1 y2 -> Svg (x1 ** y1) (x2 ** y2)
** forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: SVG). (CategoryOf SVG, Ob a) => Obj a
obj @a) of
          Svg Dot (D (Erase as)) (D (Erase bs))
d Diagram
_ -> Dot (D (Erase as)) (D (Erase '[I]))
-> Diagram -> Svg (S as) (S '[I])
forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs) =>
Dot (D (Erase as)) (D (Erase bs)) -> Diagram -> Svg (S as) (S bs)
Svg Dot (D (Erase as)) (D (Erase bs))
Dot (D (Erase as)) (D (Erase '[I]))
d (Diagram -> Diagram -> Diagram
Seq (BendKind -> [WireKind] -> [WireKind] -> Diagram
Bend BendKind
Cap (forall (ws :: [W]). IsList ws => [WireKind]
wireKinds @(UN S a)) (forall (ws :: [W]). IsList ws => [WireKind]
wireKinds @(UN S (Dual a)))) Diagram
UnitStart)

-- | 'dualCup' as a strictified arrow. The *-autonomous structure is built from it, not from the
-- compact closed 'dualityUnit', so that the laws relating the two compare different definitions.
dualCupS :: forall (a :: SVG). (Ob a) => '[] ~> [a, Dual a]
dualCupS :: forall (a :: SVG). Ob a => '[] ~> '[a, Dual a]
dualCupS = forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @SVG @a ((Ob (Dual a) => '[] ~> '[a, Dual a]) -> '[] ~> '[a, Dual a])
-> (Ob (Dual a) => '[] ~> '[a, Dual a]) -> '[] ~> '[a, Dual a]
forall a b. (a -> b) -> a -> b
$ (Fold '[] ~> Fold '[S (UN S a), S (DualList (UN S a))])
-> Strictified '[] '[S (UN S a), S (DualList (UN S a))]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str (forall (a :: SVG). Ob a => Unit ~> (a ** Dual a)
dualCup @a)

-- | 'dualCap' as a strictified arrow.
dualCapS :: forall (a :: SVG). (Ob a) => [Dual a, a] ~> '[]
dualCapS :: forall (a :: SVG). Ob a => '[Dual a, a] ~> '[]
dualCapS = forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @SVG @a ((Ob (Dual a) => '[Dual a, a] ~> '[]) -> '[Dual a, a] ~> '[])
-> (Ob (Dual a) => '[Dual a, a] ~> '[]) -> '[Dual a, a] ~> '[]
forall a b. (a -> b) -> a -> b
$ (Fold '[S (DualList (UN S a)), S (UN S a)] ~> Fold '[])
-> Strictified '[S (DualList (UN S a)), S (UN S a)] '[]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str (forall (a :: SVG). Ob a => (Dual a ** a) ~> Unit
dualCap @a)

instance CompactClosed SVG where
  distribDual :: forall (a :: SVG) (b :: SVG).
(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 @SVG @a @b ((Ob (a ** b) => Dual (a ** b) ~> (Dual a ** Dual b))
 -> Dual (a ** b) ~> (Dual a ** Dual b))
-> (Ob (a ** b) => Dual (a ** b) ~> (Dual a ** Dual b))
-> Dual (a ** b) ~> (Dual a ** Dual b)
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @SVG @a ((Ob (Dual a) => Dual (a ** b) ~> (Dual a ** Dual b))
 -> Dual (a ** b) ~> (Dual a ** Dual b))
-> (Ob (Dual a) => Dual (a ** b) ~> (Dual a ** Dual b))
-> Dual (a ** b) ~> (Dual a ** Dual b)
forall a b. (a -> b) -> a -> b
$
        forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @SVG @b ((Ob (Dual b) => Dual (a ** b) ~> (Dual a ** Dual b))
 -> Dual (a ** b) ~> (Dual a ** Dual b))
-> (Ob (Dual b) => Dual (a ** b) ~> (Dual a ** Dual b))
-> Dual (a ** b) ~> (Dual a ** Dual b)
forall a b. (a -> b) -> a -> b
$
          forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @SVG @(a ** b) ((Ob (Dual (a ** b)) => Dual (a ** b) ~> (Dual a ** Dual b))
 -> Dual (a ** b) ~> (Dual a ** Dual b))
-> (Ob (Dual (a ** b)) => Dual (a ** b) ~> (Dual a ** Dual b))
-> Dual (a ** b) ~> (Dual a ** Dual b)
forall a b. (a -> b) -> a -> b
$
            forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @SVG @(Dual a) @(Dual b) ((Ob (Dual a ** Dual b) => Dual (a ** b) ~> (Dual a ** Dual b))
 -> Dual (a ** b) ~> (Dual a ** Dual b))
-> (Ob (Dual a ** Dual b) => Dual (a ** b) ~> (Dual a ** Dual b))
-> Dual (a ** b) ~> (Dual a ** Dual b)
forall a b. (a -> b) -> a -> b
$
              forall (as :: [W]) (bs :: [W]) r.
IsList as =>
((DualList (as ++ bs) ~ (DualList as ++ DualList bs)) => r) -> r
withDualAppend @(UN S a) @(UN S b) (((DualList (UN S a ++ UN S b)
   ~ (DualList (UN S a) ++ DualList (UN S b))) =>
  Dual (a ** b) ~> (Dual a ** Dual b))
 -> Dual (a ** b) ~> (Dual a ** Dual b))
-> ((DualList (UN S a ++ UN S b)
     ~ (DualList (UN S a) ++ DualList (UN S b))) =>
    Dual (a ** b) ~> (Dual a ** Dual b))
-> Dual (a ** b) ~> (Dual a ** Dual b)
forall a b. (a -> b) -> a -> b
$
                forall (a :: SVG) (b :: SVG).
(Ob a, Ob b, Erase (UN S a) ~ Erase (UN S b)) =>
a ~> b
relabel @(Dual (a ** b)) @(Dual a ** Dual b)
  dualUnit :: Dual Unit ~> Unit
dualUnit = Dual Unit ~> Unit
S '[I] ~> S '[I]
forall (a :: SVG) (b :: SVG).
(Ob a, Ob b, Erase (UN S a) ~ Erase (UN S b)) =>
a ~> b
relabel
  dualityUnit :: forall (a :: SVG). Ob a => Unit ~> (a ** Dual a)
dualityUnit @a = forall (a :: SVG). Ob a => Unit ~> (a ** Dual a)
dualCup @a
  dualityCounit :: forall (a :: SVG). Ob a => (Dual a ** a) ~> Unit
dualityCounit @a = forall (a :: SVG). Ob a => (Dual a ** a) ~> Unit
dualCap @a

-- | The traced wires loop round the side of the diagram they are nearest to.
instance Costrong Tensor Svg where
  coact :: forall (a :: SVG) (x :: SVG) (y :: SVG).
(Ob a, Ob x, Ob y) =>
Svg (Act Tensor a x) (Act Tensor a y) -> Svg x y
coact @(S as) @(S xs) @(S ys) (Svg Dot (D (Erase as)) (D (Erase bs))
f Diagram
l) =
    forall (as :: [W]) (bs :: [W]) r.
IsList as =>
((Erase (as ++ bs) ~ (Erase as ++ Erase bs)) => r) -> r
withEraseAppend @as @xs (((Erase (UN S a ++ UN S x)
   ~ (Erase (UN S a) ++ Erase (UN S x))) =>
  Svg x y)
 -> Svg x y)
-> ((Erase (UN S a ++ UN S x)
     ~ (Erase (UN S a) ++ Erase (UN S x))) =>
    Svg x y)
-> Svg x y
forall a b. (a -> b) -> a -> b
$
      forall (as :: [W]) (bs :: [W]) r.
IsList as =>
((Erase (as ++ bs) ~ (Erase as ++ Erase bs)) => r) -> r
withEraseAppend @as @ys (((Erase (UN S a ++ UN S y)
   ~ (Erase (UN S a) ++ Erase (UN S y))) =>
  Svg x y)
 -> Svg x y)
-> ((Erase (UN S a ++ UN S y)
     ~ (Erase (UN S a) ++ Erase (UN S y))) =>
    Svg x y)
-> Svg x y
forall a b. (a -> b) -> a -> b
$
        forall (ws :: [W]) r. IsList ws => (IsList (Erase ws) => r) -> r
withIsListErase @as ((IsList (Erase (UN S a)) => Svg x y) -> Svg x y)
-> (IsList (Erase (UN S a)) => Svg x y) -> Svg x y
forall a b. (a -> b) -> a -> b
$
          ((IsList (Erase (UN S x)), IsList (Erase (UN S y))) =>
 Dot (D (Erase (UN S x))) (D (Erase (UN S y))))
-> Diagram -> Svg (S (UN S x)) (S (UN S y))
forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs) =>
((IsList (Erase as), IsList (Erase bs)) =>
 Dot (D (Erase as)) (D (Erase bs)))
-> Diagram -> Svg (S as) (S bs)
svg (forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
forall (t :: (DOT, DOT) +-> DOT) (p :: DOT +-> DOT) (a :: DOT)
       (x :: DOT) (y :: DOT).
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
coact @Tensor @Dot @(Dot.D (Erase as)) @(Dot.D (Erase xs)) @(Dot.D (Erase ys)) Dot
  (Act Tensor (D (Erase (UN S a))) (D (Erase (UN S x))))
  (Act Tensor (D (Erase (UN S a))) (D (Erase (UN S y))))
Dot (D (Erase as)) (D (Erase bs))
f) ([WireKind] -> Diagram -> Diagram
Trace (forall (ws :: [W]). IsList ws => [WireKind]
wireKinds @as) Diagram
l)

-- | Derived operations are drawn as what they are made of.
instance Labelled SVG where
  label :: forall (a :: SVG) (b :: SVG). String -> (a ~> b) -> a ~> b
label String
_ a ~> b
f = a ~> b
f

-- * Building diagrams

-- | A box with the given name, its inputs along the top and its outputs along the bottom, each
-- output labelled with its wire.
node :: forall (as :: [W]) (bs :: [W]). (IsList as, IsList bs) => String -> Svg (S as) (S bs)
node :: forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs) =>
String -> Svg (S as) (S bs)
node String
s = ((IsList (Erase as), IsList (Erase bs)) =>
 Dot (D (Erase as)) (D (Erase bs)))
-> Diagram -> Svg (S as) (S bs)
forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs) =>
((IsList (Erase as), IsList (Erase bs)) =>
 Dot (D (Erase as)) (D (Erase bs)))
-> Diagram -> Svg (S as) (S bs)
svg (forall (as :: [Symbol]) (bs :: [Symbol]).
(IsList as, IsList bs) =>
String -> Dot (D as) (D bs)
Dot.node @(Erase as) @(Erase bs) String
s) (String -> [WireKind] -> [(String, WireKind)] -> Diagram
Node String
s (forall (ws :: [W]). IsList ws => [WireKind]
wireKinds @as) (forall (ws :: [W]). IsList ws => [(String, WireKind)]
wires @bs))

-- | A wire, the identity on it.
line :: (KnownSymbol a) => Svg (S '[Wire a]) (S '[Wire a])
line :: forall (a :: Symbol).
KnownSymbol a =>
Svg (S '[Wire a]) (S '[Wire a])
line = Svg (S '[Wire a]) (S '[Wire a])
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: SVG). Ob a => Svg a a
id

-- | A crossing of fixed height. A plain 'swap' is drawn as a crossing too, but in the band where
-- the wires next change position.
swapNode
  :: forall (a :: Symbol) (b :: Symbol). (KnownSymbol a, KnownSymbol b) => Svg (S [Wire a, Wire b]) (S [Wire b, Wire a])
swapNode :: forall (a :: Symbol) (b :: Symbol).
(KnownSymbol a, KnownSymbol b) =>
Svg (S '[Wire a, Wire b]) (S '[Wire b, Wire a])
swapNode = Dot (D (Erase '[Wire a, Wire b])) (D (Erase '[Wire b, Wire a]))
-> Diagram -> Svg (S '[Wire a, Wire b]) (S '[Wire b, Wire a])
forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs) =>
Dot (D (Erase as)) (D (Erase bs)) -> Diagram -> Svg (S as) (S bs)
Svg (forall (a :: Symbol) (b :: Symbol).
(Ob a, Ob b) =>
Dot (D '[a, b]) (D '[b, a])
Dot.swapNode @a @b) (Bool -> [WireKind] -> [Int] -> Diagram
Permute Bool
True (forall (ws :: [W]). IsList ws => [WireKind]
wireKinds @[Wire a, Wire b]) [Int
1, Int
0])

-- | The unit of an adjunction, drawn as a box named η.
unitAdj :: forall (l :: Symbol) (r :: Symbol). (KnownSymbol l, KnownSymbol r) => Svg (S '[]) (S '[Wire l, Wire r])
unitAdj :: forall (l :: Symbol) (r :: Symbol).
(KnownSymbol l, KnownSymbol r) =>
Svg (S '[]) (S '[Wire l, Wire r])
unitAdj = Dot (D (Erase '[])) (D (Erase '[Wire l, Wire r]))
-> Diagram -> Svg (S '[]) (S '[Wire l, Wire r])
forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs) =>
Dot (D (Erase as)) (D (Erase bs)) -> Diagram -> Svg (S as) (S bs)
Svg (forall (l :: Symbol) (r :: Symbol).
(Ob l, Ob r) =>
Dot (D '[]) (D '[l, r])
Dot.unitAdj @l @r) (String -> [WireKind] -> [(String, WireKind)] -> Diagram
Node String
"η" [] (forall (ws :: [W]). IsList ws => [(String, WireKind)]
wires @[Wire l, Wire r]))

-- | The counit of an adjunction, drawn as a box named ϵ.
counitAdj :: forall (l :: Symbol) (r :: Symbol). (KnownSymbol l, KnownSymbol r) => Svg (S '[Wire r, Wire l]) (S '[])
counitAdj :: forall (l :: Symbol) (r :: Symbol).
(KnownSymbol l, KnownSymbol r) =>
Svg (S '[Wire r, Wire l]) (S '[])
counitAdj = Dot (D (Erase '[Wire r, Wire l])) (D (Erase '[]))
-> Diagram -> Svg (S '[Wire r, Wire l]) (S '[])
forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs) =>
Dot (D (Erase as)) (D (Erase bs)) -> Diagram -> Svg (S as) (S bs)
Svg (forall (l :: Symbol) (r :: Symbol).
(Ob l, Ob r) =>
Dot (D '[r, l]) (D '[])
Dot.counitAdj @l @r) (String -> [WireKind] -> [(String, WireKind)] -> Diagram
Node String
"ϵ" (forall (ws :: [W]). IsList ws => [WireKind]
wireKinds @[Wire r, Wire l]) [])

-- | What kind of wire a wire is, which decides how it is drawn.
data WireKind = Plain | UnitWire | DualWire
  deriving (WireKind -> WireKind -> Bool
(WireKind -> WireKind -> Bool)
-> (WireKind -> WireKind -> Bool) -> Eq WireKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: WireKind -> WireKind -> Bool
== :: WireKind -> WireKind -> Bool
$c/= :: WireKind -> WireKind -> Bool
/= :: WireKind -> WireKind -> Bool
Eq, Int -> WireKind -> String -> String
[WireKind] -> String -> String
WireKind -> String
(Int -> WireKind -> String -> String)
-> (WireKind -> String)
-> ([WireKind] -> String -> String)
-> Show WireKind
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> WireKind -> String -> String
showsPrec :: Int -> WireKind -> String -> String
$cshow :: WireKind -> String
show :: WireKind -> String
$cshowList :: [WireKind] -> String -> String
showList :: [WireKind] -> String -> String
Show)

-- * Diagrams

-- | How a diagram was built. The options come in only when it is drawn: 'hideUnits' takes out what
-- 'explicitCoherence' would show, and 'layout' decides the rest.
data Diagram
  = -- | the identity on wires of the given kinds
    Ident [WireKind]
  | -- | wires of the given kinds, output @j@ continuing input @p !! j@; when the flag is set, its
    -- crossings are drawn on their own
    Permute Bool [WireKind] [Int]
  | -- | wires carrying straight on, as many out as in, possibly of other kinds
    Straight [WireKind] [WireKind]
  | -- | a box with a name, the kinds of its inputs, and the labels and kinds of its outputs
    Node String [WireKind] [(String, WireKind)]
  | -- | a point of the given kind on each wire
    Points PointKind [WireKind]
  | -- | bends joining each wire of the first kinds to its dual, of the second kinds
    Bend BendKind [WireKind] [WireKind]
  | -- | an associator from the given grouping, on three lists of wires
    Rebracket Grouping [WireKind] [WireKind] [WireKind]
  | -- | a unitor on wires of the given kinds
    Unitor Side Direction [WireKind]
  | -- | a unit wire ending
    UnitEnd
  | -- | a unit wire starting
    UnitStart
  | -- | the first diagram above the second
    Seq Diagram Diagram
  | -- | two diagrams side by side
    Beside Diagram Diagram
  | -- | the first inputs and outputs, of the given kinds, fed back
    Trace [WireKind] Diagram
  deriving (Int -> Diagram -> String -> String
[Diagram] -> String -> String
Diagram -> String
(Int -> Diagram -> String -> String)
-> (Diagram -> String)
-> ([Diagram] -> String -> String)
-> Show Diagram
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Diagram -> String -> String
showsPrec :: Int -> Diagram -> String -> String
$cshow :: Diagram -> String
show :: Diagram -> String
$cshowList :: [Diagram] -> String -> String
showList :: [Diagram] -> String -> String
Show)

-- | The points a (co)monoid is drawn with.
data PointKind = UnitPoint | DiscardPoint | CopyPoint | MergePoint
  deriving (Int -> PointKind -> String -> String
[PointKind] -> String -> String
PointKind -> String
(Int -> PointKind -> String -> String)
-> (PointKind -> String)
-> ([PointKind] -> String -> String)
-> Show PointKind
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> PointKind -> String -> String
showsPrec :: Int -> PointKind -> String -> String
$cshow :: PointKind -> String
show :: PointKind -> String
$cshowList :: [PointKind] -> String -> String
showList :: [PointKind] -> String -> String
Show)

-- | Whether a bend opens downwards, a cup, or upwards, a cap.
data BendKind = Cup | Cap
  deriving (Int -> BendKind -> String -> String
[BendKind] -> String -> String
BendKind -> String
(Int -> BendKind -> String -> String)
-> (BendKind -> String)
-> ([BendKind] -> String -> String)
-> Show BendKind
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> BendKind -> String -> String
showsPrec :: Int -> BendKind -> String -> String
$cshow :: BendKind -> String
show :: BendKind -> String
$cshowList :: [BendKind] -> String -> String
showList :: [BendKind] -> String -> String
Show)

-- | Which pair an associator groups first: @(a ⊗ b) ⊗ c@ or @a ⊗ (b ⊗ c)@.
data Grouping = LeftFirst | RightFirst
  deriving (Int -> Grouping -> String -> String
[Grouping] -> String -> String
Grouping -> String
(Int -> Grouping -> String -> String)
-> (Grouping -> String)
-> ([Grouping] -> String -> String)
-> Show Grouping
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Grouping -> String -> String
showsPrec :: Int -> Grouping -> String -> String
$cshow :: Grouping -> String
show :: Grouping -> String
$cshowList :: [Grouping] -> String -> String
showList :: [Grouping] -> String -> String
Show)

-- | Which side of the other wires a unit wire joins them.
data Side = OnLeft | OnRight
  deriving (Int -> Side -> String -> String
[Side] -> String -> String
Side -> String
(Int -> Side -> String -> String)
-> (Side -> String) -> ([Side] -> String -> String) -> Show Side
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Side -> String -> String
showsPrec :: Int -> Side -> String -> String
$cshow :: Side -> String
show :: Side -> String
$cshowList :: [Side] -> String -> String
showList :: [Side] -> String -> String
Show)

-- | Whether a unitor ends a unit wire on another wire, or starts one from it.
data Direction = Absorb | Create
  deriving (Int -> Direction -> String -> String
[Direction] -> String -> String
Direction -> String
(Int -> Direction -> String -> String)
-> (Direction -> String)
-> ([Direction] -> String -> String)
-> Show Direction
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Direction -> String -> String
showsPrec :: Int -> Direction -> String -> String
$cshow :: Direction -> String
show :: Direction -> String
$cshowList :: [Direction] -> String -> String
showList :: [Direction] -> String -> String
Show)

-- | The diagram with its unit wires left out, and its unitors and associators turned into wires
-- carrying straight on.
hideUnits :: Diagram -> Diagram
hideUnits :: Diagram -> Diagram
hideUnits = \case
  Ident [WireKind]
ks -> [WireKind] -> Diagram
Ident ([WireKind] -> [WireKind]
noUnits [WireKind]
ks)
  Permute Bool
c [WireKind]
ks [Int]
p ->
    let kept :: [Int]
kept = [Int
i | (Int
i, WireKind
k) <- [Int] -> [WireKind] -> [(Int, WireKind)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] [WireKind]
ks, WireKind
k WireKind -> WireKind -> Bool
forall a. Eq a => a -> a -> Bool
/= WireKind
UnitWire]
        renumber :: Int -> Int
renumber Int
i = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 (Int -> [Int] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex Int
i [Int]
kept)
    in Bool -> [WireKind] -> [Int] -> Diagram
Permute Bool
c ((Int -> WireKind) -> [Int] -> [WireKind]
forall a b. (a -> b) -> [a] -> [b]
map ([WireKind]
ks [WireKind] -> Int -> WireKind
forall a. HasCallStack => [a] -> Int -> a
!!) [Int]
kept) [Int -> Int
renumber Int
i | Int
i <- [Int]
p, [WireKind]
ks [WireKind] -> Int -> WireKind
forall a. HasCallStack => [a] -> Int -> a
!! Int
i WireKind -> WireKind -> Bool
forall a. Eq a => a -> a -> Bool
/= WireKind
UnitWire]
  Straight [WireKind]
ks [WireKind]
ls -> [WireKind] -> [WireKind] -> Diagram
Straight ([WireKind] -> [WireKind]
noUnits [WireKind]
ks) ([WireKind] -> [WireKind]
noUnits [WireKind]
ls)
  Node String
s [WireKind]
ks [(String, WireKind)]
os -> String -> [WireKind] -> [(String, WireKind)] -> Diagram
Node String
s ([WireKind] -> [WireKind]
noUnits [WireKind]
ks) [(String, WireKind)
w | w :: (String, WireKind)
w@(String
_, WireKind
k) <- [(String, WireKind)]
os, WireKind
k WireKind -> WireKind -> Bool
forall a. Eq a => a -> a -> Bool
/= WireKind
UnitWire]
  Points PointKind
pk [WireKind]
ks -> PointKind -> [WireKind] -> Diagram
Points PointKind
pk ([WireKind] -> [WireKind]
noUnits [WireKind]
ks)
  Bend BendKind
b [WireKind]
ka [WireKind]
kd -> BendKind -> [WireKind] -> [WireKind] -> Diagram
Bend BendKind
b ([WireKind] -> [WireKind]
noUnits [WireKind]
ka) ([WireKind] -> [WireKind]
noUnits [WireKind]
kd)
  Rebracket Grouping
_ [WireKind]
ka [WireKind]
kb [WireKind]
kc -> [WireKind] -> Diagram
straight ([WireKind] -> [WireKind]
noUnits ([WireKind]
ka [WireKind] -> [WireKind] -> [WireKind]
forall a. [a] -> [a] -> [a]
++ [WireKind]
kb [WireKind] -> [WireKind] -> [WireKind]
forall a. [a] -> [a] -> [a]
++ [WireKind]
kc))
  Unitor Side
_ Direction
_ [WireKind]
ks -> [WireKind] -> Diagram
straight ([WireKind] -> [WireKind]
noUnits [WireKind]
ks)
  Diagram
UnitEnd -> [WireKind] -> Diagram
straight []
  Diagram
UnitStart -> [WireKind] -> Diagram
straight []
  Seq Diagram
a Diagram
b -> Diagram -> Diagram -> Diagram
Seq (Diagram -> Diagram
hideUnits Diagram
a) (Diagram -> Diagram
hideUnits Diagram
b)
  Beside Diagram
a Diagram
b -> Diagram -> Diagram -> Diagram
Beside (Diagram -> Diagram
hideUnits Diagram
a) (Diagram -> Diagram
hideUnits Diagram
b)
  Trace [WireKind]
ks Diagram
d -> [WireKind] -> Diagram -> Diagram
Trace ([WireKind] -> [WireKind]
noUnits [WireKind]
ks) (Diagram -> Diagram
hideUnits Diagram
d)
  where
    straight :: [WireKind] -> Diagram
straight [WireKind]
ks = [WireKind] -> [WireKind] -> Diagram
Straight [WireKind]
ks [WireKind]
ks

noUnits :: [WireKind] -> [WireKind]
noUnits :: [WireKind] -> [WireKind]
noUnits = (WireKind -> Bool) -> [WireKind] -> [WireKind]
forall a. (a -> Bool) -> [a] -> [a]
filter (WireKind -> WireKind -> Bool
forall a. Eq a => a -> a -> Bool
/= WireKind
UnitWire)

-- | The diagram laid out with the given options.
layout :: Options -> Diagram -> Layout
layout :: Options -> Diagram -> Layout
layout Options
o = Diagram -> Layout
go (Diagram -> Layout) -> (Diagram -> Diagram) -> Diagram -> Layout
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
. if Options -> Bool
explicitCoherence Options
o then Diagram -> Diagram
forall a. Ob a => a -> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id else Diagram -> Diagram
hideUnits
  where
    go :: Diagram -> Layout
go = \case
      Ident [WireKind]
ks -> Bool -> [WireKind] -> Layout
identity (Options -> Bool
explicitIdentities Options
o) [WireKind]
ks
      Permute Bool
c [WireKind]
ks [Int]
p -> Bool -> [WireKind] -> [Int] -> Layout
permutation (Bool
c Bool -> Bool -> Bool
|| Options -> Bool
explicitSwaps Options
o) [WireKind]
ks [Int]
p
      Straight [WireKind]
ks [WireKind]
ls -> [Int] -> [WireKind] -> [WireKind] -> Layout
Wiring [Int
0 .. [WireKind] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [WireKind]
ls Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1] [WireKind]
ks [WireKind]
ls
      Node String
s [WireKind]
ks [(String, WireKind)]
os -> Geo -> Layout
Stage ([WireKind] -> [(String, WireKind)] -> String -> Geo
nodeGeo [WireKind]
ks [(String, WireKind)]
os String
s)
      Points PointKind
pk [WireKind]
ks -> Bool -> PointKind -> [WireKind] -> Layout
points (Bool -> Bool
not (Options -> Bool
fixedSpiders Options
o)) PointKind
pk [WireKind]
ks
      Bend BendKind
b [WireKind]
ka [WireKind]
kd -> BendKind -> [WireKind] -> [WireKind] -> Layout
bend BendKind
b [WireKind]
ka [WireKind]
kd
      Rebracket Grouping
g [WireKind]
ka [WireKind]
kb [WireKind]
kc -> Geo -> Layout
Stage (Grouping -> [WireKind] -> [WireKind] -> [WireKind] -> Geo
rebracket Grouping
g [WireKind]
ka [WireKind]
kb [WireKind]
kc)
      Unitor Side
s Direction
d [WireKind]
ks -> Geo -> Layout
Stage (Side -> Direction -> [WireKind] -> Geo
unitor Side
s Direction
d [WireKind]
ks)
      Diagram
UnitEnd -> Geo -> Layout
Stage Geo
unitEnd
      Diagram
UnitStart -> Geo -> Layout
Stage (Geo -> Geo
mirror Geo
unitEnd)
      Seq Diagram
a Diagram
b -> Layout -> Layout -> Layout
compose (Diagram -> Layout
go Diagram
b) (Diagram -> Layout
go Diagram
a)
      Beside Diagram
a Diagram
b -> Layout -> Layout -> Layout
tensor (Diagram -> Layout
go Diagram
a) (Diagram -> Layout
go Diagram
b)
      Trace [WireKind]
ks Diagram
d -> Geo -> Layout
Stage (Int -> Geo -> Geo
loops ([WireKind] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [WireKind]
ks) (Double -> Layout -> Geo
toGeo Double
slot (Diagram -> Layout
go Diagram
d)))

-- | The boundary wires that are drawn with the given options.
visible :: Options -> [(String, WireKind)] -> [(String, WireKind)]
visible :: Options -> [(String, WireKind)] -> [(String, WireKind)]
visible Options
o [(String, WireKind)]
ws = [(String, WireKind)
w | w :: (String, WireKind)
w@(String
_, WireKind
k) <- [(String, WireKind)]
ws, Options -> Bool
explicitCoherence Options
o Bool -> Bool -> Bool
|| WireKind
k WireKind -> WireKind -> Bool
forall a. Eq a => a -> a -> Bool
/= WireKind
UnitWire]

-- * Layout

-- | A point in the plane, @y@ growing downwards.
type Pt = (Double, Double)

-- | The course of a piece of wire.
data Path
  = -- | straight from one point to another
    Line Pt Pt
  | -- | from one point down to another, leaving and arriving vertically
    Curve Pt Pt
  | -- | along the given corners, rounded
    Loop (NonEmpty Pt)
  | -- | a quarter of an ellipse, leaving the first point vertically and reaching the second
    -- horizontally: half of a bend
    Quarter Pt Pt
  deriving (Int -> Path -> String -> String
[Path] -> String -> String
Path -> String
(Int -> Path -> String -> String)
-> (Path -> String) -> ([Path] -> String -> String) -> Show Path
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Path -> String -> String
showsPrec :: Int -> Path -> String -> String
$cshow :: Path -> String
show :: Path -> String
$cshowList :: [Path] -> String -> String
showList :: [Path] -> String -> String
Show)

-- | What a diagram is drawn with.
data Shape
  = -- | a piece of wire of the given kind: plain, dotted for a unit wire, hollow for a dual one
    Piece WireKind Path
  | -- | a box between two corners, with a name
    Box Pt Pt String
  | -- | the dashed frame of an identity, between two corners
    Frame Pt Pt
  | -- | a bracket grouping wires, from one point to another, its ends pointing down or up
    Bracket Pt Pt Bool
  | -- | a point on a wire, filled for a comonoid and hollow for a monoid
    Point Pt Bool
  | -- | the label of the wire leaving a box
    Label Pt String
  | -- | the label of a boundary wire, centred
    Boundary Pt String
  | -- | the equals sign of an equation
    Equals Pt
  deriving (Int -> Shape -> String -> String
[Shape] -> String -> String
Shape -> String
(Int -> Shape -> String -> String)
-> (Shape -> String) -> ([Shape] -> String -> String) -> Show Shape
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Shape -> String -> String
showsPrec :: Int -> Shape -> String -> String
$cshow :: Shape -> String
show :: Shape -> String
$cshowList :: [Shape] -> String -> String
showList :: [Shape] -> String -> String
Show)

-- | A shape moved right by @dx@ and down by @dy@.
move :: Double -> Double -> Shape -> Shape
move :: Double -> Double -> Shape -> Shape
move Double
dx Double
dy = \case
  Piece WireKind
k (Line (Double, Double)
a (Double, Double)
b) -> WireKind -> Path -> Shape
Piece WireKind
k ((Double, Double) -> (Double, Double) -> Path
Line ((Double, Double) -> (Double, Double)
at (Double, Double)
a) ((Double, Double) -> (Double, Double)
at (Double, Double)
b))
  Piece WireKind
k (Curve (Double, Double)
a (Double, Double)
b) -> WireKind -> Path -> Shape
Piece WireKind
k ((Double, Double) -> (Double, Double) -> Path
Curve ((Double, Double) -> (Double, Double)
at (Double, Double)
a) ((Double, Double) -> (Double, Double)
at (Double, Double)
b))
  Piece WireKind
k (Loop NonEmpty (Double, Double)
ps) -> WireKind -> Path -> Shape
Piece WireKind
k (NonEmpty (Double, Double) -> Path
Loop (((Double, Double) -> (Double, Double))
-> NonEmpty (Double, Double) -> NonEmpty (Double, Double)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Double, Double) -> (Double, Double)
at NonEmpty (Double, Double)
ps))
  Piece WireKind
k (Quarter (Double, Double)
a (Double, Double)
b) -> WireKind -> Path -> Shape
Piece WireKind
k ((Double, Double) -> (Double, Double) -> Path
Quarter ((Double, Double) -> (Double, Double)
at (Double, Double)
a) ((Double, Double) -> (Double, Double)
at (Double, Double)
b))
  Box (Double, Double)
a (Double, Double)
b String
s -> (Double, Double) -> (Double, Double) -> String -> Shape
Box ((Double, Double) -> (Double, Double)
at (Double, Double)
a) ((Double, Double) -> (Double, Double)
at (Double, Double)
b) String
s
  Frame (Double, Double)
a (Double, Double)
b -> (Double, Double) -> (Double, Double) -> Shape
Frame ((Double, Double) -> (Double, Double)
at (Double, Double)
a) ((Double, Double) -> (Double, Double)
at (Double, Double)
b)
  Bracket (Double, Double)
a (Double, Double)
b Bool
down -> (Double, Double) -> (Double, Double) -> Bool -> Shape
Bracket ((Double, Double) -> (Double, Double)
at (Double, Double)
a) ((Double, Double) -> (Double, Double)
at (Double, Double)
b) Bool
down
  Point (Double, Double)
a Bool
f -> (Double, Double) -> Bool -> Shape
Point ((Double, Double) -> (Double, Double)
at (Double, Double)
a) Bool
f
  Label (Double, Double)
a String
s -> (Double, Double) -> String -> Shape
Label ((Double, Double) -> (Double, Double)
at (Double, Double)
a) String
s
  Boundary (Double, Double)
a String
s -> (Double, Double) -> String -> Shape
Boundary ((Double, Double) -> (Double, Double)
at (Double, Double)
a) String
s
  Equals (Double, Double)
a -> (Double, Double) -> Shape
Equals ((Double, Double) -> (Double, Double)
at (Double, Double)
a)
  where
    at :: (Double, Double) -> (Double, Double)
at (Double
x, Double
y) = (Double
x Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
dx, Double
y Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
dy)

-- | Where a wire enters a drawing along its top or leaves it along its bottom: how far along, the
-- kind of wire, and, for a leg of a copy or merge point that may trade places with the point's
-- other leg, which point it is a leg of.
data Port = Port {Port -> Double
portX :: Double, Port -> WireKind
portKind :: WireKind, Port -> Maybe Int
portLegs :: Maybe Int}
  deriving (Int -> Port -> String -> String
[Port] -> String -> String
Port -> String
(Int -> Port -> String -> String)
-> (Port -> String) -> ([Port] -> String -> String) -> Show Port
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Port -> String -> String
showsPrec :: Int -> Port -> String -> String
$cshow :: Port -> String
show :: Port -> String
$cshowList :: [Port] -> String -> String
showList :: [Port] -> String -> String
Show)

port :: Double -> WireKind -> Port
port :: Double -> WireKind -> Port
port Double
x WireKind
k = Double -> WireKind -> Maybe Int -> Port
Port Double
x WireKind
k Maybe Int
forall a. Maybe a
Nothing

-- | A port moved right by @dx@.
shiftPort :: Double -> Port -> Port
shiftPort :: Double -> Port -> Port
shiftPort Double
dx Port
p = Port
p{portX = portX p + dx}

-- | A drawn diagram: its size, its input and output ports, and its shapes.
data Geo = Geo
  { Geo -> Double
geoWidth :: Double
  , Geo -> Double
geoHeight :: Double
  , Geo -> [Port]
geoIns :: [Port]
  , Geo -> [Port]
geoOuts :: [Port]
  , Geo -> [Shape]
geoShapes :: [Shape]
  }
  deriving (Int -> Geo -> String -> String
[Geo] -> String -> String
Geo -> String
(Int -> Geo -> String -> String)
-> (Geo -> String) -> ([Geo] -> String -> String) -> Show Geo
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Geo -> String -> String
showsPrec :: Int -> Geo -> String -> String
$cshow :: Geo -> String
show :: Geo -> String
$cshowList :: [Geo] -> String -> String
showList :: [Geo] -> String -> String
Show)

-- | How a diagram is drawn. A diagram that only permutes its wires has no height of its own: its
-- crossings are drawn in the band where the wires next change position, so that a 'swap' next to
-- a box does not make the box taller.
data Layout
  = -- | output @j@ continues input @p !! j@, with the kinds of the inputs and of the outputs
    Wiring [Int] [WireKind] [WireKind]
  | Stage Geo
  deriving (Int -> Layout -> String -> String
[Layout] -> String -> String
Layout -> String
(Int -> Layout -> String -> String)
-> (Layout -> String)
-> ([Layout] -> String -> String)
-> Show Layout
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Layout -> String -> String
showsPrec :: Int -> Layout -> String -> String
$cshow :: Layout -> String
show :: Layout -> String
$cshowList :: [Layout] -> String -> String
showList :: [Layout] -> String -> String
Show)

-- | The distance between neighbouring wires.
slot :: Double
slot :: Double
slot = Double
32

-- | The length of wire above and below a box.
stub :: Double
stub :: Double
stub = Double
10

-- | The height of a box.
boxHeight :: Double
boxHeight :: Double
boxHeight = Double
24

-- | The distance between the rails of neighbouring trace loops.
loopGap :: Double
loopGap :: Double
loopGap = Double
14

-- | How far the innermost trace loop runs below and above the diagram it loops round, clear of
-- the wire labels.
loopClearance :: Double
loopClearance :: Double
loopClearance = Double
6

-- | The width of a name, roughly, in the box font.
textWidth :: String -> Double
textWidth :: String -> Double
textWidth String
s = Double
7.5 Double -> Double -> Double
forall a. Num a => a -> a -> a
* Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (String -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length String
s)

-- | The positions of @n@ wires, one slot apart.
slots :: Int -> [Double]
slots :: Int -> [Double]
slots Int
n = [Double
slot Double -> Double -> Double
forall a. Num a => a -> a -> a
* (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
k Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
0.5) | Int
k <- [Int
0 .. Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]

width :: Int -> Double
width :: Int -> Double
width Int
n = Double
slot Double -> Double -> Double
forall a. Num a => a -> a -> a
* Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n

-- | Ports at the given positions, for wires of the given kinds.
ports :: [Double] -> [WireKind] -> [Port]
ports :: [Double] -> [WireKind] -> [Port]
ports = (Double -> WireKind -> Port) -> [Double] -> [WireKind] -> [Port]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Double -> WireKind -> Port
port

-- | A permutation of wires of the given kinds, drawn over the given height.
wiringGeo :: Double -> [Int] -> [WireKind] -> [WireKind] -> Geo
wiringGeo :: Double -> [Int] -> [WireKind] -> [WireKind] -> Geo
wiringGeo Double
h [Int]
p [WireKind]
ks [WireKind]
os =
  let xs :: [Double]
xs = Int -> [Double]
slots ([Int] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Int]
p)
  in Geo
       { geoWidth :: Double
geoWidth = Int -> Double
width ([Int] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Int]
p)
       , geoHeight :: Double
geoHeight = Double
h
       , geoIns :: [Port]
geoIns = [Double] -> [WireKind] -> [Port]
ports [Double]
xs [WireKind]
ks
       , geoOuts :: [Port]
geoOuts = [Double] -> [WireKind] -> [Port]
ports [Double]
xs [WireKind]
os
       , geoShapes :: [Shape]
geoShapes = [WireKind -> Path -> Shape
Piece ([WireKind]
ks [WireKind] -> Int -> WireKind
forall a. HasCallStack => [a] -> Int -> a
!! Int
i) ((Double, Double) -> (Double, Double) -> Path
Curve ([Double]
xs [Double] -> Int -> Double
forall a. HasCallStack => [a] -> Int -> a
!! Int
i, Double
0) (Double
x, Double
h)) | (Double
x, Int
i) <- [Double] -> [Int] -> [(Double, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Double]
xs [Int]
p]
       }

-- | Straight wires of the given kinds at the given positions, from the top down to @h@.
verticals :: Double -> [Double] -> [WireKind] -> [Shape]
verticals :: Double -> [Double] -> [WireKind] -> [Shape]
verticals Double
h [Double]
xs [WireKind]
ks = [WireKind -> Path -> Shape
Piece WireKind
u ((Double, Double) -> (Double, Double) -> Path
Line (Double
x, Double
0) (Double
x, Double
h)) | (Double
x, WireKind
u) <- [Double] -> [WireKind] -> [(Double, WireKind)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Double]
xs [WireKind]
ks]

-- | A layout as geometry, a permutation drawn over the given height.
toGeo :: Double -> Layout -> Geo
toGeo :: Double -> Layout -> Geo
toGeo Double
h (Wiring [Int]
p [WireKind]
ks [WireKind]
os) = Double -> [Int] -> [WireKind] -> [WireKind] -> Geo
wiringGeo Double
h [Int]
p [WireKind]
ks [WireKind]
os
toGeo Double
_ (Stage Geo
g) = Geo
g

layoutHeight :: Layout -> Double
layoutHeight :: Layout -> Double
layoutHeight Wiring{} = Double
0
layoutHeight (Stage Geo
g) = Geo -> Double
geoHeight Geo
g

-- | Geometry made taller, centred, with its wires extended to the new top and bottom.
stretch :: Double -> Geo -> Geo
stretch :: Double -> Geo -> Geo
stretch Double
h Geo
g
  | Double
h Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Geo -> Double
geoHeight Geo
g = Geo
g
  | Bool
otherwise =
      Geo
g
        { geoHeight = h
        , geoShapes =
            map (move 0 pad) (geoShapes g)
              ++ [Piece k (Line (x, 0) (x, pad)) | Port x k _ <- geoIns g]
              ++ [Piece k (Line (x, pad + geoHeight g) (x, h)) | Port x k _ <- geoOuts g]
        }
  where
    pad :: Double
pad = (Double
h Double -> Double -> Double
forall a. Num a => a -> a -> a
- Geo -> Double
geoHeight Geo
g) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
2

-- | Two layouts side by side, as tall as the taller one.
tensor :: Layout -> Layout -> Layout
tensor :: Layout -> Layout -> Layout
tensor (Wiring [Int]
p [WireKind]
ks [WireKind]
os) (Wiring [Int]
q [WireKind]
ls [WireKind]
ps) = [Int] -> [WireKind] -> [WireKind] -> Layout
Wiring ([Int]
p [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Int]
p) [Int]
q) ([WireKind]
ks [WireKind] -> [WireKind] -> [WireKind]
forall a. [a] -> [a] -> [a]
++ [WireKind]
ls) ([WireKind]
os [WireKind] -> [WireKind] -> [WireKind]
forall a. [a] -> [a] -> [a]
++ [WireKind]
ps)
tensor Layout
l Layout
r =
  let h :: Double
h = Double -> Double -> Double
forall a. Ord a => a -> a -> a
max (Layout -> Double
layoutHeight Layout
l) (Layout -> Double
layoutHeight Layout
r)
      gl :: Geo
gl = Double -> Geo -> Geo
stretch Double
h (Double -> Layout -> Geo
toGeo Double
h Layout
l)
      gr :: Geo
gr = Double -> Geo -> Geo
stretch Double
h (Double -> Layout -> Geo
toGeo Double
h Layout
r)
      w :: Double
w = Geo -> Double
geoWidth Geo
gl
      -- the points on the right are numbered after those on the left
      n :: Int
n = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: Type -> Type) a. (Foldable t, Ord a) => t a -> a
maximum (-Int
1 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int
i | Port Double
_ WireKind
_ (Just Int
i) <- Geo -> [Port]
geoIns Geo
gl [Port] -> [Port] -> [Port]
forall a. [a] -> [a] -> [a]
++ Geo -> [Port]
geoOuts Geo
gl])
      right :: Port -> Port
right Port
q = (Double -> Port -> Port
shiftPort Double
w Port
q){portLegs = (+ n) <$> portLegs q}
  in Geo -> Layout
Stage
       Geo
         { geoWidth :: Double
geoWidth = Double
w Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Geo -> Double
geoWidth Geo
gr
         , geoHeight :: Double
geoHeight = Double
h
         , geoIns :: [Port]
geoIns = Geo -> [Port]
geoIns Geo
gl [Port] -> [Port] -> [Port]
forall a. [a] -> [a] -> [a]
++ (Port -> Port) -> [Port] -> [Port]
forall a b. (a -> b) -> [a] -> [b]
map Port -> Port
right (Geo -> [Port]
geoIns Geo
gr)
         , geoOuts :: [Port]
geoOuts = Geo -> [Port]
geoOuts Geo
gl [Port] -> [Port] -> [Port]
forall a. [a] -> [a] -> [a]
++ (Port -> Port) -> [Port] -> [Port]
forall a b. (a -> b) -> [a] -> [b]
map Port -> Port
right (Geo -> [Port]
geoOuts Geo
gr)
         , geoShapes :: [Shape]
geoShapes = Geo -> [Shape]
geoShapes Geo
gl [Shape] -> [Shape] -> [Shape]
forall a. [a] -> [a] -> [a]
++ (Shape -> Shape) -> [Shape] -> [Shape]
forall a b. (a -> b) -> [a] -> [b]
map (Double -> Double -> Shape -> Shape
move Double
w Double
0) (Geo -> [Shape]
geoShapes Geo
gr)
         }

-- | The layout of @after . before@. A permutation is absorbed into the layout next to it, so its
-- crossings end up in the next band.
compose :: Layout -> Layout -> Layout
compose :: Layout -> Layout -> Layout
compose (Wiring [Int]
p [WireKind]
_ [WireKind]
os) (Wiring [Int]
q [WireKind]
ls [WireKind]
_) = [Int] -> [WireKind] -> [WireKind] -> Layout
Wiring ((Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map ([Int]
q [Int] -> Int -> Int
forall a. HasCallStack => [a] -> Int -> a
!!) [Int]
p) [WireKind]
ls [WireKind]
os
compose (Stage Geo
g) (Wiring [Int]
p [WireKind]
ks [WireKind]
_) = Geo -> Layout
Stage Geo
g{geoIns = [(geoIns g !! j){portKind = k} | (j, k) <- zip (inverse p) ks]}
compose (Wiring [Int]
p [WireKind]
_ [WireKind]
os) (Stage Geo
f) = Geo -> Layout
Stage Geo
f{geoOuts = [(geoOuts f !! i){portKind = k} | (i, k) <- zip p os]}
compose (Stage Geo
g) (Stage Geo
f) = Geo -> Layout
Stage (Geo -> Geo -> Geo
stack Geo
f Geo
g)

inverse :: [Int] -> [Int]
inverse :: [Int] -> [Int]
inverse [Int]
p = ((Int, Int) -> Int) -> [(Int, Int)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Int) -> Int
forall a b. (a, b) -> b
snd ([(Int, Int)] -> [(Int, Int)]
forall a. Ord a => [a] -> [a]
List.sort ([Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
p [Int
0 ..]))

-- | @before@ above @after@, with a band of wires between them. The two are placed so that the wires
-- between them move sideways as little as possible.
stack :: Geo -> Geo -> Geo
stack :: Geo -> Geo -> Geo
stack Geo
f0 Geo
g0 =
  let f :: Geo
f = Geo
f0{geoOuts = untangle (map portX (geoIns g0)) (geoOuts f0)}
      g :: Geo
g = Geo
g0{geoIns = untangle (map portX (geoOuts f)) (geoIns g0)}
      dxs :: [Double]
dxs = (Port -> Port -> Double) -> [Port] -> [Port] -> [Double]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Port
a Port
b -> Port -> Double
portX Port
a Double -> Double -> Double
forall a. Num a => a -> a -> a
- Port -> Double
portX Port
b) (Geo -> [Port]
geoOuts Geo
f) (Geo -> [Port]
geoIns Geo
g)
      off :: Double
off = if [Double] -> Bool
forall a. [a] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [Double]
dxs then (Geo -> Double
geoWidth Geo
f Double -> Double -> Double
forall a. Num a => a -> a -> a
- Geo -> Double
geoWidth Geo
g) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
2 else [Double] -> [Double]
forall a. Ord a => [a] -> [a]
List.sort [Double]
dxs [Double] -> Int -> Double
forall a. HasCallStack => [a] -> Int -> a
!! ([Double] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Double]
dxs Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2)
      sf :: Double
sf = Double -> Double
forall a. Num a => a -> a
negate (Double -> Double -> Double
forall a. Ord a => a -> a -> a
min Double
0 Double
off)
      sg :: Double
sg = Double
off Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
sf
      ends :: [(Double, Double, WireKind)]
ends = [(Port -> Double
portX Port
a Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
sf, Port -> Double
portX Port
b Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
sg, Port -> WireKind
portKind Port
a) | (Port
a, Port
b) <- [Port] -> [Port] -> [(Port, Port)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Geo -> [Port]
geoOuts Geo
f) (Geo -> [Port]
geoIns Geo
g)]
      hb :: Double
hb = Double -> Double
bandHeight ([Double] -> Double
forall a. Ord a => [a] -> a
forall (t :: Type -> Type) a. (Foldable t, Ord a) => t a -> a
maximum (Double
0 Double -> [Double] -> [Double]
forall a. a -> [a] -> [a]
: [Double -> Double
forall a. Num a => a -> a
abs (Double
a Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
b) | (Double
a, Double
b, WireKind
_) <- [(Double, Double, WireKind)]
ends]))
      hf :: Double
hf = Geo -> Double
geoHeight Geo
f
  in Geo
       { geoWidth :: Double
geoWidth = Double -> Double -> Double
forall a. Ord a => a -> a -> a
max (Geo -> Double
geoWidth Geo
f Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
sf) (Geo -> Double
geoWidth Geo
g Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
sg)
       , geoHeight :: Double
geoHeight = Double
hf Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
hb Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Geo -> Double
geoHeight Geo
g
       , geoIns :: [Port]
geoIns = (Port -> Port) -> [Port] -> [Port]
forall a b. (a -> b) -> [a] -> [b]
map (Double -> Port -> Port
shiftPort Double
sf) (Geo -> [Port]
geoIns Geo
f)
       , geoOuts :: [Port]
geoOuts = (Port -> Port) -> [Port] -> [Port]
forall a b. (a -> b) -> [a] -> [b]
map (Double -> Port -> Port
shiftPort Double
sg) (Geo -> [Port]
geoOuts Geo
g)
       , geoShapes :: [Shape]
geoShapes =
           (Shape -> Shape) -> [Shape] -> [Shape]
forall a b. (a -> b) -> [a] -> [b]
map (Double -> Double -> Shape -> Shape
move Double
sf Double
0) (Geo -> [Shape]
geoShapes Geo
f)
             [Shape] -> [Shape] -> [Shape]
forall a. [a] -> [a] -> [a]
++ [WireKind -> Path -> Shape
Piece WireKind
u ((Double, Double) -> (Double, Double) -> Path
Curve (Double
a, Double
hf) (Double
b, Double
hf Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
hb)) | (Double
a, Double
b, WireKind
u) <- [(Double, Double, WireKind)]
ends]
             [Shape] -> [Shape] -> [Shape]
forall a. [a] -> [a] -> [a]
++ (Shape -> Shape) -> [Shape] -> [Shape]
forall a b. (a -> b) -> [a] -> [b]
map (Double -> Double -> Shape -> Shape
move Double
sg (Double
hf Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
hb)) (Geo -> [Shape]
geoShapes Geo
g)
       }

-- | Ports with the legs of each point that may trade places reordered, so that they run to their
-- targets without crossing each other.
untangle :: [Double] -> [Port] -> [Port]
untangle :: [Double] -> [Port] -> [Port]
untangle [Double]
targets [Port]
ps = [Port
p{portX = fromMaybe (portX p) (lookup i moved)} | (Int
i, Port
p) <- [Int] -> [Port] -> [(Int, Port)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [Port]
ps]
  where
    legs :: [(Int, Int)]
legs = [(Int
i, Int
l) | (Int
i, Port Double
_ WireKind
_ (Just Int
l)) <- [Int] -> [Port] -> [(Int, Port)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] [Port]
ps]
    groups :: [[Int]]
groups = (NonEmpty (Int, Int) -> [Int]) -> [NonEmpty (Int, Int)] -> [[Int]]
forall a b. (a -> b) -> [a] -> [b]
map (((Int, Int) -> Int) -> [(Int, Int)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Int) -> Int
forall a b. (a, b) -> a
fst ([(Int, Int)] -> [Int])
-> (NonEmpty (Int, Int) -> [(Int, Int)])
-> NonEmpty (Int, Int)
-> [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
. NonEmpty (Int, Int) -> [(Int, Int)]
forall a. NonEmpty a -> [a]
NE.toList) (((Int, Int) -> Int) -> [(Int, Int)] -> [NonEmpty (Int, Int)]
forall b a. Ord b => (a -> b) -> [a] -> [NonEmpty a]
NE.groupAllWith (Int, Int) -> Int
forall a b. (a, b) -> b
snd [(Int, Int)]
legs)
    moved :: [(Int, Double)]
moved = [[(Int, Double)]] -> [(Int, Double)]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat [[Int] -> [Double] -> [(Int, Double)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Int -> Double) -> [Int] -> [Int]
forall b a. Ord b => (a -> b) -> [a] -> [a]
List.sortOn ([Double]
targets [Double] -> Int -> Double
forall a. HasCallStack => [a] -> Int -> a
!!) [Int]
grp) ([Double] -> [Double]
forall a. Ord a => [a] -> [a]
List.sort ((Int -> Double) -> [Int] -> [Double]
forall a b. (a -> b) -> [a] -> [b]
map (Port -> Double
portX (Port -> Double) -> (Int -> Port) -> Int -> Double
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
. ([Port]
ps [Port] -> Int -> Port
forall a. HasCallStack => [a] -> Int -> a
!!)) [Int]
grp)) | [Int]
grp <- [[Int]]
groups]

-- | The height of a band whose wires move sideways by at most @d@.
bandHeight :: Double -> Double
bandHeight :: Double -> Double
bandHeight Double
d
  | Double
d Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
0.5 = Double
0
  | Bool
otherwise = Double -> Double -> Double
forall a. Ord a => a -> a -> a
max Double
16 (Double -> Double -> Double
forall a. Ord a => a -> a -> a
min Double
64 (Double
0.6 Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
d))

-- | A box with inputs of the given kinds, and outputs with the given labels and kinds. Unit wires
-- get no label.
nodeGeo :: [WireKind] -> [(String, WireKind)] -> String -> Geo
nodeGeo :: [WireKind] -> [(String, WireKind)] -> String -> Geo
nodeGeo [WireKind]
inKinds [(String, WireKind)]
outWires String
s =
  Geo
    { geoWidth :: Double
geoWidth = Double
w
    , geoHeight :: Double
geoHeight = Double
h
    , geoIns :: [Port]
geoIns = [Double] -> [WireKind] -> [Port]
ports [Double]
ins [WireKind]
inKinds
    , geoOuts :: [Port]
geoOuts = [Double] -> [WireKind] -> [Port]
ports [Double]
outs (((String, WireKind) -> WireKind)
-> [(String, WireKind)] -> [WireKind]
forall a b. (a -> b) -> [a] -> [b]
map (String, WireKind) -> WireKind
forall a b. (a, b) -> b
snd [(String, WireKind)]
outWires)
    , geoShapes :: [Shape]
geoShapes =
        [WireKind -> Path -> Shape
Piece WireKind
u ((Double, Double) -> (Double, Double) -> Path
Line (Double
x, Double
0) (Double
x, Double
stub)) | (Double
x, WireKind
u) <- [Double] -> [WireKind] -> [(Double, WireKind)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Double]
ins [WireKind]
inKinds]
          [Shape] -> [Shape] -> [Shape]
forall a. [a] -> [a] -> [a]
++ [WireKind -> Path -> Shape
Piece WireKind
u ((Double, Double) -> (Double, Double) -> Path
Line (Double
x, Double
stub Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
boxHeight) (Double
x, Double
h)) | (Double
x, (String
_, WireKind
u)) <- [Double] -> [(String, WireKind)] -> [(Double, (String, WireKind))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Double]
outs [(String, WireKind)]
outWires]
          [Shape] -> [Shape] -> [Shape]
forall a. [a] -> [a] -> [a]
++ [(Double, Double) -> (Double, Double) -> String -> Shape
Box ((Double
w Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
bw) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
2, Double
stub) ((Double
w Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
bw) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
2, Double
stub Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
boxHeight) String
s]
          [Shape] -> [Shape] -> [Shape]
forall a. [a] -> [a] -> [a]
++ [(Double, Double) -> String -> Shape
Label (Double
x Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
3, Double
stub Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
boxHeight Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
9) String
o | (Double
x, (String
o, WireKind
ok)) <- [Double] -> [(String, WireKind)] -> [(Double, (String, WireKind))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Double]
outs [(String, WireKind)]
outWires, WireKind
ok WireKind -> WireKind -> Bool
forall a. Eq a => a -> a -> Bool
/= WireKind
UnitWire]
    }
  where
    n :: Int
n = [WireKind] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [WireKind]
inKinds
    m :: Int
m = [(String, WireKind)] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [(String, WireKind)]
outWires
    k :: Int
k = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
1 (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
n Int
m)
    bw :: Double
bw = Double -> Double -> Double
forall a. Ord a => a -> a -> a
max (String -> Double
textWidth String
s Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
14) (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
slot Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
18)
    w :: Double
w = Double -> Double -> Double
forall a. Ord a => a -> a -> a
max (Double
bw Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
8) (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
k Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
slot)
    h :: Double
h = Double
stub Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
boxHeight Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
stub
    at :: Int -> [Double]
at Int
c = [Double
w Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
2 Double -> Double -> Double
forall a. Num a => a -> a -> a
+ (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i Double -> Double -> Double
forall a. Num a => a -> a -> a
- Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
2) Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
slot | Int
i <- [Int
0 .. Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]
    ins :: [Double]
ins = Int -> [Double]
at Int
n
    outs :: [Double]
outs = Int -> [Double]
at Int
m

-- | The points of a (co)monoid, one on each wire of the given kinds; nothing drawn when there are
-- no wires. The legs of copy and merge points may trade places when @free@.
points :: Bool -> PointKind -> [WireKind] -> Layout
points :: Bool -> PointKind -> [WireKind] -> Layout
points Bool
_ PointKind
_ [] = [Int] -> [WireKind] -> [WireKind] -> Layout
Wiring [] [] []
points Bool
free PointKind
pk [WireKind]
ks = Geo -> Layout
Stage (Geo -> Layout) -> Geo -> Layout
forall a b. (a -> b) -> a -> b
$ case PointKind
pk of
  PointKind
UnitPoint -> Geo
unit
  PointKind
DiscardPoint -> Geo -> Geo
mirror Geo
unit
  PointKind
MergePoint -> Geo
merge
  PointKind
CopyPoint -> Geo -> Geo
mirror Geo
merge
  where
    n :: Int
n = [WireKind] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [WireKind]
ks
    xs :: [Double]
xs = Int -> [Double]
slots Int
n
    -- each copy or merge point forks to two slots; the first legs are listed before the second
    -- ones, so with several wires the next band sorts them
    firsts :: [Double]
firsts = [Double
slot Double -> Double -> Double
forall a. Num a => a -> a -> a
* (Double
2 Double -> Double -> Double
forall a. Num a => a -> a -> a
* Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
0.5) | Int
i <- [Int
0 .. Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]
    seconds :: [Double]
seconds = (Double -> Double) -> [Double] -> [Double]
forall a b. (a -> b) -> [a] -> [b]
map (Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
slot) [Double]
firsts
    ps :: [Double]
ps = (Double -> Double -> Double) -> [Double] -> [Double] -> [Double]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Double
l Double
r -> (Double
l Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
r) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
2) [Double]
firsts [Double]
seconds
    leg :: Int -> Maybe Int
leg Int
i = if Bool
free then Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i else Maybe Int
forall a. Maybe a
Nothing
    legs :: [Port]
legs = [Double -> WireKind -> Maybe Int -> Port
Port Double
x WireKind
u (Int -> Maybe Int
leg Int
i) | (Int
i, Double
x, WireKind
u) <- [Int] -> [Double] -> [WireKind] -> [(Int, Double, WireKind)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Int
0 ..] [Double]
firsts [WireKind]
ks] [Port] -> [Port] -> [Port]
forall a. [a] -> [a] -> [a]
++ [Double -> WireKind -> Maybe Int -> Port
Port Double
x WireKind
u (Int -> Maybe Int
leg Int
i) | (Int
i, Double
x, WireKind
u) <- [Int] -> [Double] -> [WireKind] -> [(Int, Double, WireKind)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Int
0 ..] [Double]
seconds [WireKind]
ks]
    -- the wires stop at the edge of a hollow point, so that the background shows through it
    unit :: Geo
unit =
      Double -> Double -> [Port] -> [Port] -> [Shape] -> Geo
Geo (Int -> Double
width Int
n) Double
12 [] ([Double] -> [WireKind] -> [Port]
ports [Double]
xs [WireKind]
ks) ([[Shape]] -> [Shape]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat [[WireKind -> Path -> Shape
Piece WireKind
u ((Double, Double) -> (Double, Double) -> Path
Line (Double
x, Double
7) (Double
x, Double
12)), (Double, Double) -> Bool -> Shape
Point (Double
x, Double
4) Bool
False] | (Double
x, WireKind
u) <- [Double] -> [WireKind] -> [(Double, WireKind)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Double]
xs [WireKind]
ks])
    merge :: Geo
merge =
      Double -> Double -> [Port] -> [Port] -> [Shape] -> Geo
Geo
        (Int -> Double
width (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n))
        Double
20
        [Port]
legs
        ([Double] -> [WireKind] -> [Port]
ports [Double]
ps [WireKind]
ks)
        ( [[Shape]] -> [Shape]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat
            [ [WireKind -> Path -> Shape
Piece WireKind
u ((Double, Double) -> (Double, Double) -> Path
Curve (Double
l, Double
0) (Double
x, Double
11)), WireKind -> Path -> Shape
Piece WireKind
u ((Double, Double) -> (Double, Double) -> Path
Curve (Double
r, Double
0) (Double
x, Double
11)), WireKind -> Path -> Shape
Piece WireKind
u ((Double, Double) -> (Double, Double) -> Path
Line (Double
x, Double
17) (Double
x, Double
20)), (Double, Double) -> Bool -> Shape
Point (Double
x, Double
14) Bool
False]
            | (Double
x, Double
l, Double
r, WireKind
u) <- [Double]
-> [Double]
-> [Double]
-> [WireKind]
-> [(Double, Double, Double, WireKind)]
forall a b c d. [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
List.zip4 [Double]
ps [Double]
firsts [Double]
seconds [WireKind]
ks
            ]
        )

-- | The height of a swap drawn on its own.
swapHeight :: Double
swapHeight :: Double
swapHeight = Double
24

-- | A permutation of wires of the given kinds, drawn on its own when @explicit@.
permutation :: Bool -> [WireKind] -> [Int] -> Layout
permutation :: Bool -> [WireKind] -> [Int] -> Layout
permutation Bool
explicit [WireKind]
ks [Int]
p =
  let os :: [WireKind]
os = (Int -> WireKind) -> [Int] -> [WireKind]
forall a b. (a -> b) -> [a] -> [b]
map ([WireKind]
ks [WireKind] -> Int -> WireKind
forall a. HasCallStack => [a] -> Int -> a
!!) [Int]
p
  in if Bool
explicit then Geo -> Layout
Stage (Double -> [Int] -> [WireKind] -> [WireKind] -> Geo
wiringGeo Double
swapHeight [Int]
p [WireKind]
ks [WireKind]
os) else [Int] -> [WireKind] -> [WireKind] -> Layout
Wiring [Int]
p [WireKind]
ks [WireKind]
os

-- | The identity on wires of the given kinds, drawn in a dashed frame when @explicit@.
identity :: Bool -> [WireKind] -> Layout
identity :: Bool -> [WireKind] -> Layout
identity Bool
explicit [WireKind]
ks
  | Bool
explicit =
      let n :: Int
n = [WireKind] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [WireKind]
ks
          w :: Double
w = if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Double
slot Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
2 else Int -> Double
width Int
n
          h :: Double
h = Double
18
          xs :: [Double]
xs = Int -> [Double]
slots Int
n
      in Geo -> Layout
Stage
           ( Double -> Double -> [Port] -> [Port] -> [Shape] -> Geo
Geo
               Double
w
               Double
h
               ([Double] -> [WireKind] -> [Port]
ports [Double]
xs [WireKind]
ks)
               ([Double] -> [WireKind] -> [Port]
ports [Double]
xs [WireKind]
ks)
               (Double -> [Double] -> [WireKind] -> [Shape]
verticals Double
h [Double]
xs [WireKind]
ks [Shape] -> [Shape] -> [Shape]
forall a. [a] -> [a] -> [a]
++ [(Double, Double) -> (Double, Double) -> Shape
Frame (Double
2, Double
3) (Double
w Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
2, Double
h Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
3)])
           )
  | Bool
otherwise = [Int] -> [WireKind] -> [WireKind] -> Layout
Wiring [Int
0 .. [WireKind] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [WireKind]
ks Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1] [WireKind]
ks [WireKind]
ks

-- | Bends joining each wire of the given kinds to its dual: for a 'Cup' the wires and then their
-- duals leave along the bottom, for a 'Cap' the duals and then the wires enter along the top.
-- Each bend changes style at its apex.
bend :: BendKind -> [WireKind] -> [WireKind] -> Layout
bend :: BendKind -> [WireKind] -> [WireKind] -> Layout
bend BendKind
_ [] [WireKind]
_ = [Int] -> [WireKind] -> [WireKind] -> Layout
Wiring [] [] []
bend BendKind
kind [WireKind]
ka [WireKind]
kd =
  let m :: Int
m = [WireKind] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [WireKind]
ka
      h :: Double
h = Double
18
      xs :: [Double]
xs = Int -> [Double]
slots (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
m)
      ([Double]
lefts, [Double]
rights) = Int -> [Double] -> ([Double], [Double])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
m [Double]
xs
      -- bends with the given kinds on their left and on their right halves, opening downwards
      cups :: [WireKind] -> [WireKind] -> Geo
cups [WireKind]
ls [WireKind]
rs =
        Double -> Double -> [Port] -> [Port] -> [Shape] -> Geo
Geo (Int -> Double
width (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
m)) Double
h [] ([Double] -> [WireKind] -> [Port]
ports [Double]
xs ([WireKind]
ls [WireKind] -> [WireKind] -> [WireKind]
forall a. [a] -> [a] -> [a]
++ [WireKind]
rs)) ([Shape] -> Geo) -> [Shape] -> Geo
forall a b. (a -> b) -> a -> b
$
          [[Shape]] -> [Shape]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat
            [ [WireKind -> Path -> Shape
Piece WireKind
k ((Double, Double) -> (Double, Double) -> Path
Quarter (Double
l, Double
h) ((Double
l Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
r) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
2, Double
3)), WireKind -> Path -> Shape
Piece WireKind
k' ((Double, Double) -> (Double, Double) -> Path
Quarter (Double
r, Double
h) ((Double
l Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
r) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
2, Double
3))]
            | (Double
l, Double
r, WireKind
k, WireKind
k') <- [Double]
-> [Double]
-> [WireKind]
-> [WireKind]
-> [(Double, Double, WireKind, WireKind)]
forall a b c d. [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
List.zip4 [Double]
lefts [Double]
rights [WireKind]
ls [WireKind]
rs
            ]
  in Geo -> Layout
Stage (Geo -> Layout) -> Geo -> Layout
forall a b. (a -> b) -> a -> b
$ case BendKind
kind of
       BendKind
Cup -> [WireKind] -> [WireKind] -> Geo
cups [WireKind]
ka [WireKind]
kd
       BendKind
Cap -> Geo -> Geo
mirror ([WireKind] -> [WireKind] -> Geo
cups [WireKind]
kd [WireKind]
ka)

-- | An associator from the grouping given to the other one, on wires of the given kinds: the
-- wires with a bracket over the pair grouped at the top and one under the pair grouped at the
-- bottom.
rebracket :: Grouping -> [WireKind] -> [WireKind] -> [WireKind] -> Geo
rebracket :: Grouping -> [WireKind] -> [WireKind] -> [WireKind] -> Geo
rebracket Grouping
grouping [WireKind]
ka [WireKind]
kb [WireKind]
kc =
  let ks :: [WireKind]
ks = [WireKind]
ka [WireKind] -> [WireKind] -> [WireKind]
forall a. [a] -> [a] -> [a]
++ [WireKind]
kb [WireKind] -> [WireKind] -> [WireKind]
forall a. [a] -> [a] -> [a]
++ [WireKind]
kc
      n :: Int
n = [WireKind] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [WireKind]
ks
      h :: Double
h = Double
30
      xs :: [Double]
xs = Int -> [Double]
slots Int
n
      group :: Int -> Int -> [(Double, Double)]
group Int
from Int
to
        | Int
to Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
from = []
        | Bool
otherwise = [([Double]
xs [Double] -> Int -> Double
forall a. HasCallStack => [a] -> Int -> a
!! Int
from Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
slot Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
3, [Double]
xs [Double] -> Int -> Double
forall a. HasCallStack => [a] -> Int -> a
!! (Int
to Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
slot Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
3)]
      ab :: [(Double, Double)]
ab = Int -> Int -> [(Double, Double)]
group Int
0 ([WireKind] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [WireKind]
ka Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [WireKind] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [WireKind]
kb)
      bc :: [(Double, Double)]
bc = Int -> Int -> [(Double, Double)]
group ([WireKind] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [WireKind]
ka) Int
n
      leftFirst :: Geo
leftFirst =
        Double -> Double -> [Port] -> [Port] -> [Shape] -> Geo
Geo
          (Int -> Double
width Int
n)
          Double
h
          ([Double] -> [WireKind] -> [Port]
ports [Double]
xs [WireKind]
ks)
          ([Double] -> [WireKind] -> [Port]
ports [Double]
xs [WireKind]
ks)
          ( Double -> [Double] -> [WireKind] -> [Shape]
verticals Double
h [Double]
xs [WireKind]
ks
              [Shape] -> [Shape] -> [Shape]
forall a. [a] -> [a] -> [a]
++ [(Double, Double) -> (Double, Double) -> Bool -> Shape
Bracket (Double
x0, Double
6) (Double
x1, Double
6) Bool
True | (Double
x0, Double
x1) <- [(Double, Double)]
ab]
              [Shape] -> [Shape] -> [Shape]
forall a. [a] -> [a] -> [a]
++ [(Double, Double) -> (Double, Double) -> Bool -> Shape
Bracket (Double
x0, Double
h Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
6) (Double
x1, Double
h Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
6) Bool
False | (Double
x0, Double
x1) <- [(Double, Double)]
bc]
          )
  in case Grouping
grouping of Grouping
LeftFirst -> Geo
leftFirst; Grouping
RightFirst -> Geo -> Geo
mirror Geo
leftFirst

-- | A unitor on wires of the given kinds: a dotted unit wire that runs into the outermost wire on
-- its side or out of it.
unitor :: Side -> Direction -> [WireKind] -> Geo
unitor :: Side -> Direction -> [WireKind] -> Geo
unitor Side
side Direction
dir [WireKind]
ks =
  let n :: Int
n = [WireKind] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [WireKind]
ks
      h :: Double
h = Double
16
      xs :: [Double]
xs = case Side
side of Side
OnLeft -> (Double -> Double) -> [Double] -> [Double]
forall a b. (a -> b) -> [a] -> [b]
map (Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
slot) (Int -> [Double]
slots Int
n); Side
OnRight -> Int -> [Double]
slots Int
n
      xu :: Double
xu = case Side
side of Side
OnLeft -> Double
slot Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
2; Side
OnRight -> Double
slot Double -> Double -> Double
forall a. Num a => a -> a -> a
* (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
0.5)
      other :: [Double]
other = case Side
side of Side
OnLeft -> Int -> [Double] -> [Double]
forall a. Int -> [a] -> [a]
take Int
1 [Double]
xs; Side
OnRight -> Int -> [Double] -> [Double]
forall a. Int -> [a] -> [a]
drop (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [Double]
xs
      place :: forall t. t -> [t] -> [t]
      place :: forall a. a -> [a] -> [a]
place t
u [t]
us = case Side
side of Side
OnLeft -> t
u t -> [t] -> [t]
forall a. a -> [a] -> [a]
: [t]
us; Side
OnRight -> [t]
us [t] -> [t] -> [t]
forall a. [a] -> [a] -> [a]
++ [t
u]
      joining :: Path
joining = case [Double]
other of
        [Double
x] -> (Double, Double) -> (Double, Double) -> Path
Curve (Double
xu, Double
0) (Double
x, Double
h)
        [Double]
_ -> (Double, Double) -> (Double, Double) -> Path
Line (Double
xu, Double
0) (Double
xu, Double
h Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
2)
      absorb :: Geo
absorb =
        Double -> Double -> [Port] -> [Port] -> [Shape] -> Geo
Geo
          (Int -> Double
width (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))
          Double
h
          ([Double] -> [WireKind] -> [Port]
ports (Double -> [Double] -> [Double]
forall a. a -> [a] -> [a]
place Double
xu [Double]
xs) (WireKind -> [WireKind] -> [WireKind]
forall a. a -> [a] -> [a]
place WireKind
UnitWire [WireKind]
ks))
          ([Double] -> [WireKind] -> [Port]
ports [Double]
xs [WireKind]
ks)
          (WireKind -> Path -> Shape
Piece WireKind
UnitWire Path
joining Shape -> [Shape] -> [Shape]
forall a. a -> [a] -> [a]
: Double -> [Double] -> [WireKind] -> [Shape]
verticals Double
h [Double]
xs [WireKind]
ks)
  in case Direction
dir of Direction
Absorb -> Geo
absorb; Direction
Create -> Geo -> Geo
mirror Geo
absorb

-- | The end of a unit wire.
unitEnd :: Geo
unitEnd :: Geo
unitEnd = Double -> Double -> [Port] -> [Port] -> [Shape] -> Geo
Geo Double
slot Double
8 [Double -> WireKind -> Port
port (Double
slot Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
2) WireKind
UnitWire] [] [WireKind -> Path -> Shape
Piece WireKind
UnitWire ((Double, Double) -> (Double, Double) -> Path
Line (Double
slot Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
2, Double
0) (Double
slot Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
2, Double
8))]

-- | Geometry upside down: its inputs become its outputs and the other way round, so that a merge
-- point becomes a copy point, a cup a cap, and so on. A point is filled when it was hollow and
-- hollow when it was filled, as the points of a comonoid are the mirror images of a monoid's. A
-- piece of wire still runs from top to bottom, except a bend's, which runs towards its apex.
mirror :: Geo -> Geo
mirror :: Geo -> Geo
mirror Geo
g = Geo
g{geoIns = geoOuts g, geoOuts = geoIns g, geoShapes = map flipShape (geoShapes g)}
  where
    h :: Double
h = Geo -> Double
geoHeight Geo
g
    f :: (Double, Double) -> (Double, Double)
f (Double
x, Double
y) = (Double
x, Double
h Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
y)
    corners :: (Double, Double)
-> (Double, Double) -> ((Double, Double), (Double, Double))
corners (Double
x0, Double
y0) (Double
x1, Double
y1) = ((Double
x0, Double
h Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
y1), (Double
x1, Double
h Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
y0))
    flipShape :: Shape -> Shape
flipShape = \case
      Piece WireKind
k (Line (Double, Double)
a (Double, Double)
b) -> WireKind -> Path -> Shape
Piece WireKind
k ((Double, Double) -> (Double, Double) -> Path
Line ((Double, Double) -> (Double, Double)
f (Double, Double)
b) ((Double, Double) -> (Double, Double)
f (Double, Double)
a))
      Piece WireKind
k (Curve (Double, Double)
a (Double, Double)
b) -> WireKind -> Path -> Shape
Piece WireKind
k ((Double, Double) -> (Double, Double) -> Path
Curve ((Double, Double) -> (Double, Double)
f (Double, Double)
b) ((Double, Double) -> (Double, Double)
f (Double, Double)
a))
      Piece WireKind
k (Loop NonEmpty (Double, Double)
ps) -> WireKind -> Path -> Shape
Piece WireKind
k (NonEmpty (Double, Double) -> Path
Loop (NonEmpty (Double, Double) -> NonEmpty (Double, Double)
forall a. NonEmpty a -> NonEmpty a
NE.reverse (((Double, Double) -> (Double, Double))
-> NonEmpty (Double, Double) -> NonEmpty (Double, Double)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Double, Double) -> (Double, Double)
f NonEmpty (Double, Double)
ps)))
      Piece WireKind
k (Quarter (Double, Double)
a (Double, Double)
b) -> WireKind -> Path -> Shape
Piece WireKind
k ((Double, Double) -> (Double, Double) -> Path
Quarter ((Double, Double) -> (Double, Double)
f (Double, Double)
a) ((Double, Double) -> (Double, Double)
f (Double, Double)
b))
      Box (Double, Double)
a (Double, Double)
b String
s -> ((Double, Double) -> (Double, Double) -> String -> Shape)
-> ((Double, Double), (Double, Double)) -> String -> Shape
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Double, Double) -> (Double, Double) -> String -> Shape
Box ((Double, Double)
-> (Double, Double) -> ((Double, Double), (Double, Double))
corners (Double, Double)
a (Double, Double)
b) String
s
      Frame (Double, Double)
a (Double, Double)
b -> ((Double, Double) -> (Double, Double) -> Shape)
-> ((Double, Double), (Double, Double)) -> Shape
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Double, Double) -> (Double, Double) -> Shape
Frame ((Double, Double)
-> (Double, Double) -> ((Double, Double), (Double, Double))
corners (Double, Double)
a (Double, Double)
b)
      Bracket (Double, Double)
a (Double, Double)
b Bool
down -> (Double, Double) -> (Double, Double) -> Bool -> Shape
Bracket ((Double, Double) -> (Double, Double)
f (Double, Double)
a) ((Double, Double) -> (Double, Double)
f (Double, Double)
b) (Bool -> Bool
not Bool
down)
      Point (Double, Double)
a Bool
filled -> (Double, Double) -> Bool -> Shape
Point ((Double, Double) -> (Double, Double)
f (Double, Double)
a) (Bool -> Bool
not Bool
filled)
      Label (Double, Double)
a String
s -> (Double, Double) -> String -> Shape
Label ((Double, Double) -> (Double, Double)
f (Double, Double)
a) String
s
      Boundary (Double, Double)
a String
s -> (Double, Double) -> String -> Shape
Boundary ((Double, Double) -> (Double, Double)
f (Double, Double)
a) String
s
      Equals (Double, Double)
a -> (Double, Double) -> Shape
Equals ((Double, Double) -> (Double, Double)
f (Double, Double)
a)

-- | The first @k@ wires fed back from the outputs to the inputs, each looping round the side where
-- it crosses fewer other wires. The loops on one side are nested: the one whose ends are nearest
-- that side runs innermost.
loops :: Int -> Geo -> Geo
loops :: Int -> Geo -> Geo
loops Int
k Geo
g =
  Geo
    { geoWidth :: Double
geoWidth = Double
left Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
w Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
right
    , geoHeight :: Double
geoHeight = Double
depth Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
h Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
depth
    , geoIns :: [Port]
geoIns = (Port -> Port) -> [Port] -> [Port]
forall a b. (a -> b) -> [a] -> [b]
map (Double -> Port -> Port
shiftPort Double
left) (Int -> [Port] -> [Port]
forall a. Int -> [a] -> [a]
drop Int
k (Geo -> [Port]
geoIns Geo
g))
    , geoOuts :: [Port]
geoOuts = (Port -> Port) -> [Port] -> [Port]
forall a b. (a -> b) -> [a] -> [b]
map (Double -> Port -> Port
shiftPort Double
left) (Int -> [Port] -> [Port]
forall a. Int -> [a] -> [a]
drop Int
k (Geo -> [Port]
geoOuts Geo
g))
    , geoShapes :: [Shape]
geoShapes =
        (Shape -> Shape) -> [Shape] -> [Shape]
forall a b. (a -> b) -> [a] -> [b]
map (Double -> Double -> Shape -> Shape
move Double
left Double
depth) (Geo -> [Shape]
geoShapes Geo
g)
          [Shape] -> [Shape] -> [Shape]
forall a. [a] -> [a] -> [a]
++ [WireKind -> Path -> Shape
Piece WireKind
u ((Double, Double) -> (Double, Double) -> Path
Line (Double
x Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
left, Double
0) (Double
x Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
left, Double
depth)) | Port Double
x WireKind
u Maybe Int
_ <- Int -> [Port] -> [Port]
forall a. Int -> [a] -> [a]
drop Int
k (Geo -> [Port]
geoIns Geo
g)]
          [Shape] -> [Shape] -> [Shape]
forall a. [a] -> [a] -> [a]
++ [WireKind -> Path -> Shape
Piece WireKind
u ((Double, Double) -> (Double, Double) -> Path
Line (Double
x Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
left, Double
depth Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
h) (Double
x Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
left, Double
depth Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
h Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
depth)) | Port Double
x WireKind
u Maybe Int
_ <- Int -> [Port] -> [Port]
forall a. Int -> [a] -> [a]
drop Int
k (Geo -> [Port]
geoOuts Geo
g)]
          [Shape] -> [Shape] -> [Shape]
forall a. [a] -> [a] -> [a]
++ (Int -> (Double, Double, WireKind) -> Shape)
-> [Int] -> [(Double, Double, WireKind)] -> [Shape]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Double
-> (Double -> Double) -> Int -> (Double, Double, WireKind) -> Shape
loop Double
0 (\Double
d -> Double
left Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
d)) [Int
1 ..] (((Double, Double, WireKind) -> Double)
-> [(Double, Double, WireKind)] -> [(Double, Double, WireKind)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
List.sortOn (\(Double
a, Double
b, WireKind
_) -> Double -> Double -> Double
forall a. Ord a => a -> a -> a
min Double
a Double
b) [(Double, Double, WireKind)]
lefts)
          [Shape] -> [Shape] -> [Shape]
forall a. [a] -> [a] -> [a]
++ (Int -> (Double, Double, WireKind) -> Shape)
-> [Int] -> [(Double, Double, WireKind)] -> [Shape]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Double
-> (Double -> Double) -> Int -> (Double, Double, WireKind) -> Shape
loop (Double
loopGap Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
2) (\Double
d -> Double
left Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
w Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
d)) [Int
1 ..] (((Double, Double, WireKind) -> Double)
-> [(Double, Double, WireKind)] -> [(Double, Double, WireKind)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
List.sortOn (\(Double
a, Double
b, WireKind
_) -> Double -> Double
forall a. Num a => a -> a
negate (Double -> Double -> Double
forall a. Ord a => a -> a -> a
max Double
a Double
b)) [(Double, Double, WireKind)]
rights)
    }
  where
    w :: Double
w = Geo -> Double
geoWidth Geo
g
    h :: Double
h = Geo -> Double
geoHeight Geo
g
    ([(Double, Double, WireKind)]
lefts, [(Double, Double, WireKind)]
rights) = ((Double, Double, WireKind) -> Bool)
-> [(Double, Double, WireKind)]
-> ([(Double, Double, WireKind)], [(Double, Double, WireKind)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition (Double, Double, WireKind) -> Bool
goesLeft [(Port -> Double
portX Port
a, Port -> Double
portX Port
b, Port -> WireKind
portKind Port
a) | (Port
a, Port
b) <- Int -> [(Port, Port)] -> [(Port, Port)]
forall a. Int -> [a] -> [a]
take Int
k ([Port] -> [Port] -> [(Port, Port)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Geo -> [Port]
geoIns Geo
g) (Geo -> [Port]
geoOuts Geo
g))]
    -- a loop goes round the side where it crosses fewer of the wires that carry on, and round the
    -- side its ends are nearest to when that is a tie
    carryOn :: [Double]
carryOn = (Port -> Double) -> [Port] -> [Double]
forall a b. (a -> b) -> [a] -> [b]
map Port -> Double
portX (Int -> [Port] -> [Port]
forall a. Int -> [a] -> [a]
drop Int
k (Geo -> [Port]
geoIns Geo
g) [Port] -> [Port] -> [Port]
forall a. [a] -> [a] -> [a]
++ Int -> [Port] -> [Port]
forall a. Int -> [a] -> [a]
drop Int
k (Geo -> [Port]
geoOuts Geo
g))
    goesLeft :: (Double, Double, WireKind) -> Bool
goesLeft (Double
a, Double
b, WireKind
_) =
      let crossLeft :: Int
crossLeft = [Double] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length ((Double -> Bool) -> [Double] -> [Double]
forall a. (a -> Bool) -> [a] -> [a]
filter (Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double -> Double -> Double
forall a. Ord a => a -> a -> a
min Double
a Double
b) [Double]
carryOn)
          crossRight :: Int
crossRight = [Double] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length ((Double -> Bool) -> [Double] -> [Double]
forall a. (a -> Bool) -> [a] -> [a]
filter (Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
> Double -> Double -> Double
forall a. Ord a => a -> a -> a
max Double
a Double
b) [Double]
carryOn)
      in Int
crossLeft Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
crossRight Bool -> Bool -> Bool
|| (Int
crossLeft Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
crossRight Bool -> Bool -> Bool
&& Double
a Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
b Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
w)
    left :: Double
left = Double
loopGap Double -> Double -> Double
forall a. Num a => a -> a -> a
* Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([(Double, Double, WireKind)] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [(Double, Double, WireKind)]
lefts)
    right :: Double
right = Double
loopGap Double -> Double -> Double
forall a. Num a => a -> a -> a
* Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([(Double, Double, WireKind)] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [(Double, Double, WireKind)]
rights)
    depth :: Double
depth = Double
loopClearance Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
loopGap Double -> Double -> Double
forall a. Num a => a -> a -> a
* Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max ([(Double, Double, WireKind)] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [(Double, Double, WireKind)]
lefts) ([(Double, Double, WireKind)] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [(Double, Double, WireKind)]
rights))
    -- the loops on the right run half a gap higher than those on the left, so that a left and a
    -- right loop cross instead of running along each other
    loop :: Double -> (Double -> Double) -> Int -> (Double, Double, WireKind) -> Shape
    loop :: Double
-> (Double -> Double) -> Int -> (Double, Double, WireKind) -> Shape
loop Double
lift Double -> Double
rail Int
level (Double
xi, Double
xo, WireKind
u) =
      let d :: Double
d = Double
loopGap Double -> Double -> Double
forall a. Num a => a -> a -> a
* Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
level
          v :: Double
v = Double
loopClearance Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
d Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
lift
          x :: Double
x = Double -> Double
rail Double
d
      in WireKind -> Path -> Shape
Piece WireKind
u (Path -> Shape) -> Path -> Shape
forall a b. (a -> b) -> a -> b
$
           NonEmpty (Double, Double) -> Path
Loop
             ( (Double
xo Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
left, Double
depth Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
h)
                 (Double, Double) -> [(Double, Double)] -> NonEmpty (Double, Double)
forall a. a -> [a] -> NonEmpty a
:| [ (Double
xo Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
left, Double
depth Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
h Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
v)
                    , (Double
x, Double
depth Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
h Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
v)
                    , (Double
x, Double
depth Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
v)
                    , (Double
xi Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
left, Double
depth Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
v)
                    , (Double
xi Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
left, Double
depth)
                    ]
             )

-- * Rendering

-- | The height of the row of boundary labels.
labelRow :: Double
labelRow :: Double
labelRow = Double
16

-- | Geometry with its boundary: the input labels above and the output labels below, each joined
-- to its wire by a band @top@ and @bottom@ tall. Legs that may trade places are put in the
-- boundary's order.
framed :: Double -> Double -> [(String, WireKind)] -> [(String, WireKind)] -> Geo -> Geo
framed :: Double
-> Double
-> [(String, WireKind)]
-> [(String, WireKind)]
-> Geo
-> Geo
framed Double
top Double
bottom [(String, WireKind)]
ins [(String, WireKind)]
outs Geo
g =
  Geo
    { geoWidth :: Double
geoWidth = Geo -> Double
geoWidth Geo
g
    , geoHeight :: Double
geoHeight = Double
labelRow Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
top Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Geo -> Double
geoHeight Geo
g Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
bottom Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
labelRow
    , geoIns :: [Port]
geoIns = []
    , geoOuts :: [Port]
geoOuts = []
    , geoShapes :: [Shape]
geoShapes =
        [(Double, Double) -> String -> Shape
Boundary (Double
x, Double
labelRow Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
4) String
s | (Double
x, (String
s, WireKind
_)) <- [Double] -> [(String, WireKind)] -> [(Double, (String, WireKind))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Double]
inXs [(String, WireKind)]
ins]
          [Shape] -> [Shape] -> [Shape]
forall a. [a] -> [a] -> [a]
++ [WireKind -> Path -> Shape
Piece WireKind
u ((Double, Double) -> (Double, Double) -> Path
Curve (Double
x, Double
labelRow) (Double
y, Double
labelRow Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
top)) | (Double
x, Double
y, (String
_, WireKind
u)) <- [Double]
-> [Double]
-> [(String, WireKind)]
-> [(Double, Double, (String, WireKind))]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Double]
inXs [Double]
inYs [(String, WireKind)]
ins]
          [Shape] -> [Shape] -> [Shape]
forall a. [a] -> [a] -> [a]
++ (Shape -> Shape) -> [Shape] -> [Shape]
forall a b. (a -> b) -> [a] -> [b]
map (Double -> Double -> Shape -> Shape
move Double
0 (Double
labelRow Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
top)) (Geo -> [Shape]
geoShapes Geo
g)
          [Shape] -> [Shape] -> [Shape]
forall a. [a] -> [a] -> [a]
++ [WireKind -> Path -> Shape
Piece WireKind
u ((Double, Double) -> (Double, Double) -> Path
Curve (Double
y, Double
bottomAt) (Double
x, Double
bottomAt Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
bottom)) | (Double
x, Double
y, (String
_, WireKind
u)) <- [Double]
-> [Double]
-> [(String, WireKind)]
-> [(Double, Double, (String, WireKind))]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Double]
outXs [Double]
outYs [(String, WireKind)]
outs]
          [Shape] -> [Shape] -> [Shape]
forall a. [a] -> [a] -> [a]
++ [(Double, Double) -> String -> Shape
Boundary (Double
x, Double
bottomAt Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
bottom Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
labelRow Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
3) String
s | (Double
x, (String
s, WireKind
_)) <- [Double] -> [(String, WireKind)] -> [(Double, (String, WireKind))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Double]
outXs [(String, WireKind)]
outs]
    }
  where
    inYs :: [Double]
inYs = [Port] -> [Double]
inOrder (Geo -> [Port]
geoIns Geo
g)
    outYs :: [Double]
outYs = [Port] -> [Double]
inOrder (Geo -> [Port]
geoOuts Geo
g)
    inXs :: [Double]
inXs = [Double] -> [Double]
forall a. Ord a => [a] -> [a]
List.sort [Double]
inYs
    outXs :: [Double]
outXs = [Double] -> [Double]
forall a. Ord a => [a] -> [a]
List.sort [Double]
outYs
    bottomAt :: Double
bottomAt = Double
labelRow Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
top Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Geo -> Double
geoHeight Geo
g

-- | The positions of ports, the legs of each point that may trade places put in the order of the
-- wires.
inOrder :: [Port] -> [Double]
inOrder :: [Port] -> [Double]
inOrder [Port]
ps = (Port -> Double) -> [Port] -> [Double]
forall a b. (a -> b) -> [a] -> [b]
map Port -> Double
portX ([Double] -> [Port] -> [Port]
untangle ((Int -> Double) -> [Int] -> [Double]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral [Int
0 .. [Port] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Port]
ps Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]) [Port]
ps)

-- | The height of the bands joining the boundary to the wires.
boundaryBands :: Geo -> (Double, Double)
boundaryBands :: Geo -> (Double, Double)
boundaryBands Geo
g =
  let band :: [Double] -> Double
band [Double]
xs = Double -> Double -> Double
forall a. Ord a => a -> a -> a
max Double
8 (Double -> Double
bandHeight ([Double] -> Double
forall a. Ord a => [a] -> a
forall (t :: Type -> Type) a. (Foldable t, Ord a) => t a -> a
maximum (Double
0 Double -> [Double] -> [Double]
forall a. a -> [a] -> [a]
: (Double -> Double -> Double) -> [Double] -> [Double] -> [Double]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Double
a Double
b -> Double -> Double
forall a. Num a => a -> a
abs (Double
a Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
b)) ([Double] -> [Double]
forall a. Ord a => [a] -> [a]
List.sort [Double]
xs) [Double]
xs)))
  in ([Double] -> Double
band ([Port] -> [Double]
inOrder (Geo -> [Port]
geoIns Geo
g)), [Double] -> Double
band ([Port] -> [Double]
inOrder (Geo -> [Port]
geoOuts Geo
g)))

-- | The diagram as an SVG document, with the 'defaultOptions'.
render :: forall (as :: [W]) (bs :: [W]). Svg (S as) (S bs) -> String
render :: forall (as :: [W]) (bs :: [W]). Svg (S as) (S bs) -> String
render = Options -> Svg (S as) (S bs) -> String
forall (as :: [W]) (bs :: [W]).
Options -> Svg (S as) (S bs) -> String
renderWith Options
defaultOptions

-- | The diagram as an SVG document.
renderWith :: forall (as :: [W]) (bs :: [W]). Options -> Svg (S as) (S bs) -> String
renderWith :: forall (as :: [W]) (bs :: [W]).
Options -> Svg (S as) (S bs) -> String
renderWith Options
o (Svg Dot (D (Erase as)) (D (Erase bs))
_ Diagram
d) = forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs) =>
Options -> [Diagram] -> String
sideBySide @as @bs Options
o [Diagram
d]

-- | Two parallel diagrams side by side, with an equals sign between them, with the
-- 'defaultOptions'.
renderEquation :: forall (as :: [W]) (bs :: [W]). Svg (S as) (S bs) -> Svg (S as) (S bs) -> String
renderEquation :: forall (as :: [W]) (bs :: [W]).
Svg (S as) (S bs) -> Svg (S as) (S bs) -> String
renderEquation = Options -> Svg (S as) (S bs) -> Svg (S as) (S bs) -> String
forall (as :: [W]) (bs :: [W]).
Options -> Svg (S as) (S bs) -> Svg (S as) (S bs) -> String
renderEquationWith Options
defaultOptions

-- | Two parallel diagrams side by side, with an equals sign between them. Neither is simplified:
-- the picture shows two different diagrams that mean the same.
renderEquationWith
  :: forall (as :: [W]) (bs :: [W]). Options -> Svg (S as) (S bs) -> Svg (S as) (S bs) -> String
renderEquationWith :: forall (as :: [W]) (bs :: [W]).
Options -> Svg (S as) (S bs) -> Svg (S as) (S bs) -> String
renderEquationWith Options
o (Svg Dot (D (Erase as)) (D (Erase bs))
_ Diagram
l) (Svg Dot (D (Erase as)) (D (Erase bs))
_ Diagram
r) = forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs) =>
Options -> [Diagram] -> String
sideBySide @as @bs Options
o [Diagram
l, Diagram
r]

-- | Diagrams from the wires @as@ to the wires @bs@ as one SVG document: side by side, each with
-- the boundary labels, stretched to the height of the tallest, and with an equals sign between
-- each and the next.
sideBySide :: forall (as :: [W]) (bs :: [W]). (IsList as, IsList bs) => Options -> [Diagram] -> String
sideBySide :: forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs) =>
Options -> [Diagram] -> String
sideBySide Options
o [Diagram]
ds =
  let ls :: [Layout]
ls = (Diagram -> Layout) -> [Diagram] -> [Layout]
forall a b. (a -> b) -> [a] -> [b]
map (Options -> Diagram -> Layout
layout Options
o) [Diagram]
ds
      h :: Double
h = [Double] -> Double
forall a. Ord a => [a] -> a
forall (t :: Type -> Type) a. (Foldable t, Ord a) => t a -> a
maximum (Double
0 Double -> [Double] -> [Double]
forall a. a -> [a] -> [a]
: (Layout -> Double) -> [Layout] -> [Double]
forall a b. (a -> b) -> [a] -> [b]
map Layout -> Double
layoutHeight [Layout]
ls)
      gs :: [Geo]
gs = [Double -> Geo -> Geo
stretch Double
h (Double -> Layout -> Geo
toGeo (Double -> Double -> Double
forall a. Ord a => a -> a -> a
max Double
h Double
slot) Layout
l) | Layout
l <- [Layout]
ls]
      bands :: [(Double, Double)]
bands = (Geo -> (Double, Double)) -> [Geo] -> [(Double, Double)]
forall a b. (a -> b) -> [a] -> [b]
map Geo -> (Double, Double)
boundaryBands [Geo]
gs
      side :: Geo -> Geo
side = Double
-> Double
-> [(String, WireKind)]
-> [(String, WireKind)]
-> Geo
-> Geo
framed ([Double] -> Double
forall a. Ord a => [a] -> a
forall (t :: Type -> Type) a. (Foldable t, Ord a) => t a -> a
maximum (Double
0 Double -> [Double] -> [Double]
forall a. a -> [a] -> [a]
: ((Double, Double) -> Double) -> [(Double, Double)] -> [Double]
forall a b. (a -> b) -> [a] -> [b]
map (Double, Double) -> Double
forall a b. (a, b) -> a
fst [(Double, Double)]
bands)) ([Double] -> Double
forall a. Ord a => [a] -> a
forall (t :: Type -> Type) a. (Foldable t, Ord a) => t a -> a
maximum (Double
0 Double -> [Double] -> [Double]
forall a. a -> [a] -> [a]
: ((Double, Double) -> Double) -> [(Double, Double)] -> [Double]
forall a b. (a -> b) -> [a] -> [b]
map (Double, Double) -> Double
forall a b. (a, b) -> b
snd [(Double, Double)]
bands)) (Options -> [(String, WireKind)] -> [(String, WireKind)]
visible Options
o (forall (ws :: [W]). IsList ws => [(String, WireKind)]
wires @as)) (Options -> [(String, WireKind)] -> [(String, WireKind)]
visible Options
o (forall (ws :: [W]). IsList ws => [(String, WireKind)]
wires @bs))
      fs :: [Geo]
fs = (Geo -> Geo) -> [Geo] -> [Geo]
forall a b. (a -> b) -> [a] -> [b]
map Geo -> Geo
side [Geo]
gs
      -- each side starts where the one before it ends, with room for the equals sign between
      offsets :: [Double]
offsets = (Double -> Geo -> Double) -> Double -> [Geo] -> [Double]
forall b a. (b -> a -> b) -> b -> [a] -> [b]
scanl (\Double
x Geo
f -> Double
x Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Geo -> Double
geoWidth Geo
f Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
48) Double
0 [Geo]
fs
      equalsAt :: Double
equalsAt = case [Geo]
fs of Geo
f : [Geo]
_ -> Geo -> Double
geoHeight Geo
f Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
2; [] -> Double
0
      placed :: Int -> Double -> Geo -> [Shape]
placed Int
i Double
x Geo
f = [(Double, Double) -> Shape
Equals (Double
x Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
24, Double
equalsAt) | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> (Int
0 :: Int)] [Shape] -> [Shape] -> [Shape]
forall a. [a] -> [a] -> [a]
++ (Shape -> Shape) -> [Shape] -> [Shape]
forall a b. (a -> b) -> [a] -> [b]
map (Double -> Double -> Shape -> Shape
move Double
x Double
0) (Geo -> [Shape]
geoShapes Geo
f)
  in Geo -> String
document
       Geo
         { geoWidth :: Double
geoWidth = [Double] -> Double
forall a. HasCallStack => [a] -> a
last [Double]
offsets Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
48
         , geoHeight :: Double
geoHeight = [Double] -> Double
forall a. Ord a => [a] -> a
forall (t :: Type -> Type) a. (Foldable t, Ord a) => t a -> a
maximum (Double
0 Double -> [Double] -> [Double]
forall a. a -> [a] -> [a]
: (Geo -> Double) -> [Geo] -> [Double]
forall a b. (a -> b) -> [a] -> [b]
map Geo -> Double
geoHeight [Geo]
fs)
         , geoIns :: [Port]
geoIns = []
         , geoOuts :: [Port]
geoOuts = []
         , geoShapes :: [Shape]
geoShapes = [[Shape]] -> [Shape]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat ((Int -> Double -> Geo -> [Shape])
-> [Int] -> [Double] -> [Geo] -> [[Shape]]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Int -> Double -> Geo -> [Shape]
placed [Int
0 ..] [Double]
offsets [Geo]
fs)
         }

-- | The laws of @cs@ drawn with the 'defaultOptions', see 'lawSvgsWith'.
lawSvgs :: forall (cs :: [Kind -> Constraint]). (Laws cs, All cs SVG) => [(String, String)]
lawSvgs :: forall (cs :: [Type -> Constraint]).
(Laws cs, All cs SVG) =>
[(String, String)]
lawSvgs = forall (cs :: [Type -> Constraint]).
(Laws cs, All cs SVG) =>
Options -> [(String, String)]
lawSvgsWith @cs Options
defaultOptions

-- | The laws of @cs@, each drawn as an equation by 'renderEquationWith', with its name. The object
-- variables are single wires @'Wire' "a"@ to @'Wire' "e"@, and the arrows a law asks for are 'node's with the names
-- it gives them.
lawSvgsWith :: forall (cs :: [Kind -> Constraint]). (Laws cs, All cs SVG) => Options -> [(String, String)]
lawSvgsWith :: forall (cs :: [Type -> Constraint]).
(Laws cs, All cs SVG) =>
Options -> [(String, String)]
lawSvgsWith Options
o = [(Law cs -> String
forall (cs :: [Type -> Constraint]). Law cs -> String
lawName Law cs
law, Law cs -> String
draw Law cs
law) | Law cs
law <- forall (cs :: [Type -> Constraint]). Laws cs => [Law cs]
laws @cs]
  where
    draw :: Law cs -> String
    draw :: Law cs -> String
draw (Law String
_ LawBody cs
body) = Equation SVG
-> (forall (a :: SVG) (b :: SVG). (a ~> b) -> (a ~> b) -> String)
-> String
forall {k} r.
Equation k
-> (forall (a :: k) (b :: k). (a ~> b) -> (a ~> b) -> r) -> r
withSides (Identity (Equation SVG) -> Equation SVG
forall a. Identity a -> a
runIdentity (LawBody cs
forall (a :: SVG) (b :: SVG) (c :: SVG) (d :: SVG) (e :: SVG)
       (m :: Type -> Type).
(Labelled SVG, All cs SVG, Monad m, Ob a, Ob b, Ob c, Ob d,
 Ob e) =>
(forall (x :: SVG) (y :: SVG).
 (Ob x, Ob y) =>
 String -> m (x ~> y))
-> m (Equation SVG)
body @(S '[Wire "a"]) @(S '[Wire "b"]) @(S '[Wire "c"]) @(S '[Wire "d"]) @(S '[Wire "e"]) String -> Identity (x ~> y)
String -> Identity (S (UN S x) ~> S (UN S y))
forall (x :: SVG) (y :: SVG).
(Ob x, Ob y) =>
String -> Identity (x ~> y)
box)) \l :: a ~> b
l@Svg{} a ~> b
r ->
      Options -> Svg (S as) (S bs) -> Svg (S as) (S bs) -> String
forall (as :: [W]) (bs :: [W]).
Options -> Svg (S as) (S bs) -> Svg (S as) (S bs) -> String
renderEquationWith Options
o a ~> b
Svg (S as) (S bs)
l a ~> b
Svg (S as) (S bs)
r
    box :: forall (x :: SVG) (y :: SVG). (Ob x, Ob y) => String -> Identity (x ~> y)
    box :: forall (x :: SVG) (y :: SVG).
(Ob x, Ob y) =>
String -> Identity (x ~> y)
box String
s = Svg (S (UN S x)) (S (UN S y))
-> Identity (Svg (S (UN S x)) (S (UN S y)))
forall a. a -> Identity a
Identity (forall (as :: [W]) (bs :: [W]).
(IsList as, IsList bs) =>
String -> Svg (S as) (S bs)
node @(UN S x) @(UN S y) String
s)

-- | An SVG document showing the geometry. Wires, outlines and text use the current colour. Boxes
-- are not filled, and the wires stop at the edge of a hollow point, so the background shows
-- through both. Only the core of a dual wire is painted, in @--sd-paper@ (white when it is not
-- set), which a page can set to its background.
document :: Geo -> String
document :: Geo -> String
document Geo
g =
  String
"<svg xmlns=\"http://www.w3.org/2000/svg\" class=\"sd\" viewBox=\""
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((Double -> String) -> [Double] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Double -> String
num [-Double
margin, -Double
margin, Geo -> Double
geoWidth Geo
g Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
2 Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
margin, Geo -> Double
geoHeight Geo
g Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
2 Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
margin])
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\" width=\""
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ Double -> String
num (Geo -> Double
geoWidth Geo
g Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
2 Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
margin)
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\" height=\""
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ Double -> String
num (Geo -> Double
geoHeight Geo
g Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
2 Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
margin)
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\"><style>"
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".sd path{fill:none;stroke:currentColor;stroke-width:1.3;stroke-linecap:round}"
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".sd .u path{stroke-dasharray:1.3 2.6}"
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".sd .d path{stroke-linecap:butt;stroke-width:4}"
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".sd .di path{stroke:var(--sd-paper,#fff);stroke-width:1.6}"
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".sd rect,.sd .h{fill:none;stroke:currentColor;stroke-width:1.3}"
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".sd .f{fill:currentColor}"
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".sd .id{stroke-width:0.8;stroke-dasharray:3 2}"
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".sd .br{stroke-width:0.9}"
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".sd text{fill:currentColor;font-family:'STIX Two Text','Times New Roman',serif;font-style:italic}"
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".sd .n{font-size:15px;text-anchor:middle;dominant-baseline:central}"
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".sd .l{font-size:11px}"
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".sd .b{font-size:13px;text-anchor:middle}"
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".sd .e{font-size:22px;font-style:normal;text-anchor:middle;dominant-baseline:central}"
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"</style>"
    -- the outlines of all dual wires go below all their cores, so that where two dual wires meet or
    -- cross the cores run on unbroken
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
group String
"d" [String]
duals
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
group String
"di" [String]
duals
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> String) -> [String] -> String
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap String -> String
path (WireKind -> [String]
chains WireKind
Plain)
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
group String
"u" (WireKind -> [String]
chains WireKind
UnitWire)
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat [Shape -> String
shape Shape
x | Shape
x <- Geo -> [Shape]
geoShapes Geo
g, Bool -> Bool
not (Shape -> Bool
isPiece Shape
x), Bool -> Bool
not (Shape -> Bool
isText Shape
x)]
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat [Shape -> String
shape Shape
x | Shape
x <- Geo -> [Shape]
geoShapes Geo
g, Shape -> Bool
isText Shape
x]
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"</svg>"
  where
    margin :: Double
margin = Double
8
    -- the pieces of wire of one kind, joined into as few paths as possible, so that no seams show
    duals :: [String]
duals = WireKind -> [String]
chains WireKind
DualWire
    chains :: WireKind -> [String]
chains WireKind
k = [((Double, Double), (Double, Double), String)] -> [String]
joined [Path -> ((Double, Double), (Double, Double), String)
segment Path
p | Piece WireKind
k' Path
p <- Geo -> [Shape]
geoShapes Geo
g, WireKind
k' WireKind -> WireKind -> Bool
forall a. Eq a => a -> a -> Bool
== WireKind
k]
    group :: String -> [String] -> String
group String
_ [] = String
""
    group String
cls [String]
ds = String
"<g class=\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cls String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\">" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> String) -> [String] -> String
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap String -> String
path [String]
ds String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"</g>"
    isPiece :: Shape -> Bool
isPiece = \case Piece{} -> Bool
True; Shape
_ -> Bool
False
    isText :: Shape -> Bool
isText = \case Label{} -> Bool
True; Boundary{} -> Bool
True; Equals{} -> Bool
True; Shape
_ -> Bool
False

-- | Where a piece of wire starts and ends, and the SVG path from its start.
segment :: Path -> (Pt, Pt, String)
segment :: Path -> ((Double, Double), (Double, Double), String)
segment = \case
  Line (Double, Double)
a (Double, Double)
b -> ((Double, Double)
a, (Double, Double)
b, String
"L" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Double, Double) -> String
pt (Double, Double)
b)
  Curve a :: (Double, Double)
a@(Double
ax, Double
ay) b :: (Double, Double)
b@(Double
bx, Double
by)
    | Double -> Double
forall a. Num a => a -> a
abs (Double
ax Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
bx) Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
0.5 -> ((Double, Double)
a, (Double, Double)
b, String
"L" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Double, Double) -> String
pt (Double, Double)
b)
    | Bool
otherwise -> let my :: Double
my = (Double
ay Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
by) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
2 in ((Double, Double)
a, (Double, Double)
b, String
"C" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Double, Double) -> String
pt (Double
ax, Double
my) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Double, Double) -> String
pt (Double
bx, Double
my) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Double, Double) -> String
pt (Double, Double)
b)
  Loop NonEmpty (Double, Double)
ps -> (NonEmpty (Double, Double) -> (Double, Double)
forall a. NonEmpty a -> a
NE.head NonEmpty (Double, Double)
ps, NonEmpty (Double, Double) -> (Double, Double)
forall a. NonEmpty a -> a
NE.last NonEmpty (Double, Double)
ps, NonEmpty (Double, Double) -> String
rounded NonEmpty (Double, Double)
ps)
  Quarter a :: (Double, Double)
a@(Double
ax, Double
ay) b :: (Double, Double)
b@(Double
bx, Double
by) ->
    ((Double, Double)
a, (Double, Double)
b, String
"C" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Double, Double) -> String
pt (Double
ax, Double
ay Double -> Double -> Double
forall a. Num a => a -> a -> a
+ (Double
by Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
ay) Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
kappa) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Double, Double) -> String
pt (Double
bx Double -> Double -> Double
forall a. Num a => a -> a -> a
- (Double
bx Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
ax) Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
kappa, Double
by) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Double, Double) -> String
pt (Double, Double)
b)

-- | Pieces of wire joined where one ends where the next starts, each chain as one path. A chain
-- starts at a piece that no other piece leads into.
joined :: [(Pt, Pt, String)] -> [String]
joined :: [((Double, Double), (Double, Double), String)] -> [String]
joined [] = []
joined ps :: [((Double, Double), (Double, Double), String)]
ps@(((Double, Double), (Double, Double), String)
p : [((Double, Double), (Double, Double), String)]
_) =
  let start :: ((Double, Double), (Double, Double), String)
start = ((Double, Double), (Double, Double), String)
-> Maybe ((Double, Double), (Double, Double), String)
-> ((Double, Double), (Double, Double), String)
forall a. a -> Maybe a -> a
fromMaybe ((Double, Double), (Double, Double), String)
p ((((Double, Double), (Double, Double), String) -> Bool)
-> [((Double, Double), (Double, Double), String)]
-> Maybe ((Double, Double), (Double, Double), String)
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Maybe a
List.find (\((Double, Double)
a, (Double, Double)
_, String
_) -> (Double, Double) -> (Int, Int)
forall {a} {a}. (RealFrac a, RealFrac a) => (a, a) -> (Int, Int)
key (Double, Double)
a (Int, Int) -> [(Int, Int)] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`notElem` [(Double, Double) -> (Int, Int)
forall {a} {a}. (RealFrac a, RealFrac a) => (a, a) -> (Int, Int)
key (Double, Double)
b | ((Double, Double)
_, (Double, Double)
b, String
_) <- [((Double, Double), (Double, Double), String)]
ps]) [((Double, Double), (Double, Double), String)]
ps)
      chain :: [((Double, Double), (Double, Double), String)]
chain = ((Double, Double), (Double, Double), String)
-> [((Double, Double), (Double, Double), String)]
-> [((Double, Double), (Double, Double), String)]
forall {a} {a} {a} {a} {c}.
(RealFrac a, RealFrac a, RealFrac a, RealFrac a, Eq c) =>
((a, a), (a, a), c)
-> [((a, a), (a, a), c)] -> [((a, a), (a, a), c)]
follow ((Double, Double), (Double, Double), String)
start (((Double, Double), (Double, Double), String)
-> [((Double, Double), (Double, Double), String)]
-> [((Double, Double), (Double, Double), String)]
forall a. Eq a => a -> [a] -> [a]
List.delete ((Double, Double), (Double, Double), String)
start [((Double, Double), (Double, Double), String)]
ps)
      rest :: [((Double, Double), (Double, Double), String)]
rest = (((Double, Double), (Double, Double), String)
 -> [((Double, Double), (Double, Double), String)]
 -> [((Double, Double), (Double, Double), String)])
-> [((Double, Double), (Double, Double), String)]
-> [((Double, Double), (Double, Double), String)]
-> [((Double, Double), (Double, Double), String)]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Double, Double), (Double, Double), String)
-> [((Double, Double), (Double, Double), String)]
-> [((Double, Double), (Double, Double), String)]
forall a. Eq a => a -> [a] -> [a]
List.delete [((Double, Double), (Double, Double), String)]
ps (((Double, Double), (Double, Double), String)
start ((Double, Double), (Double, Double), String)
-> [((Double, Double), (Double, Double), String)]
-> [((Double, Double), (Double, Double), String)]
forall a. a -> [a] -> [a]
: [((Double, Double), (Double, Double), String)]
chain)
      ((Double, Double)
a0, (Double, Double)
_, String
_) = ((Double, Double), (Double, Double), String)
start
  in (String
"M" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Double, Double) -> String
pt (Double, Double)
a0 String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat [String
d | ((Double, Double)
_, (Double, Double)
_, String
d) <- ((Double, Double), (Double, Double), String)
start ((Double, Double), (Double, Double), String)
-> [((Double, Double), (Double, Double), String)]
-> [((Double, Double), (Double, Double), String)]
forall a. a -> [a] -> [a]
: [((Double, Double), (Double, Double), String)]
chain]) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [((Double, Double), (Double, Double), String)] -> [String]
joined [((Double, Double), (Double, Double), String)]
rest
  where
    key :: (a, a) -> (Int, Int)
key (a
x, a
y) = (a -> Int
forall b. Integral b => a -> b
forall a b. (RealFrac a, Integral b) => a -> b
round (a
x a -> a -> a
forall a. Num a => a -> a -> a
* a
100), a -> Int
forall b. Integral b => a -> b
forall a b. (RealFrac a, Integral b) => a -> b
round (a
y a -> a -> a
forall a. Num a => a -> a -> a
* a
100)) :: (Int, Int)
    follow :: ((a, a), (a, a), c)
-> [((a, a), (a, a), c)] -> [((a, a), (a, a), c)]
follow ((a, a)
_, (a, a)
b, c
_) [((a, a), (a, a), c)]
qs = case (((a, a), (a, a), c) -> Bool)
-> [((a, a), (a, a), c)] -> Maybe ((a, a), (a, a), c)
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Maybe a
List.find (\((a, a)
a', (a, a)
_, c
_) -> (a, a) -> (Int, Int)
forall {a} {a}. (RealFrac a, RealFrac a) => (a, a) -> (Int, Int)
key (a, a)
a' (Int, Int) -> (Int, Int) -> Bool
forall a. Eq a => a -> a -> Bool
== (a, a) -> (Int, Int)
forall {a} {a}. (RealFrac a, RealFrac a) => (a, a) -> (Int, Int)
key (a, a)
b) [((a, a), (a, a), c)]
qs of
      Just ((a, a), (a, a), c)
next -> ((a, a), (a, a), c)
next ((a, a), (a, a), c)
-> [((a, a), (a, a), c)] -> [((a, a), (a, a), c)]
forall a. a -> [a] -> [a]
: ((a, a), (a, a), c)
-> [((a, a), (a, a), c)] -> [((a, a), (a, a), c)]
follow ((a, a), (a, a), c)
next (((a, a), (a, a), c)
-> [((a, a), (a, a), c)] -> [((a, a), (a, a), c)]
forall a. Eq a => a -> [a] -> [a]
List.delete ((a, a), (a, a), c)
next [((a, a), (a, a), c)]
qs)
      Maybe ((a, a), (a, a), c)
Nothing -> []

path :: String -> String
path :: String -> String
path String
d = String
"<path d=\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\"/>"

-- | One shape as SVG.
shape :: Shape -> String
shape :: Shape -> String
shape = \case
  Box a :: (Double, Double)
a@(Double
x0, Double
y0) b :: (Double, Double)
b@(Double
x1, Double
y1) String
s -> String -> Double -> (Double, Double) -> (Double, Double) -> String
rect String
"" Double
7 (Double, Double)
a (Double, Double)
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> (Double, Double) -> String -> String
text String
"n" ((Double
x0 Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
x1) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
2, (Double
y0 Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
y1) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
2) String
s
  Frame (Double, Double)
a (Double, Double)
b -> String -> Double -> (Double, Double) -> (Double, Double) -> String
rect String
" class=\"id\"" Double
4 (Double, Double)
a (Double, Double)
b
  Bracket (Double
x0, Double
y0) (Double
x1, Double
y1) Bool
down ->
    let tick :: Double
tick = if Bool
down then Double
4 else -Double
4
    in String
"<path class=\"br\" d=\"M"
         String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Double, Double) -> String
pt (Double
x0, Double
y0 Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
tick)
         String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"L"
         String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Double, Double) -> String
pt (Double
x0, Double
y0)
         String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"L"
         String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Double, Double) -> String
pt (Double
x1, Double
y1)
         String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"L"
         String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Double, Double) -> String
pt (Double
x1, Double
y1 Double -> Double -> Double
forall a. Num a => a -> a -> a
+ Double
tick)
         String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\"/>"
  Point (Double
x, Double
y) Bool
filled -> String
"<circle cx=\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Double -> String
num Double
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\" cy=\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Double -> String
num Double
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\" r=\"3\" class=\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Bool
filled then String
"f" else String
"h") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\"/>"
  Label (Double, Double)
p String
s -> String -> (Double, Double) -> String -> String
text String
"l" (Double, Double)
p String
s
  Boundary (Double, Double)
p String
s -> String -> (Double, Double) -> String -> String
text String
"b" (Double, Double)
p String
s
  Equals (Double, Double)
p -> String -> (Double, Double) -> String -> String
text String
"e" (Double, Double)
p String
"="
  -- wires are drawn by 'document', joined into as few paths as possible
  Piece{} -> String
""
  where
    rect :: String -> Double -> (Double, Double) -> (Double, Double) -> String
rect String
cls Double
r (Double
x0, Double
y0) (Double
x1, Double
y1) =
      String
"<rect"
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cls
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" x=\""
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ Double -> String
num Double
x0
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\" y=\""
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ Double -> String
num Double
y0
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\" width=\""
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ Double -> String
num (Double
x1 Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
x0)
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\" height=\""
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ Double -> String
num (Double
y1 Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
y0)
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\" rx=\""
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ Double -> String
num Double
r
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\"/>"
    text :: String -> (Double, Double) -> String -> String
text String
cls (Double
x, Double
y) String
s = String
"<text class=\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cls String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\" x=\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Double -> String
num Double
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\" y=\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Double -> String
num Double
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\">" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
Dot.htmlEscape String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"</text>"

-- | How far along its tangent a cubic curve's control point lies, as a fraction of the radius,
-- for the curve to be a quarter circle.
kappa :: Double
kappa :: Double
kappa = Double
0.5523

-- | The radius of a bend, and of the corners of a trace loop, so that a small loop is a cup and a
-- cap joined by straight wire.
bendRadius :: Double
bendRadius :: Double
bendRadius = Double
slot Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
2

-- | A path from the first of the given corners along the rest, each corner rounded with a quarter
-- circle of radius 'bendRadius', or less where the wire on either side of it is too short. A
-- stretch of wire between two corners is shared between them; one at either end belongs to its
-- corner alone.
rounded :: NonEmpty Pt -> String
rounded :: NonEmpty (Double, Double) -> String
rounded NonEmpty (Double, Double)
ne = ((Int, (Double, Double), ((Double, Double), (Double, Double)))
 -> String)
-> [(Int, (Double, Double), ((Double, Double), (Double, Double)))]
-> String
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap (Int, (Double, Double), ((Double, Double), (Double, Double)))
-> String
corner ([Int]
-> [(Double, Double)]
-> [((Double, Double), (Double, Double))]
-> [(Int, (Double, Double), ((Double, Double), (Double, Double)))]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Int
0 :: Int ..] [(Double, Double)]
ps (Int -> [(Double, Double)] -> [(Double, Double)]
forall a. Int -> [a] -> [a]
drop Int
1 [(Double, Double)]
ps [(Double, Double)]
-> [(Double, Double)] -> [((Double, Double), (Double, Double))]
forall a b. [a] -> [b] -> [(a, b)]
`zip` Int -> [(Double, Double)] -> [(Double, Double)]
forall a. Int -> [a] -> [a]
drop Int
2 [(Double, Double)]
ps)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"L" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Double, Double) -> String
pt (NonEmpty (Double, Double) -> (Double, Double)
forall a. NonEmpty a -> a
NE.last NonEmpty (Double, Double)
ne)
  where
    ps :: [(Double, Double)]
ps = NonEmpty (Double, Double) -> [(Double, Double)]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty (Double, Double)
ne
    lastCorner :: Int
lastCorner = [(Double, Double)] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [(Double, Double)]
ps Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
3
    corner :: (Int, (Double, Double), ((Double, Double), (Double, Double)))
-> String
corner (Int
i, (Double, Double)
prev, ((Double, Double)
c, (Double, Double)
next)) =
      let room :: Bool -> (Double, Double) -> Double
room Bool
end (Double, Double)
q = if Bool
end then (Double, Double) -> (Double, Double) -> Double
forall {a}. Floating a => (a, a) -> (a, a) -> a
dist (Double, Double)
c (Double, Double)
q else (Double, Double) -> (Double, Double) -> Double
forall {a}. Floating a => (a, a) -> (a, a) -> a
dist (Double, Double)
c (Double, Double)
q Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
2
          rr :: Double
rr = [Double] -> Double
forall a. Ord a => [a] -> a
forall (t :: Type -> Type) a. (Foldable t, Ord a) => t a -> a
minimum [Double
bendRadius, Bool -> (Double, Double) -> Double
room (Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0) (Double, Double)
prev, Bool -> (Double, Double) -> Double
room (Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
lastCorner) (Double, Double)
next]
          a :: (Double, Double)
a = (Double, Double) -> (Double, Double) -> Double -> (Double, Double)
forall {b}. Floating b => (b, b) -> (b, b) -> b -> (b, b)
towards (Double, Double)
c (Double, Double)
prev Double
rr
          b :: (Double, Double)
b = (Double, Double) -> (Double, Double) -> Double -> (Double, Double)
forall {b}. Floating b => (b, b) -> (b, b) -> b -> (b, b)
towards (Double, Double)
c (Double, Double)
next Double
rr
      in String
"L" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Double, Double) -> String
pt (Double, Double)
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"C" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Double, Double) -> String
pt ((Double, Double) -> (Double, Double) -> (Double, Double)
between (Double, Double)
a (Double, Double)
c) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Double, Double) -> String
pt ((Double, Double) -> (Double, Double) -> (Double, Double)
between (Double, Double)
b (Double, Double)
c) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Double, Double) -> String
pt (Double, Double)
b
    dist :: (a, a) -> (a, a) -> a
dist (a
x0, a
y0) (a
x1, a
y1) = a -> a
forall a. Floating a => a -> a
sqrt ((a
x1 a -> a -> a
forall a. Num a => a -> a -> a
- a
x0) a -> Int -> a
forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
2 :: Int) a -> a -> a
forall a. Num a => a -> a -> a
+ (a
y1 a -> a -> a
forall a. Num a => a -> a -> a
- a
y0) a -> Int -> a
forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
2 :: Int))
    towards :: (b, b) -> (b, b) -> b -> (b, b)
towards c :: (b, b)
c@(b
cx, b
cy) q :: (b, b)
q@(b
x, b
y) b
d = let t :: b
t = b
d b -> b -> b
forall a. Fractional a => a -> a -> a
/ (b, b) -> (b, b) -> b
forall {a}. Floating a => (a, a) -> (a, a) -> a
dist (b, b)
c (b, b)
q in (b
cx b -> b -> b
forall a. Num a => a -> a -> a
+ (b
x b -> b -> b
forall a. Num a => a -> a -> a
- b
cx) b -> b -> b
forall a. Num a => a -> a -> a
* b
t, b
cy b -> b -> b
forall a. Num a => a -> a -> a
+ (b
y b -> b -> b
forall a. Num a => a -> a -> a
- b
cy) b -> b -> b
forall a. Num a => a -> a -> a
* b
t)
    -- the control point of a quarter circle, from its end towards the corner
    between :: (Double, Double) -> (Double, Double) -> (Double, Double)
between (Double
x, Double
y) (Double
cx, Double
cy) = (Double
x Double -> Double -> Double
forall a. Num a => a -> a -> a
+ (Double
cx Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
x) Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
kappa, Double
y Double -> Double -> Double
forall a. Num a => a -> a -> a
+ (Double
cy Double -> Double -> Double
forall a. Num a => a -> a -> a
- Double
y) Double -> Double -> Double
forall a. Num a => a -> a -> a
* Double
kappa)

pt :: Pt -> String
pt :: (Double, Double) -> String
pt (Double
x, Double
y) = Double -> String
num Double
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Double -> String
num Double
y

num :: Double -> String
num :: Double -> String
num Double
x = Maybe Int -> Double -> String -> String
forall a. RealFloat a => Maybe Int -> a -> String -> String
showFFloat (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1) Double
x String
""