-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.TP.Utils
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Various theorem-proving machinery.
-----------------------------------------------------------------------------

{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE DeriveAnyClass             #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NamedFieldPuns             #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE TupleSections              #-}
{-# LANGUAGE TypeAbstractions           #-}
{-# LANGUAGE TypeApplications           #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.TP.Utils (
         TP, runTP, runTPWith, Proof(..), ProofObj(..), assumptionFromProof, sorry, quickCheckProof
       , startTP, finishTP, getTPState, getTPConfig, setTPConfig, tpGetNextUnique, TPState(..), TPStats(..), RootOfTrust(..)
       , TPProofContext(..), message, updStats, rootOfTrust, concludeModulo
       , ProofTree(..), TPUnique(..), showProofTree, showProofTreeHTML
       , withProofCache
       , tpQuiet, tpRibbon, tpAsms, tpStats, tpCache
       ) where

import Control.Monad.Reader (ReaderT, runReaderT, MonadReader, ask, liftIO)
import Control.Monad.Trans  (MonadIO)

import Data.Time (NominalDiffTime)

import Data.Tree
import Data.Tree.View

import Data.Proxy
import Data.Typeable (typeOf, TypeRep)

import Data.Char (isSpace)
import Data.List (intercalate, isPrefixOf, isSuffixOf, isInfixOf, nubBy, partition, sort)
import Data.Int  (Int64)

import Data.SBV.Utils.Lib (unQuote)

import System.IO     (hFlush, stdout)
import System.Random (randomIO)

import Data.SBV.Core.Data      (SBool, Forall(..), quantifiedBool)
import Data.SBV.Core.Model     (label)
import Data.SBV.Core.Symbolic  (SMTConfig, TPOptions(..))
import Data.SBV.Provers.Prover (defaultSMTCfg, SMTConfig(..))

import Data.SBV.Utils.TDiff (showTDiff, timeIf)
import Control.DeepSeq (NFData(rnf))

import Data.IORef

import GHC.Generics
import Data.Dynamic

import qualified Data.Map as Map
import Data.Map (Map)

-- | Various statistics we collect
data TPStats = TPStats { TPStats -> Int
noOfCheckSats :: Int
                       , TPStats -> NominalDiffTime
solverElapsed :: NominalDiffTime
                       , TPStats -> NominalDiffTime
qcElapsed     :: NominalDiffTime
                       }

-- | Extra state we carry in a TP context
data TPState = TPState { TPState -> IORef TPStats
stats      :: IORef TPStats
                       , TPState -> IORef (Map ([Char], TypeRep) ProofObj)
proofCache :: IORef (Map (String, TypeRep) ProofObj)
                       , TPState -> IORef SMTConfig
config     :: IORef SMTConfig
                       }

-- | Monad for running TP proofs in.
newtype TP a = TP (ReaderT TPState IO a)
            deriving newtype (Functor TP
Functor TP =>
(forall a. a -> TP a)
-> (forall a b. TP (a -> b) -> TP a -> TP b)
-> (forall a b c. (a -> b -> c) -> TP a -> TP b -> TP c)
-> (forall a b. TP a -> TP b -> TP b)
-> (forall a b. TP a -> TP b -> TP a)
-> Applicative TP
forall a. a -> TP a
forall a b. TP a -> TP b -> TP a
forall a b. TP a -> TP b -> TP b
forall a b. TP (a -> b) -> TP a -> TP b
forall a b c. (a -> b -> c) -> TP a -> TP b -> TP c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall a. a -> TP a
pure :: forall a. a -> TP a
$c<*> :: forall a b. TP (a -> b) -> TP a -> TP b
<*> :: forall a b. TP (a -> b) -> TP a -> TP b
$cliftA2 :: forall a b c. (a -> b -> c) -> TP a -> TP b -> TP c
liftA2 :: forall a b c. (a -> b -> c) -> TP a -> TP b -> TP c
$c*> :: forall a b. TP a -> TP b -> TP b
*> :: forall a b. TP a -> TP b -> TP b
$c<* :: forall a b. TP a -> TP b -> TP a
<* :: forall a b. TP a -> TP b -> TP a
Applicative, (forall a b. (a -> b) -> TP a -> TP b)
-> (forall a b. a -> TP b -> TP a) -> Functor TP
forall a b. a -> TP b -> TP a
forall a b. (a -> b) -> TP a -> TP b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> TP a -> TP b
fmap :: forall a b. (a -> b) -> TP a -> TP b
$c<$ :: forall a b. a -> TP b -> TP a
<$ :: forall a b. a -> TP b -> TP a
Functor, Applicative TP
Applicative TP =>
(forall a b. TP a -> (a -> TP b) -> TP b)
-> (forall a b. TP a -> TP b -> TP b)
-> (forall a. a -> TP a)
-> Monad TP
forall a. a -> TP a
forall a b. TP a -> TP b -> TP b
forall a b. TP a -> (a -> TP b) -> TP b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall a b. TP a -> (a -> TP b) -> TP b
>>= :: forall a b. TP a -> (a -> TP b) -> TP b
$c>> :: forall a b. TP a -> TP b -> TP b
>> :: forall a b. TP a -> TP b -> TP b
$creturn :: forall a. a -> TP a
return :: forall a. a -> TP a
Monad, Monad TP
Monad TP => (forall a. IO a -> TP a) -> MonadIO TP
forall a. IO a -> TP a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
$cliftIO :: forall a. IO a -> TP a
liftIO :: forall a. IO a -> TP a
MonadIO, MonadReader TPState, Monad TP
Monad TP => (forall a. [Char] -> TP a) -> MonadFail TP
forall a. [Char] -> TP a
forall (m :: * -> *).
Monad m =>
(forall a. [Char] -> m a) -> MonadFail m
$cfail :: forall a. [Char] -> TP a
fail :: forall a. [Char] -> TP a
MonadFail)

-- | If caches are enabled, see if we cached this proof and return it; otherwise generate it, cache it, and return it
withProofCache :: forall a. Typeable a => String -> TP (Proof a) -> TP (Proof a)
withProofCache :: forall a. Typeable a => [Char] -> TP (Proof a) -> TP (Proof a)
withProofCache [Char]
nm TP (Proof a)
genProof = do
  TPState{IORef (Map ([Char], TypeRep) ProofObj)
proofCache :: TPState -> IORef (Map ([Char], TypeRep) ProofObj)
proofCache :: IORef (Map ([Char], TypeRep) ProofObj)
proofCache, IORef SMTConfig
config :: TPState -> IORef SMTConfig
config :: IORef SMTConfig
config} <- TP TPState
getTPState
  cfg :: SMTConfig
cfg@SMTConfig {tpOptions :: SMTConfig -> TPOptions
tpOptions = TPOptions {Bool
cacheProofs :: Bool
cacheProofs :: TPOptions -> Bool
cacheProofs}} <- IO SMTConfig -> TP SMTConfig
forall a. IO a -> TP a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SMTConfig -> TP SMTConfig) -> IO SMTConfig -> TP SMTConfig
forall a b. (a -> b) -> a -> b
$ IORef SMTConfig -> IO SMTConfig
forall a. IORef a -> IO a
readIORef IORef SMTConfig
config

  let key :: ([Char], TypeRep)
key = ([Char]
nm, Proxy a -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a))

  if Bool -> Bool
not Bool
cacheProofs
     then TP (Proof a)
genProof
     else do Map ([Char], TypeRep) ProofObj
