		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-const

Validate a constant.

Signature
(valid-const const table ienv) → (mv erp new-const type)
Arguments: const — Guard (constp const).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; new-const — Type (constp new-const).; type — Type (typep type).

If validation is successful, we return the type of the constant.

Definitions and Theorems

Function: valid-const

(defun valid-const (const table ienv)
  (declare (xargs :guard (and (constp const)
                              (valid-tablep table)
                              (ienvp ienv))))
  (b* (((reterr) (irr-const) (irr-type)))
    (const-case const :int
                (b* (((erp iconst type)
                      (valid-iconst const.iconst ienv)))
                  (retok (const-int iconst) type))
                :float
                (b* ((type (valid-fconst const.fconst)))
                  (retok (const-fix const) type))
                :enum
                (b* (((erp type)
                      (valid-enum-const const.ident table)))
                  (retok (const-fix const) type))
                :char
                (b* (((erp type)
                      (valid-cconst const.cconst ienv)))
                  (retok (const-fix const) type)))))

Theorem: maybe-msgp-of-valid-const.erp

(defthm maybe-msgp-of-valid-const.erp
  (b* (((mv acl2::?erp ?new-const ?type)
        (valid-const const table ienv)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: constp-of-valid-const.new-const

(defthm constp-of-valid-const.new-const
  (b* (((mv acl2::?erp ?new-const ?type)
        (valid-const const table ienv)))
    (constp new-const))
  :rule-classes :rewrite)

Theorem: typep-of-valid-const.type

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

Theorem: valid-const-of-const-fix-const

(defthm valid-const-of-const-fix-const
  (equal (valid-const (const-fix const)
                      table ienv)
         (valid-const const table ienv)))

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

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

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

(defthm valid-const-of-valid-table-fix-table
  (equal (valid-const const (valid-table-fix table)
                      ienv)
         (valid-const const table ienv)))

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

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

Theorem: valid-const-of-ienv-fix-ienv

(defthm valid-const-of-ienv-fix-ienv
  (equal (valid-const const table (ienv-fix ienv))
         (valid-const const table ienv)))

Theorem: valid-const-ienv-equiv-congruence-on-ienv

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