{-# 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 #-}
module Debug.RecoverRTTI.Constr (
Constr(..)
, KnownConstr
, knownConstr
, prettyKnownConstr
, elimKnownConstr
, 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
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))
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
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
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