• 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-input-processors
          • Def-process-input-fresh-function-name
          • Evmac-process-input-hints
          • Evmac-process-input-show-only
          • Evmac-process-input-print
      • 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-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-input-processors

Evmac-process-input-hints

Process the :hints input of an event macro.

Signature

(evmac-process-input-hints hints ctx state) 
  → 
(mv erp hints$ state)

Returns

hints$ — Type (evmac-input-hints-p hints$).

This is for event macros that have a :hints input for user-supplied hints to prove applicability conditions.

See the discussion in evmac-input-hints-p about the possible forms of the :hints input of an event macro. This utility validates the :hints input and returns it in processed form.

If the :hints input is a keyword-value list, we check that the keywords are all distinct, and return it in alist form. We do not check that the keywords identify applicability conditions that are actually present, as this would complicate this input processing function. Instead, as discussed in evmac-appcond-theorem, we let the event macro handle the situation.

If the :hints input is not a keyword-value list, we ensure that it is at least a true list, and return it unchanged.

Note that if the input is (perhaps by default) nil, it is recognized as a keyword-value list with unique (no) keywords, and returned unchanged as an alist, i.e. nil.

Definitions and Theorems

Function: evmac-process-input-hints

(defun evmac-process-input-hints (hints ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'evmac-process-input-hints))
  (declare (ignorable __function__))
  (if
   (keyword-value-listp hints)
   (b*
    ((hints$ (keyword-value-list-to-alist hints))
     (kwds (strip-cars hints$))
     ((er &)
      (ensure-list-has-no-duplicates$
       kwds
       (msg
        "The list of keywords ~x0 ~
                                                  in the keyword-value list ~
                                                  that forms the :HINTS input"
        kwds)
       t nil)))
    (value hints$))
   (if (true-listp hints)
       (value hints)
    (er-soft+
     ctx t nil
     "The :HINTS input must be ~
                 either a keyword-value list or a true list, ~
                 but it is ~x0 instead, which is neither."
     hints)))))

Theorem: evmac-input-hints-p-of-evmac-process-input-hints.hints$

(defthm evmac-input-hints-p-of-evmac-process-input-hints.hints$
  (b* (((mv ?erp ?hints$ ?state)
        (evmac-process-input-hints hints ctx state)))
    (evmac-input-hints-p hints$))
  :rule-classes :rewrite)