content: {-# OPTIONS_GHC -Wno-unused-top-binds #-}
  
  -- Added for outputFileName
  
  module Main (main) where
  
  import Control.Concurrent.MVar
  import Control.Monad.Catch (
      SomeException,
      fromException,
      handle,
      throwM,
   )
  import Control.Monad.Extra (whenJust)
  import GlobalMain
  import Kore.BugReport
  import Kore.Exec (
      proveWithRepl,
   )
  import Kore.IndexedModule.MetadataToolsBuilder qualified as MetadataTools (
      build,
   )
  import Kore.Log (
      KoreLogOptions (..),
      SomeEntry (..),
      logEntry,
      runLoggerT,
      swappableLogger,
      withLoggerLegacy,
   )
  import Kore.Log.ErrorException (
      errorException,
   )
  import Kore.Log.KoreLogOptions (
      parseKoreLogOptions,
   )
  import Kore.Log.WarnIfLowProductivity (
      warnIfLowProductivity,
   )
  import Kore.Reachability.Claim qualified as Claim
  import Kore.Repl.Data
  import Kore.Rewrite.SMT.Lemma
  import Kore.Rewrite.Timeout (
      EnableMovingAverage,
      StepTimeout,
   )
  import Kore.Syntax.Module (
      ModuleName (..),
   )
  import Kore.Unparser (
      unparseToString,
   )
  import Options.Applicative (
      InfoMod,
      Parser,
      argument,
      flag,
      fullDesc,
      header,
      help,
      long,
      metavar,
      progDesc,
      short,
      showDefault,
      str,
      strOption,
      value,
   )
  import Options.SMT (
      KoreSolverOptions (..),
      parseKoreSolverOptions,
   )
  import Prelude.Kore
  import SMT qualified
  import System.Clock (
      Clock (Monotonic),
      TimeSpec,
      getTime,
   )
  import System.Exit (
      exitFailure,
      exitWith,
   )
  import System.FilePath (
      takeDirectory,
   )
  import System.IO (
      hPutStrLn,
      stderr,
   )
  
  -- | Represents a file name along with its module name passed.
  data KoreModule = KoreModule
      { fileName :: !FilePath
      , moduleName :: !ModuleName
      }
  
  -- | Options for the kore repl.
  data KoreReplOptions = KoreReplOptions
      { definitionModule :: !KoreModule
      , proveOptions :: !KoreProveOptions
      , smtOptions :: !KoreSolverOptions
      , korePrintCommand :: !KorePrintCommand
      , replMode :: !ReplMode
      , stepTime :: StepTime
      , scriptModeOutput :: !ScriptModeOutput
      , replScript :: !ReplScript
      , outputFile :: !OutputFile
      , koreLogOptions :: !KoreLogOptions
      , bugReportOption :: !BugReportOption
      }
  
  -- | Parse options after being given the value of startTime for KoreLogOptions
  parseKoreReplOptions :: TimeSpec -> Parser KoreReplOptions
  parseKoreReplOptions startTime =
      KoreReplOptions
          <$> parseMainModule
          <*> parseKoreProveOptions
          <*> parseKoreSolverOptions
          <*> parseKorePrintCommand
          <*> parseReplMode
          <*> parseShowStepTime
          <*> parseScriptModeOutput
          <*> parseReplScript
          <*> parseOutputFile
          <*> parseKoreLogOptions (ExeName "kore-repl") startTime
          <*> parseBugReportOption
    where
      parseMainModule :: Parser KoreModule
      parseMainModule =
          KoreModule
              <$> argument
                  str
                  ( metavar "MAIN_DEFINITION_FILE"
                      <> help "Kore definition file to verify and use for execution"
                  )
              <*> GlobalMain.parseModuleName
                  "MAIN_MODULE"
                  "module"
                  "Kore main module name."
  
      parseReplMode :: Parser ReplMode
      parseReplMode =
          flag
              Interactive
              RunScript
              ( long "run-mode"
                  <> short 'r'
                  <> help "Repl run script mode"
              )
  
      parseScriptModeOutput :: Parser ScriptModeOutput
      parseScriptModeOutput =
          flag
              DisableOutput
              EnableOutput
              ( long "save-run-output"
                  <> help "Get output in run mode."
              )
  
      parseReplScript :: Parser ReplScript
      parseReplScript =
          ReplScript
              <$> optional
                  ( strOption
                      ( metavar "REPL_SCRIPT"
                          <> long "repl-script"
                          <> help "Path to the repl script file"
                      )
                  )
  
      parseOutputFile :: Parser OutputFile
      parseOutputFile =
          OutputFile
              <$> optional
                  ( strOption
                      ( metavar "PATTERN_OUTPUT_FILE"
                          <> long "output"
                          <> help "Output file to contain final Kore pattern."
                      )
                  )
  
      parseKorePrintCommand :: Parser KorePrintCommand
      parseKorePrintCommand =
          KorePrintCommand
              <$> ( strOption
                      ( metavar "EXEC_FILE"
                          <> long "kore-print-command"
                          <> help "Command to run the kore-print pretty printer."
                          <> value "kore-print"
                          <> showDefault
                      )
                  )
  
      parseShowStepTime :: Parser StepTime
      parseShowStepTime =
          flag
              DisableStepTime
              EnableStepTime
              ( long "show-step-time"
                  <> help "Print the time taken by steps."
              )
  
  parserInfoModifiers :: InfoMod options
  parserInfoModifiers =
      fullDesc
          <> progDesc "REPL debugger for proofs"
          <> header "kore-repl - a repl for Kore proofs"
  
  exeName :: ExeName
  exeName = ExeName "kore-repl"
  
  -- | Environment variable name for extra arguments
  envName :: String
  envName = "KORE_REPL_OPTS"
  
  main :: IO ()
  main = do
      startTime <- getTime Monotonic
      options <-
          mainGlobal
              Main.exeName
              (Just envName)
              (parseKoreReplOptions startTime)
              parserInfoModifiers
      whenJust (localOptions options) mainWithOptions
  
  mainWithOptions :: LocalOptions KoreReplOptions -> IO ()
  mainWithOptions LocalOptions{execOptions} = do
      exitCode <-
          withBugReport Main.exeName bugReportOption $ \tempDirectory ->
              withLoggerLegacy tempDirectory koreLogOptions $ \actualLogAction -> do
                  mvarLogAction <- newMVar actualLogAction
                  let swapLogAction = swappableLogger mvarLogAction
                  flip runLoggerT swapLogAction $
                      runExceptionHandlers $ do
                          definition <-
                              loadDefinitions [definitionFileName, specFile]
                          indexedModule <- loadModule mainModuleName definition
                          specDefIndexedModule <- loadModule specModule definition
                          let validatedDefinition =
                                  addExtraAxioms indexedModule specDefIndexedModule
  
                          let smtConfig =
                                  SMT.defaultConfig
                                      { SMT.timeOut = smtTimeOut
                                      , SMT.rLimit = smtRLimit
                                      , SMT.resetInterval = smtResetInterval
                                      , SMT.prelude = smtPrelude
                                      }
  
                          when
                              ( replMode == RunScript
                                  && isNothing (unReplScript replScript)
                              )
                              $ lift
                              $ do
                                  hPutStrLn
                                      stderr
                                      "You must supply the path to the repl script\
                                      \ in order to run the repl in run-script mode."
                                  exitFailure
  
                          when
                              ( replMode == Interactive
                                  && scriptModeOutput == EnableOutput
                              )
                              $ lift
                              $ do
                                  hPutStrLn
                                      stderr
                                      "The --save-run-output flag is only available\
                                      \ when running the repl in run-script mode."
                                  exitFailure
  
                          SMT.runSMT
                              smtConfig
                              ( declareSMTLemmas
                                  (MetadataTools.build validatedDefinition)
                                  (getSMTLemmas validatedDefinition)
                              )
                              $ proveWithRepl
                                  replMinDepth
                                  replStepTimeout
                                  replEnableMovingAverage
                                  stepTime
                                  replStuckCheck
                                  replAllowVacuous
                                  validatedDefinition
                                  specDefIndexedModule
                                  Nothing
                                  mvarLogAction
                                  replScript
                                  replMode
                                  scriptModeOutput
                                  outputFile
                                  mainModuleName
                                  koreLogOptions
                                  (GlobalMain.kFileLocations definition)
                                  kompiledDir
                                  korePrintCommand
  
                          warnIfLowProductivity
                              (GlobalMain.kFileLocations definition)
                          pure ExitSuccess
      exitWith exitCode
    where
      KoreReplOptions
          { definitionModule
          , proveOptions
          , smtOptions
          , replScript
          , replMode
          , scriptModeOutput
          , outputFile
          , koreLogOptions
          , bugReportOption
          , korePrintCommand
          , stepTime
          } = execOptions
      runExceptionHandlers action =
          action
              & handle exitReplHandler
              & handle withConfigurationHandler
              & handle someExceptionHandler
  
      exitReplHandler :: ExitCode -> Main ExitCode
      exitReplHandler = pure
  
      withConfigurationHandler :: Claim.WithConfiguration -> Main ExitCode
      withConfigurationHandler
          (Claim.WithConfiguration lastConfiguration someException) =
              do
                  liftIO $
                      hPutStrLn
                          stderr
                          ("// Last configuration:\n" <> unparseToString lastConfiguration)
                  throwM someException
  
      someExceptionHandler :: SomeException -> Main ExitCode
      someExceptionHandler someException = do
          case fromException someException of
              Just entry@(SomeEntry _ _) -> logEntry entry
              Nothing -> errorException someException
          throwM someException
  
      mainModuleName :: ModuleName
      mainModuleName = moduleName definitionModule
  
      definitionFileName :: FilePath
      definitionFileName = fileName definitionModule
  
      specModule :: ModuleName
      specModule = specMainModule proveOptions
  
      specFile :: FilePath
      specFile = specFileName proveOptions
  
      kompiledDir :: KompiledDir
      kompiledDir = KompiledDir . takeDirectory $ fileName definitionModule
  
      smtTimeOut :: SMT.TimeOut
      smtTimeOut = timeOut smtOptions
  
      smtRLimit :: SMT.RLimit
      smtRLimit = rLimit smtOptions
  
      smtResetInterval :: SMT.ResetInterval
      smtResetInterval = resetInterval smtOptions
  
      smtPrelude :: SMT.Prelude
      smtPrelude = prelude smtOptions
  
      replStuckCheck :: Claim.StuckCheck
      replStuckCheck = stuckCheck proveOptions
  
      replMinDepth :: Maybe Claim.MinDepth
      replMinDepth = minDepth proveOptions
  
      replAllowVacuous :: Claim.AllowVacuous
      replAllowVacuous = allowVacuous proveOptions
  
      replStepTimeout :: Maybe StepTimeout
      replStepTimeout = GlobalMain.stepTimeout proveOptions
  
      replEnableMovingAverage :: EnableMovingAverage
      replEnableMovingAverage = GlobalMain.enableMovingAverage proveOptions
  