Validate a decimal, octal, or hexadecimal constant.
(valid-dec/oct/hex-const const) → value
This kind of constant is always valid,
but for this function we use the naming scheme
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.
Function:
(defun valid-dec/oct/hex-const (const) (declare (xargs :guard (dec/oct/hex-constp const))) (let ((__function__ 'valid-dec/oct/hex-const)) (declare (ignorable __function__)) (dec/oct/hex-const-case const :dec const.value :oct const.value :hex (str::hex-digit-chars-value const.digits))))
Theorem:
(defthm natp-of-valid-dec/oct/hex-const (b* ((value (valid-dec/oct/hex-const const))) (natp value)) :rule-classes :rewrite)
Theorem:
(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:
(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)