cache <- IO (Map ([Char], TypeRep) ProofObj)
-> TP (Map ([Char], TypeRep) ProofObj)
forall a. IO a -> TP a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Map ([Char], TypeRep) ProofObj)
 -> TP (Map ([Char], TypeRep) ProofObj))
-> IO (Map ([Char], TypeRep) ProofObj)
-> TP (Map ([Char], TypeRep) ProofObj)
forall a b. (a -> b) -> a -> b
$ IORef (Map ([Char], TypeRep) ProofObj)
-> IO (Map ([Char], TypeRep) ProofObj)
forall a. IORef a -> IO a
readIORef IORef (Map ([Char], TypeRep) ProofObj)
proofCache
             case ([Char], TypeRep)
key ([Char], TypeRep)
-> Map ([Char], TypeRep) ProofObj -> Maybe ProofObj
forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` Map ([Char], TypeRep) ProofObj
cache of
               Just ProofObj
prf -> do IO () -> TP ()
forall a. IO a -> TP a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TP ()) -> IO () -> TP ()
forall a b. (a -> b) -> a -> b
$ do Int
tab <- SMTConfig -> Bool -> [Char] -> Int -> TPProofContext -> IO Int
startTP SMTConfig
cfg Bool
False [Char]
"Cached" Int
0 ([Char] -> [ProofObj] -> TPProofContext
TPProofOneShot [Char]
nm [])
                                          SMTConfig
-> [Char]
-> (Int, Maybe NominalDiffTime)
-> [NominalDiffTime]
-> IO ()
finishTP SMTConfig
cfg [Char]
"Q.E.D." (Int
tab, Maybe NominalDiffTime
forall a. Maybe a
Nothing) []
                              Proof a -> TP (Proof a)
forall a. a -> TP a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proof a -> TP (Proof a)) -> Proof a -> TP (Proof a)
forall a b. (a -> b) -> a -> b
$ ProofObj -> Proof a
forall a. ProofObj -> Proof a
Proof ProofObj
prf{isCached = True}
               Maybe ProofObj
Nothing  -> do Proof a
p <- TP (Proof a)
genProof
                              IO () -> TP ()
forall a. IO a -> TP a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TP ()) -> IO () -> TP ()
forall a b. (a -> b) -> a -> b
$ IORef (Map ([Char], TypeRep) ProofObj)
-> (Map ([Char], TypeRep) ProofObj
    -> Map ([Char], TypeRep) ProofObj)
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (Map ([Char], TypeRep) ProofObj)
proofCache (([Char], TypeRep)
-> ProofObj
-> Map ([Char], TypeRep) ProofObj
-> Map ([Char], TypeRep) ProofObj
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ([Char], TypeRep)
key (Proof a -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof a
p))
                              Proof a -> TP (Proof a)
forall a. a -> TP a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Proof a
p

-- | The context in which we make a check-sat call
data TPProofContext = TPProofOneShot String      -- ^ A one shot proof, with string containing its name
                                     [ProofObj]  -- ^ Helpers used (latter only used for cex generation)
                    | TPProofStep    Bool        -- ^ A proof step. If Bool is true, then these are the assumptions for that step
                                     String      -- ^ Name of original goal
                                     [String]    -- ^ The helper "strings" given by the user
                                     [String]    -- ^ The step name, i.e., the name of the branch in the proof tree

-- | Run a TP proof, using the default configuration.
runTP :: TP a -> IO a
runTP :: forall a. TP a -> IO a
runTP = SMTConfig -> TP a -> IO a
forall a. SMTConfig -> TP a -> IO a
runTPWith SMTConfig
defaultSMTCfg

-- | Run a TP proof, using the given configuration.
runTPWith :: SMTConfig -> TP a -> IO a
runTPWith :: forall a. SMTConfig -> TP a -> IO a
runTPWith cfg :: SMTConfig
cfg@SMTConfig{tpOptions :: SMTConfig -> TPOptions
tpOptions = TPOptions{Bool
printStats :: Bool
printStats :: TPOptions -> Bool
printStats}} (TP ReaderT TPState IO a
f) = do
   IORef TPStats
rStats <- TPStats -> IO (IORef TPStats)
forall a. a -> IO (IORef a)
newIORef (TPStats -> IO (IORef TPStats)) -> TPStats -> IO (IORef TPStats)
forall a b. (a -> b) -> a -> b
$ TPStats { noOfCheckSats :: Int
noOfCheckSats = Int
0, solverElapsed :: NominalDiffTime
solverElapsed = NominalDiffTime
0, qcElapsed :: NominalDiffTime
qcElapsed = NominalDiffTime
0 }
   IORef (Map ([Char], TypeRep) ProofObj)
rCache <- Map ([Char], TypeRep) ProofObj
-> IO (IORef (Map ([Char], TypeRep) ProofObj))
forall a. a -> IO (IORef a)
newIORef Map ([Char], TypeRep) ProofObj
forall k a. Map k a
Map.empty
   IORef SMTConfig
rCfg   <- SMTConfig -> IO (IORef SMTConfig)
forall a. a -> IO (IORef a)
newIORef SMTConfig
cfg
   (Maybe NominalDiffTime
mbT, a
r) <- Bool -> IO a -> IO (Maybe NominalDiffTime, a)
forall (m :: * -> *) a.
MonadIO m =>
Bool -> m a -> m (Maybe NominalDiffTime, a)
timeIf Bool
printStats (IO a -> IO (Maybe NominalDiffTime, a))
-> IO a -> IO (Maybe NominalDiffTime, a)
forall a b. (a -> b) -> a -> b
$ ReaderT TPState IO a -> TPState -> IO a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT TPState IO a
f TPState {config :: IORef SMTConfig
config = IORef SMTConfig
rCfg, stats :: IORef TPStats
stats = IORef TPStats
rStats, proofCache :: IORef (Map ([Char], TypeRep) ProofObj)
proofCache = IORef (Map ([Char], TypeRep) ProofObj)
rCache}
   case Maybe NominalDiffTime
mbT of
     Maybe NominalDiffTime
Nothing -> () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
     Just NominalDiffTime
t  -> do TPStats Int
noOfCheckSats NominalDiffTime
solverTime NominalDiffTime
qcElapsed <- IORef TPStats -> IO TPStats
forall a. IORef a -> IO a
readIORef IORef TPStats
rStats

                   let stats :: [([Char], [Char])]
stats = [ ([Char]
"SBV",       NominalDiffTime -> [Char]
showTDiff (NominalDiffTime
t NominalDiffTime -> NominalDiffTime -> NominalDiffTime
forall a. Num a => a -> a -> a
- NominalDiffTime
solverTime NominalDiffTime -> NominalDiffTime -> NominalDiffTime
forall a. Num a => a -> a -> a
- NominalDiffTime
qcElapsed))
                               , ([Char]
"Solver",    NominalDiffTime -> [Char]
showTDiff NominalDiffTime
solverTime)
                               , ([Char]
"QC",        NominalDiffTime -> [Char]
showTDiff NominalDiffTime
qcElapsed)
                               , ([Char]
"Total",     NominalDiffTime -> [Char]
showTDiff NominalDiffTime
t)
                               , ([Char]
"Decisions", Int -> [Char]
forall a. Show a => a -> [Char]
show Int
noOfCheckSats)
                               ]

                   SMTConfig -> [Char] -> IO ()
forall (m :: * -> *). MonadIO m => SMTConfig -> [Char] -> m ()
message SMTConfig
cfg ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ Char
'[' Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " [[Char]
k [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
v | ([Char]
k, [Char]
v) <- [([Char], [Char])]
stats] [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"]\n"
   a -> IO a
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
r

-- | get the state
getTPState :: TP TPState
getTPState :: TP TPState
getTPState = TP TPState
forall r (m :: * -> *). MonadReader r m => m r
ask

-- | Make a unique number in this TP run. We combine that context with the proof-count
tpGetNextUnique :: TP TPUnique
tpGetNextUnique :: TP TPUnique
tpGetNextUnique = Int64 -> TPUnique
TPUser (Int64 -> TPUnique) -> TP Int64 -> TP TPUnique
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO Int64 -> TP Int64
forall a. IO a -> TP a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO Int64
forall a (m :: * -> *). (Random a, MonadIO m) => m a
randomIO

-- | get the configuration
getTPConfig :: TP SMTConfig
getTPConfig :: TP SMTConfig
getTPConfig = do IORef SMTConfig
rCfg <- TPState -> IORef SMTConfig
config (TPState -> IORef SMTConfig) -> TP TPState -> TP (IORef SMTConfig)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TP TPState
getTPState
                 IO SMTConfig -> TP SMTConfig
forall a. IO a -> TP a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IORef SMTConfig -> IO SMTConfig
forall a. IORef a -> IO a
readIORef IORef SMTConfig
rCfg)

-- | set the configuration
setTPConfig :: SMTConfig -> TP ()
setTPConfig :: SMTConfig -> TP ()
setTPConfig SMTConfig
cfg = do TPState
st <- TP TPState
getTPState
                     IO () -> TP ()
forall a. IO a -> TP a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IORef SMTConfig -> SMTConfig -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (TPState -> IORef SMTConfig
config TPState
st) SMTConfig
cfg)

-- | Update stats
updStats :: MonadIO m => TPState -> (TPStats -> TPStats) -> m ()
updStats :: forall (m :: * -> *).
MonadIO m =>
TPState -> (TPStats -> TPStats) -> m ()
updStats TPState{IORef TPStats
stats :: TPState -> IORef TPStats
stats :: IORef TPStats
stats} TPStats -> TPStats
u = IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IORef TPStats -> (TPStats -> TPStats) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef TPStats
stats TPStats -> TPStats
u

-- | Display the message if not quiet. Note that we don't print a newline; so the message must have it if needed.
message :: MonadIO m => SMTConfig -> String -> m ()
message :: forall (m :: * -> *). MonadIO m => SMTConfig -> [Char] -> m ()
message SMTConfig{tpOptions :: SMTConfig -> TPOptions
tpOptions = TPOptions{Bool
quiet :: Bool
quiet :: TPOptions -> Bool
quiet}} [Char]
s
  | Bool
quiet = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  | Bool
True  = IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStr [Char]
s

-- | Start a proof. We return the number of characters we printed, so the finisher can align the result.
startTP :: SMTConfig -> Bool -> String -> Int -> TPProofContext -> IO Int
startTP :: SMTConfig -> Bool -> [Char] -> Int -> TPProofContext -> IO Int
startTP SMTConfig
cfg Bool
newLine [Char]
what Int
level TPProofContext
ctx = do SMTConfig -> [Char] -> IO ()
forall (m :: * -> *). MonadIO m => SMTConfig -> [Char] -> m ()
message SMTConfig
cfg ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
line [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ if Bool
newLine then [Char]
"\n" else [Char]
""
                                        Handle -> IO ()
hFlush Handle
stdout
                                        Int -> IO Int
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
line)
  where nm :: [Char]
nm = case TPProofContext
ctx of
               TPProofOneShot [Char]
n [ProofObj]
_       -> [Char]
n
               TPProofStep    Bool
_ [Char]
_ [[Char]]
hs [[Char]]
ss -> [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"." [[Char]]
ss [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
userHints [[Char]]
hs

        tab :: Int
tab = Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
level

        line :: [Char]
line = Int -> Char -> [Char]
forall a. Int -> a -> [a]
replicate Int
tab Char
' ' [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
what [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
nm

        userHints :: [[Char]] -> [Char]
userHints [] = [Char]
""
        userHints [[Char]]
ss = [Char]
" (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " [[Char]]
ss [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"

-- | Finish a proof. First argument is what we got from the call of 'startTP' above.
finishTP :: SMTConfig -> String -> (Int, Maybe NominalDiffTime) -> [NominalDiffTime] -> IO ()
finishTP :: SMTConfig
-> [Char]
-> (Int, Maybe NominalDiffTime)
-> [NominalDiffTime]
-> IO ()
finishTP cfg :: SMTConfig
cfg@SMTConfig{tpOptions :: SMTConfig -> TPOptions
tpOptions = TPOptions{Int
ribbonLength :: Int
ribbonLength :: TPOptions -> Int
ribbonLength}} [Char]
what (Int
skip, Maybe NominalDiffTime
mbT) [NominalDiffTime]
extraTiming =
   SMTConfig -> [Char] -> IO ()
forall (m :: * -> *). MonadIO m => SMTConfig -> [Char] -> m ()
message SMTConfig
cfg ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> Char -> [Char]
forall a. Int -> a -> [a]
replicate (Int
ribbonLength Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
skip) Char
' ' [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
what [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
timing [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
extras [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
 where timing :: [Char]
timing = [Char]
-> (NominalDiffTime -> [Char]) -> Maybe NominalDiffTime -> [Char]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Char]
"" ((Char
' ' Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
:) ([Char] -> [Char])
-> (NominalDiffTime -> [Char]) -> NominalDiffTime -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NominalDiffTime -> [Char]
mkTiming) Maybe NominalDiffTime
mbT
       extras :: [Char]
extras = (NominalDiffTime -> [Char]) -> [NominalDiffTime] -> [Char]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NominalDiffTime -> [Char]
mkTiming [NominalDiffTime]
extraTiming

       mkTiming :: NominalDiffTime -> [Char]
mkTiming NominalDiffTime
t = Char
'[' Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: NominalDiffTime -> [Char]
showTDiff NominalDiffTime
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"]"

-- | Unique identifier for each proof.
data TPUnique = TPInternal    -- IH's
              | TPSorry       -- sorry
              | TPQC          -- qc (quick-check)
              | TPUser Int64  -- user given
              deriving (TPUnique -> ()
(TPUnique -> ()) -> NFData TPUnique
forall a. (a -> ()) -> NFData a
$crnf :: TPUnique -> ()
rnf :: TPUnique -> ()
NFData, (forall x. TPUnique -> Rep TPUnique x)
-> (forall x. Rep TPUnique x -> TPUnique) -> Generic TPUnique
forall x. Rep TPUnique x -> TPUnique
forall x. TPUnique -> Rep TPUnique x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. TPUnique -> Rep TPUnique x
from :: forall x. TPUnique -> Rep TPUnique x
$cto :: forall x. Rep TPUnique x -> TPUnique
to :: forall x. Rep TPUnique x -> TPUnique
Generic, TPUnique -> TPUnique -> Bool
(TPUnique -> TPUnique -> Bool)
-> (TPUnique -> TPUnique -> Bool) -> Eq TPUnique
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TPUnique -> TPUnique -> Bool
== :: TPUnique -> TPUnique -> Bool
$c/= :: TPUnique -> TPUnique -> Bool
/= :: TPUnique -> TPUnique -> Bool
Eq)

-- | Proof for a 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
-- is still large: The underlying solver, SBV, and TP kernel itself. But this
-- mechanism ensures we can't create proven things out of thin air, following the standard LCF
-- methodology.)
newtype Proof a = Proof { forall a. Proof a -> ProofObj
proofOf :: ProofObj -- ^ Get the underlying proof object
                        }

-- | Grab the underlying boolean in a proof. Useful in assumption contexts where we need a boolean
assumptionFromProof :: Proof a -> SBool
assumptionFromProof :: forall a. Proof a -> SBV Bool
assumptionFromProof = ProofObj -> SBV Bool
getObjProof (ProofObj -> SBV Bool)
-> (Proof a -> ProofObj) -> Proof a -> SBV Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proof a -> ProofObj
forall a. Proof a -> ProofObj
proofOf

-- | The actual proof container
data ProofObj = ProofObj { ProofObj -> [ProofObj]
dependencies :: [ProofObj]     -- ^ Immediate dependencies of this proof. (Not transitive)
                         , ProofObj -> Bool
isUserAxiom  :: Bool           -- ^ Was this an axiom given by the user?
                         , ProofObj -> SBV Bool
getObjProof  :: SBool          -- ^ Get the underlying boolean
                         , ProofObj -> Dynamic
getProp      :: Dynamic        -- ^ The actual proposition
                         , ProofObj -> [Char]
proofName    :: String         -- ^ User given name
                         , ProofObj -> TPUnique
uniqId       :: TPUnique       -- ^ Unique identifier
                         , ProofObj -> Bool
isCached     :: Bool           -- ^ Was this a cached proof?
                         }

-- | Drop the instantiation part
shortProofName :: ProofObj -> String
shortProofName :: ProofObj -> [Char]
shortProofName ProofObj
p | [Char]
" @ " [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isInfixOf` [Char]
s = [Char] -> [Char]
forall a. [a] -> [a]
reverse ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> [Char] -> [Char]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [Char]
forall a. [a] -> [a]
reverse ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> [Char] -> [Char]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'@') ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char]
s
                 | Bool
