-- Copyright (C) 2003-2004 David Roundy
--
-- This program is free software; you can redistribute it and/or modify
-- it under the terms of the GNU General Public License as published by
-- the Free Software Foundation; either version 2, or (at your option)
-- any later version.
--
-- This program is distributed in the hope that it will be useful,
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-- GNU General Public License for more details.
--
-- You should have received a copy of the GNU General Public License
-- along with this program; see the file COPYING.  If not, write to
-- the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
-- Boston, MA 02110-1301, USA.

{-# LANGUAGE CPP , ScopedTypeVariables #-}

module Darcs.Patch.Depends
    ( getUncovered
    , areUnrelatedRepos
    , findCommonAndUncommon
    , mergeThem
    , findCommonWithThem
    , countUsThem
    , removeFromPatchSet
    , slightlyOptimizePatchset
    , getPatchesBeyondTag
    , splitOnTag
    , newsetUnion
    , newsetIntersection
    , findUncommon
    , merge2FL
    , getDeps
    , SPatchAndDeps
    ) where

import Prelude ()
import Darcs.Prelude

#include "impossible.h"

import Prelude hiding ( pi )
import Data.List ( delete, intersect, (\\) )
import Data.Maybe ( fromMaybe )
import qualified Data.ByteString.Char8 as BC ( unpack )
import Control.Arrow ( (&&&) )

import Darcs.Patch ( RepoPatch )
import Darcs.Patch.Apply( ApplyState )
import Darcs.Patch.Patchy ( Patchy )
import Darcs.Patch.Named ( Named (..), patch2patchinfo )
import Darcs.Patch.Named.Wrapped ( getdeps )
import Darcs.Patch.Choices ( Label, patchChoices, forceFirst
                           , PatchChoices, lpPatch, getChoices
                           , LabelledPatch, label )
import Darcs.Patch.Commute ( commute, commuteFL, commuteRL )
import Darcs.Patch.Info ( PatchInfo, isTag, showPatchInfoUI, _piName )
import Darcs.Patch.Merge ( Merge, mergeFL )
import Darcs.Patch.Permutations ( partitionFL, partitionRL )
import Darcs.Patch.PatchInfoAnd( PatchInfoAnd, hopefully, hopefullyM, info )
import Darcs.Patch.Set ( PatchSet(..), Tagged(..), SealedPatchSet, newset2RL,
                         appendPSFL )
import Darcs.Patch.Progress ( progressRL )
import Darcs.Patch.Witnesses.Eq ( EqCheck(..), (=\/=), (=/\=) )
import Darcs.Patch.Witnesses.Unsafe ( unsafeCoerceP, unsafeCoercePStart )
import Darcs.Patch.Witnesses.Ordered
    ( (:\/:)(..), (:/\:)(..), (:>)(..), Fork(..),
    (+>+), mapFL, RL(..), FL(..), isShorterThanRL,
    (+<+), reverseFL, reverseRL, mapRL, lengthFL, splitAtFL )
import Darcs.Patch.Witnesses.Sealed
    ( Sealed(..), FlippedSeal(..), flipSeal, seal, Sealed2(..), seal2 )

import Darcs.Util.Printer ( renderString, vcat, RenderMode(..) )
import Darcs.Util.Tree ( Tree )

{-
 - This module uses the following definitions:
 -
 - Explicit dependencies: the set of patches that a patch depends on "by name",
 - i.e. irrespective of (non-)commutation (non commuting patches are implicit
 - dependencies, or conflicts). In other words, the set of patch names in a tag
 - or patch recorded with --ask-deps.
 -
 - Covered: a patch p covers another, q, if p's explicit dependencies include
 - q. E.g. in a repo [a,b,t] where t is a tag and a,b have no explicit
 - dependencies, then t will cover a and b.
 -
 - "Clean" tag: a tag in a repository is clean if all patches prior to the tag
 - are (transitively-)covered by the tag. An obvious example of obtaining an
 - unclean tag is by pulling from one repo into another - the tag could have
 - been commuted past other patches. When patches are created, they are clean,
 - since they explicitly depend on all uncovered patches.
 -}

-- | S(ealed) Patch and his dependencies.
type SPatchAndDeps p = ( Sealed2 (LabelledPatch (Named p))
                       , Sealed2 (FL (LabelledPatch (Named p)))
                       )

-- | Searchs dependencies in @repoFL@ of the patches in @getDepsFL@.
getDeps :: (RepoPatch p, ApplyState p ~ Tree) =>
            FL (Named p) wA wR -> FL (PatchInfoAnd rt p) wX wY -> [SPatchAndDeps p]
getDeps repoFL getDepsFL =
        let repoChoices   = patchChoices repoFL
            getDepsFL'    = mapFL (BC.unpack . _piName . info) getDepsFL
            labelledDeps  = getLabelledDeps getDepsFL' repoChoices
        in
            map (deps repoChoices) labelledDeps
    where
        -- Search dependencies for the patch with label @l@ in @repoChoices@.
        deps :: (Patchy (Named p)) => PatchChoices (Named p) wX wY ->
                (String,Label) -> SPatchAndDeps p
        deps repoChoices (_,l) =
            case getChoices $ forceFirst l repoChoices of
                (ds :> _) -> let i = lengthFL ds
                             in case splitAtFL (i-1) ds of
                                    -- Separate last patch in list
                                    ds' :> (r :>: NilFL) -> (seal2 r, seal2 ds')
                                    _ -> impossible -- Because deps at least
                                                    -- has r, which is the patch
                                                    -- that we are looking at
                                                    -- dependencies.
        getLabelledDeps :: Patchy (Named p) => [String] ->
                           PatchChoices (Named p) x y -> [(String, Label)]
        getLabelledDeps patchnames repoChoices =
            case getChoices repoChoices of
                 a :> (b :> c) -> filterDepsFL patchnames a ++
                                  filterDepsFL patchnames b ++
                                  filterDepsFL patchnames c
        filterDepsFL :: [String] -> FL (LabelledPatch (Named p)) wX wY ->
                        [(String, Label)]
        filterDepsFL _ NilFL = []
        filterDepsFL patchnames (lp :>: lps) =
                                if fst dep `elem` patchnames
                                    then dep : filterDepsFL patchnames lps
                                    else filterDepsFL patchnames lps
            where
                lpTostring :: LabelledPatch (Named p) wA wB -> String
                lpTostring = BC.unpack . _piName . patch2patchinfo . lpPatch
                dep :: (String, Label)
                dep = lpTostring &&& label $ lp

