Merge remote-tracking branch 'rv/master' into full-correctness

Author: traiansf

kore/src/Kore/Exec.hs

@@ -339,9 +339,7 @@ exec
             infoExecDepth (maximum (ExecDepth 0 : depths))
             let finalConfigs' =
                     MultiOr.make $
-                        catMaybes $
-                            extractProgramState
-                                <$> finalConfigs
+                        mapMaybe extractProgramState finalConfigs
             exitCode <- getExitCode verifiedModule finalConfigs'
             let finalTerm =
                     MultiOr.map getRewritingPattern finalConfigs'

kore/src/Kore/Log/KoreLogOptions.hs

@@ -485,16 +485,10 @@ unparseKoreLogOptions
             ["--sqlog", file]
 
         debugApplyEquationOptionsFlag (DebugApplyEquationOptions set) =
-            concat $
-                ("--debug-apply-equation" :) . (: []) . Text.unpack
-                    <$> toList set
+            concatMap (("--debug-apply-equation" :) . (: []) . Text.unpack) (toList set)
 
         debugAttemptEquationOptionsFlag (DebugAttemptEquationOptions set) =
-            concat $
-                ("--debug-attempt-equation" :) . (: []) . Text.unpack
-                    <$> toList set
+            concatMap (("--debug-attempt-equation" :) . (: []) . Text.unpack) (toList set)
 
         debugEquationOptionsFlag (DebugEquationOptions set) =
-            concat $
-                ("--debug-equation" :) . (: []) . Text.unpack
-                    <$> toList set
+            concatMap (("--debug-equation" :) . (: []) . Text.unpack) (toList set)

kore/src/Kore/Validate/PatternVerifier.hs

@@ -484,8 +484,9 @@ verifyDomainValue domain = do
     verified <- Internal.DomainValueF <$> sequence domain
     let freeVariables' :: FreeVariables VariableName =
             foldMap
-                freeVariables
-                (Internal.extractAttributes <$> verified)
+                ( freeVariables . Internal.extractAttributes
+                )
+                verified
     unless
         (nullFreeVariables freeVariables')
         (koreFail "Domain value must not contain free variables.")

kore/test/Test/Data/Sup.hs

@@ -49,8 +49,7 @@ hprop_transitiveOrd =
 
 hprop_reflexiveOrd :: Property
 hprop_reflexiveOrd =
-    (property . sequence_)
-        (reflexive <$> sups)
+    property (mapM_ reflexive sups)
   where
     reflexive x = do
         annotateShow x
@@ -67,8 +66,7 @@ hprop_antisymmetricOrd =
 
 hprop_reflexiveEq :: Property
 hprop_reflexiveEq =
-    (property . sequence_)
-        (reflexive <$> sups)
+    property (mapM_ reflexive sups)
   where
     reflexive x = do
         annotateShow x

kore/test/Test/Kore/Attribute/Axiom/Concrete.hs

@@ -62,7 +62,7 @@ test_concrete_selectx2 =
                     , concreteAttribute [inject Mock.z]
                     ]
   where
-    freeVars = foldMap freeVariable $ inject <$> [Mock.x, Mock.y, Mock.z]
+    freeVars = foldMap (freeVariable . inject) [Mock.x, Mock.y, Mock.z]
     concreteVars = foldMap (freeVariable . inject) [Mock.x, Mock.z]
 
 test_Attributes :: TestTree

kore/test/Test/Kore/Attribute/Axiom/Symbolic.hs

@@ -60,7 +60,7 @@ test_symbolic_selectx2 =
                     , symbolicAttribute [inject Mock.z]
                     ]
   where
-    freeVars = foldMap freeVariable $ inject <$> [Mock.x, Mock.y, Mock.z]
+    freeVars = foldMap (freeVariable . inject) [Mock.x, Mock.y, Mock.z]
     symbolicVars = foldMap (freeVariable . inject) [Mock.x, Mock.z]
 
 test_Attributes :: TestTree