{-# 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 fx gx = f (fx :*: gx)

-- |Lifted uncurry
uncurry' :: (f x -> g x -> a) -> (f :*: g) x -> a
uncurry' f (fx :*: gx) = f fx 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 fx = fx :*: fx

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

-- |Higher-order sum eliminator
either' :: (f :-> r) -> (g :-> r) -> Sum f g :-> r
either' f _ (InL x) = f x
either' _ g (InR x) = g 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'' f g = getConst . either' (Const . f) (Const . g)

infixr 8 <.>
-- |Kleisli Composition
(<.>) :: (Monad m) => (b -> m c) -> (a -> m b) -> a -> m c
f <.> g = (>>= f) . 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) (Const b) = a == b

instance (EqHO f, EqHO g) => EqHO (f :*: g) where
  eqHO (fx :*: gx) (fy :*: gy) = eqHO fx fy && eqHO gx gy

instance (EqHO f, EqHO g) => EqHO (Sum f g) where
  eqHO (InL fx) (InL fy) = eqHO fx fy
  eqHO (InR gx) (InR gy) = eqHO gx gy
  eqHO _        _        = False

instance EqHO V1 where
  eqHO _ _ = True

instance EqHO U1 where
  eqHO _ _ = 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          = showsPrecHO 0 fx ""
  showsPrecHO _ fx s = showHO fx ++ s

instance Show a => ShowHO (Const a) where
  showsPrecHO d (Const a) = showParen (d > app_prec) $
      showString "Const " . showsPrec (app_prec + 1) a
    where app_prec = 10

instance (ShowHO f , ShowHO g) => ShowHO (f :*: g) where
  showsPrecHO d (x :*: y) = showParen (d > app_prec) $
                            showsPrecHO (app_prec+1) x
                          . showString " :*: "
                          . showsPrecHO (app_prec+1) y
    where app_prec = 10

instance (ShowHO f , ShowHO g) => ShowHO (Sum f g) where
  showsPrecHO d (InL fx) = showParen (d > app_prec) $
      showString "InL " . showsPrecHO (app_prec + 1) fx
    where app_prec = 10
  showsPrecHO d (InR gx) = showParen (d > app_prec) $
      showString "InR " . showsPrecHO (app_prec + 1) gx
    where 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 f (Exists x) = Exists (f x)

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

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

instance ShowHO f => Show (Exists f) where
  show = exElim 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 = Here
instance {-# OVERLAPPABLE #-}
    (HasElem a as) => HasElem a (b ': as) where
  hasElem = There 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 _ _ _ = go (hasElem :: ElemPrf x fam) (hasElem :: ElemPrf y fam)
 where
   go :: ElemPrf x fam' -> ElemPrf b fam' -> Maybe (x :~: b)
   go Here       Here      = Just Refl
   go (There rr) (There y) = go rr y
   go _          _         = 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 _ = witnessPrf (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 p = case witness p :: Witness Eq x of
            Witness -> (==)

-- |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 p = case witness p :: Witness Show x of
            Witness -> show

-- |Provides the witness that @x@ is an instance of @c@
witnessPrf :: (All c xs) => ElemPrf x xs -> Witness c x
witnessPrf Here      = Witness
witnessPrf (There p) = witnessPrf p