		Search-engine friendly clone of the ACL2 documentation.

Atc-input-processing

Atc-process-print

Process the :print input.

Signature
(atc-process-print options) → (mv erp print)
Arguments: options — Guard (symbol-alistp options).
Returns: print — Type (evmac-input-print-p print).

We use the evmac-input-print-p type, but we exclude the nil case; see the ATC user doc. We should probably define a new type for the printing levels supported by ATC, or perhaps change evmac-input-print-p to be that, as it may be more appropriate.

Definitions and Theorems

Function: atc-process-print

(defun atc-process-print (options)
 (declare (xargs :guard (symbol-alistp options)))
 (let ((__function__ 'atc-process-print))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil)
    (print-option (assoc-eq :print options))
    (print (if print-option (cdr print-option)
             :result))
    ((unless (and (evmac-input-print-p print) print))
     (reterr
      (msg
       "The :PRINT input must be ~
                      :ERROR, :RESULT, :INFO, or :ALL; ~
                      but it is ~x0 instead."
       print))))
   (retok print))))

Theorem: evmac-input-print-p-of-atc-process-print.print

(defthm evmac-input-print-p-of-atc-process-print.print
  (b* (((mv acl2::?erp common-lisp::?print)
        (atc-process-print options)))
    (evmac-input-print-p print))
  :rule-classes :rewrite)