		Search-engine friendly clone of the ACL2 documentation.

Event-macro-xdoc-constructors-user-level

Xdoc::evmac-desc-function/lambda/macro

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:

The subject parameter must be XDOC text that describes the subject of the assertion of the requirements. The default is the string "It", which should be appropriate if this text follows some preceding text that describes what the input is for.
The 1arg parameter must be a boolean that specifies whether the function or lambda expression must be unary (i.e. take one argument) or not.
The 1res parameter must be a boolean that specifies whether the function or lambda expression must return a single (i.e. non-mv) result or not.
The stobjs parameter must be a boolean that specifies whether the function or lambda expression can have input or output stobjs.
The guard parameter must be one of the following: (i) XDOC text that describes the condition under which the guards must be verified; (ii) t, to indicate that the guards must always be verified; (iii) nil, to indicate that there are no requirements on the guards being verified. The default is nil.
The dont-be-or-call parameter must be one of the following: (i) XDOC text that describes functions that the input (if a function) must differ from or that the input (if a lambda expression) must not reference; (ii) nil (the default), to indicate no such requirements.
The additional-function parameter must be one of the following: (i) XDOC text that describes additional requirements for the function (typically a sentence); (ii) nil (the default) for no additional text.
The additional-lambda parameter must be one of the following: (i) XDOC text that describes additional requirements for the lambda expression (typically a sentence); (ii) nil (the default) for no additional text.
The additional-forms parameter must consist of XDOC list items that describe additional possible forms of the input, besides the function and lambda expression forms. For instance, an additional form could be a keyword :auto to infer the function or lambda expression automatically. The default is the empty string, i.e. no additional forms.

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: evmac-desc-function/lambda/macro

(defmacro xdoc::evmac-desc-function/lambda/macro
          (&key (subject '"It")
                (1arg 'nil)
                (1res 'nil)
                (stobjs '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."
          (cons
           (if stobjs ""
             '(xdoc::&&
                   " This function must have no input or output "
                   (xdoc::seetopic "acl2::stobj" "stobjs")
                   "."))
           (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."
           (cons
            (if stobjs ""
             '(xdoc::&&
               " This lambda expression must have no input or output "
               (xdoc::seetopic "acl2::stobj" "stobjs")
               "."))
            (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))))