{-# LANGUAGE ExplicitNamespaces, CPP #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Singletons.TH
-- Copyright   :  (C) 2013 Richard Eisenberg
-- License     :  BSD-style (see LICENSE)
-- Maintainer  :  Richard Eisenberg (eir@cis.upenn.edu)
-- Stability   :  experimental
-- Portability :  non-portable
--
-- This module contains everything you need to derive your own singletons via
-- Template Haskell.
--
-- TURN ON @-XScopedTypeVariables@ IN YOUR MODULE IF YOU WANT THIS TO WORK.
--
----------------------------------------------------------------------------

module Data.Singletons.TH (
  -- * Primary Template Haskell generation functions
  singletons, singletonsOnly, genSingletons,
  promote, promoteOnly,

  -- ** Functions to generate equality instances
  promoteEqInstances, promoteEqInstance,
  singEqInstances, singEqInstance,
  singEqInstancesOnly, singEqInstanceOnly,
  singDecideInstances, singDecideInstance,

  -- ** Utility function
  cases,

  -- * Basic singleton definitions
  Sing(SFalse, STrue), SingI(..), SingKind(..), KindOf, Demote,
  
  -- * Auxiliary definitions
  -- | These definitions might be mentioned in code generated by Template Haskell,
  -- so they must be in scope.
  
  (:==), If, sIf, (:&&), SEq(..), 
  Any, 
  SDecide(..), (:~:)(..), Void, Refuted, Decision(..),
  KProxy(..), SomeSing(..)
 ) where

import Data.Singletons.Singletons
import Data.Singletons.Promote
import Data.Singletons.Core
import Data.Singletons.Bool
import Data.Singletons.Eq
import Data.Singletons.Types
import Data.Singletons.Void

import GHC.Exts
import Language.Haskell.TH
import Language.Haskell.TH.Syntax ( Quasi(..) )
import Language.Haskell.TH.Desugar
import Data.Singletons.Util
import Control.Applicative

#if __GLASGOW_HASKELL__ >= 707
import Data.Type.Equality
import Data.Proxy
#endif

-- | The function 'cases' generates a case expression where each right-hand side
-- is identical. This may be useful if the type-checker requires knowledge of which
-- constructor is used to satisfy equality or type-class constraints, but where
-- each constructor is treated the same.
cases :: Quasi q
      => Name        -- ^ The head of the type of the scrutinee. (Like @''Maybe@ or @''Bool@.)
      -> q Exp       -- ^ The scrutinee, in a Template Haskell quote
      -> q Exp       -- ^ The body, in a Template Haskell quote
      -> q Exp
cases tyName expq bodyq = do
  info <- reifyWithWarning tyName
  case info of
    TyConI (DataD _ _ _ ctors _) -> buildCases ctors
    TyConI (NewtypeD _ _ _ ctor _) -> buildCases [ctor]
    _ -> fail $ "Using <<cases>> with something other than a type constructor: "
                ++ (show tyName)
  where buildCases ctors =
          CaseE <$> expq <*>
                    mapM (\con -> Match (conToPat con) <$>
                                        (NormalB <$> bodyq) <*> pure []) ctors

        conToPat :: Con -> Pat
        conToPat = ctor1Case
          (\name tys -> ConP name (map (const WildP) tys))