{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE UnicodeSyntax #-}

{-# OPTIONS_GHC -Wno-incomplete-patterns -Wno-overlapping-patterns #-}

module Control.Category.Linear (
  -- Interface
  type P, unit, split, merge, pattern (:::),
  encode, decode, reduce, (!:),
  -- Helpers for cartesian categories
  ignore, copy, discard
) where


import Data.Kind (Type)

import Prelude hiding ((.),id,curry,LT,GT,EQ)
import Control.Category.Constrained
import Control.Category.FreeCartesian as Cartesian
import Unsafe.Coerce
import qualified Control.Category.FreeSMC as SMC



pattern (:::) :: forall con (k :: Type -> Type -> Type) r a b.
                   (Obj k r, Obj k a, Obj k b, Monoidal k, con (), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k) =>
                   P k r a ⊸ P k r b ⊸ P k r (a, b)
pattern x $b::: :: forall (con :: * -> Constraint) (k :: * -> * -> *) r a b.
(Obj k r, Obj k a, Obj k b, Monoidal k, con (),
 forall α β. (con α, con β) => con (α, β), con ~ Obj k) =>
P k r a -> P k r b -> P k r (a, b)
$m::: :: forall {r} {con :: * -> Constraint} {k :: * -> * -> *} {r} {a} {b}.
(Obj k r, Obj k a, Obj k b, Monoidal k, con (),
 forall α β. (con α, con β) => con (α, β), con ~ Obj k) =>
P k r (a, b) -> (P k r a -> P k r b -> r) -> (Void# -> r) -> r
::: y <- (split @con -> (x,y))
  where P k r a
x ::: P k r b
y = forall (con :: * -> Constraint) a b r (k :: * -> * -> *).
(O3 k r a b, Monoidal k, con (),
 forall α β. (con α, con β) => con (α, β), con ~ Obj k) =>
(P k r a, P k r b) %1 -> P k r (a ⊗ b)
merge @con (P k r a
x,P k r b
y)

infixr ::: -- GHC does not always see this change. rm -r dist/dante. T_T (ghc 8.8.4)


type P :: (Type -> Type -> Type) -> Type -> Type -> Type

unit     :: {-<-}forall k con r. (Obj k r, Monoidal k, con (), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k)         => {->-}P k r ()
split    :: {-<-}forall con a b r k. (O3 k r a b, Monoidal k, con (), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k) => {->-}P k r (a ⊗ b) ⊸ (P k r a, P k r b)
merge    :: {-<-}forall  con a b r k. (O3 k r a b, Monoidal k, con(), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k) => {->-}(P k r a , P k r b) ⊸ P k r (a ⊗ b)
encode   :: {-<-} O3 k r a b => {->-}  (a `k` b) -> (P k r a ⊸ P k r b)
decode   :: {-<-} forall a b k con. (con (), con ~ Obj k, Monoidal k, con a, con b, (forall α β. (con α, con β) => con (α,β))) => {->-} (forall r. {-<-}Obj k r =>{->-} P k r a ⊸ P k r b) -> (a `k` b)

(!:) :: forall  con a b r k. (O3 k r a b, Monoidal k, con(), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k)
       => P k r a ⊸ P k r b ⊸ P k r (a,b)
P k r a
x !: :: forall (con :: * -> Constraint) a b r (k :: * -> * -> *).
(O3 k r a b, Monoidal k, con (),
 forall α β. (con α, con β) => con (α, β), con ~ Obj k) =>
P k r a %1 -> P k r b %1 -> P k r (a, b)
!: P k r b
y = (P k r a, P k r b) %1 -> P k r (a ⊗ b)
forall (con :: * -> Constraint) a b r (k :: * -> * -> *).
(O3 k r a b, Monoidal k, con (),
 forall α β. (con α, con β) => con (α, β), con ~ Obj k) =>
(P k r a, P k r b) %1 -> P k r (a ⊗ b)
merge (P k r a
x,P k r b
y)


data P k r a     where
  Y :: FreeCartesian k {-<-} (Obj k) {->-} r a -> P k r a
fromP :: P k r a -> FreeCartesian k {-<-} (Obj k) {->-} r a
fromP :: forall (k :: * -> * -> *) r a.
P k r a -> FreeCartesian k (Obj k) r a
fromP (Y FreeCartesian k (Obj k) r a
f) = FreeCartesian k (Obj k) r a
f

  
encode :: forall (k :: * -> * -> *) r a b.
O3 k r a b =>
k a b -> P k r a %1 -> P k r b
encode k a b
φ (Y FreeCartesian k (Obj k) r a
f)    = FreeCartesian k (Obj k) r b -> P k r b
forall (k :: * -> * -> *) r a.
FreeCartesian k (Obj k) r a -> P k r a
Y (k a b -> FreeCartesian k (Obj k) a b
forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(con a, con b) =>
k a b -> FreeCartesian k con a b
Embed k a b
φ FreeCartesian k (Obj k) a b
-> FreeCartesian k (Obj k) r a -> FreeCartesian k (Obj k) r b
forall (k :: * -> * -> *) a b c.
(Category k, Obj k a, Obj k b, Obj k c) =>
k b c -> k a b -> k a c
∘ FreeCartesian k (Obj k) r a
f) -- put φ after f.
unit :: forall (k :: * -> * -> *) (con :: * -> Constraint) r.
(Obj k r, Monoidal k, con (),
 forall α β. (con α, con β) => con (α, β), con ~ Obj k) =>
P k r ()
unit              = FreeCartesian k (Obj k) r () -> P k r ()
forall (k :: * -> * -> *) r a.
FreeCartesian k (Obj k) r a -> P k r a
Y FreeCartesian k (Obj k) r ()
forall (k :: * -> * -> *) a. (Cartesian k, Obj k a) => k a ()
dis
split :: forall (con :: * -> Constraint) a b r (k :: * -> * -> *).
(O3 k r a b, Monoidal k, con (),
 forall α β. (con α, con β) => con (α, β), con ~ Obj k) =>
P k r (a ⊗ b) %1 -> (P k r a, P k r b)
split (Y FreeCartesian k (Obj k) r (a ⊗ b)
f)       = (FreeCartesian k (Obj k) r a -> P k r a
forall (k :: * -> * -> *) r a.
FreeCartesian k (Obj k) r a -> P k r a
Y (FreeCartesian k con (a ⊗ b) a
forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) a
exl FreeCartesian k con (a ⊗ b) a
-> FreeCartesian k con r (a ⊗ b) -> FreeCartesian k con r a
forall (k :: * -> * -> *) a b c.
(Category k, Obj k a, Obj k b, Obj k c) =>
k b c -> k a b -> k a c
∘ FreeCartesian k con r (a ⊗ b)
FreeCartesian k (Obj k) r (a ⊗ b)
f), FreeCartesian k (Obj k) r b -> P k r b
forall (k :: * -> * -> *) r a.
FreeCartesian k (Obj k) r a -> P k r a
Y (FreeCartesian k con (a ⊗ b) b
forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) b
exr FreeCartesian k con (a ⊗ b) b
-> FreeCartesian k con r (a ⊗ b) -> FreeCartesian k con r b
forall (k :: * -> * -> *) a b c.
(Category k, Obj k a, Obj k b, Obj k c) =>
k b c -> k a b -> k a c
∘ FreeCartesian k con r (a ⊗ b)
FreeCartesian k (Obj k) r (a ⊗ b)
f)) 
merge :: forall (con :: * -> Constraint) a b r (k :: * -> * -> *).
(O3 k r a b, Monoidal k, con (),
 forall α β. (con α, con β) => con (α, β), con ~ Obj k) =>
(P k r a, P k r b) %1 -> P k r (a ⊗ b)
merge (Y FreeCartesian k (Obj k) r a
f, Y FreeCartesian k (Obj k) r b
g)  = FreeCartesian k (Obj k) r (a ⊗ b) -> P k r (a ⊗ b)
forall (k :: * -> * -> *) r a.
FreeCartesian k (Obj k) r a -> P k r a
Y (FreeCartesian k con r a
FreeCartesian k (Obj k) r a
f FreeCartesian k con r a
-> FreeCartesian k con r b -> FreeCartesian k con r (a ⊗ b)
forall (k :: * -> * -> *) a b c.
(Cartesian k, Obj k a, Obj k b, Obj k c) =>
k a b -> k a c -> k a (b ⊗ c)
▵ FreeCartesian k con r b
FreeCartesian k (Obj k) r b
g)


decode :: forall a b (k :: * -> * -> *) (con :: * -> Constraint).
(con (), con ~ Obj k, Monoidal k, con a, con b,
 forall α β. (con α, con β) => con (α, β)) =>
(forall r. Obj k r => P k r a %1 -> P k r b) -> k a b
decode forall r. Obj k r => P k r a %1 -> P k r b
f          = Cat k (Obj k) a b -> k a b
forall (k :: * -> * -> *) a b (con :: * -> Constraint).
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con ~ Obj k, Monoidal k, Obj k a, Obj k b) =>
Cat k (Obj k) a b -> k a b
SMC.evalM (Cat k con a b -> FreeSMC k con a b
forall (cat :: * -> * -> *) (con :: * -> Constraint) a b.
(Obj cat ~ con, ProdObj con,
 forall α β. (con α, con β) => con (α, β), con (), con a, con b) =>
Cat cat con a b -> FreeSMC cat con a b
reduce ((forall r. Obj k r => P k r a %1 -> P k r b)
-> FreeCartesian k (Obj k) a b
forall (k :: * -> * -> *) a b.
(Obj k a, Obj k b) =>
(forall r. Obj k r => P k r a %1 -> P k r b)
-> FreeCartesian k (Obj k) a b
extract forall r. Obj k r => P k r a %1 -> P k r b
f))
extract           :: {-<-} (Obj k a, Obj k b) => {->-} (forall r. {-<-} Obj k r => {->-} P k r a ⊸ P k r b) -> FreeCartesian k {-<-} (Obj k) {->-} a b
extract :: forall (k :: * -> * -> *) a b.
(Obj k a, Obj k b) =>
(forall r. Obj k r => P k r a %1 -> P k r b)
-> FreeCartesian k (Obj k) a b
extract forall r. Obj k r => P k r a %1 -> P k r b
f         = P k a b -> FreeCartesian k (Obj k) a b
forall (k :: * -> * -> *) r a.
P k r a -> FreeCartesian k (Obj k) r a
fromP (P k a a %1 -> P k a b
forall r. Obj k r => P k r a %1 -> P k r b
f (FreeCartesian k (Obj k) a a -> P k a a
forall (k :: * -> * -> *) r a.
FreeCartesian k (Obj k) r a -> P k r a
Y FreeCartesian k (Obj k) a a
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id))


