{- |
Module      :  ./SoftFOL/EProver.hs
Description :  Analyze eprover output
Copyright   :  (c) Jonathan von Schroeder, DFKI Bremen 2013
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>
Stability   :  provisional
Portability :  portable
-}

module SoftFOL.EProver (processProof, zipF, supportsProofObject,
                        digraph, axioms, conjectures, alias, proofInfo) where

import Text.ParserCombinators.Parsec
import Common.Parsec
import SoftFOL.ParseTPTP (singleQuoted, form, genTerm, ppGenTerm)
import SoftFOL.PrintTPTP (printTPTP)
import SoftFOL.Sign (SPTerm (..))
import qualified Data.Set as Set
import System.Exit
import Common.Utils (executeProcess)
import Common.Doc (renderText)
import Common.GlobalAnnotations (emptyGlobalAnnos)
import qualified Data.Map as Map
import Data.Char (toLower)
import Data.Maybe (fromJust, fromMaybe, isNothing)
import Data.List (foldl', intercalate)
import Control.Monad (liftM)

data Role = Axiom | Conjecture | Other deriving (Int -> Role -> ShowS
[Role] -> ShowS
Role -> String
(Int -> Role -> ShowS)
-> (Role -> String) -> ([Role] -> ShowS) -> Show Role
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Role] -> ShowS
$cshowList :: [Role] -> ShowS
show :: Role -> String
$cshow :: Role -> String
showsPrec :: Int -> Role -> ShowS
$cshowsPrec :: Int -> Role -> ShowS
Show, Role -> Role -> Bool
(Role -> Role -> Bool) -> (Role -> Role -> Bool) -> Eq Role
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Role -> Role -> Bool
$c/= :: Role -> Role -> Bool
== :: Role -> Role -> Bool
$c== :: Role -> Role -> Bool
Eq)

data InferenceParent = PTerm String |
                       PInferred InferenceRule |
                       PBuiltinTheory String deriving (Int -> InferenceParent -> ShowS
[InferenceParent] -> ShowS
InferenceParent -> String
(Int -> InferenceParent -> ShowS)
-> (InferenceParent -> String)
-> ([InferenceParent] -> ShowS)
-> Show InferenceParent
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [InferenceParent] -> ShowS
$cshowList :: [InferenceParent] -> ShowS
show :: InferenceParent -> String
$cshow :: InferenceParent -> String
showsPrec :: Int -> InferenceParent -> ShowS
$cshowsPrec :: Int -> InferenceParent -> ShowS
Show, InferenceParent -> InferenceParent -> Bool
(InferenceParent -> InferenceParent -> Bool)
-> (InferenceParent -> InferenceParent -> Bool)
-> Eq InferenceParent
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: InferenceParent -> InferenceParent -> Bool
$c/= :: InferenceParent -> InferenceParent -> Bool
== :: InferenceParent -> InferenceParent -> Bool
$c== :: InferenceParent -> InferenceParent -> Bool
Eq, Eq InferenceParent
Eq InferenceParent =>
(InferenceParent -> InferenceParent -> Ordering)
-> (InferenceParent -> InferenceParent -> Bool)
-> (InferenceParent -> InferenceParent -> Bool)
-> (InferenceParent -> InferenceParent -> Bool)
-> (InferenceParent -> InferenceParent -> Bool)
-> (InferenceParent -> InferenceParent -> InferenceParent)
-> (InferenceParent -> InferenceParent -> InferenceParent)
-> Ord InferenceParent
InferenceParent -> InferenceParent -> Bool
InferenceParent -> InferenceParent -> Ordering
InferenceParent -> InferenceParent -> InferenceParent
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 :: InferenceParent -> InferenceParent -> InferenceParent
$cmin :: InferenceParent -> InferenceParent -> InferenceParent
max :: InferenceParent -> InferenceParent -> InferenceParent
$cmax :: InferenceParent -> InferenceParent -> InferenceParent
>= :: InferenceParent -> InferenceParent -> Bool
$c>= :: InferenceParent -> InferenceParent -> Bool
> :: InferenceParent -> InferenceParent -> Bool
$c> :: InferenceParent -> InferenceParent -> Bool
<= :: InferenceParent -> InferenceParent -> Bool
$c<= :: InferenceParent -> InferenceParent -> Bool
< :: InferenceParent -> InferenceParent -> Bool
$c< :: InferenceParent -> InferenceParent -> Bool
compare :: InferenceParent -> InferenceParent -> Ordering
$ccompare :: InferenceParent -> InferenceParent -> Ordering
$cp1Ord :: Eq InferenceParent
Ord)

data InferenceRule = ProofOf String
   | File { InferenceRule -> String
_fileName :: String, InferenceRule -> String
formulaName :: String }
   | Rule { InferenceRule -> String
rule :: String, InferenceRule -> String
parent :: String }
   | NoRule { parent :: String }
   | InferenceRule { rule :: String, InferenceRule -> String
status :: String,
                     InferenceRule -> Set InferenceParent
parents :: Set.Set InferenceParent,
                     InferenceRule -> Bool
_fact :: Bool }
     deriving (Int -> InferenceRule -> ShowS
[InferenceRule] -> ShowS
InferenceRule -> String
(Int -> InferenceRule -> ShowS)
-> (InferenceRule -> String)
-> ([InferenceRule] -> ShowS)
-> Show InferenceRule
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [InferenceRule] -> ShowS
$cshowList :: [InferenceRule] -> ShowS
show :: InferenceRule -> String
$cshow :: InferenceRule -> String
showsPrec :: Int -> InferenceRule -> ShowS
$cshowsPrec :: Int -> InferenceRule -> ShowS
Show, InferenceRule -> InferenceRule -> Bool
(InferenceRule -> InferenceRule -> Bool)
-> (InferenceRule -> InferenceRule -> Bool) -> Eq InferenceRule
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: InferenceRule -> InferenceRule -> Bool
$c/= :: InferenceRule -> InferenceRule -> Bool
== :: InferenceRule -> InferenceRule -> Bool
$c== :: InferenceRule -> InferenceRule -> Bool
Eq, Eq InferenceRule
Eq InferenceRule =>
(InferenceRule -> InferenceRule -> Ordering)
-> (InferenceRule -> InferenceRule -> Bool)
-> (InferenceRule -> InferenceRule -> Bool)
-> (InferenceRule -> InferenceRule -> Bool)
-> (InferenceRule -> InferenceRule -> Bool)
-> (InferenceRule -> InferenceRule -> InferenceRule)
-> (InferenceRule -> InferenceRule -> InferenceRule)
-> Ord InferenceRule
InferenceRule -> InferenceRule -> Bool
InferenceRule -> InferenceRule -> Ordering
InferenceRule -> InferenceRule -> InferenceRule
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 :: InferenceRule -> InferenceRule -> InferenceRule
$cmin :: InferenceRule -> InferenceRule -> InferenceRule
max :: InferenceRule -> InferenceRule -> InferenceRule
$cmax :: InferenceRule -> InferenceRule -> InferenceRule
>= :: InferenceRule -> InferenceRule -> Bool
$c>= :: InferenceRule -> InferenceRule -> Bool
> :: InferenceRule -> InferenceRule -> Bool
$c> :: InferenceRule -> InferenceRule -> Bool
<= :: InferenceRule -> InferenceRule -> Bool
$c<= :: InferenceRule -> InferenceRule -> Bool
< :: InferenceRule -> InferenceRule -> Bool
$c< :: InferenceRule -> InferenceRule -> Bool
compare :: InferenceRule -> InferenceRule -> Ordering
$ccompare :: InferenceRule -> InferenceRule -> Ordering
$cp1Ord :: Eq InferenceRule
Ord)

