Skip to content

Commit d0c19f0

Browse files
author
github-actions
committed
Format with fourmolu
1 parent b836ce9 commit d0c19f0

File tree

6 files changed

+150
-137
lines changed

6 files changed

+150
-137
lines changed

‎booster/library/Booster/CLOptions.hs

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -403,11 +403,11 @@ parseRewriteOptions =
403403
)
404404
<*> optional
405405
( option
406-
(intWith (> 0))
407-
( metavar "DEPTH"
408-
<> long "simplify-each"
409-
<> help "If given: Simplify the term each time the given rewrite depth is reached"
410-
)
406+
(intWith (> 0))
407+
( metavar "DEPTH"
408+
<> long "simplify-each"
409+
<> help "If given: Simplify the term each time the given rewrite depth is reached"
410+
)
411411
)
412412
where
413413
readCellName :: String -> Either String Text
@@ -425,14 +425,13 @@ parseRewriteOptions =
425425
intWith :: Integral i => (Integer -> Bool) -> ReadM i
426426
intWith p =
427427
auto >>= \case
428-
i
429-
| not (p i) -> readerError $ show i <> ": Invalid integer value."
430-
| otherwise -> pure (fromIntegral i)
428+
i
429+
| not (p i) -> readerError $ show i <> ": Invalid integer value."
430+
| otherwise -> pure (fromIntegral i)
431431

432432
nonnegativeInt :: Integral i => ReadM i
433433
nonnegativeInt = intWith (>= 0)
434434

435-
436435
versionInfoParser :: Parser (a -> a)
437436
versionInfoParser =
438437
infoOption

‎booster/library/Booster/JsonRpc.hs

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -154,7 +154,17 @@ respond stateVar request =
154154

155155
solver <- maybe (SMT.noSolver) (SMT.initSolver def) mSMTOptions
156156
result <-
157-
performRewrite doTracing def mLlvmLibrary solver substVars mbDepth cutPoints terminals rewriteOpts.interimSimplification substPat
157+
performRewrite
158+
doTracing
159+
def
160+
mLlvmLibrary
161+
solver
162+
substVars
163+
mbDepth
164+
cutPoints
165+
terminals
166+
rewriteOpts.interimSimplification
167+
substPat
158168
SMT.finaliseSolver solver
159169
stop <- liftIO $ getTime Monotonic
160170
let duration =

‎booster/library/Booster/Pattern/Rewrite.hs

Lines changed: 102 additions & 101 deletions
Original file line numberDiff line numberDiff line change
@@ -805,114 +805,115 @@ performRewrite doTracing def mLlvmLibrary smtSolver varsToAvoid mbMaxDepth cutLa
805805
logDepth $ showCounter counter
806806