---------------------------------------------------------------------
-- If the underlying category is cartesian, we have additionally:


ignore      :: (Monoidal k, {-<-} O3 k r a (), (forall α β. (con α, con β) => con (α,β)), con ~ Obj k {->-}) => P k r () ⊸ P k r a ⊸ P k r a
ignore :: forall (k :: * -> * -> *) r a (con :: * -> Constraint).
(Monoidal k, O3 k r a (), forall α β. (con α, con β) => con (α, β),
 con ~ Obj k) =>
P k r () %1 -> P k r a %1 -> P k r a
ignore P k r ()
f P k r a
g  = k (a ⊗ ()) a -> P k r (a ⊗ ()) %1 -> P k r a
forall (k :: * -> * -> *) r a b.
O3 k r a b =>
k a b -> P k r a %1 -> P k r b
encode k (a ⊗ ()) a
forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k (a ⊗ ()) a
unitor' ((P k r a, P k r ()) %1 -> P k r (a ⊗ ())
forall (con :: * -> Constraint) a b r (k :: * -> * -> *).
(O3 k r a b, Monoidal k, con (),
 forall α β. (con α, con β) => con (α, β), con ~ Obj k) =>
(P k r a, P k r b) %1 -> P k r (a ⊗ b)
merge (P k r a
g,P k r ()
f))
  
copy  :: (Cartesian k {-<-} , O2 k r a, (forall α β. (con α, con β) => con (α,β)), con ~ Obj k {->-} ) => P k r a ⊸ P k r (a ⊗ a)
copy :: forall (k :: * -> * -> *) r a (con :: * -> Constraint).
(Cartesian k, O2 k r a, forall α β. (con α, con β) => con (α, β),
 con ~ Obj k) =>
P k r a %1 -> P k r (a ⊗ a)
copy  = k a (a ⊗ a) -> P k r a %1 -> P k r (a ⊗ a)
forall (k :: * -> * -> *) r a b.
O3 k r a b =>
k a b -> P k r a %1 -> P k r b
encode k a (a ⊗ a)
forall (k :: * -> * -> *) a.
(Cartesian k, Obj k a, Obj k (a ⊗ a)) =>
k a (a ⊗ a)
dup
discard  :: (Cartesian k {-<-} , O2 k r a, (forall α β. (con α, con β) => con (α,β)), con ~ Obj k, con () {->-} ) => P k r a ⊸ P k r ()
discard :: forall (k :: * -> * -> *) r a (con :: * -> Constraint).
(Cartesian k, O2 k r a, forall α β. (con α, con β) => con (α, β),
 con ~ Obj k, con ()) =>
P k r a %1 -> P k r ()
discard  = k a () -> P k r a %1 -> P k r ()
forall (k :: * -> * -> *) r a b.
O3 k r a b =>
k a b -> P k r a %1 -> P k r b
encode k a ()
forall (k :: * -> * -> *) a. (Cartesian k, Obj k a) => k a ()
dis






type FreeSMC = SMC.Cat

-- haskell-src-exts does not like the ' before constructors. It does not honour extensions either.
type Null = '[]
type Cons x xs = x ': xs

type family Prod (xs :: [Type])  where
  Prod Null = ()
  Prod (Cons x ys) = x ⊗ Prod ys


data Merge k {-<-}con{->-} a xs where
  (:+)   :: {-<-}(con x, con (Prod xs)) => {->-}FreeCartesian k {-<-}con{->-} a x -> Merge k {-<-}con{->-} a xs
         -> Merge k {-<-}con{->-}  a (Cons x xs)
  Nil    :: Merge k {-<-}con{->-} a Null

infixr :+


-- | expose does two things:
-- 1. push abstract morphisms (E, X) into the already processed part
-- 2. turn f ▵ g into a Merge

expose  ::  {-<-}(ProdObj con, forall α β. (con α, con β) => con (α,β), con (), con a, con b) => {->-}Cat cat {-<-}con{->-} a b ->
            (  forall x. {-<-}con (Prod x) =>{->-} FreeSMC cat {-<-}con{->-} (Prod x) b ->
               Merge cat {-<-}con{->-} a x -> k) -> k
expose :: forall (con :: * -> Constraint) a b (cat :: * -> * -> *) k.
(ProdObj con, forall α β. (con α, con β) => con (α, β), con (),
 con a, con b) =>
Cat cat con a b
-> (forall (x :: [*]).
    con (Prod x) =>
    FreeSMC cat con (Prod x) b -> Merge cat con a x -> k)
-> k
expose (FreeCartesian cat con a b
f1 :▵: FreeCartesian cat con a c
f2) forall (x :: [*]).
con (Prod x) =>
FreeSMC cat con (Prod x) b -> Merge cat con a x -> k
k      =  FreeCartesian cat con a b
-> (forall (x :: [*]).
    con (Prod x) =>
    FreeSMC cat con (Prod x) b -> Merge cat con a x -> k)
-> k
forall (con :: * -> Constraint) a b (cat :: * -> * -> *) k.
(ProdObj con, forall α β. (con α, con β) => con (α, β), con (),
 con a, con b) =>
Cat cat con a b
-> (forall (x :: [*]).
    con (Prod x) =>
    FreeSMC cat con (Prod x) b -> Merge cat con a x -> k)
-> k
expose FreeCartesian cat con a b
f1 ((forall (x :: [*]).
  con (Prod x) =>
  FreeSMC cat con (Prod x) b -> Merge cat con a x -> k)
 -> k)
