{-# LANGUAGE ConstraintKinds         #-}
{-# LANGUAGE DataKinds               #-}
{-# LANGUAGE DefaultSignatures       #-}
{-# LANGUAGE DeriveGeneric           #-}
{-# LANGUAGE FlexibleContexts        #-}
{-# LANGUAGE FlexibleInstances       #-}
{-# LANGUAGE GADTs                   #-}
{-# LANGUAGE KindSignatures          #-}
{-# LANGUAGE MultiParamTypeClasses   #-}
{-# LANGUAGE PolyKinds               #-}
{-# LANGUAGE QuantifiedConstraints   #-}
{-# LANGUAGE RankNTypes              #-}
{-# LANGUAGE ScopedTypeVariables     #-}
{-# LANGUAGE StandaloneDeriving      #-}
{-# LANGUAGE TypeFamilies            #-}
{-# LANGUAGE TypeOperators           #-}
{-# LANGUAGE UndecidableInstances    #-}
-- |Introduces closed representations functor
-- for "GHC.Generics" style generics.
module Generics.Simplistic
  ( -- ** Re-exports from "GHC.Generics.Extra" module
    Generic, Rep, Rep1, Par1, Rec1, (:.:)(..), V1, U1(..), (:+:)(..)
  , (:*:)(..), K1(..), M1(..), (:=>:)(..), R
  -- * Simplistic representation on @*@ types
  , GMeta(..), SMeta(..), SMetaI(..), SRep(..) , I(..) , Simplistic
  -- ** Constraints over the leaves of a data type
  , OnLeaves
  -- ** Combinators
  -- *** Maps , zips and folds
  , repMap , repMapM , repMapCM
  , zipSRep , repLeaves , repLeavesC , repLeavesList
  -- *** Metadata
  , getDatatypeName , getConstructorName
  , repDatatypeName , repConstructorName
  -- ** Shallow Conversion
  , fromS , toS , GShallow(..)
  -- * Simplistic representation on @* -> *@ types
  , SRep1(..) , OnLeaves1 , fromS1 , toS1 , GShallow1(..) , Simplistic1
  -- * Auxiliary constraints
  , Implies, Trivial
  ) where

import Data.Proxy
import Control.Monad.Identity
import Control.DeepSeq

import GHC.Generics
import GHC.Generics.Extra
import GHC.Exts (Constraint)

import Generics.Simplistic.Util 

---------------------
-- Representations --
---------------------

data SMeta i t where
  SM_D :: Datatype    d => SMeta D d
  SM_C :: Constructor c => SMeta C c
  SM_S :: Selector    s => SMeta S s
deriving instance Show (SMeta i t)
deriving instance Eq   (SMeta i t)

-- Dirty trick to access the dictionaries I need
data SMetaI d f x = SMetaI

smetaI :: SMeta i t -> SMetaI t Proxy ()
smetaI _ = SMetaI

getDatatypeName :: SMeta D d -> String
getDatatypeName x@SM_D = datatypeName (smetaI x)

getConstructorName :: SMeta C c -> String
getConstructorName x@SM_C = conName (smetaI x)

-- |Singletons for metainformation
class GMeta i c where
  smeta :: SMeta i c

instance Constructor c => GMeta C c where
  smeta = SM_C

instance Datatype d => GMeta D d where
  smeta = SM_D

instance Selector s => GMeta S s where
  smeta = SM_S

-- |Given some @a@, a value of type @SRep w (Rep a)@ is
-- a closed representation of a generic value of type @a@.
infixr 5 :**:
data SRep w f where
  S_U1   ::                          SRep w U1
  S_L1   ::              SRep w f -> SRep w (f :+: g)
  S_R1   ::              SRep w g -> SRep w (f :+: g)
  (:**:) :: SRep w f  -> SRep w g -> SRep w (f :*: g)
  S_K1   ::              w a      -> SRep w (K1 i a)
  S_M1   :: SMeta i t -> SRep w f -> SRep w (M1 i t f)
  S_ST   ::         c => SRep w f -> SRep w (c :=>: f)
deriving instance (forall a. Show (w a)) => Show (SRep w f)
deriving instance (forall a. Eq   (w a)) => Eq   (SRep w f)
instance (forall x . NFData (w x)) => NFData (SRep w f) where
  rnf S_U1       = ()
  rnf (S_K1 w)   = rnf w
  rnf (S_M1 _ x) = rnf x
  rnf (S_L1 x)   = rnf x
  rnf (S_R1 x)   = rnf x
  rnf (x :**: y) = rnf x `seq` rnf y
  rnf (S_ST x)   = rnf x 

-- |All types supported by "GHC.Generics" are /simplistic/, this
-- constraint just couples their necessary together.
type Simplistic a = (Generic a , GShallow (Rep a))

-- |Computes the constraint that corresponds to ensuring all
-- leaves of a representation satisfy a given constraint.
-- For example,
--
-- > OnLeaves Eq (Rep (Either a b)) = (Eq a , Eq b)
--
type family OnLeaves (c :: * -> Constraint) (f :: * -> *) :: Constraint where
  OnLeaves c V1        = ()
  OnLeaves c U1        = ()
  OnLeaves c (f :+: g)  = (OnLeaves c f, OnLeaves c g)
  OnLeaves c (f :*: g)  = (OnLeaves c f, OnLeaves c g)
  OnLeaves c (K1 i a)   = c a
  OnLeaves c (M1 i p f) = OnLeaves c f
  OnLeaves c (d :=>: f) = Implies d (OnLeaves c f)

-- |Retrieves the datatype name for a representation.
-- /WARNING; UNSAFE/ this function only works if @f@ is the representation of
-- a type constructed with "GHC.Generics" builtin mechanisms.
repDatatypeName :: SRep w f -> String
repDatatypeName (S_M1 x@SM_D _)
  = getDatatypeName x
repDatatypeName (S_M1 _ x)
  = repDatatypeName x
repDatatypeName (S_L1 x)
  = repDatatypeName x
repDatatypeName (S_R1 x)
  = repDatatypeName x
repDatatypeName _
  = error "Please; use GHC's deriving mechanism. This keeps M1's at the top of the Rep"

-- |Retrieves the constructor name for a representation.
-- /WARNING; UNSAFE/ this function only works if @f@ is the representation of
-- a type constructed with "GHC.Generics" builtin mechanisms.
repConstructorName :: SRep w f -> String
repConstructorName (S_M1 x@SM_C _)
  = getConstructorName x
repConstructorName (S_M1 _ x)
  = repConstructorName x
repConstructorName (S_L1 x)
  = repConstructorName x
repConstructorName (S_R1 x)
  = repConstructorName x
repConstructorName _
  = error "Please; use GHC's deriving mechanism. This keeps M1's at the top of the Rep"

-- |Zips two representations together if they are made up of
-- the same constructor. For example,
--
-- > zipSRep (fromS (: 1 [])) (fromS (: 2 (: 3 [])))
-- >  == Just (fromS (: (1 , 2) ([] , [3])))
-- >
-- > zipSRep (fromS (: 1 [])) (fromS [])
-- >  == Nothing
zipSRep :: SRep w f -> SRep z f -> Maybe (SRep (w :*: z) f)
zipSRep S_U1         S_U1         = return S_U1
zipSRep (S_L1 x)     (S_L1 y)     = S_L1 <$> zipSRep x y
zipSRep (S_R1 x)     (S_R1 y)     = S_R1 <$> zipSRep x y
zipSRep (S_M1 m x)   (S_M1 _ y)   = S_M1 m <$> zipSRep x y
zipSRep (x1 :**: x2) (y1 :**: y2) = (:**:) <$> (zipSRep x1 y1) <*> (zipSRep x2 y2)
zipSRep (S_K1 x)     (S_K1 y)     = return $ S_K1 (x :*: y)
zipSRep _            _            = Nothing

-- |Performs a /crush/ over the leaves of a 'SRep' carrying a constraint
-- around.
repLeavesC :: (OnLeaves c rep)
           => Proxy c
           -> (forall x . c x => w x -> r) -- ^ leaf extraction
           -> (r -> r -> r)         -- ^ join product
           -> r                     -- ^ empty
           -> SRep w rep -> r
repLeavesC _ _ _ e S_U1       = e
repLeavesC p l j e (S_L1 x)   = repLeavesC p l j e x
repLeavesC p l j e (S_R1 x)   = repLeavesC p l j e x
repLeavesC p l j e (S_M1 _ x) = repLeavesC p l j e x
repLeavesC p l j e (x :**: y) = j (repLeavesC p l j e x) (repLeavesC p l j e y)
repLeavesC _ l _ _ (S_K1 x)   = l x
repLeavesC p l j e (S_ST x)   = repLeavesC p l j e x


-- |Performs a /crush/ over the leaves of a 'SRep'
repLeaves :: (forall x . w x -> r) -- ^ leaf extraction
          -> (r -> r -> r)         -- ^ join product
          -> r                     -- ^ empty
          -> SRep w rep -> r
repLeaves _ _ e S_U1       = e
repLeaves l j e (S_L1 x)   = repLeaves l j e x
repLeaves l j e (S_R1 x)   = repLeaves l j e x
repLeaves l j e (S_M1 _ x) = repLeaves l j e x
repLeaves l j e (x :**: y) = j (repLeaves l j e x) (repLeaves l j e y)
repLeaves l _ _ (S_K1 x)   = l x
repLeaves l j e (S_ST x)   = repLeaves l j e x

-- |Example of 'repLeaves' that places the values of @w@ inside
-- a list.
repLeavesList :: SRep w rep -> [Exists w]
repLeavesList = repLeaves ((:[]) . Exists) (++) []

-- |Maps a function over a representation taking into
-- account that the leaves of the representation satisfy
-- a given constraint.
repMapCM :: (Monad m , OnLeaves c rep)
         => Proxy c -- ^ Which constraint shall be threaded through
         -> (forall y . c y => f y -> m (g y))
         -> SRep f rep -> m (SRep g rep)
repMapCM _p _f (S_U1)     = return S_U1
repMapCM _p f  (S_K1 x)   = S_K1   <$> f x
repMapCM p  f  (S_M1 m x) = S_M1 m <$> repMapCM p f x
repMapCM p  f  (S_L1 x)   = S_L1   <$> repMapCM p f x
repMapCM p  f  (S_R1 x)   = S_R1   <$> repMapCM p f x
repMapCM p  f  (x :**: y) = (:**:) <$> repMapCM p f x <*> repMapCM p f y
repMapCM p  f  (S_ST x)   = S_ST   <$> repMapCM p f x 

-- |Maps a monadic function over the representation
repMapM :: (Monad m)
        => (forall y . f y -> m (g y))
        -> SRep f rep -> m (SRep g rep)
repMapM _f (S_U1)    = return S_U1
repMapM f (S_K1 x)   = S_K1 <$> f x
repMapM f (S_M1 m x) = S_M1 m <$> repMapM f x
repMapM f (S_L1 x)   = S_L1 <$> repMapM f x
repMapM f (S_R1 x)   = S_R1 <$> repMapM f x
repMapM f (S_ST x)   = S_ST <$> repMapM f x
repMapM f (x :**: y)
  = (:**:) <$> repMapM f x <*> repMapM f y

-- |Maps a simple functino over the representation
repMap :: (forall y . f y -> g y)
       -> SRep f rep -> SRep g rep
repMap f = runIdentity . repMapM (return . f)

--------------------------------

-- |Identity functor
newtype I x = I { unI :: x }
  deriving Eq

instance Show x => Show (I x) where
  showsPrec p (I x) = showParen (p > 10) $ showString "I " . showsPrec 11 x
instance Functor I where
  fmap f (I x) = I (f x)
instance Applicative I where
  pure        = I
  I f <*> I x = I (f x)
instance Monad I where
  I x >>= f = f x

-- |Shallow conversion between "GHC.Generics" representation
-- and 'SRep'; The 'fromS' and 'toS' functions provide the
-- toplevel api.
class GShallow f where
  sfrom :: f x -> SRep I f
  sto   :: SRep I f -> f x

instance GShallow U1 where
  sfrom U1 = S_U1
  sto S_U1 = U1

instance (GShallow f , GShallow g) => GShallow (f :+: g) where
  sfrom (L1 x) = S_L1 (sfrom x)
  sfrom (R1 x) = S_R1 (sfrom x)
  sto (S_L1 x) = L1 (sto x)
  sto (S_R1 x) = R1 (sto x)

instance (GShallow f , GShallow g) => GShallow (f :*: g) where
  sfrom (x :*:  y) = sfrom x :**: sfrom y
  sto   (x :**: y) = sto x   :*:  sto y

instance (GShallow f , GMeta i c) => GShallow (M1 i c f) where
  sfrom (M1 x)   = S_M1 smeta (sfrom x)
  sto (S_M1 _ x) = M1 (sto x)

instance GShallow (K1 R x) where
  sfrom (K1 x) = S_K1 (I x)
  sto (S_K1 (I x)) = K1 x

-- |Converts a value of a generic type directly to its
-- (shallow) simplistic representation.
fromS :: (Simplistic a) => a -> SRep I (Rep a)
fromS = sfrom . from

-- |Converts a simplistic representation back to its corresponding
-- value of type @a@.
toS :: (Simplistic a) => SRep I (Rep a) -> a
toS = to . sto

-- TODO: Study whether it makes sense to add rules
--       and inline pragmas for performance.
-- {-# RULES "sfrom/sto" forall x.  sfrom (sto x) = x #-}
-- {-# RULES "sto/sfrom" forall x.  sto (sfrom x) = x #-}

---------------------------------------
---------------------------------------
-- Representation of `* -> *` types  --
---------------------------------------
---------------------------------------

-- $simplistic1
--
-- "GHC.Generics" provides 'Rep' for types of kind @*@
-- and 'Rep1' for types of kind @* -> *@. Similarly,
-- we also provide 'SRep1' for a closed-universe interpretation
-- of 'Rep1'. It is worth noting the support is limitted and
-- we have not yet written combinators for 'SRep1' like we
-- did for 'SRep'. An example usage of 'SRep1' can be found
-- in "Generics.Simplistic.Derive.Functor".

infixr 5 :***:

-- |Similar to 'SRep', but is indexed over the functors that
-- make up a 'Rep1', used to explicitely encode types with
-- one parameter. 
data SRep1 f x where
  S1_U1   ::                           SRep1 U1         x
  S1_L1   ::              SRep1 f x -> SRep1 (f :+: g)  x
  S1_R1   ::              SRep1 g x -> SRep1 (f :+: g)  x
  (:***:) :: SRep1 f x -> SRep1 g x -> SRep1 (f :*: g)  x
  S1_K1   ::          a             -> SRep1 (K1 i a)   x
  S1_M1   :: SMeta i t -> SRep1 f x -> SRep1 (M1 i t f) x
  S1_ST   ::        c =>  SRep1 f x -> SRep1 (c :=>: f) x
  S1_Par  ::          x             -> SRep1 Par1       x
  S1_Rec  ::          f x           -> SRep1 (Rec1 f)   x
  S1_Comp ::          f (SRep1 g x) -> SRep1 (f :.: g)  x

type Simplistic1 f = (Generic1 f, GShallow1 (Rep1 f))

type family OnLeaves1 (c :: * -> Constraint) (r :: (* -> *) -> Constraint)
                      (f :: * -> *) :: Constraint where
  OnLeaves1 c r V1         = ()
  OnLeaves1 c r U1         = ()
  OnLeaves1 c r (f :+: g)  = (OnLeaves1 c r f, OnLeaves1 c r g)
  OnLeaves1 c r (f :*: g)  = (OnLeaves1 c r f, OnLeaves1 c r g)
  OnLeaves1 c r (K1 i a)   = c a
  OnLeaves1 c r (M1 i p f) = OnLeaves1 c r f
  OnLeaves1 c r (d :=>: f) = Implies d (OnLeaves1 c r f)
  OnLeaves1 c r Par1       = ()
  OnLeaves1 c r (Rec1 f)   = r f
  OnLeaves1 c r (f :.: g)  = (r f, OnLeaves1 c r g)

-- |Converts a value of a generic type directly to its
-- (shallow) simplistic1 representation with a parameter.
fromS1 :: (Simplistic1 f) => f x -> SRep1 (Rep1 f) x
fromS1 = sfrom1 . from1

-- |Converts a simplistic1 representation back to its corresponding
-- value of type @a@.
toS1 :: (Simplistic1 f) => SRep1 (Rep1 f) x -> f x
toS1 = to1 . sto1

class GShallow1 f where
  sfrom1 :: f a -> SRep1 f a
  sto1   :: SRep1 f a -> f a
instance GShallow1 V1 where
  sfrom1 = undefined
  sto1   = undefined
instance GShallow1 U1 where
  sfrom1 U1 = S1_U1
  sto1   S1_U1 = U1
instance (GShallow1 f, GShallow1 g) => GShallow1 (f :+: g) where
  sfrom1 (L1 x) = S1_L1 (sfrom1 x)
  sfrom1 (R1 y) = S1_R1 (sfrom1 y)
  sto1   (S1_L1 x) = L1 (sto1 x)
  sto1   (S1_R1 y) = R1 (sto1 y)
instance (GShallow1 f, GShallow1 g) => GShallow1 (f :*: g) where
  sfrom1 (x :*: y) = sfrom1 x :***: sfrom1 y
  sto1   (x :***: y) = sto1 x :*: sto1 y
instance GShallow1 (K1 i a) where
  sfrom1 (K1 x) = S1_K1 x
  sto1   (S1_K1 x) = K1 x
instance (GMeta i t, GShallow1 f) => GShallow1 (M1 i t f) where
  sfrom1 (M1 x) = S1_M1 smeta (sfrom1 x)
  sto1   (S1_M1 _ x) = M1 (sto1 x)
instance (c => GShallow1 f) => GShallow1 (c :=>: f) where
  sfrom1 (SuchThat x) = S1_ST (sfrom1 x)
  sto1   (S1_ST x) = SuchThat (sto1 x)
instance GShallow1 Par1 where
  sfrom1 (Par1 x) = S1_Par x
  sto1   (S1_Par x) = Par1 x
instance GShallow1 (Rec1 f) where
  sfrom1 (Rec1 x) = S1_Rec x
  sto1   (S1_Rec x) = Rec1 x
instance (Functor f, GShallow1 g) => GShallow1 (f :.: g) where
  sfrom1 (Comp1 x) = S1_Comp (fmap sfrom1 x)
  sto1   (S1_Comp x) = Comp1 (fmap sto1 x)