parentsOf :: InferenceRule -> Set.Set InferenceParent
parentsOf :: InferenceRule -> Set InferenceParent
parentsOf (ProofOf s :: String
s) = InferenceParent -> Set InferenceParent
forall a. a -> Set a
Set.singleton (InferenceParent -> Set InferenceParent)
-> InferenceParent -> Set InferenceParent
forall a b. (a -> b) -> a -> b
$ String -> InferenceParent
PTerm String
s
parentsOf (File _ _) = Set InferenceParent
forall a. Set a
Set.empty
parentsOf (Rule _ s :: String
s) = InferenceParent -> Set InferenceParent
forall a. a -> Set a
Set.singleton (InferenceParent -> Set InferenceParent)
-> InferenceParent -> Set InferenceParent
forall a b. (a -> b) -> a -> b
$ String -> InferenceParent
PTerm String
s
parentsOf (NoRule s :: String
s) = InferenceParent -> Set InferenceParent
forall a. a -> Set a
Set.singleton (InferenceParent -> Set InferenceParent)
-> InferenceParent -> Set InferenceParent
forall a b. (a -> b) -> a -> b
$ String -> InferenceParent
PTerm String
s
parentsOf (InferenceRule _ _ ps :: Set InferenceParent
ps _) = Set InferenceParent
ps

termParents :: Set.Set InferenceParent -> [String]
termParents :: Set InferenceParent -> [String]
termParents s :: Set InferenceParent
s = ([String] -> InferenceParent -> [String])
-> [String] -> [InferenceParent] -> [String]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ l :: [String]
l p :: InferenceParent
p -> case InferenceParent
p of
                                PTerm s' :: String
s' -> String
s' String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
l
                                PInferred ir :: InferenceRule
ir ->
                                 [String]
l [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ Set InferenceParent -> [String]
termParents (InferenceRule -> Set InferenceParent
parentsOf InferenceRule
ir)
                                _ -> [String]
l) [] ([InferenceParent] -> [String]) -> [InferenceParent] -> [String]
forall a b. (a -> b) -> a -> b
$ Set InferenceParent -> [InferenceParent]
forall a. Set a -> [a]
Set.toList Set InferenceParent
s

data ProofStep = ProofStep {
 ProofStep -> String
name :: String,
 ProofStep -> Role
role :: Role,
 ProofStep -> Maybe SPTerm
formula :: Maybe SPTerm,
 ProofStep -> InferenceRule
inference :: InferenceRule } | Empty deriving (Int -> ProofStep -> ShowS
[ProofStep] -> ShowS
ProofStep -> String
(Int -> ProofStep -> ShowS)
-> (ProofStep -> String)
-> ([ProofStep] -> ShowS)
-> Show ProofStep
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProofStep] -> ShowS
$cshowList :: [ProofStep] -> ShowS
show :: ProofStep -> String
$cshow :: ProofStep -> String
showsPrec :: Int -> ProofStep -> ShowS
$cshowsPrec :: Int -> ProofStep -> ShowS
Show, ProofStep -> ProofStep -> Bool
(ProofStep -> ProofStep -> Bool)
-> (ProofStep -> ProofStep -> Bool) -> Eq ProofStep
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ProofStep -> ProofStep -> Bool
$c/= :: ProofStep -> ProofStep -> Bool
== :: ProofStep -> ProofStep -> Bool
$c== :: ProofStep -> ProofStep -> Bool
Eq)

whiteSpace :: Parser ()
whiteSpace :: Parser ()
whiteSpace = ParsecT String () Identity Char -> Parser ()
forall (m :: * -> *) a. Monad m => m a -> m ()
forget (ParsecT String () Identity Char -> Parser ())
-> ParsecT String () Identity Char -> Parser ()
forall a b. (a -> b) -> a -> b
$ String -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
oneOf "\r\t\v\f "

lexeme :: GenParser Char () b -> GenParser Char () b
lexeme :: GenParser Char () b -> GenParser Char () b
lexeme p :: GenParser Char () b
p = Parser () -> Parser ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
skipMany Parser ()
whiteSpace Parser () -> GenParser Char () b -> GenParser Char () b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> GenParser Char () b
p

lString :: String -> GenParser Char () String
lString :: String -> GenParser Char () String
lString s :: String
s = GenParser Char () String -> GenParser Char () String
forall b. GenParser Char () b -> GenParser Char () b
lexeme (GenParser Char () String -> GenParser Char () String)
-> GenParser Char () String -> GenParser Char () String
forall a b. (a -> b) -> a -> b
$ String -> GenParser Char () String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
s