-> (forall (x :: [*]).
    con (Prod x) =>
    FreeSMC cat con (Prod x) b -> Merge cat con a x -> k)
-> k
forall a b. (a -> b) -> a -> b
$ \FreeSMC cat con (Prod x) b
g1 Merge cat con a x
fs1 ->
                             FreeCartesian cat con a c
-> (forall (x :: [*]).
    con (Prod x) =>
    FreeSMC cat con (Prod x) c -> Merge cat con a x -> k)
-> k
forall (con :: * -> Constraint) a b (cat :: * -> * -> *) k.
(ProdObj con, forall α β. (con α, con β) => con (α, β), con (),
 con a, con b) =>
Cat cat con a b
-> (forall (x :: [*]).
    con (Prod x) =>
    FreeSMC cat con (Prod x) b -> Merge cat con a x -> k)
-> k
expose FreeCartesian cat con a c
f2 ((forall (x :: [*]).
  con (Prod x) =>
  FreeSMC cat con (Prod x) c -> Merge cat con a x -> k)
 -> k)
-> (forall (x :: [*]).
    con (Prod x) =>
    FreeSMC cat con (Prod x) c -> Merge cat con a x -> k)
-> k
forall a b. (a -> b) -> a -> b
$ \FreeSMC cat con (Prod x) c
g2 Merge cat con a x
fs2 ->
                             Merge cat con a x
-> Merge cat con a x
-> (forall (zs :: [*]).
    con (Prod zs) =>
    FreeSMC cat con (Prod zs) (Prod x ⊗ Prod x)
    -> Merge cat con a zs -> k)
-> k
forall (con :: * -> Constraint) a (xs :: [*]) (ys :: [*])
       (cat :: * -> * -> *) k.
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con a, con (Prod xs), con (Prod ys)) =>
Merge cat con a xs
-> Merge cat con a ys
-> (forall (zs :: [*]).
    con (Prod zs) =>
    FreeSMC cat con (Prod zs) (Prod xs ⊗ Prod ys)
    -> Merge cat con a zs -> k)
-> k
appendSorted Merge cat con a x
fs1 Merge cat con a x
fs2 ((forall (zs :: [*]).
  con (Prod zs) =>
  FreeSMC cat con (Prod zs) (Prod x ⊗ Prod x)
  -> Merge cat con a zs -> k)
 -> k)
-> (forall (zs :: [*]).
    con (Prod zs) =>
    FreeSMC cat con (Prod zs) (Prod x ⊗ Prod x)
    -> Merge cat con a zs -> k)
-> k
forall a b. (a -> b) -> a -> b
$ \FreeSMC cat con (Prod zs) (Prod x ⊗ Prod x)
g Merge cat con a zs
fs ->
                             FreeSMC cat con (Prod zs) b -> Merge cat con a zs -> k
forall (x :: [*]).
con (Prod x) =>
FreeSMC cat con (Prod x) b -> Merge cat con a x -> k
k ((FreeSMC cat con (Prod x) b
g1 FreeSMC cat con (Prod x) b
-> FreeSMC cat con (Prod x) c
-> Cat cat con (Prod x ⊗ Prod x) (b, c)
forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× FreeSMC cat con (Prod x) c
g2) Cat cat con (Prod x ⊗ Prod x) (b, c)
-> FreeSMC cat con (Prod zs) (Prod x ⊗ Prod x)
-> Cat cat con (Prod zs) (b, c)
forall (k :: * -> * -> *) a b c.
(Category k, Obj k a, Obj k b, Obj k c) =>
k b c -> k a b -> k a c
∘ FreeSMC cat con (Prod zs) (Prod x ⊗ Prod x)
g) Merge cat con a zs
fs
expose (Embed cat b b
ϕ :<: Cat cat con a b
f) forall (x :: [*]).
con (Prod x) =>
FreeSMC cat con (Prod x) b -> Merge cat con a x -> k
k  =  Cat cat con a b
-> (forall (x :: [*]).
    con (Prod x) =>
    FreeSMC cat con (Prod x) b -> Merge cat con a x -> k)
-> k
forall (con :: * -> Constraint) a b (cat :: * -> * -> *) k.
(ProdObj con, forall α β. (con α, con β) => con (α, β), con (),
 con a, con b) =>
Cat cat con a b
-> (forall (x :: [*]).
    con (Prod x) =>
    FreeSMC cat con (Prod x) b -> Merge cat con a x -> k)
-> k
expose Cat cat con a b
f ((forall (x :: [*]).
  con (Prod x) =>
  FreeSMC cat con (Prod x) b -> Merge cat con a x -> k)
 -> k)
-> (forall (x :: [*]).
    con (Prod x) =>
    FreeSMC cat con (Prod x) b -> Merge cat con a x -> k)
-> k
forall a b. (a -> b) -> a -> b
$ \FreeSMC cat con (Prod x) b
g Merge cat con a x
fs ->
                             FreeSMC cat con (Prod x) b -> Merge cat con a x -> k
forall (x :: [*]).
con (Prod x) =>
FreeSMC cat con (Prod x) b -> Merge cat con a x -> k
k (cat b b -> Cat cat con b b
forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(con a, con b) =>
k a b -> Cat k con a b
SMC.Embed cat b b
ϕ Cat cat con b b
-> FreeSMC cat con (Prod x) b -> FreeSMC cat con (Prod x) b
forall (k :: * -> * -> *) a b c.
(Category k, Obj k a, Obj k b, Obj k c) =>
k b c -> k a b -> k a c
∘ FreeSMC cat con (Prod x) b
g) Merge cat con a x
fs
expose (FreeCartesian cat con b b
E :<: Cat cat con a b
_) forall (x :: [*]).
con (Prod x) =>
FreeSMC cat con (Prod x) b -> Merge cat con a x -> k
k        = FreeSMC cat con (Prod Null) b -> Merge cat con a Null -> k
forall (x :: [*]).
con (Prod x) =>
FreeSMC cat con (Prod x) b -> Merge cat con a x -> k
k FreeSMC cat con (Prod Null) b
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id Merge cat con a Null
forall (k :: * -> * -> *) (con :: * -> Constraint) a.
Merge k con a Null
Nil
expose FreeCartesian cat con a b
x forall (x :: [*]).
con (Prod x) =>
FreeSMC cat con (Prod x) b -> Merge cat con a x -> k
k                = FreeSMC cat con (Prod (Cons b Null)) b
-> Merge cat con a (Cons b Null) -> k
forall (x :: [*]).
con (Prod x) =>
FreeSMC cat con (Prod x) b -> Merge cat con a x -> k
k FreeSMC cat con (Prod (Cons b Null)) b
forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k (a ⊗ ()) a
unitor' (FreeCartesian cat con a b
x FreeCartesian cat con a b
-> Merge cat con a Null -> Merge cat con a (Cons b Null)
forall (con :: * -> Constraint) b (xs :: [*]) (k :: * -> * -> *) a.
(con b, con (Prod xs)) =>
FreeCartesian k con a b
-> Merge k con a xs -> Merge k con a (Cons b xs)
:+ Merge cat con a Null
forall (k :: * -> * -> *) (con :: * -> Constraint) a.
Merge k con a Null
Nil)

-- | Merge L/R pair

reduceStep  ::  {-<-}(ProdObj con, forall α β. (con α, con β) => con (α,β), con (), con a, con (Prod xs)) =>{->-} Merge cat {-<-}con{->-} a xs ->
                (  forall zs. {-<-}con (Prod zs) => {->-}FreeSMC cat {-<-}con{->-} (Prod zs) (Prod xs)  ->
                  Merge cat {-<-}con{->-} a zs -> k) -> k
-- There exists at least one pair of the form L :<: f and R :<: f if
-- already maximally exposed. So we do not handle the base cases here.

-- If R :<: f is the first in the order, then L :<: f also exists;
-- and it should be first, so the case (R :<: f) :+ (L :<: g) must be rejected.
reduceStep :: forall (con :: * -> Constraint) a (xs :: [*]) (cat :: * -> * -> *)
       k.
