Generate the named constant for the abstract syntax tree of the generated C code (i.e. C file set).
(atc-gen-prog-const prog-const fileset print) → events
This constant is not generated if
Function:
(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:
(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)