{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

module Ema.Route.Generic.RGeneric (
  RGeneric (RCode, rfrom, rto),
  RHasDatatypeInfo (RDatatypeName, RConstructorNames),
) where

import GHC.TypeLits (ErrorMessage (Text), TypeError)
import GHC.TypeLits.Extra (Impossible (impossible), TypeErr)
import Generics.SOP
import Generics.SOP.Type.Metadata qualified as SOPM
import Prelude hiding (All, Generic)

-- | Like `Generic` but for Route types only.
class (Generic r, HasDatatypeInfo r) => RGeneric r where
  type RCode r :: [Type]
  rfrom :: r -> NS I (RCode r)
  rto :: NS I (RCode r) -> r

class (RGeneric r, HasDatatypeInfo r) => RHasDatatypeInfo r where
  type RDatatypeName r :: SOPM.DatatypeName
  type RConstructorNames r :: [SOPM.ConstructorName]

instance (Generic r, HasDatatypeInfo r, RGeneric' (Code r), All RouteNP (Code r)) => RGeneric r where
  type RCode r = RCode' (Code r)
  rfrom :: r -> NS @Type I (RCode r)
rfrom = forall (xss :: [[Type]]).
RGeneric' xss =>
NS @[Type] (NP @Type I) xss -> NS @Type I (RCode' xss)
rfrom' @(Code r) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> Type) (xss :: [[k]]).
SOP @k f xss -> NS @[k] (NP @k f) xss
unSOP forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Generic a => a -> Rep a
from
  rto :: NS @Type I (RCode r) -> r
rto = forall a. Generic a => Rep a -> a
to forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k -> Type) (xss :: [[k]]).
NS @[k] (NP @k f) xss -> SOP @k f xss
SOP forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (xss :: [[Type]]).
RGeneric' xss =>
NS @Type I (RCode' xss) -> NS @[Type] (NP @Type I) xss
rto' @(Code r)

instance (RGeneric r, HasDatatypeInfo r) => RHasDatatypeInfo r where
  type RDatatypeName r = RDatatypeName' (DatatypeInfoOf r)
  type RConstructorNames r = RConstructorNames' (DatatypeInfoOf r)

class RGeneric' (xss :: [[Type]]) where
  type RCode' xss :: [Type]
  rfrom' :: NS (NP I) xss -> NS I (RCode' xss)
  rto' :: NS I (RCode' xss) -> NS (NP I) xss

instance RGeneric' '[] where
  type RCode' '[] = '[]
  rfrom' :: NS @[Type] (NP @Type I) ('[] @[Type])
-> NS @Type I (RCode' ('[] @[Type]))
rfrom' = \case {}
  rto' :: NS @Type I (RCode' ('[] @[Type]))
-> NS @[Type] (NP @Type I) ('[] @[Type])
rto' = \case {}

instance (RGeneric' xss, RouteNP xs) => RGeneric' (xs ': xss) where
  type RCode' (xs ': xss) = RouteNPType xs ': RCode' xss
  rfrom' :: NS @[Type] (NP @Type I) ((':) @[Type] xs xss)
-> NS @Type I (RCode' ((':) @[Type] xs xss))
rfrom' = \case
    Z NP @Type I x
routeNP -> forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
Z forall a b. (a -> b) -> a -> b
$ forall a. a -> I a
I forall a b. (a -> b) -> a -> b
$ forall (xs :: [Type]).
RouteNP xs =>
NP @Type I xs -> RouteNPType xs
fromRouteNP NP @Type I x
routeNP
    S NS @[Type] (NP @Type I) xs
