• 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
        • Expression-sizing
          • Expression-sizing-minutia
          • Expression-sizing-intro
          • Vl-keyvalue-pattern-collect-array-replacements
          • Vl-assignpattern-positional-replacement
          • Vl-plainarg-exprsize
          • Vl-assignpattern-keyvalue-replacement
          • Vl-keyvalue-pattern-collect-struct-replacements
          • Vl-modulelist-exprsize
          • Vl-expr-assignpattern-extend/truncate
          • Vl-structmemberlist->types
          • Vl-expr-size
          • Vl-expr-selfdetermine-type
          • Vl-assignpattern-multi-replacement
          • Vl-parse-keyval-pattern-struct
          • Vl-plainarglist-exprsize
          • Vl-parse-keyval-pattern-array
          • Vl-warn-about-implicit-extension
          • Vl-assigncontext-size
          • Vl-arguments-exprsize
          • Vl-assignpattern-replacement
          • Vl-packeddimensionlist-exprsize
          • Vl-namedparamvaluelist-exprsize
          • Vl-maybe-delayoreventcontrol-exprsize
          • Vl-repeateventcontrol-exprsize
          • Vl-paramvaluelist-exprsize
          • Vl-maybe-packeddimension-exprsize
          • Vl-delayoreventcontrol-exprsize
          • Vl-namedparamvalue-exprsize
          • Vl-namedarglist-exprsize
          • Vl-enumitemlist-exprsize
          • Vl-packeddimension-exprsize
          • Vl-maybe-paramvalue-exprsize
          • Vl-evatomlist-exprsize
          • Vl-atom-selfdetermine-type
          • Vl-rangelist-exprsize
          • Vl-maybe-gatedelay-exprsize
          • Vl-maybe-datatype-exprsize
          • Vl-gatedelay-exprsize
          • Vl-paramargs-exprsize
          • Vl-namedarg-exprsize
          • Vl-eventcontrol-exprsize
          • Vl-enumbasetype-exprsize
          • Vl-delaycontrol-exprsize
          • Vl-paramvalue-exprsize
          • Vl-maybe-range-exprsize
          • Vl-enumitem-exprsize
          • Vl-range-exprsize
          • Vl-paramdecl-exprsize
          • Vl-paramdecllist-exprsize
          • Vl-maybe-expr-size
          • Vl-evatom-exprsize
          • Vl-vardecllist-exprsize
          • Vl-portdecllist-exprsize
          • Vl-modinstlist-exprsize
          • Vl-initiallist-exprsize
          • Vl-gateinstlist-exprsize
          • Vl-fundecllist-exprsize
          • Vl-assign-exprsize
          • Vl-interfaceport-exprsize
          • Vl-assignlist-exprsize
          • Vl-alwayslist-exprsize
          • Vl-portlist-exprsize
          • Vl-modinst-exprsize
          • Vl-gateinst-exprsize
          • Vl-fundecl-exprsize
          • Vl-vardecl-exprsize
          • Vl-regularport-exprsize
          • Vl-portdecl-exprsize
          • Vl-initial-exprsize
          • Vl-always-exprsize
          • Vl-port-exprsize
          • Vl-lvalue-type
          • Vl-classify-extension-warning-hook
          • Welltyped
          • Vl-castexpr->datatype
          • Vl-expr-size-assigncontext
          • Vl-type-expr-pairs-sum-datatype-sizes
          • Vl-basictype->datatype
          • Vl-expr-replace-assignpatterns
          • Vl-design-exprsize
          • Vl-op-simple-vector-p
          • Vl-expr-val-alist-max-count
          • Vl-expr-has-patterns
          • Vl-exprlist-max-count
          • Vl-unsigned-when-size-zero-lst
          • Vl-type-expr-pairs
          • Append-n
          • Vl-expr-val-alist
          • Vl-datatypelist
        • Occform
        • Oprewrite
        • Expand-functions
        • Delayredux
        • Unparameterization
        • Caseelim
        • Split
        • Selresolve
        • Weirdint-elim
        • Vl-delta
        • Replicate-insts
        • Rangeresolve
        • Propagate
        • Clean-selects
        • Clean-params
        • Blankargs
        • Inline-mods
        • Expr-simp
        • Trunc
        • Always-top
        • Gatesplit
        • Gate-elim
        • Expression-optimization
        • Elim-supplies
        • Wildelim
        • Drop-blankports
        • Clean-warnings
        • Addinstnames
        • Custom-transform-hooks
        • Annotate
        • Latchcode
        • Elim-unused-vars
        • Problem-modules
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Expression-sizing

