{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE TypeSynonymInstances  #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE PatternSynonyms       #-}
module Generics.Simplistic.Util
  ( -- * Utility Functions and Types
    (&&&) , (***) , (:->) , (<.>)
    -- * Poly-kind indexed product functionality
  , (:*:)(..) , Delta , curry' , uncurry' , delta , deltaMap
    -- * Poly-kind indexed sums
  , Sum(..) , either' , either''
    -- * Constraints
  , Implies , Trivial
    -- * Higher-order Eq and Show
  , EqHO(..) , ShowHO(..)
    -- * Existential Wrapper
  , Exists(..) , exMap , exMapM , exElim
    -- * Elem functionality
  , Elem , NotElem , HasElem(..) , ElemPrf(..) , IsElem, sameTy
    -- * Witnessing and All constraints
  , All , Witness(..) , witness , witnessPrf
  , weq , wshow
  ) where

import Data.Kind  (Constraint)
import Data.Proxy (Proxy(..))
import Data.Functor.Sum
import Data.Functor.Const
import Data.Type.Equality
import Control.Arrow ((***) , (&&&))
import GHC.Generics ((:*:)(..), V1 , U1(..))

-- |Lifted curry
curry' :: ((f :*: g) x -> a) -> f x -> g x -> a
curry' :: ((:*:) f g x -> a) -> f x -> g x -> a
curry' f :: (:*:) f g x -> a
f fx :: f x
fx gx :: g x
gx = (:*:) f g x -> a
f (f x
fx f x -> g x -> (:*:) f g x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g x
gx)

-- |Lifted uncurry
uncurry' :: (f x -> g x -> a) -> (f :*: g) x -> a
uncurry' :: (f x -> g x -> a) -> (:*:) f g x -> a
uncurry' f :: f x -> g x -> a
f (fx :: f x
fx :*: gx :: g x
gx) = f x -> g x -> a
f f x
fx g x
gx

-- |Natural transformations
type f :-> g = forall n . f n -> g n

-- |Diagonal indexed functor
type Delta f = f :*: f

-- |Duplicates its argument
delta :: f :-> Delta f
delta :: f n -> Delta f n
delta fx :: f n
fx = f n
fx f n -> f n -> Delta f n
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: f n
fx

-- |Applies the same function to both components of the pair
deltaMap :: (f :-> g) -> Delta f :-> Delta g
deltaMap :: (f :-> g) -> Delta f :-> Delta g
deltaMap f :: f :-> g
f (x :: f n
x :*: y :: f n
y) = f n -> g n
f :-> g
f f n
x g n -> g n -> (:*:) g g n
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: f n -> g n
f :-> g
f f n
y

-- |Higher-order sum eliminator
either' :: (f :-> r) -> (g :-> r) -> Sum f g :-> r
either' :: (f :-> r) -> (g :-> r) -> Sum f g :-> r
either' f :: f :-> r
f _ (InL x :: f n
x) = f n -> r n
f :-> r
f f n
x
either' _ g :: g :-> r
g (InR x :: g n
x) = g n -> r n
g :-> r
g g n
x

-- |Just like 'either'', but the result type is of kind Star
either'' :: (forall x . f x -> a) -> (forall y . g y -> a) -> Sum f g r -> a
either'' :: (forall (x :: k). f x -> a)
-> (forall (y :: k). g y -> a) -> Sum f g r -> a
either'' f :: forall (x :: k). f x -> a
f g :: forall (y :: k). g y -> a
g = Const a r -> a
forall a k (b :: k). Const a b -> a
getConst (Const a r -> a) -> (Sum f g r -> Const a r) -> Sum f g r -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f :-> Const a) -> (g :-> Const a) -> Sum f g :-> Const a
forall k (f :: k -> *) (r :: k -> *) (g :: k -> *).
(f :-> r) -> (g :-> r) -> Sum f g :-> r
either' (a -> Const a n
forall k a (b :: k). a -> Const a b
Const (a -> Const a n) -> (f n -> a) -> f n -> Const a n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f n -> a
forall (x :: k). f x -> a
f) (a -> Const a n
forall k a (b :: k). a -> Const a b
Const (a -> Const a n) -> (g n -> a) -> g n -> Const a n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g n -> a
forall (y :: k). g y -> a
g)

infixr 8 <.>
-- |Kleisli Composition
(<.>) :: (Monad m) => (b -> m c) -> (a -> m b) -> a -> m c
f :: b -> m c
f <.> :: (b -> m c) -> (a -> m b) -> a -> m c
<.> g :: a -> m b
g = (m b -> (b -> m c) -> m c
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= b -> m c
f) (m b -> m c) -> (a -> m b) -> a -> m c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m b
g

