		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-enum-const

Validate an enumeration constant.

Signature
(valid-enum-const econst table) → (mv erp type)
Arguments: econst — Guard (identp econst).; table — Guard (valid-tablep table).
Returns: type — Type (typep type).

Here we validate an enumeration constant that occurs as an expression. Thus, the validation table must include that (ordinary) identifier, with the information of being an enumeration constant. Its type is always int [C:6.7.2.2/3], so this function always returns that type if validation succeeds; so we could have this function return nothing if there's no error, but we have it return the int type for uniformity and simplicity.

Definitions and Theorems

Function: valid-enum-const

(defun valid-enum-const (econst table)
 (declare (xargs :guard (and (identp econst)
                             (valid-tablep table))))
 (let ((__function__ 'valid-enum-const))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-type))
    ((mv info &)
     (valid-lookup-ord econst table))
    ((unless info)
     (reterr
      (msg
       "The identifier ~x0, used as an enumeration constant, ~
                      is not in scope."
       (ident-fix econst))))
    ((unless (valid-ord-info-case info :enumconst))
     (reterr
      (msg
       "The identifier ~x0, used as an enumeration constant, ~
                      is in scope, but it is not an enumeration constant: ~
                      its information is ~x1."
       (ident-fix econst)
       info))))
   (retok (type-sint)))))

Theorem: typep-of-valid-enum-const.type

(defthm typep-of-valid-enum-const.type
  (b* (((mv acl2::?erp ?type)
        (valid-enum-const econst table)))
    (typep type))
  :rule-classes :rewrite)

Theorem: valid-enum-const-of-ident-fix-econst

(defthm valid-enum-const-of-ident-fix-econst
  (equal (valid-enum-const (ident-fix econst)
                           table)
         (valid-enum-const econst table)))

Theorem: valid-enum-const-ident-equiv-congruence-on-econst

(defthm valid-enum-const-ident-equiv-congruence-on-econst
  (implies (ident-equiv econst econst-equiv)
           (equal (valid-enum-const econst table)
                  (valid-enum-const econst-equiv table)))
  :rule-classes :congruence)

Theorem: valid-enum-const-of-valid-table-fix-table

(defthm valid-enum-const-of-valid-table-fix-table
  (equal (valid-enum-const econst (valid-table-fix table))
         (valid-enum-const econst table)))

Theorem: valid-enum-const-valid-table-equiv-congruence-on-table

(defthm valid-enum-const-valid-table-equiv-congruence-on-table
  (implies (valid-table-equiv table table-equiv)
           (equal (valid-enum-const econst table)
                  (valid-enum-const econst table-equiv)))
  :rule-classes :congruence)