		Search-engine friendly clone of the ACL2 documentation.

Atc-event-and-code-generation

Atc-gen-fileset-event

Event to pretty-print the generated C code to the file system.

Signature
(atc-gen-fileset-event fileset file-name pretty-printing print) → event
Arguments: fileset — Guard (filesetp fileset).; file-name — Guard (stringp file-name).; pretty-printing — Guard (pprint-options-p pretty-printing).; print — Guard (evmac-input-print-p print).
Returns: event — Type (pseudo-event-formp event).

This serves to run pprint-fileset after the constant and theorem events have been submitted. This function generates an event form that is put (by atc-gen-everything) after the constant and theorem events. When the events are submitted to and processed by ACL2, we get to this file generation event only if the previous events are successful. This is a sort of safety/security constraint: do not even generate files, unless they are correct.

If :print is :info or :all, we also generate events to print progress messages, as done with the constant and theorem events.

In order to generate an embedded event form for output file generation, we generate a make-event whose argument generates the file. The argument must also return an embedded event form, so we use value-triple with :invisible, so there is no extra screen output. This is a ``dummy'' event, which is not supposed to do anything: it is the execution of the make-event argument that matters, because it writes the file set to the file system. In essence, we use make-event to turn a computation (the one that writes the output files) into an event. But we cannot use just value-triple because our computation returns an error triple.

Definitions and Theorems

Function: atc-gen-fileset-event

(defun atc-gen-fileset-event
       (fileset file-name pretty-printing print)
 (declare (xargs :guard (and (filesetp fileset)
                             (stringp file-name)
                             (pprint-options-p pretty-printing)
                             (evmac-input-print-p print))))
 (let ((__function__ 'atc-gen-fileset-event))
  (declare (ignorable __function__))
  (b*
   ((progress-start?
         (and (evmac-input-print->= print :info)
              '((cw-event "~%Generating the file(s)..."))))
    (progress-end? (and (evmac-input-print->= print :info)
                        '((cw-event " done.~%"))))
    (file-gen-event
     (cons
      'make-event
      (cons
       (cons
        'b*
        (cons
         (cons
          (cons
           '(er &)
           (cons
            (cons
                'pprint-fileset
                (cons (cons 'quote (cons fileset 'nil))
                      (cons file-name
                            (cons (cons 'quote
                                        (cons pretty-printing 'nil))
                                  '(state)))))
            'nil))
          'nil)
         '((acl2::value '(value-triple :invisible)))))
       'nil))))
   (cons 'progn
         (append progress-start?
                 (cons file-gen-event progress-end?))))))

Theorem: pseudo-event-formp-of-atc-gen-fileset-event

(defthm pseudo-event-formp-of-atc-gen-fileset-event
  (b*
   ((event (atc-gen-fileset-event fileset
                                  file-name pretty-printing print)))
   (pseudo-event-formp event))
  :rule-classes :rewrite)