Remove the validation options stored in a conclusion. The conclusion will have options stored in it if the client has used setOptions() on that conclusion. After calling this, a future call to getOptions() on the same conclusion will yield undefined.

Remove the validation result stored in a conclusion that has been validated before by one of this module's validation tools. If no validation result was stored there, this function does nothing.

A useful tool for converting pure validation functions into validation tools (that is, functions with the side effect of writing their results into the target object).

For example, let's say you have a function that can take as input any expression in a simple toy system and return a validation result, either { result:'valid', reason:'...' } or { result:'invalid', reason:'...' }. Call this function on it to produce a validation tool that you can install in this module, and that will write its results into the appropriate attribute of any target on which it is called.

For a general description of how validation options work, refer to the documentation for the setOptions() function. Calling this function with no arguments, Validation.getOptions(), returns the full set of module-level options. Calling it with one argument, a conclusion, Validation.getOptions(C), returns just those conclusion-specific options stored in that Expression.

This module stores a collection of validation tools. Each such tool is a function with the following signature:

• Argument 1 is a target LogicConcept to be validated.
• Argument 2 is an options object, which this module guarantees will be the module-level validation options, possibly superceded by any options passed to the validate function, and further possibly overridden by options stored in the target itself.
• The function should store the validation results in the target. If you have a function that just returns validation results instead, you can easily convert it to one that writes its results into the target, using the convenient meta-function functionToTool(). If you are writing your own validation tool, you can write the results into a target using the setResult() function.

Each tool gets stored under a name chosen by the client, so that the tool can be referred to later by this name as a unique ID. Installing another tool later with the same name overwrites the previous.

If this is the first tool installed in this module, it will immediately become the default. You can change this later using the setOptions() function; see its documentation for further details.

This is the corresponding getter function for the installTool() function. Anything installed with that function can later be looked up with this one.

This module is a collection of validation tools, which are installed using the installTool() function, each under a unique name. This function returns that list of unique names.

Read the validation result stored in a conclusion that has been validated before by one of this module's validation tools, and return it, or return undefined if no validation result is stored in the given conclusion.

When validation is performed on a conclusion, using validate(), it will compute the relevant options to be passed to the validation tool as follows. First, look up any options stored in this module, and second, look up any options stored in the conclusion to be validated, overwriting the module-level options with the conclusion-specific ones in the case of any conflicts. The resulting set of options is given to the validate() routine.

This function can be used to change options either at the module level, by calling setOptions( key1, value1, key2, value2, ... ), or for a specific conclusion, by calling setOptions( conclusion, key1, value1, key2, value2, ... ).

Although most options will be specific to the validation tool being used, one essential option that matters in all cases is which validation tool to use for the conclusion. That option has the simple key "tool", so you can set it for a conclusion with code such as Validation.setOptions( conclusion, 'tool', 'tool name here' ). But it is inconvenient to do this for every conclusion in a large LogicConcept, so it is preferable to be able to set a default validation tool that will be used when the conclusion does not specify one. Since module-level options are the defaults or "fallbacks" when a conclusion doesn't have an option specified, just set a module-level tool with code such as Validation.setOptions( 'tool', 'tool name here' ).

Store the results of a validation tool in the conclusion that was validated. Validation results are a JavaScript object amenable to JSON storage, and having the following keys (some optional, some required).

• result - any string representing the validation result, though the only officially supported ones at the moment are "valid" (meaning the user's work is correct), "invalid" (meaning the user's work has a mistake), and "indeterminate" (meaning that Lurch cannot find the answer, perhaps because of limited computing resources or some ambiguity in the user's input)
• reason - any string representing the reason for why the validation result was what it was. We leave it up to the author of the validation tool how to use this attribute, but we recommend using short English phrases as error codes that can be looked up in a larger dictionary of detailed descriptions. For example, you might use "No such reason" or "Too many premises" or any other simple phrase.
• Any other keys in the object are optional, and can be used at the discretion of the author of the validation tool to store whatever other information will help Lurch give helpful feedback to the user.

Example validation result:

{
    "result" : "invalid",
    "reason" : "Too many premises",
    "formula cited" : "conjunction introduction",
    "num premises needed" : 2,
    "num premises cited" : 4
}

This function computes the validation result for any given LogicConcept L and stores it in L's validation attribute. It prioritizes various sets of options as follows.

1. If the options stored in the LogicConcept L itself, obtained by calling Validation.getOptions( L ), give us a validation tool, then we call it on L and store its result in L.
2. Otherwise, if the second parameter to the validation function (an options object) specifies which tool to use, that one is used to compute the result. We call that validation tool and store its result in L.
3. If even that does not specify a tool, we fall back on the global options stored in the Validation module, fetched by calling Validation.getOptions(). If that gives us a validation tool, call it on L and store its result in L.
4. No tool is available, so we store in L a validation result object with result "indeterminate" and reason stating that no validation tool was available for L.

This function computes the validation result afresh every time it is called. See other functions below for how to read cache validation results.