{-|
taggedIntersection takes two 'PatchSet's and splits them into a /common/
intersection portion and two sets of patches.  The intersection, however,
is only lazily determined, so there is no guarantee that all intersecting
patches will be included in the intersection 'PatchSet'.  This is a pretty
efficient function, because it makes use of the already-broken-up nature of
'PatchSet's.

Note that the first argument to taggedIntersection should be
the repository that is more cheaply accessed (i.e. local), as
taggedIntersection does its best to reduce the number of
inventories that are accessed from its rightmost argument.
-}
taggedIntersection :: forall rt p wStart wX wY . Patchy p =>
                      PatchSet rt p wStart wX -> PatchSet rt p wStart wY ->
                      Fork (RL (Tagged rt p))
                           (RL (PatchInfoAnd rt p))
                           (RL (PatchInfoAnd rt p)) wStart wX wY
taggedIntersection (PatchSet NilRL ps1) s2 = Fork NilRL ps1 (newset2RL s2)
taggedIntersection s1 (PatchSet NilRL ps2) = Fork NilRL (newset2RL s1) ps2
taggedIntersection s1 (PatchSet (_ :<: Tagged t _ _) ps2)
    | Just (PatchSet ts1 ps1) <- maybeSplitSetOnTag (info t) s1 =
    Fork ts1 ps1 (unsafeCoercePStart ps2)
