module Darcs.Patch.Unwind
( Unwind(..)
, Unwound(..)
, mkUnwound
, squashUnwound
) where
import Darcs.Prelude
import Darcs.Patch.Commute
( Commute, commute, selfCommuter
)
import Darcs.Patch.CommuteFn
( commuterIdFL, commuterFLId
)
import Darcs.Patch.Format ( PatchListFormat )
import Darcs.Patch.FromPrim ( PrimOf )
import Darcs.Patch.Invert
( Invert(..), invertFL, invertRL
)
import Darcs.Patch.Show ( ShowPatchBasic(..) )
import Darcs.Patch.Viewing ()
import Darcs.Patch.Witnesses.Eq ( EqCheck(..), Eq2(..) )
import Darcs.Patch.Witnesses.Maybe ( Maybe2(..) )
import Darcs.Patch.Witnesses.Ordered
( FL(..), (:>)(..), (+>+), reverseFL
, RL(..), (+<+), reverseRL
)
import Darcs.Patch.Witnesses.Show ( Show1, Show2, show2 )
import Darcs.Util.Printer ( blueText, vcat )
data Unwound prim wX wY where
Unwound
:: FL prim wA wB
-> FL prim wB wC
-> RL prim wC wD
-> Unwound prim wA wD
deriving instance Show2 prim => Show (Unwound prim wX wY)
instance Show2 prim => Show1 (Unwound prim wX)
instance Show2 prim => Show2 (Unwound prim)
instance (PatchListFormat prim, ShowPatchBasic prim)
=> ShowPatchBasic (Unwound prim) where
showPatch :: forall wX wY. ShowPatchFor -> Unwound prim wX wY -> Doc
showPatch ShowPatchFor
f (Unwound FL prim wX wB
before FL prim wB wC
prims RL prim wC wY
after) =
[Doc] -> Doc
vcat [
String -> Doc
blueText String
"before:",
forall (p :: * -> * -> *) wX wY.
ShowPatchBasic p =>
ShowPatchFor -> p wX wY -> Doc
showPatch ShowPatchFor
f FL prim wX wB
before,
String -> Doc
blueText String
"prims:",
forall (p :: * -> * -> *) wX wY.
ShowPatchBasic p =>
ShowPatchFor -> p wX wY -> Doc
showPatch ShowPatchFor
f FL prim wB wC
prims,
String -> Doc
blueText String
"after:",
forall (p :: * -> * -> *) wX wY.
ShowPatchBasic p =>
ShowPatchFor -> p wX wY -> Doc
showPatch ShowPatchFor
f RL prim wC wY
after
]
instance Invert prim => Invert (Unwound prim) where
invert :: forall wX wY. Unwound prim wX wY -> Unwound prim wY wX
invert (Unwound FL prim wX wB
before FL prim wB wC
prim RL prim wC wY
after)
= forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound (forall (p :: * -> * -> *) wX wY.
Invert p =>
RL p wX wY -> FL p wY wX
invertRL RL prim wC wY
after) (forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert FL prim wB wC
prim) (forall (p :: * -> * -> *) wX wY.
Invert p =>
FL p wX wY -> RL p wY wX
invertFL FL prim wX wB
before)
class Unwind p where
fullUnwind :: p wX wY -> Unwound (PrimOf p) wX wY
mkUnwound
:: (Commute prim, Invert prim, Eq2 prim)
=> FL prim wA wB
-> FL prim wB wC
-> FL prim wC wD
-> Unwound prim wA wD
mkUnwound :: forall (prim :: * -> * -> *) wA wB wC wD.
(Commute prim, Invert prim, Eq2 prim) =>
FL prim wA wB
-> FL prim wB wC -> FL prim wC wD -> Unwound prim wA wD
mkUnwound FL prim wA wB
before FL prim wB wC
ps FL prim wC wD
after =
forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
FL prim wA wB -> Unwound prim wB wC -> Unwound prim wA wC
consBefores FL prim wA wB
before forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> FL prim wB wC -> Unwound prim wA wC
consAfters FL prim wC wD
after forall a b. (a -> b) -> a -> b
$
forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL prim wB wC
ps forall (a :: * -> * -> *) wX. RL a wX wX
NilRL
consBefores
:: (Commute prim, Invert prim, Eq2 prim)
=> FL prim wA wB
-> Unwound prim wB wC
-> Unwound prim wA wC
consBefores :: forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
FL prim wA wB -> Unwound prim wB wC -> Unwound prim wA wC
consBefores FL prim wA wB
NilFL Unwound prim wB wC
u = Unwound prim wB wC
u
consBefores (prim wA wY
b :>: FL prim wY wB
bs) Unwound prim wB wC
u = forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
prim wA wB -> Unwound prim wB wC -> Unwound prim wA wC
consBefore prim wA wY
b (forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
FL prim wA wB -> Unwound prim wB wC -> Unwound prim wA wC
consBefores FL prim wY wB
bs Unwound prim wB wC
u)
consAfters
:: (Commute prim, Invert prim, Eq2 prim)
=> Unwound prim wA wB
-> FL prim wB wC
-> Unwound prim wA wC
consAfters :: forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> FL prim wB wC -> Unwound prim wA wC
consAfters Unwound prim wA wB
u FL prim wB wC
NilFL = Unwound prim wA wB
u
consAfters Unwound prim wA wB
u (prim wB wY
a :>: FL prim wY wC
as) = forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> FL prim wB wC -> Unwound prim wA wC
consAfters (forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> prim wB wC -> Unwound prim wA wC
consAfter Unwound prim wA wB
u prim wB wY
a) FL prim wY wC
as
consBefore
:: (Commute prim, Invert prim, Eq2 prim)
=> prim wA wB
-> Unwound prim wB wC
-> Unwound prim wA wC
consBefore :: forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
prim wA wB -> Unwound prim wB wC -> Unwound prim wA wC
consBefore prim wA wB
b (Unwound FL prim wB wB
NilFL FL prim wB wC
ps RL prim wC wC
after) =
case forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn p1 (FL p2)
commuterIdFL forall (p :: * -> * -> *). Commute p => CommuteFn p p
selfCommuter (prim wA wB
b forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL prim wB wC
ps) of
Maybe ((:>) (FL prim) prim wA wC)
Nothing -> forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound (prim wA wB
b forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: forall (a :: * -> * -> *) wX. FL a wX wX
NilFL) FL prim wB wC
ps RL prim wC wC
after
Just (FL prim wA wZ
ps' :> prim wZ wC
b') -> forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL prim wA wZ
ps' (forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
(:>) (RL prim) (prim :> FL prim) wA wB -> RL prim wA wB
propagateAfter (forall (a :: * -> * -> *) wX. RL a wX wX
NilRL forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wC
b' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL prim wC wC
after))
consBefore prim wA wB
b1 (Unwound (prim wB wY
b2 :>: FL prim wY wB
bs) FL prim wB wC
ps RL prim wC wC
after)
| EqCheck wA wY
IsEq <- forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert prim wA wB
b1 forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= prim wB wY
b2 = forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wY wB
bs FL prim wB wC
ps RL prim wC wC
after
| Just (prim wA wZ
b2' :> prim wZ wY
b1') <- forall (p :: * -> * -> *). Commute p => CommuteFn p p
commute (prim wA wB
b1 forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wB wY
b2)
= case forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
prim wA wB -> Unwound prim wB wC -> Unwound prim wA wC
consBefore prim wZ wY
b1' (forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wY wB
bs FL prim wB wC
ps RL prim wC wC
after) of
Unwound FL prim wZ wB
bs' FL prim wB wC
ps' RL prim wC wC
after' -> forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound (prim wA wZ
b2' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL prim wZ wB
bs') FL prim wB wC
ps' RL prim wC wC
after'
consBefore prim wA wB
b (Unwound FL prim wB wB
bs FL prim wB wC
ps RL prim wC wC
after) = forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound (prim wA wB
b forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL prim wB wB
bs) FL prim wB wC
ps RL prim wC wC
after
consAfter
:: (Commute prim, Invert prim, Eq2 prim)
=> Unwound prim wA wB
-> prim wB wC
-> Unwound prim wA wC
consAfter :: forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> prim wB wC -> Unwound prim wA wC
consAfter (Unwound FL prim wA wB
before FL prim wB wC
ps RL prim wC wB
NilRL) prim wB wC
a =
case forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn (FL p1) p2
commuterFLId forall (p :: * -> * -> *). Commute p => CommuteFn p p
selfCommuter (FL prim wB wC
ps forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wB wC
a) of
Maybe ((:>) prim (FL prim) wB wC)
Nothing -> forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wA wB
before FL prim wB wC
ps (forall (a :: * -> * -> *) wX. RL a wX wX
NilRL forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: prim wB wC
a)
Just (prim wB wZ
a' :> FL prim wZ wC
ps') -> forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound (forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
(:>) (RL prim) (prim :> FL prim) wA wB -> FL prim wA wB
propagateBefore (forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> RL a wX wZ
reverseFL FL prim wA wB
before forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wB wZ
a' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)) FL prim wZ wC
ps' forall (a :: * -> * -> *) wX. RL a wX wX
NilRL
consAfter (Unwound FL prim wA wB
before FL prim wB wC
ps (RL prim wC wY
as :<: prim wY wB
a1)) prim wB wC
a2
| EqCheck wY wC
IsEq <- forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert prim wY wB
a1 forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= prim wB wC
a2 = forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wA wB
before FL prim wB wC
ps RL prim wC wY
as
| Just (prim wY wZ
a2' :> prim wZ wC
a1') <- forall (p :: * -> * -> *). Commute p => CommuteFn p p
commute (prim wY wB
a1 forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wB wC
a2)
= case forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> prim wB wC -> Unwound prim wA wC
consAfter (forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wA wB
before FL prim wB wC
ps RL prim wC wY
as) prim wY wZ
a2' of
Unwound FL prim wA wB
before' FL prim wB wC
ps' RL prim wC wZ
as' -> forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wA wB
before' FL prim wB wC
ps' (RL prim wC wZ
as' forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: prim wZ wC
a1')
consAfter (Unwound FL prim wA wB
before FL prim wB wC
ps RL prim wC wB
as) prim wB wC
a = forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wA wB
before FL prim wB wC
ps (RL prim wC wB
as forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: prim wB wC
a)
propagateBefore
:: (Commute prim, Invert prim, Eq2 prim)
=> (RL prim :> prim :> FL prim) wA wB
-> FL prim wA wB
propagateBefore :: forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
(:>) (RL prim) (prim :> FL prim) wA wB -> FL prim wA wB
propagateBefore (RL prim wA wZ
NilRL :> prim wZ wZ
p :> FL prim wZ wB
acc) = prim wZ wZ
p forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL prim wZ wB
acc
propagateBefore (RL prim wA wY
qs :<: prim wY wZ
q :> prim wZ wZ
p :> FL prim wZ wB
acc)
| EqCheck wY wZ
IsEq <- forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert prim wY wZ
q forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= prim wZ wZ
p = forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL prim wA wY
qs forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL prim wZ wB
acc
| Just (prim wY wZ
p' :> prim wZ wZ
q') <- forall (p :: * -> * -> *). Commute p => CommuteFn p p
commute (prim wY wZ
q forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wZ
p)
= forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
(:>) (RL prim) (prim :> FL prim) wA wB -> FL prim wA wB
propagateBefore (RL prim wA wY
qs forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wY wZ
p' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wZ
q' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL prim wZ wB
acc)
| Bool
otherwise = forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL prim wA wY
qs forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ prim wY wZ
q forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: prim wZ wZ
p forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL prim wZ wB
acc
propagateAfter
:: (Commute prim, Invert prim, Eq2 prim)
=> (RL prim :> prim :> FL prim) wA wB
-> RL prim wA wB
propagateAfter :: forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
(:>) (RL prim) (prim :> FL prim) wA wB -> RL prim wA wB
propagateAfter (RL prim wA wZ
acc :> prim wZ wZ
p :> FL prim wZ wB
NilFL) = RL prim wA wZ
acc forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: prim wZ wZ
p
propagateAfter (RL prim wA wZ
acc :> prim wZ wZ
p :> prim wZ wY
q :>: FL prim wY wB
qs)
| EqCheck wZ wY
IsEq <- forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert prim wZ wZ
p forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= prim wZ wY
q = RL prim wA wZ
acc forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> RL a wY wZ -> RL a wX wZ
+<+ forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> RL a wX wZ
reverseFL FL prim wY wB
qs
| Just (prim wZ wZ
q' :> prim wZ wY
p') <- forall (p :: * -> * -> *). Commute p => CommuteFn p p
commute (prim wZ wZ
p forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wY
q)
= forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
(:>) (RL prim) (prim :> FL prim) wA wB -> RL prim wA wB
propagateAfter (RL prim wA wZ
acc forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: prim wZ wZ
q' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wY
p' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL prim wY wB
qs)
| Bool
otherwise = RL prim wA wZ
acc forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: prim wZ wZ
p forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: prim wZ wY
q forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> RL a wY wZ -> RL a wX wZ
+<+ forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> RL a wX wZ
reverseFL FL prim wY wB
qs
squashUnwound
:: (Show2 prim, Commute prim, Eq2 prim, Invert prim)
=> FL (Unwound prim) wX wY
-> Unwound prim wX wY
squashUnwound :: forall (prim :: * -> * -> *) wX wY.
(Show2 prim, Commute prim, Eq2 prim, Invert prim) =>
FL (Unwound prim) wX wY -> Unwound prim wX wY
squashUnwound FL (Unwound prim) wX wY
NilFL = forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound forall (a :: * -> * -> *) wX. FL a wX wX
NilFL forall (a :: * -> * -> *) wX. FL a wX wX
NilFL forall (a :: * -> * -> *) wX. RL a wX wX
NilRL
squashUnwound (Unwound prim wX wY
u :>: FL (Unwound prim) wY wY
us) =
forall (prim :: * -> * -> *) wX wY.
(Show2 prim, Commute prim, Eq2 prim, Invert prim) =>
(:>) (Unwound prim) (Unwound prim) wX wY -> Unwound prim wX wY
squashPair (forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> Unwound prim wA wB
moveCommutingToBefore Unwound prim wX wY
u forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> Unwound prim wA wB
moveCommutingToAfter (forall (prim :: * -> * -> *) wX wY.
(Show2 prim, Commute prim, Eq2 prim, Invert prim) =>
FL (Unwound prim) wX wY -> Unwound prim wX wY
squashUnwound FL (Unwound prim) wY wY
us))
moveCommutingToBefore
:: (Commute prim, Invert prim, Eq2 prim)
=> Unwound prim wA wB
-> Unwound prim wA wB
moveCommutingToBefore :: forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> Unwound prim wA wB
moveCommutingToBefore (Unwound FL prim wA wB
before FL prim wB wC
ps RL prim wC wB
after) =
forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> FL prim wB wC -> Unwound prim wA wC
consAfters (forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL prim wC wB
after) forall a b. (a -> b) -> a -> b
$
forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wA wB
before FL prim wB wC
ps forall (a :: * -> * -> *) wX. RL a wX wX
NilRL
moveCommutingToAfter
:: (Commute prim, Invert prim, Eq2 prim)
=> Unwound prim wA wB
-> Unwound prim wA wB
moveCommutingToAfter :: forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> Unwound prim wA wB
moveCommutingToAfter (Unwound FL prim wA wB
before FL prim wB wC
ps RL prim wC wB
after) =
forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
FL prim wA wB -> Unwound prim wB wC -> Unwound prim wA wC
consBefores FL prim wA wB
before forall a b. (a -> b) -> a -> b
$
forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL prim wB wC
ps RL prim wC wB
after
squashPair
:: (Show2 prim, Commute prim, Eq2 prim, Invert prim)
=> (Unwound prim :> Unwound prim) wX wY
-> Unwound prim wX wY
squashPair :: forall (prim :: * -> * -> *) wX wY.
(Show2 prim, Commute prim, Eq2 prim, Invert prim) =>
(:>) (Unwound prim) (Unwound prim) wX wY -> Unwound prim wX wY
squashPair (Unwound FL prim wX wB
before FL prim wB wC
ps1 RL prim wC wZ
NilRL :> Unwound FL prim wZ wB
NilFL FL prim wB wC
ps2 RL prim wC wY
after) =
forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wX wB
before (FL prim wB wC
ps1 forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL prim wB wC
ps2) RL prim wC wY
after
squashPair (Unwound FL prim wX wB
before1 FL prim wB wC
ps1 (RL prim wC wY
after1 :<: prim wY wZ
a) :> Unwound FL prim wZ wB
before2 FL prim wB wC
ps2 RL prim wC wY
after2) =
case forall (prim :: * -> * -> *) wX wY.
(Show2 prim, Commute prim, Eq2 prim, Invert prim) =>
(:>) prim (FL prim) wX wY -> (:>) (FL prim) (Maybe2 prim) wX wY
pushPastForward (prim wY wZ
a forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL prim wZ wB
before2) of
FL prim wY wZ
before2' :> Maybe2 prim wZ wB
Nothing2 ->
forall (prim :: * -> * -> *) wX wY.
(Show2 prim, Commute prim, Eq2 prim, Invert prim) =>
(:>) (Unwound prim) (Unwound prim) wX wY -> Unwound prim wX wY
squashPair (forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wX wB
before1 FL prim wB wC
ps1 RL prim wC wY
after1 forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wY wZ
before2' FL prim wB wC
ps2 RL prim wC wY
after2)
FL prim wY wZ
before2' :> Just2 prim wZ wB
a' ->
case forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn p1 (FL p2)
commuterIdFL forall (p :: * -> * -> *). Commute p => CommuteFn p p
selfCommuter (prim wZ wB
a' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL prim wB wC
ps2) of
Maybe ((:>) (FL prim) prim wZ wC)
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"stuck patch: squashPair 1:\n" forall a. [a] -> [a] -> [a]
++ forall (a :: * -> * -> *) wX wY. Show2 a => a wX wY -> String
show2 prim wZ wB
a' forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ forall (a :: * -> * -> *) wX wY. Show2 a => a wX wY -> String
show2 FL prim wB wC
ps2
Just (FL prim wZ wZ
ps2' :> prim wZ wC
a'') ->
forall (prim :: * -> * -> *) wX wY.
(Show2 prim, Commute prim, Eq2 prim, Invert prim) =>
(:>) (Unwound prim) (Unwound prim) wX wY -> Unwound prim wX wY
squashPair (forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wX wB
before1 FL prim wB wC
ps1 RL prim wC wY
after1 forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wY wZ
before2' FL prim wZ wZ
ps2' (forall (a :: * -> * -> *) wX. RL a wX wX
NilRL forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: prim wZ wC
a'' forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> RL a wY wZ -> RL a wX wZ
+<+ RL prim wC wY
after2))
squashPair (Unwound FL prim wX wB
before1 FL prim wB wC
ps1 RL prim wC wZ
NilRL :> Unwound (prim wZ wY
b :>: FL prim wY wB
before2) FL prim wB wC
ps2 RL prim wC wY
after2) =
case forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn (FL p1) p2
commuterFLId forall (p :: * -> * -> *). Commute p => CommuteFn p p
selfCommuter (FL prim wB wC
ps1 forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wY
b) of
Maybe ((:>) prim (FL prim) wB wY)
Nothing -> forall a. HasCallStack => String -> a
error String
"stuck patch: squashPair 2"
Just (prim wB wZ
b' :> FL prim wZ wY
ps1') -> forall (prim :: * -> * -> *) wX wY.
(Show2 prim, Commute prim, Eq2 prim, Invert prim) =>
(:>) (Unwound prim) (Unwound prim) wX wY -> Unwound prim wX wY
squashPair (forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound (FL prim wX wB
before1 forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ prim wB wZ
b' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: forall (a :: * -> * -> *) wX. FL a wX wX
NilFL) FL prim wZ wY
ps1' forall (a :: * -> * -> *) wX. RL a wX wX
NilRL forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wY wB
before2 FL prim wB wC
ps2 RL prim wC wY
after2)
pushPastForward
:: (Show2 prim, Commute prim, Eq2 prim, Invert prim)
=> (prim :> FL prim) wX wY
-> (FL prim :> Maybe2 prim) wX wY
pushPastForward :: forall (prim :: * -> * -> *) wX wY.
(Show2 prim, Commute prim, Eq2 prim, Invert prim) =>
(:>) prim (FL prim) wX wY -> (:>) (FL prim) (Maybe2 prim) wX wY
pushPastForward (prim wX wZ
p :> FL prim wZ wY
NilFL) = forall (a :: * -> * -> *) wX. FL a wX wX
NilFL forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (p :: * -> * -> *) wX wY. p wX wY -> Maybe2 p wX wY
Just2 prim wX wZ
p
pushPastForward (prim wX wZ
p :> (prim wZ wY
q :>: FL prim wY wY
qs))
| EqCheck wX wY
IsEq <- forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert prim wX wZ
p forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= prim wZ wY
q = FL prim wY wY
qs forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (p :: * -> * -> *) wX. Maybe2 p wX wX
Nothing2
| Just (prim wX wZ
q' :> prim wZ wY
p') <- forall (p :: * -> * -> *). Commute p => CommuteFn p p
commute (prim wX wZ
p forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wY
q)
= case forall (prim :: * -> * -> *) wX wY.
(Show2 prim, Commute prim, Eq2 prim, Invert prim) =>
(:>) prim (FL prim) wX wY -> (:>) (FL prim) (Maybe2 prim) wX wY
pushPastForward (prim wZ wY
p' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL prim wY wY
qs) of
FL prim wZ wZ
qs' :> Maybe2 prim wZ wY
p'' -> (prim wX wZ
q' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL prim wZ wZ
qs') forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> Maybe2 prim wZ wY
p''
| Bool
otherwise = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"stuck patch: pushPastForward:\n" forall a. [a] -> [a] -> [a]
++ forall (a :: * -> * -> *) wX wY. Show2 a => a wX wY -> String
show2 prim wX wZ
p forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ forall (a :: * -> * -> *) wX wY. Show2 a => a wX wY -> String
show2 prim wZ wY
q