True                = [Char]
s
   where s :: [Char]
s = ProofObj -> [Char]
proofName ProofObj
p

-- | Nicely format a bunch of proof-names, shortened and uniquified. Note that if we get a dependency
-- via multiple routes, they can get different uniqid's; so we do a bit of compression here.
shortProofNames :: [ProofObj] -> String
shortProofNames :: [ProofObj] -> [Char]
shortProofNames = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " ([[Char]] -> [Char])
-> ([ProofObj] -> [[Char]]) -> [ProofObj] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([Char], Int) -> [Char]) -> [([Char], Int)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char], Int) -> [Char]
forall {a}. (Eq a, Num a, Show a) => ([Char], a) -> [Char]
merge ([([Char], Int)] -> [[Char]])
-> ([ProofObj] -> [([Char], Int)]) -> [ProofObj] -> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Char]] -> [([Char], Int)]
forall {a}. Eq a => [a] -> [(a, Int)]
compress ([[Char]] -> [([Char], Int)])
-> ([ProofObj] -> [[Char]]) -> [ProofObj] -> [([Char], Int)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Char]] -> [[Char]]
forall a. Ord a => [a] -> [a]
sort ([[Char]] -> [[Char]])
-> ([ProofObj] -> [[Char]]) -> [ProofObj] -> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProofObj -> [Char]) -> [ProofObj] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ProofObj -> [Char]
shortProofName ([ProofObj] -> [[Char]])
-> ([ProofObj] -> [ProofObj]) -> [ProofObj] -> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProofObj -> ProofObj -> Bool) -> [ProofObj] -> [ProofObj]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy (\ProofObj
a ProofObj
b -> ProofObj -> TPUnique
uniqId ProofObj
a TPUnique -> TPUnique -> Bool
forall a. Eq a => a -> a -> Bool
== ProofObj -> TPUnique
uniqId ProofObj
b)
 where compress :: [a] -> [(a, Int)]
