		Search-engine friendly clone of the ACL2 documentation.

Vl-define

Vl-parse-cmdline-defines-aux

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

Definitions and Theorems

Function: vl-parse-cmdline-defines-aux

(defun vl-parse-cmdline-defines-aux (x loc stickyp)
  (declare (xargs :guard (and (string-listp x)
                              (vl-location-p loc)
                              (booleanp stickyp))))
  (let ((__function__ 'vl-parse-cmdline-defines-aux))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (mv nil nil))
         ((mv okp name first)
          (vl-parse-cmdline-define (car x)
                                   loc stickyp))
         ((mv warnings rest)
          (vl-parse-cmdline-defines-aux (cdr x)
                                        loc stickyp))
         ((when okp)
          (mv warnings
              (vl-add-define name first rest))))
      (mv (fatal :type :vl-bad-define
                 :msg "Error parsing command-line define: ~s0"
                 :args (list (string-fix (car x))))
          rest))))

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: vl-parse-cmdline-defines-aux-of-bool-fix-stickyp

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

Theorem: vl-parse-cmdline-defines-aux-iff-congruence-on-stickyp

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