		Search-engine friendly clone of the ACL2 documentation.

Compilation-database

Comp-db-arguments-escape-for-shell

Signature
(comp-db-arguments-escape-for-shell arguments) → arguments$
Arguments: arguments — Guard (comp-db-arg-listp arguments).
Returns: arguments$ — Type (comp-db-arg-listp arguments$).

Definitions and Theorems

Function: comp-db-arguments-escape-for-shell

(defun comp-db-arguments-escape-for-shell (arguments)
 (declare (xargs :guard (comp-db-arg-listp arguments)))
 (b*
  ((arguments (comp-db-arg-list-fix arguments))
   ((when (endp arguments)) nil)
   (argument (first arguments))
   ((comp-db-arg argument) argument)
   (argument$
    (change-comp-db-arg
         argument :name
         (string-escape-for-shell argument.name)
         :value
         (if argument.value (string-escape-for-shell argument.value)
           nil))))
  (cons argument$
        (comp-db-arguments-escape-for-shell (rest arguments)))))

Theorem: comp-db-arg-listp-of-comp-db-arguments-escape-for-shell

(defthm comp-db-arg-listp-of-comp-db-arguments-escape-for-shell
  (b* ((arguments$ (comp-db-arguments-escape-for-shell arguments)))
    (comp-db-arg-listp arguments$))
  :rule-classes :rewrite)

Theorem: comp-db-arguments-escape-for-shell-of-comp-db-arg-list-fix-arguments

(defthm
 comp-db-arguments-escape-for-shell-of-comp-db-arg-list-fix-arguments
 (equal (comp-db-arguments-escape-for-shell
             (comp-db-arg-list-fix arguments))
        (comp-db-arguments-escape-for-shell arguments)))

Theorem: comp-db-arguments-escape-for-shell-comp-db-arg-list-equiv-congruence-on-arguments

(defthm
 comp-db-arguments-escape-for-shell-comp-db-arg-list-equiv-congruence-on-arguments
 (implies
      (comp-db-arg-list-equiv arguments arguments-equiv)
      (equal (comp-db-arguments-escape-for-shell arguments)
             (comp-db-arguments-escape-for-shell arguments-equiv)))
 :rule-classes :congruence)