{-# LANGUAGE ScopedTypeVariables #-}
module Data.Singletons.Single.Fixity where

import Prelude hiding ( exp )
import Language.Haskell.TH hiding ( cxt )
import Language.Haskell.TH.Syntax (NameSpace(..), Quasi(..))
import Data.Singletons.TH.Options
import Data.Singletons.Util
import Language.Haskell.TH.Desugar

-- Single a fixity declaration.
singInfixDecl :: forall q. OptionsMonad q => Name -> Fixity -> q (Maybe DLetDec)
singInfixDecl :: Name -> Fixity -> q (Maybe DLetDec)
singInfixDecl Name
name Fixity
fixity = do
  Options
opts  <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  Maybe NameSpace
mb_ns <- Name -> q (Maybe NameSpace)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe NameSpace)
reifyNameSpace Name
name
  case Maybe NameSpace
mb_ns of
    -- If we can't find the Name for some odd reason,
    -- fall back to singValName
    Maybe NameSpace
Nothing        -> Name -> q (Maybe DLetDec)
finish (Name -> q (Maybe DLetDec)) -> Name -> q (Maybe DLetDec)
forall a b. (a -> b) -> a -> b
$ Options -> Name -> Name
singledValueName   Options
opts Name
name
    Just NameSpace
VarName   -> Name -> q (Maybe DLetDec)
finish (Name -> q (Maybe DLetDec)) -> Name -> q (Maybe DLetDec)
forall a b. (a -> b) -> a -> b
$ Options -> Name -> Name
singledValueName   Options
opts Name
name
    Just NameSpace
DataName  -> Name -> q (Maybe DLetDec)
finish (Name -> q (Maybe DLetDec)) -> Name -> q (Maybe DLetDec)
forall a b. (a -> b) -> a -> b
$ Options -> Name -> Name
singledDataConName Options
opts Name
name
    Just NameSpace
TcClsName -> do
      Maybe DInfo
mb_info <- Name -> q (Maybe DInfo)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReify Name
name
      case Maybe DInfo
mb_info of
        Just (DTyConI DClassD{} Maybe [DDec]
_)
          -> Name -> q (Maybe DLetDec)
finish (Name -> q (Maybe DLetDec)) -> Name -> q (Maybe DLetDec)
forall a b. (a -> b) -> a -> b
$ Options -> Name -> Name
singledClassName Options
opts Name
name
        Maybe DInfo
_ -> Maybe DLetDec -> q (Maybe DLetDec)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe DLetDec
forall a. Maybe a
Nothing
          -- Don't produce anything for other type constructors (type synonyms,
          -- type families, data types, etc.).
          -- See [singletons and fixity declarations], wrinkle 1.
  where
    finish :: Name -> q (Maybe DLetDec)
    finish :: Name -> q (Maybe DLetDec)
finish = Maybe DLetDec -> q (Maybe DLetDec)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe DLetDec -> q (Maybe DLetDec))
-> (Name -> Maybe DLetDec) -> Name -> q (Maybe DLetDec)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DLetDec -> Maybe DLetDec
forall a. a -> Maybe a
Just (DLetDec -> Maybe DLetDec)
-> (Name -> DLetDec) -> Name -> Maybe DLetDec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fixity -> Name -> DLetDec
DInfixD Fixity
fixity

-- Try producing singled fixity declarations for Names by reifying them
-- /without/ consulting quoted declarations. If reification fails, recover and
-- return the empty list.
-- See [singletons and fixity declarations], wrinkle 2.
singReifiedInfixDecls :: forall q. OptionsMonad q => [Name] -> q [DDec]
singReifiedInfixDecls :: [Name] -> q [DDec]
singReifiedInfixDecls = (Name -> q (Maybe DDec)) -> [Name] -> q [DDec]
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM Name -> q (Maybe DDec)
trySingFixityDeclaration
  where
    trySingFixityDeclaration :: Name -> q (Maybe DDec)
    trySingFixityDeclaration :: Name -> q (Maybe DDec)
trySingFixityDeclaration Name
name =
      q (Maybe DDec) -> q (Maybe DDec) -> q (Maybe DDec)
forall (m :: * -> *) a. Quasi m => m a -> m a -> m a
qRecover (Maybe DDec -> q (Maybe DDec)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe DDec
forall a. Maybe a
Nothing) (q (Maybe DDec) -> q (Maybe DDec))
-> q (Maybe DDec) -> q (Maybe DDec)
forall a b. (a -> b) -> a -> b
$ do
        Maybe Fixity
mFixity <- Name -> q (Maybe Fixity)
forall (m :: * -> *). Quasi m => Name -> m (Maybe Fixity)
qReifyFixity Name
name
        case Maybe Fixity
mFixity of
          Maybe Fixity
Nothing     -> Maybe DDec -> q (Maybe DDec)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe DDec
forall a. Maybe a
Nothing
          Just Fixity
