what4-1.6.3: Solver-agnostic symbolic values support for issuing queries

Copyright | (c) Galois Inc 2015-2020
License | BSD3
Maintainer | Rob Dockins <rdockins@galois.com>
Stability | provisional
Safe Haskell | None
Language | Haskell2010

What4.Config

Contents

- Names of properties
- Option settings
- Defining option styles
  - OptionSetResult
  - Option style templates
- Describing configuration options
- Building and manipulating configurations
- Extracting entire subtrees of the current configuration
- Printing help messages for configuration options
- Verbosity

Description

This module provides access to persistent configuration settings, and is designed for access both by Haskell client code of the What4 library, and by users of the systems ultimately built using the library, for example, from within a user-facing REPL.

Configurations are defined dynamically by combining a collection of configuration option descriptions. This allows disparate modules to define their own configuration options, rather than having to define the options for all modules in a central place. Every configuration option has a name, which consists of a nonempty sequence of period-separated strings. The intention is that option names should conform to a namespace hierarchy both for organizational purposes and to avoid namespace conflicts. For example, the options for an "asdf" module might be named as:

- asdf.widget
- asdf.frob
- asdf.max_bound

At runtime, a configuration consists of a collection of nested finite maps corresponding to the namespace tree of the existing options. A configuration option may be queried or set either by using a raw string representation of the name (see `getOptionSettingFromText`), or by using a `ConfigOption` value (using `getOptionSetting`), which provides a modicum of type-safety over the basic dynamically-typed configuration maps.

Each option is associated with an "option style", which describes the underlying type of the option (e.g., integer, boolean, string, etc.) as well as the allowed settings of that value. In addition, options can take arbitrary actions when their values are changed in the `opt_onset` callback.

Every configuration comes with the built-in `verbosity` configuration option pre-defined. A `Config` value is constructed using the `initialConfig` operation, which should be given the initial verbosity value and a collection of configuration options to install. A configuration may be later extended with additional options by using the `extendConfig` operation.

Example use (assuming you wanted to use the z3 solver):

    import What4.Solver

    setupSolverConfig :: (IsExprBuilder sym) -> sym -> IO ()
    setupSolverConfig sym = do
      let cfg = getConfiguration sym
      extendConfig (solver_adapter_config_options z3Adapter) cfg
      z3PathSetter <- getOptionSetting z3Path
      res <- setOpt z3PathSetter "/usr/bin/z3"
      assert (null res) (return ())

Developer's note: we might want to add the following operations:

- a method for "unsetting" options to restore the default state of an option
- a method for removing options from a configuration altogether (i.e., to undo extendConfig)

Note regarding concurrency: the configuration data structures in this module are implemented using MVars, and may safely be used in a multithreaded way; configuration changes made in one thread will be visible to others in a properly synchronized way. Of course, if one desires to isolate configuration changes in different threads from each other, separate configuration objects are required. The `splitConfig` operation may be useful to partially isolate configuration objects. As noted in the documentation for `opt_onset`, the validation procedures for options should not look up the value of other options, or deadlock may occur.

Synopsis

- data ConfigOption (tp :: BaseType)
- configOption :: forall (tp :: BaseType). BaseTypeRepr tp -> String -> ConfigOption tp
- configOptionType :: forall (tp :: BaseType). ConfigOption tp -> BaseTypeRepr tp
- configOptionName :: forall (tp :: BaseType). ConfigOption tp -> String
- configOptionText :: forall (tp :: BaseType). ConfigOption tp -> Text
- configOptionNameParts :: forall (tp :: BaseType). ConfigOption tp -> [Text]
- data OptionSetting (tp :: BaseType) = OptionSetting {
  - optionSettingName :: ConfigOption tp
  - getOption :: IO (Maybe (ConcreteVal tp))
  - setOption :: ConcreteVal tp -> IO OptionSetResult
  }
- class Opt (tp :: BaseType) a | tp -> a where
  - getMaybeOpt :: OptionSetting tp -> IO (Maybe a)
  - trySetOpt :: OptionSetting tp -> a -> IO OptionSetResult
  - setOpt :: OptionSetting tp -> a -> IO [Doc Void]
  - getOpt :: OptionSetting tp -> IO a
