		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-implementation

Defarbrec-check-redundancy

Check if a call of defarbrec is redundant.

Signature
(defarbrec-check-redundancy fn 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 defarbrec table has no entry for fn, we return nil; the call is not redundant.

If the table has an entry for fn but the call differs, 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: defarbrec-check-redundancy

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