/usr/share/acl2-7.2dfsg/books/misc/dump-events.lisp is in acl2-books-source 7.2dfsg-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 | ; Copyright (C) 1997 Computational Logic, Inc.
; Written by Matt Kaufmann
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
; dump-events.lisp -- file-dumping utility for ACL2
; Originally written by Matt Kaufmann at Computational Logic, Inc.
; Although this file seems to work with ACL2 Release 2.0, it should be
; viewed as providing a capability that may prove useful in using
; ACL2 but _not_ as code that can be trusted to the extent that the
; ACL2 system prover may be trusted.
; To certify this book:
; (certify-book "dump-events").
(in-package "ACL2")
(include-book "xdoc/top" :dir :system)
(set-state-ok t)
(program)
(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>")
(defmacro dump-events (filename &optional (earlier-cd '0) (later-cd ':x))
`(dump-events-fn ,filename ',earlier-cd ',later-cd state))
(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)))))))
(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)))))
(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))))))))
|