Prelude.Kore: Export Foldable and Traversable (#2238)

Author: ttuegel

kore/app/exec/Main.hs

@@ -14,7 +14,6 @@ import Control.Monad.Extra as Monad
 import Data.Default
     ( def
     )
-import qualified Data.Foldable as Foldable
 import Data.Generics.Product
     ( field
     )
@@ -493,7 +492,7 @@ writeKoreProveFiles reportFile koreProveOptions = do
     let KoreProveOptions { specFileName } = koreProveOptions
     copyFile specFileName (reportFile </> "spec.kore")
     let KoreProveOptions { saveProofs } = koreProveOptions
-    Foldable.for_ saveProofs $ \filePath ->
+    for_ saveProofs $ \filePath ->
         Monad.whenM
             (doesFileExist filePath)
             (copyFile filePath (reportFile </> "save-proofs.kore"))
@@ -520,14 +519,14 @@ writeOptionsAndKoreFiles
     setPermissions shellScript $ allPermissions emptyPermissions
     copyFile definitionFileName
         (reportDirectory </> defaultDefinitionFilePath opts)
-    Foldable.for_ patternFileName
+    for_ patternFileName
         $ flip copyFile (reportDirectory </> "pgm.kore")
     writeKoreSolverFiles koreSolverOptions reportDirectory
-    Foldable.for_ koreSearchOptions
+    for_ koreSearchOptions
         (writeKoreSearchFiles reportDirectory)
-    Foldable.for_ koreMergeOptions
+    for_ koreMergeOptions
         (writeKoreMergeFiles reportDirectory)
-    Foldable.for_ koreProveOptions
+    for_ koreProveOptions
         (writeKoreProveFiles reportDirectory)
 
 exeName :: ExeName
@@ -548,7 +547,7 @@ main = do
             (Just envName)
             (parseKoreExecOptions startTime)
             parserInfoModifiers
-    Foldable.for_ (localOptions options) mainWithOptions
+    for_ (localOptions options) mainWithOptions
 
 mainWithOptions :: KoreExecOptions -> IO ()
 mainWithOptions execOptions = do
@@ -562,7 +561,7 @@ mainWithOptions execOptions = do
                 & handle handleSomeException
                 & runKoreLog tmpDir koreLogOptions
     let KoreExecOptions { rtsStatistics } = execOptions
-    Foldable.for_ rtsStatistics $ \filePath ->
+    for_ rtsStatistics $ \filePath ->
         writeStats filePath =<< getStats
     exitWith exitCode
   where
@@ -675,7 +674,7 @@ koreProve execOptions proveOptions = do
                 OrPattern.fromPatterns (MultiAnd.map getStuckConfig stuckClaims)
             getStuckConfig =
                 getRewritingPattern . getConfiguration . getStuckClaim
-    lift $ Foldable.for_ saveProofs $ saveProven specModule provenClaims
+    lift $ for_ saveProofs $ saveProven specModule provenClaims
     lift $ renderResult execOptions (unparse final)
     return exitCode
   where
@@ -704,7 +703,7 @@ koreProve execOptions proveOptions = do
         -> MultiAnd SomeClaim
         -> FilePath
         -> IO ()
-    saveProven specModule (Foldable.toList -> provenClaims) outputFile =
+    saveProven specModule (toList -> provenClaims) outputFile =
         withFile outputFile WriteMode
             (`hPutDoc` unparse provenDefinition)
       where

kore/src/Debug.hs

@@ -27,7 +27,6 @@ import Data.ByteString
     ( ByteString
     )
 import qualified Data.Char as Char
-import qualified Data.Foldable as Foldable
 import Data.Functor.Const
     ( Const
     )
@@ -341,7 +340,7 @@ instance Debug a => Debug (Set a) where
 instance Debug a => Debug (Seq a) where
     debugPrec as precOut =
         (parens (precOut >= 10) . Pretty.sep)
-        ["Data.Sequence.fromList", debug (Foldable.toList as)]
+        ["Data.Sequence.fromList", debug (toList as)]
 
 instance Debug a => Debug (Const a b)
 
@@ -578,7 +577,7 @@ instance
 instance (Debug a, Diff a) => Diff (Seq a) where
     diffPrec as bs =
         fmap wrapFromList
-        $ diffPrec (Foldable.toList as) (Foldable.toList bs)
+        $ diffPrec (toList as) (toList bs)
       where
         wrapFromList diff' precOut =
             parens (precOut >= 10) $ "Data.Sequence.fromList" <+> diff' 10

kore/src/Kore/ASTVerifier/AliasVerifier.hs

@@ -15,7 +15,6 @@ import Control.Monad.Reader
     )
 import qualified Control.Monad.Reader as Reader
 import qualified Control.Monad.State.Class as State
