{- Data/Singletons/Single/Eq.hs

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

Defines functions to generate SEq and SDecide instances.
-}

module Data.Singletons.Single.Eq where

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

-- making the SEq instance and the SDecide instance are rather similar,
-- so we generalize
type EqualityClassDesc q = ((DCon, DCon) -> q DClause, q DClause, Name, Name)
sEqClassDesc, sDecideClassDesc :: Quasi q => EqualityClassDesc q
sEqClassDesc :: EqualityClassDesc q
sEqClassDesc = ((DCon, DCon) -> q DClause
forall (q :: * -> *). Quasi q => (DCon, DCon) -> q DClause
mkEqMethClause, q DClause
forall (q :: * -> *). Applicative q => q DClause
mkEmptyEqMethClause, Name
sEqClassName, Name
sEqMethName)
sDecideClassDesc :: EqualityClassDesc q
sDecideClassDesc = ((DCon, DCon) -> q DClause
forall (q :: * -> *). Quasi q => (DCon, DCon) -> q DClause
mkDecideMethClause, q DClause
forall (q :: * -> *). Quasi q => q DClause
mkEmptyDecideMethClause, Name
sDecideClassName, Name
sDecideMethName)

mkEqualityInstance :: DsMonad q => Maybe DCxt -> DKind
                   -> [DCon] -- ^ The /original/ constructors (for inferring the instance context)
                   -> [DCon] -- ^ The /singletons/ constructors
                   -> EqualityClassDesc q -> q DDec
mkEqualityInstance :: Maybe DCxt
-> DKind -> [DCon] -> [DCon] -> EqualityClassDesc q -> q DDec
mkEqualityInstance mb_ctxt :: Maybe DCxt
mb_ctxt k :: DKind
k ctors :: [DCon]
ctors sctors :: [DCon]
sctors (mkMeth :: (DCon, DCon) -> q DClause
mkMeth, mkEmpty :: q DClause
mkEmpty, className :: Name
className, methName :: Name
methName) = do
  let sctorPairs :: [(DCon, DCon)]
sctorPairs = [ (DCon
sc1, DCon
sc2) | DCon
sc1 <- [DCon]
sctors, DCon
sc2 <- [DCon]
sctors ]
  [DClause]
methClauses <- if [DCon] -> 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
mkEmpty
                 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)
mapM (DCon, DCon) -> q DClause
mkMeth [(DCon, DCon)]
sctorPairs
  DCxt
constraints <- Maybe DCxt -> DKind -> DKind -> [DCon] -> q DCxt
forall (q :: * -> *).
DsMonad q =>
Maybe DCxt -> DKind -> DKind -> [DCon] -> q DCxt
inferConstraintsDef Maybe DCxt
mb_ctxt (Name -> DKind
DConT Name
className) DKind
k [DCon]
ctors
  DDec -> q DDec
forall (m :: * -> *) a. Monad m => a -> m a
return (DDec -> q DDec) -> DDec -> q DDec
forall a b. (a -> b) -> a -> b
$ Maybe Overlap
-> Maybe [DTyVarBndr] -> DCxt -> DKind -> [DDec] -> DDec
DInstanceD Maybe Overlap
forall a. Maybe a
Nothing Maybe [DTyVarBndr]
forall a. Maybe a
Nothing
                     DCxt
constraints
                     (DKind -> DKind -> DKind
DAppT (Name -> DKind
DConT Name
className) DKind
k)
                     [DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ Name -> [DClause] -> DLetDec
DFunD Name
methName [DClause]
methClauses]

data TestInstance = TestEquality
                  | TestCoercion

-- Make an instance of TestEquality or TestCoercion by leveraging SDecide.
mkTestInstance :: DsMonad q => Maybe DCxt -> DKind
               -> Name   -- ^ The name of the data type
               -> [DCon] -- ^ The /original/ constructors (for inferring the instance context)
               -> TestInstance -> q DDec
mkTestInstance :: Maybe DCxt -> DKind -> Name -> [DCon] -> TestInstance -> q DDec
mkTestInstance mb_ctxt :: Maybe DCxt
mb_ctxt k :: DKind
k data_name :: Name
data_name ctors :: [DCon]
ctors ti :: TestInstance
ti = do
  DCxt
constraints <- Maybe DCxt -> DKind -> DKind -> [DCon] -> q DCxt
forall (q :: * -> *).
DsMonad q =>
Maybe DCxt -> DKind -> DKind -> [DCon] -> q DCxt
inferConstraintsDef Maybe DCxt
mb_ctxt (Name -> DKind
DConT Name
sDecideClassName) DKind
k [DCon]
ctors
  DDec -> q DDec
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DDec -> q DDec) -> DDec -> q DDec
forall a b. (a -> b) -> a -> b
$ Maybe Overlap
-> Maybe [DTyVarBndr] -> DCxt -> DKind -> [DDec] -> DDec
DInstanceD Maybe Overlap
forall a. Maybe a
Nothing Maybe [DTyVarBndr]
forall a. Maybe a
Nothing
                    DCxt
