module Darcs.Patch.Ident
( Ident(..)
, SignedIdent
, PatchId
, SignedId(..)
, StorableId(..)
, IdEq2(..)
, merge2FL
, fastRemoveFL
, fastRemoveRL
, fastRemoveSubsequenceRL
, findCommonFL
, commuteToPrefix
, commuteToPostfix
, commuteWhatWeCanToPostfix
, prop_identInvariantUnderCommute
, prop_sameIdentityImpliesCommutable
, prop_equalImpliesSameIdentity
) where
import qualified Data.Set as S
import Darcs.Prelude
import Darcs.Patch.Commute ( Commute, commute, commuteFL, commuteRL )
import Darcs.Patch.Merge ( Merge, mergeFL )
import Darcs.Patch.Permutations ( partitionFL', commuteWhatWeCanFL )
import Darcs.Patch.Show ( ShowPatchFor )
import Darcs.Patch.Witnesses.Eq ( Eq2(..), EqCheck(..), isIsEq )
import Darcs.Patch.Witnesses.Ordered
( (:/\:)(..)
, (:>)(..)
, (:\/:)(..)
, FL(..)
, RL(..)
, Fork(..)
, (+<<+)
, (+>>+)
, mapFL
, mapRL
, reverseRL
)
import Darcs.Patch.Witnesses.Unsafe ( unsafeCoercePEnd, unsafeCoercePStart )
import Darcs.Util.Parser ( Parser )
import Darcs.Util.Printer ( Doc )
type family PatchId (p :: * -> * -> *)
class Ord (PatchId p) => Ident p where
ident :: p wX wY -> PatchId p
class Ord a => SignedId a where
positiveId :: a -> Bool
invertId :: a -> a
type SignedIdent p = (Ident p, SignedId (PatchId p))
class StorableId a where
readId :: Parser a
showId :: ShowPatchFor -> a -> Doc
class IdEq2 p where
(=\^/=) :: p wA wB -> p wA wC -> EqCheck wB wC
(=/^\=) :: p wA wC -> p wB wC -> EqCheck wA wB
default (=\^/=) :: Ident p => p wA wB -> p wA wC -> EqCheck wB wC
p wA wB
p =\^/= p wA wC
q = if forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wA wB
p forall a. Eq a => a -> a -> Bool
== forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wA wC
q then forall (a :: * -> * -> *) wX wY1 wY2. a wX wY1 -> a wX wY2
unsafeCoercePEnd forall wA. EqCheck wA wA
IsEq else forall wA wB. EqCheck wA wB
NotEq
default (=/^\=) :: Ident p => p wA wC -> p wB wC -> EqCheck wA wB
p wA wC
p =/^\= p wB wC
q = if forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wA wC
p forall a. Eq a => a -> a -> Bool
== forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wB wC
q then forall (a :: * -> * -> *) wX1 wY wX2. a wX1 wY -> a wX2 wY
unsafeCoercePStart forall wA. EqCheck wA wA
IsEq else forall wA wB. EqCheck wA wB
NotEq
instance (Commute p, Ident p) => IdEq2 (FL p) where
FL p wA wB
ps =\^/= :: forall wA wB wC. FL p wA wB -> FL p wA wC -> EqCheck wB wC
=\^/= FL p wA wC
qs
| forall a. Ord a => [a] -> Set a
S.fromList (forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b]
mapFL forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident FL p wA wB
ps) forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> Set a
S.fromList (forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b]
mapFL forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident FL p wA wC
qs) = forall (a :: * -> * -> *) wX wY1 wY2. a wX wY1 -> a wX wY2
unsafeCoercePEnd forall wA. EqCheck wA wA
IsEq
| Bool
otherwise = forall wA wB. EqCheck wA wB
NotEq
FL p wA wC
ps =/^\= :: forall wA wC wB. FL p wA wC -> FL p wB wC -> EqCheck wA wB
=/^\= FL p wB wC
qs
| forall a. Ord a => [a] -> Set a
S.fromList (forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b]
mapFL forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident FL p wA wC
ps) forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> Set a
S.fromList (forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b]
mapFL forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident FL p wB wC
qs) = forall (a :: * -> * -> *) wX1 wY wX2. a wX1 wY -> a wX2 wY
unsafeCoercePStart forall wA. EqCheck wA wA
IsEq
| Bool
otherwise = forall wA wB. EqCheck wA wB
NotEq
merge2FL :: (Commute p, Merge p, Ident p)
=> FL p wX wY
-> FL p wX wZ
-> (FL p :/\: FL p) wY wZ
merge2FL :: forall (p :: * -> * -> *) wX wY wZ.
(Commute p, Merge p, Ident p) =>
FL p wX wY -> FL p wX wZ -> (:/\:) (FL p) (FL p) wY wZ
merge2FL FL p wX wY
xs FL p wX wZ
NilFL = forall (a :: * -> * -> *) wX. FL a wX wX
NilFL forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\: FL p wX wY
xs
merge2FL FL p wX wY
NilFL FL p wX wZ
ys = FL p wX wZ
ys forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\: forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
merge2FL FL p wX wY
xs (p wX wY
y :>: FL p wY wZ
ys)
| Just FL p wY wY
xs' <- forall (p :: * -> * -> *) wX wY wZ.
(Commute p, Ident p) =>
p wX wY -> FL p wX wZ -> Maybe (FL p wY wZ)
fastRemoveFL p wX wY
y FL p wX wY
xs = forall (p :: * -> * -> *) wX wY wZ.
(Commute p, Merge p, Ident p) =>
FL p wX wY -> FL p wX wZ -> (:/\:) (FL p) (FL p) wY wZ
merge2FL FL p wY wY
xs' FL p wY wZ
ys
merge2FL (p wX wY
x :>: FL p wY wY
xs) FL p wX wZ
ys
| Just FL p wY wZ
ys' <- forall (p :: * -> * -> *) wX wY wZ.
(Commute p, Ident p) =>
p wX wY -> FL p wX wZ -> Maybe (FL p wY wZ)
fastRemoveFL p wX wY
x FL p wX wZ
ys = forall (p :: * -> * -> *) wX wY wZ.
(Commute p, Merge p, Ident p) =>
FL p wX wY -> FL p wX wZ -> (:/\:) (FL p) (FL p) wY wZ
merge2FL FL p wY wY
xs FL p wY wZ
ys'
| Bool
otherwise =
case forall (p :: * -> * -> *) wX wY.
Merge p =>
(:\/:) p (FL p) wX wY -> (:/\:) (FL p) p wX wY
mergeFL (p wX wY
x forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: FL p wX wZ
ys) of
FL p wY wZ
ys' :/\: p wZ wZ
x' ->
case forall (p :: * -> * -> *) wX wY wZ.
(Commute p, Merge p, Ident p) =>
FL p wX wY -> FL p wX wZ -> (:/\:) (FL p) (FL p) wY wZ
merge2FL FL p wY wY
xs FL p wY wZ
ys' of
FL p wY wZ
ys'' :/\: FL p wZ wZ
xs' -> FL p wY wZ
ys'' forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\: (p wZ wZ
x' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wZ wZ
xs')
{-# INLINABLE fastRemoveFL #-}
fastRemoveFL :: forall p wX wY wZ. (Commute p, Ident p)
=> p wX wY
-> FL p wX wZ
-> Maybe (FL p wY wZ)
fastRemoveFL :: forall (p :: * -> * -> *) wX wY wZ.
(Commute p, Ident p) =>
p wX wY -> FL p wX wZ -> Maybe (FL p wY wZ)
fastRemoveFL p wX wY
a FL p wX wZ
bs
| PatchId p
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b]
mapFL forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident FL p wX wZ
bs = forall a. Maybe a
Nothing
| Bool
otherwise = do
p wX wZ
_ :> FL p wZ wZ
bs' <- forall wA wB wC.
RL p wA wB -> FL p wB wC -> Maybe ((:>) p (FL p) wA wC)
pullout forall (a :: * -> * -> *) wX. RL a wX wX
NilRL FL p wX wZ
bs
forall a. a -> Maybe a
Just (forall (a :: * -> * -> *) wX1 wY wX2. a wX1 wY -> a wX2 wY
unsafeCoercePStart FL p wZ wZ
bs')
where
i :: PatchId p
i = forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wX wY
a
pullout :: RL p wA wB -> FL p wB wC -> Maybe ((p :> FL p) wA wC)
pullout :: forall wA wB wC.
RL p wA wB -> FL p wB wC -> Maybe ((:>) p (FL p) wA wC)
pullout RL p wA wB
_ FL p wB wC
NilFL = forall a. Maybe a
Nothing
pullout RL p wA wB
acc (p wB wY
x :>: FL p wY wC
xs)
| forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wB wY
x forall a. Eq a => a -> a -> Bool
== PatchId p
i = do
p wA wZ
x' :> RL p wZ wY
acc' <- forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> Maybe ((:>) p (RL p) wX wY)
commuteRL (RL p wA wB
acc forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wB wY
x)
forall a. a -> Maybe a
Just (p wA wZ
x' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wY
acc' forall (p :: * -> * -> *) wX wY wZ.
RL p wX wY -> FL p wY wZ -> FL p wX wZ
+>>+ FL p wY wC
xs)
| Bool
otherwise = forall wA wB wC.
RL p wA wB -> FL p wB wC -> Maybe ((:>) p (FL p) wA wC)
pullout (RL p wA wB
acc forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p wB wY
x) FL p wY wC
xs
fastRemoveRL :: forall p wX wY wZ. (Commute p, Ident p)
=> p wY wZ
-> RL p wX wZ
-> Maybe (RL p wX wY)
fastRemoveRL :: forall (p :: * -> * -> *) wX wY wZ.
(Commute p, Ident p) =>
p wY wZ -> RL p wX wZ -> Maybe (RL p wX wY)
fastRemoveRL p wY wZ
a RL p wX wZ
bs
| PatchId p
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> RL a wX wY -> [b]
mapRL forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident RL p wX wZ
bs = forall a. Maybe a
Nothing
| Bool
otherwise = do
RL p wX wZ
bs' :> p wZ wZ
_ <- forall wA wB wC.
RL p wA wB -> FL p wB wC -> Maybe ((:>) (RL p) p wA wC)
pullout RL p wX wZ
bs forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
forall a. a -> Maybe a
Just (forall (a :: * -> * -> *) wX wY1 wY2. a wX wY1 -> a wX wY2
unsafeCoercePEnd RL p wX wZ
bs')
where
i :: PatchId p
i = forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wY wZ
a
pullout :: RL p wA wB -> FL p wB wC -> Maybe ((RL p :> p) wA wC)
pullout :: forall wA wB wC.
RL p wA wB -> FL p wB wC -> Maybe ((:>) (RL p) p wA wC)
pullout RL p wA wB
NilRL FL p wB wC
_ = forall a. Maybe a
Nothing
pullout (RL p wA wY
xs :<: p wY wB
x) FL p wB wC
acc
| forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wY wB
x forall a. Eq a => a -> a -> Bool
== PatchId p
i = do
FL p wY wZ
acc' :> p wZ wC
x' <- forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> Maybe ((:>) (FL p) p wX wY)
commuteFL (p wY wB
x forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wB wC
acc)
forall a. a -> Maybe a
Just (RL p wA wY
xs forall (p :: * -> * -> *) wX wY wZ.
RL p wX wY -> FL p wY wZ -> RL p wX wZ
+<<+ FL p wY wZ
acc' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wC
x')
| Bool
otherwise = forall wA wB wC.
RL p wA wB -> FL p wB wC -> Maybe ((:>) (RL p) p wA wC)
pullout RL p wA wY
xs (p wY wB
x forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wB wC
acc)
fastRemoveSubsequenceRL :: (Commute p, Ident p)
=> RL p wY wZ
-> RL p wX wZ
-> Maybe (RL p wX wY)
fastRemoveSubsequenceRL :: forall (p :: * -> * -> *) wY wZ wX.
(Commute p, Ident p) =>
RL p wY wZ -> RL p wX wZ -> Maybe (RL p wX wY)
fastRemoveSubsequenceRL RL p wY wZ
NilRL RL p wX wZ
ys = forall a. a -> Maybe a
Just RL p wX wZ
ys
fastRemoveSubsequenceRL (RL p wY wY
xs :<: p wY wZ
x) RL p wX wZ
ys =
forall (p :: * -> * -> *) wX wY wZ.
(Commute p, Ident p) =>
p wY wZ -> RL p wX wZ -> Maybe (RL p wX wY)
fastRemoveRL p wY wZ
x RL p wX wZ
ys forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (p :: * -> * -> *) wY wZ wX.
(Commute p, Ident p) =>
RL p wY wZ -> RL p wX wZ -> Maybe (RL p wX wY)
fastRemoveSubsequenceRL RL p wY wY
xs
findCommonFL :: (Commute p, Ident p)
=> FL p wX wY
-> FL p wX wZ
-> Fork (FL p) (FL p) (FL p) wX wY wZ
findCommonFL :: forall (p :: * -> * -> *) wX wY wZ.
(Commute p, Ident p) =>
FL p wX wY -> FL p wX wZ -> Fork (FL p) (FL p) (FL p) wX wY wZ
findCommonFL FL p wX wY
xs FL p wX wZ
ys =
case forall (p :: * -> * -> *) wX wY.
(Commute p, Ident p) =>
Set (PatchId p) -> FL p wX wY -> Maybe ((:>) (FL p) (RL p) wX wY)
commuteToPrefix Set (PatchId p)
commonIds FL p wX wY
xs of
Maybe ((:>) (FL p) (RL p) wX wY)
Nothing -> forall a. HasCallStack => [Char] -> a
error [Char]
"failed to commute common patches (lhs)"
Just (FL p wX wZ
cxs :> RL p wZ wY
xs') ->
case forall (p :: * -> * -> *) wX wY.
(Commute p, Ident p) =>
Set (PatchId p) -> FL p wX wY -> Maybe ((:>) (FL p) (RL p) wX wY)
commuteToPrefix Set (PatchId p)
commonIds FL p wX wZ
ys of
Maybe ((:>) (FL p) (RL p) wX wZ)
Nothing -> forall a. HasCallStack => [Char] -> a
error [Char]
"failed to commute common patches (rhs)"
Just (FL p wX wZ
cys :> RL p wZ wZ
ys') ->
case FL p wX wZ
cxs forall (p :: * -> * -> *) wA wB wC.
IdEq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\^/= FL p wX wZ
cys of
EqCheck wZ wZ
NotEq -> forall a. HasCallStack => [Char] -> a
error [Char]
"common patches aren't equal"
EqCheck wZ wZ
IsEq -> forall (common :: * -> * -> *) (left :: * -> * -> *)
(right :: * -> * -> *) wA wX wY wU.
common wA wU
-> left wU wX -> right wU wY -> Fork common left right wA wX wY
Fork FL p wX wZ
cxs (forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL p wZ wY
xs') (forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL p wZ wZ
ys')
where
commonIds :: Set (PatchId p)
commonIds =
forall a. Ord a => [a] -> Set a
S.fromList (forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b]
mapFL forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident FL p wX wY
xs) forall a. Ord a => Set a -> Set a -> Set a
`S.intersection` forall a. Ord a => [a] -> Set a
S.fromList (forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b]
mapFL forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident FL p wX wZ
ys)
commuteToPrefix :: (Commute p, Ident p)
=> S.Set (PatchId p) -> FL p wX wY -> Maybe ((FL p :> RL p) wX wY)
commuteToPrefix :: forall (p :: * -> * -> *) wX wY.
(Commute p, Ident p) =>
Set (PatchId p) -> FL p wX wY -> Maybe ((:>) (FL p) (RL p) wX wY)
commuteToPrefix Set (PatchId p)
is FL p wX wY
ps
| FL p wX wZ
prefix :> RL p wZ wZ
NilRL :> RL p wZ wY
rest <-
forall (p :: * -> * -> *) wA wB wC wD.
Commute p =>
(forall wU wV. p wU wV -> Bool)
-> RL p wA wB
-> RL p wB wC
-> FL p wC wD
-> (:>) (FL p) (RL p :> RL p) wA wD
partitionFL' ((forall a. Ord a => a -> Set a -> Bool
`S.member` Set (PatchId p)
is) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident) forall (a :: * -> * -> *) wX. RL a wX wX
NilRL forall (a :: * -> * -> *) wX. RL a wX wX
NilRL FL p wX wY
ps = forall a. a -> Maybe a
Just (FL p wX wZ
prefix forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wY
rest)
| Bool
otherwise = forall a. Maybe a
Nothing
commuteToPostfix :: forall p wX wY. (Commute p, Ident p)
=> S.Set (PatchId p) -> RL p wX wY -> Maybe ((FL p :> RL p) wX wY)
commuteToPostfix :: forall (p :: * -> * -> *) wX wY.
(Commute p, Ident p) =>
Set (PatchId p) -> RL p wX wY -> Maybe ((:>) (FL p) (RL p) wX wY)
commuteToPostfix Set (PatchId p)
ids RL p wX wY
patches = forall wA wB.
Set (PatchId p)
-> (:>) (RL p) (FL p) wA wB -> Maybe ((:>) (FL p) (RL p) wA wB)
push Set (PatchId p)
ids (RL p wX wY
patches forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)
where
push :: S.Set (PatchId p) -> (RL p :> FL p) wA wB -> Maybe ((FL p :> RL p) wA wB)
push :: forall wA wB.
Set (PatchId p)
-> (:>) (RL p) (FL p) wA wB -> Maybe ((:>) (FL p) (RL p) wA wB)
push Set (PatchId p)
_ (RL p wA wZ
NilRL :> FL p wZ wB
left) = forall (m :: * -> *) a. Monad m => a -> m a
return (FL p wZ wB
left forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (a :: * -> * -> *) wX. RL a wX wX
NilRL)
push Set (PatchId p)
is (RL p wA wZ
ps :> FL p wZ wB
left)
| forall a. Set a -> Bool
S.null Set (PatchId p)
is = forall (m :: * -> *) a. Monad m => a -> m a
return (RL p wA wZ
ps forall (p :: * -> * -> *) wX wY wZ.
RL p wX wY -> FL p wY wZ -> FL p wX wZ
+>>+ FL p wZ wB
left forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (a :: * -> * -> *) wX. RL a wX wX
NilRL)
push Set (PatchId p)
is (RL p wA wY
ps :<: p wY wZ
p :> FL p wZ wB
left)
| let i :: PatchId p
i = forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wY wZ
p
, PatchId p
i forall a. Ord a => a -> Set a -> Bool
`S.member` Set (PatchId p)
is = do
FL p wY wZ
left' :> p wZ wB
p' <- forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> Maybe ((:>) (FL p) p wX wY)
commuteFL (p wY wZ
p forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wZ wB
left)
FL p wA wZ
left'' :> RL p wZ wZ
right <- forall wA wB.
Set (PatchId p)
-> (:>) (RL p) (FL p) wA wB -> Maybe ((:>) (FL p) (RL p) wA wB)
push (forall a. Ord a => a -> Set a -> Set a
S.delete PatchId p
i Set (PatchId p)
is) (RL p wA wY
ps forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wY wZ
left')
forall (m :: * -> *) a. Monad m => a -> m a
return (FL p wA wZ
left'' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wZ
right forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p wZ wB
p')
| Bool
otherwise = forall wA wB.
Set (PatchId p)
-> (:>) (RL p) (FL p) wA wB -> Maybe ((:>) (FL p) (RL p) wA wB)
push Set (PatchId p)
is (RL p wA wY
ps forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wY wZ
p forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wZ wB
left)
commuteWhatWeCanToPostfix :: forall p wX wY. (Commute p, Ident p)
=> S.Set (PatchId p) -> RL p wX wY -> (FL p :> RL p) wX wY
commuteWhatWeCanToPostfix :: forall (p :: * -> * -> *) wX wY.
(Commute p, Ident p) =>
Set (PatchId p) -> RL p wX wY -> (:>) (FL p) (RL p) wX wY
commuteWhatWeCanToPostfix Set (PatchId p)
ids RL p wX wY
patches = forall wA wB.
Set (PatchId p)
-> (:>) (RL p) (FL p) wA wB -> (:>) (FL p) (RL p) wA wB
push Set (PatchId p)
ids (RL p wX wY
patches forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)
where
push :: S.Set (PatchId p) -> (RL p :> FL p) wA wB -> (FL p :> RL p) wA wB
push :: forall wA wB.
Set (PatchId p)
-> (:>) (RL p) (FL p) wA wB -> (:>) (FL p) (RL p) wA wB
push Set (PatchId p)
_ (RL p wA wZ
NilRL :> FL p wZ wB
left) = FL p wZ wB
left forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (a :: * -> * -> *) wX. RL a wX wX
NilRL
push Set (PatchId p)
is (RL p wA wZ
ps :> FL p wZ wB
left)
| forall a. Set a -> Bool
S.null Set (PatchId p)
is = RL p wA wZ
ps forall (p :: * -> * -> *) wX wY wZ.
RL p wX wY -> FL p wY wZ -> FL p wX wZ
+>>+ FL p wZ wB
left forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (a :: * -> * -> *) wX. RL a wX wX
NilRL
push Set (PatchId p)
is (RL p wA wY
ps :<: p wY wZ
p :> FL p wZ wB
left)
| let i :: PatchId p
i = forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wY wZ
p
, PatchId p
i forall a. Ord a => a -> Set a -> Bool
`S.member` Set (PatchId p)
is =
case forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> (:>) (FL p) (p :> FL p) wX wY
commuteWhatWeCanFL (p wY wZ
p forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wZ wB
left) of
FL p wY wZ
left' :> p wZ wZ
p' :> FL p wZ wB
deps ->
case forall wA wB.
Set (PatchId p)
-> (:>) (RL p) (FL p) wA wB -> (:>) (FL p) (RL p) wA wB
push (forall a. Ord a => a -> Set a -> Set a
S.delete PatchId p
i Set (PatchId p)
is) (RL p wA wY
ps forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wY wZ
left') of
FL p wA wZ
left'' :> RL p wZ wZ
right -> FL p wA wZ
left'' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (RL p wZ wZ
right forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p wZ wZ
p' forall (p :: * -> * -> *) wX wY wZ.
RL p wX wY -> FL p wY wZ -> RL p wX wZ
+<<+ FL p wZ wB
deps)
| Bool
otherwise = forall wA wB.
Set (PatchId p)
-> (:>) (RL p) (FL p) wA wB -> (:>) (FL p) (RL p) wA wB
push Set (PatchId p)
is (RL p wA wY
ps forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wY wZ
p forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wZ wB
left)
prop_identInvariantUnderCommute :: (Commute p, Ident p)
=> (p :> p) wX wY -> Maybe Bool
prop_identInvariantUnderCommute :: forall (p :: * -> * -> *) wX wY.
(Commute p, Ident p) =>
(:>) p p wX wY -> Maybe Bool
prop_identInvariantUnderCommute (p wX wZ
p :> p wZ wY
q) =
case forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (p wX wZ
p forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wY
q) of
Just (p wX wZ
q' :> p wZ wY
p') -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wX wZ
p forall a. Eq a => a -> a -> Bool
== forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wZ wY
p' Bool -> Bool -> Bool
&& forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wZ wY
q forall a. Eq a => a -> a -> Bool
== forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wX wZ
q'
Maybe ((:>) p p wX wY)
Nothing -> forall a. Maybe a
Nothing
prop_sameIdentityImpliesCommutable :: (Commute p, Eq2 p, Ident p)
=> (p :\/: (RL p :> p)) wX wY -> Maybe Bool
prop_sameIdentityImpliesCommutable :: forall (p :: * -> * -> *) wX wY.
(Commute p, Eq2 p, Ident p) =>
(:\/:) p (RL p :> p) wX wY -> Maybe Bool
prop_sameIdentityImpliesCommutable (p wZ wX
p :\/: (RL p wZ wZ
ps :> p wZ wY
q))
| forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wZ wX
p forall a. Eq a => a -> a -> Bool
== forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wZ wY
q =
case forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> Maybe ((:>) p (RL p) wX wY)
commuteRL (RL p wZ wZ
ps forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wY
q) of
Just (p wZ wZ
p' :> RL p wZ wY
_) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall wA wB. EqCheck wA wB -> Bool
isIsEq (p wZ wX
p forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= p wZ wZ
p')
Maybe ((:>) p (RL p) wZ wY)
Nothing -> forall a. a -> Maybe a
Just Bool
False
| Bool
otherwise = forall a. Maybe a
Nothing
prop_equalImpliesSameIdentity :: (Eq2 p, Ident p)
=> (p :\/: p) wX wY -> Maybe Bool
prop_equalImpliesSameIdentity :: forall (p :: * -> * -> *) wX wY.
(Eq2 p, Ident p) =>
(:\/:) p p wX wY -> Maybe Bool
prop_equalImpliesSameIdentity (p wZ wX
p :\/: p wZ wY
q)
| EqCheck wX wY
IsEq <- p wZ wX
p forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= p wZ wY
q = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wZ wX
p forall a. Eq a => a -> a -> Bool
== forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wZ wY
q
| Bool
otherwise = forall a. Maybe a
Nothing