Make-event-example-3
Using make-event to define thm
The definition of thm provides a simple, yet informative,
example use of make-event. Formerly (through ACL2 Version 8.1), this
was the definition of thm, where thm-fn provides an interface to the
prover.
(defmacro thm (term &key hints otf-flg)
(list 'thm-fn
(list 'quote term)
'state
(list 'quote hints)
(list 'quote otf-flg)))
However, this version of thm did not permit calls of thm in books or encapsulate forms. To remedy that deficiency, ACL2 now
defines thm as follows; below we explain each component of this
definition.
(defmacro thm (term &key hints otf-flg)
`(with-output :off summary :stack :push
(make-event (er-progn (with-output :stack :pop
(thm-fn ',term
state
',hints
',otf-flg))
(value '(value-triple :invisible)))
:expansion? (value-triple :invisible)
:on-behalf-of :quiet!)))
The use of with-output avoids printing anything about
make-event in the summary (by using :off summary). But we do
want a summary for the prover call itself, to see the rules used, time
elapsed, and so on. By using the keyword argument :stack :push, but then
calling with-output again with argument :stack :pop before calling
thm-fn, we remove the effect of :off summary before calling
thm-fn.
By ignoring the with-output wrapper, we may view the body of the
make-event form as follows.
(er-progn (thm-fn ...)
(value '(value-triple :invisible)))
Evaluation of this call of er-progn causes thm-fn to be run
and, if there is no error and the proof succeeds, to return the event
(value-triple :invisible). That event is a no-op, and it generally
doesn't even cause a value to be printed; see ld-post-eval-print.
Since an error-free expansion is always (value-triple :invisible),
that event is specified with the :expansion? keyword so that the
expansion is not stored, in particular in a book's certificate file.
See make-event.
The use of :on-behalf-of :quiet! avoids a needless, distracting error
message from make-event when the proof fails.
