module Darcs.Patch.CommuteFn
    ( CommuteFn,
      commuterIdFL, commuterFLId,
      commuterIdRL, commuterRLId,
      commuterRLFL,
      MergeFn,
      PartialMergeFn,
      mergerIdFL,
      TotalCommuteFn,
      totalCommuterIdFL, totalCommuterFLId, totalCommuterFLFL,
      invertCommuter
    ) where

import Darcs.Prelude

import Darcs.Patch.Invert ( Invert(..) )
import Darcs.Patch.Witnesses.Ordered
    ( (:>)(..)
    , (:\/:)(..)
    , (:/\:)(..)
    , FL(..)
    , RL(..)
    )

-- |CommuteFn is the basis of a general framework for building up commutation
-- operations between different patch types in a generic manner. Unfortunately
-- type classes are not well suited to the problem because of the multiple possible
-- routes by which the commuter for (FL p1, FL p2) can be built out of the
-- commuter for (p1, p2) - and more complicated problems when we start building
-- multiple constructors on top of each other. The type class resolution machinery
-- really can't cope with selecting some route, because it doesn't know that all
-- possible routes should be equivalent.
--
-- Note that a CommuteFn cannot be lazy i.e. commute patches only when the
-- resulting sequences are demanded. This is because of the possibility of
-- failure ('Nothing'): all the commutes must be performed before we can know
-- whether the overall commute succeeds.
type CommuteFn p1 p2 = forall wX wY . (p1 :> p2) wX wY -> Maybe ((p2 :> p1) wX wY)

type TotalCommuteFn p1 p2 = forall wX wY . (p1 :> p2) wX wY -> (p2 :> p1) wX wY

type MergeFn p1 p2 = forall wX wY . (p1 :\/: p2) wX wY -> (p2 :/\: p1) wX wY

type PartialMergeFn p1 p2 = forall wX wY . (p1 :\/: p2) wX wY -> Maybe ((p2 :/\: p1) wX wY)

commuterIdRL :: CommuteFn p1 p2 -> CommuteFn p1 (RL p2)
commuterIdRL :: CommuteFn p1 p2 -> CommuteFn p1 (RL p2)
commuterIdRL CommuteFn p1 p2
_ (p1 wX wZ
x :> RL p2 wZ wY
NilRL) = (:>) (RL p2) p1 wX wZ -> Maybe ((:>) (RL p2) p1 wX wZ)
forall (m :: * -> *) a. Monad m => a -> m a
return (RL p2 wX wX
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL RL p2 wX wX -> p1 wX wZ -> (:>) (RL p2) p1 wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p1 wX wZ
x)
commuterIdRL CommuteFn p1 p2
commuter (p1 wX wZ
x :> (RL p2 wZ wY
ys :<: p2 wY wY
y))
  = do RL p2 wX wZ
ys' :> p1 wZ wY
x' <- CommuteFn p1 p2
-> (:>) p1 (RL p2) wX wY -> Maybe ((:>) (RL p2) p1 wX wY)
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn p1 (RL p2)
commuterIdRL CommuteFn p1 p2
commuter (p1 wX wZ
x p1 wX wZ -> RL p2 wZ wY -> (:>) p1 (RL p2) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p2 wZ wY
ys)
       p2 wZ wZ
