summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Proof/Internal/THCompat.hs87
-rw-r--r--Proof/Propositional/TH.hs81
-rw-r--r--equational-reasoning.cabal13
3 files changed, 74 insertions, 107 deletions
diff --git a/Proof/Internal/THCompat.hs b/Proof/Internal/THCompat.hs
deleted file mode 100644
index 61d5930..0000000
--- a/Proof/Internal/THCompat.hs
+++ /dev/null
@@ -1,87 +0,0 @@
-{-# LANGUAGE CPP, PatternSynonyms, TemplateHaskell, ViewPatterns #-}
-{-# LANGUAGE DeriveDataTypeable, DeriveGeneric #-}
-module Proof.Internal.THCompat where
-import Language.Haskell.TH
-import Language.Haskell.TH.Extras
-
-import GHC.Exts (Constraint)
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 802
-import GHC.Generics
-import Data.Data
-#endif
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 802
-data DerivClause = DerivClause (Maybe DerivStrategy) Cxt
- deriving (Eq, Data, Ord, Show, Generic)
-data DerivStrategy = StockStrategy
- | AnyclassStrategy
- | NewtypeStrategy
- deriving (Eq, Data, Ord, Show, Generic)
-#endif
-
-dcToNames :: DerivClause -> [Name]
-dcToNames (DerivClause _ ct) = map headOfType ct
-
-dcToCxt :: DerivClause -> Cxt
-dcToCxt (DerivClause _ ct) = ct
-
-
-mkDataD :: Cxt -> Name -> [TyVarBndr] -> [Con] -> [DerivClause] -> Dec
-mkDataD ctx name tvbndrs cons dc =
- DataD ctx name tvbndrs
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
- Nothing cons
-#if __GLASGOW_HASKELL__ < 802
- (concatMap dcToCxt dc)
-#else
- dc
-#endif
-#else
- cons (concatMap dcToNames dc)
-#endif
-
-
-typeName :: Type -> Name
-typeName (VarT n) = n
-typeName (ConT n) = n
-typeName (PromotedT n) = n
-typeName (TupleT n) = tupleTypeName n
-typeName (UnboxedTupleT n) = unboxedTupleTypeName n
-typeName ArrowT = ''(->)
-typeName EqualityT = ''(~)
-typeName ListT = ''[]
-typeName (PromotedTupleT n) = tupleDataName n
-typeName PromotedNilT = '[]
-typeName PromotedConsT = '(:)
-typeName ConstraintT = ''Constraint
-typeName _ = error "No names!"
-
-pattern DataDCompat :: Cxt -> Name -> [TyVarBndr] -> [Con] -> [DerivClause] -> Dec
-pattern DataDCompat ctx name tvbndrs cons dcs <-
- DataD ctx name tvbndrs
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
- _ cons
-#if __GLASGOW_HASKELL__ < 802
- (pure . DerivClause Nothing -> dcs)
-#else
- dcs
-#endif
-#else
- cons (DerivClause Nothing . map ConT -> dc)
-#endif
-
-pattern NewtypeDCompat :: Cxt -> Name -> [TyVarBndr] -> Con -> [DerivClause] -> Dec
-pattern NewtypeDCompat ctx name tvbndrs con dcs <-
- NewtypeD ctx name tvbndrs
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
- _ con
-#if __GLASGOW_HASKELL__ < 802
- (pure . DerivClause Nothing -> dcs)
-#else
- dcs
-#endif
-#else
- con
- (DerivClause Nothing . map ConT -> dcs)
-#endif
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
diff --git a/equational-reasoning.cabal b/equational-reasoning.cabal
index 30fbe33..e5d4c6e 100644
--- a/equational-reasoning.cabal
+++ b/equational-reasoning.cabal
@@ -2,7 +2,7 @@
-- documentation, see http://haskell.org/cabal/users-guide/
name: equational-reasoning
-version: 0.6.0.0
+version: 0.6.0.1
synopsis: Proof assistant for Haskell using DataKinds & PolyKinds
description: A simple convenient library to write equational / preorder proof as in Agda.
Since 0.6.0.0, this no longer depends on @singletons@ package, and the @Proof.Induction@ module goes to @equational-reasoning-induction@ package.
@@ -10,10 +10,10 @@ license: BSD3
license-file: LICENSE
author: Hiromi ISHII
maintainer: konn.jinro_at_gmail.com
-copyright: (c) Hiromi ISHII 2013-2018
+copyright: (c) Hiromi ISHII 2013-2020
category: Math
build-type: Simple
-tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.1, GHC == 8.6.3
+tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.1, GHC == 8.6.5, GHC == 8.8.2
cabal-version: >=1.8
source-repository head
@@ -24,8 +24,7 @@ library
exposed-modules: Proof.Equational, Proof.Propositional
, Proof.Propositional.Inhabited
, Proof.Propositional.Empty
- other-modules: Proof.Internal.THCompat
- , Proof.Propositional.TH
+ other-modules: Proof.Propositional.TH
ghc-options: -Wall
build-depends: base >= 4 && < 5
, containers >= 0.5 && < 0.7
@@ -33,7 +32,7 @@ library
, th-extras == 0.0.*
, void >= 0.6 && < 0.8
if impl(ghc >= 8.4)
- build-depends: th-desugar >= 1.6 && < 1.11
+ build-depends: th-desugar >= 1.8 && < 1.11
else
build-depends: semigroups == 0.18.*
- build-depends: th-desugar >= 1.6 && < 1.11
+ build-depends: th-desugar >= 1.6 && < 1.8