		Search-engine friendly clone of the ACL2 documentation.

Expression-sizing

Vl-plainarglist-exprsize

Compute sizes and types of expressions throughout a vl-plainarglist-p.

Signature
(vl-plainarglist-exprsize x ss ctx ports submod-ss warnings) → (mv successp warnings new-x)
Arguments: x — Guard (vl-plainarglist-p x).; ss — Guard (vl-scopestack-p ss).; ctx — Guard (vl-context-p ctx).; ports — Guard (vl-portlist-p ports).; submod-ss — Guard (vl-scopestack-p submod-ss).; warnings — Guard (vl-warninglist-p warnings).
Returns: successp — Type (booleanp successp).; warnings — Type (vl-warninglist-p warnings).; new-x — Type (vl-plainarglist-p new-x).

Definitions and Theorems

Function: vl-plainarglist-exprsize

(defun vl-plainarglist-exprsize (x ss ctx ports submod-ss warnings)
 (declare (xargs :guard (and (vl-plainarglist-p x)
                             (vl-scopestack-p ss)
                             (vl-context-p ctx)
                             (vl-portlist-p ports)
                             (vl-scopestack-p submod-ss)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-plainarglist-exprsize))
  (declare (ignorable __function__))
  (b* (((when (atom x)) (mv t (ok) nil))
       (ports (vl-portlist-fix ports))
       ((mv car-successp warnings car-prime)
        (vl-plainarg-exprsize (car x)
                              ss ctx (and (consp ports) (car ports))
                              submod-ss warnings))
       ((mv cdr-successp warnings cdr-prime)
        (vl-plainarglist-exprsize
             (cdr x)
             ss ctx (and (consp ports) (cdr ports))
             submod-ss warnings))
       (successp (and car-successp cdr-successp))
       (x-prime (cons car-prime cdr-prime)))
    (mv successp warnings x-prime))))

Theorem: booleanp-of-vl-plainarglist-exprsize.successp