lChar :: Char -> GenParser Char () Char
lChar :: Char -> ParsecT String () Identity Char
lChar c :: Char
c = ParsecT String () Identity Char -> ParsecT String () Identity Char
forall b. GenParser Char () b -> GenParser Char () b
lexeme (ParsecT String () Identity Char
 -> ParsecT String () Identity Char)
-> ParsecT String () Identity Char
-> ParsecT String () Identity Char
forall a b. (a -> b) -> a -> b
$ Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
c

line :: Parser ProofStep
line :: Parser ProofStep
line = ((do
 String -> GenParser Char () String
lString "cnf" GenParser Char () String
-> GenParser Char () String -> GenParser Char () String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> GenParser Char () String
lString "fof"
 Char -> ParsecT String () Identity Char
lChar '('
 String
n <- GenParser Char () String
tok
 String
r <- GenParser Char () String
tok
 SPTerm
f <- GenParser Char () SPTerm -> GenParser Char () SPTerm
forall b. GenParser Char () b -> GenParser Char () b
lexeme GenParser Char () SPTerm
form
 Char -> ParsecT String () Identity Char
lChar ','
 InferenceRule
i <- GenParser Char () InferenceRule -> GenParser Char () InferenceRule
forall b. GenParser Char () b -> GenParser Char () b
lexeme (GenParser Char () InferenceRule
noRule GenParser Char () InferenceRule
-> GenParser Char () InferenceRule
-> GenParser Char () InferenceRule
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser Char () InferenceRule
fromFile GenParser Char () InferenceRule
-> GenParser Char () InferenceRule
-> GenParser Char () InferenceRule
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser Char () InferenceRule
inferenceRule GenParser Char () InferenceRule
-> GenParser Char () InferenceRule
-> GenParser Char () InferenceRule
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> GenParser Char () InferenceRule
proofOf)
 String -> GenParser Char () String
lString ")."
 ProofStep -> Parser ProofStep
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofStep -> Parser ProofStep) -> ProofStep -> Parser ProofStep
forall a b. (a -> b) -> a -> b
$ String -> Role -> Maybe SPTerm -> InferenceRule -> ProofStep
ProofStep String
n (if String
r String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "axiom" then Role
Axiom
                       else if String
r String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "conjecture" then Role
Conjecture
                       else Role
Other)
  (SPTerm -> Maybe SPTerm
forall a. a -> Maybe a
Just SPTerm
f) InferenceRule
i) Parser ProofStep -> Parser ProofStep -> Parser ProofStep
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser ProofStep
commentOrEmptyLine) Parser ProofStep -> Parser () -> Parser ProofStep
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof

commentOrEmptyLine :: Parser ProofStep
commentOrEmptyLine :: Parser ProofStep
commentOrEmptyLine = ((ParsecT String () Identity Char -> Parser ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
skipMany (Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '#') Parser () -> GenParser Char () String -> GenParser Char () String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
 ParsecT String () Identity Char
-> Parser () -> GenParser Char () String
forall s (m :: * -> *) t u a end.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m end -> ParsecT s u m [a]
manyTill ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
anyChar (Parser () -> Parser ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m a
lookAhead Parser ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof))
 GenParser Char () String
-> GenParser Char () String -> GenParser Char () String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Parser () -> Parser ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
skipMany Parser ()
whiteSpace Parser () -> GenParser Char () String -> GenParser Char () String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> GenParser Char () String
forall (m :: * -> *) a. Monad m => a -> m a
return "")) GenParser Char () String -> Parser ProofStep -> Parser ProofStep
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ProofStep -> Parser ProofStep
forall (m :: * -> *) a. Monad m => a -> m a
return ProofStep
Empty

tok :: Parser String
tok :: GenParser Char () String
tok = GenParser Char () String -> GenParser Char () String
forall b. GenParser Char () b -> GenParser Char () b
lexeme (GenParser Char () String -> GenParser Char () String)
-> GenParser Char () String -> GenParser Char () String
forall a b. (a -> b) -> a -> b
$ ParsecT String () Identity Char -> GenParser Char () String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (String -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
noneOf ",") GenParser Char () String
-> ParsecT String () Identity Char -> GenParser Char () String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char ','

fromFile :: Parser InferenceRule
fromFile :: GenParser Char () InferenceRule
fromFile = do
   String -> GenParser Char () String
lString "file" GenParser Char () String
-> ParsecT String () Identity Char
-> ParsecT String () Identity Char
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> ParsecT String () Identity Char
lChar '('
   String
f <- GenParser Char () String -> GenParser Char () String
forall b. GenParser Char () b -> GenParser Char () b
lexeme GenParser Char () String
singleQuoted
   Char -> ParsecT String () Identity Char
lChar ',' ParsecT String () Identity Char -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser () -> Parser ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
skipMany Parser ()
whiteSpace
   String
n <- ParsecT String () Identity Char
-> ParsecT String () Identity Char -> GenParser Char () String
forall s (m :: * -> *) t u a end.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m end -> ParsecT s u m [a]
manyTill ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
anyChar (Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char ')')
   InferenceRule -> GenParser Char () InferenceRule
forall (m :: * -> *) a. Monad m => a -> m a
return (InferenceRule -> GenParser Char () InferenceRule)
-> InferenceRule -> GenParser Char () InferenceRule
forall a b. (a -> b) -> a -> b
$ String -> String -> InferenceRule
File String
f String
n

proofOf :: Parser InferenceRule
proofOf :: GenParser Char () InferenceRule
proofOf = do
   String
n <- GenParser Char () String
tok
   String -> GenParser Char () String
lString "['"
   String
r <- ParsecT String () Identity Char
-> ParsecT String () Identity Char -> GenParser Char () String
forall s (m :: * -> *) t u a end.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m end -> ParsecT s u m [a]
manyTill ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
anyChar (ParsecT String () Identity Char -> ParsecT String () Identity Char
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m a
lookAhead (ParsecT String () Identity Char
 -> ParsecT String () Identity Char)
-> ParsecT String () Identity Char
-> ParsecT String () Identity Char
forall a b. (a -> b) -> a -> b
$ String -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
oneOf "'")
   String -> GenParser Char () String
lString "']"
   InferenceRule -> GenParser Char () InferenceRule
