KD: Start using the KD monad

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

Data/SBV/Tools/KDUtils.hs

@@ -0,0 +1,63 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module    : Data.SBV.Tools.KDUtils
+-- Copyright : (c) Levent Erkok
+-- License   : BSD3
+-- Maintainer: [email protected]
+-- 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

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

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
 

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))

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