-- |Constraint implication
class    (c => d) => Implies c d
instance (c => d) => Implies c d

-- |Trivial constraint
class    Trivial c
instance Trivial c

-- |Higher order , poly kinded, version of 'Eq'
class EqHO (f :: ki -> *) where
  eqHO :: forall k . f k -> f k -> Bool

instance Eq a => EqHO (Const a) where
  eqHO :: Const a k -> Const a k -> Bool
eqHO (Const a :: a
a) (Const b :: a
b) = a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b

instance (EqHO f, EqHO g) => EqHO (f :*: g) where
  eqHO :: (:*:) f g k -> (:*:) f g k -> Bool
eqHO (fx :: f k
fx :*: gx :: g k
gx) (fy :: f k
fy :*: gy :: g k
gy) = f k -> f k -> Bool
forall ki (f :: ki -> *) (k :: ki). EqHO f => f k -> f k -> Bool
eqHO f k
fx f k
fy Bool -> Bool -> Bool
&& g k -> g k -> Bool
forall ki (f :: ki -> *) (k :: ki). EqHO f => f k -> f k -> Bool
eqHO g k
gx g k
gy

instance (EqHO f, EqHO g) => EqHO (Sum f g) where
  eqHO :: Sum f g k -> Sum f g k -> Bool
eqHO (InL fx :: f k
fx) (InL fy :: f k
fy) = f k -> f k -> Bool
forall ki (f :: ki -> *) (k :: ki). EqHO f => f k -> f k -> Bool
eqHO f k
fx f k
fy
  eqHO (InR gx :: g k
gx) (InR gy :: g k
gy) = g k -> g k -> Bool
forall ki (f :: ki -> *) (k :: ki). EqHO f => f k -> f k -> Bool
eqHO g k
gx g k
gy
  eqHO _        _        = Bool
False

instance EqHO V1 where
  eqHO :: V1 k -> V1 k -> Bool
eqHO _ _ = Bool
True

instance EqHO U1 where
  eqHO :: U1 k -> U1 k -> Bool
eqHO _ _ = Bool
True



-- |Higher order, poly kinded, version of 'Show'; We provide
-- the same 'showsPrec' mechanism. The documentation of "Text.Show"
-- has a good example of the correct usage of 'showsPrec':
--
-- > 
-- > infixr 5 :^:
-- > data Tree a =  Leaf a  |  Tree a :^: Tree a
-- >
-- > instance (Show a) => Show (Tree a) where
-- >   showsPrec d (Leaf m) = showParen (d > app_prec) $
-- >        showString "Leaf " . showsPrec (app_prec+1) m
-- >     where app_prec = 10
-- > 
-- >   showsPrec d (u :^: v) = showParen (d > up_prec) $
-- >        showsPrec (up_prec+1) u .
-- >        showString " :^: "      .
-- >        showsPrec (up_prec+1) v
-- >     where up_prec = 5
--
class ShowHO (f :: ki -> *) where
  showHO      :: forall k . f k -> String
  showsPrecHO :: forall k . Int -> f k -> ShowS
  {-# MINIMAL showHO | showsPrecHO #-}

  showHO fx :: f k
fx          = Int -> f k -> ShowS
forall ki (f :: ki -> *) (k :: ki). ShowHO f => Int -> f k -> ShowS
showsPrecHO 0 f k
fx ""
  showsPrecHO _ fx :: f k
fx s :: String
s = f k -> String
forall ki (f :: ki -> *) (k :: ki). ShowHO f => f k -> String
showHO f k
fx String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s

instance Show a => ShowHO (Const a) where
  showsPrecHO :: Int -> Const a k -> ShowS
showsPrecHO d :: Int
d (Const a :: a
a) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
app_prec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
      String -> ShowS
showString "Const " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
app_prec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) a
a
    where app_prec :: Int
app_prec = 10

instance (ShowHO f , ShowHO g) => ShowHO (f :*: g) where
  showsPrecHO :: Int -> (:*:) f g k -> ShowS
showsPrecHO d :: Int
d (x :: f k
x :*: y :: g k
y) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
app_prec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
                            Int -> f k -> ShowS
forall ki (f :: ki -> *) (k :: ki). ShowHO f => Int -> f k -> ShowS
showsPrecHO (Int
app_precInt -> Int -> Int
forall a. Num a => a -> a -> a
+1) f k
x
                          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString " :*: "
                          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> g k -> ShowS
