Format with fourmolu

runtimeverification · Mar 22, 2024 · be24db5 · be24db5
1 parent 04a0917
commit be24db5
Show file tree

Hide file tree

Showing 5 changed files with 91 additions and 62 deletions.
diff --git a/library/Booster/JsonRpc.hs b/library/Booster/JsonRpc.hs
@@ -60,7 +60,7 @@ import Booster.Pattern.Rewrite (
     performRewrite,
  )
 import Booster.Pattern.Util (sortOfPattern, substituteInPredicate, substituteInTerm)
-import Booster.Prettyprinter (renderText, renderOneLineText)
+import Booster.Prettyprinter (renderOneLineText, renderText)
 import Booster.SMT.Base qualified as SMT
 import Booster.SMT.Interface qualified as SMT
 import Booster.Syntax.Json (KoreJson (..), addHeader, prettyPattern, sortOfJson)
@@ -70,8 +70,9 @@ import Booster.Syntax.Json.Internalise (
     TermOrPredicates (..),
     internalisePattern,
     internaliseTermOrPredicate,
+    patternErrorToRpcError,
     pattern CheckSubsorts,
-    pattern DisallowAlias, patternErrorToRpcError,
+    pattern DisallowAlias,
  )
 import Booster.Syntax.ParsedKore (parseKoreModule)
 import Booster.Syntax.ParsedKore.Base hiding (ParsedModule)
@@ -105,7 +106,11 @@ respond stateVar =
             case internalised of
                 Left patternError -> do
                     Log.logDebug $ "Error internalising cterm" <> Text.pack (show patternError)
-                    pure $ Left $ RpcError.backendError $ RpcError.CouldNotVerifyPattern $ patternErrorToRpcError patternError
+                    pure $
+                        Left $
+                            RpcError.backendError $
+                                RpcError.CouldNotVerifyPattern $
+                                    patternErrorToRpcError patternError
                 Right (pat, substitution, unsupported) -> do
                     unless (null unsupported) $ do
                         Log.logWarnNS
@@ -167,11 +172,13 @@ respond stateVar =
 
                 unless (null newModule.sorts) $
                     throwE $
-                        RpcError.InvalidModule . RpcError.ErrorOnly $ "Module introduces new sorts: " <> listNames newModule.sorts
-
+                        RpcError.InvalidModule . RpcError.ErrorOnly $
+                            "Module introduces new sorts: " <> listNames newModule.sorts
+
                 unless (null newModule.symbols) $
                     throwE $
-                        RpcError.InvalidModule . RpcError.ErrorOnly $ "Module introduces new symbols: " <> listNames newModule.symbols
+                        RpcError.InvalidModule . RpcError.ErrorOnly $
+                            "Module introduces new symbols: " <> listNames newModule.symbols
 
                 -- check if we already received a module with this name
                 when nameAsId $
@@ -247,15 +254,23 @@ respond stateVar =
                         "booster"
                         (Log.LevelOther "ErrorDetails")
                         (prettyPattern req.state.term)
-                    pure $ Left $ RpcError.backendError $ RpcError.CouldNotVerifyPattern $ RpcError.ErrorOnly "Error internalising cterm."
-                Left (patternError:_) -> do
+                    pure $
+                        Left $
+                            RpcError.backendError $
+                                RpcError.CouldNotVerifyPattern $
+                                    RpcError.ErrorOnly "Error internalising cterm."
+                Left (patternError : _) -> do
                     Log.logErrorNS "booster" $
                         "Error internalising cterm: " <> pack (show patternError)
                     Log.logOtherNS
                         "booster"
                         (Log.LevelOther "ErrorDetails")
                         (prettyPattern req.state.term)
-                    pure $ Left $ RpcError.backendError $ RpcError.CouldNotVerifyPattern $ patternErrorToRpcError patternError
+                    pure $
+                        Left $
+                            RpcError.backendError $
+                                RpcError.CouldNotVerifyPattern $
+                                    patternErrorToRpcError patternError
                 -- term and predicate (pattern)
                 Right (TermAndPredicates pat substitution unsupported) -> do
                     Log.logInfoNS "booster" "Simplifying a pattern"
@@ -353,15 +368,23 @@ respond stateVar =
                             "booster"
                             (Log.LevelOther "ErrorDetails")
                             (prettyPattern req.state.term)
-                        pure $ Left $ RpcError.backendError $ RpcError.CouldNotVerifyPattern $ RpcError.ErrorOnly "Error internalising cterm."
-                    Left (patternError:_) -> do
+                        pure $
+                            Left $
+                                RpcError.backendError $
+                                    RpcError.CouldNotVerifyPattern $
+                                        RpcError.ErrorOnly "Error internalising cterm."
+                    Left (patternError : _) -> do
                         Log.logErrorNS "booster" $
                             "Error internalising cterm: " <> pack (show patternError)
                         Log.logOtherNS
                             "booster"
                             (Log.LevelOther "ErrorDetails")
                             (prettyPattern req.state.term)