- setUnicodeOpt :: Some OptionSetting -> Text -> IO [Doc Void]
- setIntegerOpt :: Some OptionSetting -> Integer -> IO [Doc Void]
- setBoolOpt :: Some OptionSetting -> Bool -> IO [Doc Void]
- data OptionStyle (tp :: BaseType) = OptionStyle {
  - opt_type :: BaseTypeRepr tp
  - opt_onset :: Maybe (ConcreteVal tp) -> ConcreteVal tp -> IO OptionSetResult
  - opt_help :: Doc Void
  - opt_default_value :: Maybe (ConcreteVal tp)
  }
- set_opt_default :: forall (tp :: BaseType). ConcreteVal tp -> OptionStyle tp -> OptionStyle tp
- set_opt_onset :: forall (tp :: BaseType). (Maybe (ConcreteVal tp) -> ConcreteVal tp -> IO OptionSetResult) -> OptionStyle tp -> OptionStyle tp
- data OptionSetResult = OptionSetResult {
  - optionSetError :: !(Maybe (Doc Void))
  - optionSetWarnings :: !(Seq (Doc Void))
  }
- optOK :: OptionSetResult
- optWarn :: Doc Void -> OptionSetResult
- optErr :: Doc Void -> OptionSetResult
- checkOptSetResult :: forall (tp :: BaseType). OptionSetting tp -> OptionSetResult -> IO [Doc Void]
- data OptSetFailure = OptSetFailure (Some OptionSetting) (Doc Void)
- data OptGetFailure = OptGetFailure OptRef (Doc Void)
- data OptCreateFailure = OptCreateFailure ConfigDesc (Doc Void)
- data Bound r
  - = Exclusive r
  - | Inclusive r
  - | Unbounded
- boolOptSty :: OptionStyle BaseBoolType
- integerOptSty :: OptionStyle BaseIntegerType
- realOptSty :: OptionStyle BaseRealType
- stringOptSty :: OptionStyle (BaseStringType Unicode)
- realWithRangeOptSty :: Bound Rational -> Bound Rational -> OptionStyle BaseRealType
- realWithMinOptSty :: Bound Rational -> OptionStyle BaseRealType
- realWithMaxOptSty :: Bound Rational -> OptionStyle BaseRealType
- integerWithRangeOptSty :: Bound Integer -> Bound Integer -> OptionStyle BaseIntegerType
- integerWithMinOptSty :: Bound Integer -> OptionStyle BaseIntegerType
- integerWithMaxOptSty :: Bound Integer -> OptionStyle BaseIntegerType
- enumOptSty :: Set Text -> OptionStyle (BaseStringType Unicode)
- listOptSty :: Map Text (IO OptionSetResult) -> OptionStyle (BaseStringType Unicode)
- executablePathOptSty :: OptionStyle (BaseStringType Unicode)
- data ConfigDesc
- mkOpt :: forall (tp :: BaseType). ConfigOption tp -> OptionStyle tp -> Maybe (Doc Void) -> Maybe (ConcreteVal tp) -> ConfigDesc
- opt :: forall help (tp :: BaseType). Pretty help => ConfigOption tp -> ConcreteVal tp -> help -> ConfigDesc
- optV :: forall (tp :: BaseType) help. Pretty help => ConfigOption tp -> ConcreteVal tp -> (ConcreteVal tp -> Maybe help) -> help -> ConfigDesc
- optU :: forall help (tp :: BaseType). Pretty help => ConfigOption tp -> help -> ConfigDesc
- optUV :: forall help (tp :: BaseType). Pretty help => ConfigOption tp -> (ConcreteVal tp -> Maybe help) -> help -> ConfigDesc
- copyOpt :: (Text -> Text) -> ConfigDesc -> ConfigDesc
- deprecatedOpt :: [ConfigDesc] -> ConfigDesc -> ConfigDesc
- data Config
- initialConfig :: Integer -> [ConfigDesc] -> IO Config
- extendConfig :: [ConfigDesc] -> Config -> IO ()
- tryExtendConfig :: [ConfigDesc] -> Config -> IO ()
- splitConfig :: Config -> IO Config
- getOptionSetting :: forall (tp :: BaseType). ConfigOption tp -> Config -> IO (OptionSetting tp)
- getOptionSettingFromText :: Text -> Config -> IO (Some OptionSetting)
- data ConfigValue where
  - ConfigValue :: forall (tp :: BaseType). ConfigOption tp -> ConcreteVal tp -> ConfigValue
