-- 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. {-# OPTIONS_GHC -cpp -fglasgow-exts #-} {-# LANGUAGE CPP #-} -- , MagicHash, TypeOperators, GADTs #-} #include "gadts.h" module Darcs.Witnesses.Ordered ( EqCheck(..), isEq, (:>)(..), (:<)(..), (:\/:)(..), (:/\:)(..), (:||:)(..), FL(..), RL(..),Proof(..), #ifndef GADT_WITNESSES unsafeUnFL, unsafeFL, unsafeRL, unsafeUnRL, #endif lengthFL, mapFL, mapFL_FL, spanFL, foldlFL, allFL, splitAtFL, bunchFL, foldlRL, lengthRL, isShorterThanRL, mapRL, mapRL_RL, zipWithFL, unsafeMap_l2f, filterE, filterFL, reverseFL, reverseRL, (+>+), (+<+), nullFL, concatFL, concatRL, concatReverseFL, headRL, MyEq, unsafeCompare, (=\/=), (=/\=), consRLSealed, nullRL, unsafeCoerceP, unsafeCoerceP2 ) where #include "impossible.h" import GHC.Base (unsafeCoerce#) import Darcs.Witnesses.Show import Darcs.Witnesses.Sealed ( FlippedSeal(..), flipSeal ) data EqCheck C(a b) where IsEq :: EqCheck C(a a) NotEq :: EqCheck C(a b) instance Eq (EqCheck C(a b)) where IsEq == IsEq = True NotEq == NotEq = True _ == _ = False isEq :: EqCheck C(a b) -> Bool isEq IsEq = True isEq NotEq = False instance Show (EqCheck C(a b)) where show IsEq = "IsEq" show NotEq = "NotEq" data Proof a C(x y) where Proof :: a -> Proof a C(x x) 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)) class MyEq p where -- Minimal definition defines any one of unsafeCompare, =\/= and =/\=. unsafeCompare :: p C(a b) -> p C(c d) -> Bool unsafeCompare a b = IsEq == (a =/\= unsafeCoerceP b) (=\/=) :: p C(a b) -> p C(a c) -> EqCheck C(b c) a =\/= b | unsafeCompare a b = unsafeCoerceP IsEq | otherwise = NotEq (=/\=) :: p C(a c) -> p C(b c) -> EqCheck C(a b) a =/\= b | IsEq == (a =\/= unsafeCoerceP b) = unsafeCoerceP IsEq | otherwise = NotEq infix 4 =\/=, =/\= unsafeCoerceP :: a C(x y) -> a C(b c) unsafeCoerceP = unsafeCoerce# unsafeCoerceP2 :: t C(w x y z) -> t C(a b c d) unsafeCoerceP2 = unsafeCoerce# instance (Show2 a, Show2 b) => Show ( (a :> b) C(x y) ) where showsPrec d (x :> y) = showOp2 1 ":>" d x y instance (Show2 a, Show2 b) => Show2 (a :> b) where showsPrec2 = showsPrec 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 showsPrec2 = showsPrec 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 => Show2 (FL a) where showsPrec2 = showsPrec -- 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 filterFL :: (FORALL(x y) p C(x y) -> EqCheck C(x y)) -> FL p C(w z) -> FL p C(w z) filterFL _ NilFL = NilFL filterFL f (x:>:xs) | IsEq <- f x = filterFL f xs | otherwise = x :>: filterFL f xs filterE :: (a -> EqCheck C(x y)) -> [a] -> [Proof a C(x y)] filterE _ [] = [] filterE p (x:xs) | IsEq <- p x = Proof x : filterE p xs | otherwise = filterE p 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 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'') -- '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 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 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 unsafeMap_l2f :: (FORALL(w z) a -> b C(w z)) -> [a] -> FL b C(x y) unsafeMap_l2f _ [] = unsafeCoerceP NilFL unsafeMap_l2f f (x:xs) = f x :>: unsafeMap_l2f f xs 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) concatReverseFL :: FL (RL a) C(x y) -> RL a C(x y) concatReverseFL = concatRL . reverseFL headRL :: RL a C(x y) -> FlippedSeal a C(y) headRL (x:<:_) = flipSeal x headRL _ = impossible consRLSealed :: a C(y z) -> FlippedSeal (RL a) C(y) -> FlippedSeal (RL a) C(z) consRLSealed a (FlippedSeal as) = flipSeal $ a :<: as #ifndef GADT_WITNESSES -- These are useful for interfacing with modules which do not yet use type witnesses unsafeUnFL :: FL a -> [a] unsafeUnFL NilFL = [] unsafeUnFL (a:>:as) = a : unsafeUnFL as unsafeUnRL :: RL a -> [a] unsafeUnRL NilRL = [] unsafeUnRL (a:<:as) = a : unsafeUnRL as unsafeFL :: [a] -> FL a unsafeFL [] = NilFL unsafeFL (a:as) = a :>: unsafeFL as unsafeRL :: [a] -> RL a unsafeRL [] = NilRL unsafeRL (a:as) = a :<: unsafeRL as #endif