summaryrefslogtreecommitdiff
path: root/Proof/Propositional/TH.hs
diff options
context:
space:
mode:
Diffstat (limited to 'Proof/Propositional/TH.hs')
-rw-r--r--Proof/Propositional/TH.hs81
1 files changed, 68 insertions, 13 deletions
diff --git a/Proof/Propositional/TH.hs b/Proof/Propositional/TH.hs
index 0f7af1c..fb32ecf 100644
--- a/Proof/Propositional/TH.hs
+++ b/Proof/Propositional/TH.hs
@@ -10,7 +10,6 @@ import Data.Foldable (asum)
import Data.Map (Map)
import qualified Data.Map as M
import Data.Maybe (fromJust)
-import Data.Semigroup (Semigroup (..))
import Data.Type.Equality ((:~:) (..))
import Language.Haskell.TH (DecsQ, Lit (CharL, IntegerL),
Name, Q, TypeQ, isInstance,
@@ -19,11 +18,18 @@ import Language.Haskell.TH.Desugar (DClause (..), DCon (..),
DConFields (..), DCxt, DDec (..),
DExp (..), DInfo (..),
DLetDec (DFunD),
- DPat (DConPa, DVarPa), DPred (..),
+#if MIN_VERSION_th_desugar(1,10,0)
+ DPat (DConP, DVarP), DPred,
+#else
+ DPat (DConPa, DVarPa), DPred(..),
+#endif
DTyVarBndr (..), DType (..),
Overlap (Overlapping), desugar,
dsReify, expandType, substTy,
sweeten)
+#if !MIN_VERSION_base(4,13,0)
+import Data.Semigroup (Semigroup (..))
+#endif
-- | Macro to automatically derive @'Empty'@ instance for
-- concrete (variable-free) types which may contain products.
@@ -32,7 +38,11 @@ refute tps = do
tp <- expandType =<< desugar =<< tps
let Just (_, tyName, args) = splitType tp
mkInst dxt cls = return $ sweeten
- [DInstanceD (Just Overlapping) dxt
+ [DInstanceD (Just Overlapping)
+#if MIN_VERSION_th_desugar(1,10,0)
+ Nothing
+#endif
+ dxt
(DAppT (DConT ''Empty) (foldl DAppT (DConT tyName) args))
[DLetDec $ DFunD 'eliminate cls]
]
@@ -58,7 +68,11 @@ prove tps = do
tp <- expandType =<< desugar =<< tps
let Just (_, tyName, args) = splitType tp
mkInst dxt cls = return $ sweeten
- [DInstanceD (Just Overlapping) dxt
+ [DInstanceD (Just Overlapping)
+#if MIN_VERSION_th_desugar(1,10,0)
+ Nothing
+#endif
+ dxt
(DAppT (DConT ''Inhabited) (foldl DAppT (DConT tyName) args))
[DLetDec $ DFunD 'trivial cls]
]
@@ -98,7 +112,11 @@ buildRefuteClause =
buildClause
''Empty (const $ newName "_x")
(const $ (DVarE 'eliminate `DAppE`) . DVarE) (const asum)
+#if 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 =
@@ -109,10 +127,10 @@ buildProveClause =
(const $ const [])
fieldsVars :: DConFields -> [DType]
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 804
-fieldsVars (DNormalC fs)
-#else
+#if MIN_VERSION_th_desugar(1,8,0)
fieldsVars (DNormalC _ fs)
+#else
+fieldsVars (DNormalC fs)
#endif
= map snd fs
fieldsVars (DRecC fs) = map (\(_,_,c) -> c) fs
@@ -148,16 +166,16 @@ substDCon dic (DCon forall'd cxt conName fields mPhantom) =
substFields :: SubstDic -> DConFields -> Q DConFields
substFields subst
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 804
- (DNormalC fs)
-#else
+#if MIN_VERSION_th_desugar(1,8,0)
(DNormalC fixi fs)
+#else
+ (DNormalC fs)
#endif
=
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 804
- DNormalC <$>
-#else
+#if MIN_VERSION_th_desugar(1,8,0)
DNormalC fixi <$>
+#else
+ DNormalC <$>
#endif
mapM (runKleisli $ second $ Kleisli $ substTy subst) fs
substFields subst (DRecC fs) =
@@ -178,6 +196,8 @@ splitType (DLitT _) = Nothing
splitType DWildCardT = Nothing
#if !MIN_VERSION_th_desugar(1,9,0)
splitType DStarT = Nothing
+#elif MIN_VERSION_th_desugar(1,10,0)
+splitType (DAppKindT _ _) = Nothing
#endif
@@ -244,6 +264,30 @@ compareCxt :: DCxt -> DCxt -> Q EqlJudge
compareCxt l r = mconcat <$> zipWithM comparePred l r
comparePred :: DPred -> DPred -> Q EqlJudge
+#if MIN_VERSION_th_desugar(1,10,0)
+comparePred DWildCardT _ = return Undecidable
+comparePred _ DWildCardT = return Undecidable
+comparePred (DVarT l) (DVarT r)
+ | l == r = return Equal
+comparePred (DVarT _) _ = return Undecidable
+comparePred _ (DVarT _) = return Undecidable
+comparePred (DSigT l t) (DSigT r s) =
+ (<>) <$> compareType' t s <*> comparePred l r
+comparePred (DSigT l _) r = comparePred l r
+comparePred l (DSigT r _) = comparePred l r
+comparePred (DAppT l1 l2) (DAppT r1 r2) = do
+ l2' <- expandType l2
+ r2' <- expandType r2
+ (<>) <$> comparePred l1 r1 <*> compareType' l2' r2'
+comparePred (DAppT _ _) _ = return NonEqual
+comparePred (DConT l) (DConT r)
+ | l == r = return Equal
+ | otherwise = return NonEqual
+comparePred (DConT _) _ = return NonEqual
+comparePred (DForallT _ _ _) (DForallT _ _ _) = return Undecidable
+comparePred (DForallT{}) _ = return NonEqual
+comparePred _ _ = fail "Kind error: Expecting type-level predicate"
+#else
comparePred DWildCardPr _ = return Undecidable
comparePred _ DWildCardPr = return Undecidable
comparePred (DVarPr l) (DVarPr r)
@@ -267,8 +311,18 @@ comparePred (DConPr _) _ = return NonEqual
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 dic (DAppT p1 p2) = DAppT <$> substPred dic p1 <*> (expandType =<< substTy dic p2)
+substPred dic (DSigT p knd) = DSigT <$> substPred dic p <*> (expandType =<< substTy dic knd)
+substPred dic prd@(DVarT p)
+ | Just (DVarT t) <- M.lookup p dic = return $ DVarT t
+ | Just (DConT t) <- M.lookup p dic = return $ DConT t
+ | otherwise = return prd
+substPred _ t = return 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)
@@ -276,6 +330,7 @@ substPred dic prd@(DVarPr p)
| Just (DConT t) <- M.lookup p dic = return $ DConPr t
| otherwise = return prd
substPred _ t = return t
+#endif