{-# language GADTs,
             DataKinds,
             PolyKinds,
             TypeOperators,
             ConstraintKinds,
             MultiParamTypeClasses,
             FlexibleContexts,
             FlexibleInstances,
             QuantifiedConstraints,
             UndecidableInstances,
             KindSignatures,
             TypeFamilies #-}
module Generics.Simplistic (
  -- * From `GHC.Generics.Extra` module
  Generic, Rep, Generic1, Rep1,
  V1, U1, (:+:), (:*:), K1, M1, (:=>:),
  -- * Simplistic representation on `*` types 
  SMeta(..), SRep(..), GenericSy, fromS, toS, fromI, toI,
  -- ** Constraints over the leaves of a data type
  OnLeaves,
  -- * Simplistic representation on `* -> *` types 
  SRep1(..), GenericSy1, fromS1, toS1,
  -- ** Constraints over the leaves of a data type
  OnLeaves1,
  -- * Auxiliary constraints
  Implies, Trivial
) where

import Control.Comonad
import Data.Functor.Identity
import Data.Constraints
import GHC.Generics.Extra
import GHC.Exts (Constraint)

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

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)

type GenericSy a = (Generic a, Sy (Rep a))

fromS :: (GenericSy a, Applicative w) => a -> SRep w (Rep a)
fromS = fromS' . from
fromI :: (GenericSy a) => a -> SRep Identity (Rep a)
fromI = fromS
toS :: (GenericSy a, Comonad w) => SRep w (Rep a) -> a
toS = to . toS'
toI :: (GenericSy a) => SRep Identity (Rep a) -> a
toI = toS

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)

infixr 5 :***:
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 GenericSy1 f = (Generic1 f, Sy1 (Rep1 f))

fromS1 :: (GenericSy1 f) => f a -> SRep1 (Rep1 f) a
fromS1 = fromS1' . from1
toS1 :: (GenericSy1 f) => SRep1 (Rep1 f) a -> f a
toS1 = to1 . toS1'

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)

-- Internal instances
class SMety i t where
  smeta :: SMeta i t
instance Datatype d => SMety D d where
  smeta = SM_D
instance Constructor c => SMety C c where
  smeta = SM_C
instance Selector s => SMety S s where
  smeta = SM_S
class Sy f where
  fromS' :: Applicative w => f a -> SRep w f
  toS'   :: Comonad     w => SRep w f -> f a
instance Sy V1 where
  fromS' = undefined
  toS'   = undefined
instance Sy U1 where
  fromS' U1 = S_U1
  toS'   S_U1 = U1
instance (Sy f, Sy g) => Sy (f :+: g) where
  fromS' (L1 x) = S_L1 (fromS' x)
  fromS' (R1 y) = S_R1 (fromS' y)
  toS'   (S_L1 x) = L1 (toS' x)
  toS'   (S_R1 y) = R1 (toS' y)
instance (Sy f, Sy g) => Sy (f :*: g) where
  fromS' (x :*: y) = fromS' x :**: fromS' y
  toS'   (x :**: y) = toS' x :*: toS' y
instance Sy (K1 i a) where
  fromS' (K1 x) = S_K1 (pure x)
  toS'   (S_K1 x) = K1 (extract x)
instance (SMety i t, Sy f) => Sy (M1 i t f) where
  fromS' (M1 x) = S_M1 smeta (fromS' x)
  toS'   (S_M1 _ x) = M1 (toS' x)
instance (c => Sy f) => Sy (c :=>: f) where
  fromS' (SuchThat x) = S_ST (fromS' x)
  toS'   (S_ST x) = SuchThat (toS' x)

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