		Search-engine friendly clone of the ACL2 documentation.

Defmapping-implementation

Defmapping-check-redundancy

Check if a call to defmapping is redundant.

Signature
(defmapping-check-redundancy name print show-only call ctx state) → (mv erp yes/no state)
Arguments: call — Guard (pseudo-event-formp call).
Returns: yes/no — A booleanp.

If the defmapping table has no entry for name, we return nil: the call is not redundant.

If the table has an entry for name but the call differs (after removing any :print and :show-only), an error occurs.

If the call is redundant, we know that all the inputs except possibly :print and :show-only are valid (because they are the same as the ones of the recorded successful call); we validate these two inputs, for better error checking. If :show-only is t, we print the recorded expansion of the call. Unless :print is nil, we print a message saying that the call is redundant.

Definitions and Theorems

Function: defmapping-check-redundancy

(defun defmapping-check-redundancy
       (name print show-only call ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (pseudo-event-formp call)))
 (let ((__function__ 'defmapping-check-redundancy))
  (declare (ignorable __function__))
  (b*
   ((table (table-alist *defmapping-table-name* (w state))
)
    (pair (assoc-equal name table))
    ((unless pair) (value nil))
    (info (cdr pair))
    (call$ (defmapping-filter-call call))
    ((unless (equal call$ (defmapping-info->call$ info)))
     (er-soft+
      ctx t nil
      "A different call to DEFMAPPING with name ~x0 ~
                   has already been performed."
      name))
    ((er &)
     (evmac-process-input-print print ctx state))
    ((er &)
     (evmac-process-input-show-only show-only ctx state))
    ((run-when show-only)
     (cw "~x0~|"
         (defmapping-info->expansion info)))
    ((run-when print)
     (cw "~%The call ~x0 is redundant.~%" call)))
   (value t))))