{- Data/Singletons/Promote/Eq.hs

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

This module defines the functions that generate type-level equality type
family instances.
-}

module Data.Singletons.Promote.Eq where

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

-- produce a closed type family helper and the instance
-- for (==) over the given list of ctors
mkEqTypeInstance :: Quasi q => DKind -> [DCon] -> q [DDec]
mkEqTypeInstance :: DKind -> [DCon] -> q [DDec]
mkEqTypeInstance kind :: DKind
kind cons :: [DCon]
cons = do
  Name
helperName <- String -> q Name
forall (q :: * -> *). Quasi q => String -> q Name
newUniqueName "Equals"
  Name
aName <- String -> q Name
forall (q :: * -> *). Quasi q => String -> q Name
qNewName "a"
  Name
bName <- String -> q Name
forall (q :: * -> *). Quasi q => String -> q Name
qNewName "b"
  [DTySynEqn]
true_branches <- (DCon -> q DTySynEqn) -> [DCon] -> q [DTySynEqn]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name -> DCon -> q DTySynEqn
forall (q :: * -> *). Quasi q => Name -> DCon -> q DTySynEqn
mk_branch Name
helperName) [DCon]
cons
  let null_branch :: DTySynEqn
null_branch  = Name -> Name -> DTySynEqn
catch_all_case Name
helperName Name
trueName
      false_branch :: DTySynEqn
false_branch = Name -> Name -> DTySynEqn
catch_all_case Name
helperName Name
falseName
      branches :: [DTySynEqn]
branches | [DCon] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DCon]
cons = [DTySynEqn
null_branch]
               | Bool
otherwise = [DTySynEqn]
true_branches [DTySynEqn] -> [DTySynEqn] -> [DTySynEqn]
forall a. [a] -> [a] -> [a]
++ [DTySynEqn
false_branch]
      closedFam :: DDec
closedFam = DTypeFamilyHead -> [DTySynEqn] -> DDec
DClosedTypeFamilyD (Name
-> [DTyVarBndr]
-> DFamilyResultSig
-> Maybe InjectivityAnn
-> DTypeFamilyHead
DTypeFamilyHead Name
helperName
                                                        -- We opt to give explicit kinds for the tyvars
                                                        -- in the helper type family.
                                                        -- See Note [Promoted class method kinds]
                                                        -- in Data.Singletons.Promote.
                                                      [ Name -> DKind -> DTyVarBndr
DKindedTV Name
aName DKind
kind
                                                      , Name -> DKind -> DTyVarBndr
DKindedTV Name
bName DKind
kind ]
                                                      (DKind -> DFamilyResultSig
DKindSig DKind
boolKi)
                                                      Maybe InjectivityAnn
forall a. Maybe a
Nothing)
                                     [DTySynEqn]
branches
      eqInst :: DDec
eqInst = DTySynEqn -> DDec
DTySynInstD (DTySynEqn -> DDec) -> DTySynEqn -> DDec
forall a b. (a -> b) -> a -> b
$
               Maybe [DTyVarBndr] -> DKind -> DKind -> DTySynEqn
DTySynEqn Maybe [DTyVarBndr]
forall a. Maybe a
Nothing
                         (Name -> DKind
DConT Name
tyEqName DKind -> DKind -> DKind
`DAppT` Name -> DKind
DVarT Name
aName DKind -> DKind -> DKind
`DAppT` Name -> DKind
DVarT Name
bName)
                         (DKind -> [DKind] -> DKind
foldType (Name -> DKind
DConT Name
helperName) [Name -> DKind
DVarT Name
aName, Name -> DKind
DVarT Name
bName])
      inst :: DDec
inst = Maybe Overlap
-> Maybe [DTyVarBndr] -> [DKind] -> DKind -> [DDec] -> DDec
DInstanceD Maybe Overlap
forall a. Maybe a
Nothing Maybe [DTyVarBndr]
forall a. Maybe a
Nothing [] ((Name -> DKind
DConT (Name -> DKind) -> Name -> DKind
forall a b. (a -> b) -> a -> b
$ Name -> Name
promoteClassName Name
eqName) DKind -> DKind -> DKind
`DAppT`
                                            DKind
kind) [DDec
eqInst]

  [DDec] -> q [DDec]
