		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-const

Check a constant.

Signature
(check-const c) → etype
Arguments: c — Guard (constp c).
Returns: etype — Type (expr-type-resultp etype).

For now we only accept integer constants.

We return an expression type. A constant is never an lvalue.

This is the static counterpart of exec-const.

Definitions and Theorems

Function: check-const

(defun check-const (c)
 (declare (xargs :guard (constp c)))
 (let ((__function__ 'check-const))
  (declare (ignorable __function__))
  (const-case
     c :int
     (b* (((okf type) (check-iconst c.get)))
       (make-expr-type :type type :lvalue nil))
     :float (reserrf (list :unsupported-float-const (const-fix c)))
     :enum (reserrf (list :unsupported-enum-const (const-fix c)))
     :char (reserrf (list :unsupported-char-const (const-fix c))))))

Theorem: expr-type-resultp-of-check-const

(defthm expr-type-resultp-of-check-const
  (b* ((etype (check-const c)))
    (expr-type-resultp etype))
  :rule-classes :rewrite)

Theorem: check-const-of-const-fix-c

(defthm check-const-of-const-fix-c
  (equal (check-const (const-fix c))
         (check-const c)))

Theorem: check-const-const-equiv-congruence-on-c

(defthm check-const-const-equiv-congruence-on-c
  (implies (const-equiv c c-equiv)
           (equal (check-const c)
                  (check-const c-equiv)))
  :rule-classes :congruence)