{- Data/Singletons/TH/Single/Decide.hs

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

Defines functions to generate SDecide instances, as well as TestEquality and
TestCoercion instances that leverage SDecide.
-}

module Data.Singletons.TH.Single.Decide where

import Language.Haskell.TH.Syntax
import Language.Haskell.TH.Desugar
import Data.Singletons.TH.Deriving.Infer
import Data.Singletons.TH.Names
import Data.Singletons.TH.Options
import Data.Singletons.TH.Promote.Type
import Data.Singletons.TH.Util
import Control.Monad

-- Make an instance of SDecide.
mkDecideInstance :: OptionsMonad q => Maybe DCxt -> DType
                 -> [DCon] -- ^ The /original/ constructors (for inferring the instance context)
                 -> [DCon] -- ^ The /singletons/ constructors
                 -> q DDec
mkDecideInstance :: forall (q :: * -> *).
OptionsMonad q =>
Maybe DCxt -> DType -> [DCon] -> [DCon] -> q DDec
mkDecideInstance Maybe DCxt
mb_ctxt DType
data_ty [DCon]
ctors [DCon]
sctors = do
  let sctorPairs :: [(DCon, DCon)]
sctorPairs = [ (DCon
sc1, DCon
sc2) | DCon
sc1 <- [DCon]
sctors, DCon
sc2 <- [DCon]
sctors ]
  methClauses <- if [DCon] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DCon]
