		Search-engine friendly clone of the ACL2 documentation.

Stv-hid-parse

Vl2014::vl-explode-hid

Explode a (resolved) vl2014::vl-hidexpr-p into a flat list of its components.

Signature
(vl2014::vl-explode-hid vl2014::x) → vl2014::pieces
Arguments: vl2014::x — The hidexpr to explode, e.g., foo.bar[2][3].baz.
Guard (vl2014::vl-expr-p vl2014::x).
Returns: vl2014::pieces — A flat, mixed list of strings and numbers, e.g., ("foo" "bar" 2 3 "baz").
Type (true-listp vl2014::pieces).

Definitions and Theorems

Function: vl-explode-hid

(defun vl2014::vl-explode-hid (vl2014::x)
 (declare (xargs :guard (vl2014::vl-expr-p vl2014::x)))
 (declare
     (xargs :guard (and (vl2014::vl-hidexpr-p vl2014::x)
                        (vl2014::vl-hidexpr-resolved-p vl2014::x))))
 (let ((__function__ 'vl2014::vl-explode-hid))
   (declare (ignorable __function__))
   (if (vl2014::vl-hidexpr->endp vl2014::x)
       (list (vl2014::vl-hidname->name vl2014::x))
     (append (vl2014::vl-explode-hidindex
                  (vl2014::vl-hidexpr->first vl2014::x))
             (vl2014::vl-explode-hid
                  (vl2014::vl-hidexpr->rest vl2014::x))))))

Theorem: true-listp-of-vl-explode-hid

(defthm vl2014::true-listp-of-vl-explode-hid
  (b* ((vl2014::pieces (vl2014::vl-explode-hid vl2014::x)))
    (true-listp vl2014::pieces))
  :rule-classes :type-prescription)