diff --git a/Proof/Internal/THCompat.hs b/Proof/Internal/THCompat.hs --- a/Proof/Internal/THCompat.hs +++ b/Proof/Internal/THCompat.hs @@ -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 diff --git a/Proof/Propositional/Inhabited.hs b/Proof/Propositional/Inhabited.hs --- a/Proof/Propositional/Inhabited.hs +++ b/Proof/Propositional/Inhabited.hs @@ -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 diff --git a/equational-reasoning.cabal b/equational-reasoning.cabal --- a/equational-reasoning.cabal +++ b/equational-reasoning.cabal @@ -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 +