forall (m :: * -> *) a. Monad m => a -> m a
return (InferenceRule -> GenParser Char () InferenceRule)
-> InferenceRule -> GenParser Char () InferenceRule
forall a b. (a -> b) -> a -> b
$ case String
r of
             "proof" -> String -> InferenceRule
ProofOf String
n
             _ -> String -> String -> InferenceRule
Rule String
r String
n

noRule :: Parser InferenceRule
noRule :: GenParser Char () InferenceRule
noRule = GenParser Char () InferenceRule -> GenParser Char () InferenceRule
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char () InferenceRule
 -> GenParser Char () InferenceRule)
-> GenParser Char () InferenceRule
-> GenParser Char () InferenceRule
forall a b. (a -> b) -> a -> b
$ do
 String
t <- GenParser Char () String -> GenParser Char () String
forall b. GenParser Char () b -> GenParser Char () b
lexeme (GenParser Char () String -> GenParser Char () String)
-> GenParser Char () String -> GenParser Char () String
forall a b. (a -> b) -> a -> b
$ ParsecT String () Identity Char -> GenParser Char () String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (String -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
noneOf ",)")
 GenParser Char () String -> GenParser Char () String
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m a
lookAhead (GenParser Char () String -> GenParser Char () String)
-> GenParser Char () String -> GenParser Char () String
forall a b. (a -> b) -> a -> b
$ String -> GenParser Char () String
lString ")."
 InferenceRule -> GenParser Char () InferenceRule
forall (m :: * -> *) a. Monad m => a -> m a
return (InferenceRule -> GenParser Char () InferenceRule)
-> InferenceRule -> GenParser Char () InferenceRule
forall a b. (a -> b) -> a -> b
$ String -> InferenceRule
NoRule String
t

inferenceRule :: Parser InferenceRule
inferenceRule :: GenParser Char () InferenceRule
inferenceRule = do
   String -> GenParser Char () String
lString "inference" GenParser Char () String
-> ParsecT String () Identity Char
-> ParsecT String () Identity Char
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> ParsecT String () Identity Char
lChar '('
   String
r <- GenParser Char () String
tok
   Char -> ParsecT String () Identity Char
lChar '[' ParsecT String () Identity Char
-> GenParser Char () String -> GenParser Char () String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> GenParser Char () String
lString "status" GenParser Char () String
-> ParsecT String () Identity Char
-> ParsecT String () Identity Char
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> ParsecT String () Identity Char
lChar '('
   String
s <- ParsecT String () Identity Char
-> ParsecT String () Identity Char -> GenParser Char () String
forall s (m :: * -> *) t u a end.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m end -> ParsecT s u m [a]
manyTill ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
anyChar (Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char ')')
   Char -> ParsecT String () Identity Char
lChar ']' ParsecT String () Identity Char
-> ParsecT String () Identity Char
-> ParsecT String () Identity Char
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> ParsecT String () Identity Char
lChar ',' ParsecT String () Identity Char
-> ParsecT String () Identity Char
-> ParsecT String () Identity Char
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> ParsecT String () Identity Char
lChar '['
   [InferenceParent]
ps <- ParsecT String () Identity InferenceParent
-> ParsecT String () Identity Char
-> ParsecT String () Identity [InferenceParent]
forall s (m :: * -> *) t u a end.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m end -> ParsecT s u m [a]
sepBy ParsecT String () Identity InferenceParent
inferenceParent (Char -> ParsecT String () Identity Char
lChar ',')
   Char -> ParsecT String () Identity Char
lChar ']' ParsecT String () Identity Char
-> ParsecT String () Identity Char
-> ParsecT String () Identity Char
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> ParsecT String () Identity Char
lChar ')'
   Bool
b <- GenParser Char () Bool -> GenParser Char () Bool
forall tok st a. GenParser tok st a -> GenParser tok st a
try (Char -> ParsecT String () Identity Char
lChar ',' ParsecT String () Identity Char
-> GenParser Char () String -> GenParser Char () String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> GenParser Char () String
lString "['proof']" GenParser Char () String
-> GenParser Char () Bool -> GenParser Char () Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> GenParser Char () Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
        GenParser Char () Bool
-> GenParser Char () Bool -> GenParser Char () Bool
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Bool -> GenParser Char () Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
   InferenceRule -> GenParser Char () InferenceRule
forall (m :: * -> *) a. Monad m => a -> m a
return (InferenceRule -> GenParser Char () InferenceRule)
-> InferenceRule -> GenParser Char () InferenceRule
forall a b. (a -> b) -> a -> b
$ String -> String -> Set InferenceParent -> Bool -> InferenceRule
InferenceRule String
r String
s ([InferenceParent] -> Set InferenceParent
forall a. Ord a => [a] -> Set a
Set.fromList [InferenceParent]
ps) Bool
b

inferenceParent :: Parser InferenceParent
inferenceParent :: ParsecT String () Identity InferenceParent
inferenceParent = ParsecT String () Identity InferenceParent
-> ParsecT String () Identity InferenceParent
forall b. GenParser Char () b -> GenParser Char () b
lexeme (ParsecT String () Identity InferenceParent
 -> ParsecT String () Identity InferenceParent)
-> ParsecT String () Identity InferenceParent
-> ParsecT String () Identity InferenceParent
forall a b. (a -> b) -> a -> b
$
   (InferenceRule -> InferenceParent)
-> GenParser Char () InferenceRule
-> ParsecT String () Identity InferenceParent
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM InferenceRule -> InferenceParent
PInferred GenParser Char () InferenceRule
inferenceRule ParsecT String () Identity InferenceParent
-> ParsecT String () Identity InferenceParent
-> ParsecT String () Identity InferenceParent
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
   do
    GenTerm
t' <- Parser GenTerm
genTerm
    let t :: String
t = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ GenTerm -> Doc
ppGenTerm GenTerm
t'
    InferenceParent -> ParsecT String () Identity InferenceParent
forall (m :: * -> *) a. Monad m => a -> m a
return (InferenceParent -> ParsecT String () Identity InferenceParent)
-> InferenceParent -> ParsecT String () Identity InferenceParent
forall a b. (a -> b) -> a -> b
$ case String
t of
     't' : 'h' : 'e' : 'o' : 'r' : 'y' : '(' : _ -> String -> InferenceParent
PBuiltinTheory String
t
     _ -> String -> InferenceParent
PTerm String
t

supportsProofObject :: IO Bool
supportsProofObject :: IO Bool
supportsProofObject = do
 (ex :: ExitCode
ex, _, _) <- String -> [String] -> String -> IO (ExitCode, String, String)
executeProcess "eprover" ["--proof-object", "-V"] ""
 case ExitCode
ex of
  ExitSuccess -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  ExitFailure _ -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

processProof :: (a -> ProofStep -> a) -> a -> [String] -> (a, Maybe String)
processProof :: (a -> ProofStep -> a) -> a -> [String] -> (a, Maybe String)
processProof fn :: a -> ProofStep -> a
fn a :: a
a = ((a, Maybe String) -> String -> (a, Maybe String))
-> (a, Maybe String) -> [String] -> (a, Maybe String)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\ (a' :: a
a', result :: Maybe String
result) l :: String
l -> case Maybe String
result of
 Just _ -> (a
a', Maybe String
result)
 Nothing -> case Parser ProofStep
-> () -> String -> String -> Either ParseError ProofStep
forall tok st a.
GenParser tok st a -> st -> String -> [tok] -> Either ParseError a
runParser Parser ProofStep
line () "" String
l of
  Right p :: ProofStep
p | ProofStep
p ProofStep -> ProofStep -> Bool
forall a. Eq a => a -> a -> Bool
/= ProofStep
Empty -> (a -> ProofStep -> a
fn a
a' ProofStep
p, Maybe String
result)
  Left e :: ParseError
e -> (a
a', String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String)
-> ([String] -> String) -> [String] -> Maybe String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines ([String] -> Maybe String) -> [String] -> Maybe String
forall a b. (a -> b) -> a -> b
$ "Warning - Failed to parse eprover proof"
               String -> [String] -> [String]
forall a. a -> [a] -> [a]
: ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((:) '\t') (("Input: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
l) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String -> [String]
lines (ParseError -> String
forall a. Show a => a -> String
show ParseError
e)))
  _ -> (a
a', Maybe String
result)
 ) (a
a, Maybe String
forall a. Maybe a
Nothing)