807807
case counter of
808-
c | depthReached c -> do
808+
c
809+
| depthReached c -> do
809810
logDepth $ "Reached maximum depth of " <> maybe "?" showCounter mbMaxDepth
810811
(if wasSimplified then pure else simplifyResult pat') $ RewriteFinished Nothing Nothing pat'
811-
| counter > 0
812-
, not wasSimplified
813-
, maybe False ((== 0) . (counter `mod`)) mbSimplify -> do
812+
| counter > 0
813+
, not wasSimplified
814+
, maybe False ((== 0) . (counter `mod`)) mbSimplify -> do
814815
logDepth $ "Interim simplification after " <> maybe "??" showCounter mbSimplify
815816
simplifyP pat' >>= \case
816817
Nothing -> pure $ RewriteTrivial pat'
817818
Just newPat -> doSteps True newPat
818-
| otherwise ->
819-
runRewriteT
820-
doTracing
821-
def
822-
mLlvmLibrary
823-
smtSolver
824-
varsToAvoid
825-
simplifierCache
826-
(withPatternContext pat' $ rewriteStep cutLabels terminalLabels pat')
827-
>>= \case
828-
Right (RewriteFinished mlbl mUniqueId single, cache) -> do
829-
whenJust mlbl $ \lbl ->
830-
whenJust mUniqueId $ \uniqueId ->
831-
emitRewriteTrace $ RewriteSingleStep lbl uniqueId pat' single
832-
updateCache cache
833-
incrementCounter
834-
doSteps False single
835-
Right (terminal@(RewriteTerminal lbl uniqueId single), _cache) -> withPatternContext pat' $ do
836-
emitRewriteTrace $ RewriteSingleStep lbl uniqueId pat' single
837-
incrementCounter
838-
simplifyResult pat' terminal
839-
Right (branching@RewriteBranch{}, cache) -> do
840-
logMessage $ "Stopped due to branching after " <> showCounter counter
841-
updateCache cache
842-
simplified <- withPatternContext pat' $ simplifyResult pat' branching
843-
case simplified of
844-
RewriteStuck{} -> withPatternContext pat' $ do
845-
logMessage ("Rewrite stuck after pruning branches" :: Text)
846-
pure simplified
847-
RewriteTrivial{} -> withPatternContext pat' $ do
848-
logMessage $ "Simplified to bottom after " <> showCounter counter
849-
pure simplified
850-
RewriteFinished mlbl mUniqueId single -> do
851-
logMessage ("All but one branch pruned, continuing" :: Text)
852-
whenJust mlbl $ \lbl ->
853-
whenJust mUniqueId $ \uniqueId ->
854-
emitRewriteTrace $ RewriteSingleStep lbl uniqueId pat' single
855-
incrementCounter
856-
doSteps False single
857-
RewriteBranch pat'' branches -> withPatternContext pat' $ do
858-
emitRewriteTrace $ RewriteBranchingStep pat'' $ fmap (\(lbl, uid, _) -> (lbl, uid)) branches
859-
pure simplified
860-
_other -> withPatternContext pat' $ error "simplifyResult: Unexpected return value"
861-
Right (cutPoint@(RewriteCutPoint lbl _ _ _), _) -> withPatternContext pat' $ do
862-
simplified <- simplifyResult pat' cutPoint
863-
case simplified of
864-
RewriteCutPoint{} ->
865-
logMessage $ "Cut point " <> lbl <> " after " <> showCounter counter
866-
RewriteStuck{} ->
867-
logMessage $ "Stuck after " <> showCounter counter
868-
RewriteTrivial{} ->
869-
logMessage $ "Simplified to bottom after " <> showCounter counter
870-
_other -> error "simplifyResult: Unexpected return value"
871-
pure simplified
872-
Right (stuck@RewriteStuck{}, cache) -> do
873-
logMessage $ "Stopped after " <> showCounter counter
874-
updateCache cache
875-
emitRewriteTrace $ RewriteStepFailed $ NoApplicableRules pat'
876-
if wasSimplified
877-
then pure stuck
878-
else withSimplified pat' "Retrying with simplified pattern" (doSteps True)
879-
Right (trivial@RewriteTrivial{}, _) -> withPatternContext pat' $ do
880-
logMessage $ "Simplified to bottom after " <> showCounter counter
881-
pure trivial
882-
Right (aborted@RewriteAborted{}, _) -> withPatternContext pat' $ do
883-
logMessage $ "Aborted after " <> showCounter counter
884-
simplifyResult pat' aborted
885-
-- if unification was unclear and the pattern was
886-
-- unsimplified, simplify and retry rewriting once
887-
Left failure@(RuleApplicationUnclear rule _ remainder)
888-
| not wasSimplified -> do
889-
emitRewriteTrace $ RewriteStepFailed failure
890-
-- simplify remainders, substitute and rerun.
891-
-- If failed, do the pattern-wide simplfication and rerun again
892-
withSimplified pat' "Retrying with simplified pattern" (doSteps True)
893-
| otherwise -> do
894-
-- was already simplified, emit an abort log entry
895-
withRuleContext rule . withContext CtxMatch . withContext CtxAbort $
896-
getPrettyModifiers >>= \case
897-
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) ->
898-
logMessage $
899-
WithJsonMessage (object ["remainder" .= (bimap externaliseTerm externaliseTerm <$> remainder)]) $
900-
renderOneLineText $
901-
"Uncertain about match with rule. Remainder:"
902-
<+> ( hsep $
903-
punctuate comma $
904-
map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $
905-
NE.toList remainder
906-
)
907-
emitRewriteTrace $ RewriteStepFailed failure
819+
| otherwise ->
820+
runRewriteT
821+
doTracing
822+
def
823+
mLlvmLibrary
824+
smtSolver
825+
varsToAvoid
826+
simplifierCache
827+
(withPatternContext pat' $ rewriteStep cutLabels terminalLabels pat')
828+
>>= \case
829+
Right (RewriteFinished mlbl mUniqueId single, cache) -> do
830+
whenJust mlbl $ \lbl ->
831+
whenJust mUniqueId $ \uniqueId ->
832+
emitRewriteTrace $ RewriteSingleStep lbl uniqueId pat' single
833+
updateCache cache
834+
incrementCounter
835+
doSteps False single
836+
Right (terminal@(RewriteTerminal lbl uniqueId single), _cache) -> withPatternContext pat' $ do
837+
emitRewriteTrace $ RewriteSingleStep lbl uniqueId pat' single
838+
incrementCounter
839+
simplifyResult pat' terminal
840+
Right (branching@RewriteBranch{}, cache) -> do
841+
logMessage $ "Stopped due to branching after " <> showCounter counter
842+
updateCache cache
843+
simplified <- withPatternContext pat' $ simplifyResult pat' branching
844+
case simplified of
845+
RewriteStuck{} -> withPatternContext pat' $ do
846+
logMessage ("Rewrite stuck after pruning branches" :: Text)
847+
pure simplified
848+
RewriteTrivial{} -> withPatternContext pat' $ do
849+
logMessage $ "Simplified to bottom after " <> showCounter counter
850+
pure simplified
851+
RewriteFinished mlbl mUniqueId single -> do
852+
logMessage ("All but one branch pruned, continuing" :: Text)
853+
whenJust mlbl $ \lbl ->
854+
whenJust mUniqueId $ \uniqueId ->
855+
emitRewriteTrace $ RewriteSingleStep lbl uniqueId pat' single
856+
incrementCounter
857+
doSteps False single
858+
RewriteBranch pat'' branches -> withPatternContext pat' $ do
859+
emitRewriteTrace $ RewriteBranchingStep pat'' $ fmap (\(lbl, uid, _) -> (lbl, uid)) branches
860+
pure simplified
861+
_other -> withPatternContext pat' $ error "simplifyResult: Unexpected return value"
862+
Right (cutPoint@(RewriteCutPoint lbl _ _ _), _) -> withPatternContext pat' $ do
863+
simplified <- simplifyResult pat' cutPoint
864+
case simplified of
865+
RewriteCutPoint{} ->
866+
logMessage $ "Cut point " <> lbl <> " after " <> showCounter counter
867+
RewriteStuck{} ->
868+
logMessage $ "Stuck after " <> showCounter counter
869+
RewriteTrivial{} ->
870+
logMessage $ "Simplified to bottom after " <> showCounter counter
871+
_other -> error "simplifyResult: Unexpected return value"
872+
pure simplified
873+
Right (stuck@RewriteStuck{}, cache) -> do
874+
logMessage $ "Stopped after " <> showCounter counter
875+
updateCache cache
876+
emitRewriteTrace $ RewriteStepFailed $ NoApplicableRules pat'
877+
if wasSimplified
878+
then pure stuck
879+
else withSimplified pat' "Retrying with simplified pattern" (doSteps True)
880+
Right (trivial@RewriteTrivial{}, _) -> withPatternContext pat' $ do
881+
logMessage $ "Simplified to bottom after " <> showCounter counter
882+
pure trivial
883+
Right (aborted@RewriteAborted{}, _) -> withPatternContext pat' $ do
908884
logMessage $ "Aborted after " <> showCounter counter
909-
pure (RewriteAborted failure pat')
910-
Left failure -> do
911-
emitRewriteTrace $ RewriteStepFailed failure
912-
let msg = "Aborted after " <> showCounter counter
913-
if wasSimplified
914-
then logMessage msg >> pure (RewriteAborted failure pat')
915-
else withSimplified pat' msg (pure . RewriteAborted failure)
885+
simplifyResult pat' aborted
886+
-- if unification was unclear and the pattern was
887+
-- unsimplified, simplify and retry rewriting once
888+
Left failure@(RuleApplicationUnclear rule _ remainder)
889+
| not wasSimplified -> do
890+
emitRewriteTrace $ RewriteStepFailed failure
891+
-- simplify remainders, substitute and rerun.
892+
-- If failed, do the pattern-wide simplfication and rerun again
893+
withSimplified pat' "Retrying with simplified pattern" (doSteps True)
894+
| otherwise -> do
895+
-- was already simplified, emit an abort log entry
896+
withRuleContext rule . withContext CtxMatch . withContext CtxAbort $
897+
getPrettyModifiers >>= \case
898+
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) ->
899+
logMessage $
900+
WithJsonMessage (object ["remainder" .= (bimap externaliseTerm externaliseTerm <$> remainder)]) $
901+
renderOneLineText $
902+
"Uncertain about match with rule. Remainder:"
903+
<+> ( hsep $
904+
punctuate comma $
905+
map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $
906+
NE.toList remainder
907+
)
908+
emitRewriteTrace $ RewriteStepFailed failure
909+
logMessage $ "Aborted after " <> showCounter counter
910+
pure (RewriteAborted failure pat')
911+
Left failure -> do
912+
emitRewriteTrace $ RewriteStepFailed failure
913+
let msg = "Aborted after " <> showCounter counter
914+
if wasSimplified
915+
then logMessage msg >> pure (RewriteAborted failure pat')
916+
else withSimplified pat' msg (pure . RewriteAborted failure)
916917
where
917918
withSimplified p msg cont = do
918919
(withPatternContext p $ simplifyP p) >>= \case

‎booster/tools/booster/Server.hs

Lines changed: 10 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -126,15 +126,16 @@ main = do
126126
, mainModuleName
127127
, port
128128
, llvmLibraryFile
129-
, logOptions = LogOptions
130-
{ logLevels
131-
, logFormat
132-
, logTimeStamps
133-
, timeStampsFormat
134-
, logContexts
135-
, logFile
136-
, prettyPrintOptions
137-
}
129+
, logOptions =
130+
LogOptions
131+
{ logLevels
132+
, logFormat
133+
, logTimeStamps
134+
, timeStampsFormat
135+
, logContexts
136+
, logFile
137+
, prettyPrintOptions
138+
}
138139
, smtOptions
139140
, equationOptions
140141
, rewriteOptions

‎dev-tools/booster-dev/Server.hs

Lines changed: 10 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -52,15 +52,16 @@ main = do
5252
, mainModuleName
5353
, llvmLibraryFile
5454
, port
55-
, logOptions = LogOptions
56-
{ logLevels
57-
, logContexts
58-
, logTimeStamps
59-
, timeStampsFormat
60-
, logFormat
61-
, logFile
62-
, prettyPrintOptions
63-
}
55+
, logOptions =
56+
LogOptions
57+
{ logLevels
58+
, logContexts
59+
, logTimeStamps
60+
, timeStampsFormat
61+
, logFormat
62+
, logFile
63+
, prettyPrintOptions
64+
}
6465
, smtOptions
6566
, equationOptions
6667
, rewriteOptions

0 commit comments

Comments
 (0)