		Search-engine friendly clone of the ACL2 documentation.

Transformation-table

Remove-irrelevant-inputs-from-transformation-call

Remove from a call to a transformation the :print and :show-only inputs, if present.

Signature
(remove-irrelevant-inputs-from-transformation-call call wrld) → call-without-print-showonly
Arguments: call — Guard (pseudo-event-formp call).; wrld — Guard (plist-worldp wrld).
Returns: call-without-print-showonly — Type (pseudo-event-formp call-without-print-showonly), given (pseudo-event-formp call).

See the discussion here for motivation.

A transformation macro consists of some mandatory inputs followed by some optional keyed inputs. We look up the number of required arguments of the macro, and use that to separate mandatory and optional inputs. We trim the optional inputs and we join them with the mandatory ones to form the trimmed call to return.

Definitions and Theorems

Function: remove-irrelevant-inputs-from-transformation-call

(defun remove-irrelevant-inputs-from-transformation-call (call wrld)
 (declare (xargs :guard (and (pseudo-event-formp call)
                             (plist-worldp wrld))))
 (let ((__function__
            'remove-irrelevant-inputs-from-transformation-call))
   (declare (ignorable __function__))
   (b*
     (((cons name args) call)
      (number-of-mandatory-inputs
           (len (macro-required-args name wrld)))
      (mandatory-inputs (take number-of-mandatory-inputs args))
      (optional-inputs (nthcdr number-of-mandatory-inputs args))
      (optional-inputs (remove-keyword :print optional-inputs))
      (optional-inputs (remove-keyword :show-only optional-inputs)))
     (cons name
           (append mandatory-inputs optional-inputs)))))

Theorem: pseudo-event-formp-of-remove-irrelevant-inputs-from-transformation-call

(defthm
 pseudo-event-formp-of-remove-irrelevant-inputs-from-transformation-call
 (implies
  (pseudo-event-formp call)
  (b*
   ((call-without-print-showonly
     (remove-irrelevant-inputs-from-transformation-call call wrld)))
   (pseudo-event-formp call-without-print-showonly)))
 :rule-classes :rewrite)