zipF :: (a -> b -> a) -> (c -> b -> c) -> (a, c) -> b -> (a, c)
zipF :: (a -> b -> a) -> (c -> b -> c) -> (a, c) -> b -> (a, c)
zipF f1 :: a -> b -> a
f1 f2 :: c -> b -> c
f2 (a :: a
a, c :: c
c) b :: b
b = (a -> b -> a
f1 a
a b
b, c -> b -> c
f2 c
c b
b)

axioms :: [(String, String)] -> ProofStep -> [(String, String)]
axioms :: [(String, String)] -> ProofStep -> [(String, String)]
axioms l :: [(String, String)]
l p :: ProofStep
p = case ProofStep -> InferenceRule
inference ProofStep
p of
              File _ _ | ProofStep -> Role
role ProofStep
p Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Axiom ->
               (InferenceRule -> String
formulaName (InferenceRule -> String)
-> (ProofStep -> InferenceRule) -> ProofStep -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofStep -> InferenceRule
inference (ProofStep -> String) -> ProofStep -> String
forall a b. (a -> b) -> a -> b
$ ProofStep
p, ProofStep -> String
name ProofStep
p) (String, String) -> [(String, String)] -> [(String, String)]
forall a. a -> [a] -> [a]
: [(String, String)]
l
              _ -> [(String, String)]
l

conjectures :: [(String, String)] -> ProofStep -> [(String, String)]
conjectures :: [(String, String)] -> ProofStep -> [(String, String)]
conjectures l :: [(String, String)]
l p :: ProofStep
p = if ProofStep -> Role
role ProofStep
p Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Conjecture
                  then (InferenceRule -> String
formulaName (InferenceRule -> String)
-> (ProofStep -> InferenceRule) -> ProofStep -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofStep -> InferenceRule
inference (ProofStep -> String) -> ProofStep -> String
forall a b. (a -> b) -> a -> b
$ ProofStep
p, ProofStep -> String
name ProofStep
p) (String, String) -> [(String, String)] -> [(String, String)]
forall a. a -> [a] -> [a]
: [(String, String)]
l else [(String, String)]
l

alias :: Map.Map String String -> ProofStep -> Map.Map String String
alias :: Map String String -> ProofStep -> Map String String
alias m :: Map String String
m p :: ProofStep
p = case ProofStep -> InferenceRule
inference ProofStep
p of
             NoRule s :: String
s -> case String -> Map String String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
s Map String String
m of
                          Just s' :: String
s' -> String -> String -> Map String String -> Map String String
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (ProofStep -> String
name ProofStep
p) String
s' Map String String
m
                          Nothing -> String -> String -> Map String String -> Map String String
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (ProofStep -> String
name ProofStep
p) String
s Map String String
m
             _ -> Map String String
m

proofInfo :: Set.Set String -> ProofStep -> Set.Set String
proofInfo :: Set String -> ProofStep -> Set String
proofInfo p_set :: Set String
p_set p :: ProofStep
p =
 if Set String -> Bool
forall a. Set a -> Bool
Set.null Set String
p_set Bool -> Bool -> Bool
|| String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (ProofStep -> String
name ProofStep
p) Set String
p_set
 then Set String -> Set String -> Set String
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set String
p_set (Set String -> Set String) -> Set String -> Set String
forall a b. (a -> b) -> a -> b
$ [String] -> Set String
forall a. Ord a => [a] -> Set a
Set.fromList ([String] -> Set String) -> [String] -> Set String
forall a b. (a -> b) -> a -> b
$
       ProofStep -> String
name ProofStep
p String -> [String] -> [String]
forall a. a -> [a] -> [a]
: Set InferenceParent -> [String]
termParents (InferenceRule -> Set InferenceParent
parentsOf (InferenceRule -> Set InferenceParent)
-> InferenceRule -> Set InferenceParent
forall a b. (a -> b) -> a -> b
$ ProofStep -> InferenceRule
inference ProofStep
p)
 else Set String
p_set

