{- |
Module      :  ./TPTP/Prover/EProver/ProofParser.hs
Description :  Parses an EProver proof.
Copyright   :  (c) Eugen Kuksa University of Magdeburg 2017
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Eugen Kuksa <kuksa@iks.cs.ovgu.de>
Stability   :  provisional
Portability :  non-portable (imports Logic)
-}

module TPTP.Prover.EProver.ProofParser (parseTimeUsed) where

import Data.Char
import Data.List

-- Find the "CPU  Time" line and parse the time
parseTimeUsed :: [String] -> Int
parseTimeUsed :: [String] -> Int
parseTimeUsed = (Int, Bool) -> Int
forall a b. (a, b) -> a
fst ((Int, Bool) -> Int)
-> ([String] -> (Int, Bool)) -> [String] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, Bool) -> String -> (Int, Bool))
-> (Int, Bool) -> [String] -> (Int, Bool)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Int, Bool) -> String -> (Int, Bool)
checkLine (-1, Bool
False)
  where
    checkLine :: (Int, Bool) -> String -> (Int, Bool)
    checkLine :: (Int, Bool) -> String -> (Int, Bool)
checkLine (time :: Int
time, found :: Bool
found) line :: String
line =
      if Bool
found
      then (Int
time, Bool
found)
      else if "CPU  Time" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` (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 let time' :: Int
time' = case (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
takeWhile Char -> Bool
isDigit (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall a. [a] -> a
last (String -> [String]
words String
line) of
                      ds :: String
ds@(_ : _) -> String -> Int
forall a. Read a => String -> a
read String
ds
                      _ -> Int
time
                in (Int
time', Bool
found)
           else (Int
time, Bool
found)