Def-error-checker
Generate an error checking function
and an associated macro abbreviation.
This macro generates an error checking function
and an associated macro abbreviation of the following form:
(define <name> (<x1> ... <xn>
(description msgp)
(error-erp (not (null error-erp))
"Flag to return in case of error.")
(error-val "Value to return in case of error.")
(ctx "Context for errors.")
state)
:returns (mv <erp>
<val>
state)
:mode <mode>
:verify-guards <verify-guards> ; may be absent
:parents <parents> ; may be absent
:short <short> ; may be absent
:long <long> ; may be absent
(b* (((unless <condition1>) (er-soft+
ctx error-erp error-val . <message1>))
...
((unless <conditionm>) (er-soft+
ctx error-erp error-val . <messagem>)))
(value <result>))
:no-function t)
(defsection <name>$
:parents (<name>)
:short "Calls @(tsee <name>) with
@('ctx') and @('state') as the last two arguments."
:long "@(def <name>$)"
(defmacro <name>$ (<x1'> ... <xn'> description error-erp error-val)
`(<name> ,<x1'> ... ,<xn'> description error-erp error-val ctx state)))where each <...>,
except <erp>, <val>, and <x1'>, ..., <xn'>,
is supplied as argument to the macro:
- <name> is the name of the function,
and, with a $ added at the end, the name of the macro.
- Each <xi> is a symbol or
an extended formal.
Let <xi'> be:
<xi> if <xi> is a symbol;
the name of the <xi> extended formal otherwise.
- <erp> is a return specifier that describes the error flag returned
inside the error triple.
This return specifier is:
(erp (implies erp (equal erp error-erp)))
if <mode> is :logic; and
(erp "@('nil or error-erp.")')
if <mode> is :program.
- <val> is a return specifier that describes the value returned
inside the error triple.
This return specifier depends on the <returns> argument to the macro
(see below for the complete list of arguments to the macro)
and on <mode>:
if no <returns> argument is supplied and <mode> is :logic,
then <val> is
(val (and (implies erp (equal val error-val))
(implies (and (not erp) error-erp) (not val))));
if no <returns> argument is supplied and <mode> is :program,
then <val> is
(val "@('nil if erp is nil, otherwise error-val.")');
if a <returns> argument is supplied,
then <val> is <returns>.
- <mode> is either :logic or :program.
- <verify-guards> is either t or nil.
If <verify-guards> is not supplied as argument,
:verify-guards is absent.
- <parents> is a list of parent XDOC topics.
If <parents> is not supplied as argument, :parents is absent.
- <short> and <long> are strings that document the function.
If <short> is not supplied as argument, :short is absent.
If <long> is not supplied as argument, :long is absent.
- Each <conditionj> is a term
whose evaluation checks a condition
on the <x1>, ..., <xn> arguments.
The conditions are checked in order.
- Each <messagej> is a list that consists of
a format string
followed by up to 10 terms,
whose values fill in the placeholders of the format string.
Generally, one of these terms should be description
and it should correspond to a ~@ placeholder
in the format string,
which is appropriate for the msgp type of description.
The <messagej> list is inserted into the er-soft+ call,
providing an error message when <conditionj> is not satisfied
(but the previous conditions are).
- <result> is a term whose value is returned
when all the conditions are satisfied.
The generated formal arguments
description, error-erp, and error-val
and the generated return variables erp and val
are symbols with those names in the same package as
the <name> symbol used as the name of the generated function.
The macro is called as follows:
(def-error-checker <name>
(<x1> ... <xn>)
:body ((<condition1> . <message1>) ... (<conditionm> . <messagem>))
:returns <returns> ; default not used
:result <result> ; default is nil
:mode <mode> ; default is :logic
:verify-guards <verify-guards> ; default not used
:parents <parents> ; default not used
:short <short> ; default not used
:long <long> ; default not used
)
A table keeps track of all the successful calls to this macro,
for redundancy checking.
Subtopics
- Def-error-checker-implementation
- Implementation of def-error-checker.
