		Search-engine friendly clone of the ACL2 documentation.

Vl-unhierarchicalize-interfaceport

Vl-hidexpr-split-right

Split off the rightmost part of a hierarchical identifier.

Signature
(vl-hidexpr-split-right x) → (mv successp prefix indices lastname)
Arguments: x — Expression to split, say foo.bar or elf.cow[3][4].horse.
Guard (vl-hidexpr-p x).
Returns: successp — We fail if this is an atomic HID expression like foo since then there's nothing to split. We also fail if we're given a HID like $root.foo, because $root isn't a valid vl-hidexpr by itself.
Type (booleanp successp).; prefix — On success: everything up to the final indexing/name. For instance, foo or elf.cow in the above examples.
Type (vl-hidexpr-p prefix).; indices — On success: any next-to-last indexing that is also chopped off. For instance, NIL and [3][4] in the above examples.
Type (vl-exprlist-p indices).; lastname — On success: the final name that was chopped off, e.g., bar or horse in the above examples.
Type (stringp lastname).

Definitions and Theorems

Function: vl-hidexpr-split-right

(defun vl-hidexpr-split-right (x)
 (declare (xargs :guard (vl-hidexpr-p x)))
 (let ((__function__ 'vl-hidexpr-split-right))
  (declare (ignorable __function__))
  (let ((x (vl-hidexpr-fix x)))
   (vl-hidexpr-case
       x
       :end (mv nil x nil "")
       :dot
       (vl-hidexpr-case
            x.rest :end
            (b* ((name1 (vl-hidindex->name x.first))
                 ((unless (stringp name1))
                  (mv nil x nil ""))
                 (prefix (make-vl-hidexpr-end :name name1)))
              (mv t prefix (vl-hidindex->indices x.first)
                  (vl-hidexpr-end->name x.rest)))
            :dot
            (b* (((mv rest-okp
                      rest-prefix rest-indices rest-lastname)
                  (vl-hidexpr-split-right x.rest))
                 (prefix (change-vl-hidexpr-dot x
                                                :rest rest-prefix)))
              (mv rest-okp
                  prefix rest-indices rest-lastname)))))))

Theorem: booleanp-of-vl-hidexpr-split-right.successp

(defthm booleanp-of-vl-hidexpr-split-right.successp
  (b* (((mv ?successp ?prefix ?indices ?lastname)
        (vl-hidexpr-split-right x)))
    (booleanp successp))
  :rule-classes :rewrite)

Theorem: vl-hidexpr-p-of-vl-hidexpr-split-right.prefix

(defthm vl-hidexpr-p-of-vl-hidexpr-split-right.prefix
  (b* (((mv ?successp ?prefix ?indices ?lastname)
        (vl-hidexpr-split-right x)))
    (vl-hidexpr-p prefix))
  :rule-classes :rewrite)

Theorem: vl-exprlist-p-of-vl-hidexpr-split-right.indices

(defthm vl-exprlist-p-of-vl-hidexpr-split-right.indices
  (b* (((mv ?successp ?prefix ?indices ?lastname)
        (vl-hidexpr-split-right x)))
    (vl-exprlist-p indices))
  :rule-classes :rewrite)

Theorem: stringp-of-vl-hidexpr-split-right.lastname

(defthm stringp-of-vl-hidexpr-split-right.lastname
  (b* (((mv ?successp ?prefix ?indices ?lastname)
        (vl-hidexpr-split-right x)))
    (stringp lastname))
  :rule-classes :rewrite)

Theorem: vl-hidexpr-split-right-of-vl-hidexpr-fix-x

(defthm vl-hidexpr-split-right-of-vl-hidexpr-fix-x
  (equal (vl-hidexpr-split-right (vl-hidexpr-fix x))
         (vl-hidexpr-split-right x)))

Theorem: vl-hidexpr-split-right-vl-hidexpr-equiv-congruence-on-x

(defthm vl-hidexpr-split-right-vl-hidexpr-equiv-congruence-on-x
  (implies (vl-hidexpr-equiv x x-equiv)
           (equal (vl-hidexpr-split-right x)
                  (vl-hidexpr-split-right x-equiv)))
  :rule-classes :congruence)