{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE InstanceSigs          #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns        #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | Type-level metadata
module Debug.RecoverRTTI.Constr (
    Constr(..)
  , KnownConstr
  , knownConstr
  , prettyKnownConstr
  , elimKnownConstr
    -- | Compute all known constructors
  , Constrs
  , GConstrs
  , GConstrsOfType
  , ConstrOf
  , IsConstrOf(..)
  , checkIsConstrOf
  , Sing(..)
  ) where

import Data.Kind
import Data.List (intercalate)
import Data.SOP
import Data.Type.Equality
import GHC.Generics
import GHC.TypeLits

import Debug.RecoverRTTI.Util
import Debug.RecoverRTTI.Util.TypeLevel

{-------------------------------------------------------------------------------
  Type-level metadata
-------------------------------------------------------------------------------}

data Constr a = Constr {
      Constr a -> a
constrPkg  :: a
    , Constr a -> a
constrModl :: a
    , Constr a -> a
constrName :: a
    }
  deriving (Int -> Constr a -> ShowS
[Constr a] -> ShowS
Constr a -> String
(Int -> Constr a -> ShowS)
-> (Constr a -> String) -> ([Constr a] -> ShowS) -> Show (Constr a)
forall a. Show a => Int -> Constr a -> ShowS
forall a. Show a => [Constr a] -> ShowS
forall a. Show a => Constr a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Constr a] -> ShowS
$cshowList :: forall a. Show a => [Constr a] -> ShowS
show :: Constr a -> String
$cshow :: forall a. Show a => Constr a -> String
showsPrec :: Int -> Constr a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Constr a -> ShowS
Show, Constr a -> Constr a -> Bool
(Constr a -> Constr a -> Bool)
-> (Constr a -> Constr a -> Bool) -> Eq (Constr a)
forall a. Eq a => Constr a -> Constr a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Constr a -> Constr a -> Bool
$c/= :: forall a. Eq a => Constr a -> Constr a -> Bool
== :: Constr a -> Constr a -> Bool
$c== :: forall a. Eq a => Constr a -> Constr a -> Bool
Eq)

type family ConstrPkg  (c :: Constr a) :: a where ConstrPkg  ('Constr p _ _) = p
type family ConstrModl (c :: Constr a) :: a where ConstrModl ('Constr _ m _) = m
type family ConstrName (c :: Constr a) :: a where ConstrName ('Constr _ _ c) = c

class (
      KnownSymbol (ConstrPkg  c)
    , KnownSymbol (ConstrModl c)
    , KnownSymbol (ConstrName c)
    , c ~ 'Constr (ConstrPkg c) (ConstrModl c) (ConstrName c)
    ) => KnownConstr c
instance (
      KnownSymbol (ConstrPkg  c)
    , KnownSymbol (ConstrModl c)
    , KnownSymbol (ConstrName c)
    , c ~ 'Constr (ConstrPkg c) (ConstrModl c) (ConstrName c)
    ) => KnownConstr c

knownConstr ::
     forall c. Sing (c :: Constr Symbol) -> Constr String
knownConstr :: Sing c -> Constr String
knownConstr Sing c
SConstr = Constr :: forall a. a -> a -> a -> Constr a
Constr {
      constrPkg :: String
constrPkg  = Proxy (ConstrPkg c) -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy (ConstrPkg c)
forall k (t :: k). Proxy t
Proxy @(ConstrPkg  c))
    , constrModl :: String
constrModl = Proxy (ConstrModl c) -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy (ConstrModl c)
forall k (t :: k). Proxy t
Proxy @(ConstrModl c))
    , constrName :: String
constrName = Proxy (ConstrName c) -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy (ConstrName c)
forall k (t :: k). Proxy t
Proxy @(ConstrName c))
    }

prettyKnownConstr :: Sing (c :: Constr Symbol) -> String
prettyKnownConstr :: Sing c -> String
prettyKnownConstr Sing c
s = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"." [String
constrPkg, String
constrModl, String
constrName]
  where
    Constr{String
constrPkg :: String
constrPkg :: forall a. Constr a -> a
constrPkg, String
constrModl :: String
constrModl :: forall a. Constr a -> a
constrModl, String
constrName :: String
constrName :: forall a. Constr a -> a
constrName} = Sing c -> Constr String
forall (c :: Constr Symbol). Sing c -> Constr String
knownConstr Sing c
s

