		Search-engine friendly clone of the ACL2 documentation.

Input-files-prog

Input-files-prog-fn

Implementation of input-files-prog.

Signature
(input-files-prog-fn 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 state) → (mv erp code state)
Arguments: files-presentp — Guard (booleanp files-presentp).; const-presentp — Guard (booleanp const-presentp).
Returns: code — Type (code-ensemblep code).

We set the flag progp for the programmatic interface to t. We ignore the event returned as result, and just return the artifacts.

Definitions and Theorems

Function: input-files-prog-fn

(defun input-files-prog-fn
       (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 state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (booleanp files-presentp)
                              (booleanp const-presentp))))
  (let ((__function__ 'input-files-prog-fn))
    (declare (ignorable __function__))
    (b* (((reterr) (irr-code-ensemble) state)
         ((erp & code 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 t state)))
      (retok code state))))

Theorem: code-ensemblep-of-input-files-prog-fn.code

(defthm code-ensemblep-of-input-files-prog-fn.code
  (b* (((mv acl2::?erp ?code acl2::?state)
        (input-files-prog-fn 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 state)))
    (code-ensemblep code))
  :rule-classes :rewrite)

Theorem: code-ensemble-unambp-of-input-files-prog-fn

(defthm code-ensemble-unambp-of-input-files-prog-fn
 (implies
   (or (equal process :disambiguate)
       (equal process :validate))
   (b* (((mv acl2::?erp ?code acl2::?state)
         (input-files-prog-fn 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 state)))
     (implies (not erp)
              (code-ensemble-unambp code)))))