- getConfigValues :: Text -> Config -> IO [ConfigValue]
- configHelp :: Text -> Config -> IO [Doc Void]
- verbosity :: ConfigOption BaseIntegerType
- verbosityLogger :: Config -> Handle -> IO (Int -> String -> IO ())

# Names of properties

data ConfigOption (tp :: BaseType) Source #

A Haskell-land wrapper around the name of a configuration option. Developers are encouraged to define and use `ConfigOption` values to avoid two classes of errors: typos in configuration option names; and dynamic type-cast failures. Both classes of errors can be lifted to statically-checkable failures (missing symbols and type-checking, respectively) by consistently using `ConfigOption` values.

The following example indicates the suggested usage

      asdfFrob :: ConfigOption BaseRealType
      asdfFrob = configOption BaseRealRepr "asdf.frob"

      asdfMaxBound :: ConfigOption BaseIntegerType
      asdfMaxBound = configOption BaseIntegerRepr "asdf.max_bound"

#### Instances

Instances details

Show (ConfigOption tp) Source # |
Instance details Defined in What4.Config Methods showsPrec :: Int -> ConfigOption tp -> ShowS Source # show :: ConfigOption tp -> String Source # showList :: [ConfigOption tp] -> ShowS Source #

configOption :: forall (tp :: BaseType). BaseTypeRepr tp -> String -> ConfigOption tp Source #

Construct a `ConfigOption` from a string name. Idiomatic usage is to define a single top-level `ConfigOption` value in the module where the option is defined to consistently fix its name and type for all subsequent uses.

configOptionType :: forall (tp :: BaseType). ConfigOption tp -> BaseTypeRepr tp Source #

Retrieve the run-time type representation of `tp`.

configOptionName :: forall (tp :: BaseType). ConfigOption tp -> String Source #

Reconstruct the original string name of this option.

configOptionText :: forall (tp :: BaseType). ConfigOption tp -> Text Source #

Reconstruct the original string name of this option.

configOptionNameParts :: forall (tp :: BaseType). ConfigOption tp -> [Text] Source #

Get the individual dot-separated segments of an option's name.

# Option settings

data OptionSetting (tp :: BaseType) Source #

An `OptionSetting` gives the direct ability to query or set the current value of an option. The `getOption` field is an action that, when executed, fetches the current value of the option, if it is set. The `setOption` method attempts to set the value of the option. If the associated `opt_onset` validation method rejects the option, it will retain its previous value; otherwise it will be set to the given value. In either case, the generated `OptionSetResult` will be returned.

Constructors

OptionSetting |

Fields

- optionSettingName :: ConfigOption tp
- getOption :: IO (Maybe (ConcreteVal tp))
- setOption :: ConcreteVal tp -> IO OptionSetResult

#### Instances

Instances details

ShowF OptionSetting Source # |
Instance details Defined in What4.Config Methods withShow :: forall p q (tp :: BaseType) a. p OptionSetting -> q tp -> (Show (OptionSetting tp) => a) -> a Source # showF :: forall (tp :: BaseType). OptionSetting tp -> String Source # showsPrecF :: forall (tp :: BaseType). Int -> OptionSetting tp -> String -> String Source #
Show (OptionSetting tp) Source # |
Instance details Defined in What4.Config Methods showsPrec :: Int -> OptionSetting tp -> ShowS Source # show :: OptionSetting tp -> String Source # showList :: [OptionSetting tp] -> ShowS Source #

class Opt (tp :: BaseType) a | tp -> a where Source #

A utility class for making working with option settings easier. The `tp` argument is a `BaseType`, and the `a` argument is an associcated Haskell type.

Minimal complete definition

getMaybeOpt, trySetOpt

Methods

getMaybeOpt :: OptionSetting tp -> IO (Maybe a) Source #

Return the current value of the option, as a `Maybe` value.

trySetOpt :: OptionSetting tp -> a -> IO OptionSetResult Source #

Attempt to set the value of an option. Return any errors or warnings.

setOpt :: OptionSetting tp -> a -> IO [Doc Void] Source #

Set the value of an option. Return any generated warnings. Throws an OptSetFailure exception if a validation error occurs.