rest -> forall {k} (a :: k -> Type) (xs :: [k]) (x :: k).
NS @k a xs -> NS @k a ((':) @k x xs)
S forall a b. (a -> b) -> a -> b
$ forall (xss :: [[Type]]).
RGeneric' xss =>
NS @[Type] (NP @Type I) xss -> NS @Type I (RCode' xss)
rfrom' @xss NS @[Type] (NP @Type I) xs
rest
  rto' :: NS @Type I (RCode' ((':) @[Type] xs xss))
-> NS @[Type] (NP @Type I) ((':) @[Type] xs xss)
rto' = \case
    Z (I x
t) -> forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS @k a ((':) @k x xs)
Z forall a b. (a -> b) -> a -> b
$ forall (xs :: [Type]).
RouteNP xs =>
RouteNPType xs -> NP @Type I xs
toRouteNP x
t
    S NS @Type I xs
rest -> forall {k} (a :: k -> Type) (xs :: [k]) (x :: k).
NS @k a xs -> NS @k a ((':) @k x xs)
S forall a b. (a -> b) -> a -> b
$ forall (xss :: [[Type]]).
RGeneric' xss =>
NS @Type I (RCode' xss) -> NS @[Type] (NP @Type I) xss
rto' @xss NS @Type I xs
rest

type family RDatatypeName' (info :: SOPM.DatatypeInfo) :: SOPM.DatatypeName where
  RDatatypeName' ( 'SOPM.ADT _ name _ _) =
    name
  RDatatypeName' ( 'SOPM.Newtype _ name _) =
    name

type family RConstructorNames' (info :: SOPM.DatatypeInfo) :: [SOPM.ConstructorName] where
  RConstructorNames' ( 'SOPM.ADT _ _ constrs _) =
    GetConstructorNames constrs
  RConstructorNames' ( 'SOPM.Newtype _ _ constr) =
    '[GetConstructorName constr]

type family GetConstructorName (info :: SOPM.ConstructorInfo) :: SOPM.ConstructorName where
  GetConstructorName ( 'SOPM.Constructor name) =
    name
  GetConstructorName ( 'SOPM.Infix name _ _) =
    name
  GetConstructorName ( 'SOPM.Record name _) =
    name

type family GetConstructorNames (infos :: [SOPM.ConstructorInfo]) :: [SOPM.ConstructorName] where
  GetConstructorNames '[] = '[]
  GetConstructorNames (x ': xs) = GetConstructorName x ': GetConstructorNames xs

{- | Class of `NP` that can be used in a route tyupe.

    Ensures that the constructor can have 0 or 1 products only.
-}
class RouteNP (xs :: [Type]) where
  type RouteNPType xs :: Type
  fromRouteNP :: NP I xs -> RouteNPType xs
  toRouteNP :: RouteNPType xs -> NP I xs

instance RouteNP '[] where
  type RouteNPType '[] = ()
  fromRouteNP :: NP @Type I ('[] @Type) -> RouteNPType ('[] @Type)
fromRouteNP NP @Type I ('[] @Type)
Nil = ()
  toRouteNP :: RouteNPType ('[] @Type) -> NP @Type I ('[] @Type)
toRouteNP () = forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil

instance RouteNP (x ': '[]) where
  type RouteNPType (x ': '[]) = x
  fromRouteNP :: NP @Type I ((':) @Type x ('[] @Type))
-> RouteNPType ((':) @Type x ('[] @Type))
fromRouteNP (I x
x :* NP @Type I xs
Nil) = x
x
  toRouteNP :: RouteNPType ((':) @Type x ('[] @Type))
-> NP @Type I ((':) @Type x ('[] @Type))
toRouteNP RouteNPType ((':) @Type x ('[] @Type))
x = forall a. a -> I a
I RouteNPType ((':) @Type x ('[] @Type))
x forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP @k a xs -> NP @k a ((':) @k x xs)
:* forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil

instance (TypeErr ( 'Text "MultiRoute: too many arguments")) => RouteNP (x ': x' ': xs) where
  type RouteNPType (x ': x' ': xs) = TypeError ( 'Text "MultiRoute: too many arguments")
  fromRouteNP :: NP @Type I ((':) @Type x ((':) @Type x' xs))
-> RouteNPType ((':) @Type x ((':) @Type x' xs))
fromRouteNP NP @Type I ((':) @Type x ((':) @Type x' xs))
_ = forall a. Impossible => a
impossible
  toRouteNP :: RouteNPType ((':) @Type x ((':) @Type x' xs))
-> NP @Type I ((':) @Type x ((':) @Type x' xs))
toRouteNP RouteNPType ((':) @Type x ((':) @Type x' xs))
_ = forall a. Impossible => a
impossible