d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin{- |

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrinModule : $Header$

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrinDescription : Analyze eprover Output

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrinCopyright : (c) Jonathan von Schroeder, DFKI Bremen 2013

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrinLicense : GPLv2 or higher, see LICENSE.txt

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrinMaintainer : Jonathan von Schroeder <j.von_schroeder@dfki.de>

96ad5d81ee4a2cc66a4ae19893efc8aa6d06fae7jailletcStability : provisional

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrinPortability : portable

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin-}

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen

2e545ce2450a9953665f701bb05350f0d3f26275ndmodule SoftFOL.EProver(proof,axiomsOf) where

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowenimport Text.ParserCombinators.Parsec

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrinimport Common.Parsec

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrinimport Common.Doc (renderText)

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrinimport Common.GlobalAnnotations (emptyGlobalAnnos)

af33a4994ae2ff15bc67d19ff1a7feb906745bf8rbowenimport SoftFOL.ParseTPTP (singleQuoted,form,genList,GenTerm(..),

3f08db06526d6901aa08c110b5bc7dde6bc39905nd GenTerm(..),GenData(..),AWord(..))

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrinimport SoftFOL.Sign (SPTerm(..))

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrinimport SoftFOL.PrintTPTP (printTPTP)

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrinimport qualified Data.Set as Set

3f08db06526d6901aa08c110b5bc7dde6bc39905ndimport Data.List (foldl')

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrindata Role = Axiom | Other deriving (Show,Eq)

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin

253547fb9cc7986e84ff68aef076f664fc4169dctakashidata Inference = ProofOf String

253547fb9cc7986e84ff68aef076f664fc4169dctakashi | File { fileName :: String, formulaName :: String }

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin | Rule { rule :: String, parent :: String }

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin | Inference { rule :: String,

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin status :: String,

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin parents :: Set.Set String } deriving Eq

a7818b8de55671a82b0863d27665713f265af7aeigalic

a7818b8de55671a82b0863d27665713f265af7aeigalicinstance Show Inference where

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin show (ProofOf s) = "Proof for " ++ s ++ ""

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin show (File f s) = "Term named " ++ s ++

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin " in file " ++ f

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin show (Rule r p) = "Used inference rule \"" ++ r ++

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin "\" on term " ++ (show p)

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin show (Inference r s p) = "Used inference rule \"" ++ r ++

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin "\" on terms " ++ (show $ Set.toList p) ++

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin ", SZS: " ++ s ++""

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrindata ProofStep = ProofStep {

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin name :: String,

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin role :: Role,

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin formula :: SPTerm,

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin inference :: Inference } | Empty deriving Eq

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrininstance Show ProofStep where

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin show (ProofStep n r f i) = case r of

016241a6ee9c7b02ff94f30f90e705012ea08e41jsl Axiom -> "Axiom " ++ show n ++ "\nFormula: (" ++

016241a6ee9c7b02ff94f30f90e705012ea08e41jsl renderText emptyGlobalAnnos (printTPTP f) ++ ")\n"

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin ++ "Source: " ++ show i

016241a6ee9c7b02ff94f30f90e705012ea08e41jsl _ -> "Inferred " ++ show n ++ "\nFormula: (" ++

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin renderText emptyGlobalAnnos (printTPTP f) ++ ")\n"

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin ++ "Inference: " ++ show i

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrinwhiteSpace :: Parser ()

016241a6ee9c7b02ff94f30f90e705012ea08e41jslwhiteSpace = oneOf "\r\t\v\f " >> return ()

016241a6ee9c7b02ff94f30f90e705012ea08e41jsl

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsfline :: Parser ProofStep

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrinline = ((do

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin string "cnf(" <|> string "fof("

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin n <- tok

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin r <- tok

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin f <- many whiteSpace >> form

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin char ','

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin i <- pinference

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin string ")."

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin return $ ProofStep n (if r == "axiom" then Axiom else Other)

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin f i) <|> commentOrEmptyLine) << eof

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrincommentOrEmptyLine :: Parser ProofStep

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrincommentOrEmptyLine = ((skipMany (char '#') >>

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin manyTill anyChar (lookAhead eof))

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin <|> (skipMany whiteSpace >> return "")) >> return Empty

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrintok :: Parser String

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrintok = skipMany whiteSpace >> many (noneOf ",")

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin << char ',' << skipMany whiteSpace

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrinpinference :: Parser Inference

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrinpinference = skipMany whiteSpace >> (

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin (do

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin string "file("

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin f <- singleQuoted

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin char ','

a29610af88e278144045bfa1bc63b4a1a4b5ff14trawick skipMany whiteSpace

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin n <- manyTill anyChar (char ')')

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin return $ File f n) <|>

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin (do

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin string "inference("

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin r <- tok

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin string "[status("

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin s <- manyTill anyChar (char ')')

30471a4650391f57975f60bbb6e4a90be7b284bfhumbedooh skipMany whiteSpace >> string "]"

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin skipMany whiteSpace >> string ","

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin ps' <- genList

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin let ps = genList2Parents ps'

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf skipMany whiteSpace

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin string ")"

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin return $ Inference r s (Set.fromList ps)

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin ) <|>

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin (do

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin n <- tok

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin string "['"

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin r <- manyTill anyChar (lookAhead $ oneOf "'")

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf string "']"

4aa603e6448b99f9371397d439795c91a93637eand return $ case r of

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic "proof" -> ProofOf n

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic _ -> Rule r n

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic ))

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalicgenList2Parents :: [GenTerm] -> [String]

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalicgenList2Parents = map genTerm2Parents

4aa603e6448b99f9371397d439795c91a93637eand

e487d6c09669296f94a5190cc34586a98e624a00ndgenTerm2Parents :: GenTerm -> String

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsfgenTerm2Parents (GenTerm (GenData (AWord n) []) Nothing) = n

d9b843d090f14405079b4a61a493316cd3f1e5b9minfringenTerm2Parents _ = []

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrinproof :: [String] -> [ProofStep]

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrinproof s =

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin snd $ foldr (\s' (s,ps') -> case runParser line () "" s' of

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin Right p' | p' /= Empty ->

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf if Set.member (name p') s || ps' == []

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin then (insertParents (inference p') s, p':ps')

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin else (s,ps')

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin _ -> (s,ps')) (Set.empty, []) s

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin where

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin insertParents :: Inference -> Set.Set String -> Set.Set String

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin insertParents (ProofOf n) s = Set.insert n s

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin insertParents (File _ n) s = Set.insert n s

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin insertParents (Rule _ p) s = Set.insert p s

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin insertParents (Inference _ szs ps'') s = Set.union ps'' s

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrinaxiomsOf :: [ProofStep] -> [String]

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrinaxiomsOf ps = map (formulaName . inference) $ filter (\p -> role p == Axiom) ps

d9b843d090f14405079b4a61a493316cd3f1e5b9minfrin