{-# LANGUAGE GADTs #-}
module Jukebox.ExternalProvers.E where

import Jukebox.Form hiding (tag, Or, run_)
import Jukebox.Name
import Jukebox.Options
import Control.Applicative hiding (Const)
import Control.Monad
import Jukebox.Utils
import Jukebox.TPTP.Parsec hiding (run)
import Jukebox.TPTP.Parse.Core hiding (newFunction, Term)
import Jukebox.TPTP.Print
import Jukebox.TPTP.Lexer hiding (Normal, keyword, Axiom, Var, Theorem)
import Data.Maybe
import qualified Data.Map.Strict as Map
import Data.Map(Map)
import Data.Symbol

data EFlags = EFlags {
  EFlags -> String
eprover :: String,
  EFlags -> Maybe Int
timeout :: Maybe Int,
  EFlags -> Maybe Int
memory :: Maybe Int
  }

eflags :: OptionParser EFlags
eflags =
  String -> OptionParser EFlags -> OptionParser EFlags
forall a. String -> OptionParser a -> OptionParser a
inGroup String
"E prover options" (OptionParser EFlags -> OptionParser EFlags)
-> OptionParser EFlags -> OptionParser EFlags
forall a b. (a -> b) -> a -> b
$
  String -> Maybe Int -> Maybe Int -> EFlags
EFlags (String -> Maybe Int -> Maybe Int -> EFlags)
-> Annotated [Flag] ParParser String
-> Annotated [Flag] ParParser (Maybe Int -> Maybe Int -> EFlags)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    String
-> [String]
-> String
-> ArgParser String
-> Annotated [Flag] ParParser String
forall a. String -> [String] -> a -> ArgParser a -> OptionParser a
flag String
"eprover"
      [String
"Path to the E theorem prover (\"eprover\" by default)."]
      String
"eprover"
      ArgParser String
argFile Annotated [Flag] ParParser (Maybe Int -> Maybe Int -> EFlags)
-> Annotated [Flag] ParParser (Maybe Int)
-> Annotated [Flag] ParParser (Maybe Int -> EFlags)
forall a b.
Annotated [Flag] ParParser (a -> b)
-> Annotated [Flag] ParParser a -> Annotated [Flag] ParParser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
    String
-> [String]
-> Maybe Int
-> ArgParser (Maybe Int)
-> Annotated [Flag] ParParser (Maybe Int)
forall a. String -> [String] -> a -> ArgParser a -> OptionParser a
flag String
"timeout"
      [String
"Timeout for E, in seconds (off by default)."]
      Maybe Int
forall a. Maybe a
Nothing
      ((Int -> Maybe Int)
-> Annotated [String] SeqParser Int -> ArgParser (Maybe Int)
forall a b.
(a -> b)
-> Annotated [String] SeqParser a -> Annotated [String] SeqParser b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Maybe Int
forall a. a -> Maybe a
Just Annotated [String] SeqParser Int
forall a. (Read a, Num a) => ArgParser a
argNum) Annotated [Flag] ParParser (Maybe Int -> EFlags)
-> Annotated [Flag] ParParser (Maybe Int) -> OptionParser EFlags
forall a b.
Annotated [Flag] ParParser (a -> b)
-> Annotated [Flag] ParParser a -> Annotated [Flag] ParParser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
    String
-> [String]
-> Maybe Int
-> ArgParser (Maybe Int)
-> Annotated [Flag] ParParser (Maybe Int)
forall a. String -> [String] -> a -> ArgParser a -> OptionParser a
flag String
"memory"
      [String
"Memory limit for E, in megabytes (unlimited by default)."]
      Maybe Int
forall a. Maybe a
Nothing
      ((Int -> Maybe Int)
-> Annotated [String] SeqParser Int -> ArgParser (Maybe Int)
forall a b.
(a -> b)
-> Annotated [String] SeqParser a -> Annotated [String] SeqParser b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Maybe Int
forall a. a -> Maybe a
Just Annotated [String] SeqParser Int
forall a. (Read a, Num a) => ArgParser a
argNum)

-- Work around bug in E answer coding.
mangleAnswer :: Symbolic a => a -> NameM a
mangleAnswer :: forall a. Symbolic a => a -> NameM a
mangleAnswer a
t =
  case a -> TypeOf a
forall a. Symbolic a => a -> TypeOf a
typeOf a
t of
    TypeOf a
Term -> Term -> NameM Term
term a
Term
t
    TypeOf a
_ -> (forall a. Symbolic a => a -> NameM a) -> a -> NameM a
forall (m :: * -> *) a.
(Monad m, Symbolic a) =>
(forall a1. Symbolic a1 => a1 -> m a1) -> a -> m a
recursivelyM a1 -> NameM a1
forall a. Symbolic a => a -> NameM a
mangleAnswer a
t
  where term :: Term -> NameM Term
term (Function
f :@: [Term
t]) | Function -> String
forall a. Named a => a -> String
base Function
f String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"$answer" = do
          Function
wrap <- String -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction String
"answer" [Term -> Type
forall a. Typed a => a -> Type
typ Term
t] ([Type] -> Type
forall a. HasCallStack => [a] -> a
head (Function -> [Type]
funArgs Function
f))
          Term -> NameM Term
forall a. a -> NameM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Function
f Function -> [Term] -> Term
:@: [Function
wrap Function -> [Term] -> Term
:@: [Term
t]])
        term Term