(ProdObj con, forall α β. (con α, con β) => con (α, β), con (),
 con a, con (Prod xs)) =>
Merge cat con a xs
-> (forall (zs :: [*]).
    con (Prod zs) =>
    FreeSMC cat con (Prod zs) (Prod xs) -> Merge cat con a zs -> k)
-> k
reduceStep ((FreeCartesian cat con b x
P1 :<: Cat cat con a b
f₁) :+ (FreeCartesian cat con b x
P2 :<: Cat cat con a b
f₂) :+ Merge cat con a xs
rest) forall (zs :: [*]).
con (Prod zs) =>
FreeSMC cat con (Prod zs) (Prod xs) -> Merge cat con a zs -> k
k
  | Order b b
EQ <- Cat cat con a b -> Cat cat con a b -> Order b b
forall (con :: * -> Constraint) a b c (cat :: * -> * -> *).
(con a, con b, con c) =>
Cat cat con a b -> Cat cat con a c -> Order b c
compareMorphisms Cat cat con a b
f₁ Cat cat con a b
f₂ =
  Cat cat con a b
-> (forall (x :: [*]).
    con (Prod x) =>
    FreeSMC cat con (Prod x) b -> Merge cat con a x -> k)
-> k
forall (con :: * -> Constraint) a b (cat :: * -> * -> *) k.
(ProdObj con, forall α β. (con α, con β) => con (α, β), con (),
 con a, con b) =>
Cat cat con a b
-> (forall (x :: [*]).
    con (Prod x) =>
    FreeSMC cat con (Prod x) b -> Merge cat con a x -> k)
-> k
expose Cat cat con a b
f₁               ((forall (x :: [*]).
  con (Prod x) =>
  FreeSMC cat con (Prod x) b -> Merge cat con a x -> k)
 -> k)
-> (forall (x :: [*]).
    con (Prod x) =>
    FreeSMC cat con (Prod x) b -> Merge cat con a x -> k)
-> k
forall a b. (a -> b) -> a -> b
$ \FreeSMC cat con (Prod x) b
g Merge cat con a x
f' -> -- expose any merge
  Merge cat con a x
-> Merge cat con a xs
-> (forall (zs :: [*]).
    con (Prod zs) =>
    FreeSMC cat con (Prod zs) (Prod x ⊗ Prod xs)
    -> Merge cat con a zs -> k)
-> k
forall (con :: * -> Constraint) a (xs :: [*]) (ys :: [*])
       (cat :: * -> * -> *) k.
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con a, con (Prod xs), con (Prod ys)) =>
Merge cat con a xs
-> Merge cat con a ys
-> (forall (zs :: [*]).
    con (Prod zs) =>
    FreeSMC cat con (Prod zs) (Prod xs ⊗ Prod ys)
    -> Merge cat con a zs -> k)
-> k
appendSorted Merge cat con a x
f' Merge cat con a xs
rest    ((forall (zs :: [*]).
  con (Prod zs) =>
  FreeSMC cat con (Prod zs) (Prod x ⊗ Prod xs)
  -> Merge cat con a zs -> k)
 -> k)
-> (forall (zs :: [*]).
    con (Prod zs) =>
    FreeSMC cat con (Prod zs) (Prod x ⊗ Prod xs)
    -> Merge cat con a zs -> k)
-> k
forall a b. (a -> b) -> a -> b
$ \FreeSMC cat con (Prod zs) (Prod x ⊗ Prod xs)
g' Merge cat con a zs
rest' -> -- insert the exposed stuff in a sorted way
  FreeSMC cat con (Prod zs) (Prod xs) -> Merge cat con a zs -> k
forall (zs :: [*]).
con (Prod zs) =>
FreeSMC cat con (Prod zs) (Prod xs) -> Merge cat con a zs -> k
k (Cat cat con ((x, b) ⊗ Prod xs) (x ⊗ (b ⊗ Prod xs))
forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
assoc Cat cat con ((x, b) ⊗ Prod xs) (x ⊗ (b ⊗ Prod xs))
-> Cat cat con (Prod x ⊗ Prod xs) ((x, b) ⊗ Prod xs)
-> Cat cat con (Prod x ⊗ Prod xs) (x ⊗ (b ⊗ Prod xs))
forall (k :: * -> * -> *) a b c.
(Category k, Obj k a, Obj k b, Obj k c) =>
k b c -> k a b -> k a c
∘ (FreeSMC cat con (Prod x) b
g FreeSMC cat con (Prod x) b
-> Cat cat con (Prod xs) (Prod xs)
-> Cat cat con (Prod x ⊗ Prod xs) (b ⊗ Prod xs)
forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× Cat cat con (Prod xs) (Prod xs)
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id) Cat cat con (Prod x ⊗ Prod xs) (x ⊗ (b ⊗ Prod xs))
-> FreeSMC cat con (Prod zs) (Prod x ⊗ Prod xs)
-> Cat cat con (Prod zs) (x ⊗ (b ⊗ Prod xs))
forall (k :: * -> * -> *) a b c.
(Category k, Obj k a, Obj k b, Obj k c) =>
k b c -> k a b -> k a c
∘ FreeSMC cat con (Prod zs) (Prod x ⊗ Prod xs)
g') Merge cat con a zs
rest'
reduceStep (FreeCartesian cat con a x
f :+ Merge cat con a xs
rest) forall (zs :: [*]).
con (Prod zs) =>
FreeSMC cat con (Prod zs) (Prod xs) -> Merge cat con a zs -> k
k =
  Merge cat con a xs
-> (forall (zs :: [*]).
    con (Prod zs) =>
    FreeSMC cat con (Prod zs) (Prod xs) -> Merge cat con a zs -> k)
-> k
forall (con :: * -> Constraint) a (xs :: [*]) (cat :: * -> * -> *)
       k.
(ProdObj con, forall α β. (con α, con β) => con (α, β), con (),
 con a, con (Prod xs)) =>
Merge cat con a xs
-> (forall (zs :: [*]).
    con (Prod zs) =>
    FreeSMC cat con (Prod zs) (Prod xs) -> Merge cat con a zs -> k)
-> k
reduceStep Merge cat con a xs
rest                    ((forall (zs :: [*]).
  con (Prod zs) =>
  FreeSMC cat con (Prod zs) (Prod xs) -> Merge cat con a zs -> k)
 -> k)
-> (forall (zs :: [*]).
    con (Prod zs) =>
    FreeSMC cat con (Prod zs) (Prod xs) -> Merge cat con a zs -> k)
-> k
forall a b. (a -> b) -> a -> b
$ \FreeSMC cat con (Prod zs) (Prod xs)
g Merge cat con a zs
rest' ->
  Merge cat con a (Cons x Null)
-> Merge cat con a zs
-> (forall (zs :: [*]).
    con (Prod zs) =>
    FreeSMC cat con (Prod zs) (Prod (Cons x Null) ⊗ Prod zs)
    -> Merge cat con a zs -> k)
-> k
forall (con :: * -> Constraint) a (xs :: [*]) (ys :: [*])
       (cat :: * -> * -> *) k.
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con a, con (Prod xs), con (Prod ys)) =>
Merge cat con a xs
-> Merge cat con a ys
-> (forall (zs :: [*]).
    con (Prod zs) =>
    FreeSMC cat con (Prod zs) (Prod xs ⊗ Prod ys)
    -> Merge cat con a zs -> k)
-> k
appendSorted (FreeCartesian cat con a x
f FreeCartesian cat con a x
-> Merge cat con a Null -> Merge cat con a (Cons x Null)
forall (con :: * -> Constraint) b (xs :: [*]) (k :: * -> * -> *) a.
(con b, con (Prod xs)) =>
FreeCartesian k con a b
-> Merge k con a xs -> Merge k con a (Cons b xs)
:+ Merge cat con a Null
forall (k :: * -> * -> *) (con :: * -> Constraint) a.
Merge k con a Null
Nil) Merge cat con a zs
rest'  ((forall (zs :: [*]).
  con (Prod zs) =>
  FreeSMC cat con (Prod zs) (Prod (Cons x Null) ⊗ Prod zs)
  -> Merge cat con a zs -> k)
 -> k)
