		Search-engine friendly clone of the ACL2 documentation.

Atc-event-and-code-generation

Atc-gen-prog-const

Generate the named constant for the abstract syntax tree of the generated C code (i.e. C file set).

Signature
(atc-gen-prog-const prog-const fileset print) → events
Arguments: prog-const — Guard (symbolp prog-const).; fileset — Guard (filesetp fileset).; print — Guard (evmac-input-print-p print).
Returns: events — Type (pseudo-event-form-listp events).

This constant is not generated if :proofs is nil.

Definitions and Theorems

Function: atc-gen-prog-const

(defun atc-gen-prog-const (prog-const fileset print)
 (declare (xargs :guard (and (symbolp prog-const)
                             (filesetp fileset)
                             (evmac-input-print-p print))))
 (let ((__function__ 'atc-gen-prog-const))
  (declare (ignorable __function__))
  (b*
   ((defconst-event
         (cons 'defconst
               (cons prog-const
                     (cons (cons 'quote (cons fileset 'nil))
                           'nil))))
    (progress-start?
         (and (evmac-input-print->= print :info)
              '((cw-event "~%Generating the named constant..."))))
    (progress-end? (and (evmac-input-print->= print :info)
                        '((cw-event " done.~%"))))
    (print-result?
     (and
      (evmac-input-print->= print :result)
      (cons
          (cons 'cw-event
                (cons '"~%~x0~|"
                      (cons (cons 'quote (cons defconst-event 'nil))
                            'nil)))
          'nil))))
   (append progress-start? (list defconst-event)
           progress-end? print-result?))))

Theorem: pseudo-event-form-listp-of-atc-gen-prog-const

(defthm pseudo-event-form-listp-of-atc-gen-prog-const
  (b* ((events (atc-gen-prog-const prog-const fileset print)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)