Remove warnings and some linting in SAPIC. (tamarin-prover#528)

* Remove warnings and some linting in SAPIC.

* Updated Stack to LTS 20-12 (GHC 9.2.6).

---------

Co-authored-by: Robert Künnemann <robert.kuennemann@cispa.saarland>

lib/sapic/src/Sapic/Annotation.hs

@@ -85,15 +85,17 @@ mayMerge Nothing Nothing = Nothing
 
 instance Monoid (ProcessAnnotation v) where
     mempty = ProcessAnnotation mempty mempty mempty mempty Nothing True False mempty Nothing
-    mappend p1 p2 = ProcessAnnotation
-        (parsingAnn p1 `mappend` parsingAnn p2)
-        (lock p1 `mappend` lock p2)
-        (unlock p1 `mappend` unlock p2)
-        (secretChannel p1 `mappend` secretChannel p2)
+
+instance Semigroup (ProcessAnnotation v) where
+  (<>)  p1 p2 = ProcessAnnotation
+        (parsingAnn p1 <> parsingAnn p2)
+        (lock p1 <> lock p2)
+        (unlock p1 <> unlock p2)
+        (secretChannel p1 <> secretChannel p2)
         (mayMerge (destructorEquation p1) (destructorEquation p2))
         (elseBranch p2)
         (pureState p1 || pureState p2)
-        (stateChannel p1 `mappend` stateChannel p2)
+        (stateChannel p1 <> stateChannel p2)
         (mayMerge (isStateChannel p1) (isStateChannel p2))
 
 getProcessNames :: GoodAnnotation ann => ann -> [String]
@@ -102,17 +104,13 @@ getProcessNames = processnames . getProcessParsedAnnotation
 setProcessNames :: GoodAnnotation a => [String] -> a -> a
 setProcessNames pn = mappendProcessParsedAnnotation (mempty {processnames = pn})
 
-
-instance Semigroup (ProcessAnnotation v) where
-    (<>) =  mappend
-
 instance (Apply s SapicTerm) => (Apply s (ProcessAnnotation v)) where
     apply = applyAnn
 
 newtype AnnotatedProcess = LProcess (ProcessAnnotation LVar)
     deriving (Typeable, Monoid,Semigroup,Show)
 
-data AnProcess ann = AnProcess (LProcess ann)
+newtype AnProcess ann = AnProcess (LProcess ann)
     deriving (Typeable, Show)
 
 -- This instance is useful for modifying annotations, but not for much more.
@@ -153,4 +151,4 @@ toAnProcess = unAnProcess . fmap f . AnProcess
 toProcess :: GoodAnnotation an => LProcess an -> PlainProcess
 toProcess = unAnProcess . fmap f . AnProcess
     where
-        f l = getProcessParsedAnnotation l
+        f = getProcessParsedAnnotation

lib/sapic/src/Sapic/Compression.hs

@@ -52,8 +52,7 @@ getConcsRules fact = List.partition  (List.any (sameName fact) . L.get rConcs)
 
 -- Get the list of all state facts produced by a rule
 getProducedFacts :: [Rule ProtoRuleEInfo] -> S.Set (Fact LNTerm)
-getProducedFacts rules =
-  facts
+getProducedFacts rules = facts
   where
     facts = List.foldl (\acc (Rule _ _ rconc _ _) ->
                               List.foldl (flip S.insert) acc (List.filter isStateProcessFact rconc)
@@ -74,9 +73,9 @@ mergeInfo info info2 =
 
 canMerge  :: Bool -> Rule ProtoRuleEInfo -> Rule ProtoRuleEInfo -> Bool
 canMerge compEvents r1 r2
-  | (any isSapicNoCompress ract) && (any isSapicNoCompress ract2)  = False  -- we cannot merge rules if it makes events be simulataneous
+  | any isSapicNoCompress ract && any isSapicNoCompress ract2  = False  -- we cannot merge rules if it makes events be simulataneous
 
-  | not(compEvents) && (ract /= []) && (ract2 /= [])  = False  -- we cannot merge rules if it makes events be simulataneous
+  | not compEvents && (ract /= []) && (ract2 /= [])  = False  -- we cannot merge rules if it makes events be simulataneous
   | (List.length rprem2' > 1) && (List.length rconc >1) = False   -- we cannot merge rules if we are breaking asynchronous behavior (i.e u->v,w and w,r->t cannot be compress, as r might be produced byi
   | (List.length rconc > 1) && (ract2 /= []) = False   -- we cannot merge rules if we are breaking asynchronous behavior (i.e u->v,w, and v-E->t cannot be compressed, else an event that could have happened with w before E cannot do so anymore.
   | List.any isOutFact rconc && List.any isOutFact rconc2 = False -- we cannot merge rules if two Out become simultaneous (might break the fact that the attacker can know smth and not smth else at a timepoint
@@ -91,7 +90,7 @@ canMerge compEvents r1 r2
 merge:: Bool -> Rule ProtoRuleEInfo -> Rule ProtoRuleEInfo -> S.Set (Rule ProtoRuleEInfo) ->S.Set (Rule ProtoRuleEInfo)
 merge compEvents rule1 rule2 ruleset =
   if canMerge compEvents rule1 rule2 then
-    Rule (mergeInfo rinfo rinfo2) newprem newrconc (List.union ract ract2) (rnew++rnew2) `S.insert` ruleset
+    Rule (mergeInfo rinfo rinfo2) newprem newrconc (ract `List.union` ract2) (rnew++rnew2) `S.insert` ruleset
   else
     rule1 `S.insert` (rule2 `S.insert` ruleset)
   where Rule rinfo rprem rconc ract rnew = rule1
@@ -140,5 +139,5 @@ pathCompression compEvents msr =
   return $ filterDeadend $ compress compEvents [initfact] S.empty msr
   where initfact = Sapic.Facts.factToFact (State LState [] S.empty)
          -- in the end, we remove the useless dangling rules
-        filterDeadend rs = List.filter (\  (Rule _ _ rconc ract _) ->
-                                          not(null ract && null rconc)  ) rs
+        filterDeadend = List.filter (\  (Rule _ _ rconc ract _) ->
+                                          not (null ract && null rconc)  )

lib/sapic/src/Sapic/Facts.hs

@@ -142,7 +142,7 @@ isNonSemiState (State kind _ _) = not $ isSemiState kind
 isNonSemiState _ = False
 
 isState :: TransFact -> Bool
-isState (State _ _ _) = True
+isState (State {}) = True
 isState _ = False
 
 addVarToState :: LVar -> TransFact -> TransFact
@@ -204,20 +204,20 @@ actionToFact (IsNotSet t )   =  protoFact Linear "IsNotSet" [t]
 actionToFact (InsertA t1 t2)   =  protoFact Linear "Insert" [t1,t2]
 actionToFact (DeleteA t )   =  protoFact Linear "Delete" [t]
 actionToFact (ChannelIn t)   =  protoFact Linear "ChannelIn" [t]
-actionToFact (EventEmpty)   =   protoFact Linear "Event" []
-actionToFact (PredicateA f)   =  mapFactName (\s -> "Pred_" ++ s) f
-actionToFact (NegPredicateA f)   =  mapFactName (\s -> "Pred_Not_" ++ s) f
+actionToFact EventEmpty   =   protoFact Linear "Event" []
+actionToFact (PredicateA f)   =  mapFactName ("Pred_" ++) f
+actionToFact (NegPredicateA f)   =  mapFactName ("Pred_Not_" ++) f
 actionToFact (LockNamed t v)   = protoFact Linear (lockFactName v) [lockPubTerm v,varTerm v, t ]
 actionToFact (LockUnnamed t v)   = protoFact Linear "Lock" [lockPubTerm v, varTerm v, t ]
 actionToFact (UnlockNamed t v) = protoFact Linear (unlockFactName v) [lockPubTerm v,varTerm v,t]
 actionToFact (UnlockUnnamed t v) = protoFact Linear "Unlock" [lockPubTerm v,varTerm v,t]
 actionToFact (ProgressFrom p) = protoFact Linear ("ProgressFrom_"++prettyPosition p) [varTerm $ varProgress p]
-actionToFact (ProgressTo p pf) = protoFact Linear ("ProgressTo_"++prettyPosition p) $ [varTerm $ varProgress pf]
+actionToFact (ProgressTo p pf) = protoFact Linear ("ProgressTo_"++prettyPosition p) [varTerm $ varProgress pf]
 actionToFact (TamarinAct f) = f
 
 toFreeMsgVariable :: LVar -> BVar LVar
 toFreeMsgVariable (LVar name LSortFresh id') = Free $ LVar name LSortMsg id'
-toFreeMsgVariable v = Free $ v
+toFreeMsgVariable v = Free v
 
 actionToFactFormula :: TransAction -> Fact (Term (Lit Name (BVar LVar)))
 actionToFactFormula = fmap (fmap $ fmap toFreeMsgVariable) . actionToFact
@@ -232,7 +232,7 @@ varMID p = LVar n s i
                 -- but I don't see an advantage (yet)
 
 factToFact :: TransFact -> Fact LNTerm
-factToFact (Fr v) = freshFact $ varTerm (v)
+factToFact (Fr v) = freshFact $ varTerm v
 factToFact (In t) = inFact t
 factToFact (Out t) = outFact t
 factToFact (FLet p t vars) = protoFact Linear ("Let"++ "_" ++ prettyPosition p) (t:ts)
@@ -247,15 +247,15 @@ factToFact (State kind p vars) = protoFact (multiplicity kind) (name kind ++ "_"
         name k = if isSemiState k then "Semistate" else "State"
         ts = map varTerm (S.toList vars)
 factToFact (TamarinFact f) = f
-factToFact (PureCell t1 t2) = protoFact Linear ("L_PureState") [t1, t2]
-factToFact (CellLocked t1 t2) = protoFact Linear ("L_CellLocked") [t1, t2]
+factToFact (PureCell t1 t2) = protoFact Linear "L_PureState" [t1, t2]
+factToFact (CellLocked t1 t2) = protoFact Linear "L_CellLocked" [t1, t2]
 
 
 pureStateFactTag :: FactTag
-pureStateFactTag =  ProtoFact Linear ("L_PureState") 2
+pureStateFactTag =  ProtoFact Linear "L_PureState" 2
 
 pureStateLockFactTag :: FactTag
-pureStateLockFactTag =  ProtoFact Linear ("L_CellLocked") 2
+pureStateLockFactTag =  ProtoFact Linear "L_CellLocked" 2
 
 
 isOutFact :: Fact t -> Bool
@@ -321,7 +321,7 @@ colorHash :: (Fractional t, Ord t) => String -> RGB t
 colorHash s = RGB r g b
       where
         nthByte x n = (x `shiftR` (8*n)) .&. 0xff
-        [r,g,b] = map ((/255) . fromIntegral . nthByte (crc32 s)) [0,1,2]
+        (r,g,b) = fmap ((/255) . fromIntegral . nthByte (crc32 s)) (0,1,2)
 
 -- Computes a color for a list of strings by first computing
 -- the CRC32 checksum of each string and then interpolating the

lib/sapic/src/Sapic/Locks.hs

@@ -38,11 +38,11 @@ annotateEachClosestUnlock t v (ProcessAction (Unlock t') a' p) =
                 return $ ProcessAction (Unlock t') (a' <> annUnlock v) p
             else do
                 p' <- annotateEachClosestUnlock t v p
-                return $ProcessAction (Unlock t') a' p'
+                return $ ProcessAction (Unlock t') a' p'
 annotateEachClosestUnlock t v (ProcessAction (Insert t1 t2) a' p) | t1==t =
                do
                 p' <- annotateEachClosestUnlock t v p
-                return $ProcessAction (Insert t1 t2)  (a' <> annUnlock v) p'
+                return $ ProcessAction (Insert t1 t2)  (a' <> annUnlock v) p'
 annotateEachClosestUnlock _ _ (ProcessAction Rep _ _) = throwM $ LocalException WFRep
 annotateEachClosestUnlock _ _ (ProcessComb Parallel _ _ _) = throwM $ LocalException WFPar
 annotateEachClosestUnlock t v (ProcessAction ac a' p) = do p' <- annotateEachClosestUnlock t v p

lib/sapic/src/Sapic/Typing.hs

@@ -21,7 +21,6 @@ import Control.Monad.Trans.State.Lazy
 import Control.Monad.Catch
 import Theory
 import Theory.Sapic
-import Term.Builtin.Rules
 import Term.SubtermRule
 import Sapic.Exceptions
 import Sapic.Bindings
@@ -73,13 +72,13 @@ typeWith :: (MonadThrow m, MonadCatch m) =>
 typeWith t tt
     | Lit2 (Var v) <- viewTerm2 t , lvar' <- slvar v -- CASE: variable
     = do
-        stype' <- 
+        stype' <-
             if lvarSort lvar' == LSortPub then
                 return Nothing
             else do
                 maybeType <- Map.lookup lvar' <$> gets vars
                 case maybeType of
-                    Nothing -> throwM $ WFUnbound (S.singleton lvar') 
+                    Nothing -> throwM $ WFUnbound (S.singleton lvar')
                     Just t' -> return t'
         t' <- catch (sqcap stype' tt) (sqHandler t)
         te <- get
@@ -140,7 +139,7 @@ typeTermsWithEnv typeEnv terms = execStateT (mapM typeWith' terms) typeEnv'
 typeProcess :: (GoodAnnotation a, MonadThrow m, MonadCatch m, Show a, Typeable a) =>
     Process a SapicLVar ->  StateT
         TypingEnvironment m (Process a SapicLVar)
-typeProcess p = traverseProcess fNull fAct fComb gAct gComb p
+typeProcess = traverseProcess fNull fAct fComb gAct gComb
      where
         -- fNull/fAcc/fComb collect variables that are bound when going downwards
         fNull ann  = return (ProcessNull ann)
@@ -183,16 +182,14 @@ toSapicTerm = fmap f
 
 typeRule ::  (MonadThrow m, MonadCatch m) =>  TypingEnvironment -> CtxtStRule -> m TypingEnvironment
 typeRule typeEnv r | (lhs `RRule` rhs) <- ctxtStRuleToRRule r = do
-                       te <- typeTermsWithEnv typeEnv (map toSapicTerm [lhs, rhs])
-                       return te
+                       typeTermsWithEnv typeEnv (map toSapicTerm [lhs, rhs])
 
 initTEFromSig :: (MonadThrow m, MonadCatch m) => OpenTheory -> m TypingEnvironment
 initTEFromSig th = do
-  te <-  foldM (\te rule->typeRule te rule) initTE sigRules
-  return te
+  foldM typeRule initTE sigRules
   where
     -- we load all funs and add default type
-    sig = (L.get sigpMaudeSig (L.get thySignature th))
+    sig = L.get sigpMaudeSig (L.get thySignature th)
     funSet = stFunSyms sig
     funTyped = foldMap (\fs@(_,(n,_,_)) -> Map.singleton fs (defaultFunctionType n)) funSet
     -- we then also add the custom used defined types
@@ -230,7 +227,7 @@ typeTheoryEnv th = do
         addFunctionTypingInfo' sym (ins,out) = addFunctionTypingInfo (sym, ins,out)
 
 -- | Type the Sapic processes in a theory
-typeTheory :: (MonadThrow m, MonadCatch m) => OpenTheory -> m (OpenTheory)
+typeTheory :: (MonadThrow m, MonadCatch m) => OpenTheory -> m OpenTheory
 typeTheory th = fst <$> typeTheoryEnv th
 
 -- | Rename a process so that all its names are unique. Returns renamed process

lib/theory/src/Theory/Constraint/Solver/Sources.hs

@@ -35,7 +35,6 @@ module Theory.Constraint.Solver.Sources (
 import           Prelude                                 hiding (id, (.))
 import           Safe
 
-import           Data.Foldable                           (asum)
 import qualified Data.Map                                as M
 import qualified Data.Set                                as S
 

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

@@ -107,8 +107,6 @@ import           Text.PrettyPrint.Highlight
 
 import           Theory.Model
 
-import           Data.Functor.Identity
-
 -- Control.Monad.Fail import will become redundant in GHC 8.8+
 -- import qualified Control.Monad.Fail as Fail
 

lib/theory/src/Theory/Text/Parser.hs

@@ -28,7 +28,6 @@ module Theory.Text.Parser (
   ) where
 
 import           Prelude                    hiding (id, (.))
-import           Data.Foldable              (asum)
 import           Data.Label
 import           Data.Maybe
 -- import           Data.Monoid                hiding (Last)

lib/theory/src/Theory/Text/Parser/Formula.hs

@@ -15,7 +15,6 @@ module Theory.Text.Parser.Formula
   )
 where
 import           Prelude                    hiding (id, (.))
-import           Data.Foldable              (asum)
 -- import           Data.Monoid                hiding (Last)
 import           Control.Applicative        hiding (empty, many, optional)
 import           Control.Category

lib/theory/src/Theory/Text/Parser/Lemma.hs

@@ -17,8 +17,6 @@ module Theory.Text.Parser.Lemma(
 where
 
 import           Prelude                    hiding (id, (.))
-import           Data.Foldable              (asum)
--- import           Data.Monoid                hiding (Last)
 import           Control.Applicative        hiding (empty, many, optional)
 import           Text.Parsec                hiding ((<|>))
 import           Theory

lib/theory/src/Theory/Text/Parser/Proof.hs

@@ -15,7 +15,6 @@ module Theory.Text.Parser.Proof (
 where
 
 import           Prelude                    hiding (id, (.))
-import           Data.Foldable              (asum)
 import qualified Data.Map                   as M
 -- import           Data.Monoid                hiding (Last)
 import           Control.Applicative        hiding (empty, many, optional)

lib/theory/src/Theory/Text/Parser/Rule.hs

@@ -21,7 +21,6 @@ where
 import           Prelude                    hiding (id, (.))
 import qualified Data.ByteString            as B
 import qualified Data.ByteString.Char8      as BC
-import           Data.Foldable              (asum)
 import           Data.Label
 import           Data.Either
 import           Data.Maybe

lib/theory/src/Theory/Text/Parser/Signature.hs

@@ -25,7 +25,6 @@ where
 
 import           Prelude                    hiding (id)
 import qualified Data.ByteString.Char8      as BC
-import           Data.Foldable              (asum)
 import           Data.Either
 -- import           Data.Monoid                hiding (Last)
 import qualified Data.Set                   as S

lib/theory/src/Theory/Text/Parser/Token.hs

@@ -117,7 +117,6 @@ module Theory.Text.Parser.Token (
 
 import           Prelude             hiding (id, (.))
 
-import           Data.Foldable       (asum)
 -- import           Data.Label
 -- import           Data.Binary
 import           Data.List (foldl')

stack.yaml

@@ -7,8 +7,10 @@ packages:
 - lib/sapic/
 - lib/export/
 - lib/accountability/
-resolver: lts-19.32
+resolver: lts-20.12
 ghc-options:
   "$everything": -Wall
 nix:
   packages: [ zlib ]
+
+