constraints
                    (DKind -> DKind -> DKind
DAppT (Name -> DKind
DConT Name
tiClassName)
                           (Name -> DKind
DConT (Name -> Name
singTyConName Name
data_name)
                             DKind -> DKind -> DKind
`DSigT` (DKind
DArrowT DKind -> DKind -> DKind
`DAppT` DKind
k DKind -> DKind -> DKind
`DAppT` Name -> DKind
DConT Name
typeKindName)))
                    [DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ Name -> [DClause] -> DLetDec
DFunD Name
tiMethName
                                     [[DPat] -> DExp -> DClause
DClause [] (Name -> DExp
DVarE Name
tiDefaultName)]]
  where
    (tiClassName :: Name
tiClassName, tiMethName :: Name
tiMethName, tiDefaultName :: Name
tiDefaultName) =
      case TestInstance
ti of
        TestEquality -> (Name
testEqualityClassName, Name
testEqualityMethName, Name
decideEqualityName)
        TestCoercion -> (Name
testCoercionClassName, Name
testCoercionMethName, Name
decideCoercionName)

mkEqMethClause :: Quasi q => (DCon, DCon) -> q DClause
mkEqMethClause :: (DCon, DCon) -> q DClause
mkEqMethClause (c1 :: DCon
c1, c2 :: DCon
c2)
  | Name
lname Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
rname = do
    [Name]
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 "a")
    [Name]
rnames <- 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 "b")
    let lpats :: [DPat]
lpats = (Name -> DPat) -> [Name] -> [DPat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DPat
DVarP [Name]
lnames
        rpats :: [DPat]
rpats = (Name -> DPat) -> [Name] -> [DPat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DPat
DVarP [Name]
rnames
        lvars :: [DExp]
lvars = (Name -> DExp) -> [Name] -> [DExp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DExp
DVarE [Name]
lnames
        rvars :: [DExp]
rvars = (Name -> DExp) -> [Name] -> [DExp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DExp
DVarE [Name]
rnames
    DClause -> q DClause
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 -> [DPat] -> DPat
DConP Name
lname [DPat]
lpats, Name -> [DPat] -> DPat
DConP Name
rname [DPat]
rpats]
      ([DExp] -> DExp
allExp ((DExp -> DExp -> DExp) -> [DExp] -> [DExp] -> [DExp]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\l :: DExp
l r :: DExp
r -> DExp -> [DExp] -> DExp
foldExp (Name -> DExp
DVarE Name
sEqMethName) [DExp
l, DExp
r])
                        [DExp]
lvars [DExp]
rvars))
  | Bool
otherwise =
    DClause -> q DClause
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 -> [DPat] -> DPat
DConP Name
lname (Int -> DPat -> [DPat]
forall a. Int -> a -> [a]
replicate Int
lNumArgs DPat
DWildP),
       Name -> [DPat] -> DPat
DConP Name
rname (Int -> DPat -> [DPat]
forall a. Int -> a -> [a]
replicate Int
rNumArgs DPat
DWildP)]
      (Name -> DExp
DConE (Name -> DExp) -> Name -> DExp
forall a b. (a -> b) -> a -> b
$ Name -> Name
singDataConName Name
falseName)
  where allExp :: [DExp] -> DExp
        allExp :: [DExp] -> DExp
allExp [] = Name -> DExp
DConE (Name -> DExp) -> Name -> DExp
forall a b. (a -> b) -> a -> b
$ Name -> Name
singDataConName Name
trueName
        allExp [one :: DExp
one] = DExp
one
        allExp (h :: DExp
h:t :: [DExp]
t) = DExp -> DExp -> DExp
DAppE (DExp -> DExp -> DExp
DAppE (Name -> DExp
DVarE (Name -> DExp) -> Name -> DExp
forall a b. (a -> b) -> a -> b
$ Name -> Name
singValName Name
andName) DExp
h) ([DExp] -> DExp
allExp [DExp]
t)

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

mkEmptyEqMethClause :: Applicative q => q DClause
mkEmptyEqMethClause :: q DClause
mkEmptyEqMethClause =
  DClause -> q DClause
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DClause -> q DClause) -> DClause -> q DClause
forall a b. (a -> b) -> a -> b
$ [DPat] -> DExp -> DClause
DClause [DPat
DWildP, DPat
DWildP]
       (DExp -> DClause) -> DExp -> DClause
forall a b. (a -> b) -> a -> b
$ Name -> DExp
DConE Name
strueName

mkDecideMethClause :: Quasi q => (DCon, DCon) -> q DClause
mkDecideMethClause :: (DCon, DCon) -> q DClause
mkDecideMethClause (c1 :: DCon
c1, c2 :: 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
== 0
    then DClause -> q DClause
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 -> [DPat] -> DPat
DConP Name
lname [], Name -> [DPat] -> DPat
DConP Name
rname []]
                          (DExp -> DExp -> DExp
DAppE (Name -> DExp
DConE Name
provedName) (Name -> DExp
DConE Name
reflName))
    else do
      [Name]
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 "a")
      [Name]
