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


module Control.Category.Linear (
  -- Interface
  type P, unit, split, merge,
  -- pattern (:::),
  encode, decode, (!:),
  -- 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



-- Linear patterns don't really work, and some version of GHC do not accept this declaration at all. Disabled for now.
-- 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 ::: y <- (split @con -> (x,y))
--   where x ::: y = merge @con (x,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 = 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)    = forall (k :: * -> * -> *) r a.
FreeCartesian k (Obj k) r a -> P k r a
Y (forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(con a, con b) =>
k a b -> FreeCartesian k con a b
Embed k a 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              = forall (k :: * -> * -> *) r a.
FreeCartesian k (Obj k) r a -> P k r a
Y 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)       = (forall (k :: * -> * -> *) r a.
FreeCartesian k (Obj k) r a -> P k r a
Y (forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) a
exl 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 ⊗ b)
f), forall (k :: * -> * -> *) r a.
FreeCartesian k (Obj k) r a -> P k r a
Y (forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) b
exr 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 ⊗ 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)  = forall (k :: * -> * -> *) r a.
FreeCartesian k (Obj k) r a -> P k r a
Y (FreeCartesian k (Obj k) r a
f 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 (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          = 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 (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 (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         = forall (k :: * -> * -> *) r a.
P k r a -> FreeCartesian k (Obj k) r a
fromP (forall r. Obj k r => P k r a %1 -> P k r b
f (forall (k :: * -> * -> *) r a.
FreeCartesian k (Obj k) r a -> P k r a
Y 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  = forall (k :: * -> * -> *) r a b.
O3 k r a b =>
k a b -> P k r a %1 -> P k r b
encode forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k (a ⊗ ()) a
unitor' (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  = forall (k :: * -> * -> *) r a b.
O3 k r a b =>
k a b -> P k r a %1 -> P k r b
encode 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  = forall (k :: * -> * -> *) r a b.
O3 k r a b =>
k a b -> P k r a %1 -> P k r b
encode 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      =  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 a b. (a -> b) -> a -> b
$ \FreeSMC cat con (Prod x) b
g1 Merge cat con a x
fs1 ->
                             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 a b. (a -> b) -> a -> b
$ \FreeSMC cat con (Prod x) c
g2 Merge cat con a x
fs2 ->
                             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 a b. (a -> b) -> a -> b
$ \FreeSMC cat con (Prod zs) (Prod x ⊗ Prod x)
g Merge cat con a zs
fs ->
                             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 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) 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  =  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 a b. (a -> b) -> a -> b
$ \FreeSMC cat con (Prod x) b
g Merge cat con a x
fs ->
                             forall (x :: [*]).
con (Prod x) =>
FreeSMC cat con (Prod x) b -> Merge cat con a x -> k
k (forall (con :: * -> Constraint) a b (k :: * -> * -> *).
(con a, con b) =>
k a b -> Cat k con a b
SMC.Embed cat b 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        = forall (x :: [*]).
con (Prod x) =>
FreeSMC cat con (Prod x) b -> Merge cat con a x -> k
k forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id 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                = forall (x :: [*]).
con (Prod x) =>
FreeSMC cat con (Prod x) b -> Merge cat con a x -> k
k forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k (a ⊗ ()) a
unitor' (FreeCartesian cat con a b
x 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)
:+ 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 <- 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₂ =
  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 a b. (a -> b) -> a -> b
$ \FreeSMC cat con (Prod x) b
g Merge cat con a x
f' -> -- expose any merge
  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 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
  forall (zs :: [*]).
con (Prod zs) =>
FreeSMC cat con (Prod zs) (Prod xs) -> Merge cat con a zs -> k
k (forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
assoc 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 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)
× forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id) 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 =
  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 a b. (a -> b) -> a -> b
$ \FreeSMC cat con (Prod zs) (Prod xs)
g Merge cat con a zs
rest' ->
  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 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)
:+ forall (k :: * -> * -> *) (con :: * -> Constraint) a.
Merge k con a Null
Nil) Merge cat con a zs
rest'  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'' ->
  forall (zs :: [*]).
con (Prod zs) =>
FreeSMC cat con (Prod zs) (Prod xs) -> Merge cat con a zs -> k
k ((forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k (a ⊗ ()) a
unitor' 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) 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 (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 = forall (zs :: [*]).
con (Prod zs) =>
FreeSMC cat con (Prod zs) (Prod xs ⊗ Prod ys)
-> Merge cat con a zs -> k
k (forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap 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
∘  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 = forall (zs :: [*]).
con (Prod zs) =>
FreeSMC cat con (Prod zs) (Prod xs ⊗ Prod ys)
-> Merge cat con a zs -> k
k          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 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  ->   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 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 a b. (a -> b) -> a -> b
$ \FreeSMC cat con (Prod zs) (Prod (x : xs) ⊗ Prod xs)
a Merge cat con a zs
zs ->
             forall (zs :: [*]).
con (Prod zs) =>
FreeSMC cat con (Prod zs) (Prod xs ⊗ Prod ys)
-> Merge cat con a zs -> k
k (forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
assoc 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
∘ (forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap 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)
× forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id) 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
∘  forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
assoc' 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
∘ (forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id 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 (x : xs) ⊗ Prod xs)
a))  (FreeCartesian cat con a x
y 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
_   ->   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 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 a b. (a -> b) -> a -> b
$ \FreeSMC cat con (Prod zs) (Prod xs ⊗ Prod (x : xs))
a Merge cat con a zs
zs ->
             forall (zs :: [*]).
con (Prod zs) =>
FreeSMC cat con (Prod zs) (Prod xs ⊗ Prod ys)
-> Merge cat con a zs -> k
k (                       forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
assoc' 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
∘ (forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id 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 ⊗ Prod (x : xs))
a))  (FreeCartesian cat con a x
x 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)) = 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 a b. (a -> b) -> a -> b
$ \FreeSMC cat con (Prod x) x
ready Merge cat con a x
m -> 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 forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k a (a ⊗ ())
unitor 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) = 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 a b. (a -> b) -> a -> b
$ \FreeSMC cat con (Prod zs) (Prod b)
r2 Merge cat con a zs
m' -> 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 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
_ Merge cat con a b
Nil) = [R cat con a b
st] -- done; and all the input is discarded
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 forall a. a -> [a] -> [a]
: 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 (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 = 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 forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k (a ⊗ ()) a
unitor' (Cat k con a x
f 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)
:+ 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 Merge cat con a b
Nil) = forall a b. a -> b
unsafeCoerce FreeSMC cat con (Prod b) b
done
-- why is the above safe? (St _ Nil) means that the whole input is
-- discarded/the whole expression has no free variable. In other
-- words, the input is the unit type. So we can coerce. 
--
-- Other explanation:
-- Our input is (f id), with f : (r `k` a) ⊸ r `k` b
-- We know that (f id) starts with discard.  Because f is linear, (f
-- id) can discard its input only if the input type is the unit in the
-- first place, hence a=().
rToFree (St FreeSMC cat con (Prod b) b
done (FreeCartesian cat con a x
I :+ Merge cat con a xs
Nil)) = FreeSMC cat con (Prod b) b
done forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. 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 = 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 forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall a. [a] -> a
last forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. 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 forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. 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 = forall {k} (a :: k). Order a a
EQ
compareMorphisms FreeCartesian cat con a b
I FreeCartesian cat con a c
_ = forall {k} (a :: k) (b :: k). Order a b
LT
compareMorphisms FreeCartesian cat con a b
_ FreeCartesian cat con a c
I = 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 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 -> forall {k} (a :: k) (b :: k). Order a b
LT
    Order b b