forall ki (f :: ki -> *) (k :: ki). ShowHO f => Int -> f k -> ShowS
showsPrecHO (Int
app_precInt -> Int -> Int
forall a. Num a => a -> a -> a
+1) g k
y
    where app_prec :: Int
app_prec = 10

instance (ShowHO f , ShowHO g) => ShowHO (Sum f g) where
  showsPrecHO :: Int -> Sum f g k -> ShowS
showsPrecHO d :: Int
d (InL fx :: f k
fx) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
app_prec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
      String -> ShowS
showString "InL " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> f k -> ShowS
forall ki (f :: ki -> *) (k :: ki). ShowHO f => Int -> f k -> ShowS
showsPrecHO (Int
app_prec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) f k
fx
    where app_prec :: Int
app_prec = 10
  showsPrecHO d :: Int
d (InR gx :: g k
gx) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
app_prec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
      String -> ShowS
showString "InR " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> g k -> ShowS
forall ki (f :: ki -> *) (k :: ki). ShowHO f => Int -> f k -> ShowS
showsPrecHO (Int
app_prec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) g k
gx
    where app_prec :: Int
app_prec = 10

-- |Existential type wrapper. This comesin particularly
-- handy when we want to add mrsop terms to
-- some container. See "Generics.MRSOP.Holes.Unify" for example.
data Exists (f :: k -> *) :: * where
  Exists :: f x -> Exists f

-- |Maps over 'Exists'
exMap :: (forall x . f x -> g x) -> Exists f -> Exists g
exMap :: (forall (x :: k). f x -> g x) -> Exists f -> Exists g
exMap f :: forall (x :: k). f x -> g x
f (Exists x :: f x
x) = g x -> Exists g
forall k (f :: k -> *) (x :: k). f x -> Exists f
Exists (f x -> g x
forall (x :: k). f x -> g x
f f x
x)

-- |Maps a monadic actino over 'Exists'
exMapM :: (Monad m) => (forall x . f x -> m (g x)) -> Exists f -> m (Exists g)
exMapM :: (forall (x :: k). f x -> m (g x)) -> Exists f -> m (Exists g)
exMapM f :: forall (x :: k). f x -> m (g x)
f (Exists x :: f x
x) = g x -> Exists g
forall k (f :: k -> *) (x :: k). f x -> Exists f
Exists (g x -> Exists g) -> m (g x) -> m (Exists g)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f x -> m (g x)
forall (x :: k). f x -> m (g x)
f f x
x

-- |eliminates an 'Exists'
exElim :: (forall x . f x -> a) -> Exists f -> a
exElim :: (forall (x :: k). f x -> a) -> Exists f -> a
exElim f :: forall (x :: k). f x -> a
f (Exists x :: f x
x) = f x -> a
forall (x :: k). f x -> a
f f x
x

instance ShowHO f => Show (Exists f) where
  show :: Exists f -> String
show = (forall (x :: k). f x -> String) -> Exists f -> String
forall k (f :: k -> *) a.
(forall (x :: k). f x -> a) -> Exists f -> a
exElim forall (x :: k). f x -> String
forall ki (f :: ki -> *) (k :: ki). ShowHO f => f k -> String
showHO

