equational-reasoning 0.6.0.0 → 0.6.0.1
raw patch · 3 files changed
+74/−107 lines, 3 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- Proof/Internal/THCompat.hs +0/−87
- Proof/Propositional/TH.hs +68/−13
- equational-reasoning.cabal +6/−7
− Proof/Internal/THCompat.hs
@@ -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
Proof/Propositional/TH.hs view
@@ -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
equational-reasoning.cabal view
@@ -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