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
mkDecideInstance :: OptionsMonad q => Maybe DCxt -> DType
-> [DCon]
-> [DCon]
-> 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 ]
[DClause]
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
DCxt
constraints <- Maybe DCxt -> DType -> DType -> [DCon] -> q DCxt
forall (q :: * -> *).
DsMonad q =>
Maybe DCxt -> DType -> DType -> [DCon] -> q DCxt
inferConstraintsDef Maybe DCxt
mb_ctxt (Name -> DType
DConT Name
sDecideClassName) DType
data_ty [DCon]
ctors
DType
data_ki <- DType -> q DType
forall (m :: * -> *). OptionsMonad m => DType -> m DType
promoteType DType
data_ty
DDec -> q DDec
forall a. a -> q a
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 [DTyVarBndrUnit] -> DCxt -> DType -> [DDec] -> DDec
DInstanceD Maybe Overlap
forall a. Maybe a
Nothing Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing
DCxt
constraints
(DType -> DType -> DType
DAppT (Name -> DType
DConT Name
sDecideClassName) DType
data_ki)
[DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ Name -> [DClause] -> DLetDec
DFunD Name
sDecideMethName [DClause]
methClauses]
data TestInstance = TestEquality
| TestCoercion
mkTestInstance :: OptionsMonad q => Maybe DCxt -> DType
-> Name
-> [DCon]
-> 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
Options
opts <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
DCxt
constraints <- Maybe DCxt -> DType -> DType -> [DCon] -> q DCxt
forall (q :: * -> *).
DsMonad q =>
Maybe DCxt -> DType -> DType -> [DCon] -> q DCxt
inferConstraintsDef Maybe DCxt
mb_ctxt (Name -> DType
DConT Name
sDecideClassName) DType
data_ty [DCon]
ctors
DType
data_ki <- DType -> q DType
forall (m :: * -> *). OptionsMonad m => DType -> m DType
promoteType DType
data_ty
DDec -> q DDec
forall a. a -> q a
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 [DTyVarBndrUnit] -> DCxt -> DType -> [DDec] -> DDec
DInstanceD Maybe Overlap
forall a. Maybe a
Nothing Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing
DCxt
constraints
(DType -> DType -> DType
DAppT (Name -> DType
DConT Name
tiClassName)
(Name -> DType
DConT (Options -> Name -> Name
singledDataTypeName Options
opts Name
data_name)
DType -> DType -> DType
`DSigT` (DType
DArrowT DType -> DType -> DType
`DAppT` DType
data_ki DType -> DType -> DType
`DAppT` Name -> DType
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
(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
[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 String
"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 String
"b")
Name
contra <- String -> q Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"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 String
"refl"
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 [] [DPat]
lpats, Name -> DCxt -> [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 (\DExp
l 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 -> DCxt -> [DPat] -> DPat
DConP Name
provedName [] [Name -> DCxt -> [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 -> DCxt -> [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
- Int
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 -> DCxt -> [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 <- [Int
0..Int
lNumArgsInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1] ]))
| Bool
otherwise = do
Name
x <- String -> q Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"x"
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) ([Name] -> DExp -> DExp
DLamE [Name
x] (DExp -> [DMatch] -> DExp
DCaseE (Name -> DExp
DVarE Name
x) [])))
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
Name
x <- String -> q Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"x"
DClause -> q DClause
forall a. a -> q a
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) []