-                        pure $ Left $ RpcError.backendError $ RpcError.CouldNotVerifyPattern $ patternErrorToRpcError patternError
+                        pure $
+                            Left $
+                                RpcError.backendError $
+                                    RpcError.CouldNotVerifyPattern $
+                                        patternErrorToRpcError patternError
                     -- various predicates obtained
                     Right things -> do
                         Log.logInfoNS "booster" "get-model request"

diff --git a/library/Booster/JsonRpc/Utils.hs b/library/Booster/JsonRpc/Utils.hs
@@ -34,15 +34,15 @@ import System.Process (readProcessWithExitCode)
 import Booster.Definition.Base qualified as Internal
 import Booster.Prettyprinter
 import Booster.Syntax.Json.Internalise
+import Data.Binary.Builder (fromByteString, fromLazyByteString, toLazyByteString)
+import Data.List (intercalate, intersperse)
 import Data.Map qualified as Map
 import Data.Set qualified as Set
+import Data.Text.Encoding qualified as Text
+import Kore.JsonRpc.Error qualified as RpcError
 import Kore.JsonRpc.Types
 import Kore.Syntax.Json.Types hiding (Left, Right)
 import Prettyprinter qualified as Pretty
-import qualified Kore.JsonRpc.Error as RpcError
-import qualified Data.Text.Encoding as Text
-import Data.List (intercalate, intersperse)
-import Data.Binary.Builder (fromByteString, fromLazyByteString, toLazyByteString)
 
 diffJson :: BS.ByteString -> BS.ByteString -> DiffResult
 diffJson file1 file2 =
@@ -261,16 +261,21 @@ diffBy def pat1 pat2 =
             <> if null u then "" else BS.unlines ("Unsupported parts: " : map Json.encode u)
     internalise =
         either
-            (("Pattern could not be internalised: " <>) . toLazyByteString . prettyRpcErrors . map patternErrorToRpcError)
+            ( ("Pattern could not be internalised: " <>)
+                . toLazyByteString
+                . prettyRpcErrors
+                . map patternErrorToRpcError
+            )
             renderBS
             . runExcept
             . internaliseTermOrPredicate DisallowAlias IgnoreSubsorts Nothing def
     prettyRpcErrors = \case
         [] -> "unknown error"
         [e] -> prettyRpcError e
-        (e:es) -> prettyRpcError e <> "\n" <> prettyRpcErrors es
-    
+        (e : es) -> prettyRpcError e <> "\n" <> prettyRpcErrors es
+
     prettyRpcError RpcError.ErrorWithTermAndContext{error = err, term, context} =
-        Text.encodeUtf8Builder err <> "\n" <>
-        maybe "" ((<> "\n") . fromLazyByteString . Json.encode) term <>
-        maybe "" (mconcat . intersperse ", " . map Text.encodeUtf8Builder) context
+        Text.encodeUtf8Builder err
+            <> "\n"
+            <> maybe "" ((<> "\n") . fromLazyByteString . Json.encode) term
+            <> maybe "" (mconcat . intersperse ", " . map Text.encodeUtf8Builder) context
diff --git a/library/Booster/SMT/Base.hs b/library/Booster/SMT/Base.hs
@@ -14,9 +14,9 @@ import Data.ByteString.Char8 qualified as BS
 import Data.Data (Data)
 import Data.Hashable (Hashable)
 import Data.String
+import Data.Text (Text)
 import GHC.Generics (Generic)
 import Language.Haskell.TH.Syntax (Lift)
-import Data.Text (Text)
 
 {- SMT lib 2 commands and responses
 
@@ -81,7 +81,7 @@ data Response
     = Success -- for command_
     | Sat
     | Unsat
-    | Unknown 
+    | Unknown
     | Values [(SExpr, Value)]
     | ReasonUnknown Text
     | Error BS.ByteString

diff --git a/library/Booster/Syntax/Json/Internalise.hs b/library/Booster/Syntax/Json/Internalise.hs
@@ -67,12 +67,12 @@ import Booster.Pattern.Base qualified as Internal
 import Booster.Pattern.Bool qualified as Internal
 import Booster.Pattern.Util (freeVariables, sortOfTerm, substituteInSort)
 import Booster.Prettyprinter (renderDefault)
+import Booster.Syntax.Json (addHeader)
 import Booster.Syntax.Json.Externalise (externaliseSort)
 import Booster.Syntax.ParsedKore.Parser (parsePattern)
 import Booster.Util (Flag (..))
+import Kore.JsonRpc.Error qualified as RpcError
 import Kore.Syntax.Json.Types qualified as Syntax
-import qualified Kore.JsonRpc.Error as RpcError
-import Booster.Syntax.Json (addHeader)
 
 pattern IsQQ, IsNotQQ :: Flag "qq"
 pattern IsQQ = Flag True
@@ -652,37 +652,36 @@ while the context provides the pattern where the error occurred.
 -}
 patternErrorToRpcError :: PatternError -> RpcError.ErrorWithTermAndContext
 patternErrorToRpcError = \case
