• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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
      • Function-definedness
      • Event-macro-input-processing
      • Event-macro-screen-printing
      • Make-event-terse
      • Event-macro-applicability-conditions
        • Evmac-input-hints-p
        • Event-macro-applicability-condition-utilities
          • Evmac-appcond-theorem
          • Evmac-appcond-theorem-list
          • Evmac-appcondp
          • Evmac-ensure-no-extra-hints
          • Make-evmac-appcond?
          • Evmac-appcond-theorems-no-extra-hints
          • Evmac-appcond-listp
      • 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-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-applicability-condition-utilities

Evmac-ensure-no-extra-hints

Ensure that there are no extra hints for applicability conditions.

Signature

(evmac-ensure-no-extra-hints remaining-hints ctx state) 
  → 
(mv erp nothing state)

Arguments

remaining-hints — Guard (evmac-input-hints-p remaining-hints).

Returns

nothing — Type (null nothing).

This is meant to be called on the hints result of evmac-appcond-theorem-list. That function removes the specific hints for applicability conditions as it turns the applicability conditions into theorem form. Thus, if there are remaining hints at the end, it means that the user has specified hints for applicability conditions that did not have to hold in that particular call of the event macro. If that is the case, the event macro may cause an error, and can use this function to do so consistently.

Note that here we cause an error only if the hints are a non-empty alist from keywords to true lists. It would be wrong to just check for consp, because if the hints originally entered by the user are not a keyword-value list, then evmac-appcond-theorem-list uses the same hints on all the applicability conditions, and never changes them.

Definitions and Theorems

Function: evmac-ensure-no-extra-hints

(defun evmac-ensure-no-extra-hints (remaining-hints ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (evmac-input-hints-p remaining-hints)))
 (let ((__function__ 'evmac-ensure-no-extra-hints))
  (declare (ignorable __function__))
  (if
   (and (keyword-truelist-alistp remaining-hints)
        (consp remaining-hints))
   (er-soft+
    ctx t nil
    "The :HINTS input includes the keywords ~x0, ~
                 which do not correspond to applicability conditions ~
                 that must hold in this call. ~
                 Double-check the names (keywords) ~
                 of the applicability conditions, ~
                 as well as the conditions under which ~
                 each applicability condition must hold."
    (strip-cars remaining-hints))
   (value nil))))

Theorem: null-of-evmac-ensure-no-extra-hints.nothing

(defthm null-of-evmac-ensure-no-extra-hints.nothing
  (b* (((mv ?erp ?nothing ?state)
        (evmac-ensure-no-extra-hints remaining-hints ctx state)))
    (null nothing))
  :rule-classes :rewrite)