		Search-engine friendly clone of the ACL2 documentation.

Input-files-implementation

Input-files-complete-preprocess-extra-args

Extend the preprocessing arguments with a -std= flag.

Signature
(input-files-complete-preprocess-extra-args preprocess-extra-args ienv) → new-preprocess-extra-args
Arguments: preprocess-extra-args — Guard (or (acl2::string-stringlist-mapp preprocess-extra-args) (string-listp preprocess-extra-args)) .; ienv — Guard (ienvp ienv).
Returns: new-preprocess-extra-args — Type (or (acl2::string-stringlist-mapp new-preprocess-extra-args) (string-listp new-preprocess-extra-args)) .

If preprocess-extra-args is a string list, we cons the -std= flag to the front of the list. If it is an omap, we cons the flag to the front of each list in the omap value set.

Definitions and Theorems

Function: input-files-complete-preprocess-extra-args

(defun input-files-complete-preprocess-extra-args
       (preprocess-extra-args ienv)
 (declare
  (xargs
       :guard
       (and (or (acl2::string-stringlist-mapp preprocess-extra-args)
                (string-listp preprocess-extra-args))
            (ienvp ienv))))
 (let ((__function__ 'input-files-complete-preprocess-extra-args))
   (declare (ignorable __function__))
   (b*
    ((arg-std (input-files-preprocess-arg-std ienv))
     (string-listp
          (mbe :logic (string-listp preprocess-extra-args)
               :exec (or (endp preprocess-extra-args)
                         (stringp (first preprocess-extra-args))))))
    (if string-listp (cons arg-std preprocess-extra-args)
      (string-stringlist-map-map-cons-values
           arg-std preprocess-extra-args)))))

Theorem: return-type-of-input-files-complete-preprocess-extra-args

(defthm return-type-of-input-files-complete-preprocess-extra-args
  (b* ((new-preprocess-extra-args (input-files-complete-preprocess-extra-args
                                       preprocess-extra-args ienv)))
    (or (acl2::string-stringlist-mapp new-preprocess-extra-args)
        (string-listp new-preprocess-extra-args)))
  :rule-classes :rewrite)

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

(defthm
 string-stringlist-mapp-of-input-files-complete-preprocess-extra-args.new-preprocess-extra-args
 (b* ((?new-preprocess-extra-args (input-files-complete-preprocess-extra-args
                                       preprocess-extra-args ienv)))
   (equal (acl2::string-stringlist-mapp new-preprocess-extra-args)
          (not (string-listp preprocess-extra-args)))))

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

(defthm
 string-listp-of-input-files-complete-preprocess-extra-args.new-preprocess-extra-args
 (b* ((?new-preprocess-extra-args (input-files-complete-preprocess-extra-args
                                       preprocess-extra-args ienv)))
  (implies
      (not (acl2::string-stringlist-mapp new-preprocess-extra-args))
      (string-listp new-preprocess-extra-args))))