Remove from a call to a transformation
the
(remove-irrelevant-inputs-from-transformation-call call wrld) → call-without-print-showonly
See the discussion
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.
Function:
(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:
(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)