diff --git a/Data/SBV/Tools/KDKernel.hs b/Data/SBV/Tools/KDKernel.hs index a7a3b315d..da19b7914 100644 --- a/Data/SBV/Tools/KDKernel.hs +++ b/Data/SBV/Tools/KDKernel.hs @@ -27,12 +27,13 @@ module Data.SBV.Tools.KDKernel ( , sorry ) where -import Data.List (intercalate, sort, nub) +import Control.Monad.Trans (liftIO) -import System.IO (hFlush, stdout) +import Data.List (intercalate, sort, nub) import Data.SBV import Data.SBV.Core.Data (Constraint) +import Data.SBV.Tools.KDUtils import qualified Data.SBV.List as SL @@ -62,29 +63,11 @@ data Proven = Proven { rootOfTrust :: RootOfTrust -- ^ Root of trust, described , getProof :: SBool -- ^ Get the underlying boolean } --- | 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 ' ' - tag = what ++ ": " ++ intercalate "." nms - line = indent ++ tag - --- | Finish a proof. First argument is what we got from the call of 'start' above. -finish :: String -> Int -> IO () -finish what skip = do putStrLn $ replicate (ribbonLength - skip) ' ' ++ what - where -- Ideally an aestheticly pleasing length of the line. Perhaps this - -- should be configurable, but this is good enough for now. - ribbonLength :: Int - ribbonLength = 40 - -- | Accept the given definition as a fact. Usually used to introduce definitial axioms, -- giving meaning to uninterpreted symbols. Note that we perform no checks on these propositions, -- if you assert nonsense, then you get nonsense back. So, calls to 'axiom' should be limited to -- definitions, or basic axioms (like commutativity, associativity) of uninterpreted function symbols. -axiom :: Proposition a => String -> a -> IO Proven +axiom :: Proposition a => String -> a -> KD Proven axiom nm p = do start False "Axiom" [nm] >>= finish "Axiom." pure (internalAxiom nm p) { isUserAxiom = True } @@ -114,7 +97,7 @@ sorry = Proven{ rootOfTrust = Self p (Forall (x :: SBool)) = label "SORRY: KnuckleDragger, proof uses \"sorry\"" x -- | Helper to generate lemma/theorem statements. -lemmaGen :: Proposition a => SMTConfig -> String -> [String] -> a -> [Proven] -> IO Proven +lemmaGen :: Proposition a => SMTConfig -> String -> [String] -> a -> [Proven] -> KD Proven lemmaGen cfg what nms inputProp by = do tab <- start (verbose cfg) what nms @@ -142,24 +125,24 @@ lemmaGen cfg what nms inputProp by = do | True = intercalate ", " depNames -- What to do if the proof fails - cex = do putStrLn $ "\n*** Failed to prove " ++ nm ++ "." - -- When trying to get a counter-example, only include in the - -- implication those facts that are user-given axioms. This - -- way our counter-example will be more likely to be relevant - -- to the proposition we're currently proving. (Hopefully.) - -- Remember that we first have to negate, and then skolemize! - SatResult res <- satWith cfg $ do - mapM_ constrain [getProof | Proven{isUserAxiom, getProof} <- by, isUserAxiom] :: Symbolic () - pure $ skolemize (qNot inputProp) - print $ ThmResult res - error "Failed" + cex = liftIO $ do putStrLn $ "\n*** Failed to prove " ++ nm ++ "." + -- When trying to get a counter-example, only include in the + -- implication those facts that are user-given axioms. This + -- way our counter-example will be more likely to be relevant + -- to the proposition we're currently proving. (Hopefully.) + -- Remember that we first have to negate, and then skolemize! + SatResult res <- satWith cfg $ do + mapM_ constrain [getProof | Proven{isUserAxiom, getProof} <- by, isUserAxiom] :: Symbolic () + pure $ skolemize (qNot inputProp) + print $ ThmResult res + error "Failed" -- bailing out - failed r = do putStrLn $ "\n*** Failed to prove " ++ nm ++ "." - print r - error "Failed" + failed r = liftIO $ do putStrLn $ "\n*** Failed to prove " ++ nm ++ "." + print r + error "Failed" - pRes <- proveWith cfg $ do + pRes <- liftIO $ proveWith cfg $ do mapM_ (constrain . getProof) by :: Symbolic () pure $ skolemize (quantifiedBool inputProp) @@ -172,19 +155,19 @@ lemmaGen cfg what nms inputProp by = do ThmResult ProofError{} -> failed pRes -- | Prove a given statement, using auxiliaries as helpers. Using the default solver. -lemma :: Proposition a => String -> a -> [Proven] -> IO Proven +lemma :: Proposition a => String -> a -> [Proven] -> KD Proven lemma = lemmaWith defaultSMTCfg -- | Prove a given statement, using auxiliaries as helpers. Using the given solver. -lemmaWith :: Proposition a => SMTConfig -> String -> a -> [Proven] -> IO Proven +lemmaWith :: Proposition a => SMTConfig -> String -> a -> [Proven] -> KD Proven lemmaWith cfg nm = lemmaGen cfg "Lemma" [nm] -- | Prove a given statement, using auxiliaries as helpers. Essentially the same as 'lemma', except for the name, using the default solver. -theorem :: Proposition a => String -> a -> [Proven] -> IO Proven +theorem :: Proposition a => String -> a -> [Proven] -> KD Proven theorem = theoremWith defaultSMTCfg -- | Prove a given statement, using auxiliaries as helpers. Essentially the same as 'lemmaWith', except for the name. -theoremWith :: Proposition a => SMTConfig -> String -> a -> [Proven] -> IO Proven +theoremWith :: Proposition a => SMTConfig -> String -> a -> [Proven] -> KD Proven theoremWith cfg nm = lemmaGen cfg "Theorem" [nm] -- | Given a predicate, return an induction principle for it. Typically, we only have one viable diff --git a/Data/SBV/Tools/KDUtils.hs b/Data/SBV/Tools/KDUtils.hs new file mode 100644 index 000000000..5a22c2fbe --- /dev/null +++ b/Data/SBV/Tools/KDUtils.hs @@ -0,0 +1,63 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.Tools.KDUtils +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer: erkokl@gmail.com +-- Stability : experimental +-- +-- Various KnuckleDrugger machinery. +----------------------------------------------------------------------------- + +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} + +{-# OPTIONS_GHC -Wall -Werror #-} + +module Data.SBV.Tools.KDUtils ( + KD, runKD, runKDWith + , start, finish + ) where + +import Control.Monad.Reader (ReaderT, runReaderT) +import Control.Monad.Trans (MonadIO(liftIO)) + +import Data.List (intercalate) +import System.IO (hFlush, stdout) + +-- | Keeping track of KD options/state +data KDConfig = KDConfig + +-- | Default KD-config +defaultKDConfig :: KDConfig +defaultKDConfig = KDConfig + +-- | Monad for running KnuckleDragger proofs in. +newtype KD a = KD (ReaderT KDConfig IO a) + deriving newtype (Applicative, Functor, Monad, MonadIO, MonadFail) + +-- | Run a KD proof, using the default configuration. +runKD :: KD a -> IO a +runKD = runKDWith defaultKDConfig + +-- | Run a KD proof, using the given configuration. +runKDWith :: KDConfig -> KD a -> IO a +runKDWith cfg (KD f) = runReaderT f cfg + +-- | Start a proof. We return the number of characters we printed, so the finisher can align the result. +start :: Bool -> String -> [String] -> KD Int +start newLine what nms = liftIO $ do putStr $ line ++ if newLine then "\n" else "" + hFlush stdout + return (length line) + where tab = 2 * length (drop 1 nms) + indent = replicate tab ' ' + tag = what ++ ": " ++ intercalate "." nms + line = indent ++ tag + +-- | Finish a proof. First argument is what we got from the call of 'start' above. +finish :: String -> Int -> KD () +finish what skip = liftIO $ putStrLn $ replicate (ribbonLength - skip) ' ' ++ what + where -- Ideally an aestheticly pleasing length of the line. Perhaps this + -- should be configurable, but this is good enough for now. + ribbonLength :: Int + ribbonLength = 40 diff --git a/Data/SBV/Tools/KnuckleDragger.hs b/Data/SBV/Tools/KnuckleDragger.hs index e39638835..48ff371e4 100644 --- a/Data/SBV/Tools/KnuckleDragger.hs +++ b/Data/SBV/Tools/KnuckleDragger.hs @@ -13,13 +13,15 @@ -- See the directory Documentation.SBV.Examples.KnuckleDragger for various examples. ----------------------------------------------------------------------------- -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE FunctionalDependencies #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE TypeAbstractions #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeAbstractions #-} {-# OPTIONS_GHC -Wall -Werror #-} @@ -38,10 +40,15 @@ module Data.SBV.Tools.KnuckleDragger ( , Induction(..) -- * Faking proofs , sorry + -- * Running KnuckleDragger proofs + , KD, runKD, runKDWith ) where +import Control.Monad.Trans (liftIO) + import Data.SBV import Data.SBV.Tools.KDKernel +import Data.SBV.Tools.KDUtils import Control.Monad(when) @@ -65,16 +72,16 @@ class ChainLemma steps step | steps -> step where -- If there are no helpers given (i.e., if @H@ is empty), then this call is equivalent to 'lemmaWith'. -- If @H@ is a singleton, then we error-out. A single step in @H@ indicates a user-error, since there's -- no sequence of steps to reason about. - chainLemma :: Proposition a => String -> a -> steps -> [Proven] -> IO Proven + chainLemma :: Proposition a => String -> a -> steps -> [Proven] -> KD Proven -- | Same as chainLemma, except tagged as Theorem - chainTheorem :: Proposition a => String -> a -> steps -> [Proven] -> IO Proven + chainTheorem :: Proposition a => String -> a -> steps -> [Proven] -> KD Proven -- | Prove a property via a series of equality steps, using the given solver. - chainLemmaWith :: Proposition a => SMTConfig -> String -> a -> steps -> [Proven] -> IO Proven + chainLemmaWith :: Proposition a => SMTConfig -> String -> a -> steps -> [Proven] -> KD Proven -- | Same as chainLemmaWith, except tagged as Theorem - chainTheoremWith :: Proposition a => SMTConfig -> String -> a -> steps -> [Proven] -> IO Proven + chainTheoremWith :: Proposition a => SMTConfig -> String -> a -> steps -> [Proven] -> KD Proven -- | Internal, shouldn't be needed outside the library makeSteps :: steps -> [step] @@ -86,17 +93,20 @@ class ChainLemma steps step | steps -> step where chainLemmaWith = chainGeneric False chainTheoremWith = chainGeneric True - chainGeneric :: Proposition a => Bool -> SMTConfig -> String -> a -> steps -> [Proven] -> IO Proven + chainGeneric :: Proposition a => Bool -> SMTConfig -> String -> a -> steps -> [Proven] -> KD Proven chainGeneric taggedTheorem cfg nm result steps base = do - putStrLn $ "Chain: " ++ nm + liftIO $ putStrLn $ "Chain: " ++ nm let proofSteps = makeSteps steps len = length proofSteps + when (len == 1) $ error $ unlines $ [ "Incorrect use of chainLemma on " ++ show nm ++ ":" , "** There must be either none, or at least two steps." , "** Was given only one step." ] + go (1 :: Int) base (zipWith (makeInter steps) proofSteps (drop 1 proofSteps)) + where go _ sofar [] | taggedTheorem = theoremWith cfg nm result sofar | True = lemmaWith cfg nm result sofar diff --git a/Documentation/SBV/Examples/KnuckleDragger/AppendRev.hs b/Documentation/SBV/Examples/KnuckleDragger/AppendRev.hs index a2833ab6c..dad1f2d02 100644 --- a/Documentation/SBV/Examples/KnuckleDragger/AppendRev.hs +++ b/Documentation/SBV/Examples/KnuckleDragger/AppendRev.hs @@ -30,6 +30,10 @@ import Data.SBV.Tools.KnuckleDragger import Data.SBV.List ((.:), (++), reverse) import qualified Data.SBV.List as SL +-- $setup +-- >>> -- For doctest purposes only: +-- >>> import Data.SBV.Tools.KnuckleDragger(runKD) + -- | Use an uninterpreted type for the elements data Elt mkUninterpretedSort ''Elt @@ -38,9 +42,9 @@ mkUninterpretedSort ''Elt -- -- We have: -- --- >>> appendNull +-- >>> runKD appendNull -- Lemma: appendNull Q.E.D. -appendNull :: IO Proven +appendNull :: KD Proven appendNull = lemma "appendNull" (\(Forall @"xs" (xs :: SList Elt)) -> xs ++ SL.nil .== xs) [] @@ -49,9 +53,9 @@ appendNull = lemma "appendNull" -- -- We have: -- --- >>> consApp +-- >>> runKD consApp -- Lemma: consApp Q.E.D. -consApp :: IO Proven +consApp :: KD Proven consApp = lemma "consApp" (\(Forall @"x" (x :: SElt)) (Forall @"xs" xs) (Forall @"ys" ys) -> (x .: xs) ++ ys .== x .: (xs ++ ys)) [] @@ -60,9 +64,9 @@ consApp = lemma "consApp" -- -- We have: -- --- >>> appendAssoc +-- >>> runKD appendAssoc -- Lemma: appendAssoc Q.E.D. -appendAssoc :: IO Proven +appendAssoc :: KD Proven appendAssoc = do -- The classic proof by induction on xs let p :: SymVal a => SList a -> SList a -> SList a -> SBool @@ -75,9 +79,9 @@ appendAssoc = do -- | @reverse (xs ++ ys) == reverse ys ++ reverse xs@ -- We have: -- --- >>> revApp +-- >>> runKD revApp -- Lemma: revApp Q.E.D. -revApp :: IO Proven +revApp :: KD Proven revApp = do let q :: SymVal a => SList a -> SList a -> SBool q xs ys = reverse (xs ++ ys) .== reverse ys ++ reverse xs @@ -89,10 +93,10 @@ revApp = do -- -- We have: -- --- >>> reverseReverse +-- >>> runKD reverseReverse -- Lemma: revApp Q.E.D. -- Lemma: reverseReverse Q.E.D. -reverseReverse :: IO Proven +reverseReverse :: KD Proven reverseReverse = do lRevApp <- revApp diff --git a/Documentation/SBV/Examples/KnuckleDragger/Induction.hs b/Documentation/SBV/Examples/KnuckleDragger/Induction.hs index 3d02062a9..eb7ec54a1 100644 --- a/Documentation/SBV/Examples/KnuckleDragger/Induction.hs +++ b/Documentation/SBV/Examples/KnuckleDragger/Induction.hs @@ -21,13 +21,17 @@ import Prelude hiding (sum, length) import Data.SBV import Data.SBV.Tools.KnuckleDragger +-- $setup +-- >>> -- For doctest purposes only: +-- >>> import Data.SBV.Tools.KnuckleDragger(runKD) + -- | Prove that sum of numbers from @0@ to @n@ is @n*(n-1)/2@. -- -- We have: -- --- >>> sumProof +-- >>> runKD sumProof -- Lemma: sum_correct Q.E.D. -sumProof :: IO Proven +sumProof :: KD Proven sumProof = do let sum :: SInteger -> SInteger sum = smtFunction "sum" $ \n -> ite (n .== 0) 0 (n + sum (n - 1)) @@ -44,9 +48,9 @@ sumProof = do -- -- We have: -- --- >>> sumSquareProof +-- >>> runKD sumSquareProof -- Lemma: sumSquare_correct Q.E.D. -sumSquareProof :: IO Proven +sumSquareProof :: KD Proven sumSquareProof = do let sumSquare :: SInteger -> SInteger sumSquare = smtFunction "sumSquare" $ \n -> ite (n .== 0) 0 (n * n + sumSquare (n - 1)) diff --git a/Documentation/SBV/Examples/KnuckleDragger/Kleene.hs b/Documentation/SBV/Examples/KnuckleDragger/Kleene.hs index 2e955ebf5..2f23834ec 100644 --- a/Documentation/SBV/Examples/KnuckleDragger/Kleene.hs +++ b/Documentation/SBV/Examples/KnuckleDragger/Kleene.hs @@ -30,6 +30,10 @@ import Prelude hiding((<=)) import Data.SBV import Data.SBV.Tools.KnuckleDragger +-- $setup +-- >>> -- For doctest purposes only: +-- >>> import Data.SBV.Tools.KnuckleDragger(runKD) + -- | An uninterpreted sort, corresponding to the type of Kleene algebra strings. data Kleene mkUninterpretedSort ''Kleene @@ -61,7 +65,7 @@ x <= y = x + y .== y -- -- We have: -- --- >>> kleeneProofs +-- >>> runKD kleeneProofs -- Axiom: par_assoc Axiom. -- Axiom: par_comm Axiom. -- Axiom: par_idem Axiom. @@ -87,7 +91,7 @@ x <= y = x + y .== y -- Lemma: star_star_2_3 Q.E.D. -- Lemma: star_star_2_1 Q.E.D. -- Lemma: star_star_2 Q.E.D. -kleeneProofs :: IO () +kleeneProofs :: KD () kleeneProofs = do -- Kozen axioms diff --git a/Documentation/SBV/Examples/KnuckleDragger/ListLen.hs b/Documentation/SBV/Examples/KnuckleDragger/ListLen.hs index 2ce5b8a6c..dc0672ad4 100644 --- a/Documentation/SBV/Examples/KnuckleDragger/ListLen.hs +++ b/Documentation/SBV/Examples/KnuckleDragger/ListLen.hs @@ -33,6 +33,7 @@ import qualified Data.SBV.List as SL -- >>> -- For doctest purposes only: -- >>> :set -XScopedTypeVariables -- >>> import Control.Exception +-- >>> import Data.SBV.Tools.KnuckleDragger(runKD) -- | Use an uninterpreted type for the elements data Elt @@ -42,9 +43,9 @@ mkUninterpretedSort ''Elt -- -- We have: -- --- >>> listLengthProof +-- >>> runKD listLengthProof -- Lemma: length_correct Q.E.D. -listLengthProof :: IO Proven +listLengthProof :: KD Proven listLengthProof = do let length :: SList Elt -> SInteger length = smtFunction "length" $ \xs -> ite (SL.null xs) 0 (1 + length (SL.tail xs)) @@ -62,14 +63,14 @@ listLengthProof = do -- and see the counter-example. Our implementation returns an incorrect answer if the given list is longer -- than 5 elements and have 42 in it. We have: -- --- >>> badProof `catch` (\(_ :: SomeException) -> pure ()) +-- >>> runKD badProof `catch` (\(_ :: SomeException) -> pure ()) -- Lemma: bad -- *** Failed to prove bad. -- Falsifiable. Counter-example: -- xs = [8,25,26,27,28,42] :: [Integer] -- imp = 42 :: Integer -- spec = 6 :: Integer -badProof :: IO () +badProof :: KD () badProof = do let length :: SList Integer -> SInteger length = smtFunction "length" $ \xs -> ite (SL.null xs) 0 (1 + length (SL.tail xs)) @@ -91,9 +92,9 @@ badProof = do -- -- We have: -- --- >>> lenAppend +-- >>> runKD lenAppend -- Lemma: lenAppend Q.E.D. -lenAppend :: IO Proven +lenAppend :: KD Proven lenAppend = lemma "lenAppend" (\(Forall @"xs" (xs :: SList Elt)) (Forall @"ys" ys) -> SL.length (xs SL.++ ys) .== SL.length xs + SL.length ys) @@ -103,9 +104,9 @@ lenAppend = lemma "lenAppend" -- -- We have: -- --- >>> lenAppend2 +-- >>> runKD lenAppend2 -- Lemma: lenAppend2 Q.E.D. -lenAppend2 :: IO Proven +lenAppend2 :: KD Proven lenAppend2 = lemma "lenAppend2" (\(Forall @"xs" (xs :: SList Elt)) (Forall @"ys" ys) -> SL.length xs .== SL.length ys diff --git a/Documentation/SBV/Examples/KnuckleDragger/RevLen.hs b/Documentation/SBV/Examples/KnuckleDragger/RevLen.hs index de0e294e6..21484a5d1 100644 --- a/Documentation/SBV/Examples/KnuckleDragger/RevLen.hs +++ b/Documentation/SBV/Examples/KnuckleDragger/RevLen.hs @@ -31,6 +31,7 @@ import Data.SBV.List (reverse, length) -- >>> -- For doctest purposes only: -- >>> :set -XScopedTypeVariables -- >>> import Control.Exception +-- >>> import Data.SBV.Tools.KnuckleDragger(runKD) -- | Use an uninterpreted type for the elements data Elt @@ -40,9 +41,9 @@ mkUninterpretedSort ''Elt -- -- We have: -- --- >>> revLen +-- >>> runKD revLen -- Lemma: revLen Q.E.D. -revLen :: IO Proven +revLen :: KD Proven revLen = do let p :: SList Elt -> SBool p xs = length (reverse xs) .== length xs @@ -58,12 +59,12 @@ revLen = do -- -- We have: -- --- >>> badRevLen `catch` (\(_ :: SomeException) -> pure ()) +-- >>> runKD badRevLen `catch` (\(_ :: SomeException) -> pure ()) -- Lemma: badRevLen -- *** Failed to prove badRevLen. -- Falsifiable. Counter-example: -- xs = [Elt!val!1,Elt!val!2,Elt!val!1] :: [Elt] -badRevLen :: IO () +badRevLen :: KD () badRevLen = do let p :: SList Elt -> SBool p xs = length (reverse xs) .== ite (length xs .== 3) 5 (length xs) diff --git a/Documentation/SBV/Examples/KnuckleDragger/Sqrt2IsIrrational.hs b/Documentation/SBV/Examples/KnuckleDragger/Sqrt2IsIrrational.hs index 868c28cf6..167435f2c 100644 --- a/Documentation/SBV/Examples/KnuckleDragger/Sqrt2IsIrrational.hs +++ b/Documentation/SBV/Examples/KnuckleDragger/Sqrt2IsIrrational.hs @@ -22,6 +22,10 @@ import Prelude hiding (even, odd) import Data.SBV import Data.SBV.Tools.KnuckleDragger +-- $setup +-- >>> -- For doctest purposes only: +-- >>> import Data.SBV.Tools.KnuckleDragger(runKD) + -- | Prove that square-root of @2@ is irrational. That is, we can never find @a@ and @b@ such that -- @sqrt 2 == a / b@ and @a@ and @b@ are co-prime. -- @@ -47,13 +51,13 @@ import Data.SBV.Tools.KnuckleDragger -- -- We have: -- --- >>> sqrt2IsIrrational +-- >>> runKD sqrt2IsIrrational -- Lemma: expandOddXInSq Q.E.D. -- Lemma: oddSquaredIsOdd Q.E.D. -- Lemma: evenIfSquareIsEven Q.E.D. -- Lemma: evenSquaredIsMult4 Q.E.D. -- Lemma: sqrt2IsIrrational Q.E.D. -sqrt2IsIrrational :: IO Proven +sqrt2IsIrrational :: KD Proven sqrt2IsIrrational = do let even, odd :: SInteger -> SBool even = (2 `sDivides`) diff --git a/sbv.cabal b/sbv.cabal index c77cf6999..e2e653738 100644 --- a/sbv.cabal +++ b/sbv.cabal @@ -269,6 +269,7 @@ Library , Data.SBV.Provers.Yices , Data.SBV.Provers.Z3 , Data.SBV.Tools.KDKernel + , Data.SBV.Tools.KDUtils , Data.SBV.Utils.CrackNum , Data.SBV.Utils.ExtractIO , Data.SBV.Utils.Numeric