{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE NoImplicitPrelude #-}

module Felix.CommandLine
    ( runCommandLine
    , Input(..)
    , VerificationOptions(..)
    , Command(..)
    , CommandOutcome(..)
    , VerifiedOutputFailure(..)
    , parseCommandArguments
    , verificationCommandOutcome
    , commandOutcomeExitCode
    , renderCommandOutcome
    ) where

import Base
import Felix.OutputPlan qualified as Output
import Felix.Parse (ParseWorkspaceError)
import Felix.Parse qualified as Parse
import Felix.Provers qualified as Provers
import Felix.RequestDump qualified as RequestDump
import Felix.Source (SafeRelativePath)
import Felix.Source.Graph qualified as SourceGraph
import Felix.Store qualified as Store
import Felix.Verification qualified as Verification
import Felix.Version qualified as Version
import Felix.Workspace qualified as Workspace
import Felix.Render.Html.Export qualified as HtmlExport
import Felix.Render.Html.Layout qualified as HtmlLayout
import Felix.Render.Html.Output qualified as HtmlOutput
import Felix.Report.Location

import Control.Monad (unless, when)
import Data.Maybe (catMaybes)
import Data.Text qualified as StrictText
import Data.Text.IO qualified as Text
import GHC.Conc qualified
import Numeric (showFFloat)
import Options.Applicative hiding (renderFailure)
import System.Environment (getArgs, lookupEnv)
import System.Exit (ExitCode(..), exitWith)
import System.IO (stderr)
import Text.Read (readMaybe)


newtype Input = Input
    { inputFilePath :: FilePath
    }
    deriving stock (Show, Eq)

data VerificationOptions = VerificationOptions
    { verificationStoreSelection :: !Store.StoreSelection
    , verificationTimeLimit :: !Provers.TimeLimit
    , verificationMemoryLimit :: !Provers.MemoryLimit
    , verificationJobsOverride :: !(Maybe Provers.EffectiveJobs)
    , verificationDumpDestination :: !(Maybe FilePath)
    , verificationHtmlRequested :: !Bool
    }
    deriving stock (Show, Eq)

data Command
    = Version
    | ParseOnly !Input
    | Verify !Input !VerificationOptions
    deriving stock (Show, Eq)

data CommandOutcome
    = CommandCompleted
    | VerificationSucceeded
        !Verification.VerificationReport
        !Provers.SlowAtpReport
    | VerificationCompletedWithGaps
        !Verification.VerificationReport
        !Provers.SlowAtpReport
    | VerificationRejected
        !Verification.VerificationReport
        !Verification.FailedVerification
        !Provers.SlowAtpReport
    | VerificationCheckingRejected
        !Verification.VerificationReport
        !Verification.VerificationDriverError
        !Provers.SlowAtpReport
    | SourcePlanningFailed !ParseWorkspaceError
    | ParseOnlyFailed !Workspace.AuthorityFreeParseError
    | VerificationDriverFailed !Verification.VerificationDriverError
    | VerificationSessionFailed
        !Store.StorePath
        !Verification.VerificationSessionError
    | StorePlanningFailed !Store.StorePlanningError
    | StoreIncompatible !Store.StorePath !Store.StoreIncompatibility
    | StoreFailed !Store.StorePath !Store.StoreLifecycleError
    | OutputPlanningFailed !Output.OutputPlanError
    | HtmlLayoutFailed !HtmlLayout.HtmlLayoutError
    | DumpObservationFailed !RequestDump.DumpObservationError
    | VerifiedOutputFailed
        !Verification.VerificationReport
        !VerifiedOutputFailure
        !Provers.SlowAtpReport
    deriving stock (Show)

data VerifiedOutputFailure
    = VerifiedHtmlExportFailed !HtmlExport.HtmlExportError
    | VerifiedHtmlOutputPlanningFailed !HtmlOutput.HtmlOutputError
    | VerifiedHtmlPublicationFailed !HtmlOutput.HtmlPublicationError
    | VerifiedHtmlLayoutUnavailable
    deriving stock (Show)

data HtmlPreflight = HtmlPreflight
    !Workspace.WorkspaceEnvironment
    !SourceGraph.ResolvedSourceGraph
    !HtmlLayout.HtmlLayout
    ![SafeRelativePath]


runCommandLine :: IO ()
runCommandLine = do
    arguments <- getArgs
    selected <- handleParseResult (parseCommandArguments arguments)
    outcome <- runCommand selected
    renderCommandOutcome outcome
    exitWith (commandOutcomeExitCode outcome)

rawCommandParserInfo :: ParserInfo RawCommand
rawCommandParserInfo =
    info
        (helper <*> rawCommandParser)
        (fullDesc <> header "Felix")

runCommand :: Command -> IO CommandOutcome
runCommand = \case
    Version -> do
        Text.putStrLn Version.info
        pure CommandCompleted
    ParseOnly (Input input) ->
        Workspace.parseWorkspace input >>= \case
            Left failure ->
                pure (ParseOnlyFailed failure)
            Right _blocks ->
                pure CommandCompleted
    Verify input options ->
        runVerification input options

runVerification
    :: Input
    -> VerificationOptions
    -> IO CommandOutcome
runVerification input options = do
    plannedStore <-
        Store.planStore
            (verificationStoreSelection options)
    case plannedStore of
        Left failure ->
            pure (StorePlanningFailed failure)
        Right storePlan -> do
            htmlResult <- discoverHtmlDestinations input options
            case htmlResult of
                Left failure ->
                    pure failure
                Right htmlPreflight ->
                    Store.withStoreLease storePlan \lease -> do
                        outputResult <-
                            Output.planVerificationOutputs
                                (Store.storeLeasePath lease)
                                (verificationDumpDestination options)
                                (fmap
                                    (\(HtmlPreflight
                                            _environment _graph _layout destinations) ->
                                        ("html", destinations))
                                    htmlPreflight)
                        case outputResult of
                            Left failure ->
                                pure (OutputPlanningFailed failure)
                            Right outputPlan ->
                                openVerificationSession
                                    input
                                    options
                                    lease
                                    outputPlan
                                    htmlPreflight

discoverHtmlDestinations
    :: Input
    -> VerificationOptions
    -> IO (Either CommandOutcome (Maybe HtmlPreflight))
discoverHtmlDestinations input options
    | not (verificationHtmlRequested options) =
        pure (Right Nothing)
    | otherwise = do
        prepared <- prepareInputSourceGraph input
        pure case prepared of
            Left failure -> Left (SourcePlanningFailed failure)
            Right (environment, graph) ->
                case planHtmlDestinations environment graph of
                    Left failure -> Left (HtmlLayoutFailed failure)
                    Right (layout, destinations) ->
                        Right
                            (Just
                                (HtmlPreflight
                                    environment graph layout destinations))

planHtmlDestinations
    :: Workspace.WorkspaceEnvironment
    -> SourceGraph.ResolvedSourceGraph
    -> Either
        HtmlLayout.HtmlLayoutError
        (HtmlLayout.HtmlLayout, [SafeRelativePath])
planHtmlDestinations environment graph = do
    layout <-
        HtmlLayout.layoutHtmlSourceGraph
            (Workspace.workspaceHtmlMountPrefixes environment)
            graph
    pure
        ( layout
        , [ HtmlLayout.routeDestination route
          | (_source, route) <-
                HtmlLayout.htmlPageRoutes layout
          ]
            <> [HtmlLayout.routeDestination
                    (HtmlLayout.htmlSupportScriptRoute layout)]
        )

prepareInputSourceGraph
    :: Input
    -> IO
        (Either
            ParseWorkspaceError
            (Workspace.WorkspaceEnvironment, SourceGraph.ResolvedSourceGraph))
prepareInputSourceGraph input = do
    preparedEnvironment <- Workspace.prepareDefaultWorkspaceEnvironment
    case preparedEnvironment of
        Left failure -> pure (Left failure)
        Right environment -> do
            preparedRoot <- Workspace.prepareWorkspaceRoot
                environment
                (inputFilePath input)
            case preparedRoot of
                Left failure -> pure (Left failure)
                Right root ->
                    fmap (fmap (\graph -> (environment, graph)))
                        (Workspace.prepareSourceGraph environment root)

openVerificationSession
    :: Input
    -> VerificationOptions
    -> Store.StoreLease
    -> Output.VerificationOutputPlan
    -> Maybe HtmlPreflight
    -> IO CommandOutcome
openVerificationSession input options lease outputPlan htmlPreflight = do
    opened <- Verification.withVerificationSession lease
        (\session ->
            runOpenVerification
                input
                options
                outputPlan
                htmlPreflight
                session)
    pure case opened of
        Left
            (Verification.VerificationSessionStoreError
                (Store.StoreLifecycleOpenFailed
                    (Store.IncompatibleStore incompatibility))) ->
                        StoreIncompatible
                            (Store.storeLeasePath lease)
                            incompatibility
        Left (Verification.VerificationSessionStoreError failure) ->
            StoreFailed (Store.storeLeasePath lease) failure
        Left failure ->
            VerificationSessionFailed (Store.storeLeasePath lease) failure
        Right outcome -> outcome

runOpenVerification
    :: Input
    -> VerificationOptions
    -> Output.VerificationOutputPlan
    -> Maybe HtmlPreflight
    -> Verification.VerificationSession
    -> IO CommandOutcome
runOpenVerification input options outputPlan htmlPreflight session = do
    observerResult <-
        RequestDump.prepareRequestObserver
            (Output.verificationDumpOutput outputPlan)
    case observerResult of
        Left failure ->
            pure (DumpObservationFailed failure)
        Right observer -> do
            (preparedGraph, htmlOutputPreparation) <- case htmlPreflight of
                Just (HtmlPreflight
                        environment graph layout _destinations) ->
                    pure
                        ( Right graph
                        , Just
                            ( Workspace.workspaceRendererSearchRoots environment
                            , layout
                            )
                        )
                Nothing -> do
                    graphResult <- fmap snd <$> prepareInputSourceGraph input
                    pure (graphResult, Nothing)
            case preparedGraph of
                Left failure -> pure (SourcePlanningFailed failure)
                Right graph -> do
                    vampirePath <- getVampireExecutable
                    jobs <- Provers.selectEffectiveJobs
                        (verificationJobsOverride options)
                        GHC.Conc.getNumProcessors
                    let vampire =
                            Provers.vampire
                                vampirePath
                                (verificationTimeLimit options)
                                (verificationMemoryLimit options)
                        validationMode =
                            case verificationStoreSelection options of
                                Store.FreshTemporaryStore ->
                                    Verification.FreshStoreValidation
                                Store.DefaultStore ->
                                    Verification.WarmStoreValidation
                                Store.ExplicitStore{} ->
                                    Verification.WarmStoreValidation
                        request = Verification.CheckRequest
                            { Verification.checkSourceGraph = graph
                            , Verification.checkStoreValidationMode =
                                validationMode
                            , Verification.checkEffectiveJobs = jobs
                            , Verification.checkVampire = vampire
                            , Verification.checkRequestObserver = observer
                            }
                    observed <- RequestDump.captureDumpFailure
                        (Verification.checkWorkspace session request)
                    case observed of
                        Left failure -> pure (DumpObservationFailed failure)
                        Right (Left failure) ->
                            pure (VerificationDriverFailed failure)
                        Right (Right outcome) ->
                            finishVerification
                                outputPlan
                                htmlOutputPreparation
                                outcome

finishVerification
    :: Output.VerificationOutputPlan
    -> Maybe ([FilePath], HtmlLayout.HtmlLayout)
    -> Verification.CheckOutcome
    -> IO CommandOutcome
finishVerification outputPlan selectedLayout outcome =
    case result of
        Verification.VerificationFailure{} ->
            pure (verificationCommandOutcome result slowReport)
        Verification.VerificationCheckingFailure{} ->
            pure (verificationCommandOutcome result slowReport)
        Verification.VerificationCompleted report presentation ->
            publishHtmlIfRequested
                outputPlan
                selectedLayout
                report
                presentation
                (VerificationSucceeded report slowReport)
                slowReport
        Verification.CompletedWithExplicitGaps report presentation ->
            publishHtmlIfRequested
                outputPlan
                selectedLayout
                report
                presentation
                (VerificationCompletedWithGaps report slowReport)
                slowReport
  where
    result = Verification.checkVerificationResult outcome
    slowReport = Verification.checkSlowAtpReport outcome

publishHtmlIfRequested
    :: Output.VerificationOutputPlan
    -> Maybe ([FilePath], HtmlLayout.HtmlLayout)
    -> Verification.VerificationReport
    -> Verification.VerificationPresentation
    -> CommandOutcome
    -> Provers.SlowAtpReport
    -> IO CommandOutcome
publishHtmlIfRequested
        outputPlan selectedLayout report presentation successOutcome slowReport =
    case Output.verificationHtmlRoutes outputPlan of
        Nothing ->
            pure successOutcome
        Just routes -> do
            case selectedLayout of
                Nothing ->
                    pure
                        (VerifiedOutputFailed
                            report
                            VerifiedHtmlLayoutUnavailable
                            slowReport)
                Just (rendererRoots, layout) -> do
                    prepared <-
                        HtmlExport.prepareHtmlExportWithLayoutFromRendererRoots
                            rendererRoots
                            layout
                            (Verification.verificationHtmlPresentation presentation)
                    case prepared of
                        Left failure ->
                            pure
                                (VerifiedOutputFailed
                                    report
                                    (VerifiedHtmlExportFailed failure)
                                    slowReport)
                        Right artifacts ->
                            case HtmlOutput.planHtmlOutputAgainst routes artifacts of
                                Left failure ->
                                    pure
                                        (VerifiedOutputFailed
                                            report
                                            (VerifiedHtmlOutputPlanningFailed failure)
                                            slowReport)
                                Right plan ->
                                    HtmlOutput.writeHtmlOutput plan >>= \case
                                        Left failure ->
                                            pure
                                                (VerifiedOutputFailed
                                                    report
                                                    (VerifiedHtmlPublicationFailed
                                                        failure)
                                                    slowReport)
                                        Right () ->
                                            pure successOutcome

verificationCommandOutcome
    :: Verification.VerificationResult
    -> Provers.SlowAtpReport
    -> CommandOutcome
verificationCommandOutcome result slowReport = case result of
    Verification.VerificationCompleted report _presentation ->
        VerificationSucceeded report slowReport
    Verification.CompletedWithExplicitGaps report _presentation ->
        VerificationCompletedWithGaps report slowReport
    Verification.VerificationFailure report failure ->
        VerificationRejected report failure slowReport
    Verification.VerificationCheckingFailure report failure ->
        VerificationCheckingRejected report failure slowReport

commandOutcomeExitCode :: CommandOutcome -> ExitCode
commandOutcomeExitCode = \case
    CommandCompleted ->
        ExitSuccess
    VerificationSucceeded{} ->
        ExitSuccess
    VerificationCompletedWithGaps{} ->
        ExitSuccess
    VerificationRejected _report failed _slow ->
        case Verification.failedVerificationReason failed of
            Verification.CountermodelFailure{} -> ExitFailure 1
            Verification.ContradictoryInputFailure{} -> ExitFailure 1
            Verification.IndeterminateFailure{} -> ExitFailure 2
            Verification.ProtocolFailure{} -> ExitFailure 2
            Verification.TransportFailure{} -> ExitFailure 2
    VerificationCheckingRejected _report failure _slow ->
        case Verification.verificationDriverErrorKind failure of
            Verification.VerificationSourceFailure -> ExitFailure 1
            Verification.VerificationInfrastructureFailure -> ExitFailure 2
    SourcePlanningFailed{} ->
        ExitFailure 1
    ParseOnlyFailed{} ->
        ExitFailure 1
    VerificationDriverFailed failure ->
        case Verification.verificationDriverErrorKind failure of
            Verification.VerificationSourceFailure -> ExitFailure 1
            Verification.VerificationInfrastructureFailure -> ExitFailure 2
    VerificationSessionFailed{} ->
        ExitFailure 2
    StorePlanningFailed{} ->
        ExitFailure 2
    StoreIncompatible{} ->
        ExitFailure 2
    StoreFailed{} ->
        ExitFailure 2
    OutputPlanningFailed{} ->
        ExitFailure 2
    HtmlLayoutFailed{} ->
        ExitFailure 2
    DumpObservationFailed{} ->
        ExitFailure 2
    VerifiedOutputFailed{} ->
        ExitFailure 2

renderCommandOutcome :: CommandOutcome -> IO ()
renderCommandOutcome = \case
    CommandCompleted ->
        pure ()
    VerificationSucceeded report slowReport -> do
        Text.hPutStrLn stderr "Verification successful."
        renderVerificationReport report
        renderSlowAtpReport slowReport
    VerificationCompletedWithGaps report slowReport -> do
        Text.hPutStrLn stderr
            "Verification completed with explicit proof gaps."
        renderVerificationReport report
        renderSlowAtpReport slowReport
    VerificationRejected report failure slowReport -> do
        renderFailedVerification failure
        renderVerificationReport report
        renderSlowAtpReport slowReport
    VerificationCheckingRejected report failure slowReport -> do
        renderVerificationDriverFailure failure
        renderVerificationReport report
        renderSlowAtpReport slowReport
    SourcePlanningFailed failure ->
        renderFailure
            ("Source planning failed: "
                <> Parse.renderParseWorkspaceError failure)
    ParseOnlyFailed failure ->
        renderFailure
            ("Parsing failed: "
                <> Workspace.renderAuthorityFreeParseError failure)
    VerificationDriverFailed failure ->
        renderVerificationDriverFailure failure
    VerificationSessionFailed path failure ->
        renderFailure case failure of
            Verification.VerificationSessionFoundationError{} ->
                "The fixed foundation manifest is invalid."
            Verification.VerificationSessionStoreError storeFailure ->
                "Store failure at "
                    <> quotePath (Store.storePathFilePath path)
                    <> ": "
                    <> Store.renderStoreLifecycleError storeFailure
            Verification.VerificationSessionTheoryMismatch expected actual ->
                "Store theory mismatch at "
                    <> quotePath (Store.storePathFilePath path)
                    <> ": expected "
                    <> StrictText.pack (show expected)
                    <> ", found "
                    <> StrictText.pack (show actual)
    StorePlanningFailed failure ->
        renderFailure
            ("Store path planning failed: "
                <> Store.renderStorePlanningError failure)
    StoreIncompatible path failure ->
        renderFailure
            ("Disposable store "
                <> quotePath (Store.storePathFilePath path)
                <> " is incompatible: "
                <> Store.renderStoreIncompatibility failure
                <> ". Use --fresh, choose another --store path, or remove the disposable store.")
    StoreFailed path failure ->
        renderFailure
            ("Store failure at "
                <> quotePath (Store.storePathFilePath path)
                <> ": " <> Store.renderStoreLifecycleError failure)
    OutputPlanningFailed failure ->
        renderFailure
            ("Verification output preflight failed: "
                <> Output.renderOutputPlanError failure)
    HtmlLayoutFailed failure ->
        renderFailure
            ("HTML route planning failed: "
                <> HtmlLayout.renderHtmlLayoutError failure)
    DumpObservationFailed failure ->
        renderFailure (RequestDump.renderDumpObservationError failure)
    VerifiedOutputFailed report failure slowReport -> do
        renderVerifiedOutputFailure failure
        renderVerificationReport report
        renderSlowAtpReport slowReport

renderFailure :: Text -> IO ()
renderFailure =
    Text.hPutStrLn stderr

renderVerificationDriverFailure
    :: Verification.VerificationDriverError
    -> IO ()
renderVerificationDriverFailure =
    renderFailure . Verification.renderVerificationDriverError

quotePath :: FilePath -> Text
quotePath = StrictText.pack . show

renderFailedVerification :: Verification.FailedVerification -> IO ()
renderFailedVerification failed =
    case Verification.failedVerificationReason failed of
        Verification.CountermodelFailure tptp -> do
            renderFailedTask tptp
            Text.hPutStrLn stderr
                ("Verification failed: prover found countermodel at "
                    <> locationToText location)
            Text.hPutStrLn stderr
                "This often happens when an explicit justification with \\cref{...} is missing some references."
        Verification.ContradictoryInputFailure tptp -> do
            renderFailedTask tptp
            Text.hPutStrLn stderr
                ("Verification failed: contradictory axioms at "
                    <> locationToText location)
            Text.hPutStrLn stderr
                "This is usually caused by an incorrect axiom or a theorem that has its proof omitted."
        Verification.IndeterminateFailure tptp -> do
            renderFailedTask tptp
            Text.hPutStrLn stderr
                ("Verification failed: prover returned an indeterminate result at "
                    <> locationToText location)
        Verification.ProtocolFailure label message -> do
            Text.hPutStrLn stderr
                ("Prover error at " <> locationToText location <> ":")
            Text.hPutStrLn stderr ("Task: " <> label)
            Text.hPutStrLn stderr ("Error: " <> message)
        Verification.TransportFailure processError -> do
            Text.hPutStrLn stderr
                ("Prover process error at " <> locationToText location <> ":")
            Text.hPutStrLn stderr (StrictText.pack (show processError))
  where
    location = Verification.failedVerificationLocation failed

renderVerifiedOutputFailure :: VerifiedOutputFailure -> IO ()
renderVerifiedOutputFailure = \case
    VerifiedHtmlExportFailed failure ->
        renderFailure
            ("Verification succeeded, but HTML preparation failed: "
                <> HtmlExport.renderHtmlExportError failure)
    VerifiedHtmlOutputPlanningFailed failure ->
        renderFailure
            ("Verification succeeded, but prepared HTML did not match the reserved routes: "
                <> HtmlOutput.renderHtmlOutputError failure)
    VerifiedHtmlPublicationFailed failure -> do
        renderFailure
            "Verification succeeded, but HTML publication did not complete."
        traverse_
            renderFailure
            (HtmlOutput.renderHtmlPublicationError failure)
    VerifiedHtmlLayoutUnavailable ->
        renderFailure
            "Verification succeeded, but the preflight HTML layout was unavailable."

renderFailedTask :: Text -> IO ()
renderFailedTask tptp = do
    Text.hPutStrLn stderr "(Failed TPTP task follows.)"
    Text.hPutStrLn stderr tptp

renderVerificationReport :: Verification.VerificationReport -> IO ()
renderVerificationReport report = do
    Text.hPutStrLn stderr
        ( "Direct source authorization summary: "
            <> renderCount
                sourceAxiomCount
                "source axiom"
            <> ", "
            <> renderCount
                omittedCount
                "explicit proof gap"
            <> "."
        )
    for_
        (Verification.verificationDirectEscapes report)
        \escape ->
            Text.hPutStrLn stderr case Verification.reportedEscapeKind escape of
                Verification.ReportedSourceAxiom ->
                    "Source axiom at "
                        <> locationToText
                            (Verification.reportedEscapeLocation escape)
                Verification.ReportedOmitted ->
                    "Explicit proof gap at "
                        <> locationToText
                            (Verification.reportedEscapeLocation escape)
  where
    sourceAxiomCount =
        length
            [ ()
            | escape <- Verification.verificationDirectEscapes report
            , Verification.reportedEscapeKind escape
                == Verification.ReportedSourceAxiom
            ]
    omittedCount =
        length
            [ ()
            | escape <- Verification.verificationDirectEscapes report
            , Verification.reportedEscapeKind escape
                == Verification.ReportedOmitted
            ]
    renderCount amount noun =
        StrictText.pack (show amount)
            <> " "
            <> noun
            <> if amount == 1 then "" else "s"

renderSlowAtpReport :: Provers.SlowAtpReport -> IO ()
renderSlowAtpReport report =
    unless (null (Provers.slowAtpTasks report)) do
        Text.hPutStrLn stderr
            "Slow Vampire tasks (executor wall time; run-local performance note):"
        traverse_ renderTask (Provers.slowAtpTasks report)
        let omitted = Provers.slowAtpOmittedTaskCount report
        when (omitted > 0)
            (Text.hPutStrLn stderr
                ( StrictText.pack
                    (show (length (Provers.slowAtpTasks report)))
                    <> " slowest shown; "
                    <> StrictText.pack (show omitted)
                    <> " additional tasks took at least 5.0 seconds."
                ))
  where
    renderTask task =
        Text.hPutStrLn stderr
            ( "  "
                <> renderAtpDuration (Provers.slowAtpDuration task)
                <> " "
                <> renderSlowAtpOutcome (Provers.slowAtpOutcome task)
                <> " at "
                <> locationToText (Provers.slowAtpLocation task)
                <> " (module "
                <> renderNatural
                    (Provers.workPositionModuleOrdinal
                        (Provers.slowAtpPosition task))
                <> ", request "
                <> renderNatural
                    (Provers.workPositionLocalRequestOrdinal
                        (Provers.slowAtpPosition task))
                <> ", id "
                <> StrictText.pack (show (Provers.slowAtpRequestId task))
                <> ")"
            )

    renderNatural = StrictText.pack . show

renderAtpDuration :: Provers.AtpDuration -> Text
renderAtpDuration duration =
    StrictText.pack
        (showFFloat
            (Just 2)
            (fromIntegral (Provers.atpDurationNanoseconds duration)
                / (1000000000 :: Double))
            "s")

renderSlowAtpOutcome :: Provers.SlowAtpOutcome -> Text
renderSlowAtpOutcome = \case
    Provers.SlowAtpAccepted -> "accepted"
    Provers.SlowAtpRejected rejection ->
        "rejected (" <> StrictText.pack (show rejection) <> ")"
    Provers.SlowAtpProtocolFailed -> "protocol failure"
    Provers.SlowAtpProcessFailed -> "process failure"

getVampireExecutable :: IO FilePath
getVampireExecutable =
    fromMaybe "vampire" <$> lookupEnv "FELIX_VAMPIRE"


data RawCommand
    = RawVersion
    | RawFile !RawFileCommand

data RawFileCommand = RawFileCommand
    { rawInput :: !Input
    , rawParseOnly :: !Bool
    , rawStore :: !(Maybe FilePath)
    , rawFresh :: !Bool
    , rawTimeLimit :: !(Maybe Provers.TimeLimit)
    , rawMemoryLimit :: !(Maybe Provers.MemoryLimit)
    , rawJobs :: !(Maybe Provers.EffectiveJobs)
    , rawDump :: !(Maybe FilePath)
    , rawHtml :: !Bool
    }

rawCommandParser :: Parser RawCommand
rawCommandParser =
    versionParser
        <|> (RawFile <$> rawFileCommandParser)

versionParser :: Parser RawCommand
versionParser =
    flag'
        RawVersion
        (long "version" <> help "Show the Felix version.")

inputParser :: Parser Input
inputParser =
    Input
        <$> strArgument
            (help "Source file" <> metavar "FILE")

rawFileCommandParser :: Parser RawFileCommand
rawFileCommandParser =
    RawFileCommand
        <$> inputParser
        <*> switch
            (long "parseonly"
                <> help "Resolve and parse source without verification.")
        <*> optional
            (strOption
                (long "store"
                    <> metavar "PATH"
                    <> help "Use the disposable SQLite store at PATH."))
        <*> switch
            (long "fresh"
                <> help "Use a fresh temporary disposable store.")
        <*> optional timeLimitParser
        <*> optional memoryLimitParser
        <*> optional jobsParser
        <*> optional
            (strOption
                (long "dump"
                    <> metavar "DUMPDIR"
                    <> help "Dump exact Vampire requests as they execute."))
        <*> switch
            (long "html"
                <> help "Publish verified HTML under ./html.")

parseCommandArguments :: [String] -> ParserResult Command
parseCommandArguments arguments =
    case execParserPure
            defaultPrefs
            rawCommandParserInfo
            arguments of
        Success raw ->
            case validateRawCommand raw of
                Left message ->
                    Failure
                        (parserFailure
                            defaultPrefs
                            rawCommandParserInfo
                            (ErrorMsg message)
                            [])
                Right selected ->
                    Success selected
        Failure failure ->
            Failure failure
        CompletionInvoked completion ->
            CompletionInvoked completion

validateRawCommand :: RawCommand -> Either String Command
validateRawCommand = \case
    RawVersion ->
        Right Version
    RawFile raw
        | rawParseOnly raw
        , not (null verificationOnlyOptions) ->
            Left
                ("--parseonly cannot be combined with verification options: "
                    <> unwords verificationOnlyOptions)
        | rawParseOnly raw ->
            Right (ParseOnly (rawInput raw))
        | isJust (rawStore raw) && rawFresh raw ->
            Left "--store and --fresh are mutually exclusive"
        | otherwise ->
            Right
                (Verify
                    (rawInput raw)
                    VerificationOptions
                        { verificationStoreSelection =
                            case rawStore raw of
                                Just path ->
                                    Store.ExplicitStore path
                                Nothing
                                    | rawFresh raw ->
                                        Store.FreshTemporaryStore
                                    | otherwise ->
                                        Store.DefaultStore
                        , verificationTimeLimit =
                            fromMaybe
                                Provers.defaultTimeLimit
                                (rawTimeLimit raw)
                        , verificationMemoryLimit =
                            fromMaybe
                                Provers.defaultMemoryLimit
                                (rawMemoryLimit raw)
                        , verificationJobsOverride = rawJobs raw
                        , verificationDumpDestination =
                            rawDump raw
                        , verificationHtmlRequested =
                            rawHtml raw
                        })
      where
        verificationOnlyOptions =
            catMaybes
                [ "--store" <$ rawStore raw
                , if rawFresh raw then Just "--fresh" else Nothing
                , "--timelimit" <$ rawTimeLimit raw
                , "--memlimit" <$ rawMemoryLimit raw
                , "--jobs" <$ rawJobs raw
                , "--dump" <$ rawDump raw
                , if rawHtml raw then Just "--html" else Nothing
                ]

timeLimitParser :: Parser Provers.TimeLimit
timeLimitParser =
    Provers.Seconds
        <$> option auto
            ( long "timelimit"
                <> short 't'
                <> metavar "SECONDS"
                <> help "Time limit for each Vampire request."
            )

memoryLimitParser :: Parser Provers.MemoryLimit
memoryLimitParser =
    Provers.Megabytes
        <$> option auto
            ( long "memlimit"
                <> short 'm'
                <> metavar "MB"
                <> help "Memory limit for each Vampire process."
            )

jobsParser :: Parser Provers.EffectiveJobs
jobsParser =
    option
        (eitherReader parseJobs)
        ( long "jobs"
            <> short 'j'
            <> metavar "JOBS"
            <> help
                "Run at most JOBS module checkers and Vampire invocations."
        )
  where
    parseJobs raw =
        case readMaybe raw >>= Provers.effectiveJobs of
            Just jobs -> Right jobs
            Nothing -> Left "JOBS must be a positive integer"