{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}

module Crux.Config.Common (
  OutputOptions(..),
  CruxOptions(..),
  PathStrategy(..),
  cruxOptions,
  defaultOutputOptions,
  postprocessOptions,
) where

import Control.Lens (set)
import Data.Functor.Alt
import Data.Generics.Product.Fields (field)
import Data.Time(DiffTime, NominalDiffTime)
import Data.Maybe(fromMaybe)
import Data.Char(toLower)
import Data.Word (Word64)
import Data.Text (pack)
import GHC.Generics (Generic)
import System.Directory ( createDirectoryIfMissing )

import Crux.Config
import Crux.Config.Load (ColorOptions(..))
import Crux.Log as Log
import Config.Schema

import What4.ProblemFeatures

data PathStrategy
  = AlwaysMergePaths
  | SplitAndExploreDepthFirst

pathStrategySpec :: ValueSpec PathStrategy
pathStrategySpec :: ValueSpec PathStrategy
pathStrategySpec =
  (PathStrategy
AlwaysMergePaths PathStrategy -> ValueSpec () -> ValueSpec PathStrategy
forall a b. a -> ValueSpec b -> ValueSpec a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Text -> ValueSpec ()
atomSpec Text
"always-merge") ValueSpec PathStrategy
-> ValueSpec PathStrategy -> ValueSpec PathStrategy
forall a. ValueSpec a -> ValueSpec a -> ValueSpec a
forall (f :: * -> *) a. Alt f => f a -> f a -> f a
<!>
  (PathStrategy
SplitAndExploreDepthFirst PathStrategy -> ValueSpec () -> ValueSpec PathStrategy
forall a b. a -> ValueSpec b -> ValueSpec a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Text -> ValueSpec ()
atomSpec Text
"split-dfs")


postprocessOptions ::
  Logs msgs =>
  SupportsCruxLogMessage msgs =>
  CruxOptions -> IO CruxOptions
postprocessOptions :: forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxOptions -> IO CruxOptions
postprocessOptions =
  CruxOptions -> IO CruxOptions
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxOptions -> IO CruxOptions
checkPathStrategyInteractions (CruxOptions -> IO CruxOptions)
-> (CruxOptions -> IO CruxOptions) -> CruxOptions -> IO CruxOptions
forall a b.
(CruxOptions -> a) -> (CruxOptions -> b) -> CruxOptions -> b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
  CruxOptions -> IO CruxOptions
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxOptions -> IO CruxOptions
checkPathSatInteractions (CruxOptions -> IO CruxOptions)
-> (CruxOptions -> IO CruxOptions) -> CruxOptions -> IO CruxOptions
forall a b.
(CruxOptions -> a) -> (CruxOptions -> b) -> CruxOptions -> b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
  CruxOptions -> IO CruxOptions
checkBldDir

checkPathStrategyInteractions ::
  Logs msgs =>
  SupportsCruxLogMessage msgs =>
  CruxOptions -> IO CruxOptions
checkPathStrategyInteractions :: forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxOptions -> IO CruxOptions
checkPathStrategyInteractions CruxOptions
crux =
  case CruxOptions -> PathStrategy
pathStrategy CruxOptions
crux of
    PathStrategy
AlwaysMergePaths -> CruxOptions -> IO CruxOptions
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return CruxOptions
crux
    PathStrategy
SplitAndExploreDepthFirst
     | CruxOptions -> Bool
profileCrucibleFunctions CruxOptions
crux Bool -> Bool -> Bool
|| CruxOptions -> Bool
branchCoverage CruxOptions
crux ->
         do CruxLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxLogMessage -> IO ()
sayCrux CruxLogMessage
Log.DisablingProfilingIncompatibleWithPathSplitting
            return CruxOptions
crux { profileCrucibleFunctions = False, branchCoverage = False }
     | Bool
otherwise -> CruxOptions -> IO CruxOptions
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return CruxOptions
crux

checkPathSatInteractions ::
  Logs msgs =>
  SupportsCruxLogMessage msgs =>
  CruxOptions -> IO CruxOptions
checkPathSatInteractions :: forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxOptions -> IO CruxOptions
checkPathSatInteractions CruxOptions
crux =
  case CruxOptions -> Bool
checkPathSat CruxOptions
crux of
    Bool
True -> CruxOptions -> IO CruxOptions
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return CruxOptions
crux
    Bool
False
      | CruxOptions -> Bool
branchCoverage CruxOptions
crux ->
          do CruxLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxLogMessage -> IO ()
sayCrux CruxLogMessage
Log.DisablingBranchCoverageRequiresPathSatisfiability
             return CruxOptions
crux { branchCoverage = False }
      | Bool
otherwise -> CruxOptions -> IO CruxOptions
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return CruxOptions
crux

checkBldDir :: CruxOptions -> IO CruxOptions
checkBldDir :: CruxOptions -> IO CruxOptions
checkBldDir CruxOptions
crux = do
  Bool -> FilePath -> IO ()