taggedIntersection s1 s2@(PatchSet (ts2 :<: Tagged t _ p) ps2) =
    case hopefullyM t of
        Just _ -> taggedIntersection s1 (PatchSet ts2 (p :<: t +<+ ps2))
        Nothing -> case splitOnTag (info t) s1 of
                       Just (PatchSet com NilRL :> us) ->
                           Fork com us (unsafeCoercePStart ps2)
                       Just _ -> impossible
                       Nothing -> Fork NilRL (newset2RL s1) (newset2RL s2)

-- |'maybeSplitSetOnTag' takes a tag's 'PatchInfo', @t0@, and a 'PatchSet' and
-- attempts to find @t0@ in one of the 'Tagged's in the PatchSet. If the tag is
-- found, the PatchSet is split up, on that tag, such that all later patches
-- are in the "since last tag" patch list. If the tag is not found, 'Nothing'
-- is returned.
maybeSplitSetOnTag :: PatchInfo -> PatchSet rt p wStart wX
                   -> Maybe (PatchSet rt p wStart wX)
maybeSplitSetOnTag t0 origSet@(PatchSet (ts :<: Tagged t _ pst) ps)
    | t0 == info t = Just origSet
    | otherwise = do
        PatchSet ts' ps' <- maybeSplitSetOnTag t0 (PatchSet ts (pst :<: t))
        Just $ PatchSet ts' (ps' +<+ ps)
maybeSplitSetOnTag _ _ = Nothing

getPatchesBeyondTag :: Patchy p => PatchInfo -> PatchSet rt p wStart wX
                    -> FlippedSeal (RL (PatchInfoAnd rt p)) wX
getPatchesBeyondTag t (PatchSet (_ :<: Tagged hp _ _) ps) | info hp == t =
    flipSeal ps
getPatchesBeyondTag t patchset@(PatchSet ts (ps :<: hp)) =
    if info hp == t
        then if getUncovered patchset == [info hp]
                 -- special case to avoid looking at redundant patches
                 then flipSeal NilRL
                 else case splitOnTag t patchset of
                     Just (_ :> e) -> flipSeal e
                     _ -> impossible
        else case getPatchesBeyondTag t (PatchSet ts ps) of
                 FlippedSeal xxs -> FlippedSeal (xxs :<: hp)
getPatchesBeyondTag t (PatchSet NilRL NilRL) =
    bug $ "tag\n" ++ renderString Encode (showPatchInfoUI t)
          ++ "\nis not in the patchset in getPatchesBeyondTag."
getPatchesBeyondTag t0 (PatchSet (ts :<: Tagged t _ ps) NilRL) =
    getPatchesBeyondTag t0 (PatchSet ts (ps :<: t))

-- |splitOnTag takes a tag's 'PatchInfo', and a 'PatchSet', and attempts to
-- find the tag in the PatchSet, returning a pair: the clean PatchSet "up to"
-- the tag, and a RL of patches after the tag; If the tag is not in the
-- PatchSet, we return Nothing.
splitOnTag :: Patchy p => PatchInfo -> PatchSet rt p wStart wX
           -> Maybe ((PatchSet rt p :> RL (PatchInfoAnd rt p)) wStart wX)
-- If the tag we are looking for is the first Tagged tag of the patchset, just
-- separate out the patchset's patches.
splitOnTag t (PatchSet ts@(_ :<: Tagged hp _ _) ps) | info hp == t =
    Just $ PatchSet ts NilRL :> ps
