{-# 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 ( Nat, Symbol )
import GHC.Exts ( Constraint )
import GHC.Show ( showCommaSpace, showSpace )
import Data.String (fromString)
import Data.Type.Equality ( TestEquality(..) )
import Data.Type.Coercion ( TestCoercion(..) )
import Control.Applicative
boolName, andName, compareName, minBoundName,
maxBoundName, repName,
nilName, consName, listName, tyFunArrowName,
applyName, applyTyConName, applyTyConAux1Name,
natName, symbolName, stringName,
eqName, ordName, boundedName, orderingName,
singFamilyName, singIName, singMethName, demoteName, withSingIName,
singKindClassName, someSingTypeName, someSingDataName,
sDecideClassName, sDecideMethName,
testEqualityClassName, testEqualityMethName, decideEqualityName,
testCoercionClassName, testCoercionMethName, decideCoercionName,
provedName, disprovedName, reflName, toSingName, fromSingName,
equalityName, applySingName, suppressClassName, suppressMethodName,
thenCmpName, 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, 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
natName :: Name
natName = ''Nat
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
singMethName :: Name
singMethName = 'sing
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
thenCmpName :: Name
thenCmpName = 'thenCmp
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
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. [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
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 (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 (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