compress []     = []
       compress (a
a:[a]
as) = case (a -> Bool) -> [a] -> ([a], [a])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
==) [a]
as of
                           ([a]
same, [a]
other) -> (a
a, [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
same Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (a, Int) -> [(a, Int)] -> [(a, Int)]
forall a. a -> [a] -> [a]
: [a] -> [(a, Int)]
compress [a]
other
       merge :: ([Char], a) -> [Char]
merge ([Char]
n, a
1) = [Char]
n
       merge ([Char]
n, a
x) = [Char]
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" (x" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"

-- | Keeping track of where the sorry originates from. Used in displaying dependencies.
newtype RootOfTrust = RootOfTrust (Maybe [ProofObj])

-- | Show instance for t'RootOfTrust'
instance Show RootOfTrust where
  show :: RootOfTrust -> [Char]
show (RootOfTrust Maybe [ProofObj]
mbp) = case Maybe [ProofObj]
mbp of
                             Maybe [ProofObj]
Nothing -> [Char]
"Nothing"
                             Just [ProofObj]
ps -> [Char]
"Just [" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [ProofObj] -> [Char]
shortProofNames [ProofObj]
ps [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"]"

-- | Trust forms a semigroup
instance Semigroup RootOfTrust where
   RootOfTrust Maybe [ProofObj]
as <> :: RootOfTrust -> RootOfTrust -> RootOfTrust
<> RootOfTrust Maybe [ProofObj]
bs = Maybe [ProofObj] -> RootOfTrust
RootOfTrust (Maybe [ProofObj] -> RootOfTrust)
-> Maybe [ProofObj] -> RootOfTrust
forall a b. (a -> b) -> a -> b
$ (ProofObj -> ProofObj -> Bool) -> [ProofObj] -> [ProofObj]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy (\ProofObj
a ProofObj
b -> ProofObj -> TPUnique
uniqId ProofObj
a TPUnique -> TPUnique -> Bool
forall a. Eq a => a -> a -> Bool
== ProofObj -> TPUnique
uniqId ProofObj
b) ([ProofObj] -> [ProofObj]) -> Maybe [ProofObj] -> Maybe [ProofObj]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Maybe [ProofObj]
as Maybe [ProofObj] -> Maybe [ProofObj] -> Maybe [ProofObj]
forall a. Semigroup a => a -> a -> a
<> Maybe [ProofObj]
bs)

-- | Trust forms a monoid
instance Monoid RootOfTrust where
  mempty :: RootOfTrust
mempty = Maybe [ProofObj] -> RootOfTrust
RootOfTrust Maybe [ProofObj]
forall a. Maybe a
Nothing

-- | NFData ignores the getProp field
instance NFData ProofObj where
  rnf :: ProofObj -> ()
rnf (ProofObj [ProofObj]
dependencies Bool
isUserAxiom SBV Bool
getObjProof Dynamic
_getProp [Char]
proofName TPUnique
uniqId Bool
isCached) =     [ProofObj] -> ()
forall a. NFData a => a -> ()
rnf [ProofObj]
dependencies
                                                                                         () -> () -> ()
forall a b. a -> b -> b
`seq` Bool -> ()
forall a. NFData a => a -> ()
rnf Bool
isUserAxiom
                                                                                         () -> () -> ()
forall a b. a -> b -> b
`seq` SBV Bool -> ()
forall a. NFData a => a -> ()
rnf SBV Bool
getObjProof
                                                                                         () -> () -> ()
forall a b. a -> b -> b
`seq` [Char] -> ()
forall a. NFData a => a -> ()
rnf [Char]
proofName
                                                                                         () -> () -> ()
forall a b. a -> b -> b
`seq` TPUnique -> ()
forall a. NFData a => a -> ()
rnf TPUnique
uniqId
                                                                                         () -> () -> ()
forall a b. a -> b -> b
`seq` Bool -> ()
forall a. NFData a => a -> ()
rnf Bool
isCached

-- | Dependencies of a proof, in a tree format.
data ProofTree = ProofTree ProofObj [ProofTree]

-- | Return all the proofs this particular proof depends on, transitively
getProofTree :: ProofObj -> ProofTree
getProofTree :: ProofObj -> ProofTree
getProofTree ProofObj
p = ProofObj -> [ProofTree] -> ProofTree
ProofTree ProofObj
p ([ProofTree] -> ProofTree) -> [ProofTree] -> ProofTree
forall a b. (a -> b) -> a -> b
$ (ProofObj -> ProofTree) -> [ProofObj] -> [ProofTree]
forall a b. (a -> b) -> [a] -> [b]
map ProofObj -> ProofTree
getProofTree (ProofObj -> [ProofObj]
dependencies ProofObj
p)

-- | Turn dependencies to a container tree, for display purposes
depsToTree :: Bool -> [TPUnique] -> (String -> Int -> Int -> a) -> (Int, ProofTree) -> ([TPUnique], Tree a)
depsToTree :: forall a.
Bool
-> [TPUnique]
-> ([Char] -> Int -> Int -> a)
-> (Int, ProofTree)
-> ([TPUnique], Tree a)
depsToTree Bool
shouldCompress [TPUnique]
visited [Char] -> Int -> Int -> a
xform (Int
cnt, ProofTree ProofObj
top [ProofTree]
ds) = ([TPUnique]
nVisited, a -> [Tree a] -> Tree a
forall a. a -> [Tree a] -> Tree a
Node ([Char] -> Int -> Int -> a
xform [Char]
nTop Int
cnt ([Tree a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Tree a]
chlds)) [Tree a]
chlds)
  where nTop :: [Char]
nTop = ProofObj -> [Char]
shortProofName ProofObj
top
        uniq :: TPUnique
uniq = ProofObj -> TPUnique
uniqId ProofObj
top

        ([TPUnique]
nVisited, [Tree a]
chlds)
           | Bool
shouldCompress Bool -> Bool -> Bool
&& TPUnique
uniq TPUnique -> [TPUnique] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TPUnique]
visited = ([TPUnique]
visited, [])
           | Bool
shouldCompress                        = [TPUnique] -> [(Int, ProofTree)] -> ([TPUnique], [Tree a])
walk (TPUnique
uniq TPUnique -> [TPUnique] -> [TPUnique]
forall a. a -> [a] -> [a]
: [TPUnique]
visited) ([ProofTree] -> [(Int, ProofTree)]
compress ((ProofTree -> Bool) -> [ProofTree] -> [ProofTree]
forall a. (a -> Bool) -> [a] -> [a]
filter ProofTree -> Bool
interesting [ProofTree]
ds))
           | Bool
True                                  = [TPUnique] -> [(Int, ProofTree)] -> ([TPUnique], [Tree a])
walk         [TPUnique]
visited  ((ProofTree -> (Int, ProofTree))
-> [ProofTree] -> [(Int, ProofTree)]
forall a b. (a -> b) -> [a] -> [b]
map (Int
1,) ((ProofTree -> Bool) -> [ProofTree] -> [ProofTree]
forall a. (a -> Bool) -> [a] -> [a]
filter ProofTree -> Bool
interesting [ProofTree]
ds))

        walk :: [TPUnique] -> [(Int, ProofTree)] -> ([TPUnique], [Tree a])
walk [TPUnique]
v []     = ([TPUnique]
v, [])
        walk [TPUnique]
v ((Int, ProofTree)
c:[(Int, ProofTree)]
cs) = let ([TPUnique]
v',  Tree a
t)  = Bool
-> [TPUnique]
-> ([Char] -> Int -> Int -> a)
-> (Int, ProofTree)
-> ([TPUnique], Tree a)
forall a.
Bool
-> [TPUnique]
-> ([Char] -> Int -> Int -> a)
-> (Int, ProofTree)
-> ([TPUnique], Tree a)
depsToTree Bool
shouldCompress [TPUnique]
v [Char] -> Int -> Int -> a
xform (Int, ProofTree)
c
                            ([TPUnique]
v'', [Tree a]
ts) = [TPUnique] -> [(Int, ProofTree)] -> ([TPUnique], [Tree a])
walk [TPUnique]
v' [(Int, ProofTree)]
cs
                        in ([TPUnique]
v'', Tree a
t Tree a -> [Tree a] -> [Tree a]
forall a. a -> [a] -> [a]
: [Tree a]
ts)

        -- Don't show internal axioms, not interesting
        interesting :: ProofTree -> Bool
interesting (ProofTree ProofObj
p [ProofTree]
_) = case ProofObj -> TPUnique
uniqId ProofObj
p of
                                        TPUnique
TPInternal -> Bool
False
                                        TPUnique
TPSorry    -> Bool
True
                                        TPUnique
TPQC       -> Bool
True
                                        TPUser{}   -> Bool
True

        -- If a proof is used twice in the same proof, compress it
        compress :: [ProofTree] -> [(Int, ProofTree)]
        compress :: [ProofTree] -> [(Int, ProofTree)]
compress []       = []
        compress (ProofTree
p : [ProofTree]
ps) = (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [()] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [() | (ProofTree
_, Bool
True) <- [(ProofTree, Bool)]
filtered], ProofTree
p) (Int, ProofTree) -> [(Int, ProofTree)] -> [(Int, ProofTree)]
forall a. a -> [a] -> [a]
: [ProofTree] -> [(Int, ProofTree)]
compress [ProofTree
d | (ProofTree
d, Bool
False) <- [(ProofTree, Bool)]
filtered]
          where filtered :: [(ProofTree, Bool)]
filtered = [(ProofTree
d, ProofObj -> TPUnique
uniqId ProofObj
p' TPUnique -> TPUnique -> Bool
forall a. Eq a => a -> a -> Bool
== TPUnique
curUniq) | d :: ProofTree
d@(ProofTree ProofObj
p' [ProofTree]
_) <- [ProofTree]
ps]
                curUniq :: TPUnique
curUniq  = case ProofTree
p of
                             ProofTree ProofObj
curProof [ProofTree]
_ -> ProofObj -> TPUnique
uniqId ProofObj
curProof

-- | Display the proof tree as ASCII text. The first argument is if we should compress the tree, showing only the first
-- use of any sublemma.
showProofTree :: Bool -> Proof a -> String
showProofTree :: forall a. Bool -> Proof a -> [Char]
showProofTree Bool
compress Proof a
d = Tree [Char] -> [Char]
showTree (Tree [Char] -> [Char]) -> Tree [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ ([TPUnique], Tree [Char]) -> Tree [Char]
forall a b. (a, b) -> b
snd (([TPUnique], Tree [Char]) -> Tree [Char])
-> ([TPUnique], Tree [Char]) -> Tree [Char]
forall a b. (a -> b) -> a -> b
$ Bool
-> [TPUnique]
-> ([Char] -> Int -> Int -> [Char])
-> (Int, ProofTree)
-> ([TPUnique], Tree [Char])
forall a.
Bool
-> [TPUnique]
-> ([Char] -> Int -> Int -> a)
-> (Int, ProofTree)
-> ([TPUnique], Tree a)
depsToTree Bool
compress [] [Char] -> Int -> Int -> [Char]
forall {a} {p}. (Eq a, Num a, Show a) => [Char] -> a -> p -> [Char]
sh (Int
1, ProofObj -> ProofTree
getProofTree (Proof a -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof a
d))
    where sh :: [Char] -> a -> p -> [Char]
sh [Char]
nm a
1 p
_ = [Char]
nm
          sh [Char]
nm a
x p
_= [Char]
nm [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" (x" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"

-- | Display the tree as an html doc for rendering purposes.
-- The first argument is if we should compress the tree, showing only the first
-- use of any sublemma. Second is the path (or URL) to external CSS file, if needed.
showProofTreeHTML :: Bool -> Maybe FilePath -> Proof a -> String
showProofTreeHTML :: forall a. Bool -> Maybe [Char] -> Proof a -> [Char]
showProofTreeHTML Bool
compress Maybe [Char]
mbCSS Proof a
p = Maybe [Char] -> Tree NodeInfo -> [Char]
htmlTree Maybe [Char]
mbCSS (Tree NodeInfo -> [Char]) -> Tree NodeInfo -> [Char]
forall a b. (a -> b) -> a -> b
$ ([TPUnique], Tree NodeInfo) -> Tree NodeInfo
forall a b. (a, b) -> b
snd (([TPUnique], Tree NodeInfo) -> Tree NodeInfo)
-> ([TPUnique], Tree NodeInfo) -> Tree NodeInfo
forall a b. (a -> b) -> a -> b
$ Bool
-> [TPUnique]
-> ([Char] -> Int -> Int -> NodeInfo)
-> (Int, ProofTree)
-> ([TPUnique], Tree NodeInfo)
forall a.
Bool
-> [TPUnique]
-> ([Char] -> Int -> Int -> a)
-> (Int, ProofTree)
-> ([TPUnique], Tree a)
depsToTree Bool
compress [] [Char] -> Int -> Int -> NodeInfo
nodify (Int
1, ProofObj -> ProofTree
getProofTree (Proof a -> ProofObj
forall a. Proof a -> ProofObj
proofOf Proof a
p))
  where nodify :: String -> Int -> Int -> NodeInfo
        nodify :: [Char] -> Int -> Int -> NodeInfo
nodify [Char]
nm Int
cnt Int
dc = NodeInfo { nodeBehavior :: Behavior
nodeBehavior = Behavior
InitiallyExpanded
                                    , nodeName :: [Char]
nodeName     = [Char]
nm
                                    , nodeInfo :: [Char]
nodeInfo     = [Char] -> [Char]
spc (Int -> [Char]
forall {a}. (Eq a, Num a, Show a) => a -> [Char]
used Int
cnt) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall {a}. (Eq a, Num a, Show a) => a -> [Char]
depCount Int
dc
                                    }
        used :: a -> [Char]
used a
1 = [Char]
""
        used a
n = [Char]
"Used " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" times."

        spc :: [Char] -> [Char]
spc [Char]
"" = [Char]
""
        spc [Char]
s  = [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" "

        depCount :: a -> [Char]
depCount a
0 = [Char]
""
        depCount a
1 = [Char]
"Has one dependency."
        depCount a
n = [Char]
"Has " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" dependencies."

-- | Show instance for t'Proof'
instance Typeable a => Show (Proof a) where
  show :: Proof a -> [Char]
show p :: Proof a
p@(Proof po :: ProofObj
po@ProofObj{proofName :: ProofObj -> [Char]
proofName = [Char]
nm}) = Char
'[' Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: RootOfTrust -> [Char]
sh (Proof a -> RootOfTrust
forall a. Proof a -> RootOfTrust
rootOfTrust Proof a
p) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"] " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
nm [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" :: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
pretty (TypeRep -> [Char]
forall a. Show a => a -> [Char]
show (Proof a -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf Proof a
p))
    where sh :: RootOfTrust -> [Char]
sh (RootOfTrust Maybe [ProofObj]
Nothing)   = [Char]
"Proven"   [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
cacheInfo
          sh (RootOfTrust (Just [ProofObj]
ps)) = [Char]
"Modulo: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [ProofObj] -> [Char]
shortProofNames [ProofObj]
ps [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
cacheInfo

          cacheInfo :: [Char]
cacheInfo = case ProofObj -> [ProofObj]
cachedProofs ProofObj
po of
                        [] -> [Char]
""
                        [ProofObj]
cs -> [Char]
". Cached: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [ProofObj] -> [Char]
shortProofNames ((ProofObj -> ProofObj -> Bool) -> [ProofObj] -> [ProofObj]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy (\ProofObj
p1 ProofObj
p2 -> ProofObj -> TPUnique
uniqId ProofObj
p1 TPUnique -> TPUnique -> Bool
forall a. Eq a => a -> a -> Bool
== ProofObj -> TPUnique
uniqId ProofObj
p2) [ProofObj]
cs)

          cachedProofs :: ProofObj -> [ProofObj]
cachedProofs prf :: ProofObj
prf@ProofObj{Bool
isCached :: ProofObj -> Bool
isCached :: Bool
isCached} = if Bool
isCached then ProofObj
prf ProofObj -> [ProofObj] -> [ProofObj]
forall a. a -> [a] -> [a]
: [ProofObj]
rest else [ProofObj]
rest
            where rest :: [ProofObj]
rest = (ProofObj -> [ProofObj]) -> [ProofObj] -> [ProofObj]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ProofObj -> [ProofObj]
cachedProofs (ProofObj -> [ProofObj]
dependencies ProofObj
prf)

          -- More mathematical notation for types.
          pretty :: String -> String
          pretty :: [Char] -> [Char]
pretty = [[Char]] -> [Char]
unwords ([[Char]] -> [Char]) -> ([Char] -> [[Char]]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Char]] -> [[Char]]
walk ([[Char]] -> [[Char]])
-> ([Char] -> [[Char]]) -> [Char] -> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [[Char]]
words ([Char] -> [[Char]]) -> ([Char] -> [Char]) -> [Char] -> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> [Char]) -> [Char] -> [Char]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\Char
c -> if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
',' then [Char]
" , " else [Char
c]) ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [Char]
clean
            where fa :: [Char] -> [[Char]]
fa [Char]
v = [Char
'Ɐ' Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char] -> [Char]
unQuote [Char]
v, [Char]
"∷"]
                  ex :: [Char] -> [[Char]]
ex [Char]
v = [Char
'∃' Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char] -> [Char]
unQuote [Char]
v, [Char]
"∷"]

                  walk :: [[Char]] -> [[Char]]
walk ([Char]
"SBV"    : [Char]
"Bool" : [[Char]]
rest) = [[Char]] -> [[Char]]
walk ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ [Char]
"Bool" [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
:  [[Char]]
rest
                  walk ([Char]
"Forall" : [Char]
xs     : [[Char]]
rest) = [[Char]] -> [[Char]]
walk ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]]
fa [Char]
xs  [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [[Char]]
rest
                  walk ([Char]
"Exists" : [Char]
xs     : [[Char]]
rest) = [[Char]] -> [[Char]]
walk ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]]
ex [Char]
xs  [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [[Char]]
rest
                  walk ([Char]
"->"              : [[Char]]
rest) = [[Char]] -> [[Char]]
walk ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ [Char]
"→"    [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
:  [[Char]]
rest

                  -- handle the double case. This isn't quite solid, but it does the trick.
                  walk ([Char]
"((Forall" : [Char]
xs : [Char]
t1 : [Char]
"," : [Char]
"(Forall" : [Char]
ys : [Char]
t2 : [[Char]]
rest) = [[Char]] -> [[Char]]
ap ([Char] -> [[Char]]
fa [Char]
xs) [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [[Char] -> [Char]
np [Char]
t1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
","] [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]]
fa [Char]
ys [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [[Char] -> [Char]
np [Char]
t2] [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [[Char]] -> [[Char]]
walk [[Char]]
rest
                     where -- remove a closing paren from the end if it's there
                           np :: [Char] -> [Char]
np [Char]
s | [Char]
")" [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isSuffixOf` [Char]
s = [Char] -> [Char]
forall a. HasCallStack => [a] -> [a]
init [Char]
s
                                | Bool
True               = [Char]
s
                           -- add open paren to the first word
                           ap :: [[Char]] -> [[Char]]
ap ([Char]
t : [[Char]]
ts) = (Char
'('Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
:[Char]
t) [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: [[Char]]
ts
                           ap []       = []

                  -- Otherwise, pass along
                  walk ([Char]
c : [[Char]]
cs) = [Char]
c [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: [[Char]] -> [[Char]]
walk [[Char]]
cs
                  walk []       = []

          -- Strip of Proof (...)
          clean :: String -> String
          clean :: [Char] -> [Char]
clean [Char]
s | [Char]
pre [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` [Char]
s Bool -> Bool -> Bool
&& [Char]
suf [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isSuffixOf` [Char]
s
                  = [Char] -> [Char]
forall a. [a] -> [a]
reverse ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Char] -> [Char]
forall a. Int -> [a] -> [a]
drop ([Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
suf) ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [Char]
forall a. [a] -> [a]
reverse ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Char] -> [Char]
forall a. Int -> [a] -> [a]
drop ([Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
pre) ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char]
s
                  | Bool
True
                  = [Char]
s
            where pre :: [Char]
pre = [Char]
"Proof ("
                  suf :: [Char]
suf = [Char]
")"

-- | A manifestly false theorem. This is useful when we want to prove a theorem that the underlying solver
-- cannot deal with, or if we want to postpone the proof for the time being. TP will keep
-- track of the uses of 'sorry' and will print them appropriately while printing proofs.
-- NB. We keep this as a t'ProofObj' as opposed to a t'Proof' as it is then easier to use it as a lemma helper.
sorry :: ProofObj
sorry :: ProofObj
sorry = ProofObj { dependencies :: [ProofObj]
dependencies = []
                 , isUserAxiom :: Bool
isUserAxiom  = Bool
False
                 , getObjProof :: SBV Bool
getObjProof  = [Char] -> SBV Bool -> SBV Bool
forall a. SymVal a => [Char] -> SBV a -> SBV a
label [Char]
"sorry" ((Forall "__sbvTP_sorry" Bool -> SBV Bool) -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
quantifiedBool Forall "__sbvTP_sorry" Bool -> SBV Bool
p)
                 , getProp :: Dynamic
getProp      = (Forall "__sbvTP_sorry" Bool -> SBV Bool) -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn Forall "__sbvTP_sorry" Bool -> SBV Bool
p
                 , proofName :: [Char]
proofName    = [Char]
"sorry"
                 , uniqId :: TPUnique
uniqId       = TPUnique
TPSorry
                 , isCached :: Bool
isCached     = Bool
False
                 }
  where -- ideally, I'd rather just use
        --   p = sFalse
        -- but then SBV constant folds the boolean, and the generated script
        -- doesn't contain the actual contents, as SBV determines unsatisfiability
        -- itself. By using the following proposition (which is easy for the backend
        -- solver to determine as false, we avoid the constant folding.
        p :: Forall "__sbvTP_sorry" Bool -> SBV Bool
p (Forall @"__sbvTP_sorry" (SBV Bool
x :: SBool)) = [Char] -> SBV Bool -> SBV Bool
forall a. SymVal a => [Char] -> SBV a -> SBV a
label [Char]
"SORRY: TP, proof uses \"sorry\"" SBV Bool
x

-- | Quick-check uses this proof. It's equivalent to sorry, really; except for its name
quickCheckProof :: ProofObj
quickCheckProof :: ProofObj
quickCheckProof = ProofObj { dependencies :: [ProofObj]
dependencies = []
                           , isUserAxiom :: Bool
isUserAxiom  = Bool
False
                           , getObjProof :: SBV Bool
getObjProof  = [Char] -> SBV Bool -> SBV Bool
forall a. SymVal a => [Char] -> SBV a -> SBV a
label [Char]
"quickCheck" ((Forall "__sbvTP_quickCheck" Bool -> SBV Bool) -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
quantifiedBool Forall "__sbvTP_quickCheck" Bool -> SBV Bool
p)
                           , getProp :: Dynamic
getProp      = (Forall "__sbvTP_quickCheck" Bool -> SBV Bool) -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn Forall "__sbvTP_quickCheck" Bool -> SBV Bool
p
                           , proofName :: [Char]
proofName    = [Char]
"quickCheck"
                           , uniqId :: TPUnique
uniqId       = TPUnique
TPQC
                           , isCached :: Bool
isCached     = Bool
False
                           }
  where -- ideally, I'd rather just use
        --   p = sFalse
        -- but then SBV constant folds the boolean, and the generated script
        -- doesn't contain the actual contents, as SBV determines unsatisfiability
        -- itself. By using the following proposition (which is easy for the backend
        -- solver to determine as false, we avoid the constant folding.
        p :: Forall "__sbvTP_quickCheck" Bool -> SBV Bool
p (Forall @"__sbvTP_quickCheck" (SBV Bool
x :: SBool)) = [Char] -> SBV Bool -> SBV Bool
forall a. SymVal a => [Char] -> SBV a -> SBV a
label [Char]
"QUICKCHECK: TP, proof uses \"qc\"" SBV Bool
x

-- | Calculate the root of trust. The returned list of proofs, if any, will need to be sorry and quickcheck free to
-- have the given proof to be sorry-free.
rootOfTrust :: Proof a -> RootOfTrust
rootOfTrust :: forall a. Proof a -> RootOfTrust
rootOfTrust = Bool -> ProofObj -> RootOfTrust
rot Bool
True (ProofObj -> RootOfTrust)
-> (Proof a -> ProofObj) -> Proof a -> RootOfTrust
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proof a -> ProofObj
forall a. Proof a -> ProofObj
proofOf
  where rot :: Bool -> ProofObj -> RootOfTrust
rot Bool
atTop p :: ProofObj
p@ProofObj{uniqId :: ProofObj -> TPUnique
uniqId = TPUnique
curUniq, [ProofObj]
dependencies :: ProofObj -> [ProofObj]
dependencies :: [ProofObj]
dependencies} = RootOfTrust -> RootOfTrust
compress RootOfTrust
res
          where res :: RootOfTrust
res = case TPUnique
curUniq of
                        TPUnique
TPInternal -> Maybe [ProofObj] -> RootOfTrust
RootOfTrust Maybe [ProofObj]
forall a. Maybe a
Nothing
                        TPUnique
TPQC       -> Maybe [ProofObj] -> RootOfTrust
RootOfTrust (Maybe [ProofObj] -> RootOfTrust)
-> Maybe [ProofObj] -> RootOfTrust
forall a b. (a -> b) -> a -> b
$ [ProofObj] -> Maybe [ProofObj]
forall a. a -> Maybe a
Just [ProofObj
quickCheckProof]
                        TPUnique
TPSorry    -> Maybe [ProofObj] -> RootOfTrust
RootOfTrust (Maybe [ProofObj] -> RootOfTrust)
-> Maybe [ProofObj] -> RootOfTrust
forall a b. (a -> b) -> a -> b
$ [ProofObj] -> Maybe [ProofObj]
forall a. a -> Maybe a
Just [ProofObj
sorry]
                        TPUser {}  -> RootOfTrust
self RootOfTrust -> RootOfTrust -> RootOfTrust
forall a. Semigroup a => a -> a -> a
<> (ProofObj -> RootOfTrust) -> [ProofObj] -> RootOfTrust
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Bool -> ProofObj -> RootOfTrust
rot Bool
False) [ProofObj]
dependencies

                -- if sorry or quickcheck is one of our direct dependencies, then we trust this proof.
                -- Note that we skip this at the top. Why? at that level, we want to see the direct
                -- dependency. But if we're down at a lower level, we just want to pick up
                self :: RootOfTrust
self | Bool
atTop                     = RootOfTrust
forall a. Monoid a => a
mempty
                     | (ProofObj -> Bool) -> [ProofObj] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ProofObj -> Bool
isUnsafe [ProofObj]
dependencies = Maybe [ProofObj] -> RootOfTrust
RootOfTrust (Maybe [ProofObj] -> RootOfTrust)
-> Maybe [ProofObj] -> RootOfTrust
forall a b. (a -> b) -> a -> b
$ [ProofObj] -> Maybe [ProofObj]
forall a. a -> Maybe a
Just [ProofObj
p]
                     | Bool
True                      = RootOfTrust
forall a. Monoid a => a
mempty

                isUnsafe :: ProofObj -> Bool
isUnsafe ProofObj{uniqId :: ProofObj -> TPUnique
uniqId = TPUnique
u} = TPUnique
u TPUnique -> [TPUnique] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TPUnique
TPSorry, TPUnique
TPQC]

                -- If we have any dependency that is not sorry itself, then we can skip all the sorries.
                -- Why? Because "sorry" will implicitly be coming from one of these anyhow. (In other
                -- words, we do not need to (or want to) distinguish between different uses of sorry.
                compress :: RootOfTrust -> RootOfTrust
compress (RootOfTrust Maybe [ProofObj]
mbps) = Maybe [ProofObj] -> RootOfTrust
RootOfTrust (Maybe [ProofObj] -> RootOfTrust)
-> Maybe [ProofObj] -> RootOfTrust
forall a b. (a -> b) -> a -> b
$ [ProofObj] -> [ProofObj]
reduce ([ProofObj] -> [ProofObj]) -> Maybe [ProofObj] -> Maybe [ProofObj]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [ProofObj]
mbps
                  where reduce :: [ProofObj] -> [ProofObj]
reduce [ProofObj]
ps = case (ProofObj -> Bool) -> [ProofObj] -> ([ProofObj], [ProofObj])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ProofObj -> Bool
isUnsafe [ProofObj]
ps of
                                      ([ProofObj]
l, []) | TPUnique
TPSorry TPUnique -> [TPUnique] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (ProofObj -> TPUnique) -> [ProofObj] -> [TPUnique]
forall a b. (a -> b) -> [a] -> [b]
map ProofObj -> TPUnique
uniqId [ProofObj]
l -> [ProofObj
sorry]
                                              | Bool
True                        -> [ProofObj
quickCheckProof]
                                      ([ProofObj]
_, [ProofObj]
os) -> [ProofObj]
os

-- | Calculate the modulo string for dependencies
concludeModulo :: [ProofObj] -> String
concludeModulo :: [ProofObj] -> [Char]
concludeModulo [ProofObj]
by = case (ProofObj -> RootOfTrust) -> [ProofObj] -> RootOfTrust
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Proof Any -> RootOfTrust
forall a. Proof a -> RootOfTrust
rootOfTrust (Proof Any -> RootOfTrust)
-> (ProofObj -> Proof Any) -> ProofObj -> RootOfTrust
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofObj -> Proof Any
forall a. ProofObj -> Proof a
Proof) [ProofObj]
by of
                      RootOfTrust Maybe [ProofObj]
Nothing   -> [Char]
""
                      RootOfTrust (Just [ProofObj]
ps) -> [Char]
" [Modulo: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [ProofObj] -> [Char]
shortProofNames [ProofObj]
ps [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"]"

-- | Make TP proofs quiet. Note that this setting will be effective with the
-- call to 'runTP'\/'runTPWith', i.e., if you change the solver in a call to 'Data.SBV.TP.lemmaWith'\/'Data.SBV.TP.theoremWith', we
-- will inherit the quiet settings from the surrounding environment.
tpQuiet :: Bool -> SMTConfig -> SMTConfig
tpQuiet :: Bool -> SMTConfig -> SMTConfig
tpQuiet Bool
b SMTConfig
cfg = SMTConfig
cfg{tpOptions = (tpOptions cfg) { quiet = b }}

-- | Change the size of the ribbon for TP proofs. Note that this setting will be effective with the
-- call to 'runTP'\/'runTPWith', i.e., if you change the solver in a call to 'Data.SBV.TP.lemmaWith'\/'Data.SBV.TP.theoremWith', we
-- will inherit the ribbon settings from the surrounding environment.
tpRibbon :: Int -> SMTConfig -> SMTConfig
tpRibbon :: Int -> SMTConfig -> SMTConfig
tpRibbon Int
i SMTConfig
cfg = SMTConfig
cfg{tpOptions = (tpOptions cfg) { ribbonLength = i }}

-- | Make TP proofs produce statistics. Note that this setting will be effective with the
-- call to 'runTP'\/'runTPWith', i.e., if you change the solver in a call to 'Data.SBV.TP.lemmaWith'\/'Data.SBV.TP.theoremWith', we
-- will inherit the statistics settings from the surrounding environment.
tpStats :: SMTConfig -> SMTConfig
tpStats :: SMTConfig -> SMTConfig
tpStats SMTConfig
cfg = SMTConfig
cfg{tpOptions = (tpOptions cfg) { printStats = True }}

-- | Make TP proofs use proof-cache. Note that if you use this option then you are obligated to ensure all
-- lemma\/theorem names\/type pairs you use are unique for the whole run. (That is, we will reuse proofs if they have the
-- same name and type; hence if you prove two theorems that share name and type will be considered the same.)
-- If you don't ensure this uniqueness,  the results are not guaranteed to be sound. A good tip is to run the proof at
-- least once to completion, and use cache for regression purposes to avoid re-runs. Also, this setting will be effective
-- with the call to 'runTP'\/'runTPWith', i.e., if you -- the solver in a call to 'Data.SBV.TP.lemmaWith'\/'Data.SBV.TP.theoremWith', we will
-- inherit the caching behavior settings from the surrounding environment.
tpCache :: SMTConfig -> SMTConfig
tpCache :: SMTConfig -> SMTConfig
tpCache SMTConfig
cfg = SMTConfig
cfg{tpOptions = (tpOptions cfg) { cacheProofs = True }}

-- | When proving assumptions for each step, print them as well. Normally, SBV doesn't
-- print assumptions in each proof step, though it does prove them as they are typically trivial.
-- But in certain cases seeing them would be helpful.
tpAsms :: SMTConfig -> SMTConfig
tpAsms :: SMTConfig -> SMTConfig
tpAsms SMTConfig
cfg = SMTConfig
cfg{tpOptions = (tpOptions cfg) { printAsms = True }}