{- 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.TH.Options
import Data.Singletons.Util
import Control.Monad

-- produce a closed type family helper and the instance
-- for (==) over the given list of ctors
mkEqTypeInstance :: OptionsMonad q => DKind -> [DCon] -> q [DDec]
mkEqTypeInstance :: DKind -> [DCon] -> q [DDec]
mkEqTypeInstance DKind
kind [DCon]
cons = do
  Options
opts <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  Name
helperName <- String -> q Name
forall (q :: * -> *). Quasi q => String -> q Name
newUniqueName String
"Equals"
  Name
aName <- String -> q Name
forall (q :: * -> *). Quasi q => String -> q Name
qNewName String
"a"
  Name
bName <- String -> q Name
forall (q :: * -> *). Quasi q => String -> q Name
qNewName String
"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 :: * -> *). OptionsMonad q => Name -> DCon -> q DTySynEqn
mk_branch Name
helperName) [DCon]
cons
  let null_branch :: DTySynEqn
null_branch  = Options -> Name -> Name -> DTySynEqn
catch_all_case Options
opts Name
helperName Name
trueName
      false_branch :: DTySynEqn
false_branch = Options -> Name -> Name -> DTySynEqn
catch_all_case Options
opts 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]
      -- We opt to give an explicit kind signature for the helper type family.
      -- See Note [Promoted class method kinds] in Data.Singletons.Promote.
      sakDec :: DDec
sakDec    = Name -> DKind -> DDec
DKiSigD Name
helperName (DKind -> DDec) -> DKind -> DDec
forall a b. (a -> b) -> a -> b
$ [DTyVarBndr] -> DCxt -> DCxt -> DKind -> DKind
ravelVanillaDType [] [] [DKind
kind, DKind
kind] DKind
boolKi
      closedFam :: DDec
closedFam = DTypeFamilyHead -> [DTySynEqn] -> DDec
DClosedTypeFamilyD (Name
-> [DTyVarBndr]
-> DFamilyResultSig
-> Maybe InjectivityAnn
-> DTypeFamilyHead
DTypeFamilyHead Name
helperName
                                                      [Name -> DTyVarBndr
DPlainTV Name
aName, Name -> DTyVarBndr
DPlainTV Name
bName]
                                                      DFamilyResultSig
DNoSig
                                                      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 -> DCxt -> DKind
foldType (Name -> DKind
DConT Name
helperName) [Name -> DKind
DVarT Name
aName, Name -> DKind
DVarT Name
bName])
      inst :: DDec
inst = Maybe Overlap
-> Maybe [DTyVarBndr] -> DCxt -> 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
$ Options -> Name -> Name
promotedClassName Options
opts Name
eqName) DKind -> DKind -> DKind
`DAppT`
                                            DKind
kind) [DDec
eqInst]

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

  where mk_branch :: OptionsMonad q => Name -> DCon -> q DTySynEqn
        mk_branch :: Name -> DCon -> q DTySynEqn
mk_branch Name
helper_name DCon
con = do
          Options
opts <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
          let (Name
name, 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 String
"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 String
"b")
          let lvars :: DCxt
lvars = (Name -> DKind) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DKind
DVarT [Name]
lnames
              rvars :: DCxt
rvars = (Name -> DKind) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DKind
DVarT [Name]
rnames
              ltype :: DKind
ltype = DKind -> DCxt -> DKind
foldType (Name -> DKind
DConT Name
name) DCxt
lvars
              rtype :: DKind
rtype = DKind -> DCxt -> DKind
foldType (Name -> DKind
DConT Name
name) DCxt
rvars
              results :: DCxt
results = (DKind -> DKind -> DKind) -> DCxt -> DCxt -> DCxt
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\DKind
l DKind
r -> DKind -> DCxt -> DKind
foldType (Name -> DKind
DConT Name
tyEqName) [DKind
l, DKind
r]) DCxt
lvars DCxt
rvars
              result :: DKind
result = Options -> DCxt -> DKind
tyAll Options
opts DCxt
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 :: Options -> Name -> Name -> DTySynEqn
        catch_all_case :: Options -> Name -> Name -> DTySynEqn
catch_all_case Options
opts Name
helper_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
DConT (Name -> DKind) -> Name -> DKind
forall a b. (a -> b) -> a -> b
$ Options -> Name -> Name
defunctionalizedName0 Options
opts Name
returned_val_name)

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