		Search-engine friendly clone of the ACL2 documentation.

Atj-types

Atj-type-of-value

ATJ type of an ACL2 value.

Signature
(atj-type-of-value val) → type
Returns: type — Type (atj-typep type).

This is the type that ATJ assigns to a quoted constant with the given value. Note that a constant like 2 does not get type :jint. Instead, ATJ assigns :jint to a term like (int-value 2) (when :deep is nil and :guards is t); see the code generation functions.

Definitions and Theorems

Function: atj-type-of-value

(defun atj-type-of-value (val)
 (declare (xargs :guard t))
 (let ((__function__ 'atj-type-of-value))
  (declare (ignorable __function__))
  (cond
   ((integerp val)
    (atj-type-acl2 (atj-atype-integer)))
   ((rationalp val)
    (atj-type-acl2 (atj-atype-rational)))
   ((acl2-numberp val)
    (atj-type-acl2 (atj-atype-number)))
   ((characterp val)
    (atj-type-acl2 (atj-atype-character)))
   ((stringp val)
    (atj-type-acl2 (atj-atype-string)))
   ((booleanp val)
    (atj-type-acl2 (atj-atype-boolean)))
   ((symbolp val)
    (atj-type-acl2 (atj-atype-symbol)))
   ((consp val)
    (atj-type-acl2 (atj-atype-cons)))
   (t
    (prog2$
     (raise
      "Internal errror: ~
                           the value ~x0 is not a number, ~
                           a character, a string, a symbol, or a CONS."
      val)
     (atj-type-irrelevant))))))

Theorem: atj-typep-of-atj-type-of-value

(defthm atj-typep-of-atj-type-of-value
  (b* ((type (atj-type-of-value val)))
    (atj-typep type))
  :rule-classes :rewrite)