-> (forall (zs :: [*]).
    con (Prod zs) =>
    FreeSMC cat con (Prod zs) (Prod (Cons x Null) ⊗ Prod zs)
    -> Merge cat con a zs -> k)
-> k
forall a b. (a -> b) -> a -> b
$ \FreeSMC cat con (Prod zs) (Prod (Cons x Null) ⊗ Prod zs)
g' Merge cat con a zs
rest'' ->
  FreeSMC cat con (Prod zs) (Prod xs) -> Merge cat con a zs -> k
forall (zs :: [*]).
con (Prod zs) =>
FreeSMC cat con (Prod zs) (Prod xs) -> Merge cat con a zs -> k
k ((Cat cat con (x ⊗ ()) x
forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k (a ⊗ ()) a
unitor' Cat cat con (x ⊗ ()) x
-> FreeSMC cat con (Prod zs) (Prod xs)
-> Cat cat con ((x ⊗ ()) ⊗ Prod zs) (x ⊗ Prod xs)
forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× FreeSMC cat con (Prod zs) (Prod xs)
g) Cat cat con ((x ⊗ ()) ⊗ Prod zs) (x ⊗ Prod xs)
-> Cat cat con (Prod zs) ((x ⊗ ()) ⊗ Prod zs)
-> Cat cat con (Prod zs) (x ⊗ Prod xs)
forall (k :: * -> * -> *) a b c.
(Category k, Obj k a, Obj k b, Obj k c) =>
k b c -> k a b -> k a c
∘ Cat cat con (Prod zs) ((x ⊗ ()) ⊗ Prod zs)
FreeSMC cat con (Prod zs) (Prod (Cons x Null) ⊗ Prod zs)
g') Merge cat con a zs
rest''
  
appendSorted  :: {-<-}(ProdObj con, forall x y. (con x, con y) => con (x,y), con (), con a, con (Prod xs), con (Prod ys)) => {->-} Merge cat {-<-}con{->-} a xs -> Merge cat {-<-}con{->-} a ys ->
                 (  forall zs. {-<-}con(Prod zs)=> {->-}FreeSMC cat {-<-}con{->-}  (Prod zs)
                                                                                   (Prod xs ⊗ Prod ys)  ->
                    Merge cat{-<-}con{->-} a zs -> k) -> k
appendSorted :: forall (con :: * -> Constraint) a (xs :: [*]) (ys :: [*])
       (cat :: * -> * -> *) k.
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con a, con (Prod xs), con (Prod ys)) =>
Merge cat con a xs
-> Merge cat con a ys
-> (forall (zs :: [*]).
    con (Prod zs) =>
    FreeSMC cat con (Prod zs) (Prod xs ⊗ Prod ys)
    -> Merge cat con a zs -> k)
-> k
appendSorted  Merge cat con a xs
Nil        Merge cat con a ys
ys         forall (zs :: [*]).
con (Prod zs) =>
FreeSMC cat con (Prod zs) (Prod xs ⊗ Prod ys)
-> Merge cat con a zs -> k
k = FreeSMC cat con (Prod ys) (Prod xs ⊗ Prod ys)
-> Merge cat con a ys -> k
forall (zs :: [*]).
con (Prod zs) =>
FreeSMC cat con (Prod zs) (Prod xs ⊗ Prod ys)
-> Merge cat con a zs -> k
k (Cat cat con (Prod ys ⊗ ()) (() ⊗ Prod ys)
forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap Cat cat con (Prod ys ⊗ ()) (() ⊗ Prod ys)
-> Cat cat con (Prod ys) (Prod ys ⊗ ())
-> Cat cat con (Prod ys) (() ⊗ Prod ys)
forall (k :: * -> * -> *) a b c.
(Category k, Obj k a, Obj k b, Obj k c) =>
k b c -> k a b -> k a c
∘  Cat cat con (Prod ys) (Prod ys ⊗ ())
forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k a (a ⊗ ())
unitor)  Merge cat con a ys
ys
appendSorted  Merge cat con a xs
xs         Merge cat con a ys
Nil        forall (zs :: [*]).
con (Prod zs) =>
FreeSMC cat con (Prod zs) (Prod xs ⊗ Prod ys)
-> Merge cat con a zs -> k
k = FreeSMC cat con (Prod xs) (Prod xs ⊗ Prod ys)
-> Merge cat con a xs -> k
forall (zs :: [*]).
con (Prod zs) =>
FreeSMC cat con (Prod zs) (Prod xs ⊗ Prod ys)
-> Merge cat con a zs -> k
k          FreeSMC cat con (Prod xs) (Prod xs ⊗ Prod ys)
forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k a (a ⊗ ())
unitor   Merge cat con a xs
xs
appendSorted  (FreeCartesian cat con a x
x :+ Merge cat con a xs
xs)  (FreeCartesian cat con a x
y :+ Merge cat con a xs
ys)  forall (zs :: [*]).
con (Prod zs) =>
FreeSMC cat con (Prod zs) (Prod xs ⊗ Prod ys)
-> Merge cat con a zs -> k
k =
  case FreeCartesian cat con a x -> FreeCartesian cat con a x -> Order x x
forall (con :: * -> Constraint) a b c (cat :: * -> * -> *).
(con a, con b, con c) =>
Cat cat con a b -> Cat cat con a c -> Order b c
compareMorphisms FreeCartesian cat con a x
x FreeCartesian cat con a x
y of
    Order x x
GT  ->   Merge cat con a (x : xs)
-> Merge cat con a xs
-> (forall (zs :: [*]).
    con (Prod zs) =>
    FreeSMC cat con (Prod zs) (Prod (x : xs) ⊗ Prod xs)
    -> Merge cat con a zs -> k)
-> k
forall (con :: * -> Constraint) a (xs :: [*]) (ys :: [*])
       (cat :: * -> * -> *) k.
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con a, con (Prod xs), con (Prod ys)) =>
Merge cat con a xs
-> Merge cat con a ys
-> (forall (zs :: [*]).
    con (Prod zs) =>
    FreeSMC cat con (Prod zs) (Prod xs ⊗ Prod ys)
    -> Merge cat con a zs -> k)
-> k
appendSorted (FreeCartesian cat con a x
x FreeCartesian cat con a x
-> Merge cat con a xs -> Merge cat con a (x : xs)
forall (con :: * -> Constraint) b (xs :: [*]) (k :: * -> * -> *) a.
(con b, con (Prod xs)) =>
FreeCartesian k con a b
-> Merge k con a xs -> Merge k con a (Cons b xs)
:+ Merge cat con a xs
xs) Merge cat con a xs
ys ((forall (zs :: [*]).
  con (Prod zs) =>
  FreeSMC cat con (Prod zs) (Prod (x : xs) ⊗ Prod xs)
  -> Merge cat con a zs -> k)
 -> k)
-> (forall (zs :: [*]).
    con (Prod zs) =>
    FreeSMC cat con (Prod zs) (Prod (x : xs) ⊗ Prod xs)
    -> Merge cat con a zs -> k)
-> k
forall a b. (a -> b) -> a -> b
$ \FreeSMC cat con (Prod zs) (Prod (x : xs) ⊗ Prod xs)
a Merge cat con a zs
zs ->
             FreeSMC cat con (Prod (Cons x zs)) (Prod xs ⊗ Prod ys)