getOpt :: OptionSetting tp -> IO a Source #

Get the current value of an option. Throw an exception if the option is not currently set.

#### Instances

Instances details

Opt BaseBoolType Bool Source # |
Instance details Defined in What4.Config Methods getMaybeOpt :: OptionSetting BaseBoolType -> IO (Maybe Bool) Source # trySetOpt :: OptionSetting BaseBoolType -> Bool -> IO OptionSetResult Source # setOpt :: OptionSetting BaseBoolType -> Bool -> IO [Doc Void] Source # getOpt :: OptionSetting BaseBoolType -> IO Bool Source #
Opt BaseIntegerType Integer Source # |
Instance details Defined in What4.Config Methods getMaybeOpt :: OptionSetting BaseIntegerType -> IO (Maybe Integer) Source # trySetOpt :: OptionSetting BaseIntegerType -> Integer -> IO OptionSetResult Source # setOpt :: OptionSetting BaseIntegerType -> Integer -> IO [Doc Void] Source # getOpt :: OptionSetting BaseIntegerType -> IO Integer Source #
Opt BaseRealType Rational Source # |
Instance details Defined in What4.Config Methods getMaybeOpt :: OptionSetting BaseRealType -> IO (Maybe Rational) Source # trySetOpt :: OptionSetting BaseRealType -> Rational -> IO OptionSetResult Source # setOpt :: OptionSetting BaseRealType -> Rational -> IO [Doc Void] Source # getOpt :: OptionSetting BaseRealType -> IO Rational Source #
Opt (BaseStringType Unicode) Text Source # |
Instance details Defined in What4.Config Methods getMaybeOpt :: OptionSetting (BaseStringType Unicode) -> IO (Maybe Text) Source # trySetOpt :: OptionSetting (BaseStringType Unicode) -> Text -> IO OptionSetResult Source # setOpt :: OptionSetting (BaseStringType Unicode) -> Text -> IO [Doc Void] Source # getOpt :: OptionSetting (BaseStringType Unicode) -> IO Text Source #

setUnicodeOpt :: Some OptionSetting -> Text -> IO [Doc Void] Source #

Given a unicode text value, set the named option to that value or generate an OptSetFailure exception if the option is not a unicode text valued option.

setIntegerOpt :: Some OptionSetting -> Integer -> IO [Doc Void] Source #

Given an integer value, set the named option to that value or generate an OptSetFailure exception if the option is not an integer valued option.

setBoolOpt :: Some OptionSetting -> Bool -> IO [Doc Void] Source #

Given a boolean value, set the named option to that value or generate an OptSetFailure exception if the option is not a boolean valued option.

# Defining option styles

data OptionStyle (tp :: BaseType) Source #

An option defines some metadata about how a configuration option behaves. It contains a base type representation, which defines the runtime type that is expected for setting and querying this option at runtime.

Constructors

OptionStyle |

Fields

- opt_type :: BaseTypeRepr tp

  base type representation of this option

- opt_onset :: Maybe (ConcreteVal tp) -> ConcreteVal tp -> IO OptionSetResult

  An operation for validating new option values. This action may also be used to take actions whenever an option setting is changed. NOTE! the onset action should not attempt to look up the values of other configuration settings, or deadlock may occur.

  The first argument is the current value of the option (if any). The second argument is the new value that is being set. If the validation fails, the operation should return a result describing why validation failed. Optionally, warnings may also be returned.

- opt_help :: Doc Void

  Documentation for the option to be displayed in the event a user asks for information about this option. This message should contain information relevant to all options in this style (e.g., its type and range of expected values), not necessarily information about a specific option.

- opt_default_value :: Maybe (ConcreteVal tp)

  This gives a default value for the option, if set.

set_opt_default :: forall (tp :: BaseType). ConcreteVal tp -> OptionStyle tp -> OptionStyle tp Source #

Update the `opt_default_value` field.

set_opt_onset :: forall (tp :: BaseType). (Maybe (ConcreteVal tp) -> ConcreteVal tp -> IO OptionSetResult) -> OptionStyle tp -> OptionStyle tp Source #

Update the `opt_onset` field.

## OptionSetResult

data OptionSetResult Source #

When setting the value of an option, a validation function is called (as defined by the associated `OptionStyle`). The result of the validation function is an `OptionSetResult`. If the option value given is invalid for some reason, an error should be returned. Additionally, warning messages may be returned, which will be passed through to the eventual call site attempting to alter the option setting.