createDirectoryIfMissing Bool
True (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ CruxOptions -> FilePath
bldDir CruxOptions
crux
  return CruxOptions
crux


data OutputOptions = OutputOptions
  { OutputOptions -> ColorOptions
colorOptions :: ColorOptions

  , OutputOptions -> Bool
printFailures :: Bool
    -- ^ Print errors regarding failed verification goals

  , OutputOptions -> Bool
printSymbolicVars :: Bool
    -- ^ Print values assigned to symbolic variables
    --   when printing failed verification goals

  , OutputOptions -> Int
simVerbose :: Int
    -- ^ Level of verbosity for the symbolic simulation

  , OutputOptions -> Bool
quietMode :: Bool
    -- ^ If true, produce minimal output

  }
  deriving ((forall x. OutputOptions -> Rep OutputOptions x)
-> (forall x. Rep OutputOptions x -> OutputOptions)
-> Generic OutputOptions
forall x. Rep OutputOptions x -> OutputOptions
forall x. OutputOptions -> Rep OutputOptions x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. OutputOptions -> Rep OutputOptions x
from :: forall x. OutputOptions -> Rep OutputOptions x
$cto :: forall x. Rep OutputOptions x -> OutputOptions
to :: forall x. Rep OutputOptions x -> OutputOptions
Generic)


defaultOutputOptions :: ColorOptions -> OutputOptions
defaultOutputOptions :: ColorOptions -> OutputOptions
defaultOutputOptions ColorOptions
copts = OutputOptions
  { colorOptions :: ColorOptions
colorOptions = ColorOptions
copts
  , printFailures :: Bool
printFailures = Bool
False
  , printSymbolicVars :: Bool
printSymbolicVars = Bool
False
  , quietMode :: Bool
quietMode = Bool
False
  , simVerbose :: Int
simVerbose = Int
0
  }


-- | Common options for Crux-based binaries.
data CruxOptions = CruxOptions
  { CruxOptions -> [FilePath]
inputFiles              :: [FilePath]
    -- ^ the files to analyze

  , CruxOptions -> FilePath
outDir                  :: FilePath
    -- ^ Write results in this location.
    -- If empty, then do not produce any analysis results.

  , CruxOptions -> FilePath
bldDir     :: FilePath
    -- ^ Directory for writing files generated from the inputFiles set
    -- (e.g. building C sources into LLVM bitcode files) for analysis.

  , CruxOptions -> Bool
checkPathSat             :: Bool
    -- ^ Should we enable path satisfiability checking?

  , CruxOptions -> Bool
profileCrucibleFunctions :: Bool
  , CruxOptions -> Bool
profileSolver            :: Bool

  , CruxOptions -> Bool
branchCoverage           :: Bool

  , CruxOptions -> PathStrategy
pathStrategy             :: PathStrategy

  , CruxOptions -> Maybe NominalDiffTime
globalTimeout            :: Maybe NominalDiffTime
  , CruxOptions -> Maybe DiffTime
goalTimeout              :: Maybe DiffTime
  , CruxOptions -> NominalDiffTime
profileOutputInterval    :: NominalDiffTime

  , CruxOptions -> Maybe Word64
loopBound                :: Maybe Word64
    -- ^ Should we artifically bound the number of loop iterations

  , CruxOptions -> Maybe Word64
recursionBound           :: Maybe Word64
    -- ^ Should we artifically bound the number of recursive calls to functions?

  , CruxOptions -> Bool
makeCexes                :: Bool
    -- ^ Should we construct counter-example executables

  , CruxOptions -> Bool
unsatCores               :: Bool
    -- ^ Should we attempt to compute unsatisfiable cores for successful
    --   proofs?
  , CruxOptions -> Maybe Word64
getNAbducts               :: Maybe Word64
    -- ^ How many abducts should we get from the solver for sat results?
    --   Only works with cvc5
  , CruxOptions -> FilePath
solver                   :: String
    -- ^ Solver to use to discharge proof obligations
  , CruxOptions -> Maybe FilePath
pathSatSolver            :: Maybe String
    -- ^ A separate solver to use for path satisfiability checking if that
    -- feature is enabled and if the path satisfiability checking solver should
    -- differ from the solver used to discharge proof obligations (default: use
    -- the proof obligation solver)
  , CruxOptions -> Bool
forceOfflineGoalSolving  :: Bool
    -- ^ Force goals to be verified using an offline solver instance, even if it
    -- would have been possible to use the same solver in online mode

  , CruxOptions -> Maybe FilePath
pathSatSolverOutput      :: Maybe FilePath
    -- ^ The file to store the interaction session between the path
    -- satisfiability checker and the solver (if path satisfiability checking is
    -- enabled)
  , CruxOptions -> Maybe FilePath
onlineSolverOutput       :: Maybe FilePath
    -- ^ The file to store the interaction with the online goal solver (if
    -- solving is being performed online)
  , CruxOptions -> Maybe FilePath
offlineSolverOutput      :: Maybe FilePath
    -- ^ A template to use for files to store interactions with offline goal
    -- solvers (if solving is being performed offline).

  , CruxOptions -> Bool
yicesMCSat               :: Bool
    -- ^ Should the MC-SAT Yices solver be enabled (disables unsat cores; default: no)

  , CruxOptions -> FilePath
floatMode                :: String
    -- ^ Tells the solver which representation to use for floating point values.

  , CruxOptions -> Bool
proofGoalsFailFast       :: Bool
    -- ^ If true, stop attempting to prove goals as soon as one is disproved

  , CruxOptions -> Bool
skipReport               :: Bool
    -- ^ Don't produce the HTML reports that describe the verification task

  , CruxOptions -> Bool
skipSuccessReports       :: Bool
    -- ^ Skip reporting on successful proof obligations

  , CruxOptions -> Bool
skipIncompleteReports    :: Bool
    -- ^ Skip reporting on goals that arise from resource exhaustion

  , CruxOptions -> Bool
hashConsing              :: Bool
    -- ^ Turn on hash-consing in the symbolic expression backend

  , CruxOptions -> ProblemFeatures
onlineProblemFeatures    :: ProblemFeatures
    -- ^ Problem Features to force in online solvers

  , CruxOptions -> OutputOptions
outputOptions            :: OutputOptions
    -- ^ Output options grouped together for easy transfer to the logger

  }
  deriving ((forall x. CruxOptions -> Rep CruxOptions x)
-> (forall x. Rep CruxOptions x -> CruxOptions)
-> Generic CruxOptions
forall x. Rep CruxOptions x -> CruxOptions
forall x. CruxOptions -> Rep CruxOptions x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CruxOptions -> Rep CruxOptions x
from :: forall x. CruxOptions -> Rep CruxOptions x
$cto :: forall x. Rep CruxOptions x -> CruxOptions
to :: forall x. Rep CruxOptions x -> CruxOptions
Generic)



cruxOptions :: Config CruxOptions
cruxOptions :: Config CruxOptions
cruxOptions = Config
  { cfgFile :: SectionsSpec CruxOptions
cfgFile =
       do [FilePath]
inputFiles <-
            Text
-> ValueSpec [FilePath]
-> [FilePath]
-> Text
-> SectionsSpec [FilePath]
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"files" (ValueSpec FilePath -> ValueSpec [FilePath]
forall a. ValueSpec a -> ValueSpec [a]
oneOrList ValueSpec FilePath
fileSpec) []
            Text
"Input files to process."

          FilePath
outDir <-
            Text
-> ValueSpec FilePath -> FilePath -> Text -> SectionsSpec FilePath
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"output-directory" ValueSpec FilePath
dirSpec FilePath
""
            Text
"Save results in this directory."

          FilePath
bldDir <-
            Text
-> ValueSpec FilePath -> FilePath -> Text -> SectionsSpec FilePath
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"build-dir" ValueSpec FilePath
dirSpec FilePath
"crux-build"
            Text
"Directory in which to create files generated from the inputFiles."

          Bool
checkPathSat <-
            Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"path-sat" ValueSpec Bool
yesOrNoSpec Bool
False
            Text
"Enable path satisfiability checking (default: no)."

          Bool
profileCrucibleFunctions <-
            Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"profile-crucible" ValueSpec Bool
yesOrNoSpec Bool
False
            Text
"Profile crucible function entry/exit. (default: no)"

          Bool
profileSolver <-
            Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"profile-solver" ValueSpec Bool
yesOrNoSpec Bool
False
            Text
"Profile solver events. (default: no)"

          Bool
branchCoverage <-
            Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"branch-coverage" ValueSpec Bool
yesOrNoSpec Bool
False
            Text
"Record branch coverage information. (default: no)"

          NominalDiffTime
profileOutputInterval <-
            Text
-> ValueSpec NominalDiffTime
-> NominalDiffTime
-> Text
-> SectionsSpec NominalDiffTime
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"profiling-period" ValueSpec NominalDiffTime
forall a. Fractional a => ValueSpec a
fractionalSpec NominalDiffTime
5
            Text
"Time between intermediate profile data reports (default: 5 seconds)"

          Maybe NominalDiffTime
globalTimeout <-
            Text
-> ValueSpec NominalDiffTime
-> Text
-> SectionsSpec (Maybe NominalDiffTime)
forall a. Text -> ValueSpec a -> Text -> SectionsSpec (Maybe a)
sectionMaybe Text
"timeout" ValueSpec NominalDiffTime
forall a. Fractional a => ValueSpec a
fractionalSpec
            Text
"Stop executing the simulator after this many seconds."

          Maybe DiffTime
goalTimeout <-
            Text -> ValueSpec DiffTime -> Text -> SectionsSpec (Maybe DiffTime)
forall a. Text -> ValueSpec a -> Text -> SectionsSpec (Maybe a)
sectionMaybe Text
"goal-timeout" ValueSpec DiffTime
forall a. Fractional a => ValueSpec a
fractionalSpec
            Text
"Stop trying to prove a goal after this many seconds."

          Maybe Word64
loopBound <-
            Text -> ValueSpec Word64 -> Text -> SectionsSpec (Maybe Word64)
forall a. Text -> ValueSpec a -> Text -> SectionsSpec (Maybe a)
sectionMaybe Text
"iteration-bound" ValueSpec Word64
forall a. Num a => ValueSpec a
numSpec
            Text
"Bound all loops to at most this many iterations."

          Maybe Word64
recursionBound <-
            Text -> ValueSpec Word64 -> Text -> SectionsSpec (Maybe Word64)
forall a. Text -> ValueSpec a -> Text -> SectionsSpec (Maybe a)
sectionMaybe Text
"recursion-bound" ValueSpec Word64
forall a. Num a => ValueSpec a
numSpec
            Text
"Bound the number of recursive calls to at most this many calls."

          PathStrategy
pathStrategy <-
            Text
-> ValueSpec PathStrategy
-> PathStrategy
-> Text
-> SectionsSpec PathStrategy
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"path-strategy" ValueSpec PathStrategy
pathStrategySpec PathStrategy
AlwaysMergePaths
            Text
"Simulator strategy for path exploration."

          Bool
makeCexes <-
            Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"make-executables" ValueSpec Bool
yesOrNoSpec Bool
True
            Text
"Should we generate counter-example executables. (default: yes)"

          Bool
unsatCores <-
            Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"unsat-cores" ValueSpec Bool
yesOrNoSpec Bool
True
            Text
"Should we attempt to compute unsatisfiable cores for successfult proofs (default: yes)"

          Maybe Word64
getNAbducts <-
            Text -> ValueSpec Word64 -> Text -> SectionsSpec (Maybe Word64)
forall a. Text -> ValueSpec a -> Text -> SectionsSpec (Maybe a)
sectionMaybe Text
"get-abducts" ValueSpec Word64
forall a. Num a => ValueSpec a
numSpec
            Text
"How many abducts should we get from the solver for sat results? Only works with cvc5, 0 otherwise."
          FilePath
solver <-
            Text
-> ValueSpec FilePath -> FilePath -> Text -> SectionsSpec FilePath
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"solver" ValueSpec FilePath
stringSpec FilePath
"yices"
            (FilePath -> Text
pack (FilePath -> Text) -> FilePath -> Text
forall a b. (a -> b) -> a -> b
$ FilePath
"Select the solver to use to discharge proof obligations. " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
             FilePath
"May be a single solver, a comma-separated list of solvers, or the string \"all\". " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
             FilePath
"Specifying multiple solvers requires the --force-offline-goal-solving option. " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
             FilePath
"(default: \"yices\")")

          Maybe FilePath
pathSatSolver <-
            Text -> ValueSpec FilePath -> Text -> SectionsSpec (Maybe FilePath)
forall a. Text -> ValueSpec a -> Text -> SectionsSpec (Maybe a)
sectionMaybe Text
"path-sat-solver" ValueSpec FilePath
stringSpec
            Text
"Select the solver to use for path satisfiability checking (if different from `solver` and required by the `path-sat` option). (default: use `solver`)"

          Bool
forceOfflineGoalSolving <-
            Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"force-offline-goal-solving" ValueSpec Bool
yesOrNoSpec Bool
False
            Text
"Force goals to be solved using an offline solver, even if the selected solver could have been used in online mode (default: no)"

          Maybe FilePath
pathSatSolverOutput <-
            Text -> ValueSpec FilePath -> Text -> SectionsSpec (Maybe FilePath)
forall a. Text -> ValueSpec a -> Text -> SectionsSpec (Maybe a)
sectionMaybe Text
"path-sat-solver-output" ValueSpec FilePath
stringSpec
            Text
"The file to store the interaction with the path satisfiability solver (if enabled and different from the main solver) (default: none)"

          Maybe FilePath
onlineSolverOutput <-
            Text -> ValueSpec FilePath -> Text -> SectionsSpec (Maybe FilePath)
forall a. Text -> ValueSpec a -> Text -> SectionsSpec (Maybe a)
sectionMaybe Text
"online-solver-output" ValueSpec FilePath
stringSpec
            Text
"The file to store the interaction with the online goal solver (if any) (default: none)"

          Maybe FilePath
offlineSolverOutput <-
            Text -> ValueSpec FilePath -> Text -> SectionsSpec (Maybe FilePath)
forall a. Text -> ValueSpec a -> Text -> SectionsSpec (Maybe a)
sectionMaybe Text
"offine-solver-output" ValueSpec FilePath
stringSpec
            (FilePath -> Text
pack FilePath
offlineSolverOutputHelp)

          Int
simVerbose <-
            Text -> ValueSpec Int -> Int -> Text -> SectionsSpec Int
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"sim-verbose" ValueSpec Int
forall a. Num a => ValueSpec a
numSpec Int
1
            Text
"Verbosity of simulators. (default: 1)"

          Bool
yicesMCSat <-
            Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"mcsat" ValueSpec Bool
yesOrNoSpec Bool
False
            Text
"Enable the MC-SAT solver in Yices (disables unsat cores) (default: no)"

          FilePath
floatMode <-
            Text
-> ValueSpec FilePath -> FilePath -> Text -> SectionsSpec FilePath
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"floating-point" ValueSpec FilePath
stringSpec FilePath
"default"
            (FilePath -> Text
pack (FilePath -> Text) -> FilePath -> Text
forall a b. (a -> b) -> a -> b
$ FilePath
"Select floating point representation,"
             FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" i.e. one of [real|ieee|uninterpreted|default]. "
             FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"Default representation is solver specific: [cvc4|yices]=>real, z3=>ieee.")

          Bool
hashConsing <-
            Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"hash-consing" ValueSpec Bool
yesOrNoSpec Bool
False
            Text
"Enable hash-consing in the symbolic expression backend"

          Bool
printFailures <-
            Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"print-failures" ValueSpec Bool
yesOrNoSpec Bool
True
            Text
"Print error messages regarding failed verification goals"

          Bool
printSymbolicVars <-
            Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"print-symbolic-vars" ValueSpec Bool
yesOrNoSpec Bool
False
            (Text
"Print values assigned to symbolic variables " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>
             Text
"when printing failed verification goals")

          Bool
skipReport <-
            Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"skip-report" ValueSpec Bool
yesOrNoSpec Bool
False
            Text
"Skip producing the HTML report after verification"

          Bool
skipSuccessReports <-
            Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"skip-success-reports" ValueSpec Bool
yesOrNoSpec Bool
False
            Text
"Skip reporting on successful proof obligations"

          Bool
skipIncompleteReports <-
            Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"skip-incomplete-reports" ValueSpec Bool
yesOrNoSpec Bool
False
            Text
"Skip reporting on proof obligations that arise from timeouts and resource exhaustion"

          Bool
noColors <-
            Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"no-colors" ValueSpec Bool
yesOrNoSpec Bool
False
            Text
"Suppress color codes in both the output and the errors"

          Bool
noColorsErr <-
            Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"no-colors-err" ValueSpec Bool
yesOrNoSpec Bool
False
            Text
"Suppress color codes in the errors"

          Bool
noColorsOut <-
            Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"no-colors-out" ValueSpec Bool
yesOrNoSpec Bool
False
            Text
"Suppress color codes in the output"

          Bool
quietMode <-
            Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"quiet-mode" ValueSpec Bool
yesOrNoSpec Bool
False
            Text
"If true, produce minimal output"

          Bool
proofGoalsFailFast <-
            Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"proof-goals-fail-fast" ValueSpec Bool
yesOrNoSpec Bool
False
            Text
"If true, stop attempting to prove goals as soon as one of them is disproved"

          ProblemFeatures
onlineProblemFeatures <- ProblemFeatures -> SectionsSpec ProblemFeatures
forall a. a -> SectionsSpec a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ProblemFeatures
noFeatures

          pure CruxOptions
            { outputOptions :: OutputOptions
outputOptions = OutputOptions
              { colorOptions :: ColorOptions
colorOptions = ColorOptions
                { noColorsErr :: Bool
noColorsErr = Bool
noColorsErr Bool -> Bool -> Bool
|| Bool
noColors
                , noColorsOut :: Bool
noColorsOut = Bool
noColorsOut Bool -> Bool -> Bool
|| Bool
noColors
                },
                Bool
Int
printFailures :: Bool
printSymbolicVars :: Bool
simVerbose :: Int
quietMode :: Bool
simVerbose :: Int
printFailures :: Bool
printSymbolicVars :: Bool
quietMode :: Bool
..
              },
              Bool
FilePath
[FilePath]
Maybe FilePath
Maybe Word64
Maybe DiffTime
Maybe NominalDiffTime
NominalDiffTime
ProblemFeatures
PathStrategy
pathStrategy :: PathStrategy
profileCrucibleFunctions :: Bool
branchCoverage :: Bool
checkPathSat :: Bool
bldDir :: FilePath
inputFiles :: [FilePath]
outDir :: FilePath
profileSolver :: Bool
globalTimeout :: Maybe NominalDiffTime
goalTimeout :: Maybe DiffTime
profileOutputInterval :: NominalDiffTime
loopBound :: Maybe Word64
recursionBound :: Maybe Word64
makeCexes :: Bool
unsatCores :: Bool
getNAbducts :: Maybe Word64
solver :: FilePath
pathSatSolver :: Maybe FilePath
forceOfflineGoalSolving :: Bool
pathSatSolverOutput :: Maybe FilePath
onlineSolverOutput :: Maybe FilePath
offlineSolverOutput :: Maybe FilePath
yicesMCSat :: Bool
floatMode :: FilePath
proofGoalsFailFast :: Bool
skipReport :: Bool
skipSuccessReports :: Bool
skipIncompleteReports :: Bool
hashConsing :: Bool
onlineProblemFeatures :: ProblemFeatures
inputFiles :: [FilePath]
outDir :: FilePath
bldDir :: FilePath
checkPathSat :: Bool
profileCrucibleFunctions :: Bool
profileSolver :: Bool
branchCoverage :: Bool
profileOutputInterval :: NominalDiffTime
globalTimeout :: Maybe NominalDiffTime
goalTimeout :: Maybe DiffTime
loopBound :: Maybe Word64
recursionBound :: Maybe Word64
pathStrategy :: PathStrategy
makeCexes :: Bool
unsatCores :: Bool
getNAbducts :: Maybe Word64
solver :: FilePath
pathSatSolver :: Maybe FilePath
forceOfflineGoalSolving :: Bool
pathSatSolverOutput :: Maybe FilePath
onlineSolverOutput :: Maybe FilePath
offlineSolverOutput :: Maybe FilePath
yicesMCSat :: Bool
floatMode :: FilePath
hashConsing :: Bool
skipReport :: Bool
skipSuccessReports :: Bool
skipIncompleteReports :: Bool
proofGoalsFailFast :: Bool
onlineProblemFeatures :: ProblemFeatures
..
            }


  , cfgEnv :: [EnvDescr CruxOptions]
cfgEnv =
      [
        FilePath
-> FilePath
-> (FilePath -> OptSetter CruxOptions)
-> EnvDescr CruxOptions
forall opts.
FilePath
-> FilePath -> (FilePath -> OptSetter opts) -> EnvDescr opts
EnvVar FilePath
"BLDDIR" FilePath
"Directory for writing build files generated from the input files."
        ((FilePath -> OptSetter CruxOptions) -> EnvDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> EnvDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \FilePath
v CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { bldDir = v }
      ]

  , cfgCmdLineFlag :: [OptDescr CruxOptions]
cfgCmdLineFlag =

      [ FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option FilePath
"d" [FilePath
"sim-verbose"]
        FilePath
"Set simulator verbosity level."
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"NUM" ((FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (Int -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a opts.
(Read a, Num a, Ord a) =>
FilePath -> (a -> opts -> opts) -> FilePath -> OptSetter opts
parsePosNum FilePath
"NUM" ((Int -> CruxOptions -> CruxOptions)
 -> FilePath -> OptSetter CruxOptions)
-> (Int -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a b. (a -> b) -> a -> b
$ \Int
v -> ASetter CruxOptions CruxOptions Int Int
-> Int -> CruxOptions -> CruxOptions
forall s t a b. ASetter s t a b -> b -> s -> t
set (forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"outputOptions" ((OutputOptions -> Identity OutputOptions)
 -> CruxOptions -> Identity CruxOptions)
-> ((Int -> Identity Int)
    -> OutputOptions -> Identity OutputOptions)
-> ASetter CruxOptions CruxOptions Int Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"simVerbose") Int
v

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"path-sat"]
        FilePath
"Enable path satisfiability checking"
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { checkPathSat = True }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"output-directory"]
        FilePath
"Location for reports. If unset, no reports will be generated."
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"DIR" ((FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \FilePath
v CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { outDir = v }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"profile-crucible"]
        FilePath
"Enable profiling of crucible function entry/exit"
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { profileCrucibleFunctions = True }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"profile-solver"]
        FilePath
"Enable profiling of solver events"
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { profileSolver = True }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"branch-coverage"]
        FilePath
"Record branch coverage information"
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { branchCoverage = True }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option FilePath
"t" [FilePath
"timeout"]
        FilePath
"Stop executing the simulator after this many seconds (default: 60)"
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (Maybe FilePath -> OptSetter CruxOptions)
-> ArgDescr CruxOptions
forall a. FilePath -> (Maybe FilePath -> OptSetter a) -> ArgDescr a
OptArg FilePath
"SECS"
        ((Maybe FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (Maybe FilePath -> OptSetter CruxOptions)
-> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions)
-> Maybe FilePath
-> OptSetter CruxOptions
forall opts.
FilePath
-> (FilePath -> OptSetter opts) -> Maybe FilePath -> OptSetter opts
dflt FilePath
"60"
        ((FilePath -> OptSetter CruxOptions)
 -> Maybe FilePath -> OptSetter CruxOptions)
-> (FilePath -> OptSetter CruxOptions)
-> Maybe FilePath
-> OptSetter CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (NominalDiffTime -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall opts.
FilePath
-> (NominalDiffTime -> opts -> opts) -> FilePath -> OptSetter opts
parseNominalDiffTime FilePath
"seconds"
        ((NominalDiffTime -> CruxOptions -> CruxOptions)
 -> FilePath -> OptSetter CruxOptions)
-> (NominalDiffTime -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a b. (a -> b) -> a -> b
$ \NominalDiffTime
v CruxOptions
opts -> CruxOptions
opts { globalTimeout = Just v }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"goal-timeout"]
        FilePath
"Stop trying to prove each goal after this many seconds (default: 10)."
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (Maybe FilePath -> OptSetter CruxOptions)
-> ArgDescr CruxOptions
forall a. FilePath -> (Maybe FilePath -> OptSetter a) -> ArgDescr a
OptArg FilePath
"SECS"
        ((Maybe FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (Maybe FilePath -> OptSetter CruxOptions)
-> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions)
-> Maybe FilePath
-> OptSetter CruxOptions
forall opts.
FilePath
-> (FilePath -> OptSetter opts) -> Maybe FilePath -> OptSetter opts
dflt FilePath
"10"
        ((FilePath -> OptSetter CruxOptions)
 -> Maybe FilePath -> OptSetter CruxOptions)
-> (FilePath -> OptSetter CruxOptions)
-> Maybe FilePath
-> OptSetter CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (DiffTime -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall opts.
FilePath
-> (DiffTime -> opts -> opts) -> FilePath -> OptSetter opts
parseDiffTime FilePath
"seconds"
        ((DiffTime -> CruxOptions -> CruxOptions)
 -> FilePath -> OptSetter CruxOptions)
-> (DiffTime -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a b. (a -> b) -> a -> b
$ \DiffTime
v CruxOptions
opts -> CruxOptions
opts { goalTimeout = Just v }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option FilePath
"" [FilePath
"path-strategy"]
        FilePath
"Strategy to use for exploring paths ('always-merge' or 'split-dfs')"
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"strategy"
        ((FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ (PathStrategy -> CruxOptions -> CruxOptions)
-> FilePath -> OptSetter CruxOptions
forall opts.
(PathStrategy -> opts -> opts) -> FilePath -> OptSetter opts
parsePathStrategy
        ((PathStrategy -> CruxOptions -> CruxOptions)
 -> FilePath -> OptSetter CruxOptions)
-> (PathStrategy -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a b. (a -> b) -> a -> b
$ \PathStrategy
strat CruxOptions
opts -> CruxOptions
opts{ pathStrategy = strat }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option FilePath
"p" [FilePath
"profiling-period"]
        FilePath
"Time between intermediate profile data reports (default: 5 seconds)"
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (Maybe FilePath -> OptSetter CruxOptions)
-> ArgDescr CruxOptions
forall a. FilePath -> (Maybe FilePath -> OptSetter a) -> ArgDescr a
OptArg FilePath
"SECS"
        ((Maybe FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (Maybe FilePath -> OptSetter CruxOptions)
-> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions)
-> Maybe FilePath
-> OptSetter CruxOptions
forall opts.
FilePath
-> (FilePath -> OptSetter opts) -> Maybe FilePath -> OptSetter opts
dflt FilePath
"5"
        ((FilePath -> OptSetter CruxOptions)
 -> Maybe FilePath -> OptSetter CruxOptions)
-> (FilePath -> OptSetter CruxOptions)
-> Maybe FilePath
-> OptSetter CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (NominalDiffTime -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall opts.
FilePath
-> (NominalDiffTime -> opts -> opts) -> FilePath -> OptSetter opts
parseNominalDiffTime FilePath
"seconds"
        ((NominalDiffTime -> CruxOptions -> CruxOptions)
 -> FilePath -> OptSetter CruxOptions)
-> (NominalDiffTime -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a b. (a -> b) -> a -> b
$ \NominalDiffTime
v CruxOptions
opts -> CruxOptions
opts { profileOutputInterval = v }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option FilePath
"i" [FilePath
"iteration-bound"]
        FilePath
"Bound all loops to at most this many iterations"
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"ITER"
        ((FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (Word64 -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a opts.
(Read a, Num a, Ord a) =>
FilePath -> (a -> opts -> opts) -> FilePath -> OptSetter opts
parsePosNum FilePath
"iterations"
        ((Word64 -> CruxOptions -> CruxOptions)
 -> FilePath -> OptSetter CruxOptions)
-> (Word64 -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a b. (a -> b) -> a -> b
$ \Word64
v CruxOptions
opts -> CruxOptions
opts { loopBound = Just v }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option FilePath
"r" [FilePath
"recursion-bound"]
        FilePath
"Bound all recursive calls to at most this many calls"
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"CALLS"
        ((FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (Word64 -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a opts.
(Read a, Num a, Ord a) =>
FilePath -> (a -> opts -> opts) -> FilePath -> OptSetter opts
parsePosNum FilePath
"calls"
        ((Word64 -> CruxOptions -> CruxOptions)
 -> FilePath -> OptSetter CruxOptions)
-> (Word64 -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a b. (a -> b) -> a -> b
$ \Word64
v CruxOptions
opts -> CruxOptions
opts { recursionBound = Just v }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option FilePath
"x" [FilePath
"no-execs"]
        FilePath
"Disable generating counter-example executables"
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { makeCexes = False }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"no-unsat-cores"]
        FilePath
"Disable computing unsat cores for successful proofs"
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { unsatCores = False }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option FilePath
"n" [FilePath
"get-abducts"]
        FilePath
"Get these many abducts. Only works with cvc5, 0 otherwise."
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"ABDUCTS"
        ((FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (Word64 -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a opts.
(Read a, Num a, Ord a) =>
FilePath -> (a -> opts -> opts) -> FilePath -> OptSetter opts
parsePosNum FilePath
"abducts"
        ((Word64 -> CruxOptions -> CruxOptions)
 -> FilePath -> OptSetter CruxOptions)
-> (Word64 -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a b. (a -> b) -> a -> b
$ \Word64
v CruxOptions
opts -> CruxOptions
opts { getNAbducts = Just v }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option FilePath
"s" [FilePath
"solver"]
        (FilePath
"Select the solver to use to discharge proof obligations. " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
         FilePath
"May be a single solver, a comma-separated list of solvers, or the string \"all\". " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
         FilePath
"Specifying multiple solvers requires the --force-offline-goal-solving option. " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
         FilePath
"(default: \"yices\")")
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"SOLVER" ((FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \FilePath
v CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { solver = map toLower v }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"path-sat-solver"]
        FilePath
"Select the solver to use for path satisfiability checking (if different from `solver` and required by the `path-sat` option). (default: use `solver`)"
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (Maybe FilePath -> OptSetter CruxOptions)
-> ArgDescr CruxOptions
forall a. FilePath -> (Maybe FilePath -> OptSetter a) -> ArgDescr a
OptArg FilePath
"SOLVER" ((Maybe FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (Maybe FilePath -> OptSetter CruxOptions)
-> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \Maybe FilePath
ms CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { pathSatSolver = ms }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"force-offline-goal-solving"]
        FilePath
"Force goals to be solved using an offline solver, even if the selected solver could have been used in online mode (default: no)"
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { forceOfflineGoalSolving = True }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"path-sat-solver-output"]
        FilePath
"The file to store the interaction with the path satisfiability solver (if enabled and different from the main solver) (default: none)"
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"FILE" ((FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \FilePath
f CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { pathSatSolverOutput = Just f }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"online-solver-output"]
        FilePath
"The file to store the interaction with the online goal solver (if any) (default: none)"
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"FILE" ((FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \FilePath
f CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { onlineSolverOutput = Just f }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"offline-solver-output"]
        FilePath
offlineSolverOutputHelp
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"FILE" ((FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \FilePath
f CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { offlineSolverOutput = Just f }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"mcsat"]
        FilePath
"Enable the MC-SAT solver in Yices (disables unsat cores)"
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { yicesMCSat = True }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"skip-report"]
        FilePath
"Skip producing the HTML report following verificaion"
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { skipReport = True }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"skip-success-reports"]
        FilePath
"Skip reporting on successful proof obligations"
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { skipSuccessReports = True }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"skip-incomplete-reports"]
        FilePath
"Skip reporting on proof obligations that arise from timeouts and resource exhaustion"
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { skipIncompleteReports = True }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"hash-consing"]
        FilePath
"Enable hash-consing in the symbolic expression backend"
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts{ hashConsing = True }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"skip-print-failures"]
        FilePath
"Skip printing messages related to failed verification goals"
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions
forall a b. b -> Either a b
Right OptSetter CruxOptions
-> (CruxOptions -> CruxOptions) -> OptSetter CruxOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter CruxOptions CruxOptions Bool Bool
-> Bool -> CruxOptions -> CruxOptions
forall s t a b. ASetter s t a b -> b -> s -> t
set (forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"outputOptions" ((OutputOptions -> Identity OutputOptions)
 -> CruxOptions -> Identity CruxOptions)
-> ((Bool -> Identity Bool)
    -> OutputOptions -> Identity OutputOptions)
-> ASetter CruxOptions CruxOptions Bool Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"printFailures") Bool
False

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"fail-fast"]
        FilePath
"Stop attempting to prove goals as soon as one of them is disproved"
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { proofGoalsFailFast = True }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option FilePath
"q" [FilePath
"quiet"]
        FilePath
"Quiet mode; produce minimal output"
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions
forall a b. b -> Either a b
Right OptSetter CruxOptions
-> (CruxOptions -> CruxOptions) -> OptSetter CruxOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter CruxOptions CruxOptions Bool Bool
-> Bool -> CruxOptions -> CruxOptions
forall s t a b. ASetter s t a b -> b -> s -> t
set (forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"outputOptions" ((OutputOptions -> Identity OutputOptions)
 -> CruxOptions -> Identity CruxOptions)
-> ((Bool -> Identity Bool)
    -> OutputOptions -> Identity OutputOptions)
-> ASetter CruxOptions CruxOptions Bool Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"quietMode") Bool
True

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option FilePath
"f" [FilePath
"floating-point"]
        (FilePath
"Select floating point representation,"
         FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" i.e. one of [real|ieee|uninterpreted|default]. "
         FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"Default representation is solver specific: [cvc4|yices]=>real, z3=>ieee.")
        (ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"FPREP" ((FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \FilePath
v CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { floatMode = map toLower v }
      ]
  }

offlineSolverOutputHelp :: String
offlineSolverOutputHelp :: FilePath
offlineSolverOutputHelp = [FilePath] -> FilePath
unlines
  [ FilePath
"A template to use for files to store interactions with offline goal solvers"
  , FilePath
"(if any) (default: none). For example, if the template is `offline-output.smt2`,"
  , FilePath
"then each file will be named `offline-output-<goal number>-<solver name>.smt2,"
  , FilePath
"where <goal number> is the number of the goal that was proven (starting at 0)"
  , FilePath
"and <solver name> is the name of the solver used to dispatch that goal."
  ]

dflt :: String -> (String -> OptSetter opts) -> (Maybe String -> OptSetter opts)
dflt :: forall opts.
FilePath
-> (FilePath -> OptSetter opts) -> Maybe FilePath -> OptSetter opts
dflt FilePath
x FilePath -> OptSetter opts
p Maybe FilePath
mb = FilePath -> OptSetter opts
p (FilePath -> Maybe FilePath -> FilePath
forall a. a -> Maybe a -> a
fromMaybe FilePath
x Maybe FilePath
mb)

parseDiffTime ::
  String -> (DiffTime -> opts -> opts) -> String -> OptSetter opts
parseDiffTime :: forall opts.
FilePath
-> (DiffTime -> opts -> opts) -> FilePath -> OptSetter opts
parseDiffTime FilePath
thing DiffTime -> opts -> opts
mk =
  FilePath -> (Double -> opts -> opts) -> FilePath -> OptSetter opts
forall a opts.
(Read a, Num a, Ord a) =>
FilePath -> (a -> opts -> opts) -> FilePath -> OptSetter opts
parsePosNum FilePath
thing (\Double
a opts
opts -> DiffTime -> opts -> opts
mk (Double -> DiffTime
cvt Double
a) opts
opts)
  where cvt :: Double -> DiffTime
        cvt :: Double -> DiffTime
cvt = Rational -> DiffTime
forall a. Fractional a => Rational -> a
fromRational (Rational -> DiffTime)
-> (Double -> Rational) -> Double -> DiffTime
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Rational
forall a. Real a => a -> Rational
toRational

parseNominalDiffTime ::
  String -> (NominalDiffTime -> opts -> opts) -> String -> OptSetter opts
parseNominalDiffTime :: forall opts.
FilePath
-> (NominalDiffTime -> opts -> opts) -> FilePath -> OptSetter opts
parseNominalDiffTime FilePath
thing NominalDiffTime -> opts -> opts
mk =
  FilePath -> (Double -> opts -> opts) -> FilePath -> OptSetter opts
forall a opts.
(Read a, Num a, Ord a) =>
FilePath -> (a -> opts -> opts) -> FilePath -> OptSetter opts
parsePosNum FilePath
thing (\Double
a opts
opts -> NominalDiffTime -> opts -> opts
mk (Double -> NominalDiffTime
cvt Double
a) opts
opts)
  where cvt :: Double -> NominalDiffTime
        cvt :: Double -> NominalDiffTime
cvt = Rational -> NominalDiffTime
forall a. Fractional a => Rational -> a
fromRational (Rational -> NominalDiffTime)
-> (Double -> Rational) -> Double -> NominalDiffTime
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Rational
forall a. Real a => a -> Rational
toRational

parsePathStrategy ::
  (PathStrategy -> opts -> opts) -> String -> OptSetter opts
parsePathStrategy :: forall opts.
(PathStrategy -> opts -> opts) -> FilePath -> OptSetter opts
parsePathStrategy PathStrategy -> opts -> opts
mk FilePath
"always-merge" opts
opts = opts -> Either FilePath opts
forall a b. b -> Either a b
Right (opts -> Either FilePath opts) -> opts -> Either FilePath opts
forall a b. (a -> b) -> a -> b
$ PathStrategy -> opts -> opts
mk PathStrategy
AlwaysMergePaths opts
opts
parsePathStrategy PathStrategy -> opts -> opts
mk FilePath
"split-dfs"    opts
opts = opts -> Either FilePath opts
forall a b. b -> Either a b
Right (opts -> Either FilePath opts) -> opts -> Either FilePath opts
forall a b. (a -> b) -> a -> b
$ PathStrategy -> opts -> opts
mk PathStrategy
SplitAndExploreDepthFirst opts
opts
parsePathStrategy PathStrategy -> opts -> opts
_mk FilePath
nm opts
_opts = FilePath -> Either FilePath opts
forall a b. a -> Either a b
Left (FilePath
"Unknown path strategy: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
forall a. Show a => a -> FilePath
show FilePath
nm)