Vl-assignpattern-keyvalue-replacement

Return the list of type/expression pairs to concatenate together to replace a key/value assignment pattern.

Signature

(vl-assignpattern-keyvalue-replacement 
     lhs-type fields orig-x ctx warnings) 
 
  → 
(mv successp pairs new-warnings)

Arguments

lhs-type — Guard (vl-datatype-p lhs-type).

fields — Guard (vl-exprlist-p fields).

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

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

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

Returns

successp — Type (booleanp successp).

pairs — Type (vl-type-expr-pairs-p pairs).

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

Definitions and Theorems

Function: vl-assignpattern-keyvalue-replacement

(defun vl-assignpattern-keyvalue-replacement
       (lhs-type fields orig-x ctx warnings)
 (declare (xargs :guard (and (vl-datatype-p lhs-type)
                             (vl-exprlist-p fields)
                             (vl-expr-p orig-x)
                             (vl-context-p ctx)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-assignpattern-keyvalue-replacement))
  (declare (ignorable __function__))
  (b*
   ((warnings (vl-warninglist-fix warnings))
    (ctx (vl-context-fix ctx))
    (orig-x (vl-expr-fix orig-x))
    (pdims (vl-datatype->pdims lhs-type))
    (udims (vl-datatype->udims lhs-type))
    ((unless (or (consp udims) (consp pdims)))
     (b*
      (((unless (eq (vl-datatype-kind lhs-type)
                    :vl-struct))
        (mv
         nil nil
         (warn
          :type :vl-assignpattern-elim-fail
          :msg
          "~a0: Positional assignment pattern must be in a ~
                              struct or array type context: ~a1"
          :args (list (vl-context-fix ctx)
                      (vl-expr-fix orig-x)))))
       ((vl-struct lhs-type))
       ((mv ok alist warnings)
        (vl-parse-keyval-pattern-struct
             fields
             lhs-type.members orig-x ctx warnings))
       ((unless ok) (mv nil nil warnings))
       ((unless (uniquep (alist-keys alist)))
        (mv
         nil nil
         (warn :type :vl-assignpattern-elim-fail
               :msg "~a0: Duplicate keys in assignment pattern: ~a1"
               :args (list ctx orig-x)))))
      (vl-keyvalue-pattern-collect-struct-replacements
           lhs-type.members
           alist orig-x ctx warnings)))
    (dim (if (consp udims)
             (car udims)
           (car pdims)))
    ((unless (and (not (eq dim :vl-unsized-dimension))
                  (vl-range-resolved-p dim)))
     (mv
      nil nil
      (warn
        :type :vl-assignpattern-elim-fail
        :msg "~a0: Unresolved packed dimensions in LHS datatype ~a1"
        :args (list (vl-context-fix ctx)
                    (vl-datatype-fix lhs-type)))))
    ((mv ok alist warnings)
     (vl-parse-keyval-pattern-array fields dim orig-x ctx warnings))
    ((unless ok) (mv nil nil warnings))
    ((unless (uniquep (alist-keys alist)))
     (mv nil nil
         (warn :type :vl-assignpattern-elim-fail
               :msg "~a0: Duplicate keys in assignment pattern: ~a1"
               :args (list ctx orig-x))))
    (new-datatype (if (consp udims)
                      (vl-datatype-update-dims pdims (cdr udims)
                                               lhs-type)
                    (vl-datatype-update-dims (cdr pdims)
                                             nil lhs-type)))
    (msb (vl-resolved->val (vl-range->msb dim)))
    (lsb (vl-resolved->val (vl-range->lsb dim)))
    (direction (if (< msb lsb) 1 -1)))
   (vl-keyvalue-pattern-collect-array-replacements
        (vl-range-size dim)
        msb direction new-datatype
        alist orig-x ctx warnings))))