Constructors

OptionSetResult |

Fields

- optionSetError :: !(Maybe (Doc Void))
- optionSetWarnings :: !(Seq (Doc Void))

#### Instances

Instances details

Monoid OptionSetResult Source # |
Instance details Defined in What4.Config Methods mempty :: OptionSetResult Source # mappend :: OptionSetResult -> OptionSetResult -> OptionSetResult Source # mconcat :: [OptionSetResult] -> OptionSetResult Source #
Semigroup OptionSetResult Source # |
Instance details Defined in What4.Config Methods (<>) :: OptionSetResult -> OptionSetResult -> OptionSetResult Source # sconcat :: NonEmpty OptionSetResult -> OptionSetResult Source # stimes :: Integral b => b -> OptionSetResult -> OptionSetResult Source #

optOK :: OptionSetResult Source #

Accept the new option value with no errors or warnings.

optWarn :: Doc Void -> OptionSetResult Source #

Accept the given option value, but report a warning message.

optErr :: Doc Void -> OptionSetResult Source #

Reject the new option value with an error message.

checkOptSetResult :: forall (tp :: BaseType). OptionSetting tp -> OptionSetResult -> IO [Doc Void] Source #

Throw an exception if the given `OptionSetResult` indicates an error. Otherwise, return any generated warnings.

data OptSetFailure Source #

Constructors

OptSetFailure (Some OptionSetting) (Doc Void) |

#### Instances

Instances details

Exception OptSetFailure Source # |
Instance details Defined in What4.Config Methods toException :: OptSetFailure -> SomeException Source # fromException :: SomeException -> Maybe OptSetFailure Source # displayException :: OptSetFailure -> String Source # backtraceDesired :: OptSetFailure -> Bool Source #
Show OptSetFailure Source # |
Instance details Defined in What4.Config Methods showsPrec :: Int -> OptSetFailure -> ShowS Source # show :: OptSetFailure -> String Source # showList :: [OptSetFailure] -> ShowS Source #

data OptGetFailure Source #

Constructors

OptGetFailure OptRef (Doc Void) |

#### Instances

Instances details

Exception OptGetFailure Source # |
Instance details Defined in What4.Config Methods toException :: OptGetFailure -> SomeException Source # fromException :: SomeException -> Maybe OptGetFailure Source # displayException :: OptGetFailure -> String Source # backtraceDesired :: OptGetFailure -> Bool Source #
Show OptGetFailure Source # |
Instance details Defined in What4.Config Methods showsPrec :: Int -> OptGetFailure -> ShowS Source # show :: OptGetFailure -> String Source # showList :: [OptGetFailure] -> ShowS Source #

data OptCreateFailure Source #

Constructors

OptCreateFailure ConfigDesc (Doc Void) |

#### Instances

Instances details

Exception OptCreateFailure Source # |
Instance details Defined in What4.Config Methods toException :: OptCreateFailure -> SomeException Source # fromException :: SomeException -> Maybe OptCreateFailure Source # displayException :: OptCreateFailure -> String Source # backtraceDesired :: OptCreateFailure -> Bool Source #
Show OptCreateFailure Source # |
Instance details Defined in What4.Config Methods showsPrec :: Int -> OptCreateFailure -> ShowS Source # show :: OptCreateFailure -> String Source # showList :: [OptCreateFailure] -> ShowS Source #

## Option style templates

data Bound r Source #

An inclusive or exclusive bound.

Constructors

Exclusive r |
Inclusive r |
Unbounded |

boolOptSty :: OptionStyle BaseBoolType Source #

Standard option style for boolean-valued configuration options

integerOptSty :: OptionStyle BaseIntegerType Source #

Standard option style for integral-valued configuration options

realOptSty :: OptionStyle BaseRealType Source #

Standard option style for real-valued configuration options

stringOptSty :: OptionStyle (BaseStringType Unicode) Source #

realWithRangeOptSty :: Bound Rational -> Bound Rational -> OptionStyle BaseRealType Source #

Option style for real-valued options with upper and lower bounds

realWithMinOptSty :: Bound Rational -> OptionStyle BaseRealType Source #

Option style for real-valued options with a lower bound

