depot/third_party/nixpkgs/pkgs/applications/science/logic/tamarin-prover/tamarin-prover-1.8.0-ghc-9.6.patch

commit 084bd5474d9ac687656c2a3a6b2e1d507febaa98
Author: Artur Cygan <arczicygan@gmail.com>
Date:   Mon Feb 26 10:04:48 2024 +0100

    Update to GHC 9.6 (#618)
    
    Cherry-picked from b3e18f61e45d701d42d794bc91ccbb4c0e3834ec.
    
    Removing Control.Monad.List

diff --git a/lib/sapic/src/Sapic/Exceptions.hs b/lib/sapic/src/Sapic/Exceptions.hs
index 146b721e..b9962478 100644
--- a/lib/sapic/src/Sapic/Exceptions.hs
+++ b/lib/sapic/src/Sapic/Exceptions.hs
@@ -23,7 +23,6 @@ import Theory.Sapic
 import Data.Label
 import qualified Data.Maybe
 import Theory.Text.Pretty
-import Sapic.Annotation  --toAnProcess
 import Theory.Sapic.Print (prettySapic)
 import qualified Theory.Text.Pretty as Pretty
 
@@ -67,14 +66,14 @@ data ExportException = UnsupportedBuiltinMS
                        | UnsupportedTypes [String]
 
 instance Show ExportException where
-    
+
     show (UnsupportedTypes incorrectFunctionUsages) = do
         let functionsString = List.intercalate ", " incorrectFunctionUsages
         (case length functionsString of
           1 -> "The function " ++ functionsString ++ ", which is declared with a user-defined type, appears in a rewrite rule. "
           _ -> "The functions " ++ functionsString ++ ", which are declared with a user-defined type, appear in a rewrite rule. ")
         ++ "However, the translation of rules only works with bitstrings at the moment."
-    show unsuppBuiltin = 
+    show unsuppBuiltin =
         "The builtins bilinear-pairing and multiset are not supported for export. However, your model uses " ++
         (case unsuppBuiltin of
             UnsupportedBuiltinBP -> "bilinear-pairing."
@@ -93,7 +92,7 @@ instance Show (SapicException an) where
     show (InvalidPosition p) = "Invalid position:" ++ prettyPosition p
     show (NotImplementedError s) = "This feature is not implemented yet. Sorry! " ++ s
     show (ImplementationError s) = "You've encountered an error in the implementation: " ++ s
-    show a@(ProcessNotWellformed e p) = "Process not well-formed: " ++ Pretty.render (text (show e) $-$ nest 2 (maybe emptyDoc prettySapic p))
+    show (ProcessNotWellformed e p) = "Process not well-formed: " ++ Pretty.render (text (show e) $-$ nest 2 (maybe emptyDoc prettySapic p))
     show ReliableTransmissionButNoProcess = "The builtin support for reliable channels currently only affects the process calculus, but you have not specified a top-level process. Please remove \"builtins: reliable-channel\" to proceed."
     show (CannotExpandPredicate facttag rstr) = "Undefined predicate "
                               ++ showFactTagArity facttag
@@ -135,7 +134,7 @@ instance Show WFerror where
                               ++ prettySapicFunType t2
                               ++ "."
     show (FunctionNotDefined sym ) = "Function not defined " ++ show sym
-        
+
 
 instance Exception WFerror
 instance (Typeable an) => Exception (SapicException an)
diff --git a/lib/term/src/Term/Narrowing/Narrow.hs b/lib/term/src/Term/Narrowing/Narrow.hs
index 56f145d9..88f89aa1 100644
--- a/lib/term/src/Term/Narrowing/Narrow.hs
+++ b/lib/term/src/Term/Narrowing/Narrow.hs
@@ -12,6 +12,7 @@ module Term.Narrowing.Narrow (
 import           Term.Unification
 import           Term.Positions
 
+import           Control.Monad
 import           Control.Monad.Reader
 
 import           Extension.Prelude
diff --git a/lib/term/src/Term/Unification.hs b/lib/term/src/Term/Unification.hs
index b5c107cd..fcf52128 100644
--- a/lib/term/src/Term/Unification.hs
+++ b/lib/term/src/Term/Unification.hs
@@ -61,7 +61,7 @@ module Term.Unification (
   , pairDestMaudeSig
   , symEncDestMaudeSig
   , asymEncDestMaudeSig
-  , signatureDestMaudeSig  
+  , signatureDestMaudeSig
   , locationReportMaudeSig
   , revealSignatureMaudeSig
   , hashMaudeSig
@@ -80,7 +80,7 @@ module Term.Unification (
   , module Term.Rewriting.Definitions
 ) where
 
--- import           Control.Applicative
+import           Control.Monad
 import           Control.Monad.RWS
 import           Control.Monad.Except
 import           Control.Monad.State
diff --git a/lib/theory/src/Theory/Constraint/System/Guarded.hs b/lib/theory/src/Theory/Constraint/System/Guarded.hs
index 99f985a8..3f0cd8d8 100644
--- a/lib/theory/src/Theory/Constraint/System/Guarded.hs
+++ b/lib/theory/src/Theory/Constraint/System/Guarded.hs
@@ -88,6 +88,7 @@ module Theory.Constraint.System.Guarded (
 
 import           Control.Arrow
 import           Control.DeepSeq
+import           Control.Monad
 import           Control.Monad.Except
 import           Control.Monad.Fresh              (MonadFresh, scopeFreshness)
 import qualified Control.Monad.Trans.PreciseFresh as Precise (Fresh, evalFresh, evalFreshT)
diff --git a/lib/utils/src/Control/Monad/Trans/Disj.hs b/lib/utils/src/Control/Monad/Trans/Disj.hs
index 96dae742..b3b63825 100644
--- a/lib/utils/src/Control/Monad/Trans/Disj.hs
+++ b/lib/utils/src/Control/Monad/Trans/Disj.hs
@@ -18,10 +18,10 @@ module Control.Monad.Trans.Disj (
   , runDisjT
   ) where
 
--- import Control.Applicative
-import Control.Monad.List
-import Control.Monad.Reader
+import Control.Monad
 import Control.Monad.Disj.Class
+import Control.Monad.Reader
+import ListT
 
 
 ------------------------------------------------------------------------------
@@ -33,12 +33,12 @@ newtype DisjT m a = DisjT { unDisjT :: ListT m a }
   deriving (Functor, Applicative, MonadTrans )
 
 -- | Construct a 'DisjT' action.
-disjT :: m [a] -> DisjT m a
-disjT = DisjT . ListT
+disjT :: (Monad m, Foldable m) => m a -> DisjT m a
+disjT = DisjT . fromFoldable
 
 -- | Run a 'DisjT' action.
-runDisjT :: DisjT m a -> m [a]
-runDisjT = runListT . unDisjT
+runDisjT :: Monad m => DisjT m a -> m [a]
+runDisjT = toList . unDisjT
 
 
 
@@ -47,8 +47,6 @@ runDisjT = runListT . unDisjT
 ------------
 
 instance Monad m => Monad (DisjT m) where
-    {-# INLINE return #-}
-    return  = DisjT . return
     {-# INLINE (>>=) #-}
     m >>= f = DisjT $ (unDisjT . f) =<< unDisjT m
 
diff --git a/lib/utils/tamarin-prover-utils.cabal b/lib/utils/tamarin-prover-utils.cabal
index 75ed2b46..bb54d1e5 100644
--- a/lib/utils/tamarin-prover-utils.cabal
+++ b/lib/utils/tamarin-prover-utils.cabal
@@ -47,6 +47,7 @@ library
       , deepseq
       , dlist
       , fclabels
+      , list-t
       , mtl
       , pretty
       , safe
diff --git a/src/Main/Mode/Batch.hs b/src/Main/Mode/Batch.hs
index e7710682..d370da85 100644
--- a/src/Main/Mode/Batch.hs
+++ b/src/Main/Mode/Batch.hs
@@ -32,7 +32,8 @@ import           Main.TheoryLoader
 import           Main.Utils
 
 import           Theory.Module
-import           Control.Monad.Except (MonadIO(liftIO), runExceptT)
+import           Control.Monad.Except (runExceptT)
+import           Control.Monad.IO.Class (MonadIO(liftIO))
 import           System.Exit (die)
 import Theory.Tools.Wellformedness (prettyWfErrorReport)
 import           Text.Printf                     (printf)
diff --git a/src/Main/TheoryLoader.hs b/src/Main/TheoryLoader.hs
index 7fffb85b..71fba2b9 100644
--- a/src/Main/TheoryLoader.hs
+++ b/src/Main/TheoryLoader.hs
@@ -42,8 +42,6 @@ module Main.TheoryLoader (
 
   ) where
 
--- import           Debug.Trace
-
 import           Prelude                             hiding (id, (.))
 
 import           Data.Char                           (toLower)
@@ -58,8 +56,10 @@ import           Data.Bifunctor (Bifunctor(bimap))
 import           Data.Bitraversable (Bitraversable(bitraverse))
 
 import           Control.Category
-import           Control.Exception (evaluate)
 import           Control.DeepSeq (force)
+import           Control.Exception (evaluate)
+import           Control.Monad
+import           Control.Monad.IO.Class (MonadIO(liftIO))
 
 import           System.Console.CmdArgs.Explicit
 import           System.Timeout (timeout)
@@ -387,10 +387,10 @@ closeTheory version thyOpts sign srcThy = do
   deducThy   <- bitraverse (return . addMessageDeductionRuleVariants)
                            (return . addMessageDeductionRuleVariantsDiff) transThy
 
-  derivCheckSignature <- Control.Monad.Except.liftIO $ toSignatureWithMaude (get oMaudePath thyOpts) $ maudePublicSig (toSignaturePure sign)
+  derivCheckSignature <- liftIO $ toSignatureWithMaude (get oMaudePath thyOpts) $ maudePublicSig (toSignaturePure sign)
   variableReport <- case compare derivChecks 0 of
     EQ -> pure $ Just []
-    _ -> Control.Monad.Except.liftIO $ timeout (1000000 * derivChecks) $ evaluate . force $ (either (\t -> checkVariableDeducability  t derivCheckSignature autoSources defaultProver)
+    _ -> liftIO $ timeout (1000000 * derivChecks) $ evaluate . force $ (either (\t -> checkVariableDeducability  t derivCheckSignature autoSources defaultProver)
       (\t-> diffCheckVariableDeducability t derivCheckSignature autoSources defaultProver defaultDiffProver) deducThy)
 
   let report = wellformednessReport  ++ (fromMaybe [(underlineTopic "Derivation Checks", Pretty.text "Derivation checks timed out. Use --derivcheck-timeout=INT to configure timeout, 0 to deactivate.")] variableReport)
diff --git a/stack.yaml b/stack.yaml
index 7267ba17..b53f6ff8 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -7,7 +7,7 @@ packages:
 - lib/sapic/
 - lib/export/
 - lib/accountability/
-resolver: lts-20.26
+resolver: lts-22.11
 ghc-options:
   "$everything": -Wall
 nix:
diff --git a/tamarin-prover.cabal b/tamarin-prover.cabal
index 89a7e3a8..986274ea 100644
--- a/tamarin-prover.cabal
+++ b/tamarin-prover.cabal
@@ -106,7 +106,7 @@ executable tamarin-prover
     default-language: Haskell2010
 
     if flag(threaded)
-        ghc-options:   -threaded -eventlog
+        ghc-options:   -threaded
 
     -- -XFlexibleInstances