Theorem: booleanp-of-vl-assignpattern-keyvalue-replacement.successp

(defthm booleanp-of-vl-assignpattern-keyvalue-replacement.successp
  (b* (((mv ?successp ?pairs ?new-warnings)
        (vl-assignpattern-keyvalue-replacement
             lhs-type fields orig-x ctx warnings)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: vl-type-expr-pairs-p-of-vl-assignpattern-keyvalue-replacement.pairs

(defthm
 vl-type-expr-pairs-p-of-vl-assignpattern-keyvalue-replacement.pairs
 (b* (((mv ?successp ?pairs ?new-warnings)
       (vl-assignpattern-keyvalue-replacement
            lhs-type fields orig-x ctx warnings)))
   (vl-type-expr-pairs-p pairs))
 :rule-classes :rewrite)

Theorem: vl-warninglist-p-of-vl-assignpattern-keyvalue-replacement.new-warnings

(defthm
 vl-warninglist-p-of-vl-assignpattern-keyvalue-replacement.new-warnings
 (b* (((mv ?successp ?pairs ?new-warnings)
       (vl-assignpattern-keyvalue-replacement
            lhs-type fields orig-x ctx warnings)))
   (vl-warninglist-p new-warnings))
 :rule-classes :rewrite)

Theorem: vl-exprlist-max-count-of-vl-assignpattern-keyvalue-replacement

(defthm
     vl-exprlist-max-count-of-vl-assignpattern-keyvalue-replacement
 (<
  (vl-exprlist-max-count
    (alist-vals (mv-nth 1
                        (vl-assignpattern-keyvalue-replacement
                             lhs-type fields orig-x ctx warnings))))
  (vl-exprlist-count fields))
 :rule-classes :linear)

Theorem: sum-sizes-of-vl-assignpattern-keyvalue-replacement

(defthm sum-sizes-of-vl-assignpattern-keyvalue-replacement
  (b* (((mv ok pairs &)
        (vl-assignpattern-keyvalue-replacement
             lhs-type fields orig-x ctx warnings))
       ((mv warning size)
        (vl-datatype-size lhs-type))
       ((mv warning1 size-sum)
        (vl-type-expr-pairs-sum-datatype-sizes pairs)))
    (implies (and ok (not warning))
             (and (not warning1)
                  (equal size-sum size)))))

Theorem: vl-assignpattern-keyvalue-replacement-of-vl-datatype-fix-lhs-type

(defthm
  vl-assignpattern-keyvalue-replacement-of-vl-datatype-fix-lhs-type
 (equal
  (vl-assignpattern-keyvalue-replacement (vl-datatype-fix lhs-type)
                                         fields orig-x ctx warnings)
  (vl-assignpattern-keyvalue-replacement
       lhs-type fields orig-x ctx warnings)))

Theorem: vl-assignpattern-keyvalue-replacement-vl-datatype-equiv-congruence-on-lhs-type

(defthm
 vl-assignpattern-keyvalue-replacement-vl-datatype-equiv-congruence-on-lhs-type
 (implies (vl-datatype-equiv lhs-type lhs-type-equiv)
          (equal (vl-assignpattern-keyvalue-replacement
                      lhs-type fields orig-x ctx warnings)
                 (vl-assignpattern-keyvalue-replacement
                      lhs-type-equiv
                      fields orig-x ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-assignpattern-keyvalue-replacement-of-vl-exprlist-fix-fields

(defthm
    vl-assignpattern-keyvalue-replacement-of-vl-exprlist-fix-fields
  (equal (vl-assignpattern-keyvalue-replacement
              lhs-type (vl-exprlist-fix fields)
              orig-x ctx warnings)
         (vl-assignpattern-keyvalue-replacement
              lhs-type fields orig-x ctx warnings)))

Theorem: vl-assignpattern-keyvalue-replacement-vl-exprlist-equiv-congruence-on-fields

(defthm
 vl-assignpattern-keyvalue-replacement-vl-exprlist-equiv-congruence-on-fields
 (implies (vl-exprlist-equiv fields fields-equiv)
          (equal (vl-assignpattern-keyvalue-replacement
                      lhs-type fields orig-x ctx warnings)
                 (vl-assignpattern-keyvalue-replacement
                      lhs-type
                      fields-equiv orig-x ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-assignpattern-keyvalue-replacement-of-vl-expr-fix-orig-x

(defthm vl-assignpattern-keyvalue-replacement-of-vl-expr-fix-orig-x
  (equal (vl-assignpattern-keyvalue-replacement
              lhs-type fields (vl-expr-fix orig-x)
              ctx warnings)
         (vl-assignpattern-keyvalue-replacement
              lhs-type fields orig-x ctx warnings)))

Theorem: vl-assignpattern-keyvalue-replacement-vl-expr-equiv-congruence-on-orig-x

(defthm
 vl-assignpattern-keyvalue-replacement-vl-expr-equiv-congruence-on-orig-x
 (implies (vl-expr-equiv orig-x orig-x-equiv)
          (equal (vl-assignpattern-keyvalue-replacement
                      lhs-type fields orig-x ctx warnings)
                 (vl-assignpattern-keyvalue-replacement
                      lhs-type
                      fields orig-x-equiv ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-assignpattern-keyvalue-replacement-of-vl-context-fix-ctx

(defthm vl-assignpattern-keyvalue-replacement-of-vl-context-fix-ctx
  (equal (vl-assignpattern-keyvalue-replacement
              lhs-type
              fields orig-x (vl-context-fix ctx)
              warnings)
         (vl-assignpattern-keyvalue-replacement
              lhs-type fields orig-x ctx warnings)))

Theorem: vl-assignpattern-keyvalue-replacement-vl-context-equiv-congruence-on-ctx

(defthm
 vl-assignpattern-keyvalue-replacement-vl-context-equiv-congruence-on-ctx
 (implies (vl-context-equiv ctx ctx-equiv)
          (equal (vl-assignpattern-keyvalue-replacement
                      lhs-type fields orig-x ctx warnings)
                 (vl-assignpattern-keyvalue-replacement
                      lhs-type
                      fields orig-x ctx-equiv warnings)))
 :rule-classes :congruence)

Theorem: vl-assignpattern-keyvalue-replacement-of-vl-warninglist-fix-warnings

(defthm
 vl-assignpattern-keyvalue-replacement-of-vl-warninglist-fix-warnings
 (equal (vl-assignpattern-keyvalue-replacement
             lhs-type fields orig-x
             ctx (vl-warninglist-fix warnings))
        (vl-assignpattern-keyvalue-replacement
             lhs-type fields orig-x ctx warnings)))

Theorem: vl-assignpattern-keyvalue-replacement-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-assignpattern-keyvalue-replacement-vl-warninglist-equiv-congruence-on-warnings
 (implies (vl-warninglist-equiv warnings warnings-equiv)
          (equal (vl-assignpattern-keyvalue-replacement
                      lhs-type fields orig-x ctx warnings)
                 (vl-assignpattern-keyvalue-replacement
                      lhs-type
                      fields orig-x ctx warnings-equiv)))
 :rule-classes :congruence)