-- 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 #-} #include "gadts.h" module Darcs.Witnesses.Ordered ( (:>)(..), (:<)(..), (:\/:)(..), (:/\:)(..), (:||:)(..), FL(..), RL(..), lengthFL, mapFL, mapFL_FL, spanFL, foldlFL, allFL, anyFL, filterFL, splitAtFL, splitAtRL, bunchFL, foldlRL, lengthRL, isShorterThanRL, mapRL, mapRL_RL, zipWithFL, filterFLFL, filterRL, reverseFL, reverseRL, (+>+), (+<+), nullFL, concatFL, concatRL, consRLSealed, nullRL, toFL, dropWhileFL, dropWhileRL, spanFL_M, eqFL, eqFLRev, eqFLUnsafe ) where #include "impossible.h" import Darcs.Witnesses.Show import Darcs.Witnesses.Sealed ( FlippedSeal(..), flipSeal, Sealed(..), FreeLeft, unFreeLeft, Sealed2(..), seal ) import Darcs.Witnesses.Eq ( MyEq(..), EqCheck(..) ) data (a1 :> a2) C(x y) = FORALL(z) (a1 C(x z)) :> (a2 C(z y)) infixr 1 :> data (a1 :< a2) C(x y) = FORALL(z) (a1 C(z y)) :< (a2 C(x z)) infix 1 :< infix 1 :/\:, :\/:, :||: data (a1 :\/: a2) C(x y) = FORALL(z) (a1 C(z x)) :\/: (a2 C(z y)) data (a1 :/\: a2) C(x y) = FORALL(z) (a1 C(x z)) :/\: (a2 C(y z)) data (a1 :||: a2) C(x y) = (a1 C(x y)) :||: (a2 C(x y)) instance (Show2 a, Show2 b) => Show ( (a :> b) C(x y) ) 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) C(x y)) where (==) = unsafeCompare instance (MyEq a, MyEq b) => MyEq (a :< b) where (a1 :< b1) =\/= (a2 :< b2) | IsEq <- b1 =\/= b2 = a1 =\/= a2 | otherwise = NotEq instance (MyEq a, MyEq b) => Eq ((a :< b) C(x y)) where (==) = unsafeCompare instance (Show2 a, Show2 b) => Show2 (a :> b) where showDict2 = ShowDictClass instance (Show2 a, Show2 b) => Show ( (a :\/: b) C(x y) ) where showsPrec d (x :\/: y) = showOp2 9 ":\\/:" d x y instance (Show2 a, Show2 b) => Show2 (a :\/: b) where showDict2 = ShowDictClass infixr 5 :>:, :<:, +>+, +<+ -- forward list data FL a C(x z) where (:>:) :: a C(x y) -> FL a C(y z) -> FL a C(x z) NilFL :: FL a C(x x) instance Show2 a => Show (FL a C(x z)) 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 C(x)) where showDict1 = ShowDictClass instance Show2 a => Show2 (FL a) where showDict2 = ShowDictClass instance Show2 a => Show (RL a C(x z)) where showsPrec _ NilRL = showString "NilRL" showsPrec d (x :<: xs) = showParen (d > prec) $ showsPrec2 (prec + 1) x . showString " :<: " . showsPrec (prec + 1) xs where prec = 5 instance Show2 a => Show1 (RL a C(x)) where showDict1 = ShowDictClass instance Show2 a => Show2 (RL a) where showDict2 = ShowDictClass instance (Show2 a, Show2 b) => Show1 ((a :> b) C(x)) where showDict1 = ShowDictClass -- reverse list data RL a C(x z) where (:<:) :: a C(y z) -> RL a C(x y) -> RL a C(x z) NilRL :: RL a C(x x) nullFL :: FL a C(x z) -> Bool nullFL NilFL = True nullFL _ = False nullRL :: RL a C(x z) -> Bool nullRL NilRL = True nullRL _ = False filterFLFL :: (FORALL(x y) p C(x y) -> EqCheck C(x y)) -> FL p C(w z) -> FL p C(w z) filterFLFL _ NilFL = NilFL filterFLFL f (x:>:xs) | IsEq <- f x = filterFLFL f xs | otherwise = x :>: filterFLFL f xs filterRL :: (FORALL(x y) p C(x y) -> Bool) -> RL p C(a b) -> [Sealed2 p] filterRL _ NilRL = [] filterRL f (x :<: xs) | f x = Sealed2 x : (filterRL f xs) | otherwise = filterRL f xs (+>+) :: FL a C(x y) -> FL a C(y z) -> FL a C(x z) NilFL +>+ ys = ys (x:>:xs) +>+ ys = x :>: xs +>+ ys (+<+) :: RL a C(y z) -> RL a C(x y) -> RL a C(x z) NilRL +<+ ys = ys (x:<:xs) +<+ ys = x :<: xs +<+ ys reverseFL :: FL a C(x z) -> RL a C(x z) reverseFL xs = r NilRL xs where r :: RL a C(l m) -> FL a C(m o) -> RL a C(l o) r ls NilFL = ls r ls (a:>:as) = r (a:<:ls) as reverseRL :: RL a C(x z) -> FL a C(x z) reverseRL xs = r NilFL xs -- r (xs :> NilFL) where r :: FL a C(m o) -> RL a C(l m) -> FL a C(l o) r ls NilRL = ls r ls (a:<:as) = r (a:>:ls) as concatFL :: FL (FL a) C(x z) -> FL a C(x z) concatFL NilFL = NilFL concatFL (a:>:as) = a +>+ concatFL as concatRL :: RL (RL a) C(x z) -> RL a C(x z) concatRL NilRL = NilRL concatRL (a:<:as) = a +<+ concatRL as spanFL :: (FORALL(w y) a C(w y) -> Bool) -> FL a C(x z) -> (FL a :> FL a) C(x z) 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 C(x z). Monad m => (FORALL(w y) a C(w y) -> m Bool) -> FL a C(x z) -> m ((FL a :> FL a) C(x z)) 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 C(x z) -> (FL a :> FL a) C(x z) 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 C(x z) -> (RL a :< RL a) C(x z) splitAtRL 0 xs = NilRL :< xs splitAtRL _ NilRL = NilRL :< NilRL splitAtRL n (x:<:xs) = case splitAtRL (n-1) xs of (xs':<xs'') -> (x:<:xs' :< xs'') -- '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 C(x y) -> FL (FL a) C(x y) bunchFL _ NilFL = NilFL bunchFL n (x:>:xs) = (x :>: NilFL) :>: bFL xs where bFL :: FL a C(x y) -> FL (FL a) C(x y) bFL NilFL = NilFL bFL bs = case splitAtFL n bs of a :> b -> a :>: bFL b allFL :: (FORALL(x y) a C(x y) -> Bool) -> FL a C(w z) -> Bool allFL f xs = and $ mapFL f xs anyFL :: (FORALL(x y) a C(x y) -> Bool) -> FL a C(w z) -> Bool anyFL f xs = or $ mapFL f xs foldlFL :: (FORALL(w y) a -> b C(w y) -> a) -> a -> FL b C(x z) -> a foldlFL _ x NilFL = x foldlFL f x (y:>:ys) = foldlFL f (f x y) ys foldlRL :: (FORALL(w y) a -> b C(w y) -> a) -> a -> RL b C(x z) -> a foldlRL _ x NilRL = x foldlRL f x (y:<:ys) = foldlRL f (f x y) ys mapFL_FL :: (FORALL(w y) a C(w y) -> b C(w y)) -> FL a C(x z) -> FL b C(x z) mapFL_FL _ NilFL = NilFL mapFL_FL f (a:>:as) = f a :>: mapFL_FL f as zipWithFL :: (FORALL(x y) a -> p C(x y) -> q C(x y)) -> [a] -> FL p C(w z) -> FL q C(w z) 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(w y) a C(w y) -> b C(w y)) -> RL a C(x z) -> RL b C(x z) mapRL_RL _ NilRL = NilRL mapRL_RL f (a:<:as) = f a :<: mapRL_RL f as mapFL :: (FORALL(w z) a C(w z) -> b) -> FL a C(x y) -> [b] mapFL _ NilFL = [] mapFL f (a :>: b) = f a : mapFL f b filterFL :: (FORALL(x y) a C(x y) -> Bool) -> FL a C(w z) -> [Sealed2 a] filterFL _ NilFL = [] filterFL f (a :>: b) = if f a then (Sealed2 a):(filterFL f b) else filterFL f b mapRL :: (FORALL(w z) a C(w z) -> b) -> RL a C(x y) -> [b] mapRL _ NilRL = [] mapRL f (a :<: b) = f a : mapRL f b lengthFL :: FL a C(x z) -> Int lengthFL xs = l xs 0 where l :: FL a C(x z) -> Int -> Int l NilFL n = n l (_:>:as) n = l as $! n+1 lengthRL :: RL a C(x z) -> Int lengthRL xs = l xs 0 where l :: RL a C(x z) -> Int -> Int l NilRL n = n l (_:<:as) n = l as $! n+1 isShorterThanRL :: RL a C(x y) -> Int -> Bool isShorterThanRL _ n | n <= 0 = False isShorterThanRL NilRL _ = True isShorterThanRL (_:<:xs) n = isShorterThanRL xs (n-1) consRLSealed :: a C(y z) -> FlippedSeal (RL a) C(y) -> FlippedSeal (RL a) C(z) consRLSealed a (FlippedSeal as) = flipSeal $ a :<: as toFL :: [FreeLeft a] -> Sealed (FL a C(x)) toFL [] = Sealed NilFL toFL (x:xs) = case unFreeLeft x of Sealed y -> case toFL xs of Sealed ys -> Sealed (y :>: ys) dropWhileFL :: (FORALL(x y) a C(x y) -> Bool) -> FL a C(r v) -> FlippedSeal (FL a) C(v) dropWhileFL _ NilFL = flipSeal NilFL dropWhileFL p xs@(x:>:xs') | p x = dropWhileFL p xs' | otherwise = flipSeal xs dropWhileRL :: (FORALL(x y) a C(x y) -> Bool) -> RL a C(r v) -> Sealed (RL a C(r)) dropWhileRL _ NilRL = seal NilRL dropWhileRL p xs@(x:<:xs') | 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 C(x y) -> FL a C(x z) -> EqCheck C(y z) eqFL NilFL NilFL = IsEq eqFL (x:>:xs) (y:>:ys) | IsEq <- x =\/= y, IsEq <- eqFL xs ys = IsEq eqFL _ _ = NotEq eqFLRev :: MyEq a => FL a C(x z) -> FL a C(y z) -> EqCheck C(x y) eqFLRev NilFL NilFL = IsEq eqFLRev (x:>:xs) (y:>:ys) | IsEq <- eqFLRev xs ys, IsEq <- x =/\= y = IsEq eqFLRev _ _ = NotEq eqFLUnsafe :: MyEq a => FL a C(x y) -> FL a C(z w) -> Bool eqFLUnsafe NilFL NilFL = True eqFLUnsafe (x:>:xs) (y:>:ys) = unsafeCompare x y && eqFLUnsafe xs ys eqFLUnsafe _ _ = False