|
|
|---|
|
|
|
|---|
Cause an error if a value is not
either the name of an existing function
or a
(ensure-function-name-or-numbered-wildcard
x description
error-erp error-val ctx state)
→
(mv erp val state)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.
Function:
(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:
(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:
(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)