Update to GHC 9.6 (#618)

Removing Control.Monad.List

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)

lib/term/src/Term/Narrowing/Narrow.hs

@@ -1,7 +1,7 @@
 -- |
 -- Copyright   : (c) 2010-2012 Benedikt Schmidt
 -- License     : GPL v3 (see LICENSE)
--- 
+--
 --
 -- One-step narrowing from a term.
 module Term.Narrowing.Narrow (
@@ -11,6 +11,7 @@ module Term.Narrowing.Narrow (
 import           Term.Unification
 import           Term.Positions
 
+import           Control.Monad
 import           Control.Monad.Reader
 
 import           Extension.Prelude

lib/term/src/Term/Unification.hs

@@ -60,7 +60,7 @@ module Term.Unification (
   , pairDestMaudeSig
   , symEncDestMaudeSig
   , asymEncDestMaudeSig
-  , signatureDestMaudeSig  
+  , signatureDestMaudeSig
   , locationReportMaudeSig
   , revealSignatureMaudeSig
   , hashMaudeSig
@@ -79,7 +79,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

lib/theory/src/Theory/Constraint/System/Guarded.hs

@@ -87,6 +87,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)

lib/utils/src/Control/Monad/Trans/Disj.hs

@@ -5,7 +5,7 @@
 -- |
 -- Copyright   : (c) 2011 Simon Meier
 -- License     : GPL v3 (see LICENSE)
--- 
+--
 -- Portability : unknown
 --
 -- A monad transformer to enable other *commutative* monads to represent
@@ -17,10 +17,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
 
 
 ------------------------------------------------------------------------------
@@ -32,12 +32,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
 
 
 
@@ -46,8 +46,6 @@ runDisjT = runListT . unDisjT
 ------------
 
 instance Monad m => Monad (DisjT m) where
-    {-# INLINE return #-}
-    return  = DisjT . return
     {-# INLINE (>>=) #-}
     m >>= f = DisjT $ (unDisjT . f) =<< unDisjT m
 

lib/utils/tamarin-prover-utils.cabal

@@ -47,6 +47,7 @@ library
       , deepseq
       , dlist
       , fclabels
+      , list-t
       , mtl
       , pretty
       , safe

src/Main/Mode/Batch.hs

@@ -28,7 +28,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)
@@ -191,7 +192,7 @@ run thisMode as
         formalComments = either (filter (/=("","")) . theoryFormalComments) (filter (/=("", "")) . diffTheoryFormalComments)
 
         isParseOnlyMode = get oParseOnlyMode thyLoadOptions
-        isTranslateOnlyMode = get oOutputModule thyLoadOptions `elem` 
+        isTranslateOnlyMode = get oOutputModule thyLoadOptions `elem`
                                 [ModuleSpthy, ModuleSpthyTyped, ModuleProVerif, ModuleProVerifEquivalence, ModuleDeepSec]
 
         handleError e@(ParserError _) = die $ show e
@@ -205,4 +206,4 @@ run thisMode as
 
         ppWf []  = Pretty.emptyDoc
         ppWf rep = Pretty.vcat $ Pretty.text ("WARNING: " ++ show (length rep) ++ " wellformedness check failed!")
-                             : [ Pretty.text   "         The analysis results might be wrong!" | get oProveMode thyLoadOptions ]
+                             : [ Pretty.text   "         The analysis results might be wrong!" | get oProveMode thyLoadOptions ]

src/Main/TheoryLoader.hs

@@ -44,24 +44,24 @@ module Main.TheoryLoader (
 
   ) where
 
--- import           Debug.Trace
-
 import           Prelude                             hiding (id, (.))
 
 import           Data.Char                           (toLower)
 import           Data.Label
 import           Data.List                           (isPrefixOf, intercalate, find)
 import qualified Data.Set
-import           Data.Maybe                          (fromMaybe, fromJust, isJust, isNothing)
+import           Data.Maybe                          (fromMaybe, isNothing)
 import           Data.Map                            (keys)
 import           Data.FileEmbed                      (embedFile)
 import qualified Data.Label as L
 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)
@@ -293,7 +293,7 @@ mkTheoryLoadOptions as = TheoryLoadOptions
     sat = findArg "SaturationLimit" as
     satDefault = L.get oSaturation defaultTheoryLoadOptions
     saturation = parseIntArg sat satDefault integerFromInt "SaturationLimit: invalid bound given"
-    
+
     derivchecks = findArg "derivcheck-timeout" as
     derivDefault = L.get oDerivationChecks defaultTheoryLoadOptions
     deriv = parseIntArg derivchecks derivDefault id "derivcheck-timeout: invalid bound given"

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:

tamarin-prover.cabal

@@ -107,7 +107,7 @@ executable tamarin-prover
     default-language: Haskell2010
 
     if flag(threaded)
-        ghc-options:   -threaded -eventlog
+        ghc-options:   -threaded
 
     -- -XFlexibleInstances