module TPTP.Prover.ProofParser ( axiomsFromProofObject
, graphFromProofObject
, filterProofLines
, findSZS
) where
import TPTP.AS ( Annotated_formula (..)
, Formula_role (..)
, Annotations (..)
, Source (..)
, DAG_source (..)
, External_source (..)
, File_source (..)
, Inference_record (..)
, Parent_info (..)
, Name (..)
, formulaRole
, annotations
, name )
import TPTP.Parser (annotated_formula)
import TPTP.Pretty ()
import Common.DocUtils
import Common.ProofTree
import Common.Id (Token (..))
import Data.Data (toConstr)
import Data.List
import Data.List.Split (splitOn)
import Data.Maybe
import Data.Graph.Inductive.Graph
import qualified Data.HashMap.Strict as Map
import Text.ParserCombinators.Parsec
axiomsFromProofObject :: [String] -> ([String], [String])
axiomsFromProofObject :: [String] -> ([String], [String])
axiomsFromProofObject =
(Either String Annotated_formula
-> ([String], [String]) -> ([String], [String]))
-> ([String], [String])
-> [Either String Annotated_formula]
-> ([String], [String])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Either String Annotated_formula
-> ([String], [String]) -> ([String], [String])
addIfAxiom ([], []) ([Either String Annotated_formula] -> ([String], [String]))
-> ([String] -> [Either String Annotated_formula])
-> [String]
-> ([String], [String])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Either String Annotated_formula)
-> [String] -> [Either String Annotated_formula]
forall a b. (a -> b) -> [a] -> [b]
map String -> Either String Annotated_formula
parseFormulae ([String] -> [Either String Annotated_formula])
-> ([String] -> [String])
-> [String]
-> [Either String Annotated_formula]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
splitFormulae (String -> [String])
-> ([String] -> String) -> [String] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines
where
addIfAxiom :: Either String Annotated_formula
-> ([String], [String]) -> ([String], [String])
addIfAxiom :: Either String Annotated_formula
-> ([String], [String]) -> ([String], [String])
addIfAxiom formulaOrError :: Either String Annotated_formula
formulaOrError (axiomNames :: [String]
axiomNames, parserErrors :: [String]
parserErrors) =
case Either String Annotated_formula
formulaOrError of
Left err :: String
err -> ([String]
axiomNames, String
err String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
parserErrors)
Right formula :: Annotated_formula
formula -> (Annotated_formula -> [String]
getAxiomName Annotated_formula
formula [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
axiomNames, [String]
parserErrors)
getAxiomName :: Annotated_formula -> [String]
getAxiomName :: Annotated_formula -> [String]
getAxiomName formula :: Annotated_formula
formula
| Formula_role
Axiom <- Annotated_formula -> Formula_role
formulaRole Annotated_formula
formula
, Annotations (Just (Source_external (ExtSrc_file (File_source _ (Just fileInfo :: Name
fileInfo))),_)) <- Annotated_formula -> Annotations
annotations Annotated_formula
formula
= [Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
fileInfo]
| Formula_role
Axiom <- Annotated_formula -> Formula_role
formulaRole Annotated_formula
formula
= [Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Name -> Doc
forall a. Pretty a => a -> Doc
pretty (Name -> Doc) -> Name -> Doc
forall a b. (a -> b) -> a -> b
$ Annotated_formula -> Name
name Annotated_formula
formula]
| Bool
otherwise
= []
splitFormulae :: String -> [String]
splitFormulae :: String -> [String]
splitFormulae = [String] -> [String]
forall a. [a] -> [a]
init ([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ s :: String
s -> String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ ").\n") ([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> [String]
forall a. Eq a => [a] -> [a] -> [[a]]
splitOn ").\n"
parseFormulae :: String -> Either String Annotated_formula
parseFormulae :: String -> Either String Annotated_formula
parseFormulae text :: String
text = case GenParser Char () Annotated_formula
-> () -> String -> String -> Either ParseError Annotated_formula
forall tok st a.
GenParser tok st a -> st -> String -> [tok] -> Either ParseError a
runParser GenParser Char () Annotated_formula
forall st. CharParser st Annotated_formula
annotated_formula () "" String
text of
Right formula :: Annotated_formula
formula -> Annotated_formula -> Either String Annotated_formula
forall a b. b -> Either a b
Right Annotated_formula
formula
Left err :: ParseError
err -> String -> Either String Annotated_formula
forall a b. a -> Either a b
Left ("Warning: unable to parse proof:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
"Formula in the proof: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
text String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
"Error: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ParseError -> String
forall a. Show a => a -> String
show ParseError
err String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n")
graphFromProofObject :: [String] -> ProofTree
graphFromProofObject :: [String] -> ProofTree
graphFromProofObject l :: [String]
l = case (((([(Int, ProofGraphNode)], [(Int, Int, Int)]),
(Int, HashMap String Int, [String]))
-> Either String Annotated_formula
-> (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
(Int, HashMap String Int, [String])))
-> (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
(Int, HashMap String Int, [String]))
-> [Either String Annotated_formula]
-> (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
(Int, HashMap String Int, [String]))
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
(Int, HashMap String Int, [String]))
-> Either String Annotated_formula
-> (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
(Int, HashMap String Int, [String]))
addNode (([], []), (0, HashMap String Int
forall k v. HashMap k v
Map.empty,[])) ([Either String Annotated_formula]
-> (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
(Int, HashMap String Int, [String])))
-> ([String] -> [Either String Annotated_formula])
-> [String]
-> (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
(Int, HashMap String Int, [String]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Either String Annotated_formula)
-> [String] -> [Either String Annotated_formula]
forall a b. (a -> b) -> [a] -> [b]
map String -> Either String Annotated_formula
parseFormulae ([String] -> [Either String Annotated_formula])
-> ([String] -> [String])
-> [String]
-> [Either String Annotated_formula]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
splitFormulae (String -> [String])
-> ([String] -> String) -> [String] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines) [String]
l of
((ns :: [(Int, ProofGraphNode)]
ns, es :: [(Int, Int, Int)]
es),(_,_,[])) -> Gr ProofGraphNode Int -> ProofTree
ProofGraph (Gr ProofGraphNode Int -> ProofTree)
-> Gr ProofGraphNode Int -> ProofTree
forall a b. (a -> b) -> a -> b
$ [(Int, ProofGraphNode)]
-> [(Int, Int, Int)] -> Gr ProofGraphNode Int
forall (gr :: * -> * -> *) a b.
Graph gr =>
[LNode a] -> [LEdge b] -> gr a b
mkGraph [(Int, ProofGraphNode)]
ns [(Int, Int, Int)]
es
_ -> String -> ProofTree
ProofTree (String -> ProofTree) -> String -> ProofTree
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String]
l
where
strName :: Name -> String
strName :: Name -> String
strName (NameString t :: Token
t ) = Token -> String
tokStr Token
t
strName (NameInteger i :: Integer
i) = Integer -> String
forall a. Show a => a -> String
show Integer
i
strSentence :: Annotated_formula -> String
strSentence :: Annotated_formula -> String
strSentence = Doc -> String
forall a. Show a => a -> String
show (Doc -> String)
-> (Annotated_formula -> Doc) -> Annotated_formula -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annotated_formula -> Doc
forall a. Pretty a => a -> Doc
pretty
addNode :: (([(Int, ProofGraphNode)], [(Int, Int, Int)]), (Int, Map.HashMap String Int,[String]))
-> Either String Annotated_formula
-> (([(Int, ProofGraphNode)], [(Int, Int, Int)]), (Int, Map.HashMap String Int,[String]))
addNode :: (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
(Int, HashMap String Int, [String]))
-> Either String Annotated_formula
-> (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
(Int, HashMap String Int, [String]))
addNode ((_,_),(_,_,errs :: [String]
errs)) (Left err :: String
err) = (([],[]),(0,HashMap String Int
forall k v. HashMap k v
Map.empty,String
errString -> [String] -> [String]
forall a. a -> [a] -> [a]
:[String]
errs))
addNode args :: (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
(Int, HashMap String Int, [String]))
args@((nodeList :: [(Int, ProofGraphNode)]
nodeList,edgeList :: [(Int, Int, Int)]
edgeList),(index :: Int
index,keyIdMap :: HashMap String Int
keyIdMap,[])) (Right formula :: Annotated_formula
formula) =
let forName :: String
forName = Name -> String
strName (Annotated_formula -> Name
name Annotated_formula
formula)
forSentence :: String
forSentence = Annotated_formula -> String
strSentence Annotated_formula
formula
(anons :: Int
anons,infrs :: [(Int, String)]
infrs,newEdges :: [(Int, Int, Int)]
newEdges) = Annotations -> (Int, [(Int, String)], [(Int, Int, Int)])
extractParentEdges (Annotated_formula -> Annotations
annotations Annotated_formula
formula) in
if String
forName String -> HashMap String Int -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
`Map.member` HashMap String Int
keyIdMap then (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
(Int, HashMap String Int, [String]))
args else
((((Int, String) -> (Int, ProofGraphNode))
-> [(Int, String)] -> [(Int, ProofGraphNode)]
forall a b. (a -> b) -> [a] -> [b]
map (\(i :: Int
i,infr :: String
infr)->(Int
i,String -> ProofGraphNode
forall a b. a -> Either a b
Left String
infr)) [(Int, String)]
infrs [(Int, ProofGraphNode)]
-> [(Int, ProofGraphNode)] -> [(Int, ProofGraphNode)]
forall a. [a] -> [a] -> [a]
++ (Int
index, (String, String) -> ProofGraphNode
forall a b. b -> Either a b
Right (String
forName,String
forSentence)) (Int, ProofGraphNode)
-> [(Int, ProofGraphNode)] -> [(Int, ProofGraphNode)]
forall a. a -> [a] -> [a]
: [(Int, ProofGraphNode)]
nodeList
, [(Int, Int, Int)]
newEdges [(Int, Int, Int)] -> [(Int, Int, Int)] -> [(Int, Int, Int)]
forall a. [a] -> [a] -> [a]
++ (-Int
indexInt -> Int -> Int
forall a. Num a => a -> a -> a
-1,Int
index,-1)(Int, Int, Int) -> [(Int, Int, Int)] -> [(Int, Int, Int)]
forall a. a -> [a] -> [a]
:[(Int, Int, Int)]
edgeList)
,(Int
index Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
anons Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
, String -> Int -> HashMap String Int -> HashMap String Int
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
Map.insert String
forName Int
index HashMap String Int
keyIdMap
, [] ))
where
extractParentEdges :: Annotations -> (Int,[(Int,String)],[(Int, Int, Int)])
extractParentEdges :: Annotations -> (Int, [(Int, String)], [(Int, Int, Int)])
extractParentEdges (Annotations (Just (src :: Source
src, _))) = Source
-> Int
-> Int
-> Maybe Int
-> (Int, [(Int, String)], [(Int, Int, Int)])
walkInferences Source
src Int
index Int
index Maybe Int
forall a. Maybe a
Nothing
extractParentEdges _ = (0,[],[])
walkInferences :: Source -> Int -> Int -> Maybe Int -> (Int,[(Int,String)],[(Int, Int, Int)])
walkInferences :: Source
-> Int
-> Int
-> Maybe Int
-> (Int, [(Int, String)], [(Int, Int, Int)])
walkInferences (Source_many srcs :: Sources
srcs) child :: Int
child start :: Int
start _ =
((Int, Source)
-> (Int, [(Int, String)], [(Int, Int, Int)])
-> (Int, [(Int, String)], [(Int, Int, Int)]))
-> (Int, [(Int, String)], [(Int, Int, Int)])
-> [(Int, Source)]
-> (Int, [(Int, String)], [(Int, Int, Int)])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Int, Source)
-> (Int, [(Int, String)], [(Int, Int, Int)])
-> (Int, [(Int, String)], [(Int, Int, Int)])
collectInferences (0,[],[]) ([Int] -> Sources -> [(Int, Source)]
forall a b. [a] -> [b] -> [(a, b)]
zip [0..] Sources
srcs)
where
collectInferences :: (Int,Source) -> (Int,[(Int,String)],[(Int,Int,Int)]) -> (Int,[(Int,String)],[(Int,Int,Int)])
collectInferences :: (Int, Source)
-> (Int, [(Int, String)], [(Int, Int, Int)])
-> (Int, [(Int, String)], [(Int, Int, Int)])
collectInferences (i :: Int
i,s :: Source
s) (oAnons :: Int
oAnons,oInfr :: [(Int, String)]
oInfr,oEdges :: [(Int, Int, Int)]
oEdges) =
let (nAnons :: Int
nAnons,nInfr :: [(Int, String)]
nInfr,nEdges :: [(Int, Int, Int)]
nEdges) = Source
-> Int
-> Int
-> Maybe Int
-> (Int, [(Int, String)], [(Int, Int, Int)])
walkInferences Source
s Int
child (Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
oAnons) (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i)
in (Int
nAnonsInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
oAnons, [(Int, String)]
nInfr [(Int, String)] -> [(Int, String)] -> [(Int, String)]
forall a. [a] -> [a] -> [a]
++ [(Int, String)]
oInfr, [(Int, Int, Int)]
nEdges [(Int, Int, Int)] -> [(Int, Int, Int)] -> [(Int, Int, Int)]
forall a. [a] -> [a] -> [a]
++ [(Int, Int, Int)]
oEdges)
walkInferences (Source_DAG (DAGS_name sname :: Name
sname)) child :: Int
child _ infrArg :: Maybe Int
infrArg =
let parent :: Int
parent = Int -> String -> HashMap String Int -> Int
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
Map.lookupDefault Int
child (Name -> String
strName Name
sname) HashMap String Int
keyIdMap
in (0,[],[(Int
parent, -Int
childInt -> Int -> Int
forall a. Num a => a -> a -> a
-1, Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe 0 Maybe Int
infrArg)])
walkInferences (Source_DAG (DAGS_record (Inference_record infrule :: Token
infrule _ parents :: Inference_parents
parents))) child :: Int
child start :: Int
start infrArg :: Maybe Int
infrArg =
let (nextNode :: Int
nextNode, nextStart :: Int
nextStart, anon :: Int
anon, aEdge :: [(Int, Int, Int)]
aEdge) =
case Maybe Int
infrArg of
Nothing -> (Int
child,Int
start,0,[])
Just iArg :: Int
iArg -> (Int
startInt -> Int -> Int
forall a. Num a => a -> a -> a
+1,Int
startInt -> Int -> Int
forall a. Num a => a -> a -> a
+1,1,[(-Int
startInt -> Int -> Int
forall a. Num a => a -> a -> a
-2,-Int
childInt -> Int -> Int
forall a. Num a => a -> a -> a
-1,Int
iArg)])
(nAnons :: Int
nAnons, nInfr :: [(Int, String)]
nInfr, nEdges :: [(Int, Int, Int)]
nEdges) =
Source
-> Int
-> Int
-> Maybe Int
-> (Int, [(Int, String)], [(Int, Int, Int)])
walkInferences (Sources -> Source
Source_many (Sources -> Source) -> Sources -> Source
forall a b. (a -> b) -> a -> b
$ (Parent_info -> Source) -> Inference_parents -> Sources
forall a b. (a -> b) -> [a] -> [b]
map (\(Parent_info src :: Source
src _) -> Source
src) Inference_parents
parents) Int
nextNode Int
nextStart Maybe Int
forall a. Maybe a
Nothing
in (Int
anonInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
nAnons,(-Int
nextNodeInt -> Int -> Int
forall a. Num a => a -> a -> a
-1, Token -> String
tokStr Token
infrule)(Int, String) -> [(Int, String)] -> [(Int, String)]
forall a. a -> [a] -> [a]
:[(Int, String)]
nInfr,[(Int, Int, Int)]
aEdge[(Int, Int, Int)] -> [(Int, Int, Int)] -> [(Int, Int, Int)]
forall a. [a] -> [a] -> [a]
++[(Int, Int, Int)]
nEdges)
walkInferences src :: Source
src child :: Int
child _ _ = (0,[(-Int
childInt -> Int -> Int
forall a. Num a => a -> a -> a
-1,Constr -> String
forall a. Show a => a -> String
show (Source -> Constr
forall a. Data a => a -> Constr
toConstr Source
src))],[])
addNode a :: (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
(Int, HashMap String Int, [String]))
a _ = (([(Int, ProofGraphNode)], [(Int, Int, Int)]),
(Int, HashMap String Int, [String]))
a
findSZS :: [String] -> String
findSZS :: [String] -> String
findSZS = (String, Bool) -> String
forall a b. (a, b) -> a
fst ((String, Bool) -> String)
-> ([String] -> (String, Bool)) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, Bool) -> String -> (String, Bool))
-> (String, Bool) -> [String] -> (String, Bool)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (String, Bool) -> String -> (String, Bool)
checkLine ("Could not determine SZS status", Bool
False)
where
checkLine :: (String, Bool) -> String -> (String, Bool)
checkLine :: (String, Bool) -> String -> (String, Bool)
checkLine (szsStatusLine :: String
szsStatusLine, found :: Bool
found) line :: String
line =
if Bool
found
then (String
szsStatusLine, Bool
found)
else if String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "Couldn't find " String
line
then (String
line, Bool
found)
else case String -> Maybe String
getSZSStatusWord String
line of
Just szsStatus :: String
szsStatus -> (String
szsStatus, Bool
True)
_ -> (String
szsStatusLine, Bool
found)
getSZSStatusWord :: String -> Maybe String
getSZSStatusWord :: String -> Maybe String
getSZSStatusWord line :: String
line = case String -> [String]
words (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe "" (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$
String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "SZS status" (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` "%# ") String
line of
[] -> Maybe String
forall a. Maybe a
Nothing
w :: String
w : _ -> String -> Maybe String
forall a. a -> Maybe a
Just String
w
filterProofLines :: [String] -> [String]
filterProofLines :: [String] -> [String]
filterProofLines = ([String], Bool) -> [String]
forall a b. (a, b) -> a
fst (([String], Bool) -> [String])
-> ([String] -> ([String], Bool)) -> [String] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> ([String], Bool) -> ([String], Bool))
-> ([String], Bool) -> [String] -> ([String], Bool)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr String -> ([String], Bool) -> ([String], Bool)
addIfInProof ([], Bool
False)
where
addIfInProof :: String -> ([String], Bool) -> ([String], Bool)
addIfInProof :: String -> ([String], Bool) -> ([String], Bool)
addIfInProof line :: String
line (addedLines :: [String]
addedLines, insideProof :: Bool
insideProof) =
if Bool
insideProof
then if String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "SZS output start" (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` "%# ") String
line
then ([String]
addedLines, Bool
False)
else (String
line String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
addedLines, Bool
insideProof)
else if String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "SZS output end" (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` "%# ") String
line
then ([String]
addedLines, Bool
True)
else ([String]
addedLines, Bool
insideProof)