y' :> p1 wZ wY
x'' <- (:>) p1 p2 wZ wY -> Maybe ((:>) p2 p1 wZ wY)
CommuteFn p1 p2
commuter (p1 wZ wY
x' p1 wZ wY -> p2 wY wY -> (:>) p1 p2 wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wY wY
y)
       (:>) (RL p2) p1 wX wY -> Maybe ((:>) (RL p2) p1 wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return ((RL p2 wX wZ
ys' RL p2 wX wZ -> p2 wZ wZ -> RL p2 wX wZ
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p2 wZ wZ
y') RL p2 wX wZ -> p1 wZ wY -> (:>) (RL p2) p1 wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p1 wZ wY
x'')

commuterIdFL :: CommuteFn p1 p2 -> CommuteFn p1 (FL p2)
commuterIdFL :: CommuteFn p1 p2 -> CommuteFn p1 (FL p2)
commuterIdFL CommuteFn p1 p2
_ (p1 wX wZ
x :> FL p2 wZ wY
NilFL) = (:>) (FL p2) p1 wX wZ -> Maybe ((:>) (FL p2) p1 wX wZ)
forall (m :: * -> *) a. Monad m => a -> m a
return (FL p2 wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL p2 wX wX -> p1 wX wZ -> (:>) (FL p2) p1 wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p1 wX wZ
x)
commuterIdFL CommuteFn p1 p2
commuter (p1 wX wZ
x :> (p2 wZ wY
y :>: FL p2 wY wY
ys))
  = do p2 wX wZ
y' :> p1 wZ wY
x' <- (:>) p1 p2 wX wY -> Maybe ((:>) p2 p1 wX wY)
CommuteFn p1 p2
commuter (p1 wX wZ
x p1 wX wZ -> p2 wZ wY -> (:>) p1 p2 wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wZ wY
y)
       FL p2 wZ wZ
ys' :> p1 wZ wY
x'' <- CommuteFn p1 p2
-> (:>) p1 (FL p2) wZ wY -> Maybe ((:>) (FL p2) p1 wZ wY)
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn p1 (FL p2)
commuterIdFL CommuteFn p1 p2
commuter (p1 wZ wY
x' p1 wZ wY -> FL p2 wY wY -> (:>) p1 (FL p2) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p2 wY wY
ys)
       (:>) (FL p2) p1 wX wY -> Maybe ((:>) (FL p2) p1 wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return ((p2 wX wZ
y' p2 wX wZ -> FL p2 wZ wZ -> FL p2 wX wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p2 wZ wZ
ys') FL p2 wX wZ -> p1 wZ wY -> (:>) (FL p2) p1 wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p1 wZ wY
x'')

-- | TODO document laziness or lack thereof
mergerIdFL :: MergeFn p1 p2 -> MergeFn p1 (FL p2)
mergerIdFL :: MergeFn p1 p2 -> MergeFn p1 (FL p2)
mergerIdFL MergeFn p1 p2
_ (p1 wZ wX
x :\/: FL p2 wZ wY
NilFL) = FL p2 wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL p2 wX wX -> p1 wZ wX -> (:/\:) (FL p2) p1 wX wZ
forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\: p1 wZ wX
x
mergerIdFL MergeFn p1 p2
merger (p1 wZ wX
x :\/: (p2 wZ wY
y :>: FL p2 wY wY
ys))
  = case (:\/:) p1 p2 wX wY -> (:/\:) p2 p1 wX wY
MergeFn p1 p2
merger (p1 wZ wX
x p1 wZ wX -> p2 wZ wY -> (:\/:) p1 p2 wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: p2 wZ wY
y) of
      p2 wX wZ
y' :/\: p1 wY wZ
x' -> case MergeFn p1 p2 -> (:\/:) p1 (FL p2) wZ wY -> (:/\:) (FL p2) p1 wZ wY
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
MergeFn p1 p2 -> MergeFn p1 (FL p2)
mergerIdFL MergeFn p1 p2
merger (p1 wY wZ
x' p1 wY wZ -> FL p2 wY wY -> (:\/:) p1 (FL p2) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: FL p2 wY wY
ys) of
          FL p2 wZ wZ
ys' :/\: p1 wY wZ
x'' -> (p2 wX wZ
y' p2 wX wZ -> FL p2 wZ wZ -> FL p2 wX wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p2 wZ wZ
ys') FL p2 wX wZ -> p1 wY wZ -> (:/\:) (FL p2) p1 wX wY
forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\: p1 wY wZ
x''

-- | TODO document laziness or lack thereof
totalCommuterIdFL :: TotalCommuteFn p1 p2 -> TotalCommuteFn p1 (FL p2)
totalCommuterIdFL :: TotalCommuteFn p1 p2 -> TotalCommuteFn p1 (FL p2)
totalCommuterIdFL TotalCommuteFn p1 p2
_ (p1 wX wZ
x :> FL p2 wZ wY
NilFL) = FL p2 wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL p2 wX wX -> p1 wX wZ -> (:>) (FL p2) p1 wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p1 wX wZ
x
totalCommuterIdFL TotalCommuteFn p1 p2
commuter (p1 wX wZ
x :> (p2 wZ wY
y :>: FL p2 wY wY
ys)) =
   case (:>) p1 p2 wX wY -> (:>) p2 p1 wX wY
TotalCommuteFn p1 p2
commuter (p1 wX wZ
x p1 wX wZ -> p2 wZ wY -> (:>) p1 p2 wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wZ wY
y) of
     p2 wX wZ
y' :> p1 wZ wY
x' -> case TotalCommuteFn p1 p2
-> (:>) p1 (FL p2) wZ wY -> (:>) (FL p2) p1 wZ wY
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
TotalCommuteFn p1 p2 -> TotalCommuteFn p1 (FL p2)
totalCommuterIdFL TotalCommuteFn p1 p2
commuter (p1 wZ wY
x' p1 wZ wY -> FL p2 wY wY -> (:>) p1 (FL p2) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p2 wY wY
ys) of
                   FL p2 wZ wZ
ys' :> p1 wZ wY
x'' -> (p2 wX wZ
y' p2 wX wZ -> FL p2 wZ wZ -> FL p2 wX wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p2 wZ wZ
ys') FL p2 wX wZ -> p1 wZ wY -> (:>) (FL p2) p1 wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p1 wZ wY
x''

commuterFLId :: CommuteFn p1 p2 -> CommuteFn (FL p1) p2
commuterFLId :: CommuteFn p1 p2 -> CommuteFn (FL p1) p2
commuterFLId CommuteFn p1 p2
_ (FL p1 wX wZ
NilFL :> p2 wZ wY
y) = (:>) p2 (FL p1) wZ wY -> Maybe ((:>) p2 (FL p1) wZ wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (p2 wZ wY
y p2 wZ wY -> FL p1 wY wY -> (:>) p2 (FL p1) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p1 wY wY
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)
commuterFLId CommuteFn p1 p2
commuter ((p1 wX wY
x :>: FL p1 wY wZ
xs) :> p2 wZ wY
y)
  = do p2 wY wZ
y' :> FL p1 wZ wY
xs' <- CommuteFn p1 p2
-> (:>) (FL p1) p2 wY wY -> Maybe ((:>) p2 (FL p1) wY wY)
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn (FL p1) p2
commuterFLId CommuteFn p1 p2
commuter (FL p1 wY wZ
xs FL p1 wY wZ -> p2 wZ wY -> (:>) (FL p1) p2 wY wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wZ wY
y)
       p2 wX wZ
y'' :> p1 wZ wZ
x' <- (:>) p1 p2 wX wZ -> Maybe ((:>) p2 p1 wX wZ)
CommuteFn p1 p2
commuter (p1 wX wY
x p1 wX wY -> p2 wY wZ -> (:>) p1 p2 wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wY wZ
y')
       (:>) p2 (FL p1) wX wY -> Maybe ((:>) p2 (FL p1) wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (p2 wX wZ
y'' p2 wX wZ -> FL p1 wZ wY -> (:>) p2 (FL p1) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (p1 wZ wZ
x' p1 wZ wZ -> FL p1 wZ wY -> FL p1 wZ wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p1 wZ wY
xs'))

commuterRLId :: CommuteFn p1 p2 -> CommuteFn (RL p1) p2
commuterRLId :: CommuteFn p1 p2 -> CommuteFn (RL p1) p2
commuterRLId CommuteFn p1 p2
_ (RL p1 wX wZ
NilRL :> p2 wZ wY
y) = (:>) p2 (RL p1) wZ wY -> Maybe ((:>) p2 (RL p1) wZ wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (p2 wZ wY
y p2 wZ wY -> RL p1 wY wY -> (:>) p2 (RL p1) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p1 wY wY
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL)
commuterRLId CommuteFn p1 p2
commuter ((RL p1 wX wY
xs :<: p1 wY wZ
x) :> p2 wZ wY
y)
  = do p2 wY wZ
y' :> p1 wZ wY
x' <- (:>) p1 p2 wY wY -> Maybe ((:>) p2 p1 wY wY)
CommuteFn p1 p2
commuter (p1 wY wZ
x p1 wY wZ -> p2 wZ wY -> (:>) p1 p2 wY wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wZ wY
y)
       p2 wX wZ
y'' :> RL p1 wZ wZ
xs' <- CommuteFn p1 p2
-> (:>) (RL p1) p2 wX wZ -> Maybe ((:>) p2 (RL p1) wX wZ)
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn (RL p1) p2
commuterRLId CommuteFn p1 p2
commuter (RL p1 wX wY
xs RL p1 wX wY -> p2 wY wZ -> (:>) (RL p1) p2 wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wY wZ
y')
       (:>) p2 (RL p1) wX wY -> Maybe ((:>) p2 (RL p1) wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (p2 wX wZ
y'' p2 wX wZ -> RL p1 wZ wY -> (:>) p2 (RL p1) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (RL p1 wZ wZ
xs' RL p1 wZ wZ -> p1 wZ wY -> RL p1 wZ wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p1 wZ wY
x'))

commuterRLFL :: forall p1 p2. CommuteFn p1 p2 -> CommuteFn (RL p1) (FL p2)
commuterRLFL :: CommuteFn p1 p2 -> CommuteFn (RL p1) (FL p2)
commuterRLFL CommuteFn p1 p2
commuter (RL p1 wX wZ
xs :> FL p2 wZ wY
ys) = RL p1 wX wZ -> FL p2 wZ wY -> Maybe ((:>) (FL p2) (RL p1) wX wY)
forall wX wY wZ.
RL p1 wX wY -> FL p2 wY wZ -> Maybe ((:>) (FL p2) (RL p1) wX wZ)
right RL p1 wX wZ
xs FL p2 wZ wY
ys
  where
    right :: RL p1 wX wY -> FL p2 wY wZ -> Maybe ((FL p2 :> RL p1) wX wZ)
    right :: RL p1 wX wY -> FL p2 wY wZ -> Maybe ((:>) (FL p2) (RL p1) wX wZ)
right RL p1 wX wY
as FL p2 wY wZ
NilFL = (:>) (FL p2) (RL p1) wX wY -> Maybe ((:>) (FL p2) (RL p1) wX wY)
forall a. a -> Maybe a
Just (FL p2 wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL p2 wX wX -> RL p1 wX wY -> (:>) (FL p2) (RL p1) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p1 wX wY
as)
    right RL p1 wX wY
as (p2 wY wY
b :>: FL p2 wY wZ
bs) = do
      p2 wX wZ
b' :> RL p1 wZ wY
as' <- CommuteFn p1 p2
-> (:>) (RL p1) p2 wX wY -> Maybe ((:>) p2 (RL p1) wX wY)
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn (RL p1) p2
commuterRLId CommuteFn p1 p2
commuter (RL p1 wX wY
as RL p1 wX wY -> p2 wY wY -> (:>) (RL p1) p2 wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wY wY
b)
      FL p2 wZ wZ
bs' :> RL p1 wZ wZ
as'' <- RL p1 wZ wY -> FL p2 wY wZ -> Maybe ((:>) (FL p2) (RL p1) wZ wZ)
forall wX wY wZ.
RL p1 wX wY -> FL p2 wY wZ -> Maybe ((:>) (FL p2) (RL p1) wX wZ)
left RL p1 wZ wY
as' FL p2 wY wZ
bs
      (:>) (FL p2) (RL p1) wX wZ -> Maybe ((:>) (FL p2) (RL p1) wX wZ)
forall (m :: * -> *) a. Monad m => a -> m a
return (p2 wX wZ
b' p2 wX wZ -> FL p2 wZ wZ -> FL p2 wX wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p2 wZ wZ
bs' FL p2 wX wZ -> RL p1 wZ wZ -> (:>) (FL p2) (RL p1) wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p1 wZ wZ
as'')
    left :: RL p1 wX wY -> FL p2 wY wZ -> Maybe ((FL p2 :> RL p1) wX wZ)
    left :: RL p1 wX wY -> FL p2 wY wZ -> Maybe ((:>) (FL p2) (RL p1) wX wZ)
left RL p1 wX wY
NilRL FL p2 wY wZ
bs = (:>) (FL p2) (RL p1) wY wZ -> Maybe ((:>) (FL p2) (RL p1) wY wZ)
forall a. a -> Maybe a
Just (FL p2 wY wZ
bs FL p2 wY wZ -> RL p1 wZ wZ -> (:>) (FL p2) (RL p1) wY wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p1 wZ wZ
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL)
    left (RL p1 wX wY
as :<: p1 wY wY
a) FL p2 wY wZ
bs = do
      FL p2 wY wZ
bs' :> p1 wZ wZ
a' <- CommuteFn p1 p2
-> (:>) p1 (FL p2) wY wZ -> Maybe ((:>) (FL p2) p1 wY wZ)
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn p1 (FL p2)
commuterIdFL CommuteFn p1 p2
commuter (p1 wY wY
a p1 wY wY -> FL p2 wY wZ -> (:>) p1 (FL p2) wY wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p2 wY wZ
bs)
      FL p2 wX wZ
bs'' :> RL p1 wZ wZ
as' <- RL p1 wX wY -> FL p2 wY wZ -> Maybe ((:>) (FL p2) (RL p1) wX wZ)
forall wX wY wZ.
RL p1 wX wY -> FL p2 wY wZ -> Maybe ((:>) (FL p2) (RL p1) wX wZ)
right RL p1 wX wY
as FL p2 wY wZ
bs'
      (:>) (FL p2) (RL p1) wX wZ -> Maybe ((:>) (FL p2) (RL p1) wX wZ)
forall (m :: * -> *) a. Monad m => a -> m a
return (FL p2 wX wZ
bs'' FL p2 wX wZ -> RL p1 wZ wZ -> (:>) (FL p2) (RL p1) wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p1 wZ wZ
as' RL p1 wZ wZ -> p1 wZ wZ -> RL p1 wZ wZ
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p1 wZ wZ
a')

-- | TODO document laziness or lack thereof
totalCommuterFLId :: TotalCommuteFn p1 p2 -> TotalCommuteFn (FL p1) p2
totalCommuterFLId :: TotalCommuteFn p1 p2 -> TotalCommuteFn (FL p1) p2
totalCommuterFLId TotalCommuteFn p1 p2
_ (FL p1 wX wZ
NilFL :> p2 wZ wY
y) = p2 wZ wY
y p2 wZ wY -> FL p1 wY wY -> (:>) p2 (FL p1) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p1 wY wY
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
totalCommuterFLId TotalCommuteFn p1 p2
commuter ((p1 wX wY
x :>: FL p1 wY wZ
xs) :> p2 wZ wY
y) =
   case TotalCommuteFn p1 p2
-> (:>) (FL p1) p2 wY wY -> (:>) p2 (FL p1) wY wY
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
TotalCommuteFn p1 p2 -> TotalCommuteFn (FL p1) p2
totalCommuterFLId TotalCommuteFn p1 p2
commuter (FL p1 wY wZ
xs FL p1 wY wZ -> p2 wZ wY -> (:>) (FL p1) p2 wY wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wZ wY
y) of
     p2 wY wZ
y' :> FL p1 wZ wY
xs' -> case (:>) p1 p2 wX wZ -> (:>) p2 p1 wX wZ
TotalCommuteFn p1 p2
commuter (p1 wX wY
x p1 wX wY -> p2 wY wZ -> (:>) p1 p2 wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wY wZ
y') of
                    p2 wX wZ
y'' :> p1 wZ wZ
x' -> p2 wX wZ
y'' p2 wX wZ -> FL p1 wZ wY -> (:>) p2 (FL p1) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (p1 wZ wZ
x' p1 wZ wZ -> FL p1 wZ wY -> FL p1 wZ wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p1 wZ wY
xs')

-- | TODO document laziness or lack thereof
totalCommuterFLFL :: TotalCommuteFn p1 p2 -> TotalCommuteFn (FL p1) (FL p2)
totalCommuterFLFL :: TotalCommuteFn p1 p2 -> TotalCommuteFn (FL p1) (FL p2)
totalCommuterFLFL TotalCommuteFn p1 p2
commuter = TotalCommuteFn p1 (FL p2) -> TotalCommuteFn (FL p1) (FL p2)
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
TotalCommuteFn p1 p2 -> TotalCommuteFn (FL p1) p2
totalCommuterFLId (TotalCommuteFn p1 p2 -> TotalCommuteFn p1 (FL p2)
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
TotalCommuteFn p1 p2 -> TotalCommuteFn p1 (FL p2)
totalCommuterIdFL TotalCommuteFn p1 p2
commuter)

-- | Make use of the inverse-commute law to reduce the number of cases
-- when defining commute for complicated patch types.
{-# INLINE invertCommuter #-}
invertCommuter :: (Invert p, Invert q) => CommuteFn p q -> CommuteFn q p
invertCommuter :: CommuteFn p q -> CommuteFn q p
invertCommuter CommuteFn p q
commuter (q wX wZ
x :> p wZ wY
y) = do
    q wY wZ
ix' :> p wZ wX
iy' <- (:>) p q wY wX -> Maybe ((:>) q p wY wX)
CommuteFn p q
commuter (p wZ wY -> p wY wZ
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wZ wY
y p wY wZ -> q wZ wX -> (:>) p q wY wX
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> q wX wZ -> q wZ wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert q wX wZ
x)
    (:>) p q wX wY -> Maybe ((:>) p q wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (p wZ wX -> p wX wZ
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wZ wX
iy' p wX wZ -> q wZ wY -> (:>) p q wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> q wY wZ -> q wZ wY
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert q wY wZ
ix')