• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
      • Transforms
        • Unparameterization
        • Elaborate
        • Addnames
        • Annotate
          • Increment-elim
          • Make-implicit-wires
          • Basic-bind-elim
          • Argresolve
          • Basicsanity
          • Portdecl-sign
          • Enum-names
            • Vl-enumname-range-declarations
            • Vl-interfacelist-add-enumname-declarations
            • Vl-packagelist-add-enumname-declarations
            • Vl-modulelist-add-enumname-declarations
            • Vl-classlist-add-enumname-declarations
            • Vl-enumitemlist-enumname-declarations
            • Vl-enumname-declarations
            • Vl-paramdecl-enumname-declarations
            • Vl-paramdecllist-enumname-declarations
            • Vl-vardecllist-enumname-declarations
            • Vl-typedeflist-enumname-declarations
            • Vl-typedef-enumname-declarations
            • Vl-vardecl-enumname-declarations
            • Vl-package-add-enumname-declarations
            • Vl-design-add-enumname-declarations
            • Vl-interface-add-enumname-declarations
            • Vl-class-add-enumname-declarations
            • Vl-module-add-enumname-declarations
            • Vl-datatype-map
          • Port-resolve
          • Udp-elim
          • Vl-annotate-design
          • Vl-annotate-module
        • Clean-warnings
        • Eliminitial
        • Custom-transform-hooks
        • Problem-modules
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Enum-names

Vl-enumitemlist-enumname-declarations

Signature

(vl-enumitemlist-enumname-declarations x lastval basetype atts loc) 
  → 
(mv warnings paramdecls)

Arguments

x — Guard (vl-enumitemlist-p x).

lastval — Guard (vl-expr-p lastval).

basetype — Guard (vl-datatype-p basetype).

atts — Guard (vl-atts-p atts).

loc — Guard (vl-location-p loc).

Returns

warnings — Type (vl-warninglist-p warnings).

paramdecls — Type (vl-paramdecllist-p paramdecls).

Definitions and Theorems

Function: vl-enumitemlist-enumname-declarations

