From 2de865548416d072378487111e7b462b21cc256c Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Tue, 3 Sep 2024 15:53:18 -0700 Subject: [PATCH] KD: Add flush, and capture sorry better --- Data/SBV/Tools/KDKernel.hs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Data/SBV/Tools/KDKernel.hs b/Data/SBV/Tools/KDKernel.hs index fc1e6de3f..82389def6 100644 --- a/Data/SBV/Tools/KDKernel.hs +++ b/Data/SBV/Tools/KDKernel.hs @@ -26,7 +26,9 @@ module Data.SBV.Tools.KDKernel ( , sorry ) where -import Data.List (intercalate, nub, sort) +import Data.List (intercalate, nub, sort) + +import System.IO (hFlush, stdout) import Data.SBV import Data.SBV.Core.Data (Constraint) @@ -53,6 +55,7 @@ data Provenance = FromSorry String -- ^ From a call to 'sorry' -- | Start a proof. We return the number of characters we printed, so the finisher can align the result. start :: Bool -> String -> [String] -> IO Int start newLine what nms = do putStr $ line ++ if newLine then "\n" else "" + hFlush stdout return (length line) where tab = 2 * length (drop 1 nms) indent = replicate tab ' ' @@ -73,7 +76,7 @@ finish origin parents skip = putStrLn $ replicate (ribbonLength - skip) ' ' ++ w FromAxiom _ -> "Admitted." FromLemma _ -> case [nm | FromSorry nm <- parents] of [] -> "Q.E.D." - xs -> "Blindly believed. [Due to: " ++ unwords xs ++ "]" + xs -> "Q.E.D. [Modulo: " ++ intercalate ", " xs ++ "]" -- | A proven property. This type is left abstract, i.e., the only way to create on is via a -- call to 'lemma'/'theorem' etc., ensuring soundness. (Note that the trusted-code base here