summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHiromiIshii <>2019-01-04 05:10:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2019-01-04 05:10:00 (GMT)
commit06416ee45e4b7158de91fb678af1ba2d10c759b0 (patch)
tree1d8c0ff21f42b92c00a4aafee968462cb2538d1b
parent81eb66ddf2473b3a3b64d9a3dae228b0a849c988 (diff)
version 0.5.1.10.5.1.1
-rw-r--r--Proof/Equational.hs2
-rw-r--r--Proof/Propositional.hs6
-rw-r--r--Proof/Propositional/TH.hs20
-rw-r--r--equational-reasoning.cabal73
4 files changed, 55 insertions, 46 deletions
diff --git a/Proof/Equational.hs b/Proof/Equational.hs
index 8063dd9..00468e4 100644
--- a/Proof/Equational.hs
+++ b/Proof/Equational.hs
@@ -157,7 +157,7 @@ coerce' _ a = unsafeCoerce a
withRefl :: forall a b r. a :~: b -> (a ~ b => r) -> r
withRefl _ r = case unsafeCoerce (Refl :: () :~: ()) :: a :~: b of
Refl -> r
-{-# INLINE [1] withRefl #-}
+{-# NOINLINE withRefl #-}
{-# RULES
"withRefl/unsafeCoerce" [~1] forall x.
withRefl x = unsafeCoerce
diff --git a/Proof/Propositional.hs b/Proof/Propositional.hs
index 36c3b06..dc41ddc 100644
--- a/Proof/Propositional.hs
+++ b/Proof/Propositional.hs
@@ -1,7 +1,7 @@
{-# LANGUAGE DataKinds, DeriveDataTypeable, EmptyCase, ExplicitForAll #-}
{-# LANGUAGE ExplicitNamespaces, FlexibleInstances, GADTs, KindSignatures #-}
-{-# LANGUAGE LambdaCase, PolyKinds, StandaloneDeriving, TemplateHaskell #-}
-{-# LANGUAGE TypeOperators, RankNTypes #-}
+{-# LANGUAGE LambdaCase, PolyKinds, RankNTypes, StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell, TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Provides type synonyms for logical connectives.
module Proof.Propositional
@@ -76,7 +76,7 @@ data IsTrue (b :: Bool) where
withWitness :: IsTrue b -> (b ~ 'True => r) -> r
withWitness Witness r = r
-{-# INLINE [1] withWitness #-}
+{-# NOINLINE withWitness #-}
{-# RULES
"withWitness/coercion" [~1] forall x.
withWitness x = unsafeCoerce
diff --git a/Proof/Propositional/TH.hs b/Proof/Propositional/TH.hs
index 74a689d..0f7af1c 100644
--- a/Proof/Propositional/TH.hs
+++ b/Proof/Propositional/TH.hs
@@ -25,7 +25,6 @@ import Language.Haskell.TH.Desugar (DClause (..), DCon (..),
dsReify, expandType, substTy,
sweeten)
-
-- | Macro to automatically derive @'Empty'@ instance for
-- concrete (variable-free) types which may contain products.
refute :: TypeQ -> DecsQ
@@ -121,7 +120,11 @@ fieldsVars (DRecC fs) = map (\(_,_,c) -> c) fs
resolveSubsts :: [DType] -> DInfo -> Q (DCxt, [DCon])
resolveSubsts args info =
case info of
- (DTyConI (DDataD _ cxt _ tvbs dcons _) _) -> do
+ (DTyConI (DDataD _ cxt _ tvbs
+#if MIN_VERSION_th_desugar(1,9,0)
+ _
+#endif
+ dcons _) _) -> do
let dic = M.fromList $ zip (map dtvbToName tvbs) args
(cxt , ) <$> mapM (substDCon dic) dcons
-- (DTyConI (DOpenTypeFamilyD n) _) -> return []
@@ -137,7 +140,11 @@ substDCon :: SubstDic -> DCon -> Q DCon
substDCon dic (DCon forall'd cxt conName fields mPhantom) =
DCon forall'd cxt conName
<$> substFields dic fields
+#if MIN_VERSION_th_desugar(1,9,0)
+ <*> substTy dic mPhantom
+#else
<*> mapM (substTy dic) mPhantom
+#endif
substFields :: SubstDic -> DConFields -> Q DConFields
substFields subst
@@ -169,7 +176,10 @@ splitType (DConT n) = Just ([], n, [])
splitType DArrowT = Just ([], ''(->), [])
splitType (DLitT _) = Nothing
splitType DWildCardT = Nothing
+#if !MIN_VERSION_th_desugar(1,9,0)
splitType DStarT = Nothing
+#endif
+
data EqlJudge = NonEqual | Undecidable | Equal
deriving (Read, Show, Eq, Ord)
@@ -225,7 +235,9 @@ compareType' (DLitT t) (DLitT s)
| t == s = return Equal
| otherwise = return NonEqual
compareType' (DLitT _) _ = return NonEqual
+#if !MIN_VERSION_th_desugar(1,9,0)
compareType' DStarT DStarT = return NonEqual
+#endif
compareType' _ _ = return NonEqual
compareCxt :: DCxt -> DCxt -> Q EqlJudge
@@ -251,6 +263,10 @@ comparePred (DConPr l) (DConPr r)
| l == r = return Equal
| otherwise = return NonEqual
comparePred (DConPr _) _ = return NonEqual
+#if MIN_VERSION_th_desugar(1,9,0)
+comparePred (DForallPr _ _ _) (DForallPr _ _ _) = return Undecidable
+comparePred (DForallPr{}) _ = return NonEqual
+#endif
substPred :: SubstDic -> DPred -> Q DPred
substPred dic (DAppPr p1 p2) = DAppPr <$> substPred dic p1 <*> (expandType =<< substTy dic p2)
diff --git a/equational-reasoning.cabal b/equational-reasoning.cabal
index c3639bf..6b0f2fa 100644
--- a/equational-reasoning.cabal
+++ b/equational-reasoning.cabal
@@ -1,46 +1,39 @@
-name: equational-reasoning
-version: 0.5.1.0
-cabal-version: >=1.8
-build-type: Simple
-license: BSD3
-license-file: LICENSE
-copyright: (c) Hiromi ISHII 2013-2018
-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 ==8.0.2 GHC ==8.2.2 GHC ==8.4.1
+-- Initial equational-reasoning.cabal generated by cabal init. For further
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name: equational-reasoning
+version: 0.5.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-2018
+category: Math
+build-type: Simple
+tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.1, GHC == 8.6.3
+cabal-version: >=1.8
source-repository head
type: git
location: git://github.com/konn/equational-reasoning-in-haskell.git
library
-
- if impl(ghc >=8.4)
- build-depends:
- th-desugar ==1.8.*
- else
- build-depends:
- semigroups ==0.18.*,
- th-desugar >=1.6 && <1.8
- 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 && <2.14,
- th-extras ==0.0.*,
- void >=0.6 && <0.8,
- singletons >=2.1 && <2.5
- other-modules:
- Proof.Internal.THCompat
- Proof.Propositional.TH
- ghc-options: -Wall
-
+ 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 && < 0.7
+ , template-haskell >= 2.11 && < 2.16
+ , th-extras == 0.0.*
+ , void >= 0.6 && < 0.8
+ , singletons >= 2.1 && < 2.6
+ if impl(ghc >= 8.4)
+ build-depends: th-desugar >= 1.6 && < 1.11
+ else
+ build-depends: semigroups == 0.18.*
+ build-depends: th-desugar >= 1.6 && < 1.11