equational-reasoning 0.4.1.1 → 0.5.0.0
raw patch · 3 files changed
+93/−41 lines, 3 filesdep +th-extrasdep ~singletonsdep ~template-haskellPVP ok
version bump matches the API change (PVP)
Dependencies added: th-extras
Dependency ranges changed: singletons, template-haskell
API changes (from Hackage documentation)
Files
- Proof/Internal/THCompat.hs +51/−10
- Proof/Propositional/Inhabited.hs +9/−3
- equational-reasoning.cabal +33/−28
Proof/Internal/THCompat.hs view
@@ -1,17 +1,45 @@ {-# 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) -mkDataD :: Cxt -> Name -> [TyVarBndr] -> [Con] -> [Name] -> Dec-mkDataD ctx name tvbndrs cons names =+#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 (map ConT names)+ Nothing cons +#if __GLASGOW_HASKELL__ < 802+ (concatMap dcToCxt dc) #else- cons names+ dc #endif+#else+ cons (concatMap dcToNames dc)+#endif typeName :: Type -> Name@@ -29,18 +57,31 @@ typeName ConstraintT = ''Constraint typeName _ = error "No names!" -pattern DataDCompat ctx name tvbndrs cons 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 (map typeName -> names)+ _ cons +#if __GLASGOW_HASKELL__ < 802+ (pure . DerivClause Nothing -> dcs)+#else + dcs+#endif #else- cons names+ cons (DerivClause Nothing . map ConT -> dc) #endif -pattern NewtypeDCompat ctx name tvbndrs con names <-+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 (map typeName -> names)+ _ con+#if __GLASGOW_HASKELL__ < 802+ (pure . DerivClause Nothing -> dcs) #else- con names+ dcs+#endif+#else+ con+ (DerivClause Nothing . map ConT -> dcs) #endif
Proof/Propositional/Inhabited.hs view
@@ -8,15 +8,21 @@ import Unsafe.Coerce (unsafeCoerce) -- | Types with at least one inhabitant, dual to @'Proof.Propositional.Empty'@.--- | Current GHC doesn't provide selective-instance,--- hence we don't @'Empty'@ provide instances--- for sum types in a generic deriving (DeriveAnyClass).+-- Currently, GHC doesn't provide a selective-instance,+-- hence we can't generically derive @'Inhabited'@ instances+-- for sum types (i.e. by @DeriveAnyClass@). -- -- To derive an instance for each concrete types, -- use @'Proof.Propositional.prove'@. -- -- Since 0.4.0.0. class Inhabited a where+ -- | A /generic/ inhabitant of type @'a'@, which means that+ -- one cannot assume anything about the value of @'trivial'@+ -- except that it+ --+ -- * is of type @a@, and+ -- * doesn't contain any partial values. trivial :: a default trivial :: (Generic a, GInhabited (Rep a)) => a
equational-reasoning.cabal view
@@ -1,34 +1,39 @@--- Initial equational-reasoning.cabal generated by cabal init. For further--- documentation, see http://haskell.org/cabal/users-guide/--name: equational-reasoning-version: 0.4.1.1-synopsis: Proof assistant for Haskell using DataKinds & PolyKinds-description: A simple convenient library to write equational / preorder proof as in Agda.-license: BSD3-license-file: LICENSE-author: Hiromi ISHII-maintainer: konn.jinro_at_gmail.com-copyright: (c) Hiromi ISHII 2013-2014-category: Math-build-type: Simple-tested-with: GHC == 7.10.3, GHC == 8.0.1-cabal-version: >=1.8+name: equational-reasoning+version: 0.5.0.0+cabal-version: >=1.8+build-type: Simple+license: BSD3+license-file: LICENSE+copyright: (c) Hiromi ISHII 2013-2014+maintainer: konn.jinro_at_gmail.com+synopsis: Proof assistant for Haskell using DataKinds & PolyKinds+description:+ A simple convenient library to write equational / preorder proof as in Agda.+category: Math+author: Hiromi ISHII+tested-with: GHC ==7.10.3 GHC ==8.0.1 source-repository head type: git location: git://github.com/konn/equational-reasoning-in-haskell.git library- exposed-modules: Proof.Equational, Proof.Propositional, Proof.Induction- , Proof.Propositional.Inhabited- , Proof.Propositional.Empty- other-modules: Proof.Internal.THCompat- , Proof.Propositional.TH- ghc-options: -Wall- build-depends: base >= 4 && < 5- , containers >= 0.5- , template-haskell- , th-desugar >= 1.6- , void >= 0.6 && < 0.8- build-depends: singletons >= 2.1 && < 2.3+ exposed-modules:+ Proof.Equational+ Proof.Propositional+ Proof.Induction+ Proof.Propositional.Inhabited+ Proof.Propositional.Empty+ build-depends:+ base ==4.*,+ containers >=0.5,+ template-haskell >=2.11.1.0,+ th-desugar >=1.6,+ th-extras >=0.0.0.4,+ void >=0.6 && <0.8,+ singletons >=2.1 && <2.4+ other-modules:+ Proof.Internal.THCompat+ Proof.Propositional.TH+ ghc-options: -Wall+