{-# LANGUAGE CPP #-}
#if __GLASGOW_HASKELL__ >= 704
{-# LANGUAGE Safe #-}
#elif __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Trustworthy #-}
#endif
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
#if __GLASGOW_HASKELL__ >= 706
{-# LANGUAGE PolyKinds #-}
#endif
{-# LANGUAGE TypeFamilies #-}
#if __GLASGOW_HASKELL__ >= 708
{-# LANGUAGE EmptyCase #-}
#endif
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Functor.Contravariant.Generic
-- Copyright   :  (C) 2007-2015 Edward Kmett
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
-- Stability   :  experimental
-- Portability :  ConstraintKinds
--
--
--
----------------------------------------------------------------------------

module Data.Functor.Contravariant.Generic
  ( Deciding(..)
  , Deciding1(..)
  ) where

import Data.Functor.Contravariant
import Data.Functor.Contravariant.Divisible
import GHC.Generics

-- | This provides machinery for deconstructing an arbitrary 'Generic' instance using a 'Decidable' 'Contravariant' functor.
--
-- /Examples:/
--
-- @
-- gcompare :: 'Deciding' 'Ord' a => a -> a -> 'Ordering'
-- gcompare = 'getComparison' $ 'deciding' (Proxy :: Proxy 'Ord') ('Comparison' 'compare')
-- @
--
-- @
-- geq :: 'Deciding' 'Eq' a => a -> a -> 'Bool'
-- geq = 'getEquivalence' $ 'deciding' (Proxy :: Proxy 'Eq') ('Equivalence' ('=='))
-- @
class (Generic a, GDeciding q (Rep' a)) => Deciding q a where
#ifndef HLINT
  deciding :: Decidable f => p q -> (forall b. q b => f b) -> f a
#endif

instance (Generic a, GG (Rep a), GDeciding q (Rep' a)) => Deciding q a  where
  deciding :: forall (f :: * -> *) (p :: (* -> Constraint) -> *).
Decidable f =>
p q -> (forall b. q b => f b) -> f a
deciding p q
p forall b. q b => f b
q = forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap (forall (r :: * -> *) p. GG r => r p -> Swizzle r p
swizzle forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a x. Generic a => a -> Rep a x
from) forall a b. (a -> b) -> a -> b
$ forall {k} (q :: * -> Constraint) (t :: k -> *) (f :: * -> *)
       (p :: (* -> Constraint) -> *) (a :: k).
(GDeciding q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f (t a)
gdeciding p q
p forall b. q b => f b
q

type Rep' a = Swizzle (Rep a)
type Rep1' f = Swizzle (Rep1 f)
type family Swizzle (r :: * -> *) :: * -> *
type instance Swizzle (M1 i c f) = M1 i c (Swizzle f)
type instance Swizzle V1 = V1
type instance Swizzle U1 = U1
type instance Swizzle Par1 = Par1
type instance Swizzle (Rec1 f) = Rec1 f
type instance Swizzle (K1 i c) = K1 i c
type instance Swizzle (f :+: g) = Swizzle f ::+: Swizzle g
type instance Swizzle (f :*: g) = Swizzle f ::*: Swizzle g
type instance Swizzle (f :.: g) = f :.: Swizzle g

newtype (::+:) f g a = Sum {forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
(::+:) f g a -> Either (f a) (g a)
unSum :: Either (f a) (g a)}
newtype (::*:) f g a = Prod {forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
(::*:) f g a -> (f a, g a)
unProd :: (f a, g a)}

class GG r where
  swizzle :: r p -> Swizzle r p
instance GG f => GG (M1 i c f) where
  swizzle :: forall p. M1 i c f p -> Swizzle (M1 i c f) p
swizzle (M1 f p
a) = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall (r :: * -> *) p. GG r => r p -> Swizzle r p
swizzle f p
a)
instance GG V1 where swizzle :: forall p. V1 p -> Swizzle V1 p
swizzle V1 p
v = V1 p
v
instance GG U1 where swizzle :: forall p. U1 p -> Swizzle U1 p
swizzle U1 p
v = U1 p
v
instance GG (K1 i c) where swizzle :: forall p. K1 i c p -> Swizzle (K1 i c) p
swizzle K1 i c p
v = K1 i c p
v
instance GG Par1 where swizzle :: forall p. Par1 p -> Swizzle Par1 p
swizzle Par1 p
v = Par1 p
v
instance GG (Rec1 f) where swizzle :: forall p. Rec1 f p -> Swizzle (Rec1 f) p
swizzle Rec1 f p
v = Rec1 f p
v
instance (GG f, GG g) => GG (f :+: g) where
  {-# INLINE swizzle #-}
  swizzle :: forall p. (:+:) f g p -> Swizzle (f :+: g) p
swizzle (L1 f p
x) = forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
Either (f a) (g a) -> (::+:) f g a
Sum (forall a b. a -> Either a b
Left (forall (r :: * -> *) p. GG r => r p -> Swizzle r p
swizzle f p
x))
  swizzle (R1 g p
x) = forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
Either (f a) (g a) -> (::+:) f g a
Sum (forall a b. b -> Either a b
Right (forall (r :: * -> *) p. GG r => r p -> Swizzle r p
swizzle g p
x))
instance (GG f, GG g) => GG (f :*: g) where
  {-# INLINE swizzle #-}
  swizzle :: forall p. (:*:) f g p -> Swizzle (f :*: g) p
swizzle (f p
x :*: g p
y) = forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
(f a, g a) -> (::*:) f g a
Prod (forall (r :: * -> *) p. GG r => r p -> Swizzle r p
swizzle f p
x, forall (r :: * -> *) p. GG r => r p -> Swizzle r p
swizzle g p
y)
{-
-- This instance wouldn't be that efficient. But we don't
-- offer instances for compositions anyway.
instance (Functor f, GG g) => GG (f :.: g) where
  swizzle (Comp1 x) = Comp1 (fmap swizzle x)
-}

-- | This provides machinery for deconstructing an arbitrary 'Generic1' instance using a 'Decidable' 'Contravariant' functor.
--
-- /Examples:/
--
-- @
-- gcompare1 :: 'Deciding1' 'Ord' f => (a -> a -> 'Ordering') -> f a -> f a -> 'Ordering'
-- gcompare1 f = 'getComparison' $ 'deciding1' (Proxy :: Proxy 'Ord') ('Comparison' compare) ('Comparison' f)
-- @
--
-- @
-- geq1 :: 'Deciding1' 'Eq' f => (a -> a -> 'Bool') -> f a -> f a -> 'Bool'
-- geq1 f = 'getEquivalence' $ 'deciding1' (Proxy :: Proxy 'Eq') ('Equivalence' ('==')) ('Equivalence' f)
-- @
class (Generic1 t, GDeciding1 q (Rep1' t)) => Deciding1 q t where
#ifndef HLINT
  deciding1 :: Decidable f => p q -> (forall b. q b => f b) -> f a -> f (t a)
#endif

instance (Generic1 t, GDeciding1 q (Rep1' t), GG (Rep1 t)) => Deciding1 q t where
  deciding1 :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f (t a)
deciding1 p q
p forall b. q b => f b
q f a
r = forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap (forall (r :: * -> *) p. GG r => r p -> Swizzle r p
swizzle forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
from1) forall a b. (a -> b) -> a -> b
$ forall (q :: * -> Constraint) (t :: * -> *) (f :: * -> *)
       (p :: (* -> Constraint) -> *) a.
(GDeciding1 q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f a -> f (t a)
gdeciding1 p q
p forall b. q b => f b
q f a
r

class GDeciding q t where
#ifndef HLINT
  gdeciding :: Decidable f => p q -> (forall b. q b => f b) -> f (t a)
#endif

instance GDeciding q U1 where
  gdeciding :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) (a :: k).
Decidable f =>
p q -> (forall b. q b => f b) -> f (U1 a)
gdeciding p q
_ forall b. q b => f b
_ = forall (f :: * -> *) a. Divisible f => f a
conquer

instance GDeciding q V1 where
  gdeciding :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) (a :: k).
Decidable f =>
p q -> (forall b. q b => f b) -> f (V1 a)
gdeciding p q
_ forall b. q b => f b
_ = forall {k} (f :: * -> *) (a :: k). Decidable f => f (V1 a)
glose

instance (GDeciding q f, GDeciding q g) => GDeciding q (f ::*: g) where
  gdeciding :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) (a :: k).
Decidable f =>
p q -> (forall b. q b => f b) -> f ((::*:) f g a)
gdeciding p q
p forall b. q b => f b
q = forall {k} (f :: * -> *) (g :: k -> *) (a :: k) (h :: k -> *).
Divisible f =>
f (g a) -> f (h a) -> f ((::*:) g h a)
gdivide (forall {k} (q :: * -> Constraint) (t :: k -> *) (f :: * -> *)
       (p :: (* -> Constraint) -> *) (a :: k).
(GDeciding q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f (t a)
gdeciding p q
p forall b. q b => f b
q) (forall {k} (q :: * -> Constraint) (t :: k -> *) (f :: * -> *)
       (p :: (* -> Constraint) -> *) (a :: k).
(GDeciding q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f (t a)
gdeciding p q
p forall b. q b => f b
q)

instance (GDeciding q f, GDeciding q g) => GDeciding q (f ::+: g) where
  gdeciding :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) (a :: k).
Decidable f =>
p q -> (forall b. q b => f b) -> f ((::+:) f g a)
gdeciding p q
p forall b. q b => f b
q = forall {k} (f :: * -> *) (g :: k -> *) (a :: k) (h :: k -> *).
Decidable f =>
f (g a) -> f (h a) -> f ((::+:) g h a)
gchoose (forall {k} (q :: * -> Constraint) (t :: k -> *) (f :: * -> *)
       (p :: (* -> Constraint) -> *) (a :: k).
(GDeciding q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f (t a)
gdeciding p q
p forall b. q b => f b
q) (forall {k} (q :: * -> Constraint) (t :: k -> *) (f :: * -> *)
       (p :: (* -> Constraint) -> *) (a :: k).
(GDeciding q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f (t a)
gdeciding p q
p forall b. q b => f b
q)

#ifndef HLINT
instance q p => GDeciding q (K1 i p) where
#endif
  gdeciding :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) (a :: k).
Decidable f =>
p q -> (forall b. q b => f b) -> f (K1 i p a)
gdeciding p q
_ forall b. q b => f b
q = forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap forall k i c (p :: k). K1 i c p -> c
unK1 forall b. q b => f b
q

instance GDeciding q f => GDeciding q (M1 i c f) where
  gdeciding :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) (a :: k).
Decidable f =>
p q -> (forall b. q b => f b) -> f (M1 i c f a)
gdeciding p q
p forall b. q b => f b
q = forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1 (forall {k} (q :: * -> Constraint) (t :: k -> *) (f :: * -> *)
       (p :: (* -> Constraint) -> *) (a :: k).
(GDeciding q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f (t a)
gdeciding p q
p forall b. q b => f b
q)

class GDeciding1 q t where
#ifndef HLINT
  gdeciding1 :: Decidable f => p q -> (forall b. q b => f b) -> f a -> f (t a)
#endif

instance GDeciding1 q U1 where
  gdeciding1 :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f (U1 a)
gdeciding1 p q
_ forall b. q b => f b
_ f a
_ = forall (f :: * -> *) a. Divisible f => f a
conquer

instance GDeciding1 q V1 where
  gdeciding1 :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f (V1 a)
gdeciding1 p q
_ forall b. q b => f b
_ f a
_ = forall {k} (f :: * -> *) (a :: k). Decidable f => f (V1 a)
glose

instance (GDeciding1 q f, GDeciding1 q g) => GDeciding1 q (f ::*: g) where
  gdeciding1 :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f ((::*:) f g a)
gdeciding1 p q
p forall b. q b => f b
q f a
r = forall {k} (f :: * -> *) (g :: k -> *) (a :: k) (h :: k -> *).
Divisible f =>
f (g a) -> f (h a) -> f ((::*:) g h a)
gdivide (forall (q :: * -> Constraint) (t :: * -> *) (f :: * -> *)
       (p :: (* -> Constraint) -> *) a.
(GDeciding1 q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f a -> f (t a)
gdeciding1 p q
p forall b. q b => f b
q f a
r) (forall (q :: * -> Constraint) (t :: * -> *) (f :: * -> *)
       (p :: (* -> Constraint) -> *) a.
(GDeciding1 q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f a -> f (t a)
gdeciding1 p q
p forall b. q b => f b
q f a
r)

instance (GDeciding1 q f, GDeciding1 q g) => GDeciding1 q (f ::+: g) where
  gdeciding1 :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f ((::+:) f g a)
gdeciding1 p q
p forall b. q b => f b
q f a
r = forall {k} (f :: * -> *) (g :: k -> *) (a :: k) (h :: k -> *).
Decidable f =>
f (g a) -> f (h a) -> f ((::+:) g h a)
gchoose (forall (q :: * -> Constraint) (t :: * -> *) (f :: * -> *)
       (p :: (* -> Constraint) -> *) a.
(GDeciding1 q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f a -> f (t a)
gdeciding1 p q
p forall b. q b => f b
q f a
r) (forall (q :: * -> Constraint) (t :: * -> *) (f :: * -> *)
       (p :: (* -> Constraint) -> *) a.
(GDeciding1 q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f a -> f (t a)
gdeciding1 p q
p forall b. q b => f b
q f a
r)

absurd1 :: V1 a -> b
#if defined(HLINT) || (__GLASGOW_HASKELL__ < 708)
absurd1 x = x `seq` error "impossible"
#else
absurd1 :: forall {k} (a :: k) b. V1 a -> b
absurd1 V1 a
x = case V1 a
x of
#endif

glose :: Decidable f => f (V1 a)
glose :: forall {k} (f :: * -> *) (a :: k). Decidable f => f (V1 a)
glose = forall (f :: * -> *) a. Decidable f => (a -> Void) -> f a
lose forall {k} (a :: k) b. V1 a -> b
absurd1
{-# INLINE glose #-}

gdivide :: Divisible f => f (g a) -> f (h a) -> f ((g::*:h) a)
gdivide :: forall {k} (f :: * -> *) (g :: k -> *) (a :: k) (h :: k -> *).
Divisible f =>
f (g a) -> f (h a) -> f ((::*:) g h a)
gdivide = forall (f :: * -> *) a b c.
Divisible f =>
(a -> (b, c)) -> f b -> f c -> f a
divide forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
(::*:) f g a -> (f a, g a)
unProd
{-# INLINE gdivide #-}

gchoose :: Decidable f => f (g a) -> f (h a) -> f ((g::+:h) a)
gchoose :: forall {k} (f :: * -> *) (g :: k -> *) (a :: k) (h :: k -> *).
Decidable f =>
f (g a) -> f (h a) -> f ((::+:) g h a)
gchoose = forall (f :: * -> *) a b c.
Decidable f =>
(a -> Either b c) -> f b -> f c -> f a
choose forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
(::+:) f g a -> Either (f a) (g a)
unSum
{-# INLINE gchoose #-}

#ifndef HLINT
instance q p => GDeciding1 q (K1 i p) where
  gdeciding1 :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f (K1 i p a)
gdeciding1 p q
_ forall b. q b => f b
q f a
_ = forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap forall k i c (p :: k). K1 i c p -> c
unK1 forall b. q b => f b
q
#endif

instance GDeciding1 q f => GDeciding1 q (M1 i c f) where
  gdeciding1 :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f (M1 i c f a)
gdeciding1 p q
p forall b. q b => f b
q f a
r = forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1 (forall (q :: * -> Constraint) (t :: * -> *) (f :: * -> *)
       (p :: (* -> Constraint) -> *) a.
(GDeciding1 q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f a -> f (t a)
gdeciding1 p q
p forall b. q b => f b
q f a
r)

instance GDeciding1 q Par1 where
  gdeciding1 :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f (Par1 a)
gdeciding1 p q
_ forall b. q b => f b
_ f a
r = forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap forall p. Par1 p -> p
unPar1 f a
r

-- instance GDeciding1 q f => GDeciding1 q (Rec1 f) where gdeciding1 p q r = contramap unRec1 (gdeciding1 p q r)

instance Deciding1 q f => GDeciding1 q (Rec1 f) where
  gdeciding1 :: forall (f :: * -> *) (p :: (* -> Constraint) -> *) a.
Decidable f =>
p q -> (forall b. q b => f b) -> f a -> f (Rec1 f a)
gdeciding1 p q
p forall b. q b => f b
q f a
r = forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap forall k (f :: k -> *) (p :: k). Rec1 f p -> f p
unRec1 (forall (q :: * -> Constraint) (t :: * -> *) (f :: * -> *)
       (p :: (* -> Constraint) -> *) a.
(Deciding1 q t, Decidable f) =>
p q -> (forall b. q b => f b) -> f a -> f (t a)
deciding1 p q
p forall b. q b => f b
q f a
r)