module Darcs.Patch.Ident
    ( Ident(..)
    , SignedIdent
    , PatchId
    , (=\^/=)
    , (=/^\=)
    , SignedId(..)
    , StorableId(..)
    , fastRemoveFL
    , fastRemoveRL
    , fastRemoveSubsequenceRL
    , findCommonFL
    , findCommonRL
    , findCommonWithThemFL
    , findCommonWithThemRL
    , commuteToPrefix
    -- * Properties
    , prop_identInvariantUnderCommute
    , prop_sameIdentityImpliesCommutable
    , prop_equalImpliesSameIdentity
    , prop_sameIdentityImpliesEqual
    ) where

import qualified Data.Set as S

import Darcs.Prelude

import Darcs.Patch.Commute ( Commute, commute, commuteFL, commuteRL )
import Darcs.Patch.Permutations ( partitionFL', partitionRL' )
import Darcs.Patch.Show ( ShowPatchFor )
import Darcs.Patch.Witnesses.Eq ( Eq2(..), EqCheck(..), isIsEq )
import Darcs.Patch.Witnesses.Ordered
    ( (:>)(..)
    , (:\/:)(..)
    , FL(..)
    , RL(..)
    , Fork(..)
    , (+<<+)
    , (+>>+)
    , mapFL
    , mapRL
    , reverseFL
    , reverseRL
    )
import Darcs.Patch.Witnesses.Unsafe ( unsafeCoercePEnd, unsafeCoercePStart )

import Darcs.Util.Parser ( Parser )
import Darcs.Util.Printer ( Doc )

-- | The reason this is not associated to class 'Ident' is that for technical
-- reasons we want to be able to define type instances for patches that don't
-- have an identity and therefore cannot be lawful members of class 'Ident'.
type family PatchId (p :: * -> * -> *)

