Split off the rightmost part of a hierarchical identifier.
(vl-hidexpr-split-right x) → (mv successp prefix indices lastname)
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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)