fixity -> (Maybe DLetDec -> Maybe DDec)
-> q (Maybe DLetDec) -> q (Maybe DDec)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((DLetDec -> DDec) -> Maybe DLetDec -> Maybe DDec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DLetDec -> DDec
DLetDec) (q (Maybe DLetDec) -> q (Maybe DDec))
-> q (Maybe DLetDec) -> q (Maybe DDec)
forall a b. (a -> b) -> a -> b
$ Name -> Fixity -> q (Maybe DLetDec)
forall (q :: * -> *).
OptionsMonad q =>
Name -> Fixity -> q (Maybe DLetDec)
singInfixDecl Name
name Fixity
fixity

{-
Note [singletons and fixity declarations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Promoting and singling fixity declarations is surprisingly tricky to get right.
This Note serves as a place to document the insights learned after getting this
wrong at various points.

As a general rule, when promoting something with a fixity declaration like this
one:

  infixl 5 `foo`

singletons will produce promoted and singled versions of them:

  infixl 5 `Foo`
  infixl 5 `sFoo`

singletons will also produce fixity declarations for its defunctionalization
symbols (see Note [Fixity declarations for defunctionalization symbols] in
D.S.Promote.Defun):

  infixl 5 `FooSym0`
  infixl 5 `FooSym1`
  ...

-----
-- Wrinkle 1: When not to promote/single fixity declarations
-----

Rules are meant to be broken, and the general rule above is no exception. There
are certain cases where singletons does *not* produce promoted or singled
versions of fixity declarations:

* During promotion, fixity declarations for the following sorts of names will
  not receive promoted counterparts:

  - Data types
  - Type synonyms
  - Type families
  - Data constructors
  - Infix values

  We exclude the first four because the promoted versions of these names are
  the same as the originals, so generating an extra fixity declaration for them
  would run the risk of having duplicates, which GHC would reject with an error.

  We exclude infix value because while their promoted versions are different,
  they share the same name base. In concrete terms, this:

    $(promote [d|
      infixl 4 ###
      (###) :: a -> a -> a
      |])

  Is promoted to the following:

    type family (###) (x :: a) (y :: a) :: a where ...

  So giving the type-level (###) a fixity declaration would clash with the
  existing one for the value-level (###).

  There *is* a scenario where we should generate a fixity declaration for the
  type-level (###), however. Imagine the above example used the `promoteOnly`
  function instead of `promote`. Then the type-level (###) would lack a fixity
  declaration altogether because the original fixity declaration was discarded
  by `promoteOnly`! The same problem would arise if one had to choose between
  the `singletons` and `singletonsOnly` functions.

  The difference between `promote` and `promoteOnly` (as well as `singletons`
  and `singletonsOnly`) is whether the `genQuotedDecs` option is set to `True`
  or `False`, respectively. Therefore, if `genQuotedDecs` is set to `False`
  when promoting the fixity declaration for an infix value, we opt to generate
  a fixity declaration (with the same name base) so that the type-level version
  of that value gets one.

* During singling, the following things will not have their fixity declarations
  singled:

  - Type synonyms or type families. This is because singletons does not
    generate singled versions of them in the first place (they only receive
    defunctionalization symbols).

  - Data types. This is because the singled version of a data type T is
    always of the form:

      data ST :: forall a_1 ... a_n. T a_1 ... a_n -> Type where ...

    Regardless of how many arguments T has, ST will have exactly one argument.
    This makes is rather pointless to generate a fixity declaration for it.

-----
-- Wrinkle 2: Making sure fixity declarations are promoted/singled properly
-----

There are two situations where singletons must promote/single fixity
declarations:

1. When quoting code, i.e., with `promote` or `singletons`.
2. When reifying code, i.e., with `genPromotions` or `genSingletons`.

In the case of (1), singletons stores the quoted fixity declarations in the
lde_infix field of LetDecEnv. Therefore, it suffices to call
promoteInfixDecl/singleInfixDecl when processing LetDecEnvs.

In the case of (2), there is no LetDecEnv to use, so we must instead reify
the fixity declarations and promote/single those. See D.S.Single.Data.singDataD
(which singles data constructors) for a place that does this—we will use
singDataD as a running example for the rest of this section.

One complication is that code paths like singDataD are invoked in both (1) and
(2). This runs the risk that singletons will generate duplicate infix
declarations for data constructors in situation (1), as it will try to single
their fixity declarations once when processing them in LetDecEnvs and again
when reifying them in singDataD.

To avoid this pitfall, when reifying declarations in singDataD we take care
*not* to consult any quoted declarations when reifying (i.e., we do not use
reifyWithLocals for functions like it). Therefore, it we are in situation (1),
then the reification in singDataD will fail (and recover gracefully), so it
will not produce any singled fixity declarations. Therefore, the only singled
fixity declarations will be produced by processing LetDecEnvs.
-}