{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}

{-|
Module       : ATP.Prove
Description  : Interface to automated theorem provers.
Copyright    : (c) Evgenii Kotelnikov, 2019-2021
License      : GPL-3
Maintainer   : evgeny.kotelnikov@gmail.com
Stability    : experimental

Interface to automated theorem provers.
-}

module ATP.Prove (
  ProvingOptions(..),
  defaultOptions,
  refute,
  refuteUsing,
  refuteWith,
  prove,
  proveUsing,
  proveWith
) where

import Control.Monad (when)
import Data.Text (Text)
import qualified Data.Text as T (pack)
import Data.TPTP (TPTP)
import Data.TPTP.Parse.Text (parseTSTPOnly)
import Data.TPTP.Pretty (pretty)
import System.Exit (ExitCode(..))
import System.Process (readProcessWithExitCode)
import Text.PrettyPrint.ANSI.Leijen (bold, text)

import ATP.Error
import ATP.FOL (Clauses, Theorem, Solution)
import ATP.Codec.TPTP (encodeClauses, encodeTheorem, decodeSolution)
import ATP.Prover


-- | The options that describe what theorem prover to use for a problem and
-- how to run it.
data ProvingOptions = ProvingOptions {
  ProvingOptions -> Prover
prover      :: Prover,
  ProvingOptions -> TimeLimit
timeLimit   :: TimeLimit,
  ProvingOptions -> TimeLimit
memoryLimit :: MemoryLimit,
  ProvingOptions -> Bool
debug       :: Bool -- ^ If @True@, print the input, the cli command,
                      --   the exit code and the output of the prover
} deriving (ProvingOptions -> ProvingOptions -> Bool
(ProvingOptions -> ProvingOptions -> Bool)
-> (ProvingOptions -> ProvingOptions -> Bool) -> Eq ProvingOptions
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ProvingOptions -> ProvingOptions -> Bool
$c/= :: ProvingOptions -> ProvingOptions -> Bool
== :: ProvingOptions -> ProvingOptions -> Bool
$c== :: ProvingOptions -> ProvingOptions -> Bool
Eq, TimeLimit -> ProvingOptions -> ShowS
[ProvingOptions] -> ShowS
ProvingOptions -> String
(TimeLimit -> ProvingOptions -> ShowS)
-> (ProvingOptions -> String)
-> ([ProvingOptions] -> ShowS)
-> Show ProvingOptions
forall a.
(TimeLimit -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProvingOptions] -> ShowS
$cshowList :: [ProvingOptions] -> ShowS
show :: ProvingOptions -> String
$cshow :: ProvingOptions -> String
showsPrec :: TimeLimit -> ProvingOptions -> ShowS
$cshowsPrec :: TimeLimit -> ProvingOptions -> ShowS
Show, Eq ProvingOptions
Eq ProvingOptions
-> (ProvingOptions -> ProvingOptions -> Ordering)
-> (ProvingOptions -> ProvingOptions -> Bool)
-> (ProvingOptions -> ProvingOptions -> Bool)
-> (ProvingOptions -> ProvingOptions -> Bool)
-> (ProvingOptions -> ProvingOptions -> Bool)
-> (ProvingOptions -> ProvingOptions -> ProvingOptions)
-> (ProvingOptions -> ProvingOptions -> ProvingOptions)
-> Ord ProvingOptions
ProvingOptions -> ProvingOptions -> Bool
ProvingOptions -> ProvingOptions -> Ordering
ProvingOptions -> ProvingOptions -> ProvingOptions
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ProvingOptions -> ProvingOptions -> ProvingOptions
$cmin :: ProvingOptions -> ProvingOptions -> ProvingOptions
max :: ProvingOptions -> ProvingOptions -> ProvingOptions
$cmax :: ProvingOptions -> ProvingOptions -> ProvingOptions
>= :: ProvingOptions -> ProvingOptions -> Bool
$c>= :: ProvingOptions -> ProvingOptions -> Bool
> :: ProvingOptions -> ProvingOptions -> Bool
$c> :: ProvingOptions -> ProvingOptions -> Bool
<= :: ProvingOptions -> ProvingOptions -> Bool
$c<= :: ProvingOptions -> ProvingOptions -> Bool
< :: ProvingOptions -> ProvingOptions -> Bool
$c< :: ProvingOptions -> ProvingOptions -> Bool
compare :: ProvingOptions -> ProvingOptions -> Ordering
$ccompare :: ProvingOptions -> ProvingOptions -> Ordering
$cp1Ord :: Eq ProvingOptions
Ord)

