format and fix minor bugs

runtimeverification · Apr 9, 2024 · 215fa27 · 215fa27
1 parent 4d58673
commit 215fa27
Show file tree

Hide file tree

Showing 6 changed files with 138 additions and 74 deletions.
diff --git a/library/Booster/Definition/Attributes/Base.hs b/library/Booster/Definition/Attributes/Base.hs
@@ -156,7 +156,7 @@ data Concreteness
     deriving stock (Eq, Ord, Show, Generic)
     deriving anyclass (NFData)
 
-data FunctionType = Partial | Total 
+data FunctionType = Partial | Total
     deriving stock (Eq, Ord, Show, Generic, Data, Lift)
     deriving anyclass (NFData, Hashable)
 

diff --git a/library/Booster/Definition/Ceil.hs b/library/Booster/Definition/Ceil.hs
@@ -143,7 +143,8 @@ computeCeilRule mllvm def [email protected]{lhs, requires, rhs, attribut
 
 computeCeil :: MonadLoggerIO io => Term -> EquationT io [Either Predicate Term]
 computeCeil term@(SymbolApplication symbol _ args)
-    | symbol.attributes.symbolType /= Booster.Definition.Attributes.Base.Function Booster.Definition.Attributes.Base.Partial =
+    | symbol.attributes.symbolType
+        /= Booster.Definition.Attributes.Base.Function Booster.Definition.Attributes.Base.Partial =
         concatMapM computeCeil args
     | otherwise = do
         ceils <- (.definition.ceils) <$> getConfig

diff --git a/library/Booster/Pattern/Base.hs b/library/Booster/Pattern/Base.hs
@@ -13,6 +13,7 @@ module Booster.Pattern.Base (
 ) where
 
 import Booster.Definition.Attributes.Base (
+    FunctionType (..),
     KCollectionMetadata (..),
     KCollectionSymbolNames (..),
     KListDefinition (..),
@@ -24,7 +25,7 @@ import Booster.Definition.Attributes.Base (
     pattern IsAssoc,
     pattern IsNotAssoc,
     pattern IsNotIdem,
-    pattern IsNotMacroOrAlias, FunctionType (..),
+    pattern IsNotMacroOrAlias,
  )
 import Booster.Prettyprinter qualified as KPretty
 
@@ -848,12 +849,16 @@ instance Pretty Pattern where
                 <> fmap (Pretty.indent 4 . pretty) (Set.toList patt.constraints)
                 <> fmap (Pretty.indent 4 . pretty) patt.ceilConditions
 
-
-
 pattern ConsApplication :: Symbol -> [Sort] -> [Term] -> Term
-pattern ConsApplication sym sorts args <- Term _ (SymbolApplicationF sym@(Symbol _ _ _ _ (SymbolAttributes{symbolType = Constructor})) sorts args)
+pattern ConsApplication sym sorts args <-
+    Term
+        _
+        (SymbolApplicationF sym@(Symbol _ _ _ _ (SymbolAttributes{symbolType = Constructor})) sorts args)
 
 pattern FunctionApplication :: Symbol -> [Sort] -> [Term] -> Term
-pattern FunctionApplication sym sorts args <- Term _ (SymbolApplicationF sym@(Symbol _ _ _ _ (SymbolAttributes{symbolType = Function _})) sorts args)
+pattern FunctionApplication sym sorts args <-
+    Term
+        _
+        (SymbolApplicationF sym@(Symbol _ _ _ _ (SymbolAttributes{symbolType = Function _})) sorts args)
 
 {-# COMPLETE AndTerm, ConsApplication, FunctionApplication, DomainValue, Var, Injection, KMap, KList, KSet #-}
diff --git a/library/Booster/Pattern/Bool.hs b/library/Booster/Pattern/Bool.hs
@@ -26,13 +26,14 @@ module Booster.Pattern.Bool (
 import Data.ByteString.Char8 (ByteString)
 
 import Booster.Definition.Attributes.Base (
+    FunctionType (..),
     SMTType (SMTHook),
     SymbolAttributes (SymbolAttributes),
     SymbolType (Function),
     pattern CanBeEvaluated,
     pattern IsNotAssoc,
     pattern IsNotIdem,
-    pattern IsNotMacroOrAlias, FunctionType (..),
+    pattern IsNotMacroOrAlias,
  )
 import Booster.Pattern.Base (
     Pattern,