showTerm :: ProofStep -> String
showTerm :: ProofStep -> String
showTerm = GlobalAnnos -> Doc -> String
renderText GlobalAnnos
emptyGlobalAnnos (Doc -> String) -> (ProofStep -> Doc) -> ProofStep -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPTerm -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP (SPTerm -> Doc) -> (ProofStep -> SPTerm) -> ProofStep -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe SPTerm -> SPTerm
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe SPTerm -> SPTerm)
-> (ProofStep -> Maybe SPTerm) -> ProofStep -> SPTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofStep -> Maybe SPTerm
formula

facts :: Set.Set String -> ProofStep -> Set.Set String
facts :: Set String -> ProofStep -> Set String
facts s :: Set String
s p :: ProofStep
p =
 let isFact :: InferenceParent -> Bool
isFact n :: InferenceParent
n = case InferenceParent
n of
                 PTerm n' :: String
n' -> String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member String
n' Set String
s
                 PInferred ir :: InferenceRule
ir -> (String -> Bool) -> [String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set String
s) ([String] -> Bool) -> [String] -> Bool
forall a b. (a -> b) -> a -> b
$
                                  Set InferenceParent -> [String]
termParents (Set InferenceParent -> [String])
-> Set InferenceParent -> [String]
forall a b. (a -> b) -> a -> b
$ InferenceRule -> Set InferenceParent
parentsOf InferenceRule
ir
                 PBuiltinTheory _ -> Bool
True
 in if (ProofStep -> Role
role ProofStep
p Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
/= Role
Conjecture) Bool -> Bool -> Bool
&&
       (InferenceParent -> Bool) -> [InferenceParent] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all InferenceParent -> Bool
isFact (Set InferenceParent -> [InferenceParent]
forall a. Set a -> [a]
Set.toList (Set InferenceParent -> [InferenceParent])
-> Set InferenceParent -> [InferenceParent]
forall a b. (a -> b) -> a -> b
$ InferenceRule -> Set InferenceParent
parentsOf (InferenceRule -> Set InferenceParent)
-> InferenceRule -> Set InferenceParent
forall a b. (a -> b) -> a -> b
$ ProofStep -> InferenceRule
inference ProofStep
p)
    then String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert (ProofStep -> String
name ProofStep
p) Set String
s else Set String
s

attributes :: [(String, String)] -> String
attributes :: [(String, String)] -> String
attributes attrs :: [(String, String)]
attrs = case [(String, String)]
attrs of
 [] -> ""
 _ -> "[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ","
  (((String, String) -> String) -> [(String, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (n :: String
n, v :: String
v) -> String
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ "=\"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\"") [(String, String)]
attrs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "]"

vertex :: String -> [(String, String)] -> String
vertex :: String -> [(String, String)] -> String
vertex s :: String
s attrs :: [(String, String)]
attrs = String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(String, String)] -> String
attributes [(String, String)]
attrs

edge :: Bool -> String -> String -> [(String, String)] -> String
edge :: Bool -> String -> String -> [(String, String)] -> String
edge inv :: Bool
inv v1 :: String
v1 v2 :: String
v2 attrs' :: [(String, String)]
attrs' =
 let attrs :: [(String, String)]
attrs = ("splines", "curved") (String, String) -> [(String, String)] -> [(String, String)]
forall a. a -> [a] -> [a]
: [(String, String)]
attrs'
 in if Bool
inv then String
v2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
v1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(String, String)] -> String
attributes [(String, String)]
attrs
    else String
v1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
v2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(String, String)] -> String
attributes [(String, String)]
attrs

digraph :: Set.Set String -> Map.Map String String ->
           (Set.Set String, Set.Set String, String,
            Map.Map (String, [String]) String) -> ProofStep ->
           (Set.Set String, Set.Set String,
            String, Map.Map (String, [String]) String)
digraph :: Set String
-> Map String String
-> (Set String, Set String, String, Map (String, [String]) String)
-> ProofStep
-> (Set String, Set String, String, Map (String, [String]) String)
digraph p_set :: Set String
p_set aliases :: Map String String
aliases (s :: Set String
s, neg :: Set String
neg, d :: String
d, m :: Map (String, [String]) String
m) p :: ProofStep
p =
 let s' :: Set String
s' = Set String -> ProofStep -> Set String
facts Set String
s ProofStep
p
     neg_ :: Set String
neg_ = String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert (ProofStep -> String
name ProofStep
p) Set String
neg
     negated :: Bool
negated = (String -> Bool) -> [String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set String
neg)
                   (Set InferenceParent -> [String]
termParents (Set InferenceParent -> [String])
-> Set InferenceParent -> [String]
forall a b. (a -> b) -> a -> b
$ InferenceRule -> Set InferenceParent
parentsOf (InferenceRule -> Set InferenceParent)
-> InferenceRule -> Set InferenceParent
forall a b. (a -> b) -> a -> b
$ ProofStep -> InferenceRule
inference ProofStep
p)
     alias' :: ShowS
alias' n :: String
n = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
n (String -> Map String String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
n Map String String
aliases)
     neg' :: Set String
neg' = case ProofStep -> InferenceRule
inference ProofStep
p of
             (InferenceRule _ st :: String
st _ _)
              | String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem ((Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
st) ["cth", "unc", "uns"]
                          -> if Bool
negated then Set String
neg else Set String
neg_
              | Bool
negated -> Set String
neg_
              | Bool
otherwise -> Set String
neg
             _ -> if Bool
negated then Set String
neg_ else Set String
neg
     isFact' :: Bool
isFact' = case ProofStep -> InferenceRule
inference ProofStep
p of
                InferenceRule _ _ _ b :: Bool
b -> Bool
b
                _ -> Bool
False
     color' :: [(String, String)]
color' = ("fillcolor", if ProofStep -> Role
role ProofStep
p Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Axiom Bool -> Bool -> Bool
|| String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (ProofStep -> String
name ProofStep
p) Set String
s'
                           then "green" else "yellow") (String, String) -> [(String, String)] -> [(String, String)]
forall a. a -> [a] -> [a]
:
              ("style", "filled") (String, String) -> [(String, String)] -> [(String, String)]
forall a. a -> [a] -> [a]
: (if String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (ProofStep -> String
name ProofStep
p) Set String
neg'
               then [("color", "red")] else [("color", "green")])
     color :: [(String, String)]
