1 files changed, 0 insertions, 130 deletions
diff --git a/nixpkgs/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-theory.patch b/nixpkgs/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-theory.patch
deleted file mode 100644
index f7393e37f1b2..000000000000
--- a/nixpkgs/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-theory.patch
+++ /dev/null
@@ -1,130 +0,0 @@
-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.