t = (forall a. Symbolic a => a -> NameM a) -> Term -> NameM Term
forall (m :: * -> *) a.
(Monad m, Symbolic a) =>
(forall a1. Symbolic a1 => a1 -> m a1) -> a -> m a
recursivelyM a1 -> NameM a1
forall a. Symbolic a => a -> NameM a
mangleAnswer Term
t

runE :: EFlags -> Problem Form -> IO (Either Answer [Term])
runE :: EFlags -> Problem Form -> IO (Either Answer [Term])
runE EFlags
flags Problem Form
prob
  | Bool -> Bool
not (Problem Form -> Bool
forall a. Symbolic a => a -> Bool
isFof Problem Form
prob) = String -> IO (Either Answer [Term])
forall a. HasCallStack => String -> a
error String
"runE: E doesn't support many-typed problems"
  | Bool
otherwise = do
    (ExitCode
_code, String
str) <- String -> [String] -> String -> IO (ExitCode, String)
popen (EFlags -> String
eprover EFlags
flags) [String]
eflags
                   (Problem Form -> String
showProblem (Problem Form
-> (Problem Form -> NameM (Problem Form)) -> Problem Form
forall a b. Symbolic a => a -> (a -> NameM b) -> b
run Problem Form
prob Problem Form -> NameM (Problem Form)
forall a. Symbolic a => a -> NameM a
mangleAnswer))
    Either Answer [Term] -> IO (Either Answer [Term])
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Problem Form -> String -> Either Answer [Term]
forall a. Symbolic a => a -> String -> Either Answer [Term]
extractAnswer Problem Form
prob String
str)
  where eflags :: [String]
eflags = [ String
"--soft-cpu-limit=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n | Just Int
n <- [EFlags -> Maybe Int
timeout EFlags
flags] ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                 [String
"--memory-limit=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n | Just Int
n <- [EFlags -> Maybe Int
memory EFlags
flags] ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                 [String
"--tstp-in", String
"--tstp-out", String
"-tAuto", String
"-xAuto"] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                 [String
"-l", String
"0"]

extractAnswer :: Symbolic a => a -> String -> Either Answer [Term]
extractAnswer :: forall a. Symbolic a => a -> String -> Either Answer [Term]
extractAnswer a
prob String
str = Either Answer [Term]
-> Maybe (Either Answer [Term]) -> Either Answer [Term]
forall a. a -> Maybe a -> a
fromMaybe (Answer -> Either Answer [Term]
forall a b. a -> Either a b
Left Answer
status) (([Term] -> Either Answer [Term])
-> Maybe [Term] -> Maybe (Either Answer [Term])
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Term] -> Either Answer [Term]
forall a b. b -> Either a b
Right Maybe [Term]
answer)
  where varMap :: Map Symbol Variable
varMap = [(Symbol, Variable)] -> Map Symbol Variable
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(String -> Symbol
intern (Name -> String
forall a. Show a => a -> String
show (Variable -> Name
forall a. Named a => a -> Name
name Variable
x)), Variable
x) | Variable
x <- a -> [Variable]
forall a. Symbolic a => a -> [Variable]
vars a
prob]
        funMap :: Map Symbol Function