color = case ProofStep -> InferenceRule
inference ProofStep
p of
               ProofOf _ | ProofStep -> Role
role ProofStep
p Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Other ->
                if Bool
negated then [("style", "filled"), ("fillcolor", "red"),
                                 ("color", "red")]
                else [("style", "filled"), ("fillcolor", "green"),
                      ("color", "green")]
               _ -> [(String, String)]
color'
     (s'' :: Set String
s'', neg'' :: Set String
neg'', m' :: Map (String, [String]) String
m', d' :: [String]
d') = (case ProofStep -> Role
role ProofStep
p of
           Axiom -> case ProofStep -> InferenceRule
inference ProofStep
p of
            File f :: String
f n :: String
n -> (Set String
s', Set String
neg', Map (String, [String]) String
m, [String -> [(String, String)] -> String
vertex ('v' Char -> ShowS
forall a. a -> [a] -> [a]
: ProofStep -> String
name ProofStep
p) ([(String, String)] -> String) -> [(String, String)] -> String
forall a b. (a -> b) -> a -> b
$ [(String, String)]
color [(String, String)] -> [(String, String)] -> [(String, String)]
forall a. [a] -> [a] -> [a]
++
             [("label", "Axiom " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ " (File: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")\\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
                        ProofStep -> String
showTerm ProofStep
p)]])
            _ -> (Set String
s', Set String
neg', Map (String, [String]) String
m, [])
           Conjecture -> case ProofStep -> InferenceRule
inference ProofStep
p of
            File f :: String
f n :: String
n -> (Set String
s', Set String
neg', Map (String, [String]) String
m, [String -> [(String, String)] -> String
vertex ('v' Char -> ShowS
forall a. a -> [a] -> [a]
: ProofStep -> String
name ProofStep
p) ([(String, String)] -> String) -> [(String, String)] -> String
forall a b. (a -> b) -> a -> b
$ [(String, String)]
color [(String, String)] -> [(String, String)] -> [(String, String)]
forall a. [a] -> [a] -> [a]
++
             [("label", "Conjecture " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ " (File: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")\\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
                        ProofStep -> String
showTerm ProofStep
p)]])
            _ -> (Set String
s', Set String
neg', Map (String, [String]) String
m, [])
           Other ->
            let (s'_ :: Set String
s'_, neg'_ :: Set String
neg'_, m'' :: Map (String, [String]) String
m'', d'' :: [String]
d'') = case ProofStep -> InferenceRule
inference ProofStep
p of
                 ProofOf tm :: String
tm ->
                  (Set String
s', Set String
neg', Map (String, [String]) String
m, [Bool -> String -> String -> [(String, String)] -> String
edge Bool
True ('v' Char -> ShowS
forall a. a -> [a] -> [a]
: ShowS
alias' String
tm)
                                           ('v' Char -> ShowS
forall a. a -> [a] -> [a]
: ShowS
alias' (ProofStep -> String
name ProofStep
p))
                      [("label", (if Bool
negated then "dis" else "")
                                 String -> ShowS
forall a. [a] -> [a] -> [a]
++ "proves")]])
                 r :: InferenceRule
r@(Rule _ _) -> (Set String
s', Set String
neg', Map (String, [String]) String
m,
                                   [Bool -> String -> String -> [(String, String)] -> String
edge Bool
False ('v' Char -> ShowS
forall a. a -> [a] -> [a]
: ShowS
alias' (InferenceRule -> String
parent InferenceRule
r))
                                               ('v' Char -> ShowS
forall a. a -> [a] -> [a]
: ShowS
alias' (ProofStep -> String
name ProofStep
p))
                                     [("label", InferenceRule -> String
rule InferenceRule
r)]])
                 r :: InferenceRule
r@(NoRule _) -> (Set String
s', Set String
neg', Map (String, [String]) String
m,
                                 [Bool -> String -> String -> [(String, String)] -> String
edge Bool
False ('v' Char -> ShowS
forall a. a -> [a] -> [a]
: ShowS
alias' (InferenceRule -> String
parent InferenceRule
r))
                                             ('v' Char -> ShowS
forall a. a -> [a] -> [a]
: ShowS
alias' (ProofStep -> String
name ProofStep
p)) []])
                 inf :: InferenceRule
inf@(InferenceRule {}) ->
                  let (r :: String
r, l1 :: [String]
l1, m1 :: Map (String, [String]) String
m1, new :: Bool
new) =
                       case (String, [String]) -> Map (String, [String]) String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup
                        (InferenceRule -> String
rule InferenceRule
inf, Set InferenceParent -> [String]
termParents (Set InferenceParent -> [String])
-> Set InferenceParent -> [String]
forall a b. (a -> b) -> a -> b
$ InferenceRule -> Set InferenceParent
parents InferenceRule
inf) Map (String, [String]) String
m of
                                Just r' :: String
r' -> (String
r',
                                 [Bool -> String -> String -> [(String, String)] -> String
edge Bool
False String
r' ('v' Char -> ShowS
forall a. a -> [a] -> [a]
: ShowS
alias' (ProofStep -> String
name ProofStep
p)) []],
                                 Map (String, [String]) String
m, Bool
False)
                                _ ->
                                 let r1 :: String
r1 = 'r' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show (Map (String, [String]) String -> Int
forall k a. Map k a -> Int
Map.size Map (String, [String]) String
m)
                                 in (String
r1, [String -> [(String, String)] -> String
vertex String
r1
                                     [("label", "Apply rule " String -> ShowS
forall a. [a] -> [a] -> [a]
++ InferenceRule -> String
rule InferenceRule
inf),
                                      ("style", "dotted")],
                                     if Bool -> Bool
not Bool
isFact' then Bool -> String -> String -> [(String, String)] -> String
edge Bool
False String
r1
                                      ((if String -> Char
forall a. [a] -> a
head (ProofStep -> String
name ProofStep
p) Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== 'r' then ""
                                        else "v") String -> ShowS
forall a. [a] -> [a] -> [a]
++
                                      ShowS
alias' (ProofStep -> String
name ProofStep
p)) [] else ""],
                                      (String, [String])
