#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
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 :>:, :<:, +>+, +<+
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
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
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 (n1) 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 (n1) xs of
(xs':<xs'') -> (x:<:xs' :< xs'')
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 (n1)
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)