Error-checking
A library of utilities for error checking.
Each error checking function in this library
causes a soft error, with an informative message,
and optionally informative error flag and value,
when certain conditions are not satisified.
These error checking functions are useful, for instance,
to programmatically validate inputs of event macros, providing the informative error messages to the user.
The informative error flags and values are useful
when event macros are invoked programmatically,
to enable the caller to take appropriate actions
based on the nature of the error,
as with an exception mechanism.
Inside b*, the er binder can be used with calls to these error checking functions.
These error checking functions include msgp parameters
to describe the values being checked in error message.
When these functions are called,
the strings in the description parameters
should be capitalized based on where they occur in the error messages.
These error checking functions are being moved
from kestrel/utilities/error-checking/
to kestrel/error-checking,
and are being refactored and improved in the process.
Subtopics
- Def-error-checker
- Generate an error checking function
and an associated macro abbreviation.
- Ensure-function/macro/lambda
- Cause an error if a value is not
the name of an existing function,
the name of an existing macro,
or a lambda expression.
- Ensure-symbol-is-fresh-event-name
- Cause an error if a symbol
cannot be used as the name of a new event of a certain type,
also given that certain symbols will be used as event names.
- Ensure-function/lambda/term-number-of-results
- Cause an error if a function or lambda expression or term
does not have a given number of results.
- Ensure-function/lambda-arity
- Cause an error if a function or lambda expression
does not have a given arity.
- Ensure-function/lambda-no-stobjs
- Cause an error if a function or lambda expression
has input or output stobjs.
- Ensure-function/lambda-guard-verified-fns
- Cause an error if a function or lambda expression is
a non-guard-verified function or
a lambda expression that calls some non-guard-verified function.
- Ensure-function-name-or-numbered-wildcard
- Cause an error if a value is not
either the name of an existing function
or a numbered name
with a wildcard index that
resolves
to the name of an existing function.
- Ensure-function/lambda-logic-mode
- Cause an error if a function or lambda expression is
a function in program mode or
a lambda expression that calls some program-mode function.
- Ensure-function/lambda-closed
- Cause an error if a function or lambda expression is
a non-closed lambda expression.
- Ensure-value-is-untranslated-term
- Cause an error if a value is not a term.
- Ensure-function-number-of-results
- Cause an error if a function does not have a given number of results.
- Ensure-boolean-or-auto-and-return-boolean
- Cause an error if a value is not t, nil, or :auto;
otherwise return a boolean result.
- Ensure-is-hints-specifier
- Cause an error if a value is not a hints specifier.
- Ensure-term-if-call
- Cause an error if a term is not a call of if.
- Ensure-value-is-not-in-list
- Cause an error if a value is a member of a list.
- Ensure-term-free-vars-subset
- Cause an error if a term includes free variables outside a given set.
- Ensure-symbol-new-event-name
- Cause an error if a symbol cannot be the name of a new event.
- Ensure-symbol-different
- Cause an error if a symbol is the same as another symbol.
- Ensure-function/lambda-guard-verified-exec-fns
- Cause an error if a function or lambda expression is
a non-guard-verified function or
a lambda expression that calls some non-guard-verified function,
except possibly in the :logic subterms of mbes.
- Ensure-value-is-in-list
- Cause an error if a value is not a member of a list.
- Ensure-list-subset
- Cause an error if any element of a true list
is not a member of another true list.
- Ensure-function-no-stobjs
- Cause an error if a function has input or output stobjs.
- Ensure-function-known-measure
- Cause an error if a recursive function
has an unknown measure (i.e. one with :?).
- Ensure-term-not-call-of
- Cause an error if a term is a call of a given function.
- Ensure-lambda-guard-verified-fns
- Cause an error if a lambda expression calls any non-guard-verified function.
- Ensure-term-guard-verified-fns
- Cause an error if a term calls any non-guard-verified function.
- Ensure-term-does-not-call
- Cause an error if a term calls a given function.
- Ensure-lambda-logic-mode
- Cause an error if a lambda expression calls any program-mode function.
- Ensure-lambda-arity
- Cause an error if a lambda expression does not have a given arity.
- Ensure-function-singly-recursive
- Cause an error if a function is not singly recursive.
- Ensure-function-is-pure-if-raw
- Cause an error if a function
has raw Lisp code and is not whitelisted as pure.
- Ensure-function-arity
- Cause an error if a function does not have a given arity.
- Ensure-term-no-stobjs
- Cause an error if a term has output stobjs.
- Ensure-term-logic-mode
- Cause an error if a term calls any program-mode function.
- Ensure-list-functions
- Cause an error if a true list
does not consist of names of existing functions.
- Ensure-keyword-value-list
- Cause an error if a value if not a true list of even length
with keywords at its even-numbered positions (counting from 0).
- Ensure-function-program-mode
- Cause an error if a function is in logic mode.
- Ensure-function-non-recursive
- Cause an error if a function is recursive.
- Ensure-function-is-logic-mode
- Cause an error if a function is in program mode.
- Ensure-function-is-guard-verified
- Cause an error if a function is not guard-verified.
- Ensure-function-is-defined
- Cause an error if a logic-mode function is not defined.
- Ensure-value-is-legal-variable-name
- Cause an error if a value is not a legal variable name.
- Ensure-value-is-function-name
- Cause an error if a value is not the name of an existing function.
- Ensure-value-is-constant-name
- Cause an error if a value is not the name of an existing constant.
- Ensure-term-ground
- Cause an error if a term is not ground (i.e. it has free variables).
- Ensure-symbol-truelist-alist
- Cause an error if a value is not an alist from symbols to true lists.
- Ensure-symbol-not-stobj
- Cause an error if a symbol is the name of a stobj.
- Ensure-symbol-function
- Cause an error if a symbol is not the name of an existing function.
- Ensure-list-has-no-duplicates
- Cause an error if a list has duplicates.
- Ensure-lambda-closed
- Cause an error if a lambda expression is not closed.
- Ensure-function-recursive
- Cause an error if a function is not recursive.
- Ensure-function-name-list
- Cause an error if a value is not
a true list of names of existing functions.
- Ensure-function-has-args
- Cause an error if a function has no arguments.
- Ensure-value-is-true-list
- Cause an error if a value is not a true list.
- Ensure-value-is-symbol-list
- Cause an error if a value is not a true list of symbols.
- Ensure-tuple
- Cause an error if a value is not a tuple of a given length.
- Ensure-symbol-not-keyword
- Cause an error if a symbol is a keyword.
- Ensure-defun-mode-or-auto
- Cause an error if a value is not a defun-mode or :auto.
- Ensure-value-is-symbol
- Cause an error if a value is not a symbol.
- Ensure-value-is-string
- Cause an error if a value is not a string.
- Ensure-value-is-boolean
- Cause an error if a value is not a boolean.
- Ensure-symbol-alist
- Cause an error if a value is not a true alist
whose keys are symbols.
- Ensure-string-or-nil
- Cause an error if a value is not a string or nil.
- Ensure-doublet-list
- Cause an error if a value is not a true list of doublets.
- Ensure-defun-mode
- Cause an error if a value is not a defun-mode.
- Ensure-constant-name
- Cause an error if a value is not a valid constant name.
- Ensure-boolean-or-auto
- Cause an error if a value is not a boolean or :auto.
- Ensure-value-is-nil
- Cause an error if a value is not nil.
- Ensure-function-not-in-termination-thm
- Cause an error if a recursive function
occurs in its own termination theorem.
- Ensure-lambda-guard-verified-exec-fns
- Cause an error if a lambda expression
calls any non-guard-verified function for execution.
- Ensure-term-guard-verified-exec-fns
- Cause an error if a term
calls any non-guard-verified function for execution.