realWithMaxOptSty :: Bound Rational -> OptionStyle BaseRealType Source #

Option style for real-valued options with an upper bound

integerWithRangeOptSty :: Bound Integer -> Bound Integer -> OptionStyle BaseIntegerType Source #

Option style for integer-valued options with upper and lower bounds

integerWithMinOptSty :: Bound Integer -> OptionStyle BaseIntegerType Source #

Option style for integer-valued options with a lower bound

integerWithMaxOptSty :: Bound Integer -> OptionStyle BaseIntegerType Source #

Option style for integer-valued options with an upper bound

enumOptSty :: Set Text -> OptionStyle (BaseStringType Unicode) Source #

A configuration style for options that must be one of a fixed set of text values

listOptSty :: Map Text (IO OptionSetResult) -> OptionStyle (BaseStringType Unicode) Source #

A configuration syle for options that must be one of a fixed set of text values. Associated with each string is a validation/callback action that will be run whenever the named string option is selected.

executablePathOptSty :: OptionStyle (BaseStringType Unicode) Source #

A configuration style for options that are expected to be paths to an executable image. Configuration options with this style generate a warning message if set to a value that cannot be resolved to an absolute path to an executable file in the current OS environment.

# Describing configuration options

data ConfigDesc Source #

A `ConfigDesc` describes a configuration option before it is installed into a `Config` object. It consists of a `ConfigOption` name for the option, an `OptionStyle` describing the sort of option it is, and an optional help message describing the semantics of this option.

#### Instances

Instances details

Show ConfigDesc Source # |
Instance details Defined in What4.Config Methods showsPrec :: Int -> ConfigDesc -> ShowS Source # show :: ConfigDesc -> String Source # showList :: [ConfigDesc] -> ShowS Source #

mkOpt Source #

Arguments

:: forall (tp :: BaseType). ConfigOption tp | Fixes the name and the type of this option
-> OptionStyle tp | Define the style of this option
-> Maybe (Doc Void) | Help text
-> Maybe (ConcreteVal tp) | A default value for this option
-> ConfigDesc |

The most general method for constructing a normal `ConfigDesc`.

opt Source #

Arguments

:: forall help (tp :: BaseType). Pretty help |
=> ConfigOption tp | Fixes the name and the type of this option
-> ConcreteVal tp | Default value for the option
-> help | An informational message describing this option
-> ConfigDesc |

Construct an option using a default style with a given initial value

optV Source #

Arguments

:: forall (tp :: BaseType) help. Pretty help |
=> ConfigOption tp | Fixes the name and the type of this option
-> ConcreteVal tp | Default value for the option
-> (ConcreteVal tp -> Maybe help) | Validation function. Return `Just err` if the value to set is not valid.
-> help | An informational message describing this option
-> ConfigDesc |

Construct an option using a default style with a given initial value. Also provide a validation function to check new values as they are set.

optU Source #

Arguments

:: forall help (tp :: BaseType). Pretty help |
=> ConfigOption tp | Fixes the name and the type of this option
-> help | An informational message describing this option
-> ConfigDesc |

Construct an option using a default style with no initial value.

optUV Source #

Arguments

:: forall help (tp :: BaseType). Pretty help |
=> ConfigOption tp | Fixes the name and the type of this option
-> (ConcreteVal tp -> Maybe help) | Validation function. Return `Just err` if the value to set is not valid.
-> help | An informational message describing this option
-> ConfigDesc |

Construct an option using a default style with no initial value. Also provide a validation function to check new values as they are set.

copyOpt :: (Text -> Text) -> ConfigDesc -> ConfigDesc Source #

The copyOpt creates a duplicate ConfigDesc under a different name. This is typically used to taking a common operation and modify the prefix to apply it to a more specialized role (e.g. solver.strict_parsing --> solver.z3.strict_parsing). The style and help text of the input ConfigDesc are preserved, but any deprecation is discarded.

deprecatedOpt :: [ConfigDesc] -> ConfigDesc -> ConfigDesc Source #

Used as a wrapper for an option that has been deprecated. If the option is actually set (as opposed to just using the default value) then this will emit an OptionSetResult warning that time, optionally mentioning the replacement option (if specified).

