src/Darcs/Ordered.lhs

   1 %  Copyright (C) 2007 David Roundy
   2 %
   3 %  This program is free software; you can redistribute it and/or modify
   4 %  it under the terms of the GNU General Public License as published by
   5 %  the Free Software Foundation; either version 2, or (at your option)
   6 %  any later version.
   7 %
   8 %  This program is distributed in the hope that it will be useful,
   9 %  but WITHOUT ANY WARRANTY; without even the implied warranty of
  10 %  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  11 %  GNU General Public License for more details.
  12 %
  13 %  You should have received a copy of the GNU General Public License
  14 %  along with this program; see the file COPYING.  If not, write to
  15 %  the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
  16 %  Boston, MA 02110-1301, USA.
  17
  18 \begin{code}
  19 {-# OPTIONS_GHC -cpp -fglasgow-exts #-}
  20 {-# LANGUAGE CPP #-}
  21 -- , MagicHash, TypeOperators, GADTs #-}
  22
  23 #include "gadts.h"
  24
  25 module Darcs.Ordered ( EqCheck(..), isEq, (:>)(..), (:<)(..), (:\/:)(..), (:/\:)(..),
  26                              FL(..), RL(..),Proof(..),
  27 #ifndef GADT_WITNESSES
  28                              unsafeUnFL, unsafeFL, unsafeRL, unsafeUnRL,
  29 #endif
  30                              lengthFL, mapFL, mapFL_FL, spanFL, foldlFL, allFL,
  31                              splitAtFL, bunchFL, foldlRL,
  32                              lengthRL, isShorterThanRL, mapRL, mapRL_RL, zipWithFL,
  33                              unsafeMap_l2f, filterE, filterFL,
  34                              reverseFL, reverseRL, (+>+), (+<+),
  35                              nullFL, concatFL, concatRL, concatReverseFL, headRL,
  36                              MyEq, unsafeCompare, (=\/=), (=/\=),
  37                              consRLSealed, nullRL,
  38                              unsafeCoerceP, unsafeCoerceP2
  39                            ) where
  40
  41 #include "impossible.h"
  42 import GHC.Base (unsafeCoerce#)
  43 import Darcs.Show
  44 import Darcs.Sealed ( FlippedSeal(..), flipSeal )
  45
  46 data EqCheck C(a b) where
  47     IsEq :: EqCheck C(a a)
  48     NotEq :: EqCheck C(a b)
  49
  50 instance Eq (EqCheck C(a b)) where
  51     IsEq == IsEq = True
  52     NotEq == NotEq = True
  53     _ == _ = False
  54
  55 isEq :: EqCheck C(a b) -> Bool
  56 isEq IsEq = True
  57 isEq NotEq = False
  58
  59 instance Show (EqCheck C(a b)) where
  60     show IsEq = "IsEq"
  61     show NotEq = "NotEq"
  62
  63 data Proof a C(x y) where
  64     Proof :: a -> Proof a C(x x)
  65
  66 data (a1 :> a2) C(x y) = FORALL(z) (a1 C(x z)) :> (a2 C(z y))
  67 infixr 1 :>
  68 data (a1 :< a2) C(x y) = FORALL(z) (a1 C(z y)) :< (a2 C(x z))
  69 infix 1 :<
  70 infix 1 :/\:, :\/:
  71 data (a1 :\/: a2) C(x y) = FORALL(z) (a1 C(z x)) :\/: (a2 C(z y))
  72 data (a1 :/\: a2) C(x y) = FORALL(z) (a1 C(x z)) :/\: (a2 C(y z))
  73 class MyEq p where
  74     -- Minimal definition defines any one of unsafeCompare, =\/= and =/\=.
  75     unsafeCompare :: p C(a b) -> p C(c d) -> Bool
  76     unsafeCompare a b = IsEq == (a =/\= unsafeCoerceP b)
  77     (=\/=) :: p C(a b) -> p C(a c) -> EqCheck C(b c)
  78     a =\/= b | unsafeCompare a b = unsafeCoerceP IsEq
  79              | otherwise = NotEq
  80     (=/\=) :: p C(a c) -> p C(b c) -> EqCheck C(a b)
  81     a =/\= b | IsEq == (a =\/= unsafeCoerceP b) = unsafeCoerceP IsEq
  82              | otherwise = NotEq
  83
  84 infix 4 =\/=, =/\=
  85
  86 unsafeCoerceP :: a C(x y) -> a C(b c)
  87 unsafeCoerceP = unsafeCoerce#
  88
  89 unsafeCoerceP2 :: t C(w x y z) -> t C(a b c d)
  90 unsafeCoerceP2 = unsafeCoerce#
  91
  92 instance (Show2 a, Show2 b) => Show ( (a :> b) C(x y) ) where
  93     showsPrec d (x :> y) = showOp2 1 ":>" d x y
  94
  95 instance (Show2 a, Show2 b) => Show2 (a :> b) where
  96     showsPrec2 = showsPrec
  97
  98 instance (Show2 a, Show2 b) => Show ( (a :\/: b) C(x y) ) where
  99     showsPrec d (x :\/: y) = showOp2 9 ":\\/:" d x y
 100
 101 instance (Show2 a, Show2 b) => Show2 (a :\/: b) where
 102     showsPrec2 = showsPrec
 103
 104 infixr 5 :>:, :<:, +>+, +<+
 105
 106 -- forward list
 107 data FL a C(x z) where
 108     (:>:) :: a C(x y) -> FL a C(y z) -> FL a C(x z)
 109     NilFL :: FL a C(x x)
 110
 111 instance Show2 a => Show (FL a C(x z)) where
 112    showsPrec _ NilFL = showString "NilFL"
 113    showsPrec d (x :>: xs) = showParen (d > prec) $ showsPrec2 (prec + 1) x .
 114                             showString " :>: " . showsPrec (prec + 1) xs
 115        where prec = 5
 116
 117 instance Show2 a => Show2 (FL a) where
 118    showsPrec2 = showsPrec
 119
 120 -- reverse list
 121 data RL a C(x z) where
 122     (:<:) :: a C(y z) -> RL a C(x y) -> RL a C(x z)
 123     NilRL :: RL a C(x x)
 124
 125 nullFL :: FL a C(x z) -> Bool
 126 nullFL NilFL = True
 127 nullFL _ = False
 128
 129 nullRL :: RL a C(x z) -> Bool
 130 nullRL NilRL = True
 131 nullRL _ = False
 132
 133 filterFL :: (FORALL(x y) p C(x y) -> EqCheck C(x y)) -> FL p C(w z) -> FL p C(w z)
 134 filterFL _ NilFL = NilFL
 135 filterFL f (x:>:xs) | IsEq <- f x = filterFL f xs
 136                     | otherwise = x :>: filterFL f xs
 137
 138 filterE :: (a -> EqCheck C(x y)) -> [a] -> [Proof a C(x y)]
 139 filterE _ [] = []
 140 filterE p (x:xs)
 141     | IsEq <- p x = Proof x : filterE p xs
 142     | otherwise   = filterE p xs
 143
 144 (+>+) :: FL a C(x y) -> FL a C(y z) -> FL a C(x z)
 145 NilFL +>+ ys = ys
 146 (x:>:xs) +>+ ys = x :>: xs +>+ ys
 147
 148 (+<+) :: RL a C(y z) -> RL a C(x y) -> RL a C(x z)
 149 NilRL +<+ ys = ys
 150 (x:<:xs) +<+ ys = x :<: xs +<+ ys
 151
 152 reverseFL :: FL a C(x z) -> RL a C(x z)
 153 reverseFL xs = r NilRL xs
 154   where r :: RL a C(l m) -> FL a C(m o) -> RL a C(l o)
 155         r ls NilFL = ls
 156         r ls (a:>:as) = r (a:<:ls) as
 157
 158 reverseRL :: RL a C(x z) -> FL a C(x z)
 159 reverseRL xs = r NilFL xs -- r (xs :> NilFL)
 160   where r :: FL a C(m o) -> RL a C(l m) -> FL a C(l o)
 161         r ls NilRL = ls
 162         r ls (a:<:as) = r (a:>:ls) as
 163
 164 concatFL :: FL (FL a) C(x z) -> FL a C(x z)
 165 concatFL NilFL = NilFL
 166 concatFL (a:>:as) = a +>+ concatFL as
 167
 168 concatRL :: RL (RL a) C(x z) -> RL a C(x z)
 169 concatRL NilRL = NilRL
 170 concatRL (a:<:as) = a +<+ concatRL as
 171
 172 spanFL :: (FORALL(w y) a C(w y) -> Bool) -> FL a C(x z) -> (FL a :> FL a) C(x z)
 173 spanFL f (x:>:xs) | f x = case spanFL f xs of
 174                             ys :> zs -> (x:>:ys) :> zs
 175 spanFL _ xs = NilFL :> xs
 176
 177 splitAtFL :: Int -> FL a C(x z) -> (FL a :> FL a) C(x z)
 178 splitAtFL 0 xs = NilFL :> xs
 179 splitAtFL _ NilFL = NilFL :> NilFL
 180 splitAtFL n (x:>:xs) = case splitAtFL (n-1) xs of
 181                        (xs':>xs'') -> (x:>:xs' :> xs'')
 182
 183 -- 'bunchFL n' groups patches into batches of n, except that it always puts
 184 -- the first patch in its own group, this being a recognition that the
 185 -- first patch is often *very* large.
 186
 187 bunchFL :: Int -> FL a C(x y) -> FL (FL a) C(x y)
 188 bunchFL _ NilFL = NilFL
 189 bunchFL n (x:>:xs) = (x :>: NilFL) :>: bFL xs
 190     where bFL :: FL a C(x y) -> FL (FL a) C(x y)
 191           bFL NilFL = NilFL
 192           bFL bs = case splitAtFL n bs of
 193                    a :> b -> a :>: bFL b
 194
 195
 196 allFL :: (FORALL(x y) a C(x y) -> Bool) -> FL a C(w z) -> Bool
 197 allFL f xs = and $ mapFL f xs
 198
 199 foldlFL :: (FORALL(w y) a -> b C(w y) -> a) -> a -> FL b C(x z) -> a
 200 foldlFL _ x NilFL = x
 201 foldlFL f x (y:>:ys) = foldlFL f (f x y) ys
 202
 203 foldlRL :: (FORALL(w y) a -> b C(w y) -> a) -> a -> RL b C(x z) -> a
 204 foldlRL _ x NilRL = x
 205 foldlRL f x (y:<:ys) = foldlRL f (f x y) ys
 206
 207 mapFL_FL :: (FORALL(w y) a C(w y) -> b C(w y)) -> FL a C(x z) -> FL b C(x z)
 208 mapFL_FL _ NilFL = NilFL
 209 mapFL_FL f (a:>:as) = f a :>: mapFL_FL f as
 210
 211 zipWithFL :: (FORALL(x y) a -> p C(x y) -> q C(x y))
 212           -> [a] -> FL p C(w z) -> FL q C(w z)
 213 zipWithFL f (x:xs) (y :>: ys) = f x y :>: zipWithFL f xs ys
 214 zipWithFL _ _ NilFL = NilFL
 215 zipWithFL _ [] (_:>:_) = bug "zipWithFL called with too short a list"
 216
 217 mapRL_RL :: (FORALL(w y) a C(w y) -> b C(w y)) -> RL a C(x z) -> RL b C(x z)
 218 mapRL_RL _ NilRL = NilRL
 219 mapRL_RL f (a:<:as) = f a :<: mapRL_RL f as
 220
 221 mapFL :: (FORALL(w z) a C(w z) -> b) -> FL a C(x y) -> [b]
 222 mapFL _ NilFL = []
 223 mapFL f (a :>: b) = f a : mapFL f b
 224
 225 mapRL :: (FORALL(w z) a C(w z) -> b) -> RL a C(x y) -> [b]
 226 mapRL _ NilRL = []
 227 mapRL f (a :<: b) = f a : mapRL f b
 228
 229 unsafeMap_l2f :: (FORALL(w z) a -> b C(w z)) -> [a] -> FL b C(x y)
 230 unsafeMap_l2f _ [] = unsafeCoerceP NilFL
 231 unsafeMap_l2f f (x:xs) = f x :>: unsafeMap_l2f f xs
 232
 233 lengthFL :: FL a C(x z) -> Int
 234 lengthFL xs = l xs 0
 235   where l :: FL a C(x z) -> Int -> Int
 236         l NilFL n = n
 237         l (_:>:as) n = l as $! n+1
 238
 239 lengthRL :: RL a C(x z) -> Int
 240 lengthRL xs = l xs 0
 241   where l :: RL a C(x z) -> Int -> Int
 242         l NilRL n = n
 243         l (_:<:as) n = l as $! n+1
 244
 245 isShorterThanRL :: RL a C(x y) -> Int -> Bool
 246 isShorterThanRL _ n | n <= 0 = False
 247 isShorterThanRL NilRL _ = True
 248 isShorterThanRL (_:<:xs) n = isShorterThanRL xs (n-1)
 249
 250 concatReverseFL :: FL (RL a) C(x y) -> RL a C(x y)
 251 concatReverseFL = concatRL . reverseFL
 252
 253 headRL :: RL a C(x y) -> FlippedSeal a C(y)
 254 headRL (x:<:_) = flipSeal x
 255 headRL _ = impossible
 256
 257 consRLSealed :: a C(y z) -> FlippedSeal (RL a) C(y) -> FlippedSeal (RL a) C(z)
 258 consRLSealed a (FlippedSeal as) = flipSeal $ a :<: as
 259
 260 #ifndef GADT_WITNESSES
 261 -- These are useful for interfacing with modules outside of
 262 -- patch theory, such as Show.lhs
 263 unsafeUnFL :: FL a -> [a]
 264 unsafeUnFL NilFL = []
 265 unsafeUnFL (a:>:as) = a : unsafeUnFL as
 266
 267 unsafeUnRL :: RL a -> [a]
 268 unsafeUnRL NilRL = []
 269 unsafeUnRL (a:<:as) = a : unsafeUnRL as
 270
 271 unsafeFL :: [a] -> FL a
 272 unsafeFL [] = NilFL
 273 unsafeFL (a:as) = a :>: unsafeFL as
 274
 275 unsafeRL :: [a] -> RL a
 276 unsafeRL [] = NilRL
 277 unsafeRL (a:as) = a :<: unsafeRL as
 278 #endif
 279
 280 \end{code}