{- Data/Singletons/TH/Names.hs

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

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

{-# 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

{-
Note [Wired-in Names]
~~~~~~~~~~~~~~~~~~~~~
The list of Names below contains everything that the Template Haskell machinery
needs to have special knowledge of. These names can be broadly categorized into
two groups:

1. Names of basic singleton definitions (Sing, SingKind, etc.). These are
   spliced directly into TH-generated code.
2. Names of definitions from the Prelude. These are not spliced into
   TH-generated code, but are instead used as the namesakes for promoted and
   singled definitions. For example, the TH machinery must be aware of the Name
   `fromInteger` so that it can promote and single the expression `42` to
   `FromInteger 42` and `sFromInteger (sing @42)`, respectively.

Note that we deliberately do not wire in promoted or singled Names, such as
FromInteger or sFromInteger, for two reasons:

a. We want all promoted and singled names to go through the naming options in
   D.S.TH.Options. Splicing the name FromInteger directly into TH-generated
   code, for instance, would prevent users from overriding the default options
   in order to promote `fromInteger` to something else (e.g.,
   MyCustomFromInteger).
b. Wired in names live in particular modules, so if we were to wire in the name
   FromInteger, it would come from GHC.Num.Singletons. This would effectively
   prevent anyone from defining their own version of FromInteger and
   piggybacking on top of the TH machinery to generate it, however. As a
   result, we generate the name FromInteger completely unqualified so that
   it picks up whichever version of FromInteger is in scope.
-}

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"   -- 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
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
fromEnumName :: Name
fromEnumName = '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)

-- 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 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

{-
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.
-}