		Search-engine friendly clone of the ACL2 documentation.

Error-checking

Ensure-symbol-is-fresh-event-name

Cause an error if a symbol cannot be used as the name of a new event of a certain type, also given that certain symbols will be used as event names.

Signature
(ensure-symbol-is-fresh-event-name sym description type other-event-names-to-avoid error-erp error-val ctx state) → (mv erp val state)
Arguments: sym — Symbol to check.
Guard (symbolp sym).; description — Description of sym, for the error messages.
Guard (msgp description).; type — Guard (member-eq type '(function macro const stobj constrained-function nil)) .; other-event-names-to-avoid — Guard (symbol-listp other-event-names-to-avoid).; error-erp — Flag to return in case of error.
Guard (not (null error-erp)).; error-val — Value to return in case of error.; ctx — Guard (ctxp ctx).
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 sym) (symbol-listp other-event-names-to-avoid)) (symbol-listp val))) .

The typical use of this error checker is in code that generates events. The name of each event must be fresh, i.e. not already in use in the ACL2 world: we check this via fresh-namep-msg-weak; the type of event here is the same as in that utility. Furthermore, when multiple events are generated, we must ensure that the names (which are not yet in the world) are all distinct from each other: the symbol list parameter of this error checker contains names of other events that are being generated; we check that the symbol is distinct form of them.

Definitions and Theorems

Function: ensure-symbol-is-fresh-event-name

(defun
 ensure-symbol-is-fresh-event-name
 (sym description
      type other-event-names-to-avoid
      error-erp error-val ctx state)
 (declare (xargs :stobjs (state)))
 (declare
  (xargs
   :guard
   (and (symbolp sym)
        (msgp description)
        (member-eq type
                   '(function macro
                              const stobj constrained-function nil))
        (symbol-listp other-event-names-to-avoid)
        (not (null error-erp))
        (ctxp ctx))))
 (let
  ((__function__ 'ensure-symbol-is-fresh-event-name))
  (declare (ignorable __function__))
  (b*
   ((msg/nil (fresh-namep-msg-weak sym type (w state)))
    ((when msg/nil)
     (er-soft+ ctx error-erp
               error-val "~@0 is already in use.  ~@1"
               description msg/nil))
    ((when (member-eq sym other-event-names-to-avoid))
     (er-soft+
      ctx error-erp error-val
      "~@0 must be distinct from the names ~&1 ~
                   of events that are also being generated, ~
                   but it is not."
      description
      other-event-names-to-avoid)))
   (value (cons sym other-event-names-to-avoid)))))

Theorem: return-type-of-ensure-symbol-is-fresh-event-name.erp

(defthm return-type-of-ensure-symbol-is-fresh-event-name.erp
        (b* (((mv ?erp ?val ?state)
              (ensure-symbol-is-fresh-event-name
                   sym description
                   type other-event-names-to-avoid
                   error-erp error-val ctx state)))
            (implies erp (equal erp error-erp)))
        :rule-classes :rewrite)

Theorem: return-type-of-ensure-symbol-is-fresh-event-name.val

(defthm
   return-type-of-ensure-symbol-is-fresh-event-name.val
   (b* (((mv ?erp ?val ?state)
         (ensure-symbol-is-fresh-event-name
              sym description
              type other-event-names-to-avoid
              error-erp error-val ctx state)))
       (and (implies erp (equal val error-val))
            (implies (and (not erp)
                          error-erp (symbolp sym)
                          (symbol-listp other-event-names-to-avoid))
                     (symbol-listp val))))
   :rule-classes :rewrite)

Subtopics

Ensure-symbol-is-fresh-event-name$: Call ensure-symbol-is-fresh-event-name with ctx and state as the last two arguments.