		Search-engine friendly clone of the ACL2 documentation.

Compilation-database

Comp-db-arguments-absolute-dirs

Signature
(comp-db-arguments-absolute-dirs directory arguments state) → arguments$
Arguments: directory — Guard (stringp directory).; arguments — Guard (comp-db-arg-listp arguments).
Returns: arguments$ — Type (comp-db-arg-listp arguments$).

Definitions and Theorems

Function: comp-db-arguments-absolute-dirs

(defun comp-db-arguments-absolute-dirs (directory arguments state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (stringp directory)
                             (comp-db-arg-listp arguments))))
 (b*
  ((directory (acl2::str-fix directory))
   (arguments (comp-db-arg-list-fix arguments))
   ((when (endp arguments)) nil)
   (argument (first arguments))
   ((comp-db-arg argument) argument)
   ((unless (member-equal argument.name *cc-options-dir*))
    (cons
         (comp-db-arg-fix argument)
         (comp-db-arguments-absolute-dirs directory (rest arguments)
                                          state)))
   (value
      (if argument.value
          (ec-call (extend-pathname directory argument.value state))
        argument.value))
   (value (if (stringp value)
              value
            argument.value)))
  (cons (change-comp-db-arg argument
                            :value value)
        (comp-db-arguments-absolute-dirs directory (rest arguments)
                                         state))))

Theorem: comp-db-arg-listp-of-comp-db-arguments-absolute-dirs

(defthm comp-db-arg-listp-of-comp-db-arguments-absolute-dirs
 (b*
  ((arguments$
       (comp-db-arguments-absolute-dirs directory arguments state)))
  (comp-db-arg-listp arguments$))
 :rule-classes :rewrite)

Theorem: comp-db-arguments-absolute-dirs-of-str-fix-directory

(defthm comp-db-arguments-absolute-dirs-of-str-fix-directory
  (equal
       (comp-db-arguments-absolute-dirs (acl2::str-fix directory)
                                        arguments state)
       (comp-db-arguments-absolute-dirs directory arguments state)))

Theorem: comp-db-arguments-absolute-dirs-streqv-congruence-on-directory

(defthm
     comp-db-arguments-absolute-dirs-streqv-congruence-on-directory
 (implies
  (acl2::streqv directory directory-equiv)
  (equal (comp-db-arguments-absolute-dirs directory arguments state)
         (comp-db-arguments-absolute-dirs
              directory-equiv arguments state)))
 :rule-classes :congruence)

Theorem: comp-db-arguments-absolute-dirs-of-comp-db-arg-list-fix-arguments

(defthm
  comp-db-arguments-absolute-dirs-of-comp-db-arg-list-fix-arguments
 (equal
   (comp-db-arguments-absolute-dirs directory
                                    (comp-db-arg-list-fix arguments)
                                    state)
   (comp-db-arguments-absolute-dirs directory arguments state)))

Theorem: comp-db-arguments-absolute-dirs-comp-db-arg-list-equiv-congruence-on-arguments

(defthm
 comp-db-arguments-absolute-dirs-comp-db-arg-list-equiv-congruence-on-arguments
 (implies
  (comp-db-arg-list-equiv arguments arguments-equiv)
  (equal (comp-db-arguments-absolute-dirs directory arguments state)
         (comp-db-arguments-absolute-dirs
              directory arguments-equiv state)))
 :rule-classes :congruence)