-- Boolean predicate about being element of a list
type family IsElem (a :: k) (as :: [ k ]) :: Bool where
  IsElem a (a ': as) = 'True
  IsElem a (b ': as) = IsElem a as
  IsElem a '[]       = 'False

-- An actual proof that something is an element
data ElemPrf a as where
  Here  :: ElemPrf a (a ': as)
  There :: ElemPrf a as -> ElemPrf a (b ': as)

-- Constructing these proofs
class HasElem a as where
  hasElem :: ElemPrf a as
instance {-# OVERLAPPING #-} HasElem a (a ': as) where
  hasElem :: ElemPrf a (a : as)
hasElem = ElemPrf a (a : as)
forall a (a :: a) (as :: [a]). ElemPrf a (a : as)
Here
instance {-# OVERLAPPABLE #-}
    (HasElem a as) => HasElem a (b ': as) where
  hasElem :: ElemPrf a (b : as)
hasElem = ElemPrf a as -> ElemPrf a (b : as)
forall a (a :: a) (as :: [a]) (b :: a).
ElemPrf a as -> ElemPrf a (b : as)
There ElemPrf a as
forall k (a :: k) (as :: [k]). HasElem a as => ElemPrf a as
hasElem

-- |We will carry constructive information on the
-- constraint. Forcing 'IsElem' to true 
type Elem    a as = (IsElem a as ~ 'True , HasElem a as)

-- |Negation of 'Elem'
type NotElem a as = IsElem a as ~ 'False

-- |Returns whether two types are the same, given that
-- both belong to the same list.
sameTy :: forall fam x y . (Elem x fam , Elem y fam) 
      => Proxy fam -> Proxy x -> Proxy y -> Maybe (x :~: y)
sameTy :: Proxy fam -> Proxy x -> Proxy y -> Maybe (x :~: y)
sameTy _ _ _ = ElemPrf x fam -> ElemPrf y fam -> Maybe (x :~: y)
forall (fam' :: [k]) (b :: k).
ElemPrf x fam' -> ElemPrf b fam' -> Maybe (x :~: b)
go (ElemPrf x fam
forall k (a :: k) (as :: [k]). HasElem a as => ElemPrf a as
hasElem :: ElemPrf x fam) (ElemPrf y fam
forall k (a :: k) (as :: [k]). HasElem a as => ElemPrf a as
hasElem :: ElemPrf y fam)
 where
   go :: ElemPrf x fam' -> ElemPrf b fam' -> Maybe (x :~: b)
   go :: ElemPrf x fam' -> ElemPrf b fam' -> Maybe (x :~: b)
go Here       Here      = (x :~: x) -> Maybe (x :~: x)
forall a. a -> Maybe a
Just x :~: x
forall k (a :: k). a :~: a
Refl
   go (There rr :: ElemPrf x as
rr) (There y :: ElemPrf b as
y) = ElemPrf x as -> ElemPrf b as -> Maybe (x :~: b)
forall (fam' :: [k]) (b :: k).
ElemPrf x fam' -> ElemPrf b fam' -> Maybe (x :~: b)
go ElemPrf x as
rr ElemPrf b as
ElemPrf b as
y
   go _          _         = Maybe (x :~: b)
forall a. Maybe a
Nothing

type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint where
  All c '[]       = ()
  All c (x ': xs) = (c x , All c xs)

-- |Carries information about @x@ being an instance of @c@
data Witness c x where
  Witness :: (c x) => Witness c x

-- |Provides the witness that @x@ is an instance of @c@
witness :: forall x xs c
         . (HasElem x xs , All c xs)
        => Proxy xs -> Witness c x
witness :: Proxy xs -> Witness c x
witness _ = ElemPrf x xs -> Witness c x
forall k (c :: k -> Constraint) (xs :: [k]) (x :: k).
All c xs =>
ElemPrf x xs -> Witness c x
witnessPrf (ElemPrf x xs
forall k (a :: k) (as :: [k]). HasElem a as => ElemPrf a as
hasElem :: ElemPrf x xs)

-- |Fetches the 'Eq' instance for an element of a list
weq :: forall x xs
     . (All Eq xs , Elem x xs)
    => Proxy xs -> x -> x -> Bool
weq :: Proxy xs -> x -> x -> Bool
weq p :: Proxy xs
p = case Proxy xs -> Witness Eq x
forall k (x :: k) (xs :: [k]) (c :: k -> Constraint).
(HasElem x xs, All c xs) =>
Proxy xs -> Witness c x
witness Proxy xs
p :: Witness Eq x of
            Witness -> x -> x -> Bool
forall a. Eq a => a -> a -> Bool
(==)

-- |Fetches the 'Eq' instance for an element of a list
wshow :: forall x xs
       . (All Show xs , Elem x xs)
      => Proxy xs -> x -> String
wshow :: Proxy xs -> x -> String
wshow p :: Proxy xs
p = case Proxy xs -> Witness Show x
forall k (x :: k) (xs :: [k]) (c :: k -> Constraint).
(HasElem x xs, All c xs) =>
Proxy xs -> Witness c x
witness Proxy xs
p :: Witness Show x of
            Witness -> x -> String
forall a. Show a => a -> String
show

-- |Provides the witness that @x@ is an instance of @c@
witnessPrf :: (All c xs) => ElemPrf x xs -> Witness c x
witnessPrf :: ElemPrf x xs -> Witness c x
witnessPrf Here      = Witness c x
forall k (c :: k -> Constraint) (x :: k). c x => Witness c x
Witness
witnessPrf (There p :: ElemPrf x as
p) = ElemPrf x as -> Witness c x
forall k (c :: k -> Constraint) (xs :: [k]) (x :: k).
All c xs =>
ElemPrf x xs -> Witness c x
witnessPrf ElemPrf x as
p