elimKnownConstr :: forall r.
     Constr String
  -> (forall c. Sing (c :: Constr Symbol) -> r)
  -> r
elimKnownConstr :: Constr String -> (forall (c :: Constr Symbol). Sing c -> r) -> r
elimKnownConstr Constr{String
constrPkg :: String
constrPkg :: forall a. Constr a -> a
constrPkg, String
constrModl :: String
constrModl :: forall a. Constr a -> a
constrModl, String
constrName :: String
constrName :: forall a. Constr a -> a
constrName} forall (c :: Constr Symbol). Sing c -> r
k =
    String
-> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r
forall r.
String
-> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r
elimKnownSymbol String
constrPkg  ((forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r)
-> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Proxy n
pPkg  ->
    String
-> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r
forall r.
String
-> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r
elimKnownSymbol String
constrModl ((forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r)
-> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Proxy n
pModl ->
    String
-> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r
forall r.
String
-> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r
elimKnownSymbol String
constrName ((forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r)
-> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Proxy n
pName ->
      Proxy n -> Proxy n -> Proxy n -> r
forall (pkg :: Symbol) (modl :: Symbol) (constr :: Symbol).
(KnownSymbol pkg, KnownSymbol modl, KnownSymbol constr) =>
Proxy pkg -> Proxy modl -> Proxy constr -> r
go Proxy n
pPkg Proxy n
pModl Proxy n
pName
  where
    go :: forall pkg modl constr. (
              KnownSymbol pkg
            , KnownSymbol modl
            , KnownSymbol constr
            )
       => Proxy pkg -> Proxy modl -> Proxy constr -> r
    go :: Proxy pkg -> Proxy modl -> Proxy constr -> r
go Proxy pkg
_ Proxy modl
_ Proxy constr
_ = Sing ('Constr pkg modl constr) -> r
forall (c :: Constr Symbol). Sing c -> r
k (Sing ('Constr pkg modl constr)
forall k (a :: k). SingI a => Sing a
sing :: Sing ('Constr pkg modl constr))

{-------------------------------------------------------------------------------
  Singleton
-------------------------------------------------------------------------------}

data instance Sing (c :: Constr Symbol) where
  SConstr :: KnownConstr c => Sing c

instance KnownConstr c => SingI (c :: Constr Symbol) where
  sing :: Sing c
sing = Sing c
forall (c :: Constr Symbol). KnownConstr c => Sing c
SConstr

instance Show (Sing (c :: Constr Symbol)) where
  showsPrec :: Int -> Sing c -> ShowS
showsPrec Int
p Sing c
proxy = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        String -> ShowS
showString String
"SConstr "
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Constr String -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 (Sing c -> Constr String
forall (c :: Constr Symbol). Sing c -> Constr String
knownConstr Sing c
proxy)

instance DecidableEquality (Constr Symbol) where
  decideEquality :: forall c c'.
       Sing (c  :: Constr Symbol)
    -> Sing (c' :: Constr Symbol)
    -> Maybe (c :~: c')
  decideEquality :: Sing c -> Sing c' -> Maybe (c :~: c')
decideEquality Sing c
SConstr Sing c'
SConstr =
    case ( Sing (ConstrPkg c)
-> Sing (ConstrPkg c') -> Maybe (ConstrPkg c :~: ConstrPkg c')
forall k (a :: k) (b :: k).
DecidableEquality k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality (Sing (ConstrPkg c)
forall k (a :: k). SingI a => Sing a
sing :: Sing (ConstrPkg  c)) (Sing (ConstrPkg c')
forall k (a :: k). SingI a => Sing a
sing :: Sing (ConstrPkg  c'))
         , Sing (ConstrModl c)
-> Sing (ConstrModl c') -> Maybe (ConstrModl c :~: ConstrModl c')
forall k (a :: k) (b :: k).
DecidableEquality k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality (Sing (ConstrModl c)
forall k (a :: k). SingI a => Sing a
sing :: Sing (ConstrModl c)) (Sing (ConstrModl c')
forall k (a :: k). SingI a => Sing a
sing :: Sing (ConstrModl c'))
         , Sing (ConstrName c)
-> Sing (ConstrName c') -> Maybe (ConstrName c :~: ConstrName c')
forall k (a :: k) (b :: k).
DecidableEquality k =>
Sing a -> Sing b -> Maybe (a :~: b)
decideEquality (Sing (ConstrName c)
forall k (a :: k). SingI a => Sing a
sing :: Sing (ConstrName c)) (Sing (ConstrName c')
forall k (a :: k). SingI a => Sing a
sing :: Sing (ConstrName c'))
         ) of
      (Just ConstrPkg c :~: ConstrPkg c'
Refl, Just ConstrModl c :~: ConstrModl c'
Refl, Just ConstrName c :~: ConstrName c'
Refl) ->
        (c :~: c) -> Maybe (c :~: c)
forall a. a -> Maybe a
Just c :~: c
forall k (a :: k). a :~: a
Refl
      (Maybe (ConstrPkg c :~: ConstrPkg c'),
 Maybe (ConstrModl c :~: ConstrModl c'),
 Maybe (ConstrName c :~: ConstrName c'))
_otherwise ->
        Maybe (c :~: c')
forall a. Maybe a
Nothing

{-------------------------------------------------------------------------------
  Reverse direction: from type to the known constructors
-------------------------------------------------------------------------------}

-- | Compute all constructors of the given type
type family Constrs (a :: Type) :: [Constr Symbol] where
  Constrs a = GConstrs (Rep a)

type family GConstrs f :: [Constr Symbol] where
  GConstrs (M1 D ('MetaData typ modl pkg isNewtype) f) =
    GConstrsOfType pkg modl f '[]

type family GConstrsOfType pkg modl f acc :: [Constr Symbol] where
  GConstrsOfType pkg modl (f :+: g) acc =
    GConstrsOfType pkg modl g (GConstrsOfType pkg modl f acc)
  GConstrsOfType pkg modl (M1 C ('MetaCons constr fixity isRecord) f) acc =
    'Constr pkg modl constr ': acc

-- | Require that specified type has the given constructor
--
-- Intended usage:
--
-- > castUserDefined :: forall c a. ConstrOf a c => UserDefined c -> a
-- > castUserDefined = unsafeCoerce
type family ConstrOf (a :: Type) (c :: Constr Symbol) :: Constraint where
  ConstrOf a c =
      Assert
        (Elem c (Constrs a))
        (TypeError (
                  (       'ShowType c
                    ':<>: 'Text " is not a valid constructor of "
                    ':<>: 'ShowType a
                  )
            ':$$: (       'Text "Valid constructors are: "
                    ':<>: 'ShowType (Constrs a)
                  )
          ))

data IsConstrOf (a :: Type) (c :: Constr Symbol) where
  IsConstrOf :: Elem c (Constrs a) ~ 'True => IsConstrOf a c

checkIsConstrOf :: forall (a :: Type) (c :: Constr Symbol).
      SingI (Constrs a)
   => Sing c -> Maybe (IsConstrOf a c)
checkIsConstrOf :: Sing c -> Maybe (IsConstrOf a c)
checkIsConstrOf Sing c
s =
    IsElem c (GConstrs (Rep a)) -> IsConstrOf a c
IsElem c (Constrs a) -> IsConstrOf a c
aux (IsElem c (GConstrs (Rep a)) -> IsConstrOf a c)
-> Maybe (IsElem c (GConstrs (Rep a))) -> Maybe (IsConstrOf a c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sing c
-> Sing (GConstrs (Rep a)) -> Maybe (IsElem c (GConstrs (Rep a)))
forall k (x :: k) (xs :: [k]).
DecidableEquality k =>
Sing x -> Sing xs -> Maybe (IsElem x xs)
checkIsElem Sing c
s (SingI (Constrs a) => Sing (Constrs a)
forall k (a :: k). SingI a => Sing a
sing @_ @(Constrs a))
  where
    aux :: IsElem c (Constrs a) -> IsConstrOf a c
    aux :: IsElem c (Constrs a) -> IsConstrOf a c
aux IsElem c (Constrs a)
IsElem = IsConstrOf a c
forall (c :: Constr Symbol) a.
(Elem c (Constrs a) ~ 'True) =>
IsConstrOf a c
IsConstrOf