-> Merge cat con a (Cons x zs) -> k
forall (zs :: [*]).
con (Prod zs) =>
FreeSMC cat con (Prod zs) (Prod xs ⊗ Prod ys)
-> Merge cat con a zs -> k
k (Cat
  cat
  con
  (((x ⊗ Prod xs) ⊗ x) ⊗ Prod xs)
  ((x ⊗ Prod xs) ⊗ (x ⊗ Prod xs))
forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
assoc Cat
  cat
  con
  (((x ⊗ Prod xs) ⊗ x) ⊗ Prod xs)
  ((x ⊗ Prod xs) ⊗ (x ⊗ Prod xs))
-> Cat
     cat
     con
     ((x ⊗ (x ⊗ Prod xs)) ⊗ Prod xs)
     (((x ⊗ Prod xs) ⊗ x) ⊗ Prod xs)
-> Cat
     cat
     con
     ((x ⊗ (x ⊗ Prod xs)) ⊗ Prod xs)
     ((x ⊗ Prod xs) ⊗ (x ⊗ Prod xs))
forall (k :: * -> * -> *) a b c.
(Category k, Obj k a, Obj k b, Obj k c) =>
k b c -> k a b -> k a c
∘ (Cat cat con (x ⊗ (x ⊗ Prod xs)) ((x ⊗ Prod xs) ⊗ x)
forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap Cat cat con (x ⊗ (x ⊗ Prod xs)) ((x ⊗ Prod xs) ⊗ x)
-> Cat cat con (Prod xs) (Prod xs)
-> Cat
     cat
     con
     ((x ⊗ (x ⊗ Prod xs)) ⊗ Prod xs)
     (((x ⊗ Prod xs) ⊗ x) ⊗ Prod xs)
forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× Cat cat con (Prod xs) (Prod xs)
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id) Cat
  cat
  con
  ((x ⊗ (x ⊗ Prod xs)) ⊗ Prod xs)
  ((x ⊗ Prod xs) ⊗ (x ⊗ Prod xs))
-> Cat
     cat
     con
     (x ⊗ ((x ⊗ Prod xs) ⊗ Prod xs))
     ((x ⊗ (x ⊗ Prod xs)) ⊗ Prod xs)
-> Cat
     cat
     con
     (x ⊗ ((x ⊗ Prod xs) ⊗ Prod xs))
     ((x ⊗ Prod xs) ⊗ (x ⊗ Prod xs))
forall (k :: * -> * -> *) a b c.
(Category k, Obj k a, Obj k b, Obj k c) =>
k b c -> k a b -> k a c
∘  Cat
  cat
  con
  (x ⊗ ((x ⊗ Prod xs) ⊗ Prod xs))
  ((x ⊗ (x ⊗ Prod xs)) ⊗ Prod xs)
forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
assoc' Cat
  cat
  con
  (x ⊗ ((x ⊗ Prod xs) ⊗ Prod xs))
  ((x ⊗ Prod xs) ⊗ (x ⊗ Prod xs))
-> Cat cat con (x ⊗ Prod zs) (x ⊗ ((x ⊗ Prod xs) ⊗ Prod xs))
-> Cat cat con (x ⊗ Prod zs) ((x ⊗ Prod xs) ⊗ (x ⊗ Prod xs))
forall (k :: * -> * -> *) a b c.
(Category k, Obj k a, Obj k b, Obj k c) =>
k b c -> k a b -> k a c
∘ (Cat cat con x x
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id Cat cat con x x
-> Cat cat con (Prod zs) ((x ⊗ Prod xs) ⊗ Prod xs)
-> Cat cat con (x ⊗ Prod zs) (x ⊗ ((x ⊗ Prod xs) ⊗ Prod xs))
forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× Cat cat con (Prod zs) ((x ⊗ Prod xs) ⊗ Prod xs)
FreeSMC cat con (Prod zs) (Prod (x : xs) ⊗ Prod xs)
a))  (FreeCartesian cat con a x
y FreeCartesian cat con a x
-> Merge cat con a zs -> Merge cat con a (Cons x zs)
forall (con :: * -> Constraint) b (xs :: [*]) (k :: * -> * -> *) a.
(con b, con (Prod xs)) =>
FreeCartesian k con a b
-> Merge k con a xs -> Merge k con a (Cons b xs)
:+ Merge cat con a zs
zs)
    Order x x
_   ->   Merge cat con a xs
-> Merge cat con a (x : xs)
-> (forall (zs :: [*]).
    con (Prod zs) =>
    FreeSMC cat con (Prod zs) (Prod xs ⊗ Prod (x : xs))
    -> Merge cat con a zs -> k)
-> k
forall (con :: * -> Constraint) a (xs :: [*]) (ys :: [*])
       (cat :: * -> * -> *) k.
(ProdObj con, forall x y. (con x, con y) => con (x, y), con (),
 con a, con (Prod xs), con (Prod ys)) =>
Merge cat con a xs
-> Merge cat con a ys
-> (forall (zs :: [*]).
    con (Prod zs) =>
    FreeSMC cat con (Prod zs) (Prod xs ⊗ Prod ys)
    -> Merge cat con a zs -> k)
-> k
appendSorted Merge cat con a xs
xs (FreeCartesian cat con a x
y FreeCartesian cat con a x
-> Merge cat con a xs -> Merge cat con a (x : xs)
forall (con :: * -> Constraint) b (xs :: [*]) (k :: * -> * -> *) a.
(con b, con (Prod xs)) =>
FreeCartesian k con a b
-> Merge k con a xs -> Merge k con a (Cons b xs)
:+ Merge cat con a xs
ys) ((forall (zs :: [*]).
  con (Prod zs) =>
  FreeSMC cat con (Prod zs) (Prod xs ⊗ Prod (x : xs))
  -> Merge cat con a zs -> k)
 -> k)
-> (forall (zs :: [*]).
    con (Prod zs) =>
    FreeSMC cat con (Prod zs) (Prod xs ⊗ Prod (x : xs))
    -> Merge cat con a zs -> k)
-> k
forall a b. (a -> b) -> a -> b
$ \FreeSMC cat con (Prod zs) (Prod xs ⊗ Prod (x : xs))
a Merge cat con a zs
zs ->
             FreeSMC cat con (Prod (Cons x zs)) (Prod xs ⊗ Prod ys)
-> Merge cat con a (Cons x zs) -> k
forall (zs :: [*]).
con (Prod zs) =>
FreeSMC cat con (Prod zs) (Prod xs ⊗ Prod ys)
-> Merge cat con a zs -> k
k (                       Cat
  cat
  con
  (x ⊗ (Prod xs ⊗ (x ⊗ Prod xs)))
  ((x ⊗ Prod xs) ⊗ (x ⊗ Prod xs))
forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
assoc' Cat
  cat
  con
  (x ⊗ (Prod xs ⊗ (x ⊗ Prod xs)))
  ((x ⊗ Prod xs) ⊗ (x ⊗ Prod xs))
-> Cat cat con (x ⊗ Prod zs) (x ⊗ (Prod xs ⊗ (x ⊗ Prod xs)))
-> Cat cat con (x ⊗ Prod zs) ((x ⊗ Prod xs) ⊗ (x ⊗ Prod xs))
forall (k :: * -> * -> *) a b c.
(Category k, Obj k a, Obj k b, Obj k c) =>
k b c -> k a b -> k a c
∘ (Cat cat con x x
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id Cat cat con x x
-> Cat cat con (Prod zs) (Prod xs ⊗ (x ⊗ Prod xs))
-> Cat cat con (x ⊗ Prod zs) (x ⊗ (Prod xs ⊗ (x ⊗ Prod xs)))
forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× Cat cat con (Prod zs) (Prod xs ⊗ (x ⊗ Prod xs))
FreeSMC cat con (Prod zs) (Prod xs ⊗ Prod (x : xs))
a))  (FreeCartesian cat con a x
x FreeCartesian cat con a x
-> Merge cat con a zs -> Merge cat con a (Cons x zs)
forall (con :: * -> Constraint) b (xs :: [*]) (k :: * -> * -> *) a.
(con b, con (Prod xs)) =>
FreeCartesian k con a b
-> Merge k con a xs -> Merge k con a (Cons b xs)
:+ Merge cat con a zs
zs)

-- | intermediate result
data R cat con a b where
  St :: con (Prod b)
    => FreeSMC k con (Prod b) c -- already processed part (SMC here)
    -> Merge k con a b -- maximally exposed and sorted merge tree (see 'expose' below)
    -> R k con a c

