		Search-engine friendly clone of the ACL2 documentation.

Vl-value

Vl-value-p

Recognizer for vl-value structures.

Signature
(vl-value-p x) → *

Definitions and Theorems

Function: vl-value-p

(defun vl-value-p (x)
 (declare (xargs :guard t))
 (let ((__function__ 'vl-value-p))
  (declare (ignorable __function__))
  (and
   (consp x)
   (cond
    ((or (atom x) (eq (car x) :vl-constint))
     (and (std::prod-consp (cdr x))
          (std::prod-consp (std::prod-car (cdr x)))
          (std::prod-consp (std::prod-cdr (cdr x)))
          (b* ((origwidth (std::prod-car (std::prod-car (cdr x))))
               (value (std::prod-cdr (std::prod-car (cdr x))))
               (origsign (std::prod-car (std::prod-cdr (cdr x))))
               (wasunsized (std::prod-cdr (std::prod-cdr (cdr x)))))
            (and (posp origwidth)
                 (natp value)
                 (vl-exprsign-p origsign)
                 (booleanp wasunsized)
                 (unsigned-byte-p origwidth value)))))
    ((eq (car x) :vl-weirdint)
     (and (std::prod-consp (cdr x))
          (std::prod-consp (std::prod-cdr (cdr x)))
          (b* ((bits (std::prod-car (cdr x)))
               (origsign (std::prod-car (std::prod-cdr (cdr x))))
               (wasunsized (std::prod-cdr (std::prod-cdr (cdr x)))))
            (and (vl-bitlist-p bits)
                 (vl-exprsign-p origsign)
                 (booleanp wasunsized)
                 (consp bits)))))
    ((eq (car x) :vl-extint)
     (and (b* ((value (cdr x)))
            (vl-bit-p value))))
    ((eq (car x) :vl-real)
     (and (b* ((value (cdr x))) (stringp value))))
    ((eq (car x) :vl-time)
     (and (std::prod-consp (cdr x))
          (b* ((quantity (std::prod-car (cdr x)))
               (units (std::prod-cdr (cdr x))))
            (and (stringp quantity)
                 (vl-timeunit-p units)))))
    (t (and (eq (car x) :vl-string)
            (and)
            (b* ((value (cdr x)))
              (stringp value))))))))

Theorem: consp-when-vl-value-p

(defthm consp-when-vl-value-p
  (implies (vl-value-p x) (consp x))
  :rule-classes :compound-recognizer)