Construct a common description text for an input that must be a term.
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-term (&key (subject 'nil) (free-vars 'nil) (1res 'nil) (guard 'nil) (dont-call 'nil) (additional 'nil)) (cons 'xdoc::&& (append (if subject (list subject " must be a") (list "A")) (cons '" term that only references logic-mode functions" (cons (if free-vars (cons 'xdoc::&& (cons '" and that includes no free variables other than " (cons free-vars 'nil))) "") (cons '". This term must have no output " (cons '(xdoc::seetopic "acl2::stobj" "stobjs") (cons '"." (cons (if 1res '(xdoc::&& " This term must return a single (i.e. non-" (xdoc::seetopic "acl2::mv" "@('mv')") " value.") "") (cons (cond ((eq guard t) '(xdoc::&& " This term 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 this term 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 (if dont-call (cons 'xdoc::&& (cons '" This term must not reference " (cons dont-call '(".")))) "") (cons (if additional (cons 'xdoc::&& (cons '" " (cons additional 'nil))) "") 'nil))))))))))))