-- Copyright (C) 2007 David Roundy, 2009 Ganesh Sittampalam -- -- 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. {-# LANGUAGE FlexibleInstances #-} {-# OPTIONS_HADDOCK ignore-exports #-} module Darcs.Patch.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 Prelude () import Darcs.Prelude import Darcs.Patch.Witnesses.Eq ( Eq2, EqCheck(..) ) import Darcs.Patch.Witnesses.Show import Darcs.Patch.Witnesses.Eq ( (=\/=) ) import Darcs.Patch.Witnesses.Unsafe ( unsafeCoerceP1, unsafeCoerceP ) -- |A 'Sealed' type is a way of hide an existentially quantified type parameter, -- in this case wX, inside the type. Note that the only thing we can currently -- recover about the existentially quantified type wX is that it exists. data Sealed a where Sealed :: a wX -> Sealed a seal :: a wX -> Sealed a seal = Sealed instance Eq2 a => Eq (Sealed (a wX)) where Sealed x == Sealed y | IsEq <- x =\/= y = True | otherwise = False -- |The same as 'Sealed' but for two parameters (wX and wY). data Sealed2 a where Sealed2 :: !(a wX wY) -> Sealed2 a seal2 :: a wX wY -> Sealed2 a seal2 = Sealed2 data FlippedSeal a wY where FlippedSeal :: !(a wX wY) -> FlippedSeal a wY flipSeal :: a wX wY -> FlippedSeal a wY flipSeal = FlippedSeal unsafeUnseal :: Sealed a -> a wX unsafeUnseal (Sealed a) = unsafeCoerceP1 a unsafeUnsealFlipped :: FlippedSeal a wY -> a wX wY unsafeUnsealFlipped (FlippedSeal a) = unsafeCoerceP a unsafeUnseal2 :: Sealed2 a -> a wX wY unsafeUnseal2 (Sealed2 a) = unsafeCoerceP a unseal :: (forall wX . a wX -> b) -> Sealed a -> b unseal f x = f (unsafeUnseal x) -- laziness property: -- unseal (const True) undefined == True unsealM :: Monad m => m (Sealed a) -> (forall wX . a wX -> m b) -> m b unsealM m1 m2 = do sx <- m1 unseal m2 sx liftSM :: Monad m => (forall wX . a wX -> b) -> m (Sealed a) -> m b liftSM f m = do sx <- m return (unseal f sx) mapSeal :: (forall wX . a wX -> b wX) -> Sealed a -> Sealed b mapSeal f = unseal (seal . f) mapFlipped :: (forall wX . a wX wY -> b wX wZ) -> FlippedSeal a wY -> FlippedSeal b wZ mapFlipped f (FlippedSeal x) = FlippedSeal (f x) unseal2 :: (forall wX wY . a wX wY -> b) -> Sealed2 a -> b unseal2 f a = f (unsafeUnseal2 a) mapSeal2 :: (forall wX wY . a wX wY -> b wX wY) -> Sealed2 a -> Sealed2 b mapSeal2 f = unseal2 (seal2 . f) unsealFlipped :: (forall wX wY . a wX wY -> b) -> FlippedSeal a wZ -> 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 -- |'Poly' is similar to 'Sealed', but the type argument is -- universally quantified instead of being existentially quantified. newtype Poly a = Poly { unPoly :: forall wX . a wX } -- |'Stepped' is a type level composition operator. -- For example, @ 'Stepped' ('Sealed' p) @ is equivalent to -- @ \\x -> 'Sealed' (p x) @ newtype Stepped (f :: (* -> *) -> *) a wX = Stepped { unStepped :: f (a wX) } -- |'FreeLeft' p is @ \forall x . \exists y . p x y @ -- In other words the caller is free to specify the left witness, -- and then the right witness is an existential. -- Note that the order of the type constructors is important for ensuring -- that @ y @ is dependent on the @ x @ that is supplied. -- This is why 'Stepped' is needed, rather than writing the more obvious -- 'Sealed' ('Poly' p) which would notionally have the same quantification -- of the type witnesses. newtype FreeLeft p = FLInternal (Poly (Stepped Sealed p)) -- |'FreeRight' p is @ \forall y . \exists x . p x y @ -- In other words the caller is free to specify the right witness, -- and then the left witness is an existential. -- Note that the order of the type constructors is important for ensuring -- that @ x @ is dependent on the @ y @ that is supplied. newtype FreeRight p = FRInternal (Poly (FlippedSeal p)) -- |Unwrap a 'FreeLeft' value unFreeLeft :: FreeLeft p -> Sealed (p wX) unFreeLeft (FLInternal x) = unStepped (unPoly x) -- |Unwrap a 'FreeRight' value unFreeRight :: FreeRight p -> FlippedSeal p wX unFreeRight (FRInternal x) = unPoly x -- |'Gap' abstracts over 'FreeLeft' and 'FreeRight' for code constructing these values class Gap w where -- |An empty 'Gap', e.g. 'NilFL' or 'NilRL' emptyGap :: (forall wX . p wX wX) -> w p -- |A 'Gap' constructed from a completely polymorphic value, for example the constructors -- for primitive patches freeGap :: (forall wX wY . p wX wY) -> w p -- |Compose two 'Gap' values together in series, e.g. 'joinGap (+>+)' or 'joinGap (:>:)' 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 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')))