-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Tools.KDUtils
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Various KnuckleDrugger machinery.
-----------------------------------------------------------------------------

{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NamedFieldPuns             #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Tools.KDUtils (
         KD, runKD, runKDWith
       , start, finish
       ) where

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

import Data.List (intercalate)
import System.IO (hFlush, stdout)

import Data.SBV.Core.Symbolic  (SMTConfig)
import Data.SBV.Provers.Prover (defaultSMTCfg, SMTConfig(..))

-- | Monad for running KnuckleDragger proofs in.
newtype KD a = KD (ReaderT SMTConfig IO a)
            deriving newtype (Functor KD
Functor KD =>
(forall a. a -> KD a)
-> (forall a b. KD (a -> b) -> KD a -> KD b)
-> (forall a b c. (a -> b -> c) -> KD a -> KD b -> KD c)
-> (forall a b. KD a -> KD b -> KD b)
-> (forall a b. KD a -> KD b -> KD a)
-> Applicative KD
forall a. a -> KD a
forall a b. KD a -> KD b -> KD a
forall a b. KD a -> KD b -> KD b
forall a b. KD (a -> b) -> KD a -> KD b
forall a b c. (a -> b -> c) -> KD a -> KD b -> KD 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 -> KD a
pure :: forall a. a -> KD a
$c<*> :: forall a b. KD (a -> b) -> KD a -> KD b
<*> :: forall a b. KD (a -> b) -> KD a -> KD b
$cliftA2 :: forall a b c. (a -> b -> c) -> KD a -> KD b -> KD c
liftA2 :: forall a b c. (a -> b -> c) -> KD a -> KD b -> KD c
$c*> :: forall a b. KD a -> KD b -> KD b
*> :: forall a b. KD a -> KD b -> KD b
$c<* :: forall a b. KD a -> KD b -> KD a
<* :: forall a b. KD a -> KD b -> KD a
Applicative, (forall a b. (a -> b) -> KD a -> KD b)
-> (forall a b. a -> KD b -> KD a) -> Functor KD
forall a b. a -> KD b -> KD a
forall a b. (a -> b) -> KD a -> KD 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) -> KD a -> KD b
fmap :: forall a b. (a -> b) -> KD a -> KD b
$c<$ :: forall a b. a -> KD b -> KD a
<$ :: forall a b. a -> KD b -> KD a
Functor, Applicative KD
Applicative KD =>
(forall a b. KD a -> (a -> KD b) -> KD b)
-> (forall a b. KD a -> KD b -> KD b)
-> (forall a. a -> KD a)
-> Monad KD
forall a. a -> KD a
forall a b. KD a -> KD b -> KD b
forall a b. KD a -> (a -> KD b) -> KD 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. KD a -> (a -> KD b) -> KD b
>>= :: forall a b. KD a -> (a -> KD b) -> KD b
$c>> :: forall a b. KD a -> KD b -> KD b
>> :: forall a b. KD a -> KD b -> KD b
$creturn :: forall a. a -> KD a
return :: forall a. a -> KD a
Monad, Monad KD
Monad KD => (forall a. IO a -> KD a) -> MonadIO KD
forall a. IO a -> KD a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
$cliftIO :: forall a. IO a -> KD a
liftIO :: forall a. IO a -> KD a
MonadIO, MonadReader SMTConfig, Monad KD
Monad KD => (forall a. String -> KD a) -> MonadFail KD
forall a. String -> KD a
forall (m :: * -> *).
Monad m =>
(forall a. String -> m a) -> MonadFail m
$cfail :: forall a. String -> KD a
fail :: forall a. String -> KD a
MonadFail)

-- | Run a KD proof, using the default configuration.
runKD :: KD a -> IO a
runKD :: forall a. KD a -> IO a
runKD = SMTConfig -> KD a -> IO a
forall a. SMTConfig -> KD a -> IO a
runKDWith SMTConfig
defaultSMTCfg

-- | Run a KD proof, using the given configuration.
runKDWith :: SMTConfig -> KD a -> IO a
runKDWith :: forall a. SMTConfig -> KD a -> IO a
runKDWith SMTConfig
cfg (KD ReaderT SMTConfig IO a
f) = ReaderT SMTConfig IO a -> SMTConfig -> IO a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT SMTConfig IO a
f SMTConfig
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 :: Bool -> String -> [String] -> KD Int
start Bool
newLine String
what [String]
nms = IO Int -> KD Int
forall a. IO a -> KD a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Int -> KD Int) -> IO Int -> KD Int
forall a b. (a -> b) -> a -> b
$ do String -> IO ()
putStr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
line String -> String -> String
forall a. [a] -> [a] -> [a]
++ if Bool
newLine then String
"\n" else String
""
                                     Handle -> IO ()
hFlush Handle
stdout
                                     Int -> IO Int
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
line)
  where tab :: Int
tab    = Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* [String] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Int -> [String] -> [String]
forall a. Int -> [a] -> [a]
drop Int
1 [String]
nms)
        indent :: String
indent = Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
tab Char
' '
        tag :: String
tag    = String
what String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"." [String]
nms
        line :: String
line   = String
indent String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tag

-- | Finish a proof. First argument is what we got from the call of 'start' above.
finish :: String -> Int -> KD ()
finish :: String -> Int -> KD ()
finish String
what Int
skip = do SMTConfig{kdRibbonLength} <- KD SMTConfig
forall r (m :: * -> *). MonadReader r m => m r
ask
                      liftIO $ putStrLn $ replicate (kdRibbonLength - skip) ' ' ++ what