2cfc0bb7ee
See https://hydra.nixos.org/build/81125645
`tamarin-prover' upstream has a patch to fix GHC 8.4 compilation (and
uses stack lts-12.1 now), but it's not released yet:
a08f6e4007
The build is divided in several derivations, therefore the patch had to
be splitted and rebased for `lib/term', `lib/theory' and `lib/utils' to
ensure that the patch applies properly during the `patchPhase'.
Addresses #45960
140 lines
5.2 KiB
Diff
140 lines
5.2 KiB
Diff
From a08f6e400772899b9b0fc16befc50391cd70696b Mon Sep 17 00:00:00 2001
|
|
From: Felix Yan <felixonmars@archlinux.org>
|
|
Date: Fri, 18 May 2018 16:24:41 +0800
|
|
Subject: [PATCH] GHC 8.4 support
|
|
|
|
---
|
|
src/Extension/Data/Bounded.hs | 10 ++++-
|
|
src/Extension/Data/Monoid.hs | 14 +++---
|
|
src/Logic/Connectives.hs | 4 +-
|
|
src/Text/PrettyPrint/Class.hs | 4 +-
|
|
src/Text/PrettyPrint/Html.hs | 6 ++-
|
|
11 files changed, 79 insertions(+), 48 deletions(-)
|
|
|
|
|
|
diff --git a/src/Extension/Data/Bounded.hs b/src/Extension/Data/Bounded.hs
|
|
index 5f166006..f416a44c 100644
|
|
--- a/src/Extension/Data/Bounded.hs
|
|
+++ b/src/Extension/Data/Bounded.hs
|
|
@@ -11,19 +11,25 @@ module Extension.Data.Bounded (
|
|
) where
|
|
|
|
-- import Data.Monoid
|
|
+import Data.Semigroup
|
|
|
|
-- | A newtype wrapper for a monoid of the maximum of a bounded type.
|
|
newtype BoundedMax a = BoundedMax {getBoundedMax :: a}
|
|
deriving( Eq, Ord, Show )
|
|
|
|
+instance (Ord a, Bounded a) => Semigroup (BoundedMax a) where
|
|
+ BoundedMax x <> BoundedMax y = BoundedMax (max x y)
|
|
+
|
|
instance (Ord a, Bounded a) => Monoid (BoundedMax a) where
|
|
mempty = BoundedMax minBound
|
|
- (BoundedMax x) `mappend` (BoundedMax y) = BoundedMax (max x y)
|
|
+ mappend = (<>)
|
|
|
|
-- | A newtype wrapper for a monoid of the minimum of a bounded type.
|
|
newtype BoundedMin a = BoundedMin {getBoundedMin :: a}
|
|
deriving( Eq, Ord, Show )
|
|
|
|
+instance (Ord a, Bounded a) => Semigroup (BoundedMin a) where
|
|
+ BoundedMin x <> BoundedMin y = BoundedMin (min x y)
|
|
+
|
|
instance (Ord a, Bounded a) => Monoid (BoundedMin a) where
|
|
mempty = BoundedMin maxBound
|
|
- (BoundedMin x) `mappend` (BoundedMin y) = BoundedMin (min x y)
|
|
\ No newline at end of file
|
|
diff --git a/src/Extension/Data/Monoid.hs b/src/Extension/Data/Monoid.hs
|
|
index 83655c34..9ce2f91b 100644
|
|
--- a/src/Extension/Data/Monoid.hs
|
|
+++ b/src/Extension/Data/Monoid.hs
|
|
@@ -18,6 +18,7 @@ module Extension.Data.Monoid (
|
|
) where
|
|
|
|
import Data.Monoid
|
|
+import Data.Semigroup
|
|
|
|
#if __GLASGOW_HASKELL__ < 704
|
|
|
|
@@ -38,10 +39,13 @@ newtype MinMax a = MinMax { getMinMax :: Maybe (a, a) }
|
|
minMaxSingleton :: a -> MinMax a
|
|
minMaxSingleton x = MinMax (Just (x, x))
|
|
|
|
+instance Ord a => Semigroup (MinMax a) where
|
|
+ MinMax Nothing <> y = y
|
|
+ x <> MinMax Nothing = x
|
|
+ MinMax (Just (xMin, xMax)) <> MinMax (Just (yMin, yMax)) =
|
|
+ MinMax (Just (min xMin yMin, max xMax yMax))
|
|
+
|
|
+
|
|
instance Ord a => Monoid (MinMax a) where
|
|
mempty = MinMax Nothing
|
|
-
|
|
- MinMax Nothing `mappend` y = y
|
|
- x `mappend` MinMax Nothing = x
|
|
- MinMax (Just (xMin, xMax)) `mappend` MinMax (Just (yMin, yMax)) =
|
|
- MinMax (Just (min xMin yMin, max xMax yMax))
|
|
+ mappend = (<>)
|
|
diff --git a/src/Logic/Connectives.hs b/src/Logic/Connectives.hs
|
|
index 2e441172..7206cc2c 100644
|
|
--- a/src/Logic/Connectives.hs
|
|
+++ b/src/Logic/Connectives.hs
|
|
@@ -23,12 +23,12 @@ import Control.DeepSeq
|
|
|
|
-- | A conjunction of atoms of type a.
|
|
newtype Conj a = Conj { getConj :: [a] }
|
|
- deriving (Monoid, Foldable, Traversable, Eq, Ord, Show, Binary,
|
|
+ deriving (Monoid, Semigroup, Foldable, Traversable, Eq, Ord, Show, Binary,
|
|
Functor, Applicative, Monad, Alternative, MonadPlus, Typeable, Data, NFData)
|
|
|
|
-- | A disjunction of atoms of type a.
|
|
newtype Disj a = Disj { getDisj :: [a] }
|
|
- deriving (Monoid, Foldable, Traversable, Eq, Ord, Show, Binary,
|
|
+ deriving (Monoid, Semigroup, Foldable, Traversable, Eq, Ord, Show, Binary,
|
|
Functor, Applicative, Monad, Alternative, MonadPlus, Typeable, Data, NFData)
|
|
|
|
instance MonadDisj Disj where
|
|
diff --git a/src/Text/PrettyPrint/Class.hs b/src/Text/PrettyPrint/Class.hs
|
|
index f5eb42fe..13be6515 100644
|
|
--- a/src/Text/PrettyPrint/Class.hs
|
|
+++ b/src/Text/PrettyPrint/Class.hs
|
|
@@ -187,9 +187,11 @@ instance Document Doc where
|
|
nest i (Doc d) = Doc $ P.nest i d
|
|
caseEmptyDoc yes no (Doc d) = if P.isEmpty d then yes else no
|
|
|
|
+instance Semigroup Doc where
|
|
+ Doc d1 <> Doc d2 = Doc $ (P.<>) d1 d2
|
|
+
|
|
instance Monoid Doc where
|
|
mempty = Doc $ P.empty
|
|
- mappend (Doc d1) (Doc d2) = Doc $ (P.<>) d1 d2
|
|
|
|
------------------------------------------------------------------------------
|
|
-- Additional combinators
|
|
diff --git a/src/Text/PrettyPrint/Html.hs b/src/Text/PrettyPrint/Html.hs
|
|
index 3de5e307..10103eb7 100644
|
|
--- a/src/Text/PrettyPrint/Html.hs
|
|
+++ b/src/Text/PrettyPrint/Html.hs
|
|
@@ -90,7 +90,7 @@ attribute (key,value) = " " ++ key ++ "=\"" ++ escapeHtmlEntities value ++ "\""
|
|
|
|
-- | A 'Document' transformer that adds proper HTML escaping.
|
|
newtype HtmlDoc d = HtmlDoc { getHtmlDoc :: d }
|
|
- deriving( Monoid )
|
|
+ deriving( Monoid, Semigroup )
|
|
|
|
-- | Wrap a document such that HTML markup can be added without disturbing the
|
|
-- layout.
|
|
@@ -182,9 +182,11 @@ getNoHtmlDoc = runIdentity . unNoHtmlDoc
|
|
instance NFData d => NFData (NoHtmlDoc d) where
|
|
rnf = rnf . getNoHtmlDoc
|
|
|
|
+instance Semigroup d => Semigroup (NoHtmlDoc d) where
|
|
+ (<>) = liftA2 (<>)
|
|
+
|
|
instance Monoid d => Monoid (NoHtmlDoc d) where
|
|
mempty = pure mempty
|
|
- mappend = liftA2 mappend
|
|
|
|
instance Document d => Document (NoHtmlDoc d) where
|
|
char = pure . char
|