There are three cases of deprecation: 1. Removing an option that no longer applies 2. Changing the name or heirarchical position of an option. 3. #2 and also changing the type. 4. Replacing an option by multiple new options (e.g. split url option into hostname and port options)

In the case of #1, the option will presumably be ignored by the code and the warnings are provided to allow the user to clean the option from their configurations.

In the case of #2, the old option and the new option will share the same value storage: changes to one can be seen via the other and vice versa. The code can be switched over to reference the new option entirely, and user configurations setting the old option will still work until they have been updated and the definition of the old option is removed entirely.

NOTE: in order to support #2, the newer option should be declared (via `insertOption`) *before* the option it deprecates.

In the case of #3, it is not possible to share storage space, so during the deprecation period, the code using the option config value must check both locations and decide which value to utilize.

Case #4 is an enhanced form of #3 and #2, and is generally treated as #3, but adds the consideration that deprecation warnings will need to advise about multiple new options. The inverse of #4 (multiple options being combined to a single newer option) is just treated as separate deprecations.

NOTE: in order to support #4, the newer options should all be declared (via `insertOption`) *before* the options they deprecate.

Nested deprecations are valid, and replacement warnings are automatically transitive to the newest options.

Any user-supplied value for the old option will result in warnings emitted to the OptionSetResult for all four cases. Code should ensure that these warnings are appropriately communicated to the user to allow configuration updates to occur.

Note that for #1 and #2, the overhead burden of continuing to define the deprecated option is very small, so actual removal of the older config can be delayed indefinitely.

# Building and manipulating configurations

data Config Source #

The main configuration datatype. It consists of a Read/Write var containing the actual configuration data.

initialConfig Source #

Arguments

:: Integer | Initial value for the `verbosity` option
-> [ConfigDesc] | Option descriptions to install
-> IO Config |

Construct a new configuration from the given configuration descriptions.

extendConfig :: [ConfigDesc] -> Config -> IO () Source #

Extend an existing configuration with new options. An `OptCreateFailure` exception will be raised if any of the given options clash with options that already exists.

tryExtendConfig :: [ConfigDesc] -> Config -> IO () Source #

Extend an existing configuration with new options. If any of the given options are already present in the configuration, nothing is done for that option and it is silently skipped.

splitConfig :: Config -> IO Config Source #

Create a new configuration object that shares the option settings currently in the given input config. However, any options added to either configuration using `extendConfig` will not be propagated to the other.

Option settings that already exist in the input configuration will be shared between both; changes to those options will be visible in both configurations.

getOptionSetting :: forall (tp :: BaseType). ConfigOption tp -> Config -> IO (OptionSetting tp) Source #

Given a `ConfigOption` name, produce an `OptionSetting` object for accessing and setting the value of that option.

An exception is thrown if the named option cannot be found the `Config` object, or if a type mismatch occurs.

getOptionSettingFromText :: Text -> Config -> IO (Some OptionSetting) Source #

Given a text name, produce an `OptionSetting` object for accessing and setting the value of that option.

An exception is thrown if the named option cannot be found.

# Extracting entire subtrees of the current configuration

data ConfigValue where Source #

A `ConfigValue` bundles together the name of an option with its current value.

Constructors

ConfigValue :: forall (tp :: BaseType). ConfigOption tp -> ConcreteVal tp -> ConfigValue |

#### Instances

Instances details

Pretty ConfigValue Source # |
Instance details Defined in What4.Config Methods pretty :: ConfigValue -> Doc ann Source # prettyList :: [ConfigValue] -> Doc ann Source #

getConfigValues :: Text -> Config -> IO [ConfigValue] Source #

Given the name of a subtree, return all the currently-set configuration values in that subtree.

If the subtree name is empty, the entire tree will be traversed.

# Printing help messages for configuration options

configHelp :: Text -> Config -> IO [Doc Void] Source #

Given the name of a subtree, compute help text for all the options available in that subtree.

If the subtree name is empty, the entire tree will be traversed.

# Verbosity

verbosity :: ConfigOption BaseIntegerType Source #

Verbosity of the simulator. This option controls how much informational and debugging output is generated. 0 yields low information output; 5 is extremely chatty.

verbosityLogger :: Config -> Handle -> IO (Int -> String -> IO ()) Source #

Return an operation that will consult the current value of the verbosity option, and will print a string to the given `Handle` if the provided int is smaller than the current verbosity setting.