Filtering...

dump-events

books/misc/dump-events

Included Books

top
other
(in-package "ACL2")
include-book
(include-book "xdoc/top" :dir :system)
other
(set-state-ok t)
other
(program)
other
(defxdoc dump-events
  :parents (events)
  :short "Dump events to a file."
  :long "<p>Examples</p>

@({
  (include-book "misc/dump-events" :dir :system)
  (dump-events "xxx")        ; dump all user events to file xxx
  (dump-events "xxx" :x-2)   ; dump the last two events to file xxx
  (dump-events "xxx" 2 :x-1) ; dump all events from after command 2
                             ; up through the next-to-last command
})

<p>General Form</p>

@({
  (dump-events dumpfile
               &optional earlier-command-desc later-command-desc)
})

<p>where the form of the optional command descriptors is explained elsewhere;
see @(see command-descriptor).  All events strictly after the first command
descriptor up through the second, which by default are @('0') and @(':x') (thus
indicating that all user events should be dumped to the dumpfile), are written
to the indicated dumpfile.  In addition, an extra form is written to the top of
the dumpfile: @('(in-package "ACL2")').  This makes it convenient to use the
dumpfile as a source file for ACL2 in a later session.</p>

<p>Each event that was originally executed underneath @(see LOCAL) will be
placed inside @(see LOCAL) in the dumpfile.</p>

<p>The dumpfile will be overwritten if it already exists.</p>")
dump-eventsmacro
(defmacro dump-events
  (filename &optional (earlier-cd '0) (later-cd ':x))
  `(dump-events-fn ,FILENAME ',EARLIER-CD ',LATER-CD state))
dump-events-fn1function
(defun dump-events-fn1
  (earlier-wrld later-wrld acc in-local-flg)
  (cond ((equal earlier-wrld later-wrld) acc)
    (t (let ((tuple (car later-wrld)))
        (case-match tuple
          (('command-landmark 'global-value & ':logic 'local . &) (dump-events-fn1 earlier-wrld (cdr later-wrld) acc t))
          (('command-landmark 'global-value & 'local . &) (dump-events-fn1 earlier-wrld (cdr later-wrld) acc t))
          (('command-landmark 'global-value . &) (dump-events-fn1 earlier-wrld (cdr later-wrld) acc nil))
          (('event-landmark 'global-value n (& . &) . ev) (cond ((integerp n) (dump-events-fn1 earlier-wrld
                  (cdr later-wrld)
                  (cons (if in-local-flg
                      (list 'local ev)
                      ev)
                    acc)
                  in-local-flg))
              (t (dump-events-fn1 earlier-wrld
                  (cdr later-wrld)
                  acc
                  in-local-flg))))
          (('event-landmark 'global-value n . ev) (cond ((integerp n) (dump-events-fn1 earlier-wrld
                  (cdr later-wrld)
                  (cons (if in-local-flg
                      (list 'local ev)
                      ev)
                    acc)
                  in-local-flg))
              (t (dump-events-fn1 earlier-wrld
                  (cdr later-wrld)
                  acc
                  in-local-flg))))
          (& (dump-events-fn1 earlier-wrld
              (cdr later-wrld)
              acc
              in-local-flg)))))))
fmt-lstfunction
(defun fmt-lst
  (lst chan state)
  (cond ((endp lst) state)
    (t (pprogn (fms "~q0" (list (cons #\0 (car lst))) chan state nil)
        (fmt-lst (cdr lst) chan state)))))
dump-events-fnfunction
(defun dump-events-fn
  (filename earlier-cd later-cd state)
  (let ((wrld (w state)))
    (er-let* ((earlier-wrld (er-decode-cd earlier-cd wrld 'dump-events state)) (later-wrld (er-decode-cd later-cd wrld 'dump-events state)))
      (cond ((<= (length later-wrld) (length earlier-wrld)) (er soft
            'dump-events
            "The command descriptor ~p0 does not refer to a later (longer) ~
                 world than does the command descriptor ~p1."
            later-cd
            earlier-cd))
        (t (mv-let (chan state)
            (open-output-channel filename :character state)
            (pprogn (fms "(in-package ~p0)~%"
                (list (cons #\0 (f-get-global 'current-package state)))
                chan
                state
                nil)
              (fmt-lst (dump-events-fn1 earlier-wrld later-wrld nil nil)
                chan
                state)
              (close-output-channel chan state)
              (value :invisible))))))))