Simplify some obligation-proving code

GaloisInc · Jun 25, 2024 · 6beaf4f · 6beaf4f
1 parent ae52603
commit 6beaf4f
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 16 deletions.
diff --git 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
@@ -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