{-# OPTIONS_HADDOCK ignore-exports #-}
module Darcs.Patch.Witnesses.Sealed
( Sealed(..)
, seal
, unseal
, mapSeal
, Sealed2(..)
, seal2
, unseal2
, mapSeal2
, FlippedSeal(..)
, flipSeal
, unsealFlipped
, mapFlipped
, Dup(..)
, Gap(..)
, FreeLeft
, unFreeLeft
, FreeRight
, unFreeRight
) where
import Darcs.Prelude
import Data.Functor.Compose ( Compose(..) )
import Darcs.Patch.Witnesses.Eq ( Eq2, EqCheck(..) )
import Darcs.Patch.Witnesses.Show
import Darcs.Patch.Witnesses.Eq ( (=\/=) )
import Darcs.Patch.Witnesses.Unsafe ( unsafeCoerceP1, unsafeCoerceP )
data Sealed a where
Sealed :: a wX -> Sealed a
seal :: a wX -> Sealed a
seal :: forall (a :: * -> *) wX. a wX -> Sealed a
seal = a wX -> Sealed a
forall (a :: * -> *) wX. a wX -> Sealed a
Sealed
instance Eq2 a => Eq (Sealed (a wX)) where
Sealed a wX wX
x == :: Sealed (a wX) -> Sealed (a wX) -> Bool
== Sealed a wX wX
y | EqCheck wX wX
IsEq <- a wX wX
x a wX wX -> a wX wX -> EqCheck wX wX
forall wA wB wC. a wA wB -> a wA wC -> EqCheck wB wC
forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= a wX wX
y = Bool
True
| Bool
otherwise = Bool
False
data Sealed2 a where
Sealed2 :: !(a wX wY) -> Sealed2 a
seal2 :: a wX wY -> Sealed2 a
seal2 :: forall (a :: * -> * -> *) wX wY. a wX wY -> Sealed2 a
seal2 = a wX wY -> Sealed2 a
forall (a :: * -> * -> *) wX wY. a wX wY -> Sealed2 a
Sealed2
data FlippedSeal a wY where
FlippedSeal :: !(a wX wY) -> FlippedSeal a wY
flipSeal :: a wX wY -> FlippedSeal a wY
flipSeal :: forall (a :: * -> * -> *) wX wY. a wX wY -> FlippedSeal a wY
flipSeal = a wX wY -> FlippedSeal a wY
forall (a :: * -> * -> *) wX wY. a wX wY -> FlippedSeal a wY
FlippedSeal
unsafeUnseal :: Sealed a -> a wX
unsafeUnseal :: forall (a :: * -> *) wX. Sealed a -> a wX
unsafeUnseal (Sealed a wX
a) = a wX -> a wX
forall (a :: * -> *) wX wY. a wX -> a wY
unsafeCoerceP1 a wX
a
unsafeUnseal2 :: Sealed2 a -> a wX wY
unsafeUnseal2 :: forall (a :: * -> * -> *) wX wY. Sealed2 a -> a wX wY
unsafeUnseal2 (Sealed2 a wX wY
a) = a wX wY -> a wX wY
forall (a :: * -> * -> *) wX wY wB wC. a wX wY -> a wB wC
unsafeCoerceP a wX wY
a
unseal :: (forall wX . a wX -> b) -> Sealed a -> b
unseal :: forall (a :: * -> *) b. (forall wX. a wX -> b) -> Sealed a -> b
unseal forall wX. a wX -> b
f Sealed a
x = a Any -> b
forall wX. a wX -> b
f (Sealed a -> a Any
forall (a :: * -> *) wX. Sealed a -> a wX
unsafeUnseal Sealed a
x)
mapSeal :: (forall wX . a wX -> b wX) -> Sealed a -> Sealed b
mapSeal :: forall (a :: * -> *) (b :: * -> *).
(forall wX. a wX -> b wX) -> Sealed a -> Sealed b
mapSeal forall wX. a wX -> b wX
f = (forall wX. a wX -> Sealed b) -> Sealed a -> Sealed b
forall (a :: * -> *) b. (forall wX. a wX -> b) -> Sealed a -> b
unseal (b wX -> Sealed b
forall (a :: * -> *) wX. a wX -> Sealed a
seal (b wX -> Sealed b) -> (a wX -> b wX) -> a wX -> Sealed b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a wX -> b wX
forall wX. a wX -> b wX
f)
mapFlipped :: (forall wX . a wX wY -> b wX wZ) -> FlippedSeal a wY -> FlippedSeal b wZ
mapFlipped :: forall (a :: * -> * -> *) wY (b :: * -> * -> *) wZ.
(forall wX. a wX wY -> b wX wZ)
-> FlippedSeal a wY -> FlippedSeal b wZ
mapFlipped forall wX. a wX wY -> b wX wZ
f (FlippedSeal a wX wY
x) = b wX wZ -> FlippedSeal b wZ
forall (a :: * -> * -> *) wX wY. a wX wY -> FlippedSeal a wY
FlippedSeal (a wX wY -> b wX wZ
forall wX. a wX wY -> b wX wZ
f a wX wY
x)
unseal2 :: (forall wX wY . a wX wY -> b) -> Sealed2 a -> b
unseal2 :: forall (a :: * -> * -> *) b.
(forall wX wY. a wX wY -> b) -> Sealed2 a -> b
unseal2 forall wX wY. a wX wY -> b
f Sealed2 a
a = a Any Any -> b
forall wX wY. a wX wY -> b
f (Sealed2 a -> a Any Any
forall (a :: * -> * -> *) wX wY. Sealed2 a -> a wX wY
unsafeUnseal2 Sealed2 a
a)
mapSeal2 :: (forall wX wY . a wX wY -> b wX wY) -> Sealed2 a -> Sealed2 b
mapSeal2 :: forall (a :: * -> * -> *) (b :: * -> * -> *).
(forall wX wY. a wX wY -> b wX wY) -> Sealed2 a -> Sealed2 b
mapSeal2 forall wX wY. a wX wY -> b wX wY
f = (forall wX wY. a wX wY -> Sealed2 b) -> Sealed2 a -> Sealed2 b
forall (a :: * -> * -> *) b.
(forall wX wY. a wX wY -> b) -> Sealed2 a -> b
unseal2 (b wX wY -> Sealed2 b
forall (a :: * -> * -> *) wX wY. a wX wY -> Sealed2 a
seal2 (b wX wY -> Sealed2 b)
-> (a wX wY -> b wX wY) -> a wX wY -> Sealed2 b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a wX wY -> b wX wY
forall wX wY. a wX wY -> b wX wY
f)
unsealFlipped :: (forall wX wY . a wX wY -> b) -> FlippedSeal a wZ -> b
unsealFlipped :: forall (a :: * -> * -> *) b wZ.
(forall wX wY. a wX wY -> b) -> FlippedSeal a wZ -> b
unsealFlipped forall wX wY. a wX wY -> b
f (FlippedSeal a wX wZ
a) = a wX wZ -> b
forall wX wY. a wX wY -> b
f a wX wZ
a
instance Show1 a => Show (Sealed a) where
showsPrec :: Int -> Sealed a -> ShowS
showsPrec Int
d (Sealed a wX
x) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
appPrec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Sealed " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a wX -> ShowS
forall (a :: * -> *) wX. Show1 a => Int -> a wX -> ShowS
showsPrec1 (Int
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) a wX
x
instance Show2 a => Show (Sealed2 a) where
showsPrec :: Int -> Sealed2 a -> ShowS
showsPrec Int
d (Sealed2 a wX wY
x) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
appPrec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Sealed2 " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a wX wY -> ShowS
forall (a :: * -> * -> *) wX wY. Show2 a => Int -> a wX wY -> ShowS
showsPrec2 (Int
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) a wX wY
x
data Dup p wX wY where
Dup :: p wX -> Dup p wX wX
newtype Poly a = Poly { forall (a :: * -> *). Poly a -> forall wX. a wX
unPoly :: forall wX . a wX }
newtype FreeLeft p = FLInternal (Poly (Compose Sealed p))
newtype FreeRight p = FRInternal (Poly (FlippedSeal p))
unFreeLeft :: FreeLeft p -> Sealed (p wX)
unFreeLeft :: forall (p :: * -> * -> *) wX. FreeLeft p -> Sealed (p wX)
unFreeLeft (FLInternal Poly (Compose Sealed p)
x) = Compose Sealed p wX -> Sealed (p wX)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Poly (Compose Sealed p) -> forall wX. Compose Sealed p wX
forall (a :: * -> *). Poly a -> forall wX. a wX
unPoly Poly (Compose Sealed p)
x)
unFreeRight :: FreeRight p -> FlippedSeal p wX
unFreeRight :: forall (p :: * -> * -> *) wX. FreeRight p -> FlippedSeal p wX
unFreeRight (FRInternal Poly (FlippedSeal p)
x) = Poly (FlippedSeal p) -> forall wX. FlippedSeal p wX
forall (a :: * -> *). Poly a -> forall wX. a wX
unPoly Poly (FlippedSeal p)
x
class Gap w where
emptyGap :: (forall wX . p wX wX) -> w p
freeGap :: (forall wX wY . p wX wY) -> w p
joinGap :: (forall wX wY wZ . p wX wY -> q wY wZ -> r wX wZ) -> w p -> w q -> w r
instance Gap FreeLeft where
emptyGap :: forall (p :: * -> * -> *). (forall wX. p wX wX) -> FreeLeft p
emptyGap forall wX. p wX wX
e = Poly (Compose Sealed p) -> FreeLeft p
forall (p :: * -> * -> *). Poly (Compose Sealed p) -> FreeLeft p
FLInternal ((forall wX. Compose Sealed p wX) -> Poly (Compose Sealed p)
forall (a :: * -> *). (forall wX. a wX) -> Poly a
Poly (Sealed (p wX) -> Compose Sealed p wX
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (p wX wX -> Sealed (p wX)
forall (a :: * -> *) wX. a wX -> Sealed a
Sealed p wX wX
forall wX. p wX wX
e)))
freeGap :: forall (p :: * -> * -> *). (forall wX wY. p wX wY) -> FreeLeft p
freeGap forall wX wY. p wX wY
e = Poly (Compose Sealed p) -> FreeLeft p
forall (p :: * -> * -> *). Poly (Compose Sealed p) -> FreeLeft p
FLInternal ((forall wX. Compose Sealed p wX) -> Poly (Compose Sealed p)
forall (a :: * -> *). (forall wX. a wX) -> Poly a
Poly (Sealed (p wX) -> Compose Sealed p wX
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (p wX Any -> Sealed (p wX)
forall (a :: * -> *) wX. a wX -> Sealed a
Sealed p wX Any
forall wX wY. p wX wY
e)))
joinGap :: forall (p :: * -> * -> *) (q :: * -> * -> *) (r :: * -> * -> *).
(forall wX wY wZ. p wX wY -> q wY wZ -> r wX wZ)
-> FreeLeft p -> FreeLeft q -> FreeLeft r
joinGap forall wX wY wZ. p wX wY -> q wY wZ -> r wX wZ
op (FLInternal Poly (Compose Sealed p)
p) (FLInternal Poly (Compose Sealed q)
q) =
Poly (Compose Sealed r) -> FreeLeft r
forall (p :: * -> * -> *). Poly (Compose Sealed p) -> FreeLeft p
FLInternal
((forall wX. Compose Sealed r wX) -> Poly (Compose Sealed r)
forall (a :: * -> *). (forall wX. a wX) -> Poly a
Poly
(case Poly (Compose Sealed p) -> forall wX. Compose Sealed p wX
forall (a :: * -> *). Poly a -> forall wX. a wX
unPoly Poly (Compose Sealed p)
p of
Compose (Sealed p wX wX
p') ->
case Poly (Compose Sealed q) -> forall wX. Compose Sealed q wX
forall (a :: * -> *). Poly a -> forall wX. a wX
unPoly Poly (Compose Sealed q)
q of
Compose (Sealed q wX wX
q') -> Sealed (r wX) -> Compose Sealed r wX
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (r wX wX -> Sealed (r wX)
forall (a :: * -> *) wX. a wX -> Sealed a
Sealed (p wX wX
p' p wX wX -> q wX wX -> r wX wX
forall wX wY wZ. p wX wY -> q wY wZ -> r wX wZ
`op` q wX wX
q'))))
instance Gap FreeRight where
emptyGap :: forall (p :: * -> * -> *). (forall wX. p wX wX) -> FreeRight p
emptyGap forall wX. p wX wX
e = Poly (FlippedSeal p) -> FreeRight p
forall (p :: * -> * -> *). Poly (FlippedSeal p) -> FreeRight p
FRInternal ((forall wX. FlippedSeal p wX) -> Poly (FlippedSeal p)
forall (a :: * -> *). (forall wX. a wX) -> Poly a
Poly (p wX wX -> FlippedSeal p wX
forall (a :: * -> * -> *) wX wY. a wX wY -> FlippedSeal a wY
FlippedSeal p wX wX
forall wX. p wX wX
e))
freeGap :: forall (p :: * -> * -> *). (forall wX wY. p wX wY) -> FreeRight p
freeGap forall wX wY. p wX wY
e = Poly (FlippedSeal p) -> FreeRight p
forall (p :: * -> * -> *). Poly (FlippedSeal p) -> FreeRight p
FRInternal ((forall wX. FlippedSeal p wX) -> Poly (FlippedSeal p)
forall (a :: * -> *). (forall wX. a wX) -> Poly a
Poly (p Any wX -> FlippedSeal p wX
forall (a :: * -> * -> *) wX wY. a wX wY -> FlippedSeal a wY
FlippedSeal p Any wX
forall wX wY. p wX wY
e))
joinGap :: forall (p :: * -> * -> *) (q :: * -> * -> *) (r :: * -> * -> *).
(forall wX wY wZ. p wX wY -> q wY wZ -> r wX wZ)
-> FreeRight p -> FreeRight q -> FreeRight r
joinGap forall wX wY wZ. p wX wY -> q wY wZ -> r wX wZ
op (FRInternal Poly (FlippedSeal p)
p) (FRInternal Poly (FlippedSeal q)
q) =
Poly (FlippedSeal r) -> FreeRight r
forall (p :: * -> * -> *). Poly (FlippedSeal p) -> FreeRight p
FRInternal
((forall wX. FlippedSeal r wX) -> Poly (FlippedSeal r)
forall (a :: * -> *). (forall wX. a wX) -> Poly a
Poly
(case Poly (FlippedSeal q) -> forall wX. FlippedSeal q wX
forall (a :: * -> *). Poly a -> forall wX. a wX
unPoly Poly (FlippedSeal q)
q of
FlippedSeal q wX wX
q' ->
case Poly (FlippedSeal p) -> forall wX. FlippedSeal p wX
forall (a :: * -> *). Poly a -> forall wX. a wX
unPoly Poly (FlippedSeal p)
p of
FlippedSeal p wX wX
p' -> r wX wX -> FlippedSeal r wX
forall (a :: * -> * -> *) wX wY. a wX wY -> FlippedSeal a wY
FlippedSeal (p wX wX
p' p wX wX -> q wX wX -> r wX wX
forall wX wY wZ. p wX wY -> q wY wZ -> r wX wZ
`op` q wX wX
q')))