		Search-engine friendly clone of the ACL2 documentation.

Input-files-implementation

Input-files-process-preprocess

Process the :preprocess input.

Signature
(input-files-process-preprocess preprocess) → (mv erp preprocessor)
Returns: preprocessor — Type (string-optionp preprocessor).

Definitions and Theorems

Function: input-files-process-preprocess

(defun input-files-process-preprocess (preprocess)
 (declare (xargs :guard t))
 (let ((__function__ 'input-files-process-preprocess))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil)
    ((unless (input-files-preprocess-inputp preprocess))
     (reterr
      (msg
       "The :PREPROCESS input must be NIL, :AUTO, or a string, ~
                      but it is ~x0 instead."
       preprocess)))
    (preprocessor (if (eq preprocess :auto)
                      "gcc"
                    preprocess)))
   (retok preprocessor))))

Theorem: string-optionp-of-input-files-process-preprocess.preprocessor

(defthm
      string-optionp-of-input-files-process-preprocess.preprocessor
  (b* (((mv acl2::?erp ?preprocessor)
        (input-files-process-preprocess preprocess)))
    (string-optionp preprocessor))
  :rule-classes :rewrite)