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
110 lines
4.2 KiB
Diff
110 lines
4.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/Term/Maude/Signature.hs | 8 ++--
|
|
src/Term/Rewriting/Definitions.hs | 23 ++++++----
|
|
src/Term/Unification.hs | 4 +-
|
|
11 files changed, 79 insertions(+), 48 deletions(-)
|
|
|
|
diff --git a/src/Term/Maude/Signature.hs b/src/Term/Maude/Signature.hs
|
|
index 98c25d9f..1a4ce82f 100644
|
|
--- a/src/Term/Maude/Signature.hs
|
|
+++ b/src/Term/Maude/Signature.hs
|
|
@@ -104,9 +104,9 @@ maudeSig msig@(MaudeSig {enableDH,enableBP,enableMSet,enableXor,enableDiff=_,stF
|
|
`S.union` dhReducibleFunSig `S.union` bpReducibleFunSig `S.union` xorReducibleFunSig
|
|
|
|
-- | A monoid instance to combine maude signatures.
|
|
-instance Monoid MaudeSig where
|
|
- (MaudeSig dh1 bp1 mset1 xor1 diff1 stFunSyms1 stRules1 _ _) `mappend`
|
|
- (MaudeSig dh2 bp2 mset2 xor2 diff2 stFunSyms2 stRules2 _ _) =
|
|
+instance Semigroup MaudeSig where
|
|
+ MaudeSig dh1 bp1 mset1 xor1 diff1 stFunSyms1 stRules1 _ _ <>
|
|
+ MaudeSig dh2 bp2 mset2 xor2 diff2 stFunSyms2 stRules2 _ _ =
|
|
maudeSig (mempty {enableDH=dh1||dh2
|
|
,enableBP=bp1||bp2
|
|
,enableMSet=mset1||mset2
|
|
@@ -114,6 +114,8 @@ instance Monoid MaudeSig where
|
|
,enableDiff=diff1||diff2
|
|
,stFunSyms=S.union stFunSyms1 stFunSyms2
|
|
,stRules=S.union stRules1 stRules2})
|
|
+
|
|
+instance Monoid MaudeSig where
|
|
mempty = MaudeSig False False False False False S.empty S.empty S.empty S.empty
|
|
|
|
-- | Non-AC function symbols.
|
|
diff --git a/src/Term/Rewriting/Definitions.hs b/src/Term/Rewriting/Definitions.hs
|
|
index bd942b6a..18562e4e 100644
|
|
--- a/src/Term/Rewriting/Definitions.hs
|
|
+++ b/src/Term/Rewriting/Definitions.hs
|
|
@@ -44,10 +44,12 @@ evalEqual (Equal l r) = l == r
|
|
instance Functor Equal where
|
|
fmap f (Equal lhs rhs) = Equal (f lhs) (f rhs)
|
|
|
|
+instance Semigroup a => Semigroup (Equal a) where
|
|
+ (Equal l1 r1) <> (Equal l2 r2) =
|
|
+ Equal (l1 <> l2) (r1 <> r2)
|
|
+
|
|
instance Monoid a => Monoid (Equal a) where
|
|
mempty = Equal mempty mempty
|
|
- (Equal l1 r1) `mappend` (Equal l2 r2) =
|
|
- Equal (l1 `mappend` l2) (r1 `mappend` r2)
|
|
|
|
instance Foldable Equal where
|
|
foldMap f (Equal l r) = f l `mappend` f r
|
|
@@ -104,14 +106,15 @@ instance Functor Match where
|
|
fmap _ NoMatch = NoMatch
|
|
fmap f (DelayedMatches ms) = DelayedMatches (fmap (f *** f) ms)
|
|
|
|
+instance Semigroup (Match a) where
|
|
+ NoMatch <> _ = NoMatch
|
|
+ _ <> NoMatch = NoMatch
|
|
+ DelayedMatches ms1 <> DelayedMatches ms2 =
|
|
+ DelayedMatches (ms1 <> ms2)
|
|
+
|
|
instance Monoid (Match a) where
|
|
mempty = DelayedMatches []
|
|
|
|
- NoMatch `mappend` _ = NoMatch
|
|
- _ `mappend` NoMatch = NoMatch
|
|
- DelayedMatches ms1 `mappend` DelayedMatches ms2 =
|
|
- DelayedMatches (ms1 `mappend` ms2)
|
|
-
|
|
|
|
instance Foldable Match where
|
|
foldMap _ NoMatch = mempty
|
|
@@ -136,10 +139,12 @@ data RRule a = RRule a a
|
|
instance Functor RRule where
|
|
fmap f (RRule lhs rhs) = RRule (f lhs) (f rhs)
|
|
|
|
+instance Monoid a => Semigroup (RRule a) where
|
|
+ (RRule l1 r1) <> (RRule l2 r2) =
|
|
+ RRule (l1 <> l2) (r1 <> r2)
|
|
+
|
|
instance Monoid a => Monoid (RRule a) where
|
|
mempty = RRule mempty mempty
|
|
- (RRule l1 r1) `mappend` (RRule l2 r2) =
|
|
- RRule (l1 `mappend` l2) (r1 `mappend` r2)
|
|
|
|
instance Foldable RRule where
|
|
foldMap f (RRule l r) = f l `mappend` f r
|
|
diff --git a/src/Term/Unification.hs b/src/Term/Unification.hs
|
|
index e1de0163..7ce6bb41 100644
|
|
--- a/src/Term/Unification.hs
|
|
+++ b/src/Term/Unification.hs
|
|
@@ -265,9 +265,11 @@ unifyRaw l0 r0 = do
|
|
|
|
data MatchFailure = NoMatcher | ACProblem
|
|
|
|
+instance Semigroup MatchFailure where
|
|
+ _ <> _ = NoMatcher
|
|
+
|
|
instance Monoid MatchFailure where
|
|
mempty = NoMatcher
|
|
- mappend _ _ = NoMatcher
|
|
|
|
-- | Ensure that the computed substitution @sigma@ satisfies
|
|
-- @t ==_AC apply sigma p@ after the delayed equations are solved.
|