-- | Perform 1 reduction step, assumes input is already maximally exposed and sorted. 
reductionStep :: (ProdObj con, forall α β. (con α, con β) => con (α,β), con (), con a, con b) => R cat con a b -> R cat con a b
reductionStep :: forall (con :: * -> Constraint) a b (cat :: * -> * -> *).
(ProdObj con, forall α β. (con α, con β) => con (α, β), con (),
 con a, con b) =>
R cat con a b -> R cat con a b
reductionStep (St FreeSMC cat con (Prod b) b
r1 (FreeCartesian cat con a x
f :+ Merge cat con a xs
Nil)) = FreeCartesian cat con a x
-> (forall (x :: [*]).
    con (Prod x) =>
    FreeSMC cat con (Prod x) x -> Merge cat con a x -> R cat con a b)
-> R cat con a b
forall (con :: * -> Constraint) a b (cat :: * -> * -> *) k.
(ProdObj con, forall α β. (con α, con β) => con (α, β), con (),
 con a, con b) =>
Cat cat con a b
-> (forall (x :: [*]).
    con (Prod x) =>
    FreeSMC cat con (Prod x) b -> Merge cat con a x -> k)
-> k
expose FreeCartesian cat con a x
f ((forall (x :: [*]).
  con (Prod x) =>
  FreeSMC cat con (Prod x) x -> Merge cat con a x -> R cat con a b)
 -> R cat con a b)
-> (forall (x :: [*]).
    con (Prod x) =>
    FreeSMC cat con (Prod x) x -> Merge cat con a x -> R cat con a b)
-> R cat con a b
forall a b. (a -> b) -> a -> b
$ \FreeSMC cat con (Prod x) x
ready Merge cat con a x
m -> FreeSMC cat con (Prod x) b -> Merge cat con a x -> R cat con a b
forall (con :: * -> Constraint) (b :: [*]) (k :: * -> * -> *) c a.
con (Prod b) =>
FreeSMC k con (Prod b) c -> Merge k con a b -> R k con a c
St (Cat cat con (x ⊗ ()) b
FreeSMC cat con (Prod b) b
r1 Cat cat con (x ⊗ ()) b -> Cat cat con x (x ⊗ ()) -> Cat cat con x b
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Cat cat con x (x ⊗ ())
forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k a (a ⊗ ())
unitor Cat cat con x b
-> FreeSMC cat con (Prod x) x -> FreeSMC cat con (Prod x) b
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. FreeSMC cat con (Prod x) x
ready) Merge cat con a x
m  -- single morphism to analyse
reductionStep (St FreeSMC cat con (Prod b) b
r1 Merge cat con a b
m) = Merge cat con a b
-> (forall (zs :: [*]).
    con (Prod zs) =>
    FreeSMC cat con (Prod zs) (Prod b)
    -> Merge cat con a zs -> R cat con a b)
-> R cat con a b
forall (con :: * -> Constraint) a (xs :: [*]) (cat :: * -> * -> *)
       k.
(ProdObj con, forall α β. (con α, con β) => con (α, β), con (),
 con a, con (Prod xs)) =>
Merge cat con a xs
-> (forall (zs :: [*]).
    con (Prod zs) =>
    FreeSMC cat con (Prod zs) (Prod xs) -> Merge cat con a zs -> k)
-> k
reduceStep Merge cat con a b
m ((forall (zs :: [*]).
  con (Prod zs) =>
  FreeSMC cat con (Prod zs) (Prod b)
  -> Merge cat con a zs -> R cat con a b)
 -> R cat con a b)
-> (forall (zs :: [*]).
    con (Prod zs) =>
    FreeSMC cat con (Prod zs) (Prod b)
    -> Merge cat con a zs -> R cat con a b)
-> R cat con a b
forall a b. (a -> b) -> a -> b
$ \FreeSMC cat con (Prod zs) (Prod b)
r2 Merge cat con a zs
m' -> FreeSMC cat con (Prod zs) b -> Merge cat con a zs -> R cat con a b
forall (con :: * -> Constraint) (b :: [*]) (k :: * -> * -> *) c a.
con (Prod b) =>
FreeSMC k con (Prod b) c -> Merge k con a b -> R k con a c
St (FreeSMC cat con (Prod b) b
r1 FreeSMC cat con (Prod b) b
-> FreeSMC cat con (Prod zs) (Prod b)
-> FreeSMC cat con (Prod zs) b
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. FreeSMC cat con (Prod zs) (Prod b)
r2) Merge cat con a zs
m' -- L/R pair to find and reduce

-- | Perform all reduction steps and return intermediate states
reductionSteps  :: (ProdObj con, forall α β. (con α, con β) => con (α,β), con (), 
               con a, con b) => R cat con a b -> [R cat con a b]
reductionSteps :: forall (con :: * -> Constraint) a b (cat :: * -> * -> *).
(ProdObj con, forall α β. (con α, con β) => con (α, β), con (),
 con a, con b) =>
R cat con a b -> [R cat con a b]
reductionSteps st :: R cat con a b
st@(St FreeSMC cat con (Prod b) b
_ (FreeCartesian cat con a x
I :+ Merge cat con a xs
Nil)) = [R cat con a b
st] -- done!
reductionSteps R cat con a b
st = R cat con a b
st R cat con a b -> [R cat con a b] -> [R cat con a b]
forall a. a -> [a] -> [a]
: R cat con a b -> [R cat con a b]
forall (con :: * -> Constraint) a b (cat :: * -> * -> *).
(ProdObj con, forall α β. (con α, con β) => con (α, β), con (),
 con a, con b) =>
R cat con a b -> [R cat con a b]
reductionSteps (R cat con a b -> R cat con a b
forall (con :: * -> Constraint) a b (cat :: * -> * -> *).
(ProdObj con, forall α β. (con α, con β) => con (α, β), con (),
 con a, con b) =>
R cat con a b -> R cat con a b
reductionStep R cat con a b
st)

freeToR :: (ProdObj con, forall α β. (con α, con β) => con (α,β), con (),
           con x) => Cat k con a x -> R k con a x
freeToR :: forall (con :: * -> Constraint) x (k :: * -> * -> *) a.
(ProdObj con, forall α β. (con α, con β) => con (α, β), con (),
 con x) =>
Cat k con a x -> R k con a x
freeToR Cat k con a x
f = FreeSMC k con (Prod (Cons x Null)) x
-> Merge k con a (Cons x Null) -> R k con a x
forall (con :: * -> Constraint) (b :: [*]) (k :: * -> * -> *) c a.
con (Prod b) =>
FreeSMC k con (Prod b) c -> Merge k con a b -> R k con a c
St FreeSMC k con (Prod (Cons x Null)) x
forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k (a ⊗ ()) a
unitor' (Cat k con a x
f Cat k con a x -> Merge k con a Null -> Merge k con a (Cons x Null)
forall (con :: * -> Constraint) b (xs :: [*]) (k :: * -> * -> *) a.
(con b, con (Prod xs)) =>
FreeCartesian k con a b
-> Merge k con a xs -> Merge k con a (Cons b xs)
:+ Merge k con a Null
forall (k :: * -> * -> *) (con :: * -> Constraint) a.
Merge k con a Null
Nil)

rToFree :: (Obj cat ~ con, ProdObj con, forall α β. (con α, con β) => con (α,β), con (), con a, con b)
        => R cat con a b -> FreeSMC cat con a b
rToFree :: forall (cat :: * -> * -> *) (con :: * -> Constraint) a b.
(Obj cat ~ con, ProdObj con,
 forall α β. (con α, con β) => con (α, β), con (), con a, con b) =>
R cat con a b -> FreeSMC cat con a b
rToFree (St FreeSMC cat con (Prod b) b
done (FreeCartesian cat con a x
I :+ Merge cat con a xs
Nil)) = Cat cat con (a ⊗ ()) b
FreeSMC cat con (Prod b) b
done Cat cat con (a ⊗ ()) b -> Cat cat con a (a ⊗ ()) -> Cat cat con a b
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Cat cat con a (a ⊗ ())
forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k a (a ⊗ ())
unitor

reduce  :: (Obj cat ~ con, ProdObj con, forall α β. (con α, con β) => con (α,β), con (),
             con a, con b) => Cartesian.Cat cat con a b -> FreeSMC cat con a b