-- If the tag is the most recent patch in the set, we check if the patch is the
-- only non-depended-on patch in the set (i.e. it is a clean tag); creating a
-- new Tagged out of the patches and tag, and adding it to the patchset, if
-- this is the case. Otherwise, we try to make the tag clean.
splitOnTag t patchset@(PatchSet ts hps@(ps :<: hp)) | info hp == t =
    if getUncovered patchset == [t]
        then Just $ PatchSet (ts :<: Tagged hp Nothing ps) NilRL :> NilRL
        else case partitionRL ((`notElem` (t : ds)) . info) hps of
            -- Partition hps by those that are the tag and its explicit deps.
            tagAndDeps@(ds' :<: hp') :> nonDeps ->
                -- If @ds@ doesn't contain the tag of the first Tagged, that
                -- tag will also be returned by the call to getUncovered - so
                -- we need to unwrap the next Tagged in order to expose it to
                -- being partitioned out in the recursive call to splitOnTag.
                if getUncovered (PatchSet ts tagAndDeps) == [t]
                    then let tagged = Tagged hp' Nothing ds' in
                         return $ PatchSet (ts :<: tagged) NilRL :> nonDeps
                    else do
                        unfolded <- unwrapOneTagged $ PatchSet ts tagAndDeps
                        xx :> yy <- splitOnTag t unfolded
                        return $ xx :> (yy +<+ nonDeps)
            _ -> impossible
  where
    ds = getdeps (hopefully hp)
-- We drop the leading patch, to try and find a non-Tagged tag.
splitOnTag t (PatchSet ts (ps :<: p)) = do
    ns :> x <- splitOnTag t (PatchSet ts ps)
    return $ ns :> (x :<: p)
-- If there are no patches left, we "unfold" the next Tagged, and try again.
splitOnTag t0 patchset@(PatchSet (_ :<: Tagged _ _ _s) NilRL) =
    unwrapOneTagged patchset >>= splitOnTag t0
-- If we've checked all the patches, but haven't found the tag, return Nothing.
splitOnTag _ (PatchSet NilRL NilRL) = Nothing

-- |'unwrapOneTagged' unfolds a single Tagged object in a PatchSet, adding the
-- tag and patches to the PatchSet's patch list.
unwrapOneTagged :: (Monad m) => PatchSet rt p wX wY -> m (PatchSet rt p wX wY)
unwrapOneTagged (PatchSet (ts :<: Tagged t _ tps) ps) =
    return $ PatchSet ts (tps :<: t +<+ ps)
unwrapOneTagged _ = fail "called unwrapOneTagged with no Tagged's in the set"

-- | @getUncovered ps@ returns the 'PatchInfo' for all the patches in
--   @ps@ that are not depended on by anything else *through explicit
--   dependencies*. Tags are a likely candidate, although we may also
--   find some non-tag patches in this list.
--
--   Keep in mind that in a typical repository with a lot of tags, only a small
--   fraction of tags would be returned as they would be at least indirectly
--   depended on by the topmost ones.
getUncovered :: PatchSet rt p wStart wX -> [PatchInfo]
getUncovered patchset = case patchset of
    (PatchSet NilRL ps) -> findUncovered (mapRL infoAndExplicitDeps ps)
    (PatchSet (_ :<: Tagged t _ _) ps) ->
        findUncovered (mapRL infoAndExplicitDeps (NilRL :<: t +<+ ps))
  where
    findUncovered :: [(PatchInfo, Maybe [PatchInfo])] -> [PatchInfo]
    findUncovered [] = []
    findUncovered ((pi, Nothing) : rest) = pi : findUncovered rest
    findUncovered ((pi, Just deps) : rest) =
        pi : findUncovered (dropDepsIn deps rest)

    -- |dropDepsIn traverses the list of patches, dropping any patches that
    -- occur in the dependency list; when a patch is dropped, its dependencies
    -- are added to the dependency list used for later patches.
    dropDepsIn :: [PatchInfo] -> [(PatchInfo, Maybe [PatchInfo])]
               -> [(PatchInfo, Maybe [PatchInfo])]
    dropDepsIn [] pps = pps
    dropDepsIn _  []  = []
    dropDepsIn ds (hp : pps)
        | fst hp `elem` ds =
            let extraDeps = fromMaybe [] $ snd hp in
            dropDepsIn (extraDeps ++ delete (fst hp) ds) pps
        | otherwise = hp : dropDepsIn ds pps

    -- |infoAndExplicitDeps returns the patch info and (for tags only) the list
    -- of explicit dependencies of a patch.
    infoAndExplicitDeps :: PatchInfoAnd rt p wX wY
                        -> (PatchInfo, Maybe [PatchInfo])
    infoAndExplicitDeps p
        | isTag (info p) = (info p, getdeps `fmap` hopefullyM p)
        | otherwise = (info p, Nothing)