(defun
    vl-enumitemlist-enumname-declarations
    (x lastval basetype atts loc)
    (declare (xargs :guard (and (vl-enumitemlist-p x)
                                (vl-expr-p lastval)
                                (vl-datatype-p basetype)
                                (vl-atts-p atts)
                                (vl-location-p loc))))
    (let ((__function__ 'vl-enumitemlist-enumname-declarations))
         (declare (ignorable __function__))
         (b* (((when (atom x)) (mv nil nil))
              ((mv warnings decls nextval)
               (vl-enumname-declarations (car x)
                                         lastval basetype atts loc))
              ((mv warnings-rest decls-rest)
               (vl-enumitemlist-enumname-declarations
                    (cdr x)
                    nextval basetype atts loc)))
             (mv (append-without-guard warnings warnings-rest)
                 (append-without-guard decls decls-rest)))))

Theorem: vl-warninglist-p-of-vl-enumitemlist-enumname-declarations.warnings

(defthm
  vl-warninglist-p-of-vl-enumitemlist-enumname-declarations.warnings
  (b* (((mv ?warnings ?paramdecls)
        (vl-enumitemlist-enumname-declarations
             x lastval basetype atts loc)))
      (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-paramdecllist-p-of-vl-enumitemlist-enumname-declarations.paramdecls

(defthm
 vl-paramdecllist-p-of-vl-enumitemlist-enumname-declarations.paramdecls
 (b* (((mv ?warnings ?paramdecls)
       (vl-enumitemlist-enumname-declarations
            x lastval basetype atts loc)))
     (vl-paramdecllist-p paramdecls))
 :rule-classes :rewrite)

Theorem: vl-enumitemlist-enumname-declarations-of-vl-enumitemlist-fix-x

(defthm
 vl-enumitemlist-enumname-declarations-of-vl-enumitemlist-fix-x
 (equal
   (vl-enumitemlist-enumname-declarations (vl-enumitemlist-fix x)
                                          lastval basetype atts loc)
   (vl-enumitemlist-enumname-declarations
        x lastval basetype atts loc)))

Theorem: vl-enumitemlist-enumname-declarations-vl-enumitemlist-equiv-congruence-on-x

(defthm
 vl-enumitemlist-enumname-declarations-vl-enumitemlist-equiv-congruence-on-x
 (implies (vl-enumitemlist-equiv x x-equiv)
          (equal (vl-enumitemlist-enumname-declarations
                      x lastval basetype atts loc)
                 (vl-enumitemlist-enumname-declarations
                      x-equiv lastval basetype atts loc)))
 :rule-classes :congruence)

Theorem: vl-enumitemlist-enumname-declarations-of-vl-expr-fix-lastval

(defthm
 vl-enumitemlist-enumname-declarations-of-vl-expr-fix-lastval
 (equal
      (vl-enumitemlist-enumname-declarations x (vl-expr-fix lastval)
                                             basetype atts loc)
      (vl-enumitemlist-enumname-declarations
           x lastval basetype atts loc)))

Theorem: vl-enumitemlist-enumname-declarations-vl-expr-equiv-congruence-on-lastval

(defthm
 vl-enumitemlist-enumname-declarations-vl-expr-equiv-congruence-on-lastval
 (implies (vl-expr-equiv lastval lastval-equiv)
          (equal (vl-enumitemlist-enumname-declarations
                      x lastval basetype atts loc)
                 (vl-enumitemlist-enumname-declarations
                      x lastval-equiv basetype atts loc)))
 :rule-classes :congruence)

Theorem: vl-enumitemlist-enumname-declarations-of-vl-datatype-fix-basetype

(defthm
   vl-enumitemlist-enumname-declarations-of-vl-datatype-fix-basetype
   (equal (vl-enumitemlist-enumname-declarations
               x lastval (vl-datatype-fix basetype)
               atts loc)
          (vl-enumitemlist-enumname-declarations
               x lastval basetype atts loc)))

Theorem: vl-enumitemlist-enumname-declarations-vl-datatype-equiv-congruence-on-basetype

(defthm
 vl-enumitemlist-enumname-declarations-vl-datatype-equiv-congruence-on-basetype
 (implies (vl-datatype-equiv basetype basetype-equiv)
          (equal (vl-enumitemlist-enumname-declarations
                      x lastval basetype atts loc)
                 (vl-enumitemlist-enumname-declarations
                      x lastval basetype-equiv atts loc)))
 :rule-classes :congruence)

Theorem: vl-enumitemlist-enumname-declarations-of-vl-atts-fix-atts

(defthm vl-enumitemlist-enumname-declarations-of-vl-atts-fix-atts
        (equal (vl-enumitemlist-enumname-declarations
                    x lastval basetype (vl-atts-fix atts)
                    loc)
               (vl-enumitemlist-enumname-declarations
                    x lastval basetype atts loc)))

Theorem: vl-enumitemlist-enumname-declarations-vl-atts-equiv-congruence-on-atts

(defthm
 vl-enumitemlist-enumname-declarations-vl-atts-equiv-congruence-on-atts
 (implies (vl-atts-equiv atts atts-equiv)
          (equal (vl-enumitemlist-enumname-declarations
                      x lastval basetype atts loc)
                 (vl-enumitemlist-enumname-declarations
                      x lastval basetype atts-equiv loc)))
 :rule-classes :congruence)

Theorem: vl-enumitemlist-enumname-declarations-of-vl-location-fix-loc

(defthm vl-enumitemlist-enumname-declarations-of-vl-location-fix-loc
        (equal (vl-enumitemlist-enumname-declarations
                    x lastval
                    basetype atts (vl-location-fix loc))
               (vl-enumitemlist-enumname-declarations
                    x lastval basetype atts loc)))

Theorem: vl-enumitemlist-enumname-declarations-vl-location-equiv-congruence-on-loc

(defthm
 vl-enumitemlist-enumname-declarations-vl-location-equiv-congruence-on-loc
 (implies (vl-location-equiv loc loc-equiv)
          (equal (vl-enumitemlist-enumname-declarations
                      x lastval basetype atts loc)
                 (vl-enumitemlist-enumname-declarations
                      x lastval basetype atts loc-equiv)))
 :rule-classes :congruence)