		Search-engine friendly clone of the ACL2 documentation.

Input-files-implementation

Input-files-gen-events

Generate the events.

Signature
(input-files-gen-events files path preprocessor preprocess-extra-args process const keep-going ienv progp state) → (mv erp events code state)
Arguments: files — Guard (string-listp files).; path — Guard (stringp path).; preprocessor — Guard (string-optionp preprocessor).; preprocess-extra-args — Guard (or (acl2::string-stringlist-mapp preprocess-extra-args) (string-listp preprocess-extra-args)) .; process — Guard (input-files-process-inputp process).; const — Guard (symbolp const).; keep-going — Guard (booleanp keep-going).; ienv — Guard (ienvp ienv).; progp — Guard (booleanp progp).
Returns: events — Type (pseudo-event-form-listp events).; code — Type (code-ensemblep code).

We perform all the necessary preprocessing and processing. Besides the events, we also return the code ensemble resulting from processing the (possibly preprocessed) files, together with the implementation environment. If the programmatic interface is being used, no events are actually generated.

Definitions and Theorems

Function: input-files-gen-events

(defun input-files-gen-events
       (files path preprocessor
              preprocess-extra-args process
              const keep-going ienv progp state)
 (declare (xargs :stobjs (state)))
 (declare
  (xargs
       :guard
       (and (string-listp files)
            (stringp path)
            (string-optionp preprocessor)
            (or (acl2::string-stringlist-mapp preprocess-extra-args)
                (string-listp preprocess-extra-args))
            (input-files-process-inputp process)
            (symbolp const)
            (booleanp keep-going)
            (ienvp ienv)
            (booleanp progp))))
 (let ((__function__ 'input-files-gen-events))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil (irr-code-ensemble) state)
    (events nil)
    ((erp files state)
     (if preprocessor
         (preprocess-files
              files
              :path path
              :preprocessor preprocessor
              :extra-args (input-files-complete-preprocess-extra-args
                               preprocess-extra-args ienv))
       (input-files-read-files files path state)))
    ((erp tunits)
     (parse-fileset files (ienv->version ienv)
                    keep-going))
    ((when (eq process :parse))
     (b*
      ((code (make-code-ensemble :transunits tunits
                                 :ienv ienv))
       (events
         (if (not progp)
             (rcons (cons 'defconst
                          (cons const
                                (cons (cons 'quote (cons code 'nil))
                                      'nil)))
                    events)
           events)))
      (retok events code state)))
    ((erp tunits)
     (dimb-transunit-ensemble tunits (ienv->gcc ienv)
                              keep-going))
    ((when (eq process :disambiguate))
     (b*
      ((code (make-code-ensemble :transunits tunits
                                 :ienv ienv))
       (events
         (if (not progp)
             (rcons (cons 'defconst
                          (cons const
                                (cons (cons 'quote (cons code 'nil))
                                      'nil)))
                    events)
           events)))
      (retok events code state)))
    ((erp tunits)
     (valid-transunit-ensemble tunits ienv keep-going))
    (code (make-code-ensemble :transunits tunits
                              :ienv ienv))
    (events
         (if (not progp)
             (rcons (cons 'defconst
                          (cons const
                                (cons (cons 'quote (cons code 'nil))
                                      'nil)))
                    events)
           events)))
   (retok events code state))))

Theorem: pseudo-event-form-listp-of-input-files-gen-events.events

(defthm pseudo-event-form-listp-of-input-files-gen-events.events
  (b* (((mv acl2::?erp ?events ?code acl2::?state)
        (input-files-gen-events files path preprocessor
                                preprocess-extra-args process
                                const keep-going ienv progp state)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)

Theorem: code-ensemblep-of-input-files-gen-events.code

(defthm code-ensemblep-of-input-files-gen-events.code
  (b* (((mv acl2::?erp ?events ?code acl2::?state)
        (input-files-gen-events files path preprocessor
                                preprocess-extra-args process
                                const keep-going ienv progp state)))
    (code-ensemblep code))
  :rule-classes :rewrite)

Theorem: code-ensemble-unambp-of-input-files-gen-events

(defthm code-ensemble-unambp-of-input-files-gen-events
 (implies
  (or (equal process :disambiguate)
      (equal process :validate))
  (b* (((mv acl2::?erp ?events ?code acl2::?state)
        (input-files-gen-events files path preprocessor
                                preprocess-extra-args process
                                const keep-going ienv progp state)))
    (implies (not erp)
             (code-ensemble-unambp code)))))