-> String
-> Map (String, [String]) String
-> Map (String, [String]) String
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (InferenceRule -> String
rule InferenceRule
inf, Set InferenceParent -> [String]
termParents (Set InferenceParent -> [String])
-> Set InferenceParent -> [String]
forall a b. (a -> b) -> a -> b
$
                                       InferenceRule -> Set InferenceParent
parents InferenceRule
inf) String
r1 Map (String, [String]) String
m, Bool
True)
                      (s2' :: Set String
s2', neg2' :: Set String
neg2', l3 :: [String]
l3, m3 :: Map (String, [String]) String
m3) =
                       ((Set String, Set String, [String], Map (String, [String]) String)
 -> InferenceParent
 -> (Set String, Set String, [String],
     Map (String, [String]) String))
-> (Set String, Set String, [String],
    Map (String, [String]) String)
-> [InferenceParent]
-> (Set String, Set String, [String],
    Map (String, [String]) String)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ (s1' :: Set String
s1', neg1' :: Set String
neg1', l2 :: [String]
l2, m2 :: Map (String, [String]) String
m2) s1 :: InferenceParent
s1 -> case InferenceParent
s1 of
                                 PTerm s2 :: String
s2 -> if Bool
new then
                                  (Set String
s1', Set String
neg1', [String]
l2 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [Bool -> String -> String -> [(String, String)] -> String
edge Bool
False
                                                      ('v' Char -> ShowS
forall a. a -> [a] -> [a]
: ShowS
alias' String
s2) String
r [],
                                        Bool -> String -> String -> [(String, String)] -> String
edge (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member String
s2 Set String
s')
                                             ('v' Char -> ShowS
forall a. a -> [a] -> [a]
: ShowS
alias' String
s2) String
r
                                         [("label", "SZS " String -> ShowS
forall a. [a] -> [a] -> [a]
++ InferenceRule -> String
status InferenceRule
inf),
                                          ("color", "blue"),
                                          ("fontcolor", "blue")] ], Map (String, [String]) String
m2)
                                  else (Set String
s1', Set String
neg1', [String]
l2, Map (String, [String]) String
m2)
                                 PInferred ir :: InferenceRule
ir ->
                                  let (s1'' :: Set String
s1'', neg1'' :: Set String
neg1'', l2' :: String
l2', m2' :: Map (String, [String]) String
m2') = Set String
-> Map String String
-> (Set String, Set String, String, Map (String, [String]) String)
-> ProofStep
-> (Set String, Set String, String, Map (String, [String]) String)
digraph Set String
p_set
                                       Map String String
aliases (Set String
s1', Set String
neg1', [String] -> String
unlines [String]
l2, Map (String, [String]) String
m2) (ProofStep
 -> (Set String, Set String, String, Map (String, [String]) String))
-> ProofStep
-> (Set String, Set String, String, Map (String, [String]) String)
forall a b. (a -> b) -> a -> b
$
                                        String -> Role -> Maybe SPTerm -> InferenceRule -> ProofStep
ProofStep String
r Role
Other Maybe SPTerm
forall a. Maybe a
Nothing InferenceRule
ir
                                  in (Set String
s1'', Set String
neg1'', [String
l2'], Map (String, [String]) String
m2')
                                 PBuiltinTheory s2 :: String
s2 ->
                                  case (String, [String]) -> Map (String, [String]) String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (String
s2, []) Map (String, [String]) String
m2 of
                                   Just s2'' :: String
s2'' -> (Set String
s1', Set String
neg1', [String]
l2 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                                                 [Bool -> String -> String -> [(String, String)] -> String
edge Bool
False String
s2'' String
r []], Map (String, [String]) String
m2)
                                   Nothing ->
                                    let s2'' :: String
s2'' = 't' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show (Map (String, [String]) String -> Int
forall k a. Map k a -> Int
Map.size Map (String, [String]) String
m2)
                                    in (Set String
s1', Set String
neg1', [String]
l2 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String -> [(String, String)] -> String
vertex String
s2''
                                            [("style", "filled"),
                                             ("fillcolor", "green"),
                                             ("color", "green"), ("label", String
s2)],
                                             Bool -> String -> String -> [(String, String)] -> String
edge Bool
False String
s2'' String
r []],
                                       (String, [String])
-> String
-> Map (String, [String]) String
-> Map (String, [String]) String
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (String
s2, []) String
s2'' Map (String, [String]) String
m2))
                                (Set String
s', Set String
neg', [String]
l1, Map (String, [String]) String
m1) (Set InferenceParent -> [InferenceParent]
forall a. Set a -> [a]
Set.toList (Set InferenceParent -> [InferenceParent])
-> Set InferenceParent -> [InferenceParent]
forall a b. (a -> b) -> a -> b
$ InferenceRule -> Set InferenceParent
parentsOf InferenceRule
inf)
                  in (Set String
s2', Set String
neg2', Map (String, [String]) String
m3, [String]
l3)
                 _ -> (Set String
s', Set String
neg', Map (String, [String]) String
m, [])
            in (Set String
s'_, Set String
neg'_, Map (String, [String]) String
m'', case ProofStep -> Maybe SPTerm
formula ProofStep
p of
                               Just _ | Bool -> Bool
not Bool
isFact' -> String -> [(String, String)] -> String
vertex ('v' Char -> ShowS
forall a. a -> [a] -> [a]
: ProofStep -> String
name ProofStep
p)
                                ([(String, String)]
color [(String, String)] -> [(String, String)] -> [(String, String)]
forall a. [a] -> [a] -> [a]
++ [("label", ProofStep -> String
showTerm ProofStep
p)]) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
d''
                               _ -> [String]
d''))
 in if (String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (ProofStep -> String
name ProofStep
p) Set String
p_set Bool -> Bool -> Bool
|| Maybe SPTerm -> Bool
forall a. Maybe a -> Bool
isNothing (ProofStep -> Maybe SPTerm
formula ProofStep
p)) Bool -> Bool -> Bool
&&
       String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem (ProofStep -> String
name ProofStep
p) (Map String String -> [String]
forall k a. Map k a -> [k]
Map.keys Map String String
aliases)
    then (Set String
s'', Set String
neg'', [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
d String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
d', Map (String, [String]) String
m')
    else (Set String
s', Set String
neg', String
d, Map (String, [String]) String
m)