forall (m :: * -> *) a. Monad m => a -> m a
return [DDec
closedFam, DDec
inst]

  where mk_branch :: Quasi q => Name -> DCon -> q DTySynEqn
        mk_branch :: Name -> DCon -> q DTySynEqn
mk_branch helper_name :: Name
helper_name con :: DCon
con = do
          let (name :: Name
name, numArgs :: Int
numArgs) = DCon -> (Name, Int)
extractNameArgs DCon
con
          [Name]
lnames <- Int -> q Name -> q [Name]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
numArgs (String -> q Name
forall (q :: * -> *). Quasi q => String -> q Name
qNewName "a")
          [Name]
rnames <- Int -> q Name -> q [Name]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
numArgs (String -> q Name
forall (q :: * -> *). Quasi q => String -> q Name
qNewName "b")
          let lvars :: [DKind]
lvars = (Name -> DKind) -> [Name] -> [DKind]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DKind
DVarT [Name]
lnames
              rvars :: [DKind]
rvars = (Name -> DKind) -> [Name] -> [DKind]
forall a b. (a -> b) -> [a] -> [b]
map Name -> DKind
DVarT [Name]
rnames
              ltype :: DKind
ltype = DKind -> [DKind] -> DKind
foldType (Name -> DKind
DConT Name
name) [DKind]
lvars
              rtype :: DKind
rtype = DKind -> [DKind] -> DKind
foldType (Name -> DKind
DConT Name
name) [DKind]
rvars
              results :: [DKind]
results = (DKind -> DKind -> DKind) -> [DKind] -> [DKind] -> [DKind]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\l :: DKind
l r :: DKind
r -> DKind -> [DKind] -> DKind
foldType (Name -> DKind
DConT Name
tyEqName) [DKind
l, DKind
r]) [DKind]
lvars [DKind]
rvars
              result :: DKind
result = [DKind] -> DKind
tyAll [DKind]
results
          DTySynEqn -> q DTySynEqn
forall (m :: * -> *) a. Monad m => a -> m a
return (DTySynEqn -> q DTySynEqn) -> DTySynEqn -> q DTySynEqn
forall a b. (a -> b) -> a -> b
$ Maybe [DTyVarBndr] -> DKind -> DKind -> DTySynEqn
DTySynEqn Maybe [DTyVarBndr]
forall a. Maybe a
Nothing
                             (Name -> DKind
DConT Name
helper_name DKind -> DKind -> DKind
`DAppT` DKind
ltype DKind -> DKind -> DKind
`DAppT` DKind
rtype)
                             DKind
result

        catch_all_case :: Name -> Name -> DTySynEqn
        catch_all_case :: Name -> Name -> DTySynEqn
catch_all_case helper_name :: Name
helper_name returned_val_name :: Name
returned_val_name =
          Maybe [DTyVarBndr] -> DKind -> DKind -> DTySynEqn
DTySynEqn Maybe [DTyVarBndr]
forall a. Maybe a
Nothing
                    (Name -> DKind
DConT Name
helper_name
                       DKind -> DKind -> DKind
`DAppT` DKind -> DKind -> DKind
DSigT DKind
DWildCardT DKind
kind
                       DKind -> DKind -> DKind
`DAppT` DKind -> DKind -> DKind
DSigT DKind
DWildCardT DKind
kind)
                    (Name -> DKind
promoteValRhs Name
returned_val_name)

        tyAll :: [DType] -> DType -- "all" at the type level
        tyAll :: [DKind] -> DKind
tyAll [] = (Name -> DKind
promoteValRhs Name
trueName)
        tyAll [one :: DKind
one] = DKind
one
        tyAll (h :: DKind
h:t :: [DKind]
t) = DKind -> [DKind] -> DKind
foldType (Name -> DKind
DConT (Name -> DKind) -> Name -> DKind
forall a b. (a -> b) -> a -> b
$ Name -> Name
promoteValNameLhs Name
andName) [DKind
h, ([DKind] -> DKind
tyAll [DKind]
t)]
           -- I could use the Apply nonsense here, but there's no reason to