-- | @slightlyOptimizePatchset@ only works on the surface inventory
--   (see 'optimizePatchset') and only optimises at most one tag in
--   there, going for the most recent tag which has no non-depended
--   patch after it. Older tags won't be 'clean', which means the
--   PatchSet will not be in 'clean :> unclean' state.
slightlyOptimizePatchset :: PatchSet rt p wStart wX -> PatchSet rt p wStart wX
slightlyOptimizePatchset (PatchSet ps0 ts0) =
    sops $ PatchSet (prog ps0) ts0
  where
    prog = progressRL "Optimizing inventory"
    sops :: PatchSet rt p wStart wY -> PatchSet rt p wStart wY
    sops patchset@(PatchSet _ NilRL) = patchset
    sops patchset@(PatchSet ts (ps :<: hp))
        | isTag (info hp) =
            if getUncovered patchset == [info hp]
                -- exactly one tag and it depends on everything not already
                -- archived
                then PatchSet (ts :<: Tagged hp Nothing ps) NilRL
                -- other tags or other top-level patches too (so move past hp)
                else let ps' = sops $ PatchSet ts (prog ps) in
                     appendPSFL ps' (hp :>: NilFL)
        | otherwise = appendPSFL (sops $ PatchSet ts ps) (hp :>: NilFL)

removeFromPatchSet :: Patchy p => FL (PatchInfoAnd rt p) wX wY
                   -> PatchSet rt p wStart wY -> Maybe (PatchSet rt p wStart wX)