(defthm booleanp-of-vl-plainarglist-exprsize.successp
  (b*
    (((mv ?successp ?warnings ?new-x)
      (vl-plainarglist-exprsize x ss ctx ports submod-ss warnings)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-plainarglist-exprsize.warnings

(defthm vl-warninglist-p-of-vl-plainarglist-exprsize.warnings
  (b*
    (((mv ?successp ?warnings ?new-x)
      (vl-plainarglist-exprsize x ss ctx ports submod-ss warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-plainarglist-p-of-vl-plainarglist-exprsize.new-x

(defthm vl-plainarglist-p-of-vl-plainarglist-exprsize.new-x
  (b*
    (((mv ?successp ?warnings ?new-x)
      (vl-plainarglist-exprsize x ss ctx ports submod-ss warnings)))
    (vl-plainarglist-p new-x))
  :rule-classes :rewrite)

Theorem: true-listp-of-vl-plainarglist-exprsize

(defthm true-listp-of-vl-plainarglist-exprsize
 (true-listp
  (mv-nth
      2
      (vl-plainarglist-exprsize x ss ctx ports submod-ss warnings)))
 :rule-classes :type-prescription)

Theorem: vl-plainarglist-exprsize-of-vl-plainarglist-fix-x

(defthm vl-plainarglist-exprsize-of-vl-plainarglist-fix-x
 (equal
      (vl-plainarglist-exprsize (vl-plainarglist-fix x)
                                ss ctx ports submod-ss warnings)
      (vl-plainarglist-exprsize x ss ctx ports submod-ss warnings)))

Theorem: vl-plainarglist-exprsize-vl-plainarglist-equiv-congruence-on-x

(defthm
     vl-plainarglist-exprsize-vl-plainarglist-equiv-congruence-on-x
 (implies
   (vl-plainarglist-equiv x x-equiv)
   (equal
        (vl-plainarglist-exprsize x ss ctx ports submod-ss warnings)
        (vl-plainarglist-exprsize x-equiv
                                  ss ctx ports submod-ss warnings)))
 :rule-classes :congruence)

Theorem: vl-plainarglist-exprsize-of-vl-scopestack-fix-ss

(defthm vl-plainarglist-exprsize-of-vl-scopestack-fix-ss
 (equal
      (vl-plainarglist-exprsize x (vl-scopestack-fix ss)
                                ctx ports submod-ss warnings)
      (vl-plainarglist-exprsize x ss ctx ports submod-ss warnings)))

Theorem: vl-plainarglist-exprsize-vl-scopestack-equiv-congruence-on-ss

(defthm
      vl-plainarglist-exprsize-vl-scopestack-equiv-congruence-on-ss
 (implies
   (vl-scopestack-equiv ss ss-equiv)
   (equal
        (vl-plainarglist-exprsize x ss ctx ports submod-ss warnings)
        (vl-plainarglist-exprsize
             x
             ss-equiv ctx ports submod-ss warnings)))
 :rule-classes :congruence)

Theorem: vl-plainarglist-exprsize-of-vl-context-fix-ctx

(defthm vl-plainarglist-exprsize-of-vl-context-fix-ctx
 (equal
      (vl-plainarglist-exprsize x ss (vl-context-fix ctx)
                                ports submod-ss warnings)
      (vl-plainarglist-exprsize x ss ctx ports submod-ss warnings)))

Theorem: vl-plainarglist-exprsize-vl-context-equiv-congruence-on-ctx

(defthm vl-plainarglist-exprsize-vl-context-equiv-congruence-on-ctx
 (implies
   (vl-context-equiv ctx ctx-equiv)
   (equal
        (vl-plainarglist-exprsize x ss ctx ports submod-ss warnings)
        (vl-plainarglist-exprsize
             x
             ss ctx-equiv ports submod-ss warnings)))
 :rule-classes :congruence)

Theorem: vl-plainarglist-exprsize-of-vl-portlist-fix-ports

(defthm vl-plainarglist-exprsize-of-vl-portlist-fix-ports
 (equal
      (vl-plainarglist-exprsize x ss ctx (vl-portlist-fix ports)
                                submod-ss warnings)
      (vl-plainarglist-exprsize x ss ctx ports submod-ss warnings)))

Theorem: vl-plainarglist-exprsize-vl-portlist-equiv-congruence-on-ports

(defthm
     vl-plainarglist-exprsize-vl-portlist-equiv-congruence-on-ports
 (implies
   (vl-portlist-equiv ports ports-equiv)
   (equal
        (vl-plainarglist-exprsize x ss ctx ports submod-ss warnings)
        (vl-plainarglist-exprsize
             x
             ss ctx ports-equiv submod-ss warnings)))
 :rule-classes :congruence)

Theorem: vl-plainarglist-exprsize-of-vl-scopestack-fix-submod-ss

(defthm vl-plainarglist-exprsize-of-vl-scopestack-fix-submod-ss
 (equal
   (vl-plainarglist-exprsize x ss
                             ctx ports (vl-scopestack-fix submod-ss)
                             warnings)
   (vl-plainarglist-exprsize x ss ctx ports submod-ss warnings)))

Theorem: vl-plainarglist-exprsize-vl-scopestack-equiv-congruence-on-submod-ss

(defthm
 vl-plainarglist-exprsize-vl-scopestack-equiv-congruence-on-submod-ss
 (implies
   (vl-scopestack-equiv submod-ss submod-ss-equiv)
   (equal
        (vl-plainarglist-exprsize x ss ctx ports submod-ss warnings)
        (vl-plainarglist-exprsize
             x
             ss ctx ports submod-ss-equiv warnings)))
 :rule-classes :congruence)

Theorem: vl-plainarglist-exprsize-of-vl-warninglist-fix-warnings

(defthm vl-plainarglist-exprsize-of-vl-warninglist-fix-warnings
 (equal
  (vl-plainarglist-exprsize x ss ctx ports
                            submod-ss (vl-warninglist-fix warnings))
  (vl-plainarglist-exprsize x ss ctx ports submod-ss warnings)))

Theorem: vl-plainarglist-exprsize-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-plainarglist-exprsize-vl-warninglist-equiv-congruence-on-warnings
 (implies
   (vl-warninglist-equiv warnings warnings-equiv)
   (equal
        (vl-plainarglist-exprsize x ss ctx ports submod-ss warnings)
        (vl-plainarglist-exprsize
             x
             ss ctx ports submod-ss warnings-equiv)))
 :rule-classes :congruence)