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/Theory/Proof.hs                | 43 +++++++++++--------
 11 files changed, 79 insertions(+), 48 deletions(-)

diff --git a/src/Theory/Constraint/Solver/Reduction.hs b/src/Theory/Constraint/Solver/Reduction.hs
index ddbc965a..6daadd0d 100644
--- a/src/Theory/Constraint/Solver/Reduction.hs
+++ b/src/Theory/Constraint/Solver/Reduction.hs
@@ -139,13 +139,14 @@ execReduction m ctxt se fs =
 data ChangeIndicator = Unchanged | Changed
        deriving( Eq, Ord, Show )
 
+instance Semigroup ChangeIndicator where
+    Changed   <> _         = Changed
+    _         <> Changed   = Changed
+    Unchanged <> Unchanged = Unchanged
+
 instance Monoid ChangeIndicator where
     mempty = Unchanged
 
-    Changed   `mappend` _         = Changed
-    _         `mappend` Changed   = Changed
-    Unchanged `mappend` Unchanged = Unchanged
-
 -- | Return 'True' iff there was a change.
 wasChanged :: ChangeIndicator -> Bool
 wasChanged Changed   = True
diff --git a/src/Theory/Constraint/System/Guarded.hs b/src/Theory/Constraint/System/Guarded.hs
index f98fc7c2..2aac8ce2 100644
--- a/src/Theory/Constraint/System/Guarded.hs
+++ b/src/Theory/Constraint/System/Guarded.hs
@@ -435,7 +435,7 @@ gall ss atos gf               = GGuarded All ss atos gf
 
 -- | Local newtype to avoid orphan instance.
 newtype ErrorDoc d = ErrorDoc { unErrorDoc :: d }
-    deriving( Monoid, NFData, Document, HighlightDocument )
+    deriving( Monoid, Semigroup, NFData, Document, HighlightDocument )
 
 -- | @formulaToGuarded fm@ returns a guarded formula @gf@ that is
 -- equivalent to @fm@ under the assumption that this is possible.
diff --git a/src/Theory/Proof.hs b/src/Theory/Proof.hs
index 74fb77b1..7971b9fc 100644
--- a/src/Theory/Proof.hs
+++ b/src/Theory/Proof.hs
@@ -388,17 +388,19 @@ data ProofStatus =
        | TraceFound         -- ^ There is an annotated solved step
     deriving ( Show, Generic, NFData, Binary )
 
+instance Semigroup ProofStatus where
+    TraceFound <> _                        = TraceFound
+    _ <> TraceFound                        = TraceFound
+    IncompleteProof <> _                   = IncompleteProof
+    _ <> IncompleteProof                   = IncompleteProof
+    _ <> CompleteProof                     = CompleteProof
+    CompleteProof <> _                     = CompleteProof
+    UndeterminedProof <> UndeterminedProof = UndeterminedProof
+
+
 instance Monoid ProofStatus where
     mempty = CompleteProof
 
-    mappend TraceFound _                        = TraceFound
-    mappend _ TraceFound                        = TraceFound
-    mappend IncompleteProof _                   = IncompleteProof
-    mappend _ IncompleteProof                   = IncompleteProof
-    mappend _ CompleteProof                     = CompleteProof
-    mappend CompleteProof _                     = CompleteProof
-    mappend UndeterminedProof UndeterminedProof = UndeterminedProof
-
 -- | The status of a 'ProofStep'.
 proofStepStatus :: ProofStep (Maybe a) -> ProofStatus
 proofStepStatus (ProofStep _         Nothing ) = UndeterminedProof
@@ -560,10 +562,12 @@ newtype Prover =  Prover
               -> Maybe IncrementalProof    -- resulting proof
           }
 
+instance Semigroup Prover where
+    p1 <> p2 = Prover $ \ctxt d se ->
+        runProver p1 ctxt d se >=> runProver p2 ctxt d se
+
 instance Monoid Prover where
     mempty          = Prover $ \_  _ _ -> Just
-    p1 `mappend` p2 = Prover $ \ctxt d se ->
-        runProver p1 ctxt d se >=> runProver p2 ctxt d se
 
 -- | Provers whose sequencing is handled via the 'Monoid' instance.
 --
@@ -579,10 +583,12 @@ newtype DiffProver =  DiffProver
               -> Maybe IncrementalDiffProof    -- resulting proof
           }
 
+instance Semigroup DiffProver where
+    p1 <> p2 = DiffProver $ \ctxt d se ->
+        runDiffProver p1 ctxt d se >=> runDiffProver p2 ctxt d se
+
 instance Monoid DiffProver where
     mempty          = DiffProver $ \_  _ _ -> Just
-    p1 `mappend` p2 = DiffProver $ \ctxt d se ->
-        runDiffProver p1 ctxt d se >=> runDiffProver p2 ctxt d se
 
 -- | Map the proof generated by the prover.
 mapProverProof :: (IncrementalProof -> IncrementalProof) -> Prover -> Prover
@@ -784,15 +790,16 @@ runAutoDiffProver (AutoProver heuristic bound cut) =
 -- | The result of one pass of iterative deepening.
 data IterDeepRes = NoSolution | MaybeNoSolution | Solution ProofPath
 
+instance Semigroup IterDeepRes where
+    x@(Solution _)   <> _                = x
+    _                <> y@(Solution _)   = y
+    MaybeNoSolution  <> _                = MaybeNoSolution
+    _                <> MaybeNoSolution  = MaybeNoSolution
+    NoSolution       <> NoSolution       = NoSolution
+
 instance Monoid IterDeepRes where
     mempty = NoSolution
 
-    x@(Solution _)   `mappend` _                = x
-    _                `mappend` y@(Solution _)   = y
-    MaybeNoSolution  `mappend` _                = MaybeNoSolution
-    _                `mappend` MaybeNoSolution  = MaybeNoSolution
-    NoSolution       `mappend` NoSolution       = NoSolution
-
 -- | @cutOnSolvedDFS prf@ removes all other cases if an attack is found. The
 -- attack search is performed using a parallel DFS traversal with iterative
 -- deepening.