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

{-# OPTIONS_HADDOCK ignore-exports #-}

module Darcs.Patch.Witnesses.Sealed
    ( Sealed(..)
    , seal
    , unseal
    , mapSeal
    , Sealed2(..)
    , seal2
    , unseal2
    , mapSeal2
    , FlippedSeal(..)
    , flipSeal
    , unsealFlipped
    , mapFlipped
    , 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 )

-- |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 :: 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 (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

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

-- laziness property:
-- unseal (const True) undefined == True
--
-- Pattern-matching on Sealed is currently strict in GHC because it's an existential:
-- https://gitlab.haskell.org/ghc/ghc/issues/17130
-- Implementing unseal via unsafeUnseal (with the unsafeCoerceP1 underneath) works
-- around that, and we rely on that occasionally for performance, e.g. when reading
-- the history of a repository.
--
-- TODO: this is quite obscure and makes it hard to know whether we really need
-- laziness in a certain place or are just getting it incidentally because someone
-- chose to use unseal rather than pattern-matching. We should introduce an explicit
-- "Make this Sealed lazy" combinator (also using unsafeCoerceP1 in the implementation)
-- and then make the seal implementation itself be strict.
--
-- The combinator would work by making a value with a fresh Sealed constructor, so even
-- though the subsequent pattern-match/unseal on that would itself be strict, it would
-- only force as far as the newly introduced Sealed.
--
-- All this applies to Sealed2 too, and FlippedSeal if we ever need a lazy one (but
-- the implementation of unsealFlipped has been strict for a long time without causing
-- trouble).

mapSeal :: (forall wX . a wX -> b wX) -> Sealed a -> Sealed b
mapSeal :: (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 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 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 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 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

-- |'Poly' is similar to 'Sealed', but the type argument is
-- universally quantified instead of being existentially quantified.
newtype Poly a = Poly { Poly a -> forall wX. a wX
unPoly :: forall wX . 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 (Compose 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 :: FreeLeft p -> Sealed (p wX)
unFreeLeft (FLInternal Poly (Compose Sealed p)
x) = Compose Sealed p wX -> Sealed (p wX)
forall k1 (f :: k1 -> *) k2 (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)

-- |Unwrap a 'FreeRight' value
unFreeRight :: FreeRight p -> FlippedSeal p wX
unFreeRight :: 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

-- |'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 :: (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 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 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 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 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 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')))