funMap = [(Symbol, Function)] -> Map Symbol Function
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(String -> Symbol
intern (Name -> String
forall a. Show a => a -> String
show (Function -> Name
forall a. Named a => a -> Name
name Function
x)), Function
x) | Function
x <- a -> [Function]
forall a. Symbolic a => a -> [Function]
functions a
prob]
        result :: [String]
result = String -> [String]
lines String
str
        status :: Answer
status = [Answer] -> Answer
forall a. HasCallStack => [a] -> a
head ([Answer] -> Answer) -> [Answer] -> Answer
forall a b. (a -> b) -> a -> b
$
          [SatReason -> Maybe [String] -> Answer
Sat SatReason
Satisfiable Maybe [String]
forall a. Maybe a
Nothing | String
"# SZS status Satisfiable" <- [String]
result] [Answer] -> [Answer] -> [Answer]
forall a. [a] -> [a] -> [a]
++
          [SatReason -> Maybe [String] -> Answer
Sat SatReason
CounterSatisfiable Maybe [String]
forall a. Maybe a
Nothing | String
"# SZS status CounterSatisfiable" <- [String]
result] [Answer] -> [Answer] -> [Answer]
forall a. [a] -> [a] -> [a]
++
          [UnsatReason -> Maybe [String] -> Answer
Unsat UnsatReason
Unsatisfiable Maybe [String]
forall a. Maybe a
Nothing | String
"# SZS status Unsatisfiable" <- [String]
result] [Answer] -> [Answer] -> [Answer]
forall a. [a] -> [a] -> [a]
++
          [UnsatReason -> Maybe [String] -> Answer
Unsat UnsatReason
Theorem Maybe [String]
forall a. Maybe a
Nothing | String
"# SZS status Theorem" <- [String]
result] [Answer] -> [Answer] -> [Answer]
forall a. [a] -> [a] -> [a]
++
          [NoAnswerReason -> Answer
NoAnswer NoAnswerReason
Timeout | String
"# SZS status ResourceOut" <- [String]
result] [Answer] -> [Answer] -> [Answer]
forall a. [a] -> [a] -> [a]
++
          [NoAnswerReason -> Answer
NoAnswer NoAnswerReason
Timeout | String
"# SZS status Timeout" <- [String]
result] [Answer] -> [Answer] -> [Answer]
forall a. [a] -> [a] -> [a]
++
          [NoAnswerReason -> Answer
NoAnswer NoAnswerReason
Timeout | String
"# SZS status MemyOut" <- [String]
result] [Answer] -> [Answer] -> [Answer]
forall a. [a] -> [a] -> [a]
++
          [NoAnswerReason -> Answer
NoAnswer NoAnswerReason
GaveUp]
        answer :: Maybe [Term]