-import qualified Data.Foldable as Foldable
 import qualified Data.Functor.Foldable as Recursive
 import Data.Generics.Product
 import Data.Map.Strict
@@ -63,7 +62,7 @@ verifyAliases sentences = do
             $ mapMaybe projectSentenceAlias sentences
         aliasIds = Map.keysSet aliases
     runReaderT
-        (Foldable.traverse_ verifyAlias aliasIds)
+        (traverse_ verifyAlias aliasIds)
         AliasContext { aliases, verifying = Set.empty }
 
 aliasName :: SentenceAlias patternType -> Id
@@ -123,7 +122,7 @@ verifyUncachedAlias :: Id -> AliasVerifier ()
 verifyUncachedAlias name = do
     sentence <- lookupParsedAlias name
     dependencies <- aliasDependencies sentence
-    Foldable.traverse_ verifyAlias dependencies
+    traverse_ verifyAlias dependencies
     verified <- SentenceVerifier.verifyAliasSentence sentence & lift
     attrs <- parseAttributes (sentenceAliasAttributes verified) & liftParser
     State.modify' $ addAlias verified attrs
@@ -145,7 +144,7 @@ collectAliasIds
     -> AliasVerifier (Set Id)
 collectAliasIds base = do
     _ :< patternF <- sequence base
-    let names = Foldable.fold patternF
+    let names = fold patternF
     AliasContext { aliases } <- Reader.ask
     case patternF of
         ApplicationF application | Map.member name aliases ->

kore/src/Kore/ASTVerifier/AttributesVerifier.hs

@@ -18,16 +18,12 @@ module Kore.ASTVerifier.AttributesVerifier
     , parseAttributes
     ) where
 
-import qualified Control.Lens as Lens
-import Data.Foldable
-    ( find
-    , for_
-    )
-import Data.Generics.Product
 import Prelude.Kore
 
 import qualified Control.Comonad.Trans.Cofree as Cofree
+import qualified Control.Lens as Lens
 import qualified Data.Functor.Foldable as Recursive
+import Data.Generics.Product
 
 import Kore.ASTVerifier.Error
 import qualified Kore.Attribute.Axiom as Attribute

kore/src/Kore/ASTVerifier/DefinitionVerifier.hs

@@ -22,7 +22,6 @@ import Control.Lens
 import Control.Monad
     ( foldM
     )
-import qualified Data.Foldable as Foldable
 import Data.Generics.Product
     ( field
     )
@@ -133,7 +132,7 @@ verifyAndIndexDefinitionWithBase
         implicitModule = ImplicitIndexedModule implicitIndexedModule
         parsedModules = modulesByName (definitionModules definition)
         definitionModuleNames = moduleName <$> definitionModules definition
-        verifyModules = Foldable.traverse_ verifyModule definitionModuleNames
+        verifyModules = traverse_ verifyModule definitionModuleNames
 
     -- Verify the contents of the definition.
     (_, index) <-

kore/src/Kore/ASTVerifier/ModuleVerifier.hs

@@ -20,7 +20,6 @@ import Control.Lens
 import qualified Control.Lens as Lens
 import qualified Control.Monad.Reader.Class as Reader
 import qualified Control.Monad.State.Class as State
-import qualified Data.Foldable as Foldable
 import Data.Generics.Product
 import qualified Data.List as List
 import qualified Data.Map.Strict as Map
@@ -133,7 +132,7 @@ The named modules are verified and imported into the current 'VerifiedModule'.
 
  -}
 verifyImports :: [ParsedSentence] -> SentenceVerifier ()
-verifyImports = Foldable.traverse_ verifyImport . mapMaybe projectSentenceImport
+verifyImports = traverse_ verifyImport . mapMaybe projectSentenceImport
 
 verifyImport :: SentenceImport ParsedPattern -> SentenceVerifier ()
 verifyImport sentence =

kore/src/Kore/ASTVerifier/PatternVerifier.hs

@@ -19,7 +19,6 @@ import qualified Control.Monad as Monad
 import qualified Control.Monad.Reader as Reader
 import qualified Control.Monad.Trans.Class as Trans
 import Control.Monad.Trans.Maybe
-import qualified Data.Foldable as Foldable
 import qualified Data.Functor.Foldable as Recursive
 import qualified Data.Map.Strict as Map
 import qualified Data.Set as Set
