		Search-engine friendly clone of the ACL2 documentation.

Vl-expr-selfsize

Vl-atom-selfsize

Compute the self-determined size of an atom.

Signature
(vl-atom-selfsize x ss ctx warnings) → (mv warnings size)
Arguments: x — Guard (vl-expr-p x).; ss — Guard (vl-scopestack-p ss).; ctx — Guard (vl-context-p ctx).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).; size — Type (maybe-natp size).

Warning: this function should typically only be called by the expression-sizing transform.

We attempt to compute the "self-determined size" of the atom x. Another way to look at this function is as an extension of "origwidth" from constint/weirdint atoms to include identifiers.

We have taken special care in our lexer to ensure that every constant, whether it is a vl-weirdint-p or vl-constint-p, has a determined width. As a result, it is easy to determine the self-determined size of a constant, and we never fail to do so.

For identifiers, we must look up the identifier in the module to try to determine its size. This can fail if the identifier is not declared in the module, or if its size is not resolved. In these cases, we add a fatal warning to warnings and return nil as the size.

We do not try to size other atoms, such as real numbers, individual HID pieces, function names, system function names, etc.; instead we just return nil as the size. But we do not issue a warning in this case, because it seems like these things are not really supposed to have sizes.

Definitions and Theorems

Function: vl-atom-selfsize

(defun vl-atom-selfsize (x ss ctx warnings)
  (declare (xargs :guard (and (vl-expr-p x)
                              (vl-scopestack-p ss)
                              (vl-context-p ctx)
                              (vl-warninglist-p warnings))))
  (declare (xargs :guard (vl-atom-p x)))
  (let ((__function__ 'vl-atom-selfsize))
    (declare (ignorable __function__))
    (b* ((x (vl-expr-fix x))
         (ctx (vl-context-fix ctx))
         (guts (vl-atom->guts x))
         ((when (vl-fast-constint-p guts))
          (mv (ok) (vl-constint->origwidth guts)))
         ((when (vl-fast-weirdint-p guts))
          (mv (ok) (vl-weirdint->origwidth guts)))
         ((when (vl-fast-string-p guts))
          (mv (ok)
              (* 8 (length (vl-string->value guts)))))
         ((when (eq (tag guts) :vl-extint))
          (mv (ok) 1))
         ((unless (or (vl-fast-id-p guts)
                      (vl-fast-hidpiece-p guts)))
          (mv (ok) nil)))
      (vl-index-selfsize x ss ctx warnings))))

Theorem: vl-warninglist-p-of-vl-atom-selfsize.warnings

(defthm vl-warninglist-p-of-vl-atom-selfsize.warnings
  (b* (((mv ?warnings ?size)
        (vl-atom-selfsize x ss ctx warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: maybe-natp-of-vl-atom-selfsize.size

(defthm maybe-natp-of-vl-atom-selfsize.size
  (b* (((mv ?warnings ?size)
        (vl-atom-selfsize x ss ctx warnings)))
    (maybe-natp size))
  :rule-classes :type-prescription)

Theorem: warning-irrelevance-of-vl-atom-selfsize

(defthm warning-irrelevance-of-vl-atom-selfsize
  (let ((ret1 (vl-atom-selfsize x ss ctx warnings))
        (ret2 (vl-atom-selfsize x ss nil nil)))
    (implies (syntaxp (not (and (equal ctx ''nil)
                                (equal warnings ''nil))))
             (equal (mv-nth 1 ret1)
                    (mv-nth 1 ret2)))))

Theorem: vl-atom-selfsize-of-vl-expr-fix-x

(defthm vl-atom-selfsize-of-vl-expr-fix-x
  (equal (vl-atom-selfsize (vl-expr-fix x)
                           ss ctx warnings)
         (vl-atom-selfsize x ss ctx warnings)))

Theorem: vl-atom-selfsize-vl-expr-equiv-congruence-on-x

(defthm vl-atom-selfsize-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-atom-selfsize x ss ctx warnings)
                  (vl-atom-selfsize x-equiv ss ctx warnings)))
  :rule-classes :congruence)

Theorem: vl-atom-selfsize-of-vl-scopestack-fix-ss

(defthm vl-atom-selfsize-of-vl-scopestack-fix-ss
  (equal (vl-atom-selfsize x (vl-scopestack-fix ss)
                           ctx warnings)
         (vl-atom-selfsize x ss ctx warnings)))

Theorem: vl-atom-selfsize-vl-scopestack-equiv-congruence-on-ss

(defthm vl-atom-selfsize-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-atom-selfsize x ss ctx warnings)
                  (vl-atom-selfsize x ss-equiv ctx warnings)))
  :rule-classes :congruence)

Theorem: vl-atom-selfsize-of-vl-context-fix-ctx

(defthm vl-atom-selfsize-of-vl-context-fix-ctx
  (equal (vl-atom-selfsize x ss (vl-context-fix ctx)
                           warnings)
         (vl-atom-selfsize x ss ctx warnings)))

Theorem: vl-atom-selfsize-vl-context-equiv-congruence-on-ctx

(defthm vl-atom-selfsize-vl-context-equiv-congruence-on-ctx
  (implies (vl-context-equiv ctx ctx-equiv)
           (equal (vl-atom-selfsize x ss ctx warnings)
                  (vl-atom-selfsize x ss ctx-equiv warnings)))
  :rule-classes :congruence)

Theorem: vl-atom-selfsize-of-vl-warninglist-fix-warnings

(defthm vl-atom-selfsize-of-vl-warninglist-fix-warnings
  (equal (vl-atom-selfsize x ss ctx (vl-warninglist-fix warnings))
         (vl-atom-selfsize x ss ctx warnings)))

Theorem: vl-atom-selfsize-vl-warninglist-equiv-congruence-on-warnings

(defthm vl-atom-selfsize-vl-warninglist-equiv-congruence-on-warnings
  (implies (vl-warninglist-equiv warnings warnings-equiv)
           (equal (vl-atom-selfsize x ss ctx warnings)
                  (vl-atom-selfsize x ss ctx warnings-equiv)))
  :rule-classes :congruence)