reduce :: forall (cat :: * -> * -> *) (con :: * -> Constraint) a b.
(Obj cat ~ con, ProdObj con,
 forall α β. (con α, con β) => con (α, β), con (), con a, con b) =>
Cat cat con a b -> FreeSMC cat con a b
reduce = R cat con a b -> FreeSMC cat con a b
forall (cat :: * -> * -> *) (con :: * -> Constraint) a b.
(Obj cat ~ con, ProdObj con,
 forall α β. (con α, con β) => con (α, β), con (), con a, con b) =>
R cat con a b -> FreeSMC cat con a b
rToFree (R cat con a b -> FreeSMC cat con a b)
-> ([R cat con a b] -> R cat con a b)
-> [R cat con a b]
-> FreeSMC cat con a b
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. [R cat con a b] -> R cat con a b
forall a. [a] -> a
last ([R cat con a b] -> FreeSMC cat con a b)
-> (R cat con a b -> [R cat con a b])
-> R cat con a b
-> FreeSMC cat con a b
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. R cat con a b -> [R cat con a b]
forall (con :: * -> Constraint) a b (cat :: * -> * -> *).
(ProdObj con, forall α β. (con α, con β) => con (α, β), con (),
 con a, con b) =>
R cat con a b -> [R cat con a b]
reductionSteps (R cat con a b -> FreeSMC cat con a b)
-> (Cat cat con a b -> R cat con a b)
-> Cat cat con a b
-> FreeSMC cat con a b
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. Cat cat con a b -> R cat con a b
forall (con :: * -> Constraint) x (k :: * -> * -> *) a.
(ProdObj con, forall α β. (con α, con β) => con (α, β), con (),
 con x) =>
Cat k con a x -> R k con a x
freeToR

-- Invariant: same source!
compareMorphisms :: (con a, con b, con c) => Cat cat con a b -> Cat cat con a c -> Order b c
compareMorphisms :: forall (con :: * -> Constraint) a b c (cat :: * -> * -> *).
(con a, con b, con c) =>
Cat cat con a b -> Cat cat con a c -> Order b c
compareMorphisms FreeCartesian cat con a b
I FreeCartesian cat con a c
I = Order b c
forall {k} (a :: k). Order a a
EQ
compareMorphisms FreeCartesian cat con a b
I FreeCartesian cat con a c
_ = Order b c
forall {k} (a :: k) (b :: k). Order a b
LT
compareMorphisms FreeCartesian cat con a b
_ FreeCartesian cat con a c
I = Order b c
forall {k} (a :: k) (b :: k). Order a b
GT
compareMorphisms (Cat cat con b b
f Cartesian.:>: Cat cat con a b
g) (Cat cat con b c
f' Cartesian.:>: Cat cat con a b
g') =
  case Cat cat con a b -> Cat cat con a b -> Order b b
forall (con :: * -> Constraint) a b c (cat :: * -> * -> *).
(con a, con b, con c) =>
Cat cat con a b -> Cat cat con a c -> Order b c
compareAtoms Cat cat con a b
g Cat cat con a b
g' of
    Order b b
LT -> Order b c
forall {k} (a :: k) (b :: k). Order a b
LT
    Order b b
GT -> Order b c
forall {k} (a :: k) (b :: k). Order a b
GT
    Order b b
EQ -> Cat cat con b b -> Cat cat con b c -> Order b c
forall (con :: * -> Constraint) a b c (cat :: * -> * -> *).
(con a, con b, con c) =>
Cat cat con a b -> Cat cat con a c -> Order b c
compareMorphisms Cat cat con b b
f Cat cat con b c
Cat cat con b c
f'

-- Invariant: same source!
compareAtoms :: (con a, con b, con c) => Cat cat con a b -> Cat cat con a c -> Order b c
compareAtoms :: forall (con :: * -> Constraint) a b c (cat :: * -> * -> *).
(con a, con b, con c) =>
Cat cat con a b -> Cat cat con a c -> Order b c
compareAtoms FreeCartesian cat con a b
P1 FreeCartesian cat con a c
P1 = Order b c
forall {k} (a :: k). Order a a
EQ
compareAtoms FreeCartesian cat con a b
P2 FreeCartesian cat con a c
P2 = Order b c
forall {k} (a :: k). Order a a
EQ
compareAtoms FreeCartesian cat con a b
E FreeCartesian cat con a c
E = Order b c
forall {k} (a :: k). Order a a
EQ
compareAtoms (Embed cat a b
_) (Embed cat a c
_) = Order Any Any -> Order b c
forall a b. a -> b
unsafeCoerce Order Any Any
forall {k} (a :: k). Order a a
EQ -- Same source -> same Atoms
compareAtoms (FreeCartesian cat con a b
f :▵: FreeCartesian cat con a c
g) (FreeCartesian cat con a b
f' :▵: FreeCartesian cat con a c
g') = case FreeCartesian cat con a b -> FreeCartesian cat con a b -> Order b b
forall (con :: * -> Constraint) a b c (cat :: * -> * -> *).
(con a, con b, con c) =>
Cat cat con a b -> Cat cat con a c -> Order b c
compareMorphisms FreeCartesian cat con a b
f FreeCartesian cat con a b
f' of
  Order b b
LT -> Order b c
forall {k} (a :: k) (b :: k). Order a b
LT
  Order b b
GT -> Order b c
forall {k} (a :: k) (b :: k). Order a b
GT
  Order b b
EQ -> case FreeCartesian cat con a c -> FreeCartesian cat con a c -> Order c c
forall (con :: * -> Constraint) a b c (cat :: * -> * -> *).
(con a, con b, con c) =>
Cat cat con a b -> Cat cat con a c -> Order b c
compareMorphisms FreeCartesian cat con a c
g FreeCartesian cat con a c
g' of
    Order c c
LT -> Order b c
forall {k} (a :: k) (b :: k). Order a b
LT
    Order c c
GT -> Order b c
forall {k} (a :: k) (b :: k). Order a b
GT
    Order c c
EQ -> Order b c
forall {k} (a :: k). Order a a
EQ
compareAtoms (FreeCartesian cat con a b
P1) (FreeCartesian cat con a c
_) = Order b c
forall {k} (a :: k) (b :: k). Order a b
LT
compareAtoms (FreeCartesian cat con a b
_) (FreeCartesian cat con a c
P1) = Order b c
forall {k} (a :: k) (b :: k). Order a b
GT
compareAtoms (FreeCartesian cat con a b
P2) (FreeCartesian cat con a c
_) = Order b c
forall {k} (a :: k) (b :: k). Order a b
LT
compareAtoms (FreeCartesian cat con a b
_) (FreeCartesian cat con a c
P2) = Order b c
forall {k} (a :: k) (b :: k). Order a b
GT
compareAtoms (Embed cat a b
_) (FreeCartesian cat con a c
_) = Order b c
forall {k} (a :: k) (b :: k). Order a b
LT
compareAtoms (FreeCartesian cat con a b
_) (Embed cat a c
_) = Order b c
forall {k} (a :: k) (b :: k). Order a b
GT
compareAtoms (FreeCartesian cat con a b
E) (FreeCartesian cat con a c
_) = Order b c
forall {k} (a :: k) (b :: k). Order a b
LT
compareAtoms (FreeCartesian cat con a b
_) (FreeCartesian cat con a c
E) = Order b c
forall {k} (a :: k) (b :: k). Order a b
GT
compareAtoms FreeCartesian cat con a b
f FreeCartesian cat con a c
g = [Char] -> Order b c
forall a. HasCallStack => [Char] -> a
error ([Char]
"compareAtoms:\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> FreeCartesian cat con a b -> [Char] -> [Char]
forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
Int -> Cat k con a b -> [Char] -> [Char]
showDbg Int
0 FreeCartesian cat con a b
f [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> FreeCartesian cat con a c -> [Char] -> [Char]
forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
Int -> Cat k con a b -> [Char] -> [Char]
showDbg Int
0 FreeCartesian cat con a c
g [Char]
"" )