{- Data/Singletons/Names.hs

(c) Richard Eisenberg 2014
rae@cs.brynmawr.edu

Defining names and manipulations on names for use in promotion and singling.
-}

{-# LANGUAGE TemplateHaskell #-}

module Data.Singletons.Names where

import Data.Singletons.Internal
import Data.Singletons.SuppressUnusedWarnings
import Data.Singletons.Decide
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.Type.Equality ( TestEquality(..) )
import Data.Type.Coercion ( TestCoercion(..) )
import Data.Typeable ( TypeRep )
import Data.Singletons.Util
import Control.Applicative
import Control.Monad

boolName, andName, tyEqName, compareName, minBoundName,
  maxBoundName, repName,
  nilName, consName, listName, tyFunArrowName,
  applyName, applyTyConName, applyTyConAux1Name,
  natName, symbolName, typeRepName, stringName,
  eqName, ordName, boundedName, orderingName,
  singFamilyName, singIName, singMethName, demoteName, withSingIName,
  singKindClassName, sEqClassName, sEqMethName, sconsName, snilName, strueName,
  sIfName,
  someSingTypeName, someSingDataName,
  sListName, sDecideClassName, sDecideMethName,
  testEqualityClassName, testEqualityMethName, decideEqualityName,
  testCoercionClassName, testCoercionMethName, decideCoercionName,
  provedName, disprovedName, reflName, toSingName, fromSingName,
  equalityName, applySingName, suppressClassName, suppressMethodName,
  thenCmpName,
  sameKindName, tyFromIntegerName, tyNegateName, sFromIntegerName,
  sNegateName, errorName, foldlName, cmpEQName, cmpLTName, cmpGTName,
  singletonsToEnumName, singletonsFromEnumName, enumName, singletonsEnumName,
  equalsName, constraintName,
  showName, showSName, showCharName, showCommaSpaceName, showParenName, showsPrecName,
  showSpaceName, showStringName, showSingName, showSing'Name,
  composeName, gtName, tyFromStringName, sFromStringName,
  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
tyEqName :: Name
tyEqName = String -> String -> Name
mk_name_tc String
"Data.Singletons.Prelude.Eq" String
"=="
repName :: Name
repName = String -> Name
mkName String
"Rep"   -- this is actually defined in client code!
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
typeRepName :: Name
typeRepName = ''TypeRep
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
sEqClassName :: Name
sEqClassName = String -> String -> Name
mk_name_tc String
"Data.Singletons.Prelude.Eq" String
"SEq"
sEqMethName :: Name
sEqMethName = String -> String -> Name
mk_name_v String
"Data.Singletons.Prelude.Eq" String
"%=="
sIfName :: Name
sIfName = String -> String -> Name
mk_name_v String
"Data.Singletons.Prelude.Bool" String
"sIf"
sconsName :: Name
sconsName = String -> String -> Name
mk_name_d String
"Data.Singletons.Prelude.Instances" String
"SCons"
snilName :: Name
snilName = String -> String -> Name
mk_name_d String
"Data.Singletons.Prelude.Instances" String
"SNil"
strueName :: Name
strueName = String -> String -> Name
mk_name_d String
"Data.Singletons.Prelude.Instances" String
"STrue"
someSingTypeName :: Name
someSingTypeName = ''SomeSing
someSingDataName :: Name
someSingDataName = 'SomeSing
sListName :: Name
sListName = String -> String -> Name
mk_name_tc String
"Data.Singletons.Prelude.Instances" String
"SList"
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 = String -> String -> Name
mk_name_v String
"Data.Singletons.Prelude.Ord" String
"thenCmp"
sameKindName :: Name
sameKindName = ''SameKind
tyFromIntegerName :: Name
tyFromIntegerName = String -> String -> Name
mk_name_tc String
"Data.Singletons.Prelude.Num" String
"FromInteger"
tyNegateName :: Name
tyNegateName = String -> String -> Name
mk_name_tc String
"Data.Singletons.Prelude.Num" String
"Negate"
sFromIntegerName :: Name
sFromIntegerName = String -> String -> Name
mk_name_v String
"Data.Singletons.Prelude.Num" String
"sFromInteger"
sNegateName :: Name
sNegateName = String -> String -> Name
mk_name_v String
"Data.Singletons.Prelude.Num" String
"sNegate"
errorName :: Name
errorName = 'error
foldlName :: Name
foldlName = 'foldl
cmpEQName :: Name
cmpEQName = 'EQ
cmpLTName :: Name
cmpLTName = 'LT
cmpGTName :: Name
cmpGTName = 'GT
singletonsToEnumName :: Name
singletonsToEnumName = String -> String -> Name
mk_name_v String
"Data.Singletons.Prelude.Enum" String
"toEnum"
singletonsFromEnumName :: Name
singletonsFromEnumName = String -> String -> Name
mk_name_v String
"Data.Singletons.Prelude.Enum" String
"fromEnum"
enumName :: Name
enumName = ''Enum
singletonsEnumName :: Name
singletonsEnumName = String -> String -> Name
mk_name_tc String
"Data.Singletons.Prelude.Enum" String
"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 = String -> String -> Name
mk_name_tc String
"Data.Singletons.ShowSing" String
"ShowSing"
showSing'Name :: Name
showSing'Name = String -> String -> Name
mk_name_tc String
"Data.Singletons.ShowSing" String
"ShowSing'"
composeName :: Name
composeName = '(.)
gtName :: Name
gtName = '(>)
showCommaSpaceName :: Name
showCommaSpaceName = 'showCommaSpace
tyFromStringName :: Name
tyFromStringName = String -> String -> Name
mk_name_tc String
"Data.Singletons.Prelude.IsString" String
"FromString"
sFromStringName :: Name
sFromStringName = String -> String -> Name
mk_name_v String
"Data.Singletons.Prelude.IsString" String
"sFromString"
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

singPkg :: String
singPkg :: String
singPkg = $( (LitE . StringL . loc_package) `liftM` location )

mk_name_tc :: String -> String -> Name
mk_name_tc :: String -> String -> Name
mk_name_tc = String -> String -> String -> Name
mkNameG_tc String
singPkg

mk_name_d :: String -> String -> Name
mk_name_d :: String -> String -> Name
mk_name_d = String -> String -> String -> Name
mkNameG_d String
singPkg

mk_name_v :: String -> String -> Name
mk_name_v :: String -> String -> Name
mk_name_v = String -> String -> String -> Name
mkNameG_v String
singPkg

mkTupleTypeName :: Int -> Name
mkTupleTypeName :: Int -> Name
mkTupleTypeName Int
n = String -> String -> Name
mk_name_tc String
"Data.Singletons.Prelude.Instances" (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$
                    String
"STuple" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int -> String
forall a. Show a => a -> String
show Int
n)

mkTupleDataName :: Int -> Name
mkTupleDataName :: Int -> Name
mkTupleDataName Int
n = String -> String -> Name
mk_name_d String
"Data.Singletons.Prelude.Instances" (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$
                    String
"STuple" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int -> String
forall a. Show a => a -> String
show Int
n)

mkTyName :: Quasi q => Name -> q Name
mkTyName :: 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 -> String -> Name
mk_name_tc String
"Data.Singletons.Internal" (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)

-- apply a type to a list of types using Apply type family
-- This is defined here, not in Utils, to avoid cyclic dependencies
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

-- make an equality predicate
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]

-- | If a 'String' begins with one or more underscores, return
-- @'Just' (us, rest)@, where @us@ contain all of the underscores at the
-- beginning of the 'String' and @rest@ contains the remainder of the 'String'.
-- Otherwise, return 'Nothing'.
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

-- Walk a DType, applying a function to all occurrences of constructor names.
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 ForallVisFlag
fvf [DTyVarBndr]
tvbs DKind
p) = ForallVisFlag -> [DTyVarBndr] -> DKind -> DKind
DForallT ForallVisFlag
fvf [DTyVarBndr]
tvbs (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

{-
Note [Defunctionalization symbol suffixes]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Before, we used to denote defunctionalization symbols by simply appending dollar
signs at the end (e.g., (+$) and (+$$)). But this can lead to ambiguity when you
have function names that consist of solely $ characters. For instance, if you
tried to promote ($) and ($$) simultaneously, you'd get these promoted types:

$
$$

And these defunctionalization symbols:

$$
$$$

But now there's a name clash between the promoted type for ($) and the
defunctionalization symbol for ($$)! The solution is to use a precede these
defunctionalization dollar signs with another string (we choose @#@).
So now the new defunctionalization symbols would be:

$@#@$
$@#@$$

And there is no conflict.
-}