		Search-engine friendly clone of the ACL2 documentation.

Transformation-table

Record-transformation-call-event

Create an event form to record a transformation call into the transformation table.

Signature
(record-transformation-call-event call encapsulate wrld) → event
Arguments: call — Guard (pseudo-event-formp call).; encapsulate — Guard (pseudo-event-formp encapsulate).; wrld — Guard (plist-worldp wrld).
Returns: event — Type (pseudo-event-formp event).

The :print and :show-only inputs, if present, are removed from the call prior to recording it. See the discussion here for motivation.

Definitions and Theorems

Function: record-transformation-call-event

(defun record-transformation-call-event (call encapsulate wrld)
 (declare (xargs :guard (and (pseudo-event-formp call)
                             (pseudo-event-formp encapsulate)
                             (plist-worldp wrld))))
 (let ((__function__ 'record-transformation-call-event))
  (declare (ignorable __function__))
  (b*
   ((call
     (remove-irrelevant-inputs-from-transformation-call call wrld)))
   (cons 'table
         (cons 'transformation-table
               (cons (cons 'quote (cons call 'nil))
                     (cons (cons 'quote (cons encapsulate 'nil))
                           'nil)))))))

Theorem: pseudo-event-formp-of-record-transformation-call-event

(defthm pseudo-event-formp-of-record-transformation-call-event
 (b*
  ((event (record-transformation-call-event call encapsulate wrld)))
  (pseudo-event-formp event))
 :rule-classes :rewrite)