		Search-engine friendly clone of the ACL2 documentation.

Vl-define

Vl-parse-cmdline-defines

Signature
(vl-parse-cmdline-defines x loc sticky) → (mv warnings defs)
Arguments: x — Guard (string-listp x).; loc — Guard (vl-location-p loc).; sticky — Guard (booleanp sticky).
Returns: warnings — Type (vl-warninglist-p warnings).; defs — Type (vl-defines-p defs).

Definitions and Theorems

Function: vl-parse-cmdline-defines

(defun vl-parse-cmdline-defines (x loc sticky)
 (declare (xargs :guard (and (string-listp x)
                             (vl-location-p loc)
                             (booleanp sticky))))
 (let ((__function__ 'vl-parse-cmdline-defines))
  (declare (ignorable __function__))
  (b*
   (((mv warnings defs)
     (vl-parse-cmdline-defines-aux x loc sticky))
    (dupes
         (duplicated-members (vl-defines->names (mergesort defs))))
    (warnings (if (not dupes)
                  (ok)
                (fatal :type :vl-bad-defines
                       :msg "Conflict command-line defines for ~&0."
                       :args (list dupes)))))
   (mv warnings defs))))

Theorem: vl-warninglist-p-of-vl-parse-cmdline-defines.warnings

(defthm vl-warninglist-p-of-vl-parse-cmdline-defines.warnings
  (b* (((mv ?warnings ?defs)
        (vl-parse-cmdline-defines x loc sticky)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-defines-p-of-vl-parse-cmdline-defines.defs

(defthm vl-defines-p-of-vl-parse-cmdline-defines.defs
  (b* (((mv ?warnings ?defs)
        (vl-parse-cmdline-defines x loc sticky)))
    (vl-defines-p defs))
  :rule-classes :rewrite)

Theorem: vl-parse-cmdline-defines-of-string-list-fix-x

(defthm vl-parse-cmdline-defines-of-string-list-fix-x
  (equal (vl-parse-cmdline-defines (string-list-fix x)
                                   loc sticky)
         (vl-parse-cmdline-defines x loc sticky)))

Theorem: vl-parse-cmdline-defines-string-list-equiv-congruence-on-x

(defthm vl-parse-cmdline-defines-string-list-equiv-congruence-on-x
  (implies (str::string-list-equiv x x-equiv)
           (equal (vl-parse-cmdline-defines x loc sticky)
                  (vl-parse-cmdline-defines x-equiv loc sticky)))
  :rule-classes :congruence)

Theorem: vl-parse-cmdline-defines-of-vl-location-fix-loc

(defthm vl-parse-cmdline-defines-of-vl-location-fix-loc
  (equal (vl-parse-cmdline-defines x (vl-location-fix loc)
                                   sticky)
         (vl-parse-cmdline-defines x loc sticky)))

Theorem: vl-parse-cmdline-defines-vl-location-equiv-congruence-on-loc

(defthm vl-parse-cmdline-defines-vl-location-equiv-congruence-on-loc
  (implies (vl-location-equiv loc loc-equiv)
           (equal (vl-parse-cmdline-defines x loc sticky)
                  (vl-parse-cmdline-defines x loc-equiv sticky)))
  :rule-classes :congruence)

Theorem: vl-parse-cmdline-defines-of-bool-fix-sticky

(defthm vl-parse-cmdline-defines-of-bool-fix-sticky
  (equal (vl-parse-cmdline-defines x loc (acl2::bool-fix sticky))
         (vl-parse-cmdline-defines x loc sticky)))

Theorem: vl-parse-cmdline-defines-iff-congruence-on-sticky

(defthm vl-parse-cmdline-defines-iff-congruence-on-sticky
  (implies (iff sticky sticky-equiv)
           (equal (vl-parse-cmdline-defines x loc sticky)
                  (vl-parse-cmdline-defines x loc sticky-equiv)))
  :rule-classes :congruence)