Format with fourmolu

booster/library/Booster/SMT/Interface.hs

@@ -515,6 +515,6 @@ closureOver atoms exprs = loop mempty exprs atoms
     loop acc exprs' currentAtoms =
         let (addedExprs, rest) = Set.partition (Set.null . Set.intersection currentAtoms . smtVars) exprs'
             newAtoms = Set.unions $ Set.map smtVars addedExprs
-        in if Set.null addedExprs
-               then acc
-               else loop (acc <> addedExprs) rest newAtoms
+         in if Set.null addedExprs
+                then acc
+                else loop (acc <> addedExprs) rest newAtoms

kore/src/Kore/Rewrite/SMT/Evaluator.hs

@@ -112,7 +112,11 @@ evalPredicate onUnknown predicate sideConditionM = case predicate of
         Nothing ->
             decidePredicate onUnknown SideCondition.top [] predicate
         Just sideCondition ->
-            decidePredicate onUnknown sideCondition (Predicate.getMultiAndPredicate $ from @_ @(Predicate _) sideCondition) predicate
+            decidePredicate
+                onUnknown
+                sideCondition
+                (Predicate.getMultiAndPredicate $ from @_ @(Predicate _) sideCondition)
+                predicate
 
 {- | Attempt to evaluate the 'Conditional' argument with an optional side
  condition using an external SMT solver.
@@ -193,11 +197,12 @@ decidePredicate onUnknown sideCondition sideConditionPredicates predicate =
     query = onErrorUnknown $ SMT.withSolver . evalTranslator $ do
         tools <- Simplifier.askMetadataTools
         Morph.hoist SMT.liftSMT $ do
-            sideConditionPredicates' <- concatMap SMT.splitAnd <$>
-                traverse
-                    (translatePredicate sideCondition tools)
-                    sideConditionPredicates
-            predicate' <- SMT.splitAnd <$> translatePredicate sideCondition tools predicate 
+            sideConditionPredicates' <-
+                concatMap SMT.splitAnd
+                    <$> traverse
+                        (translatePredicate sideCondition tools)
+                        sideConditionPredicates
+            predicate' <- SMT.splitAnd <$> translatePredicate sideCondition tools predicate
             let predicates' = SMT.transitiveClosure (Set.fromList predicate') $ Set.fromList sideConditionPredicates'
             -- when (Set.fromList predicate' /= predicates') $ liftIO $ do
             --     putStrLn $ "predicate: " <> show (Set.fromList predicate')

kore/src/SMT/Utils.hs

@@ -1,4 +1,5 @@
 module SMT.Utils (module SMT.Utils) where
+
 import Data.Set (Set)
 import Data.Set qualified as Set
 import Data.Text (Text, isPrefixOf, isSuffixOf)
@@ -8,21 +9,22 @@ import SMT qualified
 
 splitAnd :: SMT.SExpr -> [SMT.SExpr]
 splitAnd = \case
-  SMT.List (SMT.Atom "and": xs) -> concatMap splitAnd xs
-  other -> [other]
+    SMT.List (SMT.Atom "and" : xs) -> concatMap splitAnd xs
+    other -> [other]
 
 varAtoms :: SMT.SExpr -> Set Text
 varAtoms = \case
-  SMT.Atom a
-    | "<" `isPrefixOf` a && ">" `isSuffixOf` a -> Set.singleton a
-    | otherwise -> mempty
-  SMT.List xs -> mconcat $ map varAtoms xs
-  _ -> mempty
+    SMT.Atom a
+        | "<" `isPrefixOf` a && ">" `isSuffixOf` a -> Set.singleton a
+        | otherwise -> mempty
+    SMT.List xs -> mconcat $ map varAtoms xs
+    _ -> mempty
 
-transitiveClosure :: Set SMT.SExpr ->  Set SMT.SExpr ->  Set SMT.SExpr
+transitiveClosure :: Set SMT.SExpr -> Set SMT.SExpr -> Set SMT.SExpr
 transitiveClosure cl' rest' = loop (Set.unions (Set.map varAtoms cl')) cl' rest'
   where
-    loop clVars cl rest = 
-      let (nonCommon, common) = Set.partition (null . Set.intersection clVars . varAtoms) rest in
-        if null common then cl else 
-          loop (clVars <> Set.unions (Set.map varAtoms common)) (cl <> common) nonCommon
+    loop clVars cl rest =
+        let (nonCommon, common) = Set.partition (null . Set.intersection clVars . varAtoms) rest
+         in if null common
+                then cl
+                else loop (clVars <> Set.unions (Set.map varAtoms common)) (cl <> common) nonCommon