		Search-engine friendly clone of the ACL2 documentation.

Expression-sizing

Vl-parse-keyval-pattern-struct

Signature
(vl-parse-keyval-pattern-struct fields members orig-x ctx warnings) → (mv successp alist new-warnings)
Arguments: fields — Guard (vl-exprlist-p fields).; members — Guard (vl-structmemberlist-p members).; 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).; alist — Type (vl-expr-val-alist-p alist).; new-warnings — Type (vl-warninglist-p new-warnings).

Definitions and Theorems

Function: vl-parse-keyval-pattern-struct

(defun vl-parse-keyval-pattern-struct
       (fields members orig-x ctx warnings)
 (declare (xargs :guard (and (vl-exprlist-p fields)
                             (vl-structmemberlist-p members)
                             (vl-expr-p orig-x)
                             (vl-context-p ctx)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-parse-keyval-pattern-struct))
  (declare (ignorable __function__))
  (b*
   ((warnings (vl-warninglist-fix warnings))
    (ctx (vl-context-fix ctx))
    (orig-x (vl-expr-fix orig-x))
    ((when (atom fields))
     (mv t nil warnings))
    (pair (vl-expr-fix (car fields)))
    ((unless (and (not (vl-atom-p pair))
                  (eq (vl-nonatom->op pair)
                      :vl-keyvalue)))
     (mv
      nil nil
      (warn
       :type :vl-assignpattern-elim-fail
       :msg
       "~a0: Expected key-value pairs in assignment ~
                                  pattern ~a1 (bad: ~a2)"
       :args (list ctx orig-x pair))))
    (pair.args (vl-nonatom->args pair))
    (idx (first pair.args))
    (defaultp (and (vl-atom-p idx)
                   (equal (vl-atom->guts idx)
                          (vl-keyguts :vl-default))))
    ((unless (or defaultp (vl-idexpr-p idx)))
     (mv
      nil nil
      (warn
       :type :vl-assignpattern-elim-fail
       :msg
       "~a0: Expected keys in struct keyval pattern ~
                                  to be identifiers (except for default): ~a1 ~
                                  (bad: ~a2)"
       :args (list ctx orig-x pair))))
    (key (if defaultp :default
           (vl-idexpr->name idx)))
    ((unless (or defaultp
                 (vl-find-structmember key members)))
     (mv
      nil nil
      (warn
       :type :vl-assignpattern-elim-fail
       :msg
       "~a0: Assign pattern key out of range for ~
                                  struct type: ~a1 (bad: ~a2)"
       :args (list ctx orig-x pair))))
    ((mv rest-ok rest warnings)
     (vl-parse-keyval-pattern-struct (cdr fields)
                                     members orig-x ctx warnings)))
   (mv rest-ok
       (cons (cons key (second pair.args))
             rest)
       warnings))))

Theorem: booleanp-of-vl-parse-keyval-pattern-struct.successp

