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
131 lines
5.3 KiB
Diff
131 lines
5.3 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/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.
|