removeFromPatchSet bad (PatchSet ts ps) | all (`elem` mapRL info ps) (mapFL info bad) = do
    ps' <- fastRemoveSubsequenceRL (reverseFL bad) ps
    return (PatchSet ts ps')
removeFromPatchSet _ (PatchSet NilRL _) = Nothing
removeFromPatchSet bad (PatchSet (ts :<: Tagged t _ tps) ps) =
    removeFromPatchSet bad (PatchSet ts (tps :<: t +<+ ps))

fastRemoveSubsequenceRL :: Patchy p
                        => RL (PatchInfoAnd rt p) wY wZ
                        -> RL (PatchInfoAnd rt p) wX wZ
                        -> Maybe (RL (PatchInfoAnd rt p) wX wY)
fastRemoveSubsequenceRL NilRL ys = Just ys
fastRemoveSubsequenceRL (xs:<:x) ys = fastRemoveRL x ys >>= fastRemoveSubsequenceRL xs

findCommonAndUncommon :: forall rt p wStart wX wY . Patchy p
                      => PatchSet rt p wStart wX -> PatchSet rt p wStart wY
                      -> Fork (PatchSet rt p)
                              (FL (PatchInfoAnd rt p))
                              (FL (PatchInfoAnd rt p)) wStart wX wY
findCommonAndUncommon us them = case taggedIntersection us them of
    Fork common us' them' ->
        case partitionFL (infoIn them') $ reverseRL us' of
            _ :> bad@(_ :>: _) :> _ ->
                bug $ "Failed to commute common patches:\n"
                      ++ renderString Encode
                          (vcat $ mapRL (showPatchInfoUI . info) $ reverseFL bad)
            (common2 :> NilFL :> only_ours) ->
                case partitionFL (infoIn us') $ reverseRL them' of
                    _ :> bad@(_ :>: _) :> _ ->
                        bug $ "Failed to commute common patches:\n"
                            ++ renderString Encode (vcat $
                                mapRL (showPatchInfoUI . info) $ reverseFL bad)
                    _ :> NilFL :> only_theirs ->
                        Fork (PatchSet common (reverseFL common2))
                            only_ours (unsafeCoercePStart only_theirs)
  where
    infoIn inWhat = (`elem` mapRL info inWhat) . info

findCommonWithThem :: Patchy p
                   => PatchSet rt p wStart wX
                   -> PatchSet rt p wStart wY
                   -> (PatchSet rt p :> FL (PatchInfoAnd rt p)) wStart wX
findCommonWithThem us them = case taggedIntersection us them of
    Fork common us' them' ->
        case partitionFL ((`elem` mapRL info them') . info) $ reverseRL us' of
            _ :> bad@(_ :>: _) :> _ ->
                bug $ "Failed to commute common patches:\n"
                      ++ renderString Encode
                          (vcat $ mapRL (showPatchInfoUI . info) $ reverseFL bad)
            common2 :> _nilfl :> only_ours ->
                PatchSet common (reverseFL common2) :> unsafeCoerceP only_ours

findUncommon :: Patchy p
             => PatchSet rt p wStart wX -> PatchSet rt p wStart wY
             -> (FL (PatchInfoAnd rt p) :\/: FL (PatchInfoAnd rt p)) wX wY
findUncommon us them =
    case findCommonWithThem us them of
        _common :> us' -> case findCommonWithThem them us of
            _ :> them' -> unsafeCoercePStart us' :\/: them'

countUsThem :: Patchy p
            => PatchSet rt p wStart wX
            -> PatchSet rt p wStart wY
            -> (Int, Int)
countUsThem us them =
    case taggedIntersection us them of
        Fork _ us' them' -> let uu = mapRL info us'
                                tt = mapRL info them' in
                            (length $ uu \\ tt, length $ tt \\ uu)

mergeThem :: (Patchy p, Merge p)
          => PatchSet rt p wStart wX -> PatchSet rt p wStart wY
          -> Sealed (FL (PatchInfoAnd rt p) wX)
mergeThem us them =
    case taggedIntersection us them of
        Fork _ us' them' ->
            case merge2FL (reverseRL us') (reverseRL them') of
               them'' :/\: _ -> Sealed them''

newsetIntersection :: Patchy p
                   => [SealedPatchSet rt p wStart]
                   -> SealedPatchSet rt p wStart
newsetIntersection [] = seal $ PatchSet NilRL NilRL
newsetIntersection [x] = x
newsetIntersection (Sealed y : ys) =
    case newsetIntersection ys of
        Sealed z -> case taggedIntersection y z of
            Fork common a b -> case mapRL info a `intersect` mapRL info b of
                morecommon ->
                    case partitionRL (\e -> info e `notElem` morecommon) a of
                        commonps :> _ -> seal $ PatchSet common commonps

newsetUnion :: (Patchy p, Merge p)
            => [SealedPatchSet rt p wStart]
            -> SealedPatchSet rt p wStart
newsetUnion [] = seal $ PatchSet NilRL NilRL
newsetUnion [x] = x
newsetUnion (Sealed y@(PatchSet tsy psy) : Sealed y2 : ys) =
    case mergeThem y y2 of
        Sealed p2 ->
            newsetUnion $ seal (PatchSet tsy (psy +<+ reverseFL p2)) : ys

-- | Merge two FLs (say L and R), starting in a common context. The result is a
-- FL starting in the original end context of L, going to a new context that is
-- the result of applying all patches from R on top of patches from L.
--
-- While this function is similar to 'mergeFL', there are some important
-- differences to keep in mind:
--
-- * 'mergeFL' does not correctly deal with duplicate patches whereas this one
--   does
--   (Question from Eric Kow: in what sense? Why not fix 'mergeFL'?)
--   (bf: I guess what was meant here is that 'merge2FL' works in the
--    the way it does because it considers patch meta data whereas
--    'mergeFL' cannot since it must work for primitive patches, too.
merge2FL :: (Patchy p, Merge p)
         => FL (PatchInfoAnd rt p) wX wY
         -> FL (PatchInfoAnd rt p) wX wZ
         -> (FL (PatchInfoAnd rt p) :/\: FL (PatchInfoAnd rt 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')

areUnrelatedRepos :: Patchy p
                  => PatchSet rt p wStart wX
                  -> PatchSet rt p wStart wY -> Bool
areUnrelatedRepos us them =
    case taggedIntersection us them of
        Fork c u t -> checkit c u t
  where
    checkit (_ :<: Tagged{}) _ _ = False
    checkit _ u t | t `isShorterThanRL` 5 = False
                  | u `isShorterThanRL` 5 = False
                  | otherwise = null $ intersect (mapRL info u) (mapRL info t)

-- | Remove a patch from FL, using PatchInfo equality. The result is Just
-- whenever the patch has been found and removed. If the patch is not present
-- in the sequence at all or any commutation fails, we get Nothing. First two
-- cases are optimisations for the common cases where the head of the list is
-- the patch to remove, or the patch is not there at all.
--
-- A note on the witness types: the patch to be removed is typed as if it had
-- to be the first in the list, since it has the same pre-context as the list.
-- The types fit together (internally, in this module) because we commute the
-- patch to the front before removing it and commutation inside a sequence does
-- not change the sequence's contexts.
--
-- However, the use sites outside this module are something different. We
-- usually need coercions to get the patch(es) to be removed in shape. This is
-- not very nice but probably unavoidable given the approximative nature of
-- context witnesses.
fastRemoveFL :: Patchy p
             => PatchInfoAnd rt p wX wY -- this type assumes element is at the front
             -> FL (PatchInfoAnd rt p) wX wZ
             -> Maybe (FL (PatchInfoAnd rt p) wY wZ)
fastRemoveFL _ NilFL = Nothing
fastRemoveFL a (b :>: bs) | IsEq <- a =\/= b = Just bs
                          | info a `notElem` mapFL info bs = Nothing
fastRemoveFL a (b :>: bs) = do
    a' :> bs' <- pullout NilRL bs
    a'' :> b' <- commute (b :> a')
    IsEq <- return (a'' =\/= a)
    Just (b' :>: bs')
  where
    i = info a
    pullout :: Patchy p
            => RL (PatchInfoAnd rt p) wA wB
            -> FL (PatchInfoAnd rt p) wB wC
            -> Maybe ((PatchInfoAnd rt p :> FL (PatchInfoAnd rt p)) wA wC)
    pullout _ NilFL = Nothing
    pullout acc (x :>: xs)
        | info x == i = do x' :> acc' <- commuteRL (acc :> x)
                           Just (x' :> reverseRL acc' +>+ xs)
        | otherwise = pullout (acc :<: x) xs

-- | Same as 'fastRemoveFL' only for 'RL'.
fastRemoveRL :: Patchy p
             => PatchInfoAnd rt p wY wZ -- this type assumes element is at the back
             -> RL (PatchInfoAnd rt p) wX wZ
             -> Maybe (RL (PatchInfoAnd rt p) wX wY)
fastRemoveRL _ NilRL = Nothing
fastRemoveRL a (bs :<: b) | IsEq <- b =/\= a = Just bs
                          | info a `notElem` mapRL info bs = Nothing
fastRemoveRL a (bs :<: b) = do
    bs' :> a' <- pullout bs NilFL
    b' :> a'' <- commute (a' :> b)
    IsEq <- return (a'' =/\= a)
    Just (bs' :<: b')
  where
    i = info a
    pullout :: Patchy p
            => RL (PatchInfoAnd rt p) wA wB
            -> FL (PatchInfoAnd rt p) wB wC
            -> Maybe ((RL (PatchInfoAnd rt p) :> PatchInfoAnd rt p) wA wC)
    pullout NilRL _ = Nothing
    pullout (xs :<: x) acc
        | info x == i = do acc' :> x' <- commuteFL (x :> acc)
                           Just (xs +<+ reverseFL acc' :> x')
        | otherwise = pullout xs (x :>: acc)