		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-dec/oct/hex-const

Validate a decimal, octal, or hexadecimal constant.

Signature
(valid-dec/oct/hex-const const) → value
Arguments: const — Guard (dec/oct/hex-constp const).
Returns: value — Type (natp value).

This kind of constant is always valid, but for this function we use the naming scheme valid-... for uniformity with the other validator's functions.

This function actually evaluates the constant, to a natural number. This is needed by the validator in order to assign types to integer constants. This function returns a natural number, which can be arbitrarily large; whether an integer constant is too large is checked elsewhere.

For a decimal or octal constant, the value is a component of the fixtype. For a hexadecimal constant, we use a library function to convert the digits into a value; the digits are as they appear in the concrete syntax, i.e. in big-endian order.

Definitions and Theorems

Function: valid-dec/oct/hex-const

(defun valid-dec/oct/hex-const (const)
  (declare (xargs :guard (dec/oct/hex-constp const)))
  (dec/oct/hex-const-case
       const
       :dec const.value
       :oct const.value
       :hex (str::hex-digit-chars-value const.digits)))

Theorem: natp-of-valid-dec/oct/hex-const

(defthm natp-of-valid-dec/oct/hex-const
  (b* ((value (valid-dec/oct/hex-const const)))
    (natp value))
  :rule-classes :rewrite)

Theorem: valid-dec/oct/hex-const-of-dec/oct/hex-const-fix-const

(defthm valid-dec/oct/hex-const-of-dec/oct/hex-const-fix-const
  (equal (valid-dec/oct/hex-const (dec/oct/hex-const-fix const))
         (valid-dec/oct/hex-const const)))

Theorem: valid-dec/oct/hex-const-dec/oct/hex-const-equiv-congruence-on-const

(defthm
 valid-dec/oct/hex-const-dec/oct/hex-const-equiv-congruence-on-const
 (implies (dec/oct/hex-const-equiv const const-equiv)
          (equal (valid-dec/oct/hex-const const)
                 (valid-dec/oct/hex-const const-equiv)))
 :rule-classes :congruence)