-- | The default options used by 'refute' and 'prove'.
--
-- >>> defaultOptions
-- ProvingOptions {prover = Prover {vendor = E, executable = "eprover"}, timeLimit = 300, memoryLimit = 2000, debug = False}
defaultOptions :: ProvingOptions
defaultOptions :: ProvingOptions
defaultOptions = ProvingOptions :: Prover -> TimeLimit -> TimeLimit -> Bool -> ProvingOptions
ProvingOptions {
  prover :: Prover
prover = Prover
defaultProver,
  timeLimit :: TimeLimit
timeLimit = TimeLimit
300,
  memoryLimit :: TimeLimit
memoryLimit = TimeLimit
2000,
  debug :: Bool
debug = Bool
False
}

-- | Attempt to refute a set of clauses using 'defaultProver'.
--
-- > refute = refuteWith defaultOptions
refute :: Clauses -> IO (Partial Solution)
refute :: Clauses -> IO (Partial Solution)
refute = ProvingOptions -> Clauses -> IO (Partial Solution)
refuteWith ProvingOptions
defaultOptions

-- | Attempt to refute a set of clauses using a given prover.
refuteUsing :: Prover -> Clauses -> IO (Partial Solution)
refuteUsing :: Prover -> Clauses -> IO (Partial Solution)
refuteUsing Prover
p = ProvingOptions -> Clauses -> IO (Partial Solution)
refuteWith ProvingOptions
defaultOptions{prover :: Prover
prover = Prover
p}

-- | Attempt to refute a set of clauses with a given set of options.
refuteWith :: ProvingOptions -> Clauses -> IO (Partial Solution)
refuteWith :: ProvingOptions -> Clauses -> IO (Partial Solution)
refuteWith ProvingOptions
opts = ProvingOptions -> TPTP -> IO (Partial Solution)
runWith ProvingOptions
opts (TPTP -> IO (Partial Solution))
-> (Clauses -> TPTP) -> Clauses -> IO (Partial Solution)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clauses -> TPTP
encodeClauses

-- | Attempt to prove a theorem using 'defaultProver'.
--
-- > prove = proveWith defaultOptions
prove :: Theorem -> IO (Partial Solution)
prove :: Theorem -> IO (Partial Solution)
prove = ProvingOptions -> Theorem -> IO (Partial Solution)
proveWith ProvingOptions
defaultOptions

-- | Attempt to prove a theorem using a given prover.
proveUsing :: Prover -> Theorem -> IO (Partial Solution)
proveUsing :: Prover -> Theorem -> IO (Partial Solution)
proveUsing Prover
p = ProvingOptions -> Theorem -> IO (Partial Solution)
proveWith ProvingOptions
defaultOptions{prover :: Prover
prover = Prover
p}

-- | Attempt to prove a theorem with a given set of options.
proveWith :: ProvingOptions -> Theorem -> IO (Partial Solution)
proveWith :: ProvingOptions -> Theorem -> IO (Partial Solution)
proveWith ProvingOptions
opts = ProvingOptions -> TPTP -> IO (Partial Solution)
runWith ProvingOptions
opts (TPTP -> IO (Partial Solution))
-> (Theorem -> TPTP) -> Theorem -> IO (Partial Solution)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Theorem -> TPTP
encodeTheorem

