		Search-engine friendly clone of the ACL2 documentation.

Clause-processor

Make-summary-data

Return summary data from a clause-processor function

For relevant background, see clause-processor. Here we discuss the value d and its effect in the signature [3+] shown in that topic:

[3+] ((CL-PROC cl hint st_1 ... st_k) => (mv erp cl-list st_i1 ... st_in d))

The purpose of d is to return summary information, as illustrated by the following (admittedly artificial) example. Here we abbreviate somewhat; the full example may be found in the community-book, books/clause-processors/basic-examples.lisp.

(defevaluator evl evl-list ...)

(defun strengthen-cl2 (cl term state)
  (declare (xargs :stobjs state))
  (cond ((null term) ; then no change
         (mv nil (list cl) state nil))
        ...
        ((pseudo-termp term)
         (mv nil
             (list (cons (list 'not term)
                         cl)
                   (list term))
             state
             (make-summary-data :runes '((:rewrite car-cons)
                                         (:rewrite cdr-cons)
                                         (:rewrite car-cons))
                                :use-names '(nth binary-append)
                                :by-names '(nthcdr)
                                :clause-processor-fns
                                '(note-fact-clause-processor))))
        (t ..)))

(defthm correctness-of-strengthen-cl2
  (implies (and (pseudo-term-listp cl)
                (alistp a)
                (evl (conjoin-clauses
                      (clauses-result (strengthen-cl2 cl term state)))
                     a))
           (evl (disjoin cl) a))
  :rule-classes :clause-processor)

(defthm test-strengthen-cl2
  (equal y y)
  :hints (("Goal"
           :instructions
           ((:prove
             :hints (("Goal"
                      :clause-processor
                      (strengthen-cl2 clause '(equal x x) state)))))))
  :rule-classes nil)

Evaluation of the final defthm event above prints the following summary, which illustrates how the values of the four legal keywords for make-summary-data naturally translate to the summary, specifically, to the "Rules" field for the :runes keyword and to the "Hint-events" field for the others.

Summary
Form:  ( DEFTHM TEST-STRENGTHEN-CL2 ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS))
Hint-events: ((:BY NTHCDR)
              (:CLAUSE-PROCESSOR NOTE-FACT-CLAUSE-PROCESSOR)
              (:CLAUSE-PROCESSOR STRENGTHEN-CL2)
              (:USE BINARY-APPEND)
              (:USE NTH))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Note that each keyword is optional; in particular, the form (make-summary-data) is legal, and it specifies nil for each of the four keywords. Moreover, it is also legal for d to be nil, which is equivalent to (make-summary-data). Thus, if d is nil or (make-summary-data) then [3+] and [3] in the documentation for clause-processor have the same effect: that is, there will be no visible effect if we change such a clause-processor function (i.e., one returning empty summary data) from form [3+] to form [3] by dropping the return value of d.

Duplicates are allowed in the list, for each argument of make-summary-data; no duplicates will appear in the summary. There is also no need to sort elements of those lists.

Finally, note that the summary information from d not only goes into the summary, but also is incorporated when extending the proof-supporters-alist to record the dependencies of the completed event.

(assert-event
 (equal (sort-symbol-listp
         (car (global-val 'proof-supporters-alist (w state))))
        '(BINARY-APPEND CAR-CONS CDR-CONS
                        NOTE-FACT-CLAUSE-PROCESSOR NTH NTHCDR
                        STRENGTHEN-CL2 TEST-STRENGTHEN-CL2)))