answer = [[Term]] -> Maybe [Term]
forall a. [a] -> Maybe a
listToMaybe ([[Term]] -> Maybe [Term]) -> [[Term]] -> Maybe [Term]
forall a b. (a -> b) -> a -> b
$
          [ String -> [Term]
parse String
xs
          | String
line <- [String]
result
          , let prefix :: String
prefix = String
"# SZS answers Tuple ["
                suffix :: String
suffix = String
"|_]"
                (String
prefix', String
mid) = Int -> String -> (String, String)
forall a. Int -> [a] -> ([a], [a])
splitAt (String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
prefix) String
line
                (String
xs, String
suffix') = Int -> String -> (String, String)
forall a. Int -> [a] -> ([a], [a])
splitAt (String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
mid 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 String
suffix) String
mid
          , String
prefix String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
prefix'
          , String
suffix String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
suffix' ]
        parse :: String -> [Term]
parse String
xs =
          let toks :: TokenStream
toks = String -> TokenStream
scan String
xs
          in case Parsec ParsecState [Term]
-> ParsecState -> Result (Position ParsecState) [Term]
forall a c b.
Stream a c =>
Parsec a b -> a -> Result (Position a) b
run_ Parsec ParsecState [Term]
parser (ParseState -> TokenStream -> ParsecState
forall state stream. state -> stream -> UserState state stream
UserState (Maybe String -> ParseState
initialState Maybe String
forall a. Maybe a
Nothing) TokenStream
toks) of
            Ok Position ParsecState
_ [Term]
ts -> [Term]
ts
            Result (Position ParsecState) [Term]
_ -> String -> [Term]
forall a. HasCallStack => String -> a
error String
"runE: couldn't parse result from E"
        parser :: Parsec ParsecState [Term]
parser =
          Parsec ParsecState [Term] -> Parsec ParsecState [Term]
forall a. Parser a -> Parser a
parens (Parser Term -> Parser Term
forall a. Parser a -> Parser a
bracks Parser Term
term Parser Term
-> Parsec ParsecState Token -> Parsec ParsecState [Term]
forall a b c. Parsec a b -> Parsec a c -> Parsec a [b]
`sepBy1` Punct -> Parsec ParsecState Token
forall {a}. Stream a Token => Punct -> Parsec a Token
punct Punct
Or)
          Parsec ParsecState [Term]
-> Parsec ParsecState [Term] -> Parsec ParsecState [Term]
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Term -> [Term]) -> Parser Term -> Parsec ParsecState [Term]
forall a b.
(a -> b) -> Parsec ParsecState a -> Parsec ParsecState b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[]) (Parser Term -> Parser Term
forall a. Parser a -> Parser a
bracks Parser Term
term)
        term :: Parser Term
term =
          (Symbol -> Term) -> Parsec ParsecState Symbol -> Parser Term
forall a b.
(a -> b) -> Parsec ParsecState a -> Parsec ParsecState b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Variable -> Term
Var (Variable -> Term) -> (Symbol -> Variable) -> Symbol -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Symbol Variable -> Symbol -> Variable
forall a. Map Symbol a -> Symbol -> a
lookup Map Symbol Variable
varMap) Parsec ParsecState Symbol
variable Parser Term -> Parser Term -> Parser Term
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
          (Function -> [Term] -> Term)
-> Parsec ParsecState Function
-> Parsec ParsecState [Term]
-> Parser Term
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Function -> [Term] -> Term
(:@:) ((Symbol -> Function)
-> Parsec ParsecState Symbol -> Parsec ParsecState Function
forall a b.
(a -> b) -> Parsec ParsecState a -> Parsec ParsecState b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Map Symbol Function -> Symbol -> Function
forall a. Map Symbol a -> Symbol -> a
lookup Map Symbol Function
funMap) Parsec ParsecState Symbol
atom) Parsec ParsecState [Term]
terms
        terms :: Parsec ParsecState [Term]
terms =
          Parsec ParsecState [Term] -> Parsec ParsecState [Term]
forall a. Parser a -> Parser a
bracks (Parser Term
term Parser Term
-> Parsec ParsecState Token -> Parsec ParsecState [Term]
forall a b c. Parsec a b -> Parsec a c -> Parsec a [b]
`sepBy1` Punct -> Parsec ParsecState Token
forall {a}. Stream a Token => Punct -> Parsec a Token
punct Punct
Comma)
          Parsec ParsecState [Term]
-> Parsec ParsecState [Term] -> Parsec ParsecState [Term]
forall a.
Parsec ParsecState a
-> Parsec ParsecState a -> Parsec ParsecState a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Term] -> Parsec ParsecState [Term]
forall a. a -> Parsec ParsecState a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        lookup :: Map Symbol a -> Symbol -> a
        lookup :: forall a. Map Symbol a -> Symbol -> a
lookup Map Symbol a
m Symbol
x = a -> Symbol -> Map Symbol a -> a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> a
forall a. HasCallStack => String -> a
error String
"runE: result from E mentions free names") Symbol
x Map Symbol a
m