module Darcs.Patch.Ident
    ( Ident(..)
    , SignedIdent
    , PatchId
    , SignedId(..)
    , StorableId(..)
    , IdEq2(..)
    , merge2FL
    , fastRemoveFL
    , fastRemoveRL
    , fastRemoveSubsequenceRL
    , findCommonFL
    , commuteToPrefix
    , commuteToPostfix
    , commuteWhatWeCanToPostfix
    -- * Properties
    , 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 of patches that have an identity.

It generalizes named prim patches a la camp (see Darcs.Patch.Prim.Named) and
Named patches i.e. those with a PatchInfo.

Patch identity should be invariant under commutation: if there is also an
@instance 'Commute' p@, then

prop> commute (p :> q) == Just (q' :> p') => ident p == ident p' && ident q == ident q'

The converse should also be true: patches with the same identity can be
commuted (back) to the same context and then compare equal. Assuming

@
  p :: p wX wY, (ps :> q) :: (RL p :> p) wX wZ
@

then

prop> ident p == ident q => commuteRL (ps :> q) == Just (p :> _)

As a special case we get that parallel patches with the same identity are
equal: if @p :: p wX wY, q :: p wX wZ@, then

prop> ident p == ident q => p =\/= q == IsEq

In general, comparing patches via their identity is coarser than
(structural) equality, so we only have

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

{- | 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 a@ can be parsed by 'readId' to produce @a@.
-}
class StorableId a where
  readId :: Parser a
  showId :: ShowPatchFor -> a -> Doc

-- | Faster equality tests for patches with an identity.
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 =\^/= q = if ident p == ident q then unsafeCoercePEnd IsEq else NotEq
  default (=/^\=) :: Ident p => p wA wC -> p wB wC -> EqCheck wA wB
  p =/^\= q = if ident p == ident q then unsafeCoercePStart IsEq else NotEq

-- | The 'Commute' requirement here is not technically needed but makes
-- sense logically.
instance (Commute p, Ident p) => IdEq2 (FL p) where
  ps =\^/= qs
    | S.fromList (mapFL ident ps) == S.fromList (mapFL ident qs) = unsafeCoercePEnd IsEq
    | otherwise = NotEq
  ps =/^\= qs
    | S.fromList (mapFL ident ps) == S.fromList (mapFL ident qs) = unsafeCoercePStart IsEq
    | otherwise = NotEq

-- | This function is similar to 'merge', but with one important
-- difference: 'merge' works on patches for which there is not necessarily a
-- concept of identity (e.g. primitive patches, conflictors, etc). Thus it does
-- not even try to recognize patches that are common to both sequences. Instead
-- these are passed on to the Merge instance for single patches. This instance
-- may handle duplicate patches by creating special patches (Duplicate,
-- Conflictor).
-- 
-- We do not want this to happen for named patches, or in general for patches
-- with an identity. Instead, we want to
-- /discard/ one of the two duplicates, retaining only one copy. This is done
-- by the fastRemoveFL calls below. We call mergeFL only after we have ensured
-- that the head of the left hand side does not occur in the right hand side.
merge2FL :: (Commute p, Merge p, Ident p)
         => FL p wX wY
         -> FL p wX wZ
         -> (FL p :/\: FL p) wY wZ
merge2FL xs NilFL = NilFL :/\: xs
merge2FL NilFL ys = ys :/\: NilFL
merge2FL xs (y :>: ys)
  | Just xs' <- fastRemoveFL y xs = merge2FL xs' ys
merge2FL (x :>: xs) ys
  | Just ys' <- fastRemoveFL x ys = merge2FL xs ys'
  | otherwise =
    case mergeFL (x :\/: ys) of
      ys' :/\: x' ->
        case merge2FL xs ys' of
          ys'' :/\: xs' -> ys'' :/\: (x' :>: xs')

{-# 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.
fastRemoveFL :: forall p wX wY wZ. (Commute p, Ident p)
             => p wX wY
             -> FL p wX wZ
             -> Maybe (FL p wY wZ)
fastRemoveFL a bs
  | i `notElem` mapFL ident bs = Nothing
  | otherwise = do
      _ :> bs' <- pullout NilRL bs
      Just (unsafeCoercePStart bs')
  where
    i = ident a
    pullout :: RL p wA wB -> FL p wB wC -> Maybe ((p :> FL p) wA wC)
    pullout _ NilFL = Nothing
    pullout acc (x :>: xs)
      | ident x == i = do
          x' :> acc' <- commuteRL (acc :> x)
          Just (x' :> acc' +>>+ xs)
      | otherwise = pullout (acc :<: x) 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 a bs
  | i `notElem` mapRL ident bs = Nothing
  | otherwise = do
      bs' :> _ <- pullout bs NilFL
      Just (unsafeCoercePEnd bs')
  where
    i = ident a
    pullout :: RL p wA wB -> FL p wB wC -> Maybe ((RL p :> p) wA wC)
    pullout NilRL _ = Nothing
    pullout (xs :<: x) acc
      | ident x == i = do
          acc' :> x' <- commuteFL (x :> acc)
          Just (xs +<<+ acc' :> x')
      | otherwise = pullout xs (x :>: acc)

fastRemoveSubsequenceRL :: (Commute p, Ident p)
                        => RL p wY wZ
                        -> RL p wX wZ
                        -> Maybe (RL p wX wY)
fastRemoveSubsequenceRL NilRL ys = Just ys
fastRemoveSubsequenceRL (xs :<: x) ys =
  fastRemoveRL x ys >>= fastRemoveSubsequenceRL 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, similar to 'merge2FL'.
findCommonFL :: (Commute p, Ident p)
             => FL p wX wY
             -> FL p wX wZ
             -> Fork (FL p) (FL p) (FL p) wX wY wZ
findCommonFL xs ys =
  case commuteToPrefix commonIds xs of
    Nothing -> error "failed to commute common patches (lhs)"
    Just (cxs :> xs') ->
      case commuteToPrefix commonIds ys of
        Nothing -> error "failed to commute common patches (rhs)"
        Just (cys :> ys') ->
          case cxs =\^/= cys of
            NotEq -> error "common patches aren't equal"
            IsEq -> Fork cxs (reverseRL xs') (reverseRL ys')
  where
    commonIds =
      S.fromList (mapFL ident xs) `S.intersection` S.fromList (mapFL ident ys)

-- | Try to commute patches matching any of the 'PatchId's in the set to the
-- head of an 'FL', i.e. backwards in history. It is not required that all the
-- 'PatchId's are found in the sequence, but if they do then the traversal
-- terminates as soon as the set is exhausted.
commuteToPrefix :: (Commute p, Ident p)
                => S.Set (PatchId p) -> FL p wX wY -> Maybe ((FL p :> RL p) wX wY)
commuteToPrefix is ps
  | prefix :> NilRL :> rest <-
      partitionFL' ((`S.member` is) . ident) NilRL NilRL ps = Just (prefix :> rest)
  | otherwise = Nothing

-- | Try to commute patches matching any of the 'PatchId's in the set to the
-- head of an 'RL', i.e. forwards in history. It is not required that all the
-- 'PatchId's are found in the sequence, but if they do then the traversal
-- terminates as soon as the set is exhausted.
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 ids patches = push ids (patches :> NilFL)
  where
    push :: S.Set (PatchId p) -> (RL p :> FL p) wA wB -> Maybe ((FL p :> RL p) wA wB)
    push _ (NilRL :> left) = return (left :> NilRL) -- input RL is ehausted
    push is (ps :> left)
      | S.null is = return (ps +>>+ left :> NilRL) -- set of IDs is exhausted
    push is (ps :<: p :> left)
      | let i = ident p
      , i `S.member` is = do
          left' :> p' <- commuteFL (p :> left)
          left'' :> right <- push (S.delete i is) (ps :> left')
          return (left'' :> right :<: p')
      | otherwise = push is (ps :> p :>: left)

-- | Like 'commuteToPostfix' but drag dependencies with us.
commuteWhatWeCanToPostfix :: forall p wX wY. (Commute p, Ident p)
                          => S.Set (PatchId p) -> RL p wX wY -> (FL p :> RL p) wX wY
commuteWhatWeCanToPostfix ids patches = push ids (patches :> NilFL)
  where
    push :: S.Set (PatchId p) -> (RL p :> FL p) wA wB -> (FL p :> RL p) wA wB
    push _ (NilRL :> left) = left :> NilRL -- input RL is ehausted
    push is (ps :> left)
      | S.null is = ps +>>+ left :> NilRL -- set of IDs is exhausted
    push is (ps :<: p :> left)
      | let i = ident p
      , i `S.member` is =
          case commuteWhatWeCanFL (p :> left) of
            left' :> p' :> deps ->
              case push (S.delete i is) (ps :> left') of
                left'' :> right -> left'' :> (right :<: p' +<<+ deps)
      | otherwise = push is (ps :> p :>: left)

prop_identInvariantUnderCommute :: (Commute p, Ident p)
                                => (p :> p) wX wY -> Maybe Bool
prop_identInvariantUnderCommute (p :> q) =
  case commute (p :> q) of
    Just (q' :> p') -> Just $ ident p == ident p' && ident q == ident q'
    Nothing -> Nothing

prop_sameIdentityImpliesCommutable :: (Commute p, Eq2 p, Ident p)
                                   => (p :\/: (RL p :> p)) wX wY -> Maybe Bool
prop_sameIdentityImpliesCommutable (p :\/: (ps :> q))
  | ident p == ident q =
      case commuteRL (ps :> q) of
        Just (p' :> _) -> Just $ isIsEq (p =\/= p')
        Nothing -> Just False
  | otherwise = Nothing

prop_equalImpliesSameIdentity :: (Eq2 p, Ident p)
                              => (p :\/: p) wX wY -> Maybe Bool
prop_equalImpliesSameIdentity (p :\/: q)
  | IsEq <- p =\/= q = Just $ ident p == ident q
  | otherwise = Nothing