rnames <- 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 "b")
      Name
contra <- String -> q Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName "contra"
      let lpats :: [DPat]
lpats = (Name -> DPat) -> [Name] -> [DPat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DPat
DVarP [Name]
lnames
          rpats :: [DPat]
rpats = (Name -> DPat) -> [Name] -> [DPat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DPat
DVarP [Name]
rnames
          lvars :: [DExp]
lvars = (Name -> DExp) -> [Name] -> [DExp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DExp
DVarE [Name]
lnames
          rvars :: [DExp]
rvars = (Name -> DExp) -> [Name] -> [DExp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DExp
DVarE [Name]
rnames
      Name
refl <- String -> q Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName "refl"
      DClause -> q DClause
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 -> [DPat] -> DPat
DConP Name
lname [DPat]
lpats, Name -> [DPat] -> DPat
DConP Name
rname [DPat]
rpats]
        (DExp -> [DMatch] -> DExp
DCaseE ([DExp] -> DExp
mkTupleDExp ([DExp] -> DExp) -> [DExp] -> DExp
forall a b. (a -> b) -> a -> b
$
                 (DExp -> DExp -> DExp) -> [DExp] -> [DExp] -> [DExp]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\l :: DExp
l r :: DExp
r -> DExp -> [DExp] -> DExp
foldExp (Name -> DExp
DVarE Name
sDecideMethName) [DExp
l, DExp
r])
                         [DExp]
lvars [DExp]
rvars)
                ((DPat -> DExp -> DMatch
DMatch ([DPat] -> DPat
mkTupleDPat (Int -> DPat -> [DPat]
forall a. Int -> a -> [a]
replicate Int
lNumArgs
                                        (Name -> [DPat] -> DPat
DConP Name
provedName [Name -> [DPat] -> DPat
DConP Name
reflName []])))
                        (DExp -> DExp -> DExp
DAppE (Name -> DExp
DConE Name
provedName) (Name -> DExp
DConE Name
reflName))) DMatch -> [DMatch] -> [DMatch]
forall a. a -> [a] -> [a]
:
                 [DPat -> DExp -> DMatch
DMatch ([DPat] -> DPat
mkTupleDPat (Int -> DPat -> [DPat]
forall a. Int -> a -> [a]
replicate Int
i DPat
DWildP [DPat] -> [DPat] -> [DPat]
forall a. [a] -> [a] -> [a]
++
                                       Name -> [DPat] -> DPat
DConP Name
disprovedName [Name -> DPat
DVarP Name
contra] DPat -> [DPat] -> [DPat]
forall a. a -> [a] -> [a]
:
                                       Int -> DPat -> [DPat]
forall a. Int -> a -> [a]
replicate (Int
lNumArgs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) DPat
DWildP))
                         (DExp -> DExp -> DExp
DAppE (Name -> DExp
DConE Name
disprovedName)
                                ([Name] -> DExp -> DExp
DLamE [Name
refl] (DExp -> DExp) -> DExp -> DExp
forall a b. (a -> b) -> a -> b
$
                                 DExp -> [DMatch] -> DExp
DCaseE (Name -> DExp
DVarE Name
refl)
                                        [DPat -> DExp -> DMatch
DMatch (Name -> [DPat] -> DPat
DConP Name
reflName []) (DExp -> DMatch) -> DExp -> DMatch
forall a b. (a -> b) -> a -> b
$
                                         (DExp -> DExp -> DExp
DAppE (Name -> DExp
DVarE Name
contra)
                                                (Name -> DExp
DConE Name
reflName))]))
                 | Int
i <- [0..Int
lNumArgsInt -> Int -> Int
forall a. Num a => a -> a -> a
-1] ]))

  | Bool
otherwise = do
    Name
x <- String -> q Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName "x"
    DClause -> q DClause
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 -> [DPat] -> DPat
DConP Name
lname (Int -> DPat -> [DPat]
forall a. Int -> a -> [a]
replicate Int
lNumArgs DPat
DWildP),
       Name -> [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) ([Name] -> DExp -> DExp
DLamE [Name
x] (DExp -> [DMatch] -> DExp
DCaseE (Name -> DExp
DVarE Name
x) [])))

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

mkEmptyDecideMethClause :: Quasi q => q DClause
mkEmptyDecideMethClause :: q DClause
mkEmptyDecideMethClause = do
  Name
x <- String -> q Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName "x"
  DClause -> q DClause
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DClause -> q DClause) -> DClause -> q DClause
forall a b. (a -> b) -> a -> b
$ [DPat] -> DExp -> DClause
DClause [Name -> DPat
DVarP Name
x, DPat
DWildP]
       (DExp -> DClause) -> DExp -> DClause
forall a b. (a -> b) -> a -> b
$ Name -> DExp
DConE Name
provedName DExp -> DExp -> DExp
`DAppE` DExp -> [DMatch] -> DExp
DCaseE (Name -> DExp
DVarE Name
x) []