-- 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. {-# LANGUAGE CPP #-} module Darcs.Patch.Witnesses.Ordered ( -- * Directed Types -- $DirectedTypes (:>)(..) , FL(..) , RL(..) -- * Merge Types -- $MergeTypes , (:\/:)(..) , (:/\:)(..) , (:||:)(..) , Fork(..) -- * Functions , lengthFL , mapFL , mapFL_FL , spanFL , foldlFL , allFL , anyFL , filterFL , splitAtFL , splitAtRL , bunchFL , foldlRL , lengthRL , isShorterThanRL , mapRL , mapRL_RL , zipWithFL , filterOutFLFL , filterOutRLRL , filterRL , reverseFL , reverseRL , (+>+) , (+<+) , nullFL , concatFL , concatRL , snocRLSealed , nullRL , toFL , dropWhileFL , dropWhileRL , spanFL_M , mapFL_FL_M , eqFL , eqFLRev , eqFLUnsafe ) where import Prelude () import Darcs.Prelude #include "impossible.h" import Darcs.Patch.Witnesses.Show import Darcs.Patch.Witnesses.Sealed ( FlippedSeal(..) , flipSeal , Sealed(..) , FreeLeft , unFreeLeft , Sealed2(..) , seal ) import Darcs.Patch.Witnesses.Eq ( MyEq(..), 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 (MyEq a, MyEq b) => MyEq (a :> b) where (a1 :> b1) =\/= (a2 :> b2) | IsEq <- a1 =\/= a2 = b1 =\/= b2 | otherwise = NotEq instance (MyEq a, MyEq 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 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 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) 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 'MyEq' instance for 'FL' which -- uses commutation. eqFL :: MyEq 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 :: MyEq 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 :: MyEq 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