(defthm booleanp-of-vl-parse-keyval-pattern-struct.successp
  (b* (((mv ?successp ?alist ?new-warnings)
        (vl-parse-keyval-pattern-struct
             fields members orig-x ctx warnings)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: vl-expr-val-alist-p-of-vl-parse-keyval-pattern-struct.alist

(defthm vl-expr-val-alist-p-of-vl-parse-keyval-pattern-struct.alist
  (b* (((mv ?successp ?alist ?new-warnings)
        (vl-parse-keyval-pattern-struct
             fields members orig-x ctx warnings)))
    (vl-expr-val-alist-p alist))
  :rule-classes :rewrite)

Theorem: vl-warninglist-p-of-vl-parse-keyval-pattern-struct.new-warnings

(defthm
    vl-warninglist-p-of-vl-parse-keyval-pattern-struct.new-warnings
  (b* (((mv ?successp ?alist ?new-warnings)
        (vl-parse-keyval-pattern-struct
             fields members orig-x ctx warnings)))
    (vl-warninglist-p new-warnings))
  :rule-classes :rewrite)

Theorem: vl-exprlist-max-count-of-vl-parse-keyval-pattern-struct

(defthm vl-exprlist-max-count-of-vl-parse-keyval-pattern-struct
 (<
  (vl-exprlist-max-count
     (alist-vals (mv-nth 1
                         (vl-parse-keyval-pattern-struct
                              fields members orig-x ctx warnings))))
  (vl-exprlist-count fields))
 :rule-classes :linear)

Theorem: vl-parse-keyval-pattern-struct-of-vl-exprlist-fix-fields

(defthm vl-parse-keyval-pattern-struct-of-vl-exprlist-fix-fields
 (equal (vl-parse-keyval-pattern-struct (vl-exprlist-fix fields)
                                        members orig-x ctx warnings)
        (vl-parse-keyval-pattern-struct
             fields members orig-x ctx warnings)))

Theorem: vl-parse-keyval-pattern-struct-vl-exprlist-equiv-congruence-on-fields

(defthm
 vl-parse-keyval-pattern-struct-vl-exprlist-equiv-congruence-on-fields
 (implies
  (vl-exprlist-equiv fields fields-equiv)
  (equal
      (vl-parse-keyval-pattern-struct
           fields members orig-x ctx warnings)
      (vl-parse-keyval-pattern-struct fields-equiv
                                      members orig-x ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-parse-keyval-pattern-struct-of-vl-structmemberlist-fix-members

(defthm
  vl-parse-keyval-pattern-struct-of-vl-structmemberlist-fix-members
  (equal (vl-parse-keyval-pattern-struct
              fields (vl-structmemberlist-fix members)
              orig-x ctx warnings)
         (vl-parse-keyval-pattern-struct
              fields members orig-x ctx warnings)))

Theorem: vl-parse-keyval-pattern-struct-vl-structmemberlist-equiv-congruence-on-members

(defthm
 vl-parse-keyval-pattern-struct-vl-structmemberlist-equiv-congruence-on-members
 (implies (vl-structmemberlist-equiv members members-equiv)
          (equal (vl-parse-keyval-pattern-struct
                      fields members orig-x ctx warnings)
                 (vl-parse-keyval-pattern-struct
                      fields
                      members-equiv orig-x ctx warnings)))
 :rule-classes :congruence)

Theorem: vl-parse-keyval-pattern-struct-of-vl-expr-fix-orig-x

(defthm vl-parse-keyval-pattern-struct-of-vl-expr-fix-orig-x
  (equal (vl-parse-keyval-pattern-struct
              fields members (vl-expr-fix orig-x)
              ctx warnings)
         (vl-parse-keyval-pattern-struct
              fields members orig-x ctx warnings)))

Theorem: vl-parse-keyval-pattern-struct-vl-expr-equiv-congruence-on-orig-x

(defthm
  vl-parse-keyval-pattern-struct-vl-expr-equiv-congruence-on-orig-x
  (implies (vl-expr-equiv orig-x orig-x-equiv)
           (equal (vl-parse-keyval-pattern-struct
                       fields members orig-x ctx warnings)
                  (vl-parse-keyval-pattern-struct
                       fields
                       members orig-x-equiv ctx warnings)))
  :rule-classes :congruence)

Theorem: vl-parse-keyval-pattern-struct-of-vl-context-fix-ctx

(defthm vl-parse-keyval-pattern-struct-of-vl-context-fix-ctx
  (equal (vl-parse-keyval-pattern-struct
              fields
              members orig-x (vl-context-fix ctx)
              warnings)
         (vl-parse-keyval-pattern-struct
              fields members orig-x ctx warnings)))

Theorem: vl-parse-keyval-pattern-struct-vl-context-equiv-congruence-on-ctx

(defthm
  vl-parse-keyval-pattern-struct-vl-context-equiv-congruence-on-ctx
  (implies (vl-context-equiv ctx ctx-equiv)
           (equal (vl-parse-keyval-pattern-struct
                       fields members orig-x ctx warnings)
                  (vl-parse-keyval-pattern-struct
                       fields
                       members orig-x ctx-equiv warnings)))
  :rule-classes :congruence)

Theorem: vl-parse-keyval-pattern-struct-of-vl-warninglist-fix-warnings

(defthm
      vl-parse-keyval-pattern-struct-of-vl-warninglist-fix-warnings
 (equal
  (vl-parse-keyval-pattern-struct fields members orig-x
                                  ctx (vl-warninglist-fix warnings))
  (vl-parse-keyval-pattern-struct
       fields members orig-x ctx warnings)))

Theorem: vl-parse-keyval-pattern-struct-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-parse-keyval-pattern-struct-vl-warninglist-equiv-congruence-on-warnings
 (implies (vl-warninglist-equiv warnings warnings-equiv)
          (equal (vl-parse-keyval-pattern-struct
                      fields members orig-x ctx warnings)
                 (vl-parse-keyval-pattern-struct
                      fields
                      members orig-x ctx warnings-equiv)))
 :rule-classes :congruence)