{- | Class of patches that have an identity/name.

Patches with an identity give rise to the notion of /nominal equality/,
expressed by the operators '=\^/=' and '=/^\='.

Laws:

[/ident-commute/]

    Patch identity must be invariant under commutation:

    prop> 'commute' (p :> _) == 'Just' (_ :> p') => 'ident' p == 'ident' p'

    and thus (via symmetry of 'commute'):

    prop> 'commute' (_ :> q) == 'Just' (q' :> _) => 'ident' q == 'ident' q'

    Conversely, patches with the same identity result from a series of
    'commute's:

    prop> 'ident' p == 'ident' p' => exists qs, qs' :: FL p. 'commuteFL' (p :> qs) == 'Just' (qs' :> p')

[/ident-compare/]

    In general, comparing patches via their identity is
    weaker than (semantic) equality:

    prop> 'unsafeCompare' p q => 'ident' p == 'ident' q

    However, if the patches have a common context, then semantic and nominal
    equality should coincide, up to internal re-ordering:

    prop> p '=\~/=' q  <=> p '=\^/=' q
    prop> p '=/~\=' q  <=> p '=/^\=' q

    (Technical note: equality up to internal re-ordering is currently only
    defined for 'FL's, but it should be obvious how to generalize it.)

Taken together, these laws express the assumption that recording a patch
gives it a universally unique identity.

Note that violations of this universal property are currently not detected
in a reliable way. Fixing this is possible but far from easy.

-}
class Ord (PatchId p) => Ident p where
  ident :: p wX wY -> PatchId p

type instance PatchId (FL p) = S.Set (PatchId p)
type instance PatchId (RL p) = S.Set (PatchId p)
type instance PatchId (p :> p) = S.Set (PatchId p)

instance Ident p => Ident (FL p) where
  ident :: forall wX wY. FL p wX wY -> PatchId (FL p)
ident = [PatchId p] -> Set (PatchId p)
forall a. Ord a => [a] -> Set a
S.fromList ([PatchId p] -> Set (PatchId p))
-> (FL p wX wY -> [PatchId p]) -> FL p wX wY -> Set (PatchId p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall wW wZ. p wW wZ -> PatchId p) -> FL p wX wY -> [PatchId p]
forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b]
mapFL p wW wZ -> PatchId p
forall wW wZ. p wW wZ -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident

instance Ident p => Ident (RL p) where
  ident :: forall wX wY. RL p wX wY -> PatchId (RL p)
ident = [PatchId p] -> Set (PatchId p)
forall a. Ord a => [a] -> Set a
S.fromList ([PatchId p] -> Set (PatchId p))
-> (RL p wX wY -> [PatchId p]) -> RL p wX wY -> Set (PatchId p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall wW wZ. p wW wZ -> PatchId p) -> RL p wX wY -> [PatchId p]
forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> RL a wX wY -> [b]
mapRL p wW wZ -> PatchId p
forall wW wZ. p wW wZ -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident

instance Ident p => Ident (p :> p) where
  ident :: forall wX wY. (:>) p p wX wY -> PatchId (p :> p)
ident (p wX wZ
p :> p wZ wY
q) = [PatchId p] -> Set (PatchId p)
forall a. Ord a => [a] -> Set a
S.fromList [p wX wZ -> PatchId p
forall wX wY. p wX wY -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wX wZ
p, p wZ wY -> PatchId p
forall wX wY. p wX wY -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wZ wY
q]

-- | Nominal equality for patches with an identity in the same context. Usually
-- quite a bit faster than structural equality.
(=\^/=) :: Ident p => p wA wB -> p wA wC -> EqCheck wB wC
p wA wB
p =\^/= :: forall (p :: * -> * -> *) wA wB wC.
Ident p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\^/= p wA wC
q = if p wA wB -> PatchId p
forall wX wY. p wX wY -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wA wB
p PatchId p -> PatchId p -> Bool
forall a. Eq a => a -> a -> Bool
== p wA wC -> PatchId p
forall wX wY. p wX wY -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wA wC
q then EqCheck wB wB -> EqCheck wB wC
forall (a :: * -> * -> *) wX wY1 wY2. a wX wY1 -> a wX wY2
unsafeCoercePEnd EqCheck wB wB
forall wA. EqCheck wA wA
IsEq else EqCheck wB wC
forall wA wB. EqCheck wA wB
NotEq

(=/^\=) :: Ident p => p wA wC -> p wB wC -> EqCheck wA wB
p wA wC
p =/^\= :: forall (p :: * -> * -> *) wA wC wB.
Ident p =>
p wA wC -> p wB wC -> EqCheck wA wB
=/^\= p wB wC
q = if p wA wC -> PatchId p
forall wX wY. p wX wY -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wA wC
p PatchId p -> PatchId p -> Bool
forall a. Eq a => a -> a -> Bool
== p wB wC -> PatchId p
forall wX wY. p wX wY -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wB wC
q then EqCheck wB wB -> EqCheck wA wB
forall (a :: * -> * -> *) wX1 wY wX2. a wX1 wY -> a wX2 wY
unsafeCoercePStart EqCheck wB wB
forall wA. EqCheck wA wA
IsEq else EqCheck wA wB
forall wA wB. EqCheck wA wB
NotEq


{- | Signed identities.

Like for class 'Invert', we require that 'invertId' is self-inverse:

prop> 'invertId' . 'invertId' = 'id'

We also require that inverting changes the sign:

prop> 'positiveId' . 'invertId' = 'not' . 'positiveId'

Side remark: in mathematical terms, these properties can be expressed by
stating that 'invertId' is an involution and that 'positiveId' is a
"homomorphism of sets with an involution" (there is no official term for
this) from @a@ to the simplest non-trivial set with involution, namely
'Bool' with the involution 'not'.
-}
class Ord a => SignedId a where
  positiveId :: a -> Bool
  invertId :: a -> a

{- | Constraint for patches that have an identity that is signed,
     i.e. can be positive (uninverted) or negative (inverted).

Provided that an instance 'Invert' exists, inverting a patch
inverts its identity:

prop> 'ident' ('invert' p) = 'invertId' ('ident' p)

-}
type SignedIdent p = (Ident p, SignedId (PatchId p))


{- | Storable identities.

The methods here can be used to help implement ReadPatch and ShowPatch
for a patch type containing the identity.

As with all Read/Show pairs, We expect that the output of
@showId ForStorage x@ can be parsed by 'readId' to produce @x@:

prop> 'parse' 'readId' . 'renderPS' . 'showId' 'ForStorage' == 'id'

-}
class StorableId a where
  readId :: Parser a
  showId :: ShowPatchFor -> a -> Doc

{-# INLINABLE fastRemoveFL #-}
-- | Remove a patch from an FL of patches with an identity. The result is
-- 'Just' whenever the patch has been found and removed and 'Nothing'
-- otherwise. If the patch is not found at the head of the sequence we must
-- first commute it to the head before we can remove it.
-- 
-- We assume that this commute always succeeds. This is justified because
-- patches are created with a (universally) unique identity, implying that if
-- two patches have the same identity, then they have originally been the same
-- patch; thus being at a different position must be due to commutation,
-- meaning we can commute it back.
--
-- For patch types that define semantic equality via nominal equality, this is
-- only faster than 'removeFL' if the patch does not occur in the sequence,
-- otherwise we have to perform the same number of commutations.
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 PatchId p -> [PatchId p] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` (forall wW wZ. p wW wZ -> PatchId p) -> FL p wX wZ -> [PatchId p]
forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b]
mapFL p wW wZ -> PatchId p
forall wW wZ. p wW wZ -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident FL p wX wZ
bs = Maybe (FL p wY wZ)
forall a. Maybe a
Nothing
  | Bool
otherwise = do
      p wX wZ
_ :> FL p wZ wZ
bs' <- RL p wX wX -> FL p wX wZ -> Maybe ((:>) p (FL p) wX wZ)
forall wA wB wC.
RL p wA wB -> FL p wB wC -> Maybe ((:>) p (FL p) wA wC)
pullout RL p wX wX
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL FL p wX wZ
bs
      FL p wY wZ -> Maybe (FL p wY wZ)
forall a. a -> Maybe a
Just (FL p wZ wZ -> FL p wY wZ
forall (a :: * -> * -> *) wX1 wY wX2. a wX1 wY -> a wX2 wY
unsafeCoercePStart FL p wZ wZ
bs')
  where
    i :: PatchId p
i = p wX wY -> PatchId p
forall wW wZ. p wW wZ -> PatchId p
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 = Maybe ((:>) p (FL p) wA wC)
forall a. Maybe a
Nothing
    pullout RL p wA wB
acc (p wB wY
x :>: FL p wY wC
xs)
      | p wB wY -> PatchId p
forall wW wZ. p wW wZ -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wB wY
x PatchId p -> PatchId p -> Bool
forall a. Eq a => a -> a -> Bool
== PatchId p
i = do
          p wA wZ
x' :> RL p wZ wY
acc' <- (:>) (RL p) p wA wY -> Maybe ((:>) p (RL p) wA wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> Maybe ((:>) p (RL p) wX wY)
commuteRL (RL p wA wB
acc RL p wA wB -> p wB wY -> (:>) (RL p) p wA wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wB wY
x)
          (:>) p (FL p) wA wC -> Maybe ((:>) p (FL p) wA wC)
forall a. a -> Maybe a
Just (p wA wZ
x' p wA wZ -> FL p wZ wC -> (:>) p (FL p) wA wC
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wY
acc' RL p wZ wY -> FL p wY wC -> FL p wZ wC
forall (p :: * -> * -> *) wX wY wZ.
RL p wX wY -> FL p wY wZ -> FL p wX wZ
+>>+ FL p wY wC
xs)
      | Bool
otherwise = RL p wA wY -> FL p wY wC -> Maybe ((:>) p (FL p) wA wC)
forall wA wB wC.
RL p wA wB -> FL p wB wC -> Maybe ((:>) p (FL p) wA wC)
pullout (RL p wA wB
acc RL p wA wB -> p wB wY -> RL p wA wY
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

-- | Same as 'fastRemoveFL' only for 'RL'.
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 PatchId p -> [PatchId p] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` (forall wW wZ. p wW wZ -> PatchId p) -> RL p wX wZ -> [PatchId p]
forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> RL a wX wY -> [b]
mapRL p wW wZ -> PatchId p
forall wW wZ. p wW wZ -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident RL p wX wZ
bs = Maybe (RL p wX wY)
forall a. Maybe a
Nothing
  | Bool
otherwise = do
      RL p wX wZ
bs' :> p wZ wZ
_ <- RL p wX wZ -> FL p wZ wZ -> Maybe ((:>) (RL p) p wX 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 FL p wZ wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
      RL p wX wY -> Maybe (RL p wX wY)
forall a. a -> Maybe a
Just (RL p wX wZ -> RL p wX wY
forall (a :: * -> * -> *) wX wY1 wY2. a wX wY1 -> a wX wY2
unsafeCoercePEnd RL p wX wZ
bs')
  where
    i :: PatchId p
i = p wY wZ -> PatchId p
forall wW wZ. p wW wZ -> PatchId p
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
_ = Maybe ((:>) (RL p) p wA wC)
forall a. Maybe a
Nothing
    pullout (RL p wA wY
xs :<: p wY wB
x) FL p wB wC
acc
      | p wY wB -> PatchId p
forall wW wZ. p wW wZ -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wY wB
x PatchId p -> PatchId p -> Bool
forall a. Eq a => a -> a -> Bool
== PatchId p
i = do
          FL p wY wZ
acc' :> p wZ wC
x' <- (:>) p (FL p) wY wC -> Maybe ((:>) (FL p) p wY wC)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> Maybe ((:>) (FL p) p wX wY)
commuteFL (p wY wB
x p wY wB -> FL p wB wC -> (:>) p (FL p) wY wC
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wB wC
acc)
          (:>) (RL p) p wA wC -> Maybe ((:>) (RL p) p wA wC)
forall a. a -> Maybe a
Just (RL p wA wY
xs RL p wA wY -> FL p wY wZ -> RL p wA wZ
forall (p :: * -> * -> *) wX wY wZ.
RL p wX wY -> FL p wY wZ -> RL p wX wZ
+<<+ FL p wY wZ
acc' RL p wA wZ -> p wZ wC -> (:>) (RL p) p wA wC
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wC
x')
      | Bool
otherwise = RL p wA wY -> FL p wY wC -> Maybe ((:>) (RL p) p wA wC)
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 p wY wB -> FL p wB wC -> FL p wY wC
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 = RL p wX wY -> Maybe (RL p wX wY)
forall a. a -> Maybe a
Just RL p wX wY
RL p wX wZ
ys
fastRemoveSubsequenceRL (RL p wY wY
xs :<: p wY wZ
x) RL p wX wZ
ys =
  p wY wZ -> RL p wX wZ -> Maybe (RL p wX wY)
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 Maybe (RL p wX wY)
-> (RL p wX wY -> Maybe (RL p wX wY)) -> Maybe (RL p wX wY)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= RL p wY wY -> RL p wX wY -> Maybe (RL p wX wY)
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

-- | Find the common and uncommon parts of two lists that start in a common
-- context, using patch identity for comparison. Of the common patches, only
-- one is retained, the other is discarded.
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 FL p wX wY -> FL p wX wZ -> (:>) (FL p) (FL p) wX wY
forall (p :: * -> * -> *) wX wY wZ.
(Commute p, Ident p) =>
FL p wX wY -> FL p wX wZ -> (:>) (FL p) (FL p) wX wY
findCommonWithThemFL FL p wX wY
xs FL p wX wZ
ys of
    FL p wX wZ
cxs :> FL p wZ wY
xs' ->
      case FL p wX wZ -> FL p wX wY -> (:>) (FL p) (FL p) wX wZ
forall (p :: * -> * -> *) wX wY wZ.
(Commute p, Ident p) =>
FL p wX wY -> FL p wX wZ -> (:>) (FL p) (FL p) wX wY
findCommonWithThemFL FL p wX wZ
ys FL p wX wY
xs of
        FL p wX wZ
cys :> FL p wZ wZ
ys' ->
          case FL p wX wZ
cxs FL p wX wZ -> FL p wX wZ -> EqCheck wZ wZ
forall (p :: * -> * -> *) wA wB wC.
Ident p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\^/= FL p wX wZ
cys of
            EqCheck wZ wZ
NotEq -> [Char] -> Fork (FL p) (FL p) (FL p) wX wY wZ
forall a. HasCallStack => [Char] -> a
error [Char]
"common patches aren't equal"
            EqCheck wZ wZ
IsEq -> FL p wX wZ
-> FL p wZ wY -> FL p wZ wZ -> Fork (FL p) (FL p) (FL p) wX wY wZ
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 FL p wZ wY
xs' FL p wZ wZ
FL p wZ wZ
ys'

findCommonWithThemFL
  :: (Commute p, Ident p) => FL p wX wY -> FL p wX wZ -> (FL p :> FL p) wX wY
findCommonWithThemFL :: forall (p :: * -> * -> *) wX wY wZ.
(Commute p, Ident p) =>
FL p wX wY -> FL p wX wZ -> (:>) (FL p) (FL p) wX wY
findCommonWithThemFL FL p wX wY
xs FL p wX wZ
ys =
  case (forall wU wV. p wU wV -> Bool)
-> RL p wX wX
-> RL p wX wX
-> FL p wX wY
-> (:>) (FL p) (RL p :> RL p) wX wY
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' ((PatchId p -> Set (PatchId p) -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set (PatchId p)
yids) (PatchId p -> Bool) -> (p wU wV -> PatchId p) -> p wU wV -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p wU wV -> PatchId p
forall wX wY. p wX wY -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident) RL p wX wX
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL RL p wX wX
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL FL p wX wY
xs of
    FL p wX wZ
cxs :> RL p wZ wZ
NilRL :> RL p wZ wY
xs' -> FL p wX wZ
cxs FL p wX wZ -> FL p wZ wY -> (:>) (FL p) (FL p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wY -> FL p wZ wY
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL p wZ wY
RL p wZ wY
xs'
    (:>) (FL p) (RL p :> RL p) wX wY
_ -> [Char] -> (:>) (FL p) (FL p) wX wY
forall a. HasCallStack => [Char] -> a
error [Char]
"failed to commute common patches"
  where
    yids :: Set (PatchId p)
yids = [PatchId p] -> Set (PatchId p)
forall a. Ord a => [a] -> Set a
S.fromList ((forall wX wY. p wX wY -> PatchId p) -> FL p wX wZ -> [PatchId p]
forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b]
mapFL p wW wZ -> PatchId p
forall wX wY. p wX wY -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident FL p wX wZ
ys)

findCommonRL :: (Commute p, Ident p)
             => RL p wX wY
             -> RL p wX wZ
             -> Fork (RL p) (RL p) (RL p) wX wY wZ
findCommonRL :: forall (p :: * -> * -> *) wX wY wZ.
(Commute p, Ident p) =>
RL p wX wY -> RL p wX wZ -> Fork (RL p) (RL p) (RL p) wX wY wZ
findCommonRL RL p wX wY
xs RL p wX wZ
ys =
  case RL p wX wY -> RL p wX wZ -> (:>) (RL p) (RL p) wX wY
forall (p :: * -> * -> *) wX wY wZ.
(Commute p, Ident p) =>
RL p wX wY -> RL p wX wZ -> (:>) (RL p) (RL p) wX wY
findCommonWithThemRL RL p wX wY
xs RL p wX wZ
ys of
    RL p wX wZ
cxs :> RL p wZ wY
xs' ->
      case RL p wX wZ -> RL p wX wY -> (:>) (RL p) (RL p) wX wZ
forall (p :: * -> * -> *) wX wY wZ.
(Commute p, Ident p) =>
RL p wX wY -> RL p wX wZ -> (:>) (RL p) (RL p) wX wY
findCommonWithThemRL RL p wX wZ
ys RL p wX wY
xs of
        RL p wX wZ
cys :> RL p wZ wZ
ys' ->
          case RL p wX wZ
cxs RL p wX wZ -> RL p wX wZ -> EqCheck wZ wZ
forall (p :: * -> * -> *) wA wB wC.
Ident p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\^/= RL p wX wZ
cys of
            EqCheck wZ wZ
NotEq -> [Char] -> Fork (RL p) (RL p) (RL p) wX wY wZ
forall a. HasCallStack => [Char] -> a
error [Char]
"common patches aren't equal"
            EqCheck wZ wZ
IsEq -> RL p wX wZ
-> RL p wZ wY -> RL p wZ wZ -> Fork (RL p) (RL p) (RL p) wX wY wZ
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 RL p wX wZ
cxs RL p wZ wY
xs' RL p wZ wZ
RL p wZ wZ
ys'

findCommonWithThemRL
  :: (Commute p, Ident p) => RL p wX wY -> RL p wX wZ -> (RL p :> RL p) wX wY
findCommonWithThemRL :: forall (p :: * -> * -> *) wX wY wZ.
(Commute p, Ident p) =>
RL p wX wY -> RL p wX wZ -> (:>) (RL p) (RL p) wX wY
findCommonWithThemRL RL p wX wY
xs RL p wX wZ
ys =
  case (forall wU wV. p wU wV -> Bool)
-> RL p wX wY -> (:>) (FL p) (FL p :> RL p) wX wY
forall (p :: * -> * -> *) wX wY.
Commute p =>
(forall wU wV. p wU wV -> Bool)
-> RL p wX wY -> (:>) (FL p) (FL p :> RL p) wX wY
partitionRL' (Bool -> Bool
not (Bool -> Bool) -> (p wU wV -> Bool) -> p wU wV -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PatchId p -> Set (PatchId p) -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set (PatchId p)
yids) (PatchId p -> Bool) -> (p wU wV -> PatchId p) -> p wU wV -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p wU wV -> PatchId p
forall wX wY. p wX wY -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident) RL p wX wY
xs of
    FL p wX wZ
cxs :> FL p wZ wZ
NilFL :> RL p wZ wY
xs' -> FL p wX wZ -> RL p wX wZ
forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> RL a wX wZ
reverseFL FL p wX wZ
cxs RL p wX wZ -> RL p wZ wY -> (:>) (RL p) (RL p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wY
RL p wZ wY
xs'
    (:>) (FL p) (FL p :> RL p) wX wY
_ -> [Char] -> (:>) (RL p) (RL p) wX wY
forall a. HasCallStack => [Char] -> a
error [Char]
"failed to commute common patches"
  where
    yids :: Set (PatchId p)
yids = [PatchId p] -> Set (PatchId p)
forall a. Ord a => [a] -> Set a
S.fromList ((forall wX wY. p wX wY -> PatchId p) -> RL p wX wZ -> [PatchId p]
forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> RL a wX wY -> [b]
mapRL p wW wZ -> PatchId p
forall wX wY. p wX wY -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident RL p wX wZ
ys)

-- | Try to commute all patches matching any of the 'PatchId's in the set to the
-- head of an 'FL', i.e. backwards in history.
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 wU wV. p wU wV -> Bool)
-> RL p wX wX
-> RL p wX wX
-> FL p wX wY
-> (:>) (FL p) (RL p :> RL p) wX wY
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' ((PatchId p -> Set (PatchId p) -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set (PatchId p)
is) (PatchId p -> Bool) -> (p wU wV -> PatchId p) -> p wU wV -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p wU wV -> PatchId p
forall wX wY. p wX wY -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident) RL p wX wX
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL RL p wX wX
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL FL p wX wY
ps = (:>) (FL p) (RL p) wX wY -> Maybe ((:>) (FL p) (RL p) wX wY)
forall a. a -> Maybe a
Just (FL p wX wZ
prefix FL p wX wZ -> RL p wZ wY -> (:>) (FL p) (RL p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wY
RL p wZ wY
rest)
  | Bool
otherwise = Maybe ((:>) (FL p) (RL p) wX wY)
forall a. Maybe a
Nothing

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 (:>) p p wX wY -> Maybe ((:>) p p wX wY)
forall wX wY. (:>) p p wX wY -> Maybe ((:>) p p wX wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (p wX wZ
p p wX wZ -> p wZ wY -> (:>) p p wX wY
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') -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ p wX wZ -> PatchId p
forall wX wY. p wX wY -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wX wZ
p PatchId p -> PatchId p -> Bool
forall a. Eq a => a -> a -> Bool
== p wZ wY -> PatchId p
forall wX wY. p wX wY -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wZ wY
p' Bool -> Bool -> Bool
&& p wZ wY -> PatchId p
forall wX wY. p wX wY -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wZ wY
q PatchId p -> PatchId p -> Bool
forall a. Eq a => a -> a -> Bool
== p wX wZ -> PatchId p
forall wX wY. p wX wY -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wX wZ
q'
    Maybe ((:>) p p wX wY)
Nothing -> Maybe Bool
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))
  | p wZ wX -> PatchId p
forall wX wY. p wX wY -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wZ wX
p PatchId p -> PatchId p -> Bool
forall a. Eq a => a -> a -> Bool
== p wZ wY -> PatchId p
forall wX wY. p wX wY -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wZ wY
q =
      case (:>) (RL p) p wZ wY -> Maybe ((:>) p (RL p) wZ wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> Maybe ((:>) p (RL p) wX wY)
commuteRL (RL p wZ wZ
ps RL p wZ wZ -> p wZ wY -> (:>) (RL p) p wZ wY
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
_) -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ EqCheck wX wZ -> Bool
forall wA wB. EqCheck wA wB -> Bool
isIsEq (p wZ wX
p p wZ wX -> p wZ wZ -> EqCheck wX wZ
forall wA wB wC. p wA wB -> p wA wC -> EqCheck wB wC
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 -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
  | Bool
otherwise = Maybe Bool
forall a. Maybe a
Nothing

prop_equalImpliesSameIdentity :: (Eq2 p, Ident p)
                              => p wA wB -> p wC wD -> Maybe Bool
prop_equalImpliesSameIdentity :: forall (p :: * -> * -> *) wA wB wC wD.
(Eq2 p, Ident p) =>
p wA wB -> p wC wD -> Maybe Bool
prop_equalImpliesSameIdentity p wA wB
p p wC wD
q
  | p wA wB
p p wA wB -> p wC wD -> Bool
forall wA wB wC wD. p wA wB -> p wC wD -> Bool
forall (p :: * -> * -> *) wA wB wC wD.
Eq2 p =>
p wA wB -> p wC wD -> Bool
`unsafeCompare` p wC wD
q = Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ p wA wB -> PatchId p
forall wX wY. p wX wY -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wA wB
p PatchId p -> PatchId p -> Bool
forall a. Eq a => a -> a -> Bool
== p wC wD -> PatchId p
forall wX wY. p wX wY -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wC wD
q
  | Bool
otherwise = Maybe Bool
forall a. Maybe a
Nothing

-- Note the assumption of coinciding start states here!
prop_sameIdentityImpliesEqual :: (Eq2 p, Ident p)
                              => (p :\/: p) wX wY -> Maybe Bool
prop_sameIdentityImpliesEqual :: forall (p :: * -> * -> *) wX wY.
(Eq2 p, Ident p) =>
(:\/:) p p wX wY -> Maybe Bool
prop_sameIdentityImpliesEqual (p wZ wX
p :\/: p wZ wY
q)
  | p wZ wX -> PatchId p
forall wX wY. p wX wY -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wZ wX
p PatchId p -> PatchId p -> Bool
forall a. Eq a => a -> a -> Bool
== p wZ wY -> PatchId p
forall wX wY. p wX wY -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wZ wY
q = Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ EqCheck wX wY -> Bool
forall wA wB. EqCheck wA wB -> Bool
isIsEq (EqCheck wX wY -> Bool) -> EqCheck wX wY -> Bool
forall a b. (a -> b) -> a -> b
$ p wZ wX
p p wZ wX -> p wZ wY -> EqCheck wX wY
forall wA wB wC. p wA wB -> p wA wC -> EqCheck wB wC
forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= p wZ wY
q
  | Bool
otherwise = Maybe Bool
forall a. Maybe a
Nothing