Construct a common description text for an input that must be a function name or a lambda expression or a macro name.
This text expresses some common requirements on this kind of inputs to event macros.
This utility provides some customization facilities:
Looking at some uses of this utility should make it clearer.
This utility may need to be extended and generalized in the future, in particular with more customization facilities.
Macro:
(defmacro xdoc::evmac-desc-function/lambda/macro (&key (subject '"It") (1arg 'nil) (1res 'nil) (guard 'nil) (dont-be-or-call 'nil) (additional-function 'nil) (additional-lambda 'nil) (additional-forms '"")) (cons 'xdoc::&& (cons (cons 'xdoc::p (cons subject '(" must be one of the following:"))) (cons (cons 'xdoc::ul (cons (cons 'xdoc::li (cons '"The name of a " (cons (if 1arg "unary " "") (cons '"logic-mode function. This function must have no input or output " (cons '(xdoc::seetopic "acl2::stobj" "stobjs") (cons '"." (cons (if 1res '(xdoc::&& " This function must return a single (i.e. non-" (xdoc::seetopic "acl2::mv" "@('mv')") " result.") "") (cons (cond ((eq guard t) " This function must be guard-verified.") ((eq guard nil) "") (t (cons 'xdoc::&& (cons '" If " (cons guard '(", then this function must be guard-verified.")))))) (cons (if dont-be-or-call (cons 'xdoc::&& (cons '" This function must be distinct from " (cons dont-be-or-call '(".")))) "") (cons (if additional-function (cons 'xdoc::&& (cons '" " (cons additional-function 'nil))) "") 'nil)))))))))) (cons (cons 'xdoc::li (cons '"A " (cons (if 1arg "unary " "") (cons '"closed lambda expression that only references logic-mode functions. This lambda expression must have no input or output " (cons '(xdoc::seetopic "acl2::stobj" "stobjs") (cons '"." (cons (if 1res '(xdoc::&& " This lambda expression must return a single (i.e. non-" (xdoc::seetopic "acl2::mv" "@('mv')") " result.") "") (cons (cond ((eq guard t) '(xdoc::&& " The body of this lambda expression must only call guard-verified functions, except possibly in the @(':logic') subterms of " (xdoc::seetopic "acl2::mbe" "@('mbe')") "s or via " (xdoc::seetopic "acl2::ec-call" "@('ec-call')") ".")) ((eq guard nil) "") (t (cons 'xdoc::&& (cons '" If " (cons guard '(", then the body of this lambda expression must only call guard-verified functions, except possibly in the @(':logic') subterms of " (xdoc::seetopic "acl2::mbe" "@('mbe')") "s or via " (xdoc::seetopic "acl2::ec-call" "@('ec-call')") ".")))))) (cons '" As an abbreviation, the name @('mac') of a macro stands for the lambda expression @('(lambda (z1 z2 ...) (mac z1 z2 ...))'), where @('z1'), @('z2'), ... are the required parameters of @('mac'); that is, a macro name abbreviates its eta-expansion (considering only the macro's required parameters)." (cons (if dont-be-or-call (cons 'xdoc::&& (cons '" This lambda expression must not reference " (cons dont-be-or-call '(".")))) "") (cons (if additional-lambda (cons 'xdoc::&& (cons '" " (cons additional-lambda 'nil))) "") 'nil))))))))))) (cons additional-forms 'nil)))) 'nil))))