#include "gadts.h"
module Darcs.Witnesses.Sealed ( Sealed(..), seal, unseal, mapSeal,
unsafeUnseal, unsafeUnsealFlipped, unsafeUnseal2,
Sealed2(..), seal2, unseal2, mapSeal2,
FlippedSeal(..), flipSeal, unsealFlipped, mapFlipped,
unsealM, liftSM,
Gap(..), FreeLeft, unFreeLeft, FreeRight, unFreeRight
) where
import Darcs.Witnesses.Eq ( MyEq, EqCheck(..) )
import Darcs.Witnesses.Show
import Darcs.Witnesses.Eq ( (=\/=) )
import Darcs.Witnesses.Unsafe ( unsafeCoerceP1, unsafeCoerceP )
data Sealed a where
Sealed :: a C(x ) -> Sealed a
seal :: a C(x ) -> Sealed a
seal = Sealed
instance MyEq a => Eq (Sealed (a C(x ))) where
Sealed x == Sealed y | IsEq <- x =\/= y = True
| otherwise = False
data Sealed2 a where
Sealed2 :: !(a C(x y )) -> Sealed2 a
seal2 :: a C(x y ) -> Sealed2 a
seal2 = Sealed2
data FlippedSeal a C(y) where
FlippedSeal :: !(a C(x y)) -> FlippedSeal a C(y)
flipSeal :: a C(x y) -> FlippedSeal a C(y)
flipSeal = FlippedSeal
unsafeUnseal :: Sealed a -> a C(x)
unsafeUnseal (Sealed a) = unsafeCoerceP1 a
unsafeUnsealFlipped :: FlippedSeal a C(y) -> a C(x y)
unsafeUnsealFlipped (FlippedSeal a) = unsafeCoerceP a
unsafeUnseal2 :: Sealed2 a -> a C(x y)
unsafeUnseal2 (Sealed2 a) = unsafeCoerceP a
unseal :: (FORALL(x) a C(x ) -> b) -> Sealed a -> b
unseal f x = f (unsafeUnseal x)
unsealM :: Monad m => m (Sealed a) -> (FORALL(x) a C(x) -> m b) -> m b
unsealM m1 m2 = do sx <- m1
unseal m2 sx
liftSM :: Monad m => (FORALL(x) a C(x) -> b) -> m (Sealed a) -> m b
liftSM f m = do sx <- m
return (unseal f sx)
mapSeal :: (FORALL(x) a C(x ) -> b C(x )) -> Sealed a -> Sealed b
mapSeal f = unseal (seal . f)
mapFlipped :: (FORALL(x) a C(x y) -> b C(x z)) -> FlippedSeal a C(y) -> FlippedSeal b C(z)
mapFlipped f (FlippedSeal x) = FlippedSeal (f x)
unseal2 :: (FORALL(x y) a C(x y ) -> b) -> Sealed2 a -> b
unseal2 f a = f (unsafeUnseal2 a)
mapSeal2 :: (FORALL(x y) a C(x y ) -> b C(x y )) -> Sealed2 a -> Sealed2 b
mapSeal2 f = unseal2 (seal2 . f)
unsealFlipped :: (FORALL(x y) a C(x y) -> b) -> FlippedSeal a C(z) -> b
unsealFlipped f (FlippedSeal a) = f a
instance Show1 a => Show (Sealed a) where
showsPrec d (Sealed x) = showParen (d > appPrec) $ showString "Sealed " . showsPrec1 (appPrec + 1) x
instance Show2 a => Show (Sealed2 a) where
showsPrec d (Sealed2 x) = showParen (d > appPrec) $ showString "Sealed2 " . showsPrec2 (appPrec + 1) x
newtype Poly a = Poly { unPoly :: FORALL(x) a C(x) }
newtype Stepped (f :: SEALEDPATCHKIND -> *) a C(x) = Stepped { unStepped :: f (a C(x)) }
newtype FreeLeft p = FLInternal (Poly (Stepped Sealed p))
newtype FreeRight p = FRInternal (Poly (FlippedSeal p))
unFreeLeft :: FreeLeft p -> Sealed (p C(x))
unFreeLeft (FLInternal x) = unStepped (unPoly x)
unFreeRight :: FreeRight p -> FlippedSeal p C(x)
unFreeRight (FRInternal x) = unPoly x
class Gap w where
emptyGap :: (FORALL(x) p C(x x)) -> w p
freeGap :: (FORALL(x y) p C(x y)) -> w p
joinGap :: (FORALL(x y z) p C(x y) -> q C(y z) -> r C(x z)) -> w p -> w q -> w r
instance Gap FreeLeft where
emptyGap e = FLInternal (Poly (Stepped (Sealed e)))
freeGap e = FLInternal (Poly (Stepped (Sealed e)))
joinGap op (FLInternal p) (FLInternal q)
= FLInternal (Poly (case unPoly p of Stepped (Sealed p') -> case unPoly q of Stepped (Sealed q') -> Stepped (Sealed (p' `op` q'))))
instance Gap FreeRight where
emptyGap e = FRInternal (Poly (FlippedSeal e))
freeGap e = FRInternal (Poly (FlippedSeal e))
joinGap op (FRInternal p) (FRInternal q)
= FRInternal (Poly (case unPoly q of FlippedSeal q' -> case unPoly p of FlippedSeal p' -> FlippedSeal (p' `op` q')))