-        NotSupported p ->
-            wrap "Pattern not supported" p
-        NoTermFound p ->
-            wrap "Pattern must contain at least one term" p
-        PatternSortError p sortErr ->
-            wrap (renderSortError sortErr) p
-        InconsistentPattern p ->
-            wrap "Inconsistent pattern" p
-        TermExpected p ->
-            wrap "Expected a term but found a predicate" p
-        PredicateExpected p ->
-            wrap "Expected a predicate but found a term" p
-        UnknownSymbol sym p ->
-            wrap ("Unknown symbol '" <> Syntax.getId sym <> "'") p
-        MacroOrAliasSymbolNotAllowed sym p ->
-            wrap ("Symbol '" <> Syntax.getId sym <> "' is a macro/alias") p
-        SubstitutionNotAllowed -> RpcError.ErrorOnly "Substitution predicates are not allowed here"
-        IncorrectSymbolArity p s expected got ->
-            wrap
-                ( "Inconsistent pattern. Symbol '"
-                    <> Syntax.getId s
-                    <> "' expected "
-                    <> (pack $ show expected)
-                    <> " arguments but got "
-                    <> (pack $ show got)
-                )
-                p
-      where
-        wrap :: Text -> Syntax.KorePattern -> RpcError.ErrorWithTermAndContext
-        wrap err p = RpcError.ErrorWithTerm err $ addHeader p
-
+    NotSupported p ->
+        wrap "Pattern not supported" p
+    NoTermFound p ->
+        wrap "Pattern must contain at least one term" p
+    PatternSortError p sortErr ->
+        wrap (renderSortError sortErr) p
+    InconsistentPattern p ->
+        wrap "Inconsistent pattern" p
+    TermExpected p ->
+        wrap "Expected a term but found a predicate" p
+    PredicateExpected p ->
+        wrap "Expected a predicate but found a term" p
+    UnknownSymbol sym p ->
+        wrap ("Unknown symbol '" <> Syntax.getId sym <> "'") p
+    MacroOrAliasSymbolNotAllowed sym p ->
+        wrap ("Symbol '" <> Syntax.getId sym <> "' is a macro/alias") p
+    SubstitutionNotAllowed -> RpcError.ErrorOnly "Substitution predicates are not allowed here"
+    IncorrectSymbolArity p s expected got ->
+        wrap
+            ( "Inconsistent pattern. Symbol '"
+                <> Syntax.getId s
+                <> "' expected "
+                <> (pack $ show expected)
+                <> " arguments but got "
+                <> (pack $ show got)
+            )
+            p
+  where
+    wrap :: Text -> Syntax.KorePattern -> RpcError.ErrorWithTermAndContext
+    wrap err p = RpcError.ErrorWithTerm err $ addHeader p
 
 data SortError
     = UnknownSort Syntax.Sort

diff --git a/library/Booster/Syntax/ParsedKore/Internalise.hs b/library/Booster/Syntax/ParsedKore/Internalise.hs
@@ -60,9 +60,9 @@ import Booster.Syntax.Json.Internalise
 import Booster.Syntax.ParsedKore.Base
 import Booster.Syntax.ParsedKore.Parser (ParsedSentence (SentenceSymbol), parseSentence)
 import Booster.Util (Flag (..))
+import Kore.JsonRpc.Error qualified as RpcError
 import Kore.Syntax.Json.Types (Id, Sort)
 import Kore.Syntax.Json.Types qualified as Syntax
-import qualified Kore.JsonRpc.Error as RpcError
 
 {- | Traverses all modules of a parsed definition, to build internal
 @KoreDefinition@s for each of the modules (when used as the main
@@ -1337,8 +1337,11 @@ definitionErrorToRpcError = \case
     DuplicateAliases aliases ->
         "DuplicateAliases" `withContext` map (.name.getId) aliases
     DefinitionPatternError ref patErr ->
-        let err@RpcError.ErrorWithTermAndContext{context} = patternErrorToRpcError patErr in
-            err{RpcError.context = Just $ "Pattern error at " <> render ref <> " in definition": fromMaybe [] context}
+        let err@RpcError.ErrorWithTermAndContext{context} = patternErrorToRpcError patErr
+         in err
+                { RpcError.context =
+                    Just $ "Pattern error at " <> render ref <> " in definition" : fromMaybe [] context
+                }
     DefinitionAxiomError (MalformedRewriteRule rule) ->
         "Malformed rewrite rule" `withContext` [renderOneLineText $ location rule]
     DefinitionAxiomError (MalformedEquation rule) ->
@@ -1347,7 +1350,7 @@ definitionErrorToRpcError = \case
         "Unknown kind of axiom" `withContext` [renderOneLineText $ location rule]
     other ->
         RpcError.ErrorOnly $ render other
-    where
+  where
     withContext :: Text -> [Text] -> RpcError.ErrorWithTermAndContext
     withContext = RpcError.ErrorWithContext
 
@@ -1358,7 +1361,6 @@ definitionErrorToRpcError = \case
         either (const "unknown location") pretty $
             runExcept (Attributes.readLocation rule.attributes)
 
-
 data AliasError
     = UnknownAlias AliasName
     | WrongAliasSortCount ParsedAlias