table-replay - ACL2 Book

other

(in-package "ACL2")

table-replay-initmacro

(defmacro table-replay-init
  (name)
  `(local (table table-replay-table ',NAME :init)))

replay-table-changesfunction

(defun replay-table-changes
  (name world)
  (declare (xargs :mode :program))
  (if (atom world)
    nil
    (let* ((entry (car world)) (entry-type (car entry)))
      (if (and (eq entry-type 'event-landmark)
          (eq (access-event-tuple-type (cddr entry)) 'table))
        (let* ((form (access-event-tuple-form (cddr entry))) (table-name (cadr form)))
          (cond ((eq name table-name) (cons form (replay-table-changes name (cdr world))))
            ((and (eq name 'table-replay-table)
               (equal (cadr form) (list 'quote name))
               (eq (caddr form) :init)) nil)
            (t (replay-table-changes name (cdr world)))))
        (replay-table-changes name (cdr world))))))

table-replaymacro

(defmacro table-replay
  (name)
  `(make-event (cons 'progn
      (reverse (replay-table-changes ',NAME (w state))))))