		Search-engine friendly clone of the ACL2 documentation.

Input-files-implementation

Input-files-process-preprocess-args

Process the :preprocess-args input.

Signature
(input-files-process-preprocess-args preprocessor preprocess-args state) → (mv erp preprocess-extra-args)
Arguments: preprocessor — Guard (string-optionp preprocessor).
Returns: preprocess-extra-args — Type (or (string-listp preprocess-extra-args) (acl2::string-stringlist-mapp preprocess-extra-args)) .

The preprocessor input to this function is the result of processing the :preprocess input. If it is nil, the :preprocess-args input is expected to also be nil.

If processing of the :preprocess-args input is successful, we return its value, which is either a string list or an omap from strings to string lists. This value is passed as part of the :extra-args input of preprocess-files, which justifies the name of the result.

Definitions and Theorems

Function: input-files-process-preprocess-args

(defun input-files-process-preprocess-args
       (preprocessor preprocess-args state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (string-optionp preprocessor)))
 (declare (ignore state))
 (let ((__function__ 'input-files-process-preprocess-args))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil)
    ((when (and (not preprocessor)
                preprocess-args))
     (reterr
      (msg
       "Since the :PREPROCESS input is NIL, ~
                      the :PREPROCESS-ARGS input must also be NIL, ~
                      but it is ~x0 instead."
       preprocess-args)))
    ((unless (or (string-listp preprocess-args)
                 (acl2::string-stringlist-mapp preprocess-args)))
     (reterr
      (msg
       "The :PREPROCESS-ARGS input must evaluate to ~
                      a list of strings ~
                      or an omap associating strings to lists of strings, ~
                      but it evaluates to ~x0 instead."
       preprocess-args))))
   (retok preprocess-args))))

Theorem: return-type-of-input-files-process-preprocess-args.preprocess-extra-args

(defthm
 return-type-of-input-files-process-preprocess-args.preprocess-extra-args
 (b* (((mv acl2::?erp ?preprocess-extra-args)
       (input-files-process-preprocess-args
            preprocessor preprocess-args state)))
   (or (string-listp preprocess-extra-args)
       (acl2::string-stringlist-mapp preprocess-extra-args)))
 :rule-classes :rewrite)

Theorem: string-listp-of-input-files-process-preprocess-args.preprocess-extra-args

(defthm
 string-listp-of-input-files-process-preprocess-args.preprocess-extra-args
 (b* (((mv acl2::?erp ?preprocess-extra-args)
       (input-files-process-preprocess-args
            preprocessor preprocess-args state)))
   (implies
        (not (acl2::string-stringlist-mapp preprocess-extra-args))
        (string-listp preprocess-extra-args))))

Theorem: string-stringlist-mapp-of-input-files-process-preprocess-args.preprocess-extra-args

(defthm
 string-stringlist-mapp-of-input-files-process-preprocess-args.preprocess-extra-args
 (b* (((mv acl2::?erp ?preprocess-extra-args)
       (input-files-process-preprocess-args
            preprocessor preprocess-args state)))
   (implies (not (string-listp preprocess-extra-args))
            (acl2::string-stringlist-mapp preprocess-extra-args))))