(vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx warnings) → (mv successp pairs new-warnings)
Function:
(defun vl-keyvalue-pattern-collect-array-replacements (count idx incr datatype field-alist orig-x ctx warnings) (declare (xargs :guard (and (natp count) (integerp idx) (integerp incr) (vl-datatype-p datatype) (vl-expr-val-alist-p field-alist) (vl-expr-p orig-x) (vl-context-p ctx) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-keyvalue-pattern-collect-array-replacements)) (declare (ignorable __function__)) (b* ((warnings (vl-warninglist-fix warnings)) (orig-x (vl-expr-fix orig-x)) (ctx (vl-context-fix ctx)) (idx (lifix idx)) (field-alist (vl-expr-val-alist-fix field-alist)) ((when (zp count)) (mv t nil warnings)) (lookup (or (hons-assoc-equal idx field-alist) (hons-assoc-equal :default field-alist))) ((unless lookup) (mv nil nil (warn :type :vl-assignpattern-elim-fail :msg "~a0: Missing array index ~x1 in assignment pattern ~a2" :args (list ctx idx orig-x)))) ((mv ok rest warnings) (vl-keyvalue-pattern-collect-array-replacements (1- count) (+ idx (lifix incr)) incr datatype field-alist orig-x ctx warnings))) (mv ok (cons (cons (vl-datatype-fix datatype) (cdr lookup)) rest) warnings))))
Theorem:
(defthm booleanp-of-vl-keyvalue-pattern-collect-array-replacements.successp (b* (((mv ?successp ?pairs ?new-warnings) (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx warnings))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-type-expr-pairs-p-of-vl-keyvalue-pattern-collect-array-replacements.pairs (b* (((mv ?successp ?pairs ?new-warnings) (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx warnings))) (vl-type-expr-pairs-p pairs)) :rule-classes :rewrite)
Theorem:
(defthm vl-warninglist-p-of-vl-keyvalue-pattern-collect-array-replacements.new-warnings (b* (((mv ?successp ?pairs ?new-warnings) (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx warnings))) (vl-warninglist-p new-warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-exprlist-max-count-of-vl-keyvalue-pattern-collect-array-replacements (<= (vl-exprlist-max-count (alist-vals (mv-nth 1 (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx warnings)))) (vl-exprlist-max-count (alist-vals field-alist))) :rule-classes :linear)
Theorem:
(defthm vl-type-expr-pairs-sum-datatype-sizes-of-array-replacements (b* (((mv ok pairs &) (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx warnings)) ((mv warning size) (vl-datatype-size datatype)) ((mv warning1 size1) (vl-type-expr-pairs-sum-datatype-sizes pairs))) (implies (and ok (not warning)) (and (not warning1) (equal size1 (* (nfix count) size))))))
Theorem:
(defthm vl-keyvalue-pattern-collect-array-replacements-of-nfix-count (equal (vl-keyvalue-pattern-collect-array-replacements (nfix count) idx incr datatype field-alist orig-x ctx warnings) (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx warnings)))
Theorem:
(defthm vl-keyvalue-pattern-collect-array-replacements-nat-equiv-congruence-on-count (implies (acl2::nat-equiv count count-equiv) (equal (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx warnings) (vl-keyvalue-pattern-collect-array-replacements count-equiv idx incr datatype field-alist orig-x ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-keyvalue-pattern-collect-array-replacements-of-ifix-idx (equal (vl-keyvalue-pattern-collect-array-replacements count (ifix idx) incr datatype field-alist orig-x ctx warnings) (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx warnings)))
Theorem:
(defthm vl-keyvalue-pattern-collect-array-replacements-int-equiv-congruence-on-idx (implies (acl2::int-equiv idx idx-equiv) (equal (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx warnings) (vl-keyvalue-pattern-collect-array-replacements count idx-equiv incr datatype field-alist orig-x ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-keyvalue-pattern-collect-array-replacements-of-ifix-incr (equal (vl-keyvalue-pattern-collect-array-replacements count idx (ifix incr) datatype field-alist orig-x ctx warnings) (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx warnings)))
Theorem:
(defthm vl-keyvalue-pattern-collect-array-replacements-int-equiv-congruence-on-incr (implies (acl2::int-equiv incr incr-equiv) (equal (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx warnings) (vl-keyvalue-pattern-collect-array-replacements count idx incr-equiv datatype field-alist orig-x ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-keyvalue-pattern-collect-array-replacements-of-vl-datatype-fix-datatype (equal (vl-keyvalue-pattern-collect-array-replacements count idx incr (vl-datatype-fix datatype) field-alist orig-x ctx warnings) (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx warnings)))
Theorem:
(defthm vl-keyvalue-pattern-collect-array-replacements-vl-datatype-equiv-congruence-on-datatype (implies (vl-datatype-equiv datatype datatype-equiv) (equal (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx warnings) (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype-equiv field-alist orig-x ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-keyvalue-pattern-collect-array-replacements-of-vl-expr-val-alist-fix-field-alist (equal (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype (vl-expr-val-alist-fix field-alist) orig-x ctx warnings) (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx warnings)))
Theorem:
(defthm vl-keyvalue-pattern-collect-array-replacements-vl-expr-val-alist-equiv-congruence-on-field-alist (implies (vl-expr-val-alist-equiv field-alist field-alist-equiv) (equal (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx warnings) (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist-equiv orig-x ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-keyvalue-pattern-collect-array-replacements-of-vl-expr-fix-orig-x (equal (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist (vl-expr-fix orig-x) ctx warnings) (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx warnings)))
Theorem:
(defthm vl-keyvalue-pattern-collect-array-replacements-vl-expr-equiv-congruence-on-orig-x (implies (vl-expr-equiv orig-x orig-x-equiv) (equal (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx warnings) (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x-equiv ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-keyvalue-pattern-collect-array-replacements-of-vl-context-fix-ctx (equal (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x (vl-context-fix ctx) warnings) (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx warnings)))
Theorem:
(defthm vl-keyvalue-pattern-collect-array-replacements-vl-context-equiv-congruence-on-ctx (implies (vl-context-equiv ctx ctx-equiv) (equal (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx warnings) (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-keyvalue-pattern-collect-array-replacements-of-vl-warninglist-fix-warnings (equal (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx (vl-warninglist-fix warnings)) (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx warnings)))
Theorem:
(defthm vl-keyvalue-pattern-collect-array-replacements-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx warnings) (vl-keyvalue-pattern-collect-array-replacements count idx incr datatype field-alist orig-x ctx warnings-equiv))) :rule-classes :congruence)