{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE LambdaCase #-}

-- |
-- Module       : Main
-- Description  : Run the TPTP parser on the entire TPTP library.
-- Copyright    : (c) Evgenii Kotelnikov, 2019
-- License      : GPL-3
-- Maintainer   : evgeny.kotelnikov@gmail.com
-- Stability    : experimental
--

module Main where

import System.Directory
import System.Environment
import System.IO

import Control.Monad.Extra

import Data.List (isSuffixOf)
import Data.Text (Text, isInfixOf)
import Text.Printf
import qualified Data.Text.IO as Text.IO
import Data.TPTP.Parse.Text (parseTPTPOnly)

data Result
  = Success
  | Failure String
  | Skipped
  deriving (Show, Eq, Ord)

unsupportedFile :: Text -> Bool
unsupportedFile contents = "thf" `isInfixOf` contents

parseInput :: Text -> Result
parseInput input
  | unsupportedFile input = Skipped
  | otherwise = either Failure (const Success) (parseTPTPOnly input)

printResult :: Result -> IO ()
printResult = \case
  Success   -> putStrLn "OK"
  Failure e -> putStrLn "FAIL" >> hPutStrLn stderr ("Error: " ++ e)
  Skipped   -> putStrLn "SKIP"

parseFile :: FilePath -> IO Result
parseFile fp = do
  input <- Text.IO.readFile fp
  putStr (fp ++ "\t")
  let result = parseInput input
  printResult result
  return result

listDirectory' :: FilePath -> IO [FilePath]
listDirectory' dir = do
  files <- listDirectory dir
  return [dir ++ "/" ++ file | file <- files]

tptpAxioms :: FilePath -> IO [FilePath]
tptpAxioms libraryPath = listDirectory' (libraryPath ++ "/" ++ "Axioms")

tptpProblems :: FilePath -> IO [FilePath]
tptpProblems libraryPath =  listDirectory' (libraryPath ++ "/" ++ "Problems")
                        >>= concatMapM listDirectory'

tptpSolutions :: FilePath -> IO [FilePath]
tptpSolutions libraryPath =  listDirectory' (libraryPath ++ "/" ++ "Solutions")
                         >>= concatMapM listDirectory'
                         >>= concatMapM listDirectory'

isTptpFile :: FilePath -> IO Bool
isTptpFile file = do
  isFile <- doesFileExist file
  return $ isFile && any (`isSuffixOf` file) [".p", ".ax", ".rm", ".s"]

main :: IO ()
main = do
  args <- getArgs
  let tptpLibraryPath = head args
  -- axioms   <- tptpAxioms tptpLibraryPath
  -- problems <- tptpProblems tptpLibraryPath
  solutions <- tptpSolutions tptpLibraryPath
  tptpFiles <- filterM isTptpFile solutions -- (axioms ++ problems)
  results <- mapM parseFile tptpFiles
  let (successful, failed, skipped) = statistic results
  let total = successful + failed + skipped
  putStrLn $ printf "Total: %d (%d successful, %d failed, %d skipped)"
                    total successful failed skipped

statistic :: [Result] -> (Int, Int, Int)
statistic = foldl update (0, 0, 0)
  where
    update (s, f, u) = \case
      Success   -> (s + 1, f,     u)
      Failure{} -> (s,     f + 1, u)
      Skipped   -> (s,     f,     u + 1)