runWith :: ProvingOptions -> TPTP -> IO (Partial Solution)
runWith :: ProvingOptions -> TPTP -> IO (Partial Solution)
runWith ProvingOptions
opts TPTP
tptp = do
  let ProvingOptions{Prover
prover :: Prover
prover :: ProvingOptions -> Prover
prover} = ProvingOptions
opts
  let Prover{Vendor
vendor :: Prover -> Vendor
vendor :: Vendor
vendor} = Prover
prover
  let input :: String
input = Doc Any -> String
forall a. Show a => a -> String
show (TPTP -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty TPTP
tptp)
  (ExitCode
exitCode, Text
stdout, Text
stderr) <- ProvingOptions -> String -> IO (ExitCode, Text, Text)
runProver ProvingOptions
opts String
input
  let output :: Partial Text
output = Vendor -> ExitCode -> Text -> Text -> Partial Text
proverOutput Vendor
vendor ExitCode
exitCode Text
stdout Text
stderr
  let solution :: Partial Solution
solution = Partial Text
output Partial Text -> (Text -> Partial Solution) -> Partial Solution
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Text -> Partial Solution
parseSolution
  Partial Solution -> IO (Partial Solution)
forall (m :: * -> *) a. Monad m => a -> m a
return Partial Solution
solution

runProver :: ProvingOptions -> String -> IO (ExitCode, Text, Text)
runProver :: ProvingOptions -> String -> IO (ExitCode, Text, Text)
runProver ProvingOptions
opts String
input = do
  let ProvingOptions{Prover
prover :: Prover
prover :: ProvingOptions -> Prover
prover, TimeLimit
timeLimit :: TimeLimit
timeLimit :: ProvingOptions -> TimeLimit
timeLimit, TimeLimit
memoryLimit :: TimeLimit
memoryLimit :: ProvingOptions -> TimeLimit
memoryLimit, Bool
debug :: Bool
debug :: ProvingOptions -> Bool
debug} = ProvingOptions
opts
  let Prover{Vendor
vendor :: Vendor
vendor :: Prover -> Vendor
vendor, String
executable :: Prover -> String
executable :: String
executable} = Prover
prover
  let arguments :: [String]
arguments = Vendor -> TimeLimit -> TimeLimit -> [String]
proverArguments Vendor
vendor TimeLimit
timeLimit TimeLimit
memoryLimit
  let debugPrint :: String -> String -> IO ()
debugPrint String
header String
str = Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
debug (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
                              Doc -> IO ()
forall a. Show a => a -> IO ()
print (Doc -> Doc
bold (String -> Doc
text String
header)) IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                              String -> IO ()
putStrLn String
str IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> IO ()
putStr String
"\n"
  String -> String -> IO ()
debugPrint String
"Input" String
input
  String -> String -> IO ()
debugPrint String
"Command" (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords (String
executableString -> [String] -> [String]
forall a. a -> [a] -> [a]
:[String]
arguments)
  (ExitCode
exitCode, String
stdout, String
stderr) <- String -> [String] -> String -> IO (ExitCode, String, String)
readProcessWithExitCode String
executable [String]
arguments String
input
  String -> String -> IO ()
debugPrint String
"Exit code" (ExitCode -> String
forall a. Show a => a -> String
show ExitCode
exitCode)
  String -> String -> IO ()
debugPrint String
"Standard output" String
stdout
  String -> String -> IO ()
debugPrint String
"Standard error"  String
stderr
  (ExitCode, Text, Text) -> IO (ExitCode, Text, Text)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExitCode
exitCode, String -> Text
T.pack String
stdout, String -> Text
T.pack String
stderr)

parseSolution :: Text -> Partial Solution
parseSolution :: Text -> Partial Solution
parseSolution = (String -> Partial Solution)
-> (TSTP -> Partial Solution)
-> Either String TSTP
-> Partial Solution
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either String -> Partial Solution
forall (m :: * -> *) a. Monad m => String -> PartialT m a
parsingError TSTP -> Partial Solution
decodeSolution (Either String TSTP -> Partial Solution)
-> (Text -> Either String TSTP) -> Text -> Partial Solution
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Either String TSTP
parseTSTPOnly