{-# LANGUAGE CPP, ExplicitNamespaces, MultiWayIf, PatternGuards #-}
{-# LANGUAGE TemplateHaskell, TupleSections, ViewPatterns #-}
module Proof.Propositional.TH where
import Proof.Propositional.Empty
import Proof.Propositional.Inhabited
import Control.Arrow (Kleisli (..), second)
import Control.Monad (forM, zipWithM)
import Data.Foldable (asum)
import Data.Map (Map)
import qualified Data.Map as M
import Data.Maybe (fromJust)
import Data.Type.Equality ((:~:) (..))
import Language.Haskell.TH (DecsQ, Lit (CharL, IntegerL),
Name, Q, TypeQ, isInstance,
newName, ppr)
import Language.Haskell.TH.Desugar (DClause (..), DCon (..),
DConFields (..), DCxt, DDec (..),
DExp (..), DInfo (..),
DLetDec (DFunD),
#if MIN_VERSION_th_desugar(1,10,0)
DPat (DConP, DVarP), DPred,
#else
DPat (DConPa, DVarPa), DPred(..),
#endif
#if MIN_VERSION_th_desugar(1,12,0)
DForallTelescope(..),
#endif
DTyVarBndr (..), DType (..),
Overlap (Overlapping), desugar,
dsReify, expandType, substTy,
sweeten)
#if !MIN_VERSION_base(4,13,0)
import Data.Semigroup (Semigroup (..))
#endif
#if MIN_VERSION_th_desugar(1,12,0)
import Data.Functor (void)
#endif
refute :: TypeQ -> DecsQ
refute :: TypeQ -> DecsQ
refute TypeQ
tps = do
DType
tp <- forall (q :: * -> *). DsMonad q => DType -> q DType
expandType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall th ds (q :: * -> *).
(Desugar th ds, DsMonad q) =>
th -> q ds
desugar forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TypeQ
tps
let Just ([Name]
_, Name
tyName, [DType]
args) = DType -> Maybe ([Name], Name, [DType])
splitType DType
tp
mkInst :: [DType] -> [DClause] -> m [Dec]
mkInst [DType]
dxt [DClause]
cls = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall th ds. Desugar th ds => ds -> th
sweeten
[Maybe Overlap
-> Maybe [DTyVarBndrUnit] -> [DType] -> DType -> [DDec] -> DDec
DInstanceD (forall a. a -> Maybe a
Just Overlap
Overlapping)
#if MIN_VERSION_th_desugar(1,10,0)
forall a. Maybe a
Nothing
#endif
[DType]
dxt
(DType -> DType -> DType
DAppT (Name -> DType
DConT ''Empty) (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl DType -> DType -> DType
DAppT (Name -> DType
DConT Name
tyName) [DType]
args))
[DLetDec -> DDec
DLetDec forall a b. (a -> b) -> a -> b
$ Name -> [DClause] -> DLetDec
DFunD 'eliminate [DClause]
cls]
]
if Name
tyName forall a. Eq a => a -> a -> Bool
== ''(:~:)
then do
let [DType
l, DType
r] = [DType]
args
Name
v <- forall (m :: * -> *). Quote m => String -> m Name
newName String
"_v"
EqlJudge
dist <- DType -> DType -> Q EqlJudge
compareType DType
l DType
r
case EqlJudge
dist of
EqlJudge
NonEqual -> forall {m :: * -> *}. Monad m => [DType] -> [DClause] -> m [Dec]
mkInst [] [[DPat] -> DExp -> DClause
DClause [] forall a b. (a -> b) -> a -> b
$ [Name] -> DExp -> DExp
DLamE [Name
v] (DExp -> [DMatch] -> DExp
DCaseE (Name -> DExp
DVarE Name
v) []) ]
EqlJudge
Equal -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Equal: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Ppr a => a -> Doc
ppr forall a b. (a -> b) -> a -> b
$ forall th ds. Desugar th ds => ds -> th
sweeten DType
l) forall a. [a] -> [a] -> [a]
++ String
" ~ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Ppr a => a -> Doc
ppr forall a b. (a -> b) -> a -> b
$ forall th ds. Desugar th ds => ds -> th
sweeten DType
r)
EqlJudge
Undecidable -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"No enough info to check non-equality: " forall a. [a] -> [a] -> [a]
++
forall a. Show a => a -> String
show (forall a. Ppr a => a -> Doc
ppr forall a b. (a -> b) -> a -> b
$ forall th ds. Desugar th ds => ds -> th
sweeten DType
l) forall a. [a] -> [a] -> [a]
++ String
" ~ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Ppr a => a -> Doc
ppr forall a b. (a -> b) -> a -> b
$ forall th ds. Desugar th ds => ds -> th
sweeten DType
r)
else do
([DType]
dxt, [DCon]
cons) <- [DType] -> DInfo -> Q ([DType], [DCon])
resolveSubsts [DType]
args forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasCallStack => Maybe a -> a
fromJust forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReify Name
tyName
Just [DClause]
cls <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM DCon -> Q (Maybe DClause)
buildRefuteClause [DCon]
cons
forall {m :: * -> *}. Monad m => [DType] -> [DClause] -> m [Dec]
mkInst [DType]
dxt [DClause]
cls
prove :: TypeQ -> DecsQ
prove :: TypeQ -> DecsQ
prove TypeQ
tps = do
DType
tp <- forall (q :: * -> *). DsMonad q => DType -> q DType
expandType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall th ds (q :: * -> *).
(Desugar th ds, DsMonad q) =>
th -> q ds
desugar forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TypeQ
tps
let Just ([Name]
_, Name
tyName, [DType]
args) = DType -> Maybe ([Name], Name, [DType])
splitType DType
tp
mkInst :: [DType] -> [DClause] -> m [Dec]
mkInst [DType]
dxt [DClause]
cls = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall th ds. Desugar th ds => ds -> th
sweeten
[Maybe Overlap
-> Maybe [DTyVarBndrUnit] -> [DType] -> DType -> [DDec] -> DDec
DInstanceD (forall a. a -> Maybe a
Just Overlap
Overlapping)
#if MIN_VERSION_th_desugar(1,10,0)
forall a. Maybe a
Nothing
#endif
[DType]
dxt
(DType -> DType -> DType
DAppT (Name -> DType
DConT ''Inhabited) (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl DType -> DType -> DType
DAppT (Name -> DType
DConT Name
tyName) [DType]
args))
[DLetDec -> DDec
DLetDec forall a b. (a -> b) -> a -> b
$ Name -> [DClause] -> DLetDec
DFunD 'trivial [DClause]
cls]
]
Bool
isNum <- Name -> [Type] -> Q Bool
isInstance ''Num [forall th ds. Desugar th ds => ds -> th
sweeten DType
tp]
if | Bool
isNum -> forall {m :: * -> *}. Monad m => [DType] -> [DClause] -> m [Dec]
mkInst [] [[DPat] -> DExp -> DClause
DClause [] forall a b. (a -> b) -> a -> b
$ Lit -> DExp
DLitE forall a b. (a -> b) -> a -> b
$ Integer -> Lit
IntegerL Integer
0 ]
| Name
tyName forall a. Eq a => a -> a -> Bool
== ''Char -> forall {m :: * -> *}. Monad m => [DType] -> [DClause] -> m [Dec]
mkInst [] [[DPat] -> DExp -> DClause
DClause [] forall a b. (a -> b) -> a -> b
$ Lit -> DExp
DLitE forall a b. (a -> b) -> a -> b
$ Char -> Lit
CharL Char
'\NUL']
| Name
tyName forall a. Eq a => a -> a -> Bool
== ''(:~:) -> do
let [DType
l, DType
r] = [DType]
args
EqlJudge
dist <- DType -> DType -> Q EqlJudge
compareType DType
l DType
r
case EqlJudge
dist of
EqlJudge
NonEqual -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Equal: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Ppr a => a -> Doc
ppr forall a b. (a -> b) -> a -> b
$ forall th ds. Desugar th ds => ds -> th
sweeten DType
l) forall a. [a] -> [a] -> [a]
++ String
" ~ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Ppr a => a -> Doc
ppr forall a b. (a -> b) -> a -> b
$ forall th ds. Desugar th ds => ds -> th
sweeten DType
r)
EqlJudge
Equal -> forall {m :: * -> *}. Monad m => [DType] -> [DClause] -> m [Dec]
mkInst [] [[DPat] -> DExp -> DClause
DClause [] forall a b. (a -> b) -> a -> b
$ Name -> DExp
DConE 'Refl ]
EqlJudge
Undecidable -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"No enough info to check non-equality: " forall a. [a] -> [a] -> [a]
++
forall a. Show a => a -> String
show (forall a. Ppr a => a -> Doc
ppr forall a b. (a -> b) -> a -> b
$ forall th ds. Desugar th ds => ds -> th
sweeten DType
l) forall a. [a] -> [a] -> [a]
++ String
" ~ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Ppr a => a -> Doc
ppr forall a b. (a -> b) -> a -> b
$ forall th ds. Desugar th ds => ds -> th
sweeten DType
r)
| Bool
otherwise -> do
([DType]
dxt, [DCon]
cons) <- [DType] -> DInfo -> Q ([DType], [DCon])
resolveSubsts [DType]
args forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasCallStack => Maybe a -> a
fromJust forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReify Name
tyName
Just DClause
cls <- forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM DCon -> Q (Maybe DClause)
buildProveClause [DCon]
cons
forall {m :: * -> *}. Monad m => [DType] -> [DClause] -> m [Dec]
mkInst [DType]
dxt [DClause
cls]
buildClause :: Name -> (DType -> Q b) -> (DType -> b -> DExp)
-> (Name -> [Maybe DExp] -> Maybe DExp) -> (Name -> [b] -> [DPat])
-> DCon -> Q (Maybe DClause)
buildClause :: forall b.
Name
-> (DType -> Q b)
-> (DType -> b -> DExp)
-> (Name -> [Maybe DExp] -> Maybe DExp)
-> (Name -> [b] -> [DPat])
-> DCon
-> Q (Maybe DClause)
buildClause Name
clsName DType -> Q b
genPlaceHolder DType -> b -> DExp
buildFactor Name -> [Maybe DExp] -> Maybe DExp
flattenExps Name -> [b] -> [DPat]
toPats (DCon [DTyVarBndrSpec]
_ [DType]
_ Name
cName DConFields
flds DType
_) = do
let tys :: [DType]
tys = DConFields -> [DType]
fieldsVars DConFields
flds
[b]
varDic <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM DType -> Q b
genPlaceHolder [DType]
tys
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([DPat] -> DExp -> DClause
DClause forall a b. (a -> b) -> a -> b
$ Name -> [b] -> [DPat]
toPats Name
cName [b]
varDic) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Maybe DExp] -> Maybe DExp
flattenExps Name
cName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM DType -> b -> Q (Maybe DExp)
tryProc [DType]
tys [b]
varDic
where
tryProc :: DType -> b -> Q (Maybe DExp)
tryProc DType
ty b
name = do
Bool
isEmpty <- Name -> [Type] -> Q Bool
isInstance Name
clsName forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[]) forall a b. (a -> b) -> a -> b
$ forall th ds. Desugar th ds => ds -> th
sweeten DType
ty
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if Bool
isEmpty
then forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ DType -> b -> DExp
buildFactor DType
ty b
name
else forall a. Maybe a
Nothing
buildRefuteClause :: DCon -> Q (Maybe DClause)
buildRefuteClause :: DCon -> Q (Maybe DClause)
buildRefuteClause =
forall b.
Name
-> (DType -> Q b)
-> (DType -> b -> DExp)
-> (Name -> [Maybe DExp] -> Maybe DExp)
-> (Name -> [b] -> [DPat])
-> DCon
-> Q (Maybe DClause)
buildClause
''Empty (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Quote m => String -> m Name
newName String
"_x")
(forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ (Name -> DExp
DVarE 'eliminate DExp -> DExp -> DExp
`DAppE`) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> DExp
DVarE) (forall a b. a -> b -> a
const forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum)
#if MIN_VERSION_th_desugar(1,13,0)
(\Name
cName [Name]
ps -> [Name -> [DType] -> [DPat] -> DPat
DConP Name
cName [] forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Name -> DPat
DVarP [Name]
ps])
#elif MIN_VERSION_th_desugar(1,10,0)
(\cName ps -> [DConP cName $ map DVarP ps])
#else
(\cName ps -> [DConPa cName $ map DVarPa ps])
#endif
buildProveClause :: DCon -> Q (Maybe DClause)
buildProveClause :: DCon -> Q (Maybe DClause)
buildProveClause =
forall b.
Name
-> (DType -> Q b)
-> (DType -> b -> DExp)
-> (Name -> [Maybe DExp] -> Maybe DExp)
-> (Name -> [b] -> [DPat])
-> DCon
-> Q (Maybe DClause)
buildClause
''Inhabited (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ())
(forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Name -> DExp
DVarE 'trivial)
(\ Name
con [Maybe DExp]
args -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl DExp -> DExp -> DExp
DAppE (Name -> DExp
DConE Name
con) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Maybe DExp]
args )
(forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const [])
fieldsVars :: DConFields -> [DType]
#if MIN_VERSION_th_desugar(1,8,0)
fieldsVars :: DConFields -> [DType]
fieldsVars (DNormalC Bool
_ [DBangType]
fs)
#else
fieldsVars (DNormalC fs)
#endif
= forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [DBangType]
fs
fieldsVars (DRecC [DVarBangType]
fs) = forall a b. (a -> b) -> [a] -> [b]
map (\(Name
_,Bang
_,DType
c) -> DType
c) [DVarBangType]
fs
resolveSubsts :: [DType] -> DInfo -> Q (DCxt, [DCon])
resolveSubsts :: [DType] -> DInfo -> Q ([DType], [DCon])
resolveSubsts [DType]
args DInfo
info =
case DInfo
info of
(DTyConI (DDataD DataFlavor
_ [DType]
cxt Name
_ [DTyVarBndrUnit]
tvbs
#if MIN_VERSION_th_desugar(1,9,0)
Maybe DType
_
#endif
[DCon]
dcons [DDerivClause]
_) Maybe [DDec]
_) -> do
let dic :: Map Name DType
dic = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall flag. DTyVarBndr flag -> Name
dtvbToName [DTyVarBndrUnit]
tvbs) [DType]
args
([DType]
cxt , ) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Map Name DType -> DCon -> Q DCon
substDCon Map Name DType
dic) [DCon]
dcons
(DTyConI DDec
_ Maybe [DDec]
_) -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Not supported data ty"
DInfo
_ -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Please pass data-type"
type SubstDic = Map Name DType
substDCon :: SubstDic -> DCon -> Q DCon
substDCon :: Map Name DType -> DCon -> Q DCon
substDCon Map Name DType
dic (DCon [DTyVarBndrSpec]
forall'd [DType]
cxt Name
conName DConFields
fields DType
mPhantom) =
[DTyVarBndrSpec] -> [DType] -> Name -> DConFields -> DType -> DCon
DCon [DTyVarBndrSpec]
forall'd [DType]
cxt Name
conName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Name DType -> DConFields -> Q DConFields
substFields Map Name DType
dic DConFields
fields
#if MIN_VERSION_th_desugar(1,9,0)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (q :: * -> *). Quasi q => Map Name DType -> DType -> q DType
substTy Map Name DType
dic DType
mPhantom
#else
<*> mapM (substTy dic) mPhantom
#endif
substFields :: SubstDic -> DConFields -> Q DConFields
substFields :: Map Name DType -> DConFields -> Q DConFields
substFields Map Name DType
subst
#if MIN_VERSION_th_desugar(1,8,0)
(DNormalC Bool
fixi [DBangType]
fs)
#else
(DNormalC fs)
#endif
=
#if MIN_VERSION_th_desugar(1,8,0)
Bool -> [DBangType] -> DConFields
DNormalC Bool
fixi forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
#else
DNormalC <$>
#endif
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a b. Kleisli m a b -> a -> m b
runKleisli forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli forall a b. (a -> b) -> a -> b
$ forall (q :: * -> *). Quasi q => Map Name DType -> DType -> q DType
substTy Map Name DType
subst) [DBangType]
fs
substFields Map Name DType
subst (DRecC [DVarBangType]
fs) =
[DVarBangType] -> DConFields
DRecC forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [DVarBangType]
fs (\(Name
a,Bang
b,DType
c) -> (Name
a, Bang
b ,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (q :: * -> *). Quasi q => Map Name DType -> DType -> q DType
substTy Map Name DType
subst DType
c)
splitType :: DType -> Maybe ([Name], Name, [DType])
#if MIN_VERSION_th_desugar(1,11,0)
splitType :: DType -> Maybe ([Name], Name, [DType])
splitType (DConstrainedT [DType]
_ DType
t) = DType -> Maybe ([Name], Name, [DType])
splitType DType
t
#if MIN_VERSION_th_desugar(1,12,0)
splitType (DForallT (DForallTelescope -> [DTyVarBndrUnit]
unTelescope -> [DTyVarBndrUnit]
vs) DType
t)
#else
splitType (DForallT _ vs t)
#endif
#else
splitType (DForallT vs _ t)
#endif
= (\([Name]
a,Name
b,[DType]
c) -> (forall a b. (a -> b) -> [a] -> [b]
map forall flag. DTyVarBndr flag -> Name
dtvbToName [DTyVarBndrUnit]
vs forall a. [a] -> [a] -> [a]
++ [Name]
a, Name
b, [DType]
c)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> Maybe ([Name], Name, [DType])
splitType DType
t
splitType (DAppT DType
t1 DType
t2) = (\([Name]
a,Name
b,[DType]
c) -> ([Name]
a, Name
b, [DType]
c forall a. [a] -> [a] -> [a]
++ [DType
t2])) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> Maybe ([Name], Name, [DType])
splitType DType
t1
splitType (DSigT DType
t DType
_) = DType -> Maybe ([Name], Name, [DType])
splitType DType
t
splitType (DVarT Name
_) = forall a. Maybe a
Nothing
splitType (DConT Name
n) = forall a. a -> Maybe a
Just ([], Name
n, [])
splitType DType
DArrowT = forall a. a -> Maybe a
Just ([], ''(->), [])
splitType (DLitT TyLit
_) = forall a. Maybe a
Nothing
splitType DType
DWildCardT = forall a. Maybe a
Nothing
#if !MIN_VERSION_th_desugar(1,9,0)
splitType DStarT = Nothing
#elif MIN_VERSION_th_desugar(1,10,0)
splitType (DAppKindT DType
_ DType
_) = forall a. Maybe a
Nothing
#endif
data EqlJudge = NonEqual | Undecidable | Equal
deriving (ReadPrec [EqlJudge]
ReadPrec EqlJudge
Int -> ReadS EqlJudge
ReadS [EqlJudge]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [EqlJudge]
$creadListPrec :: ReadPrec [EqlJudge]
readPrec :: ReadPrec EqlJudge
$creadPrec :: ReadPrec EqlJudge
readList :: ReadS [EqlJudge]
$creadList :: ReadS [EqlJudge]
readsPrec :: Int -> ReadS EqlJudge
$creadsPrec :: Int -> ReadS EqlJudge
Read, Int -> EqlJudge -> ShowS
[EqlJudge] -> ShowS
EqlJudge -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [EqlJudge] -> ShowS
$cshowList :: [EqlJudge] -> ShowS
show :: EqlJudge -> String
$cshow :: EqlJudge -> String
showsPrec :: Int -> EqlJudge -> ShowS
$cshowsPrec :: Int -> EqlJudge -> ShowS
Show, EqlJudge -> EqlJudge -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: EqlJudge -> EqlJudge -> Bool
$c/= :: EqlJudge -> EqlJudge -> Bool
== :: EqlJudge -> EqlJudge -> Bool
$c== :: EqlJudge -> EqlJudge -> Bool
Eq, Eq EqlJudge
EqlJudge -> EqlJudge -> Bool
EqlJudge -> EqlJudge -> Ordering
EqlJudge -> EqlJudge -> EqlJudge
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: EqlJudge -> EqlJudge -> EqlJudge
$cmin :: EqlJudge -> EqlJudge -> EqlJudge
max :: EqlJudge -> EqlJudge -> EqlJudge
$cmax :: EqlJudge -> EqlJudge -> EqlJudge
>= :: EqlJudge -> EqlJudge -> Bool
$c>= :: EqlJudge -> EqlJudge -> Bool
> :: EqlJudge -> EqlJudge -> Bool
$c> :: EqlJudge -> EqlJudge -> Bool
<= :: EqlJudge -> EqlJudge -> Bool
$c<= :: EqlJudge -> EqlJudge -> Bool
< :: EqlJudge -> EqlJudge -> Bool
$c< :: EqlJudge -> EqlJudge -> Bool
compare :: EqlJudge -> EqlJudge -> Ordering
$ccompare :: EqlJudge -> EqlJudge -> Ordering
Ord)
instance Semigroup EqlJudge where
EqlJudge
NonEqual <> :: EqlJudge -> EqlJudge -> EqlJudge
<> EqlJudge
_ = EqlJudge
NonEqual
EqlJudge
Undecidable <> EqlJudge
NonEqual = EqlJudge
NonEqual
EqlJudge
Undecidable <> EqlJudge
_ = EqlJudge
Undecidable
EqlJudge
Equal <> EqlJudge
m = EqlJudge
m
instance Monoid EqlJudge where
mappend :: EqlJudge -> EqlJudge -> EqlJudge
mappend = forall a. Semigroup a => a -> a -> a
(<>)
mempty :: EqlJudge
mempty = EqlJudge
Equal
compareType :: DType -> DType -> Q EqlJudge
compareType :: DType -> DType -> Q EqlJudge
compareType DType
t0 DType
s0 = do
DType
t <- forall (q :: * -> *). DsMonad q => DType -> q DType
expandType DType
t0
DType
s <- forall (q :: * -> *). DsMonad q => DType -> q DType
expandType DType
s0
DType -> DType -> Q EqlJudge
compareType' DType
t DType
s
compareType' :: DType -> DType -> Q EqlJudge
compareType' :: DType -> DType -> Q EqlJudge
compareType' (DSigT DType
t1 DType
t2) (DSigT DType
s1 DType
s2)
= forall a. Semigroup a => a -> a -> a
(<>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> DType -> Q EqlJudge
compareType' DType
t1 DType
s1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DType -> DType -> Q EqlJudge
compareType' DType
t2 DType
s2
compareType' (DSigT DType
t DType
_) DType
s
= DType -> DType -> Q EqlJudge
compareType' DType
t DType
s
compareType' DType
t (DSigT DType
s DType
_)
= DType -> DType -> Q EqlJudge
compareType' DType
t DType
s
compareType' (DVarT Name
t) (DVarT Name
s)
| Name
t forall a. Eq a => a -> a -> Bool
== Name
s = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
| Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
compareType' (DVarT Name
_) DType
_ = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
compareType' DType
_ (DVarT Name
_) = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
compareType' DType
DWildCardT DType
_ = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
compareType' DType
_ DType
DWildCardT = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
#if MIN_VERSION_th_desugar(1,11,0)
compareType' (DConstrainedT [DType]
tCxt DType
t) (DConstrainedT [DType]
sCxt DType
s) = do
EqlJudge
pd <- [DType] -> [DType] -> Q EqlJudge
compareCxt [DType]
tCxt [DType]
sCxt
EqlJudge
bd <- DType -> DType -> Q EqlJudge
compareType' DType
t DType
s
forall (m :: * -> *) a. Monad m => a -> m a
return (EqlJudge
pd forall a. Semigroup a => a -> a -> a
<> EqlJudge
bd)
compareType' DConstrainedT{} DType
_ = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
#if MIN_VERSION_th_desugar(1,12,0)
compareType' (DForallT (DForallTelescope -> [DTyVarBndrUnit]
unTelescope -> [DTyVarBndrUnit]
tTvBs) DType
t) (DForallT (DForallTelescope -> [DTyVarBndrUnit]
unTelescope -> [DTyVarBndrUnit]
sTvBs) DType
s)
#else
compareType' (DForallT _ tTvBs t) (DForallT _ sTvBs s)
#endif
| forall (t :: * -> *) a. Foldable t => t a -> Int
length [DTyVarBndrUnit]
tTvBs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [DTyVarBndrUnit]
sTvBs = do
let dic :: Map Name DType
dic = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall flag. DTyVarBndr flag -> Name
dtvbToName [DTyVarBndrUnit]
sTvBs) (forall a b. (a -> b) -> [a] -> [b]
map (Name -> DType
DVarT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall flag. DTyVarBndr flag -> Name
dtvbToName) [DTyVarBndrUnit]
tTvBs)
DType
s' <- forall (q :: * -> *). Quasi q => Map Name DType -> DType -> q DType
substTy Map Name DType
dic DType
s
EqlJudge
bd <- DType -> DType -> Q EqlJudge
compareType' DType
t DType
s'
forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
bd
| Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
#else
compareType' (DForallT tTvBs tCxt t) (DForallT sTvBs sCxt s)
| length tTvBs == length sTvBs = do
let dic = M.fromList $ zip (map dtvbToName sTvBs) (map (DVarT . dtvbToName) tTvBs)
s' <- substTy dic s
pd <- compareCxt tCxt =<< mapM (substPred dic) sCxt
bd <- compareType' t s'
return (pd <> bd)
| otherwise = return NonEqual
#endif
compareType' DForallT{} DType
_ = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareType' (DAppT DType
t1 DType
t2) (DAppT DType
s1 DType
s2)
= forall a. Semigroup a => a -> a -> a
(<>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> DType -> Q EqlJudge
compareType' DType
t1 DType
s1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DType -> DType -> Q EqlJudge
compareType' DType
t2 DType
s2
compareType' (DConT Name
t) (DConT Name
s)
| Name
t forall a. Eq a => a -> a -> Bool
== Name
s = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
| Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareType' (DConT Name
_) DType
_ = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareType' DType
DArrowT DType
DArrowT = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
compareType' DType
DArrowT DType
_ = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareType' (DLitT TyLit
t) (DLitT TyLit
s)
| TyLit
t forall a. Eq a => a -> a -> Bool
== TyLit
s = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
| Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareType' (DLitT TyLit
_) DType
_ = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
#if !MIN_VERSION_th_desugar(1,9,0)
compareType' DStarT DStarT = return NonEqual
#endif
compareType' DType
_ DType
_ = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
compareCxt :: DCxt -> DCxt -> Q EqlJudge
compareCxt :: [DType] -> [DType] -> Q EqlJudge
compareCxt [DType]
l [DType]
r = forall a. Monoid a => [a] -> a
mconcat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM DType -> DType -> Q EqlJudge
comparePred [DType]
l [DType]
r
comparePred :: DPred -> DPred -> Q EqlJudge
#if MIN_VERSION_th_desugar(1,10,0)
comparePred :: DType -> DType -> Q EqlJudge
comparePred DType
DWildCardT DType
_ = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
comparePred DType
_ DType
DWildCardT = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
comparePred (DVarT Name
l) (DVarT Name
r)
| Name
l forall a. Eq a => a -> a -> Bool
== Name
r = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
comparePred (DVarT Name
_) DType
_ = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
comparePred DType
_ (DVarT Name
_) = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
comparePred (DSigT DType
l DType
t) (DSigT DType
r DType
s) =
forall a. Semigroup a => a -> a -> a
(<>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> DType -> Q EqlJudge
compareType' DType
t DType
s forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DType -> DType -> Q EqlJudge
comparePred DType
l DType
r
comparePred (DSigT DType
l DType
_) DType
r = DType -> DType -> Q EqlJudge
comparePred DType
l DType
r
comparePred DType
l (DSigT DType
r DType
_) = DType -> DType -> Q EqlJudge
comparePred DType
l DType
r
comparePred (DAppT DType
l1 DType
l2) (DAppT DType
r1 DType
r2) = do
DType
l2' <- forall (q :: * -> *). DsMonad q => DType -> q DType
expandType DType
l2
DType
r2' <- forall (q :: * -> *). DsMonad q => DType -> q DType
expandType DType
r2
forall a. Semigroup a => a -> a -> a
(<>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> DType -> Q EqlJudge
comparePred DType
l1 DType
r1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DType -> DType -> Q EqlJudge
compareType' DType
l2' DType
r2'
comparePred (DAppT DType
_ DType
_) DType
_ = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
comparePred (DConT Name
l) (DConT Name
r)
| Name
l forall a. Eq a => a -> a -> Bool
== Name
r = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Equal
| Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
comparePred (DConT Name
_) DType
_ = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
#if MIN_VERSION_th_desugar(1,12,0)
comparePred (DForallT DForallTelescope
_ DType
_) (DForallT DForallTelescope
_ DType
_) = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
Undecidable
#else
comparePred (DForallT _ _ _) (DForallT _ _ _) = return Undecidable
#endif
comparePred (DForallT{}) DType
_ = forall (m :: * -> *) a. Monad m => a -> m a
return EqlJudge
NonEqual
comparePred DType
_ DType
_ = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Kind error: Expecting type-level predicate"
#else
comparePred DWildCardPr _ = return Undecidable
comparePred _ DWildCardPr = return Undecidable
comparePred (DVarPr l) (DVarPr r)
| l == r = return Equal
comparePred (DVarPr _) _ = return Undecidable
comparePred _ (DVarPr _) = return Undecidable
comparePred (DSigPr l t) (DSigPr r s) =
(<>) <$> compareType' t s <*> comparePred l r
comparePred (DSigPr l _) r = comparePred l r
comparePred l (DSigPr r _) = comparePred l r
comparePred (DAppPr l1 l2) (DAppPr r1 r2) = do
l2' <- expandType l2
r2' <- expandType r2
(<>) <$> comparePred l1 r1 <*> compareType' l2' r2'
comparePred (DAppPr _ _) _ = return NonEqual
comparePred (DConPr l) (DConPr r)
| l == r = return Equal
| otherwise = return NonEqual
comparePred (DConPr _) _ = return NonEqual
#if MIN_VERSION_th_desugar(1,9,0)
comparePred (DForallPr _ _ _) (DForallPr _ _ _) = return Undecidable
comparePred (DForallPr{}) _ = return NonEqual
#endif
#endif
substPred :: SubstDic -> DPred -> Q DPred
#if MIN_VERSION_th_desugar(1,10,0)
substPred :: Map Name DType -> DType -> Q DType
substPred Map Name DType
dic (DAppT DType
p1 DType
p2) = DType -> DType -> DType
DAppT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Name DType -> DType -> Q DType
substPred Map Name DType
dic DType
p1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (q :: * -> *). DsMonad q => DType -> q DType
expandType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (q :: * -> *). Quasi q => Map Name DType -> DType -> q DType
substTy Map Name DType
dic DType
p2)
substPred Map Name DType
dic (DSigT DType
p DType
knd) = DType -> DType -> DType
DSigT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Name DType -> DType -> Q DType
substPred Map Name DType
dic DType
p forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (q :: * -> *). DsMonad q => DType -> q DType
expandType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (q :: * -> *). Quasi q => Map Name DType -> DType -> q DType
substTy Map Name DType
dic DType
knd)
substPred Map Name DType
dic prd :: DType
prd@(DVarT Name
p)
| Just (DVarT Name
t) <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
p Map Name DType
dic = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Name -> DType
DVarT Name
t
| Just (DConT Name
t) <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
p Map Name DType
dic = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Name -> DType
DConT Name
t
| Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return DType
prd
substPred Map Name DType
_ DType
t = forall (m :: * -> *) a. Monad m => a -> m a
return DType
t
#else
substPred dic (DAppPr p1 p2) = DAppPr <$> substPred dic p1 <*> (expandType =<< substTy dic p2)
substPred dic (DSigPr p knd) = DSigPr <$> substPred dic p <*> (expandType =<< substTy dic knd)
substPred dic prd@(DVarPr p)
| Just (DVarT t) <- M.lookup p dic = return $ DVarPr t
| Just (DConT t) <- M.lookup p dic = return $ DConPr t
| otherwise = return prd
substPred _ t = return t
#endif
#if MIN_VERSION_th_desugar(1,12,0)
dtvbToName :: DTyVarBndr flag -> Name
dtvbToName :: forall flag. DTyVarBndr flag -> Name
dtvbToName (DPlainTV Name
n flag
_) = Name
n
dtvbToName (DKindedTV Name
n flag
_ DType
_) = Name
n
#else
dtvbToName :: DTyVarBndr -> Name
dtvbToName (DPlainTV n) = n
dtvbToName (DKindedTV n _) = n
#endif
#if MIN_VERSION_th_desugar(1,12,0)
unTelescope :: DForallTelescope -> [DTyVarBndr ()]
unTelescope :: DForallTelescope -> [DTyVarBndrUnit]
unTelescope (DForallVis [DTyVarBndrUnit]
vis) = forall a b. (a -> b) -> [a] -> [b]
map forall (f :: * -> *) a. Functor f => f a -> f ()
void [DTyVarBndrUnit]
vis
unTelescope (DForallInvis [DTyVarBndrSpec]
vis) = forall a b. (a -> b) -> [a] -> [b]
map forall (f :: * -> *) a. Functor f => f a -> f ()
void [DTyVarBndrSpec]
vis
#endif