-- Copyright (C) 2003 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.

module Darcs.Patch.Set
    ( PatchSet(..)
    , Tagged(..)
    , SealedPatchSet
    , Origin
    , progressPatchSet
    , patchSetInventoryHashes
    , patchSetTags
    , emptyPatchSet
    , appendPSFL
    , patchSet2RL
    , patchSet2FL
    , inOrderTags
    , patchSetSnoc
    , patchSetSplit
    , patchSetDrop
    ) where

import Darcs.Prelude
import Data.Maybe ( catMaybes )
import qualified Data.Set as S

import Darcs.Patch.Ident ( Ident(..), PatchId )
import Darcs.Patch.Info ( PatchInfo, piTag )
import Darcs.Patch.PatchInfoAnd ( PatchInfoAnd, info )
import Darcs.Patch.Witnesses.Sealed ( Sealed(..) )
import Darcs.Patch.Witnesses.Ordered
    ( FL, RL(..), (+<+), (+<<+), (:>)(..), reverseRL,
    mapRL_RL, concatRL, mapRL )
import Darcs.Patch.Witnesses.Show ( Show1, Show2 )

import Darcs.Util.Progress ( progress )
import Darcs.Util.ValidHash ( InventoryHash )

-- |'Origin' is a type used to represent the initial context of a repo.
data Origin

type SealedPatchSet p wStart = Sealed ((PatchSet p) wStart)

-- |The patches in a repository are stored in chunks broken up at \"clean\"
-- tags. A tag is clean if the only patches before it in the current
-- repository ordering are ones that the tag depends on (either directly
-- or indirectly). Each chunk is stored in a separate inventory file on disk.
--
-- A 'PatchSet' represents a repo's history as the list of patches since the
-- last clean tag, and then a list of patch lists each delimited by clean tags.
--
-- Because the invariants about clean tags can only be maintained if a
-- 'PatchSet' contains the whole history, the first witness is always forced
-- to be 'Origin'. The type still has two witnesses so it can easily be used
-- with combinators like ':>' and 'Fork'.
--
-- The history is lazily loaded from disk so does not normally need to be all
-- kept in memory.
data PatchSet p wStart wY where
    PatchSet :: RL (Tagged p) Origin wX -> RL (PatchInfoAnd p) wX wY
             -> PatchSet p Origin wY

deriving instance Show2 p => Show (PatchSet p wStart wY)

instance Show2 p => Show1 (PatchSet p wStart)

instance Show2 p => Show2 (PatchSet p)

type instance PatchId (PatchSet p) = S.Set PatchInfo

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

emptyPatchSet :: PatchSet p Origin Origin
emptyPatchSet :: forall (p :: * -> * -> *). PatchSet p Origin Origin
emptyPatchSet = RL (Tagged p) Origin Origin
-> RL (PatchInfoAnd p) Origin Origin -> PatchSet p Origin Origin
forall (p :: * -> * -> *) wY wY.
RL (Tagged p) Origin wY
-> RL (PatchInfoAnd p) wY wY -> PatchSet p Origin wY
PatchSet RL (Tagged p) Origin Origin
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL RL (PatchInfoAnd p) Origin Origin
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL

-- |A 'Tagged' is a single chunk of a 'PatchSet'.
-- It has a 'PatchInfo' representing a clean tag,
-- the hash of the previous inventory (if it exists),
-- and the list of patches since that previous inventory.
data Tagged p wX wZ where
    Tagged :: RL (PatchInfoAnd p) wX wY -> PatchInfoAnd p wY wZ -> Maybe InventoryHash
           -> Tagged p wX wZ

deriving instance Show2 p => Show (Tagged p wX wZ)

instance Show2 p => Show1 (Tagged p wX)

instance Show2 p => Show2 (Tagged p)


