• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
        • Getting-started
        • Utilities
        • Loader
        • Transforms
        • Lint
        • Mlib
          • Scopestack
          • Filtering-by-name
          • Vl-namefactory
          • Substitution
          • Allexprs
          • Hid-tools
            • Following-hids
            • Vl-hidexpr-traverse-datatype
            • Abstract-hids
              • Vl-hidexpr-p
              • Vl-hidindex-p
              • Vl-hidexpr-collect-indices
              • Vl-hidindex->indices
                • Vl-hidindex->indices-exec
              • Vl-hidexpr->rest
              • Vl-indexexpr->indices
              • Vl-hidexpr->first
              • Vl-indexexpr->scopeexpr
              • Vl-scopeexpr->scopes
              • Vl-hidname-p
              • Vl-hidexpr->endp
              • Vl-scopeexpr->hid
              • Vl-hidname->name
              • Vl-hidindex->name
              • Vl-hidindex-count-indices
              • Vl-scopeexpr-p
              • Vl-scopeatom->name
              • Vl-scopename-p
              • Vl-scopename-fix
              • Vl-indexexpr-p
              • Vl-fast-keyguts-p
              • Vl-scopeatom-p
              • Vl-scopenamelist
            • Vl-hidexpr-find-type
          • Vl-consteval
          • Range-tools
          • Lvalexprs
          • Hierarchy
          • Finding-by-name
          • Expr-tools
          • Expr-slicing
          • Stripping-functions
          • Stmt-tools
          • Modnamespace
          • Vl-parse-expr-from-str
          • Welltyped
          • Reordering-by-name
          • Flat-warnings
          • Genblob
          • Expr-building
          • Datatype-tools
          • Syscalls
          • Relocate
          • Expr-cleaning
          • Namemangle
          • Caremask
          • Port-tools
          • Lvalues
        • Server
        • Kit
        • Printer
        • Esim-vl
        • Well-formedness
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Abstract-hids

Vl-hidindex->indices

For instance, bar[3][4][5] → (3 4 5).

Signature
(vl-hidindex->indices x) → indices
Arguments
x — Guard (vl-expr-p x).
Returns
indices — Type (vl-exprlist-p indices).

Definitions and Theorems

Function: vl-hidindex->indices$inline

(defun vl-hidindex->indices$inline (x)
  (declare (xargs :guard (vl-expr-p x)))
  (declare (xargs :guard (vl-hidindex-p x)))
  (let ((__function__ 'vl-hidindex->indices))
    (declare (ignorable __function__))
    (mbe :logic
         (b* (((when (vl-atom-p x)) nil)
              ((vl-nonatom x) x))
           (append (vl-hidindex->indices (first x.args))
                   (list (vl-expr-fix (second x.args)))))
         :exec (vl-hidindex->indices-exec x nil))))

Theorem: vl-exprlist-p-of-vl-hidindex->indices

(defthm vl-exprlist-p-of-vl-hidindex->indices
  (b* ((indices (vl-hidindex->indices$inline x)))
    (vl-exprlist-p indices))
  :rule-classes :rewrite)

Theorem: vl-hidindex->indices-when-vl-atom-p

(defthm vl-hidindex->indices-when-vl-atom-p
  (implies (vl-atom-p x)
           (equal (vl-hidindex->indices x) nil)))

Theorem: vl-exprlist-count-of-vl-hidindex->indices-weak

(defthm vl-exprlist-count-of-vl-hidindex->indices-weak
  (implies (vl-hidindex-p x)
           (<= (vl-exprlist-count (vl-hidindex->indices x))
               (vl-expr-count x)))
  :rule-classes ((:rewrite) (:linear)))

Theorem: vl-exprlist-count-of-vl-hidindex->indices-strong

(defthm vl-exprlist-count-of-vl-hidindex->indices-strong
  (implies (and (vl-hidindex-p x)
                (not (vl-atom-p x)))
           (< (vl-exprlist-count (vl-hidindex->indices x))
              (vl-expr-count x)))
  :rule-classes ((:rewrite) (:linear)))

Theorem: vl-hidindex->indices$inline-of-vl-expr-fix-x

(defthm vl-hidindex->indices$inline-of-vl-expr-fix-x
  (equal (vl-hidindex->indices$inline (vl-expr-fix x))
         (vl-hidindex->indices$inline x)))

Theorem: vl-hidindex->indices$inline-vl-expr-equiv-congruence-on-x

(defthm vl-hidindex->indices$inline-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-hidindex->indices$inline x)
                  (vl-hidindex->indices$inline x-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-hidindex->indices-exec