		Search-engine friendly clone of the ACL2 documentation.

Error-checking

Ensure-function-name-or-numbered-wildcard

Cause an error if a value is not either the name of an existing function or a numbered name with a wildcard index that resolves to the name of an existing function.

Signature
(ensure-function-name-or-numbered-wildcard x description error-erp error-val ctx state) → (mv erp val state)
Arguments: x — Value to check.; description — Guard (msgp description).; error-erp — Flag to return in case of error.; error-val — Value to return in case of error.; ctx — Context for errors.
Returns: erp — Type (implies erp (equal erp error-erp)).; val — Type (and (implies erp (equal val error-val)) (implies (and (not erp) error-erp) (symbolp val))) .

If successful, return the name of the existing function.

The string in the description should be capitalized because it occurs at the beginning of all the error messages except one; for that one, msg-downcase-first is applied to the description.

Definitions and Theorems

Function: ensure-function-name-or-numbered-wildcard

(defun ensure-function-name-or-numbered-wildcard
       (x description
          error-erp error-val ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (msgp description)))
 (let ((__function__ 'ensure-function-name-or-numbered-wildcard))
  (declare (ignorable __function__))
  (b* (((er &)
        (ensure-value-is-symbol$ x description error-erp error-val))
       (name (resolve-numbered-name-wildcard x (w state)))
       ((er &)
        (ensure-symbol-function$
             name
             (if (eq x name)
                 (msg "~@0, which is the symbol ~x1,"
                      description x)
               (msg "The symbol ~x0, to which ~@1 resolves to,"
                    name (msg-downcase-first description)))
             error-erp error-val)))
    (value name))))

Theorem: return-type-of-ensure-function-name-or-numbered-wildcard.erp

(defthm return-type-of-ensure-function-name-or-numbered-wildcard.erp
  (b* (((mv ?erp ?val ?state)
        (ensure-function-name-or-numbered-wildcard
             x description
             error-erp error-val ctx state)))
    (implies erp (equal erp error-erp)))
  :rule-classes :rewrite)

Theorem: return-type-of-ensure-function-name-or-numbered-wildcard.val

(defthm return-type-of-ensure-function-name-or-numbered-wildcard.val
  (b* (((mv ?erp ?val ?state)
        (ensure-function-name-or-numbered-wildcard
             x description
             error-erp error-val ctx state)))
    (and (implies erp (equal val error-val))
         (implies (and (not erp) error-erp)
                  (symbolp val))))
  :rule-classes :rewrite)

Subtopics

Ensure-function-name-or-numbered-wildcard$: Call ensure-function-name-or-numbered-wildcard with ctx and state as the last two arguments.