-- |'patchSet2RL' takes a 'PatchSet' and returns an equivalent, linear 'RL' of
-- patches.
patchSet2RL :: PatchSet p wStart wX -> RL (PatchInfoAnd p) wStart wX
patchSet2RL :: forall (p :: * -> * -> *) wStart wX.
PatchSet p wStart wX -> RL (PatchInfoAnd p) wStart wX
patchSet2RL (PatchSet RL (Tagged p) Origin wX
ts RL (PatchInfoAnd p) wX wX
ps) = RL (RL (PatchInfoAnd p)) wStart wX -> RL (PatchInfoAnd p) wStart wX
forall (a :: * -> * -> *) wX wZ. RL (RL a) wX wZ -> RL a wX wZ
concatRL ((forall wW wY. Tagged p wW wY -> RL (PatchInfoAnd p) wW wY)
-> RL (Tagged p) wStart wX -> RL (RL (PatchInfoAnd p)) wStart wX
forall (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> RL a wX wZ -> RL b wX wZ
mapRL_RL Tagged p wW wY -> RL (PatchInfoAnd p) wW wY
forall wW wY. Tagged p wW wY -> RL (PatchInfoAnd p) wW wY
forall (p :: * -> * -> *) wY wZ.
Tagged p wY wZ -> RL (PatchInfoAnd p) wY wZ
ts2rl RL (Tagged p) wStart wX
RL (Tagged p) Origin wX
ts) RL (PatchInfoAnd p) wStart wX
-> RL (PatchInfoAnd p) wX wX -> RL (PatchInfoAnd p) wStart wX
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> RL a wY wZ -> RL a wX wZ
+<+ RL (PatchInfoAnd p) wX wX
ps
  where
    ts2rl :: Tagged p wY wZ -> RL (PatchInfoAnd p) wY wZ
    ts2rl :: forall (p :: * -> * -> *) wY wZ.
Tagged p wY wZ -> RL (PatchInfoAnd p) wY wZ
ts2rl (Tagged RL (PatchInfoAnd p) wY wY
ps2 PatchInfoAnd p wY wZ
t Maybe InventoryHash
_) = RL (PatchInfoAnd p) wY wY
ps2 RL (PatchInfoAnd p) wY wY
-> PatchInfoAnd p wY wZ -> RL (PatchInfoAnd p) wY wZ
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: PatchInfoAnd p wY wZ
t

-- |'patchSet2FL' takes a 'PatchSet' and returns an equivalent, linear 'FL' of
-- patches.
patchSet2FL :: PatchSet p wStart wX -> FL (PatchInfoAnd p) wStart wX
patchSet2FL :: forall (p :: * -> * -> *) wStart wX.
PatchSet p wStart wX -> FL (PatchInfoAnd p) wStart wX
patchSet2FL = RL (PatchInfoAnd p) wStart wX -> FL (PatchInfoAnd p) wStart wX
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL (RL (PatchInfoAnd p) wStart wX -> FL (PatchInfoAnd p) wStart wX)
-> (PatchSet p wStart wX -> RL (PatchInfoAnd p) wStart wX)
-> PatchSet p wStart wX
-> FL (PatchInfoAnd p) wStart wX
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatchSet p wStart wX -> RL (PatchInfoAnd p) wStart wX
forall (p :: * -> * -> *) wStart wX.
PatchSet p wStart wX -> RL (PatchInfoAnd p) wStart wX
patchSet2RL

-- |'appendPSFL' takes a 'PatchSet' and a 'FL' of patches that "follow" the
-- PatchSet, and concatenates the patches into the PatchSet.
appendPSFL :: PatchSet p wStart wX -> FL (PatchInfoAnd p) wX wY
           -> PatchSet p wStart wY
appendPSFL :: forall (p :: * -> * -> *) wStart wX wY.
PatchSet p wStart wX
-> FL (PatchInfoAnd p) wX wY -> PatchSet p wStart wY
appendPSFL (PatchSet RL (Tagged p) Origin wX
ts RL (PatchInfoAnd p) wX wX
ps) FL (PatchInfoAnd p) wX wY
newps = RL (Tagged p) Origin wX
-> RL (PatchInfoAnd p) wX wY -> PatchSet p Origin wY
forall (p :: * -> * -> *) wY wY.
RL (Tagged p) Origin wY
-> RL (PatchInfoAnd p) wY wY -> PatchSet p Origin wY
PatchSet RL (Tagged p) Origin wX
ts (RL (PatchInfoAnd p) wX wX
ps RL (PatchInfoAnd p) wX wX
-> FL (PatchInfoAnd p) wX wY -> RL (PatchInfoAnd p) wX wY
forall (p :: * -> * -> *) wX wY wZ.
RL p wX wY -> FL p wY wZ -> RL p wX wZ
+<<+ FL (PatchInfoAnd p) wX wY
newps)

-- |Runs a progress action for each tag and patch in a given PatchSet, using
-- the passed progress message. Does not alter the PatchSet.
progressPatchSet :: String -> PatchSet p wStart wX -> PatchSet p wStart wX
progressPatchSet :: forall (p :: * -> * -> *) wStart wX.
String -> PatchSet p wStart wX -> PatchSet p wStart wX
progressPatchSet String
k (PatchSet RL (Tagged p) Origin wX
ts RL (PatchInfoAnd p) wX wX
ps) =
    RL (Tagged p) Origin wX
-> RL (PatchInfoAnd p) wX wX -> PatchSet p Origin wX
forall (p :: * -> * -> *) wY wY.
RL (Tagged p) Origin wY
-> RL (PatchInfoAnd p) wY wY -> PatchSet p Origin wY
PatchSet ((forall wW wY. Tagged p wW wY -> Tagged p wW wY)
-> RL (Tagged p) Origin wX -> RL (Tagged p) Origin wX
forall (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> RL a wX wZ -> RL b wX wZ
mapRL_RL Tagged p wW wY -> Tagged p wW wY
forall wW wY. Tagged p wW wY -> Tagged p wW wY
forall (p :: * -> * -> *) wY wZ. Tagged p wY wZ -> Tagged p wY wZ
progressTagged RL (Tagged p) Origin wX
ts) ((forall wW wY. PatchInfoAnd p wW wY -> PatchInfoAnd p wW wY)
-> RL (PatchInfoAnd p) wX wX -> RL (PatchInfoAnd p) wX wX
forall (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> RL a wX wZ -> RL b wX wZ
mapRL_RL PatchInfoAnd p wW wY -> PatchInfoAnd p wW wY
forall {a}. a -> a
forall wW wY. PatchInfoAnd p wW wY -> PatchInfoAnd p wW wY
prog RL (PatchInfoAnd p) wX wX
ps)
  where
    prog :: a -> a
prog = String -> a -> a
forall a. String -> a -> a
progress String
k

    progressTagged :: Tagged p wY wZ -> Tagged p wY wZ
    progressTagged :: forall (p :: * -> * -> *) wY wZ. Tagged p wY wZ -> Tagged p wY wZ
progressTagged (Tagged RL (PatchInfoAnd p) wY wY
tps PatchInfoAnd p wY wZ
t Maybe InventoryHash
h) = RL (PatchInfoAnd p) wY wY
-> PatchInfoAnd p wY wZ -> Maybe InventoryHash -> Tagged p wY wZ
forall (p :: * -> * -> *) wX wY wZ.
RL (PatchInfoAnd p) wX wY
-> PatchInfoAnd p wY wZ -> Maybe InventoryHash -> Tagged p wX wZ
Tagged ((forall wW wY. PatchInfoAnd p wW wY -> PatchInfoAnd p wW wY)
-> RL (PatchInfoAnd p) wY wY -> RL (PatchInfoAnd p) wY wY
forall (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> RL a wX wZ -> RL b wX wZ
mapRL_RL PatchInfoAnd p wW wY -> PatchInfoAnd p wW wY
forall {a}. a -> a
forall wW wY. PatchInfoAnd p wW wY -> PatchInfoAnd p wW wY
prog RL (PatchInfoAnd p) wY wY
tps) (PatchInfoAnd p wY wZ -> PatchInfoAnd p wY wZ
forall {a}. a -> a
prog PatchInfoAnd p wY wZ
t) Maybe InventoryHash
h

patchSetInventoryHashes :: PatchSet p wX wY -> [Maybe InventoryHash]
patchSetInventoryHashes :: forall (p :: * -> * -> *) wX wY.
PatchSet p wX wY -> [Maybe InventoryHash]
patchSetInventoryHashes (PatchSet RL (Tagged p) Origin wX
ts RL (PatchInfoAnd p) wX wY
_) = (forall wW wZ. Tagged p wW wZ -> Maybe InventoryHash)
-> RL (Tagged p) Origin wX -> [Maybe InventoryHash]
forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> RL a wX wY -> [b]
mapRL (\(Tagged RL (PatchInfoAnd p) wW wY
_ PatchInfoAnd p wY wZ
_ Maybe InventoryHash
mh) -> Maybe InventoryHash
mh) RL (Tagged p) Origin wX
ts

-- | The tag names of /all/ tags of a given 'PatchSet'.
patchSetTags :: PatchSet p wX wY -> [String]
patchSetTags :: forall (p :: * -> * -> *) wX wY. PatchSet p wX wY -> [String]
patchSetTags = [Maybe String] -> [String]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe String] -> [String])
-> (PatchSet p wX wY -> [Maybe String])
-> PatchSet p wX wY
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall wW wZ. PatchInfoAnd p wW wZ -> Maybe String)
-> RL (PatchInfoAnd p) wX wY -> [Maybe String]
forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> RL a wX wY -> [b]
mapRL (PatchInfo -> Maybe String
piTag (PatchInfo -> Maybe String)
-> (PatchInfoAnd p wW wZ -> PatchInfo)
-> PatchInfoAnd p wW wZ
-> Maybe String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatchInfoAnd p wW wZ -> PatchInfo
forall (p :: * -> * -> *) wA wB. PatchInfoAndG p wA wB -> PatchInfo
info) (RL (PatchInfoAnd p) wX wY -> [Maybe String])
-> (PatchSet p wX wY -> RL (PatchInfoAnd p) wX wY)
-> PatchSet p wX wY
-> [Maybe String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatchSet p wX wY -> RL (PatchInfoAnd p) wX wY
forall (p :: * -> * -> *) wStart wX.
PatchSet p wStart wX -> RL (PatchInfoAnd p) wStart wX
patchSet2RL

inOrderTags :: PatchSet p wS wX -> [PatchInfo]
inOrderTags :: forall (p :: * -> * -> *) wS wX. PatchSet p wS wX -> [PatchInfo]
inOrderTags (PatchSet RL (Tagged p) Origin wX
ts RL (PatchInfoAnd p) wX wX
_) = RL (Tagged p) Origin wX -> [PatchInfo]
forall (t1 :: * -> * -> *) wT wY.
RL (Tagged t1) wT wY -> [PatchInfo]
go RL (Tagged p) Origin wX
ts
  where go :: RL(Tagged t1) wT wY -> [PatchInfo]
        go :: forall (t1 :: * -> * -> *) wT wY.
RL (Tagged t1) wT wY -> [PatchInfo]
go (RL (Tagged t1) wT wY
ts' :<: Tagged RL (PatchInfoAnd t1) wY wY
_ PatchInfoAnd t1 wY wY
t Maybe InventoryHash
_) = PatchInfoAnd t1 wY wY -> PatchInfo
forall (p :: * -> * -> *) wA wB. PatchInfoAndG p wA wB -> PatchInfo
info PatchInfoAnd t1 wY wY
t PatchInfo -> [PatchInfo] -> [PatchInfo]
forall a. a -> [a] -> [a]
: RL (Tagged t1) wT wY -> [PatchInfo]
forall (t1 :: * -> * -> *) wT wY.
RL (Tagged t1) wT wY -> [PatchInfo]
go RL (Tagged t1) wT wY
ts'
        go RL (Tagged t1) wT wY
NilRL = []

patchSetSnoc :: PatchSet p wX wY -> PatchInfoAnd p wY wZ -> PatchSet p wX wZ
patchSetSnoc :: forall (p :: * -> * -> *) wX wY wZ.
PatchSet p wX wY -> PatchInfoAnd p wY wZ -> PatchSet p wX wZ
patchSetSnoc (PatchSet RL (Tagged p) Origin wX
ts RL (PatchInfoAnd p) wX wY
ps) PatchInfoAnd p wY wZ
p = RL (Tagged p) Origin wX
-> RL (PatchInfoAnd p) wX wZ -> PatchSet p Origin wZ
forall (p :: * -> * -> *) wY wY.
RL (Tagged p) Origin wY
-> RL (PatchInfoAnd p) wY wY -> PatchSet p Origin wY
PatchSet RL (Tagged p) Origin wX
ts (RL (PatchInfoAnd p) wX wY
ps RL (PatchInfoAnd p) wX wY
-> PatchInfoAnd p wY wZ -> RL (PatchInfoAnd p) wX wZ
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: PatchInfoAnd p wY wZ
p)

-- | Split a 'PatchSet' /before/ the latest known clean tag. The left part
-- is what comes before the tag, the right part is the tag and its
-- non-dependencies.
patchSetSplit :: PatchSet p wX wY
              -> (PatchSet p :> RL (PatchInfoAnd p)) wX wY
patchSetSplit :: forall (p :: * -> * -> *) wX wY.
PatchSet p wX wY -> (:>) (PatchSet p) (RL (PatchInfoAnd p)) wX wY
patchSetSplit (PatchSet (RL (Tagged p) Origin wY
ts :<: Tagged RL (PatchInfoAnd p) wY wY
ps' PatchInfoAnd p wY wX
t Maybe InventoryHash
_) RL (PatchInfoAnd p) wX wY
ps) =
  RL (Tagged p) Origin wY
-> RL (PatchInfoAnd p) wY wY -> PatchSet p Origin wY
forall (p :: * -> * -> *) wY wY.
RL (Tagged p) Origin wY
-> RL (PatchInfoAnd p) wY wY -> PatchSet p Origin wY
PatchSet RL (Tagged p) Origin wY
ts RL (PatchInfoAnd p) wY wY
ps' PatchSet p wX wY
-> RL (PatchInfoAnd p) wY wY
-> (:>) (PatchSet p) (RL (PatchInfoAnd p)) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> ((RL (PatchInfoAnd p) wY wY
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL RL (PatchInfoAnd p) wY wY
-> PatchInfoAnd p wY wX -> RL (PatchInfoAnd p) wY wX
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: PatchInfoAnd p wY wX
t) RL (PatchInfoAnd p) wY wX
-> RL (PatchInfoAnd p) wX wY -> RL (PatchInfoAnd p) wY wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> RL a wY wZ -> RL a wX wZ
+<+ RL (PatchInfoAnd p) wX wY
ps)
patchSetSplit (PatchSet RL (Tagged p) Origin wX
NilRL RL (PatchInfoAnd p) wX wY
ps) = RL (Tagged p) Origin Origin
-> RL (PatchInfoAnd p) Origin Origin -> PatchSet p Origin Origin
forall (p :: * -> * -> *) wY wY.
RL (Tagged p) Origin wY
-> RL (PatchInfoAnd p) wY wY -> PatchSet p Origin wY
PatchSet RL (Tagged p) Origin Origin
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL RL (PatchInfoAnd p) Origin Origin
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL PatchSet p wX Origin
-> RL (PatchInfoAnd p) Origin wY
-> (:>) (PatchSet p) (RL (PatchInfoAnd p)) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL (PatchInfoAnd p) wX wY
RL (PatchInfoAnd p) Origin wY
ps

-- | Drop the last @n@ patches from the given 'PatchSet'.
patchSetDrop :: Int
             -> PatchSet p wStart wX
             -> SealedPatchSet p wStart
patchSetDrop :: forall (p :: * -> * -> *) wStart wX.
Int -> PatchSet p wStart wX -> SealedPatchSet p wStart
patchSetDrop Int
n PatchSet p wStart wX
ps | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = PatchSet p wStart wX -> Sealed (PatchSet p wStart)
forall (a :: * -> *) wX. a wX -> Sealed a
Sealed PatchSet p wStart wX
ps
patchSetDrop Int
n (PatchSet (RL (Tagged p) Origin wY
ts :<: Tagged RL (PatchInfoAnd p) wY wY
ps PatchInfoAnd p wY wX
t Maybe InventoryHash
_) RL (PatchInfoAnd p) wX wX
NilRL) =
  Int -> PatchSet p wStart wX -> Sealed (PatchSet p wStart)
forall (p :: * -> * -> *) wStart wX.
Int -> PatchSet p wStart wX -> SealedPatchSet p wStart
patchSetDrop Int
n (PatchSet p wStart wX -> Sealed (PatchSet p wStart))
-> PatchSet p wStart wX -> Sealed (PatchSet p wStart)
forall a b. (a -> b) -> a -> b
$ RL (Tagged p) Origin wY
-> RL (PatchInfoAnd p) wY wX -> PatchSet p Origin wX
forall (p :: * -> * -> *) wY wY.
RL (Tagged p) Origin wY
-> RL (PatchInfoAnd p) wY wY -> PatchSet p Origin wY
PatchSet RL (Tagged p) Origin wY
ts (RL (PatchInfoAnd p) wY wY
ps RL (PatchInfoAnd p) wY wY
-> PatchInfoAnd p wY wX -> RL (PatchInfoAnd p) wY wX
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: PatchInfoAnd p wY wX
t)
patchSetDrop Int
_ (PatchSet RL (Tagged p) Origin wX
NilRL RL (PatchInfoAnd p) wX wX
NilRL) = PatchSet p wStart Origin -> Sealed (PatchSet p wStart)
forall (a :: * -> *) wX. a wX -> Sealed a
Sealed (PatchSet p wStart Origin -> Sealed (PatchSet p wStart))
-> PatchSet p wStart Origin -> Sealed (PatchSet p wStart)
forall a b. (a -> b) -> a -> b
$ RL (Tagged p) Origin Origin
-> RL (PatchInfoAnd p) Origin Origin -> PatchSet p Origin Origin
forall (p :: * -> * -> *) wY wY.
RL (Tagged p) Origin wY
-> RL (PatchInfoAnd p) wY wY -> PatchSet p Origin wY
PatchSet RL (Tagged p) Origin Origin
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL RL (PatchInfoAnd p) Origin Origin
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL
patchSetDrop Int
n (PatchSet RL (Tagged p) Origin wX
ts (RL (PatchInfoAnd p) wX wY
ps :<: PatchInfoAnd p wY wX
_)) = Int -> PatchSet p wStart wY -> Sealed (PatchSet p wStart)
forall (p :: * -> * -> *) wStart wX.
Int -> PatchSet p wStart wX -> SealedPatchSet p wStart
patchSetDrop (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (PatchSet p wStart wY -> Sealed (PatchSet p wStart))
-> PatchSet p wStart wY -> Sealed (PatchSet p wStart)
forall a b. (a -> b) -> a -> b
$ RL (Tagged p) Origin wX
-> RL (PatchInfoAnd p) wX wY -> PatchSet p Origin wY
forall (p :: * -> * -> *) wY wY.
RL (Tagged p) Origin wY
-> RL (PatchInfoAnd p) wY wY -> PatchSet p Origin wY
PatchSet RL (Tagged p) Origin wX
ts RL (PatchInfoAnd p) wX wY
ps