diff --git a/Proof/Internal/THCompat.hs b/Proof/Internal/THCompat.hs deleted file mode 100644 --- 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 --- a/Proof/Propositional/TH.hs +++ b/Proof/Propositional/TH.hs @@ -10,7 +10,6 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ (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 @@ 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 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 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 (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 @@ | 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 --- 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-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 @@ 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 @@ , 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