@@ -345,7 +344,7 @@ verifyApplyAlias application =
     let verified = application { applicationSymbolOrAlias = alias }
         sorts = Internal.aliasSorts alias
     leftVariables <- getLeftVariables (Internal.aliasConstructor alias)
-    Foldable.traverse_ ensureChildIsDeclaredVarType $ zip leftVariables children
+    traverse_ ensureChildIsDeclaredVarType $ zip leftVariables children
     verifyApplicationChildren Internal.termLikeSort verified sorts
   where
     Application

kore/src/Kore/ASTVerifier/PatternVerifier/PatternVerifier.hs

@@ -41,7 +41,6 @@ import Control.Monad.Reader
 import qualified Control.Monad.Reader as Reader
 import qualified Control.Monad.Trans.Class as Trans
 import Control.Monad.Trans.Maybe
-import qualified Data.Foldable as Foldable
 import qualified Data.Map.Strict as Map
 import Data.Set
     ( Set
@@ -259,8 +258,7 @@ uniqueDeclaredVariables
     :: Foldable f
     => f (SomeVariable VariableName)
     -> PatternVerifier DeclaredVariables
-uniqueDeclaredVariables =
-    Foldable.foldlM newDeclaredVariable emptyDeclaredVariables
+uniqueDeclaredVariables = foldlM newDeclaredVariable emptyDeclaredVariables
 
 {- | Run a 'PatternVerifier' in a particular variable context.
 

kore/src/Kore/ASTVerifier/SentenceVerifier.hs

@@ -34,7 +34,6 @@ import Control.Monad.State.Strict
     , runStateT
     )
 import qualified Control.Monad.State.Strict as State
-import qualified Data.Foldable as Foldable
 import Data.Generics.Product.Fields
 import qualified Data.Map.Strict as Map
 import Data.Set
@@ -195,7 +194,7 @@ runSentenceVerifier sentenceVerifier verifiedModule =
 
 verifyHookedSorts :: [ParsedSentence] -> SentenceVerifier ()
 verifyHookedSorts =
-    Foldable.traverse_ verifyHookedSortSentence
+    traverse_ verifyHookedSortSentence
     . mapMaybe projectSentenceHookedSort
 
 verifyHookedSortSentence :: SentenceSort ParsedPattern -> SentenceVerifier ()
@@ -222,7 +221,7 @@ verifyHookedSymbols
     :: [ParsedSentence]
     -> SentenceVerifier ()
 verifyHookedSymbols =
-    Foldable.traverse_ verifyHookedSymbolSentence
+    traverse_ verifyHookedSymbolSentence
     . mapMaybe projectSentenceHookedSymbol
 
 verifyHookedSymbolSentence
@@ -257,7 +256,7 @@ addIndexedModuleHook name hook =
       | otherwise           = id
 
 verifySymbols :: [ParsedSentence] -> SentenceVerifier ()
-verifySymbols = Foldable.traverse_ verifySymbolSentence . mapMaybe project
+verifySymbols = traverse_ verifySymbolSentence . mapMaybe project
   where
     project sentence =
         projectSentenceSymbol sentence <|> projectSentenceHookedSymbol sentence
@@ -349,7 +348,7 @@ verifyAliasSentence sentence = do
 
 verifyAxioms :: [ParsedSentence] -> SentenceVerifier ()
 verifyAxioms =
-    Foldable.traverse_ verifyAxiomSentence
+    traverse_ verifyAxiomSentence
     . mapMaybe projectSentenceAxiom
 
 verifyAxiomSentence :: SentenceAxiom ParsedPattern -> SentenceVerifier ()
@@ -383,7 +382,7 @@ verifyClaims
     :: [ParsedSentence]
     -> SentenceVerifier ()
 verifyClaims =
-    Foldable.traverse_ verifyClaimSentence
+    traverse_ verifyClaimSentence
     . mapMaybe projectSentenceClaim
 
 verifyClaimSentence :: SentenceClaim ParsedPattern -> SentenceVerifier ()
@@ -420,7 +419,7 @@ verifyClaimSentence sentence =
                 freeVariablesLeft claimPattern & FreeVariables.toSet
 
 verifySorts :: [ParsedSentence] -> SentenceVerifier ()
-verifySorts = Foldable.traverse_ verifySortSentence . mapMaybe project
+verifySorts = traverse_ verifySortSentence . mapMaybe project
   where
     project sentence =
         projectSentenceSort sentence <|> projectSentenceHookedSort sentence
@@ -445,7 +444,7 @@ verifyNonHooks
     :: [ParsedSentence]
     -> SentenceVerifier ()
 verifyNonHooks sentences=
-    Foldable.traverse_ verifyNonHookSentence nonHookSentences
+    traverse_ verifyNonHookSentence nonHookSentences
   where
     nonHookSentences = mapMaybe project sentences
     project (SentenceHookSentence _) = Nothing

kore/src/Kore/Attribute/Axiom.hs

@@ -46,7 +46,6 @@ import Data.Default
     ( Default (..)
     )
 import qualified Data.Default as Default
-import qualified Data.Foldable as Foldable
 import Data.Generics.Product
 import Data.Proxy
 import qualified Generics.SOP as SOP
@@ -254,7 +253,7 @@ parseAxiomAttributes
     -> Attributes
     -> Parser (Axiom SymbolOrAlias VariableName)
 parseAxiomAttributes freeVariables (Attributes attrs) =
-    Foldable.foldlM (flip $ parseAxiomAttribute freeVariables) Default.def attrs
+    foldlM (flip $ parseAxiomAttribute freeVariables) Default.def attrs
 
 mapAxiomVariables
     :: Ord variable2

kore/src/Kore/Attribute/Parser.hs

@@ -85,7 +85,6 @@ import Data.Default
     ( Default (..)
     )
 import qualified Data.Default as Default
-import qualified Data.Foldable as Foldable
 import qualified Data.Functor.Foldable as Recursive
 import qualified Data.List as List
 import Data.Text
@@ -162,7 +161,7 @@ parseAttributesWith
     -> attrs
     -> Parser attrs
 parseAttributesWith (Attributes attrs) def' =
-    Foldable.foldlM (flip parseAttribute) def' attrs
+    foldlM (flip parseAttribute) def' attrs
 
 parseAttributes :: ParseAttributes attrs => Attributes -> Parser attrs
 parseAttributes attrs = parseAttributesWith attrs Default.def

kore/src/Kore/Attribute/Pattern/Defined.hs

@@ -11,7 +11,6 @@ module Kore.Attribute.Pattern.Defined
 import Prelude.Kore
 
 import Control.DeepSeq
-import qualified Data.Foldable as Foldable
 import Data.Functor.Const
 import qualified Data.Map.Strict as Map
 import Data.Monoid
@@ -54,7 +53,7 @@ instance Synthetic Defined (Bottom sort) where
 -- arguments are 'Defined'.
 instance Synthetic Defined (Application Internal.Symbol) where
     synthetic application =
-        totalSymbol <> Foldable.fold children
+        totalSymbol <> fold children
       where
         totalSymbol = Defined (Internal.isTotal symbol)
         children = applicationChildren application
@@ -120,7 +119,7 @@ instance Synthetic Defined (Nu sort) where
 
 -- | An 'Or' pattern is 'Defined' if any of its subterms is 'Defined'.
 instance Synthetic Defined (Or sort) where
-    synthetic = Defined . getAny . Foldable.foldMap (Any . isDefined)
+    synthetic = Defined . getAny . foldMap (Any . isDefined)
     {-# INLINE synthetic #-}
 
 instance Synthetic Defined (Rewrites sort) where
@@ -139,7 +138,7 @@ instance Synthetic Defined (Builtin key) where
             {builtinAcChild = NormalizedMap builtinMapChild}
         )
       = normalizedAcDefined builtinMapChild
-    synthetic builtin = Foldable.fold builtin
+    synthetic builtin = fold builtin
     {-# INLINE synthetic #-}
 
 normalizedAcDefined
@@ -165,7 +164,7 @@ normalizedAcDefined ac@(NormalizedAc _ _ _) =
           | Map.null concreteElements -> sameAsChildren
         _ -> Defined False
   where
-    sameAsChildren = Foldable.fold ac
+    sameAsChildren = fold ac
 
 
 -- | A 'Top' pattern is always 'Defined'.

kore/src/Kore/Attribute/Pattern/FreeVariables.hs

@@ -21,10 +21,11 @@ module Kore.Attribute.Pattern.FreeVariables
     , HasFreeVariables (..)
     ) where
 
-import Prelude.Kore
+import Prelude.Kore hiding
+    ( toList
+    )
 
 import Control.DeepSeq
-import qualified Data.Foldable as Foldable
 import Data.Functor.Const
 import Data.Map.Strict
     ( Map
@@ -119,8 +120,7 @@ bindVariables
     => f (SomeVariable variable)
     -> FreeVariables variable
     -> FreeVariables variable
-bindVariables bound free =
-    Foldable.foldl' (flip bindVariable) free bound
+bindVariables bound free = foldl' (flip bindVariable) free bound
 {-# INLINE bindVariables #-}
 
 isFreeVariable