sctors
                 then (DClause -> [DClause] -> [DClause]
forall a. a -> [a] -> [a]
:[]) (DClause -> [DClause]) -> q DClause -> q [DClause]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> q DClause
forall (q :: * -> *). Quasi q => q DClause
mkEmptyDecideMethClause
                 else ((DCon, DCon) -> q DClause) -> [(DCon, DCon)] -> q [DClause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (DCon, DCon) -> q DClause
forall (q :: * -> *). Quasi q => (DCon, DCon) -> q DClause
mkDecideMethClause [(DCon, DCon)]
sctorPairs
  constraints <- inferConstraintsDef mb_ctxt (DConT sDecideClassName) data_ty ctors
  data_ki <- promoteType data_ty
  return $ DInstanceD Nothing Nothing
                     constraints
                     (DAppT (DConT sDecideClassName) data_ki)
                     [DLetDec $ DFunD sDecideMethName methClauses]

-- Make a boilerplate Eq instance for a singleton type, e.g.,
--
-- @
-- instance Eq (SExample (z :: Example a)) where
--   _ == _ = True
-- @
mkEqInstanceForSingleton :: OptionsMonad q
                         => DType
                         -> Name
                         -- ^ The name of the data type
                         -> q DDec
mkEqInstanceForSingleton :: forall (q :: * -> *). OptionsMonad q => DType -> Name -> q DDec
mkEqInstanceForSingleton DType
data_ty Name
data_name = do
  opts <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  z <- qNewName "z"
  data_ki <- promoteType data_ty
  let sdata_name = Options -> Name -> Name
singledDataTypeName Options
opts Name
data_name
  pure $ DInstanceD Nothing Nothing []
           (DAppT (DConT eqName) (DConT sdata_name `DAppT` DSigT (DVarT z) data_ki))
           [DLetDec $
            DFunD equalsName
                  [DClause [DWildP, DWildP] (DConE trueName)]]

data TestInstance = TestEquality
                  | TestCoercion

-- Make an instance of TestEquality or TestCoercion by leveraging SDecide.
mkTestInstance :: OptionsMonad q => Maybe DCxt -> DType
               -> Name   -- ^ The name of the data type
               -> [DCon] -- ^ The /original/ constructors (for inferring the instance context)
               -> TestInstance -> q DDec
mkTestInstance :: forall (q :: * -> *).
OptionsMonad q =>
Maybe DCxt -> DType -> Name -> [DCon] -> TestInstance -> q DDec
mkTestInstance Maybe DCxt
mb_ctxt DType
data_ty Name
data_name [DCon]
ctors TestInstance
ti = do
  opts <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  constraints <- inferConstraintsDef mb_ctxt (DConT sDecideClassName) data_ty ctors
  data_ki <- promoteType data_ty
  pure $ DInstanceD Nothing Nothing
                    constraints
                    (DAppT (DConT tiClassName)
                           (DConT (singledDataTypeName opts data_name)
                             `DSigT` (DArrowT `DAppT` data_ki `DAppT` DConT typeKindName)))
                    [DLetDec $ DFunD tiMethName
                                     [DClause [] (DVarE tiDefaultName)]]
  where
    (Name
tiClassName, Name
tiMethName, Name
tiDefaultName) =
      case TestInstance
ti of
        TestInstance
TestEquality -> (Name
testEqualityClassName, Name
testEqualityMethName, Name
decideEqualityName)
        TestInstance
TestCoercion -> (Name
testCoercionClassName, Name
testCoercionMethName, Name
decideCoercionName)

mkDecideMethClause :: Quasi q => (DCon, DCon) -> q DClause
mkDecideMethClause :: forall (q :: * -> *). Quasi q => (DCon, DCon) -> q DClause
mkDecideMethClause (DCon
c1, DCon
c2)
  | Name
lname Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
rname =
    if Int
lNumArgs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
    then DClause -> q DClause
forall a. a -> q a
forall (m :: * -> *) a. Monad m => a -> m a
return (DClause -> q DClause) -> DClause -> q DClause
forall a b. (a -> b) -> a -> b
$ [DPat] -> DExp -> DClause
DClause [Name -> DCxt -> [DPat] -> DPat
DConP Name
lname [] [], Name -> DCxt -> [DPat] -> DPat
DConP Name
rname [] []]
                          (DExp -> DExp -> DExp
DAppE (Name -> DExp
DConE Name
provedName) (Name -> DExp
DConE Name
reflName))
    else do
      lnames <- Int -> q Name -> q [Name]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
lNumArgs (String -> q Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"a")
      rnames <- replicateM lNumArgs (qNewName "b")
      contra <- qNewName "contra"
      let lpats = (Name -> DPat) -> [Name] -> [DPat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DPat
DVarP [Name]
lnames
          rpats = (Name -> DPat) -> [Name] -> [DPat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DPat
DVarP [Name]
rnames
          lvars = (Name -> DExp) -> [Name] -> [DExp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DExp
DVarE [Name]
lnames
          rvars = (Name -> DExp) -> [Name] -> [DExp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DExp
DVarE [Name]
rnames
      return $ DClause
        [DConP lname [] lpats, DConP rname [] rpats]
        (dCasesE
          (zipWith (\DExp
l DExp
r -> DExp -> [DExp] -> DExp
foldExp (Name -> DExp
DVarE Name
sDecideMethName) [DExp
l, DExp
r])
                   lvars rvars)
          ((DClause
              (replicate
                lNumArgs
                (DConP provedName [] [DConP reflName [] []]))
              (DAppE (DConE provedName) (DConE reflName))) :
           [ DClause
               (replicate i DWildP ++
                  DConP disprovedName [] [DVarP contra] :
                  replicate (lNumArgs - i - 1) DWildP)
               (DAppE
                  (DConE disprovedName)
                  (dLamCaseE
                     [DMatch (DConP reflName [] []) $
                      (DAppE (DVarE contra)
                             (DConE reflName))]))
           | i <- [0..lNumArgs-1] ]))

  | Bool
otherwise =
    DClause -> q DClause
forall a. a -> q a
forall (m :: * -> *) a. Monad m => a -> m a
return (DClause -> q DClause) -> DClause -> q DClause
forall a b. (a -> b) -> a -> b
$ [DPat] -> DExp -> DClause
DClause
      [Name -> DCxt -> [DPat] -> DPat
DConP Name
lname [] (Int -> DPat -> [DPat]
forall a. Int -> a -> [a]
replicate Int
lNumArgs DPat
DWildP),
       Name -> DCxt -> [DPat] -> DPat
DConP Name
rname [] (Int -> DPat -> [DPat]
forall a. Int -> a -> [a]
replicate Int
rNumArgs DPat
DWildP)]
      (DExp -> DExp -> DExp
DAppE (Name -> DExp
DConE Name
disprovedName) ([DMatch] -> DExp
dLamCaseE []))

  where
    (Name
lname, Int
lNumArgs) = DCon -> (Name, Int)
extractNameArgs DCon
c1
    (Name
rname, Int
rNumArgs) = DCon -> (Name, Int)
extractNameArgs DCon
c2

mkEmptyDecideMethClause :: Quasi q => q DClause
mkEmptyDecideMethClause :: forall (q :: * -> *). Quasi q => q DClause
mkEmptyDecideMethClause = do
  x <- String -> q Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"x"
  pure $ DClause [DVarP x, DWildP]
       $ DConE provedName `DAppE` dCaseE (DVarE x) []