GT -> forall {k} (a :: k) (b :: k). Order a b
GT
    Order b b
EQ -> 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
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 = forall {k} (a :: k). Order a a
EQ
compareAtoms FreeCartesian cat con a b
P2 FreeCartesian cat con a c
P2 = forall {k} (a :: k). Order a a
EQ
compareAtoms FreeCartesian cat con a b
E FreeCartesian cat con a c
E = forall {k} (a :: k). Order a a
EQ
compareAtoms (Embed cat a b
_) (Embed cat a c
_) = forall a b. a -> b
unsafeCoerce 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 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 -> forall {k} (a :: k) (b :: k). Order a b
LT
  Order b b
GT -> forall {k} (a :: k) (b :: k). Order a b
GT
  Order b b
EQ -> case 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 -> forall {k} (a :: k) (b :: k). Order a b
LT
    Order c c
GT -> forall {k} (a :: k) (b :: k). Order a b
GT
    Order c c
EQ -> forall {k} (a :: k). Order a a
EQ
compareAtoms FreeCartesian cat con a b
P1 FreeCartesian cat con a c
_ = forall {k} (a :: k) (b :: k). Order a b
LT
compareAtoms FreeCartesian cat con a b
_ FreeCartesian cat con a c
P1 = forall {k} (a :: k) (b :: k). Order a b
GT
compareAtoms FreeCartesian cat con a b
P2 FreeCartesian cat con a c
_ = forall {k} (a :: k) (b :: k). Order a b
LT
compareAtoms FreeCartesian cat con a b
_ FreeCartesian cat con a c
P2 = forall {k} (a :: k) (b :: k). Order a b
GT
compareAtoms (Embed cat a b
_) FreeCartesian cat con a c
_ = forall {k} (a :: k) (b :: k). Order a b
LT
compareAtoms FreeCartesian cat con a b
_ (Embed cat a c
_) = forall {k} (a :: k) (b :: k). Order a b
GT
compareAtoms FreeCartesian cat con a b
E FreeCartesian cat con a c
_ = forall {k} (a :: k) (b :: k). Order a b
LT
compareAtoms FreeCartesian cat con a b
_ FreeCartesian cat con a c
E = forall {k} (a :: k) (b :: k). Order a b
GT
compareAtoms FreeCartesian cat con a b
f FreeCartesian cat con a c
g = forall a. HasCallStack => [Char] -> a
error ([Char]
"compareAtoms:\n" forall a. [a] -> [a] -> [a]
++ forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
Int -> Cat k con a b -> ShowS
showDbg Int
0 FreeCartesian cat con a b
f [Char]
"\n" forall a. [a] -> [a] -> [a]
++ forall (k :: * -> * -> *) (con :: * -> Constraint) a b.
Int -> Cat k con a b -> ShowS
showDbg Int
0 FreeCartesian cat con a c
g [Char]
"" )