From 6beaf4f3a163c7860920199a97987ab3b9dbf446 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Tue, 25 Jun 2024 12:01:58 -0400
Subject: [PATCH] Simplify some obligation-proving code

---
 crucible-cli/src/Lang/Crucible/CLI.hs         | 21 +++++++++++--------
 .../src/Lang/Crucible/Syntax/Overrides.hs     | 16 +++++++-------
 2 files changed, 21 insertions(+), 16 deletions(-)

diff --git a/crucible-cli/src/Lang/Crucible/CLI.hs b/crucible-cli/src/Lang/Crucible/CLI.hs
index bcfbb27bf..3ad8171c5 100644
--- a/crucible-cli/src/Lang/Crucible/CLI.hs
+++ b/crucible-cli/src/Lang/Crucible/CLI.hs
@@ -187,15 +187,18 @@ simulateProgramWithExtension mkExt fn theInput outh profh opts hooks =
                        let timeout = CTO.Timeout (Sec.secondsFromInt 5)
                        let prover = Prove.offlineProver timeout sym defaultLogData z3Adapter
                        let strat = Prove.ProofStrategy prover Prove.keepGoing
-                       merr <- runExceptT $ Prove.proveCurrentObligations bak strat $ Prove.ProofConsumer $ \goal res -> do
-                         hPrint outh =<< ppProofObligation sym goal
-                         case res of
-                           Prove.Proved {} -> hPutStrLn outh "PROVED"
-                           Prove.Disproved {} -> hPutStrLn outh "COUNTEREXAMPLE"
-                           Prove.Unknown {} -> hPutStrLn outh "UNKNOWN"
-                       case merr of
-                         Left CTO.TimedOut -> hPutStrLn outh $ unlines ["TIMEOUT"]
-                         Right () -> pure ()
+                       let ppResult =
+                             \case
+                               Prove.Proved {} ->  "PROVED"
+                               Prove.Disproved {} -> "COUNTEREXAMPLE"
+                               Prove.Unknown {} -> "UNKNOWN"
+                       let printer = Prove.ProofConsumer $ \goal res -> do
+                             hPrint outh =<< ppProofObligation sym goal
+                             hPutStrLn outh (ppResult res)
+                       runExceptT (Prove.proveCurrentObligations bak strat printer) >>=
+                         \case
+                           Left CTO.TimedOut -> hPutStrLn outh "TIMEOUT"
+                           Right () -> pure ()
 
                   _ -> hPutStrLn outh "No suitable main function found"
 
diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs
index e9a293149..0645296f2 100644
--- a/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs
+++ b/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs
@@ -54,13 +54,15 @@ proveObligations =
        let timeout = CTO.Timeout (Sec.secondsFromInt 5)
        let prover = CB.offlineProver timeout sym logData z3Adapter
        let strat = CB.ProofStrategy prover CB.keepGoing
-       merr <- runExceptT $ CB.proveCurrentObligations bak strat $ CB.ProofConsumer $ \o ->
+       let ppResult o =
+             \case
+               CB.Proved {}  -> unlines ["Proof Succeeded!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
+               CB.Disproved {} -> unlines ["Proof failed!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
+               CB.Unknown {} -> unlines ["Proof inconclusive!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
+       let printer = CB.ProofConsumer $ \o r -> hPutStrLn h (ppResult o r)
+       runExceptT (CB.proveCurrentObligations bak strat printer) >>=
          \case
-           CB.Proved {}  -> hPutStrLn h $ unlines ["Proof Succeeded!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
-           CB.Disproved {} -> hPutStrLn h $ unlines ["Proof failed!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
-           CB.Unknown {} -> hPutStrLn h $ unlines ["Proof inconclusive!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
-       case merr of
-         Left CTO.TimedOut -> hPutStrLn h $ unlines ["Proof timed out!"]
-         Right () -> pure ()
+           Left CTO.TimedOut -> hPutStrLn h $ unlines ["Proof timed out!"]
+           Right () -> pure ()
 
        clearProofObligations bak