-- Copyright (C) 2007 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.Witnesses.Ordered
(
-- * Directed Types
-- $DirectedTypes
(:>)(..)
, FL(..)
, RL(..)
-- * Merge Types
-- $MergeTypes
, (:\/:)(..)
, (:/\:)(..)
, (:||:)(..)
, Fork(..)
-- * Functions for 'FL's and 'RL's
, nullFL
, nullRL
, lengthFL
, lengthRL
, mapFL
, mapRL
, mapFL_FL
, mapRL_RL
, foldlFL
, foldlRL
, allFL
, allRL
, anyFL
, anyRL
, filterFL
, filterRL
, splitAtFL
, splitAtRL
, filterOutFLFL
, filterOutRLRL
, reverseFL
, reverseRL
, (+>+)
, (+<+)
, (+>>+)
, (+<<+)
, concatFL
, concatRL
, dropWhileFL
, dropWhileRL
-- * 'FL' only
, bunchFL
, foldFL_M
, spanFL
, spanFL_M
, zipWithFL
, toFL
, mapFL_FL_M
, sequenceFL_
, eqFL
, eqFLRev
, eqFLUnsafe
, initsFL
-- * 'RL' only
, isShorterThanRL
, snocRLSealed
) where
import Prelude ()
import Darcs.Prelude
import Darcs.Patch.Witnesses.Show
import Darcs.Patch.Witnesses.Sealed
( FlippedSeal(..)
, flipSeal
, Sealed(..)
, FreeLeft
, unFreeLeft
, Sealed2(..)
, seal
)
import Darcs.Patch.Witnesses.Eq ( Eq2(..), EqCheck(..) )
-- * Directed Types
-- $DirectedTypes
-- Darcs patches have a notion of transforming between contexts. This
-- naturally leads us to container types that are \"directed\" and
-- transform from one context to another.
--
-- For example, the swap of names of files x and y could be represented
-- with the following sequence of patches:
--
-- @ Move x z ':>' Move y x ':>' Move z y @
--
-- or using forward lists, like
--
-- @ Move x z ':>:' Move y x ':>:' Move z y ':>:' NilFL @
-- | Directed Forward Pairs
data (a1 :> a2) wX wY = forall wZ . (a1 wX wZ) :> (a2 wZ wY)
infixr 1 :>
-- | Forward lists
data FL a wX wZ where
(:>:) :: a wX wY -> FL a wY wZ -> FL a wX wZ
NilFL :: FL a wX wX
-- | Reverse lists
data RL a wX wZ where
(:<:) :: RL a wX wY -> a wY wZ -> RL a wX wZ
NilRL :: RL a wX wX
instance Show2 a => Show (FL a wX wZ) where
showsPrec _ NilFL = showString "NilFL"
showsPrec d (x :>: xs) = showParen (d > prec) $ showsPrec2 (prec + 1) x .
showString " :>: " . showsPrec (prec + 1) xs
where prec = 5
instance Show2 a => Show1 (FL a wX) where
showDict1 = ShowDictClass
instance Show2 a => Show2 (FL a) where
showDict2 = ShowDictClass
instance Show2 a => Show (RL a wX wZ) where
showsPrec _ NilRL = showString "NilRL"
showsPrec d (xs :<: x) = showParen (d > prec) $ showsPrec (prec + 1) xs .
showString " :<: " . showsPrec2 (prec + 1) x
where prec = 5
instance Show2 a => Show1 (RL a wX) where
showDict1 = ShowDictClass
instance Show2 a => Show2 (RL a) where
showDict2 = ShowDictClass
instance (Show2 a, Show2 b) => Show1 ((a :> b) wX) where
showDict1 = ShowDictClass
-- * Merge Types
-- $MergeTypes
-- When we have two patches which commute and share the same pre-context we can
-- merge the patches. Whenever patches, or sequences of patches, share a
-- pre-context we say they are Forking Pairs (':\/:'). The same way, when
-- patches or sequences of patches, share a post-context we say they are
-- Joining Pairs (':/\:').
--
-- The following diagram shows the symmetry of merge types:
--
-- @ wZ
-- ':/\:'
-- a3 / \ a4
-- / \
-- wX wY
-- \ /
-- a1 \ / a2
-- ':\/:'
-- wZ
-- @
--
-- (non-haddock version)
-- wZ
-- :/\:
-- a3 / \ a4
-- / \
-- wX wY
-- \ /
-- a1 \ / a2
-- :\/:
-- wZ
--
infix 1 :/\:, :\/:, :||:
-- | Forking Pairs (Implicit starting context)
data (a1 :\/: a2) wX wY = forall wZ . (a1 wZ wX) :\/: (a2 wZ wY)
-- | Joining Pairs
data (a3 :/\: a4) wX wY = forall wZ . (a3 wX wZ) :/\: (a4 wY wZ)
-- | Forking Pair (Explicit starting context)
--
-- @ wX wY
-- \ /
-- \ /
-- \ /
-- wU
-- |
-- |
-- |
-- wA
-- @
--
-- (non-haddock version)
--
-- wX wY
-- \ /
-- \ /
-- \ /
-- wU
-- |
-- |
-- |
-- wA
--
data Fork common left right wA wX wY =
forall wU. Fork (common wA wU) (left wU wX) (right wU wY)
-- | Parallel Pairs
data (a1 :||: a2) wX wY = (a1 wX wY) :||: (a2 wX wY)
instance (Show2 a, Show2 b) => Show ( (a :> b) wX wY ) where
showsPrec d (x :> y) = showOp2 1 ":>" d x y
instance (Eq2 a, Eq2 b) => Eq2 (a :> b) where
(a1 :> b1) =\/= (a2 :> b2) | IsEq <- a1 =\/= a2 = b1 =\/= b2
| otherwise = NotEq
instance (Eq2 a, Eq2 b) => Eq ((a :> b) wX wY) where
(==) = unsafeCompare
instance (Show2 a, Show2 b) => Show2 (a :> b) where
showDict2 = ShowDictClass
instance (Show2 a, Show2 b) => Show ( (a :\/: b) wX wY ) where
showsPrec d (x :\/: y) = showOp2 9 ":\\/:" d x y
instance (Show2 a, Show2 b) => Show2 (a :\/: b) where
showDict2 = ShowDictClass
instance (Show2 a, Show2 b) => Show ( (a :/\: b) wX wY ) where
showsPrec d (x :/\: y) = showOp2 1 ":/\\:" d x y
instance (Show2 a, Show2 b) => Show2 ( (a :/\: b) ) where
showDict2 = ShowDictClass
-- * Functions
infixr 5 :>:, +>+
infixl 5 :<:, +<+
nullFL :: FL a wX wZ -> Bool
nullFL NilFL = True
nullFL _ = False
nullRL :: RL a wX wZ -> Bool
nullRL NilRL = True
nullRL _ = False
-- | @filterOutFLFL p xs@ deletes any @x@ in @xs@ for which @p x == IsEq@
-- (indicating that @x@ has no effect as far as we are concerned, and can be
-- safely removed from the chain)
filterOutFLFL :: (forall wX wY . p wX wY -> EqCheck wX wY) -> FL p wW wZ -> FL p wW wZ
filterOutFLFL _ NilFL = NilFL
filterOutFLFL f (x:>:xs) | IsEq <- f x = filterOutFLFL f xs
| otherwise = x :>: filterOutFLFL f xs
filterOutRLRL :: (forall wX wY . p wX wY -> EqCheck wX wY) -> RL p wW wZ -> RL p wW wZ
filterOutRLRL _ NilRL = NilRL
filterOutRLRL f (xs:<:x) | IsEq <- f x = filterOutRLRL f xs
| otherwise = filterOutRLRL f xs :<: x
filterRL :: (forall wX wY . p wX wY -> Bool) -> RL p wA wB -> [Sealed2 p]
filterRL _ NilRL = []
filterRL f (xs :<: x) | f x = Sealed2 x : (filterRL f xs)
| otherwise = filterRL f xs
(+>+) :: FL a wX wY -> FL a wY wZ -> FL a wX wZ
NilFL +>+ ys = ys
(x:>:xs) +>+ ys = x :>: xs +>+ ys
(+<+) :: RL a wX wY -> RL a wY wZ -> RL a wX wZ
xs +<+ NilRL = xs
xs +<+ (ys:<:y) = xs +<+ ys :<: y
reverseFL :: FL a wX wZ -> RL a wX wZ
reverseFL xs = r NilRL xs
where r :: RL a wL wM -> FL a wM wO -> RL a wL wO
r ls NilFL = ls
r ls (a:>:as) = r (ls:<:a) as
reverseRL :: RL a wX wZ -> FL a wX wZ
reverseRL xs = r NilFL xs
where r :: FL a wM wO -> RL a wL wM -> FL a wL wO
r ls NilRL = ls
r ls (as:<:a) = r (a:>:ls) as
concatFL :: FL (FL a) wX wZ -> FL a wX wZ
concatFL NilFL = NilFL
concatFL (a:>:as) = a +>+ concatFL as
concatRL :: RL (RL a) wX wZ -> RL a wX wZ
concatRL NilRL = NilRL
concatRL (as:<:a) = concatRL as +<+ a
spanFL :: (forall wW wY . a wW wY -> Bool) -> FL a wX wZ -> (FL a :> FL a) wX wZ
spanFL f (x:>:xs) | f x = case spanFL f xs of
ys :> zs -> (x:>:ys) :> zs
spanFL _ xs = NilFL :> xs
spanFL_M :: forall a m wX wZ. Monad m =>
(forall wW wY . a wW wY -> m Bool) -> FL a wX wZ
-> m ((FL a :> FL a) wX wZ)
spanFL_M f (x:>:xs) =
do
continue <- f x
if continue
then do (ys :> zs) <- spanFL_M f xs
return $ (x :>: ys) :> zs
else return $ NilFL :> (x :>: xs)
spanFL_M _ (NilFL) = return $ NilFL :> NilFL
splitAtFL :: Int -> FL a wX wZ -> (FL a :> FL a) wX wZ
splitAtFL 0 xs = NilFL :> xs
splitAtFL _ NilFL = NilFL :> NilFL
splitAtFL n (x:>:xs) = case splitAtFL (n-1) xs of
(xs':>xs'') -> (x:>:xs' :> xs'')
splitAtRL :: Int -> RL a wX wZ -> (RL a :> RL a) wX wZ
splitAtRL 0 xs = xs :> NilRL
splitAtRL _ NilRL = NilRL :> NilRL
splitAtRL n (xs:<:x) = case splitAtRL (n-1) xs of
(xs'':>xs') -> (xs'':> xs':<:x)
-- 'bunchFL n' groups patches into batches of n, except that it always puts
-- the first patch in its own group, this being a recognition that the
-- first patch is often *very* large.
bunchFL :: Int -> FL a wX wY -> FL (FL a) wX wY
bunchFL _ NilFL = NilFL
bunchFL n (x:>:xs) = (x :>: NilFL) :>: bFL xs
where bFL :: FL a wX wY -> FL (FL a) wX wY
bFL NilFL = NilFL
bFL bs = case splitAtFL n bs of
a :> b -> a :>: bFL b
-- | Monadic fold over an 'FL'
-- associating to the left, i.e. from left to right.
-- The order of arguments follows the standard 'foldM' from base.
foldFL_M :: Monad m
=> (forall wA wB. r wA -> p wA wB -> m (r wB))
-> r wX -> FL p wX wY -> m (r wY)
foldFL_M _ r NilFL = return r
foldFL_M f r (x :>: xs) = f r x >>= \r' -> foldFL_M f r' xs
allFL :: (forall wX wY . a wX wY -> Bool) -> FL a wW wZ -> Bool
allFL f xs = and $ mapFL f xs
anyFL :: (forall wX wY . a wX wY -> Bool) -> FL a wW wZ -> Bool
anyFL f xs = or $ mapFL f xs
allRL :: (forall wA wB . a wA wB -> Bool) -> RL a wX wY -> Bool
allRL f xs = and $ mapRL f xs
anyRL :: (forall wA wB . a wA wB -> Bool) -> RL a wX wY -> Bool
anyRL f xs = or $ mapRL f xs
foldlFL :: (forall wW wY . a -> b wW wY -> a) -> a -> FL b wX wZ -> a
foldlFL _ x NilFL = x
foldlFL f x (y:>:ys) = foldlFL f (f x y) ys
foldlRL :: (forall wW wY . a -> b wW wY -> a) -> a -> RL b wX wZ -> a
foldlRL _ x NilRL = x
foldlRL f x (ys:<:y) = foldlRL f (f x y) ys
mapFL_FL :: (forall wW wY . a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ
mapFL_FL _ NilFL = NilFL
mapFL_FL f (a:>:as) = f a :>: mapFL_FL f as
mapFL_FL_M :: Monad m => (forall wW wY . a wW wY -> m (b wW wY)) -> FL a wX wZ -> m (FL b wX wZ)
mapFL_FL_M _ NilFL = return NilFL
mapFL_FL_M f (a:>:as) = do b <- f a
bs <- mapFL_FL_M f as
return (b:>:bs)
sequenceFL_ :: Monad m => (forall wW wZ . a wW wZ -> m b) -> FL a wX wY -> m ()
sequenceFL_ f = sequence_ . mapFL f
zipWithFL :: (forall wX wY . a -> p wX wY -> q wX wY)
-> [a] -> FL p wW wZ -> FL q wW wZ
zipWithFL f (x:xs) (y :>: ys) = f x y :>: zipWithFL f xs ys
zipWithFL _ _ NilFL = NilFL
zipWithFL _ [] (_:>:_) = bug "zipWithFL called with too short a list"
mapRL_RL :: (forall wW wY . a wW wY -> b wW wY) -> RL a wX wZ -> RL b wX wZ
mapRL_RL _ NilRL = NilRL
mapRL_RL f (as:<:a) = mapRL_RL f as :<: f a
mapFL :: (forall wW wZ . a wW wZ -> b) -> FL a wX wY -> [b]
mapFL _ NilFL = []
mapFL f (a :>: b) = f a : mapFL f b
filterFL :: (forall wX wY . a wX wY -> Bool) -> FL a wW wZ -> [Sealed2 a]
filterFL _ NilFL = []
filterFL f (a :>: b) = if f a
then (Sealed2 a):(filterFL f b)
else filterFL f b
mapRL :: (forall wW wZ . a wW wZ -> b) -> RL a wX wY -> [b]
mapRL _ NilRL = []
mapRL f (as :<: a) = f a : mapRL f as
lengthFL :: FL a wX wZ -> Int
lengthFL xs = l xs 0
where l :: FL a wX wZ -> Int -> Int
l NilFL n = n
l (_:>:as) n = l as $! n+1
lengthRL :: RL a wX wZ -> Int
lengthRL xs = l xs 0
where l :: RL a wX wZ -> Int -> Int
l NilRL n = n
l (as:<:_) n = l as $! n+1
isShorterThanRL :: RL a wX wY -> Int -> Bool
isShorterThanRL _ n | n <= 0 = False
isShorterThanRL NilRL _ = True
isShorterThanRL (xs:<:_) n = isShorterThanRL xs (n-1)
snocRLSealed :: FlippedSeal (RL a) wY -> a wY wZ -> FlippedSeal (RL a) wZ
snocRLSealed (FlippedSeal as) a = flipSeal $ as :<: a
toFL :: [FreeLeft a] -> Sealed (FL a wX)
toFL [] = Sealed NilFL
toFL (x:xs) = case unFreeLeft x of Sealed y -> case toFL xs of Sealed ys -> Sealed (y :>: ys)
dropWhileFL :: (forall wX wY . a wX wY -> Bool) -> FL a wR wV -> FlippedSeal (FL a) wV
dropWhileFL _ NilFL = flipSeal NilFL
dropWhileFL p xs@(x:>:xs')
| p x = dropWhileFL p xs'
| otherwise = flipSeal xs
dropWhileRL :: (forall wX wY . a wX wY -> Bool) -> RL a wR wV -> Sealed (RL a wR)
dropWhileRL _ NilRL = seal NilRL
dropWhileRL p xs@(xs':<:x)
| p x = dropWhileRL p xs'
| otherwise = seal xs
-- |Check that two 'FL's are equal element by element.
-- This differs from the 'Eq2' instance for 'FL' which
-- uses commutation.
eqFL :: Eq2 a => FL a wX wY -> FL a wX wZ -> EqCheck wY wZ
eqFL NilFL NilFL = IsEq
eqFL (x:>:xs) (y:>:ys) | IsEq <- x =\/= y, IsEq <- eqFL xs ys = IsEq
eqFL _ _ = NotEq
eqFLRev :: Eq2 a => FL a wX wZ -> FL a wY wZ -> EqCheck wX wY
eqFLRev NilFL NilFL = IsEq
eqFLRev (x:>:xs) (y:>:ys) | IsEq <- eqFLRev xs ys, IsEq <- x =/\= y = IsEq
eqFLRev _ _ = NotEq
eqFLUnsafe :: Eq2 a => FL a wX wY -> FL a wZ wW -> Bool
eqFLUnsafe NilFL NilFL = True
eqFLUnsafe (x:>:xs) (y:>:ys) = unsafeCompare x y && eqFLUnsafe xs ys
eqFLUnsafe _ _ = False
infixr 5 +>>+
infixl 5 +<<+
-- | Prepend an 'RL' to an 'FL'. This traverses only the left hand side.
(+>>+) :: RL p wX wY -> FL p wY wZ -> FL p wX wZ
NilRL +>>+ ys = ys
(xs:<:x) +>>+ ys = xs +>>+ (x :>: ys)
-- | Append an 'FL' to an 'RL'. This traverses only the right hand side.
(+<<+) :: RL p wX wY -> FL p wY wZ -> RL p wX wZ
xs +<<+ NilFL = xs
xs +<<+ (y:>:ys) = (xs:<:y) +<<+ ys
initsFL :: FL p wX wY -> [Sealed ((p :> FL p) wX)]
initsFL NilFL = []
initsFL (x :>: xs) =
Sealed (x :> NilFL) :
map (\(Sealed (y :> xs')) -> Sealed (x :> y :>: xs')) (initsFL xs)