• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
      • Evmac-input-hints-p
      • Evmac-input-print-p
      • Event-macro-input-processing
      • Function-definedness
      • Event-macro-screen-printing
      • Make-event-terse
      • Event-macro-applicability-conditions
      • Event-macro-results
      • Template-generators
      • Event-macro-event-generators
      • Event-macro-proof-preparation
      • Try-event
      • Restore-output?
      • Restore-output
      • Fail-event
      • Cw-event
      • Event-macro-xdoc-constructors
        • Event-macro-xdoc-constructors-user-level
          • Xdoc::evmac-desc-function/lambda/macro
          • Xdoc::evmac-desc-term
          • Xdoc::evmac-topic-design-notes
          • Xdoc::evmac-appcond
          • Xdoc::evmac-desc-input-name
          • Xdoc::evmac-section-redundancy
          • Xdoc::evmac-input-show-only
          • Xdoc::evmac-input-print
          • Xdoc::evmac-desc-input-enable-t/nil
          • Xdoc::evmac-section-appconds
          • Xdoc::evmac-input-hints
          • Xdoc::evmac-section-generated
          • Xdoc::evmac-section-intro
          • Xdoc::evmac-section-inputs
          • Xdoc::evmac-section-form
        • Event-macro-xdoc-constructors-implementation-level
      • Event-macro-intro-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Event-macro-xdoc-constructors-user-level

Xdoc::evmac-desc-term

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:

• The subject parameter must be either nil or XDOC text that describes the subject of the assertion of the requirements. The default is nil, which means that there is no subject, and the description starts with "A term that...". If not nil, the description starts with "subject must be a term...".
• The free-vars parameter must be one of the following: (i) XDOC text that describes the allowed free variables in the term; (ii) nil (the default) for no requirements on free variables.
• The 1res parameter must be a boolean that specifies whether the term must return a single (i.e. non-mv) value or not.
• The stobjs parameter must be a boolean that specifies whether the term 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-call parameters must one of the following: (i) XDOC text that describes functions that this term must not call; (ii) nil (the default), to indicate that the term may call any function.
• The additional parameter must be one of the following: (i) XDOC text that describes additional requirements for the term (typically a sentence); (ii) nil (the default) for no additional text.

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-term

(defmacro xdoc::evmac-desc-term (&key (subject 'nil)
                                      (free-vars 'nil)
                                      (1res 'nil)
                                      (stobjs '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
      (if stobjs ""
        '(xdoc::&& ". This term must have no output "
                   (xdoc::seetopic "acl2::stobj" "stobjs")
                   "."))
      (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))))))))))