		Search-engine friendly clone of the ACL2 documentation.

Input-files-implementation

Input-files-process-inputs-and-gen-events

Process the inputs and generate the events.

Signature
(input-files-process-inputs-and-gen-events files-presentp files path preprocess preprocess-args process const-presentp const keep-going std gcc short-bytes int-bytes long-bytes long-long-bytes plain-char-signed progp state) → (mv erp event code state)
Arguments: files-presentp — Guard (booleanp files-presentp).; const-presentp — Guard (booleanp const-presentp).; progp — Guard (booleanp progp).
Returns: event — Type (pseudo-event-formp event).; code — Type (code-ensemblep code).

The event is an empty progn if this is called via the programmatic interface. We also return the translation unit ensemble resulting from processing the (possibly preprocessed) files.

Definitions and Theorems

Function: input-files-process-inputs-and-gen-events

(defun input-files-process-inputs-and-gen-events
       (files-presentp files path preprocess
                       preprocess-args process const-presentp
                       const keep-going std gcc short-bytes
                       int-bytes long-bytes long-long-bytes
                       plain-char-signed progp state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (booleanp files-presentp)
                             (booleanp const-presentp)
                             (booleanp progp))))
 (let ((__function__ 'input-files-process-inputs-and-gen-events))
  (declare (ignorable __function__))
  (b* (((reterr)
        '(_)
        (irr-code-ensemble)
        state)
       ((erp files
             path preprocessor preprocess-extra-args
             process const keep-going ienv)
        (input-files-process-inputs
             files-presentp files path preprocess
             preprocess-args process const-presentp
             const keep-going std gcc short-bytes
             int-bytes long-bytes long-long-bytes
             plain-char-signed progp state))
       ((erp events code state)
        (input-files-gen-events files path preprocessor
                                preprocess-extra-args process
                                const keep-going ienv progp state)))
    (retok (cons 'progn events)
           code state))))

Theorem: pseudo-event-formp-of-input-files-process-inputs-and-gen-events.event

(defthm
 pseudo-event-formp-of-input-files-process-inputs-and-gen-events.event
 (b* (((mv acl2::?erp
           acl2::?event ?code acl2::?state)
       (input-files-process-inputs-and-gen-events
            files-presentp files path preprocess
            preprocess-args process const-presentp
            const keep-going std gcc short-bytes
            int-bytes long-bytes long-long-bytes
            plain-char-signed progp state)))
   (pseudo-event-formp event))
 :rule-classes :rewrite)

Theorem: code-ensemblep-of-input-files-process-inputs-and-gen-events.code

(defthm
   code-ensemblep-of-input-files-process-inputs-and-gen-events.code
  (b* (((mv acl2::?erp
            acl2::?event ?code acl2::?state)
        (input-files-process-inputs-and-gen-events
             files-presentp files path preprocess
             preprocess-args process const-presentp
             const keep-going std gcc short-bytes
             int-bytes long-bytes long-long-bytes
             plain-char-signed progp state)))
    (code-ensemblep code))
  :rule-classes :rewrite)

Theorem: code-ensemble-unambp-of-input-files-process-inputs-and-gen-events

(defthm
  code-ensemble-unambp-of-input-files-process-inputs-and-gen-events
  (implies (or (equal process :disambiguate)
               (equal process :validate))
           (b* (((mv acl2::?erp
                     acl2::?event ?code acl2::?state)
                 (input-files-process-inputs-and-gen-events
                      files-presentp files path preprocess
                      preprocess-args process const-presentp
                      const keep-going std gcc short-bytes
                      int-bytes long-bytes long-long-bytes
                      plain-char-signed progp state)))
             (implies (not erp)
                      (code-ensemble-unambp code)))))