• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • 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-follow-hidexpr
            • Vl-partselect-type-top-dimension-replacement
            • Vl-hidindex-datatype-resolve-dims
            • Vl-follow-hidexpr-error
            • Vl-follow-hidexpr-dimscheck
            • Vl-index-find-type
            • Vl-follow-hidexpr-dimcheck
            • Vl-partselect-expr-type
            • Vl-ss-find-hidexpr-range!!
            • Vl-hidstep
            • Vl-ss-find-hidexpr-range
            • Vl-genarrayblocklist-find-block
            • Vl-flatten-hidindex
            • Vl-hidexpr-resolved-p
            • Vl-flatten-hidexpr
            • Vl-hidindex-resolved-p
            • Vl-hidtrace
          • Vl-hidexpr-traverse-datatype
          • Abstract-hids
          • 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

• Following-hids

Vl-partselect-expr-type

Signature

(vl-partselect-expr-type x ss ctx) → (mv warning type)

Arguments

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

ss — Guard (vl-scopestack-p ss).

ctx — context.
    Guard (vl-context-p ctx).

Returns

warning — Type (iff (vl-warning-p warning) warning).

type — Type (implies (not warning) (vl-datatype-p type)).

Definitions and Theorems

Function: vl-partselect-expr-type

(defun vl-partselect-expr-type (x ss ctx)
 (declare (xargs :guard (and (vl-expr-p x)
                             (vl-scopestack-p ss)
                             (vl-context-p ctx))))
 (declare (xargs :guard (not (eq (vl-expr-kind x) :atom))))
 (let ((__function__ 'vl-partselect-expr-type))
  (declare (ignorable __function__))
  (b*
   ((ctx (vl-context-fix ctx))
    ((vl-nonatom x) (vl-expr-fix x))
    ((unless
      (member
         x.op
         '(:vl-select-colon
               :vl-select-pluscolon
               :vl-select-minuscolon :vl-partselect-colon
               :vl-partselect-pluscolon :vl-partselect-minuscolon)))
     (mv
      (make-vl-warning
       :type :vl-programming-error
       :msg
       "~a0: called vl-partselect-selfsize on non-partselect expr ~a1"
       :args (list ctx x)
       :fn __function__)
      nil))
    ((mv warning sub-type)
     (vl-index-find-type (first x.args)
                         ss ctx))
    ((when warning) (mv warning nil))
    (udims (vl-datatype->udims sub-type))
    (pdims (vl-datatype->pdims sub-type))
    ((unless (or (consp udims) (consp pdims)))
     (b*
      (((unless (vl-datatype-bitselect-ok sub-type))
        (mv
         (make-vl-warning
          :type :vl-bad-indexing-operator
          :msg
          "~a0: Can't apply an index operator to ~a1 because it ~
                         has no dimensions; its type is ~a2."
          :args (list ctx (first x.args) sub-type)
          :fn __function__)
         nil))
       ((mv warning size)
        (vl-datatype-size sub-type))
       ((when warning) (mv warning nil))
       (range (make-vl-range :msb (vl-make-index (1- size))
                             :lsb (vl-make-index 0)))
       ((mv warning new-dim1)
        (vl-partselect-type-top-dimension-replacement range x ctx))
       ((when warning) (mv warning nil))
       (new-type (make-vl-coretype :name :vl-logic
                                   :pdims (list new-dim1))))
      (mv nil new-type)))
    (dim1 (if (consp udims)
              (car udims)
            (car pdims)))
    ((mv warning new-dim1)
     (vl-partselect-type-top-dimension-replacement dim1 x ctx))
    ((when warning) (mv warning nil))
    (new-type
         (vl-datatype-update-dims (if (consp udims)
                                      pdims
                                    (cons new-dim1 (cdr pdims)))
                                  (and (consp udims)
                                       (cons new-dim1 (cdr udims)))
                                  sub-type))
    (new-type (if (consp udims)
                  new-type
                (vl-datatype-set-unsigned new-type))))
   (mv nil new-type))))

Theorem: return-type-of-vl-partselect-expr-type.warning

(defthm return-type-of-vl-partselect-expr-type.warning
  (b* (((mv common-lisp::?warning
            common-lisp::?type)
        (vl-partselect-expr-type x ss ctx)))
    (iff (vl-warning-p warning) warning))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-partselect-expr-type.type

(defthm return-type-of-vl-partselect-expr-type.type
  (b* (((mv common-lisp::?warning
            common-lisp::?type)
        (vl-partselect-expr-type x ss ctx)))
    (implies (not warning)
             (vl-datatype-p type)))
  :rule-classes :rewrite)

Theorem: context-irrelevance-of-vl-partselect-expr-type

(defthm context-irrelevance-of-vl-partselect-expr-type
 (implies
  (syntaxp
   (not
     (equal
          ctx
          (list 'quote
                (with-guard-checking :none (vl-context-fix nil))))))
  (and (equal (mv-nth 1 (vl-partselect-expr-type x ss ctx))
              (mv-nth 1 (vl-partselect-expr-type x ss nil)))
       (iff (mv-nth 0 (vl-partselect-expr-type x ss ctx))
            (mv-nth 0
                    (vl-partselect-expr-type x ss nil))))))

Theorem: vl-partselect-expr-type-of-vl-expr-fix-x

(defthm vl-partselect-expr-type-of-vl-expr-fix-x
  (equal (vl-partselect-expr-type (vl-expr-fix x)
                                  ss ctx)
         (vl-partselect-expr-type x ss ctx)))

Theorem: vl-partselect-expr-type-vl-expr-equiv-congruence-on-x

(defthm vl-partselect-expr-type-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-partselect-expr-type x ss ctx)
                  (vl-partselect-expr-type x-equiv ss ctx)))
  :rule-classes :congruence)

Theorem: vl-partselect-expr-type-of-vl-scopestack-fix-ss

(defthm vl-partselect-expr-type-of-vl-scopestack-fix-ss
  (equal (vl-partselect-expr-type x (vl-scopestack-fix ss)
                                  ctx)
         (vl-partselect-expr-type x ss ctx)))

Theorem: vl-partselect-expr-type-vl-scopestack-equiv-congruence-on-ss

(defthm vl-partselect-expr-type-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-partselect-expr-type x ss ctx)
                  (vl-partselect-expr-type x ss-equiv ctx)))
  :rule-classes :congruence)

Theorem: vl-partselect-expr-type-of-vl-context-fix-ctx

(defthm vl-partselect-expr-type-of-vl-context-fix-ctx
  (equal (vl-partselect-expr-type x ss (vl-context-fix ctx))
         (vl-partselect-expr-type x ss ctx)))

Theorem: vl-partselect-expr-type-vl-context-equiv-congruence-on-ctx

(defthm vl-partselect-expr-type-vl-context-equiv-congruence-on-ctx
  (implies (vl-context-equiv ctx ctx-equiv)
           (equal (vl-partselect-expr-type x ss ctx)
                  (vl-partselect-expr-type x ss ctx-equiv)))
  :rule-classes :congruence)