Added new state global variable requested by Jared, last-event-data.
Documentation may come later.  For now, I'll just point to this
comment from get-event-data, which is the utility that returns an
alist associating keys to summary data:

; This function returns an alist with the following keys, reflecting
; information printed in summaries.

; form
; hint-events
; namex [0, a single name, or a list of names; see access-event-tuple-namex]
; prover-steps-counted
; rules
; splitter-rules (case-split immed-forced if-intro)
; time = (prove print proof-tree other)
; warnings

One change is that summary info for rules, hint-events, and
splitter-rules is now computed even if summary printing is inhibited.
So for example, after executing
(thm (equal (append (append x y) z) (append x y z))):

ACL2 !>(fmx "~x0" (@ last-event-data))

((WARNINGS)
 (SPLITTER-RULES)
 (HINT-EVENTS)
 (RULES (:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION BINARY-APPEND)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS))
 (TIME 3/250 0 0 0)
 (FORM . "( THM ...)")
 (PROVER-STEPS-COUNTED . 435))
(0 <state>)
ACL2 !>

Notice that there was no namex because THM doesn't modify the world.

The following timing results for "make regression" were with summary
printing inhibited (via a temporary modification of INHIBIT in
books/build/make_cert).  The first was before we started computing
summary info for rules, hint-events, and splitter-rules even with
summary printing inhibited; the second was after that.

; before:
29719.581u 436.427s 1:09:07.25 727.1%	0+0k 93128+1865928io 122pf+0w

; after:
29837.724u 433.611s 1:09:39.33 724.3%	0+0k 1136+1866120io 0pf+0w

The slowdown is sufficiently small that it seems OK, especially since
summary info isn't usually inhibited.  The alternative would be to
complicate the code and the use of event-data, something that J,
Jared, and I prefer to avoid.

Note that when skipping proofs (e.g., during include-book), we do not
compute summary info for rules, hint-events, and splitter-rules.

Proper documentation may come at a later time.  For now, here is an
example to try that shows how this works.  Use get-event-data instead
if you want particular fields (see above).

(defun my-finalize-event-user (ctx body state)
  (declare (xargs :stobjs state))
  (f-put-global 'my-event-data
                (list :ctx ctx
                      :body body
                      :event-data
                      (and (f-boundp-global 'last-event-data state)
                           (f-get-global 'last-event-data state)))
                state))

(defattach finalize-event-user my-finalize-event-user)

(thm (equal (append (append x y) z) (append x y z)))

(fmx "~x0" (@ my-event-data))


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1333 5d84a466-a78b-0930-a311-59b22171a541
Improved efficiency of *1* functions in the case of :program-mode functions that have invariant-risk.  Jared reports that this patch reduced time results on a problem from 5559.34 seconds, 1,232,196,848,416 bytes to 3.87 seconds, 173,123,280 bytes.

git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1334 5d84a466-a78b-0930-a311-59b22171a541