{-# LANGUAGE TemplateHaskellQuotes #-}
module Data.Singletons.TH.Names where
import Data.Singletons
import Data.Singletons.Decide
import Data.Singletons.ShowSing
import Data.Singletons.TH.SuppressUnusedWarnings
import Data.Singletons.TH.Util
import Language.Haskell.TH.Syntax
import Language.Haskell.TH.Desugar
import GHC.TypeLits ( Symbol )
import GHC.Exts ( Constraint )
import GHC.Show ( showCommaSpace, showSpace )
import Data.String (fromString)
import Data.Type.Equality ( TestEquality(..) )
import Data.Type.Coercion ( TestCoercion(..) )
boolName, andName, compareName, minBoundName,
maxBoundName, repName,
nilName, consName, listName, tyFunArrowName,
applyName, applyTyConName, applyTyConAux1Name,
symbolName, stringName,
eqName, ordName, boundedName, orderingName,
singFamilyName, singIName, singI1Name, singI2Name,
singMethName, liftSingName, liftSing2Name, demoteName, withSingIName,
singKindClassName, someSingTypeName, someSingDataName,
sDecideClassName, sDecideMethName,
testEqualityClassName, testEqualityMethName, decideEqualityName,
testCoercionClassName, testCoercionMethName, decideCoercionName,
provedName, disprovedName, reflName, toSingName, fromSingName,
equalityName, applySingName, suppressClassName, suppressMethodName,
sameKindName, fromIntegerName, negateName,
errorName, foldlName, cmpEQName, cmpLTName, cmpGTName,
toEnumName, fromEnumName, enumName,
equalsName, constraintName,
showName, showSName, showCharName, showCommaSpaceName, showParenName, showsPrecName,
showSpaceName, showStringName, showSingName,
composeName, gtName, fromStringName,
foldableName, foldMapName, memptyName, mappendName, sappendName, foldrName,
functorName, fmapName, replaceName,
traversableName, traverseName, pureName, apName, liftA2Name :: Name
boolName :: Name
boolName = ''Bool
andName :: Name
andName = '(&&)
compareName :: Name
compareName = 'compare
minBoundName :: Name
minBoundName = 'minBound
maxBoundName :: Name
maxBoundName = 'maxBound
repName :: Name
repName = String -> Name
mkName String
"Rep"
nilName :: Name
nilName = '[]
consName :: Name
consName = '(:)
listName :: Name
listName = ''[]
tyFunArrowName :: Name
tyFunArrowName = ''(~>)
applyName :: Name
applyName = ''Apply
applyTyConName :: Name
applyTyConName = ''ApplyTyCon
applyTyConAux1Name :: Name
applyTyConAux1Name = ''ApplyTyConAux1
symbolName :: Name
symbolName = ''Symbol
stringName :: Name
stringName = ''String
eqName :: Name
eqName = ''Eq
ordName :: Name
ordName = ''Ord
boundedName :: Name
boundedName = ''Bounded
orderingName :: Name
orderingName = ''Ordering
singFamilyName :: Name
singFamilyName = ''Sing
singIName :: Name
singIName = ''SingI
singI1Name :: Name
singI1Name = ''SingI1
singI2Name :: Name
singI2Name = ''SingI2
singMethName :: Name
singMethName = 'sing
liftSingName :: Name
liftSingName = 'liftSing
liftSing2Name :: Name
liftSing2Name = 'liftSing2
toSingName :: Name
toSingName = 'toSing
fromSingName :: Name
fromSingName = 'fromSing
demoteName :: Name
demoteName = ''Demote
withSingIName :: Name
withSingIName = 'withSingI
singKindClassName :: Name
singKindClassName = ''SingKind
someSingTypeName :: Name
someSingTypeName = ''SomeSing
someSingDataName :: Name
someSingDataName = 'SomeSing
sDecideClassName :: Name
sDecideClassName = ''SDecide
sDecideMethName :: Name
sDecideMethName = '(%~)
testEqualityClassName :: Name
testEqualityClassName = ''TestEquality
testEqualityMethName :: Name
testEqualityMethName = 'testEquality
decideEqualityName :: Name
decideEqualityName = 'decideEquality
testCoercionClassName :: Name
testCoercionClassName = ''TestCoercion
testCoercionMethName :: Name
testCoercionMethName = 'testCoercion
decideCoercionName :: Name
decideCoercionName = 'decideCoercion
provedName :: Name
provedName = 'Proved
disprovedName :: Name
disprovedName = 'Disproved
reflName :: Name
reflName = 'Refl
equalityName :: Name
equalityName = ''(~)
applySingName :: Name
applySingName = 'applySing
suppressClassName :: Name
suppressClassName = ''SuppressUnusedWarnings
suppressMethodName :: Name
suppressMethodName = 'suppressUnusedWarnings
sameKindName :: Name
sameKindName = ''SameKind
fromIntegerName :: Name
fromIntegerName = 'fromInteger
negateName :: Name
negateName = 'negate
errorName :: Name
errorName = 'error
foldlName :: Name
foldlName = 'foldl
cmpEQName :: Name
cmpEQName = 'EQ
cmpLTName :: Name
cmpLTName = 'LT
cmpGTName :: Name
cmpGTName = 'GT
toEnumName :: Name
toEnumName = 'toEnum
= 'fromEnum
enumName :: Name
enumName = ''Enum
equalsName :: Name
equalsName = '(==)
constraintName :: Name
constraintName = ''Constraint
showName :: Name
showName = ''Show
showSName :: Name
showSName = ''ShowS
showCharName :: Name
showCharName = 'showChar
showParenName :: Name
showParenName = 'showParen
showSpaceName :: Name
showSpaceName = 'showSpace
showsPrecName :: Name
showsPrecName = 'showsPrec
showStringName :: Name
showStringName = 'showString
showSingName :: Name
showSingName = ''ShowSing
composeName :: Name
composeName = '(.)
gtName :: Name
gtName = '(>)
showCommaSpaceName :: Name
showCommaSpaceName = 'showCommaSpace
fromStringName :: Name
fromStringName = 'fromString
foldableName :: Name
foldableName = ''Foldable
foldMapName :: Name
foldMapName = 'foldMap
memptyName :: Name
memptyName = 'mempty
mappendName :: Name
mappendName = 'mappend
sappendName :: Name
sappendName = '(<>)
foldrName :: Name
foldrName = 'foldr
functorName :: Name
functorName = ''Functor
fmapName :: Name
fmapName = 'fmap
replaceName :: Name
replaceName = '(<$)
traversableName :: Name
traversableName = ''Traversable
traverseName :: Name
traverseName = 'traverse
pureName :: Name
pureName = 'pure
apName :: Name
apName = '(<*>)
liftA2Name :: Name
liftA2Name = 'liftA2
mkTyName :: Quasi q => Name -> q Name
mkTyName :: forall (q :: * -> *). Quasi q => Name -> q Name
mkTyName Name
tmName = do
let nameStr :: String
nameStr = Name -> String
nameBase Name
tmName
symbolic :: Bool
symbolic = Bool -> Bool
not (Char -> Bool
isHsLetter (String -> Char
forall a. HasCallStack => [a] -> a
head String
nameStr))
String -> q Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName (if Bool
symbolic then String
"ty" else String
nameStr)
mkTyConName :: Int -> Name
mkTyConName :: Int -> Name
mkTyConName Int
i = String -> Name
mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
"TyCon" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
mkSingIName :: Int -> Name
mkSingIName :: Int -> Name
mkSingIName Int
0 = Name
singIName
mkSingIName Int
1 = Name
singI1Name
mkSingIName Int
2 = Name
singI2Name
mkSingIName Int
n = String -> Name
forall a. HasCallStack => String -> a
error (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
"SingI" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" does not exist"
mkSingMethName :: Int -> Name
mkSingMethName :: Int -> Name
mkSingMethName Int
0 = Name
singMethName
mkSingMethName Int
1 = Name
liftSingName
mkSingMethName Int
2 = Name
liftSing2Name
mkSingMethName Int
n = String -> Name
forall a. HasCallStack => String -> a
error (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
"SingI" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" does not exist"
boolKi :: DKind
boolKi :: DKind
boolKi = Name -> DKind
DConT Name
boolName
singFamily :: DType
singFamily :: DKind
singFamily = Name -> DKind
DConT Name
singFamilyName
singKindConstraint :: DKind -> DPred
singKindConstraint :: DKind -> DKind
singKindConstraint = DKind -> DKind -> DKind
DAppT (Name -> DKind
DConT Name
singKindClassName)
demote :: DType
demote :: DKind
demote = Name -> DKind
DConT Name
demoteName
apply :: DType -> DType -> DType
apply :: DKind -> DKind -> DKind
apply DKind
t1 DKind
t2 = DKind -> DKind -> DKind
DAppT (DKind -> DKind -> DKind
DAppT (Name -> DKind
DConT Name
applyName) DKind
t1) DKind
t2
mkListE :: [DExp] -> DExp
mkListE :: [DExp] -> DExp
mkListE =
(DExp -> DExp -> DExp) -> DExp -> [DExp] -> DExp
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\DExp
h DExp
t -> Name -> DExp
DConE Name
consName DExp -> DExp -> DExp
`DAppE` DExp
h DExp -> DExp -> DExp
`DAppE` DExp
t) (Name -> DExp
DConE Name
nilName)
foldApply :: DType -> [DType] -> DType
foldApply :: DKind -> [DKind] -> DKind
foldApply = (DKind -> DKind -> DKind) -> DKind -> [DKind] -> DKind
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl DKind -> DKind -> DKind
apply
mkEqPred :: DType -> DType -> DPred
mkEqPred :: DKind -> DKind -> DKind
mkEqPred DKind
ty1 DKind
ty2 = DKind -> [DKind] -> DKind
foldType (Name -> DKind
DConT Name
equalityName) [DKind
ty1, DKind
ty2]
splitUnderscores :: String -> Maybe (String, String)
splitUnderscores :: String -> Maybe (String, String)
splitUnderscores String
s = case (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_') String
s of
([], String
_) -> Maybe (String, String)
forall a. Maybe a
Nothing
(String, String)
res -> (String, String) -> Maybe (String, String)
forall a. a -> Maybe a
Just (String, String)
res
modifyConNameDType :: (Name -> Name) -> DType -> DType
modifyConNameDType :: (Name -> Name) -> DKind -> DKind
modifyConNameDType Name -> Name
mod_con_name = DKind -> DKind
go
where
go :: DType -> DType
go :: DKind -> DKind
go (DForallT DForallTelescope
tele DKind
p) = DForallTelescope -> DKind -> DKind
DForallT DForallTelescope
tele (DKind -> DKind
go DKind
p)
go (DConstrainedT [DKind]
cxt DKind
p) = [DKind] -> DKind -> DKind
DConstrainedT ((DKind -> DKind) -> [DKind] -> [DKind]
forall a b. (a -> b) -> [a] -> [b]
map DKind -> DKind
go [DKind]
cxt) (DKind -> DKind
go DKind
p)
go (DAppT DKind
p DKind
t) = DKind -> DKind -> DKind
DAppT (DKind -> DKind
go DKind
p) DKind
t
go (DAppKindT DKind
p DKind
k) = DKind -> DKind -> DKind
DAppKindT (DKind -> DKind
go DKind
p) DKind
k
go (DSigT DKind
p DKind
k) = DKind -> DKind -> DKind
DSigT (DKind -> DKind
go DKind
p) DKind
k
go p :: DKind
p@(DVarT Name
_) = DKind
p
go (DConT Name
n) = Name -> DKind
DConT (Name -> Name
mod_con_name Name
n)
go p :: DKind
p@DKind
DWildCardT = DKind
p
go p :: DKind
p@(DLitT {}) = DKind
p
go p :: DKind
p@DKind
DArrowT = DKind
p