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