-- 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(..),
                             lengthFL, mapFL, mapFL_FL, spanFL, foldlFL, allFL, anyFL,
                             filterFL,
                             splitAtFL, splitAtRL, bunchFL, foldlRL,
                             lengthRL, isShorterThanRL, mapRL, mapRL_RL, zipWithFL,
                             unsafeMap_l2f, filterE, filterFLFL,
                             filterRL,
                             reverseFL, reverseRL, (+>+), (+<+),
                             nullFL, concatFL, concatRL, concatReverseFL, headRL,
                             MyEq, unsafeCompare, (=\/=), (=/\=),
                             consRLSealed, nullRL, toFL,
                             (:>>)(..),
                             unsafeCoercePStart, unsafeCoercePEnd,
                             unsafeCoerceP, unsafeCoerceP2, spanFL_M
                           ) where

#include "impossible.h"
import GHC.Base (unsafeCoerce#)
import Darcs.Witnesses.Show
import Darcs.Witnesses.Sealed ( FlippedSeal(..), flipSeal, Sealed(..), FreeLeft, unFreeLeft, Sealed2(..) )

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))

data (a1 :>> a2) C(y) = FORALL(z) (a1 C(z)) :>> (a2 C(z y))
infixr 1 :>>

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#

unsafeCoercePStart :: a C(x1 y) -> a C(x2 y)
unsafeCoercePStart = unsafeCoerce#

unsafeCoercePEnd :: a C(x y1) -> a C(x y2)
unsafeCoercePEnd = 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 (MyEq a, MyEq b) => MyEq (a :> b) where
    (a1 :> b1) =\/= (a2 :> b2) | IsEq <- a1 =\/= a2 = b1 =\/= b2
                               | otherwise = NotEq

instance (MyEq a, MyEq b) => MyEq (a :< b) where
    (a1 :< b1) =\/= (a2 :< b2) | IsEq <- b1 =\/= b2 = a1 =\/= a2
                               | otherwise = NotEq

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

instance MyEq a => Eq (Sealed (a C(x))) where
    Sealed x == Sealed y | IsEq <- x =\/= y = True
                         | otherwise = False

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
   showDict2 = 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(x y) ->  [Sealed2 p]
filterRL _ NilRL = []
filterRL f (x :<: xs) | f x = Sealed2 x : (filterRL f xs)
                      | otherwise = filterRL 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

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(x y) -> [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

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

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)