		Search-engine friendly clone of the ACL2 documentation.

Types

Tyname-to-type

Turn a type name into a type.

Signature
(tyname-to-type tyname) → type
Arguments: tyname — Guard (tynamep tyname).
Returns: type — Type (typep type).

A type name denotes a type [C:6.7.7/2]. This ACL2 function returns the denoted type. As mentioned in type, a semantic type is an abstraction of a type name: this function reifies that abstraction.

If an array declarator in the type name has no size, we turn that into an array type with unspecified size. If the size is present (as an integer constant), we use its integer value as the array type size. If the size is present but 0, we cannot use that as the array type size, which must be positive; in this case, we return an array type of unspecified size, just to make this ACL2 function total, but when this function is used, other ACL2 code ensures that the integer constant is not 0. We may revise this treatment of an integer constant 0 as array size, at some point in the future.

Definitions and Theorems

Function: tyname-to-type-aux

(defun tyname-to-type-aux (tyspec declor)
 (declare (xargs :guard (and (tyspecseqp tyspec)
                             (obj-adeclorp declor))))
 (let ((__function__ 'tyname-to-type-aux))
  (declare (ignorable __function__))
  (obj-adeclor-case
   declor :none (tyspecseq-to-type tyspec)
   :pointer
   (type-pointer (tyname-to-type-aux tyspec declor.decl))
   :array
   (if declor.size
    (b* ((size (iconst->value declor.size)))
      (if
        (= size 0)
        (make-type-array :of (tyname-to-type-aux tyspec declor.decl)
                         :size nil)
        (make-type-array :of (tyname-to-type-aux tyspec declor.decl)
                         :size size)))
    (make-type-array :of (tyname-to-type-aux tyspec declor.decl)
                     :size nil)))))

Theorem: typep-of-tyname-to-type-aux

(defthm typep-of-tyname-to-type-aux
  (b* ((type (tyname-to-type-aux tyspec declor)))
    (typep type))
  :rule-classes :rewrite)

Theorem: tyname-to-type-aux-of-tyspecseq-fix-tyspec

(defthm tyname-to-type-aux-of-tyspecseq-fix-tyspec
  (equal (tyname-to-type-aux (tyspecseq-fix tyspec)
                             declor)
         (tyname-to-type-aux tyspec declor)))

Theorem: tyname-to-type-aux-tyspecseq-equiv-congruence-on-tyspec

(defthm tyname-to-type-aux-tyspecseq-equiv-congruence-on-tyspec
  (implies (tyspecseq-equiv tyspec tyspec-equiv)
           (equal (tyname-to-type-aux tyspec declor)
                  (tyname-to-type-aux tyspec-equiv declor)))
  :rule-classes :congruence)

Theorem: tyname-to-type-aux-of-obj-adeclor-fix-declor

(defthm tyname-to-type-aux-of-obj-adeclor-fix-declor
  (equal (tyname-to-type-aux tyspec (obj-adeclor-fix declor))
         (tyname-to-type-aux tyspec declor)))

Theorem: tyname-to-type-aux-obj-adeclor-equiv-congruence-on-declor

(defthm tyname-to-type-aux-obj-adeclor-equiv-congruence-on-declor
  (implies (obj-adeclor-equiv declor declor-equiv)
           (equal (tyname-to-type-aux tyspec declor)
                  (tyname-to-type-aux tyspec declor-equiv)))
  :rule-classes :congruence)

Function: tyname-to-type

(defun tyname-to-type (tyname)
  (declare (xargs :guard (tynamep tyname)))
  (let ((__function__ 'tyname-to-type))
    (declare (ignorable __function__))
    (tyname-to-type-aux (tyname->tyspec tyname)
                        (tyname->declor tyname))))

Theorem: typep-of-tyname-to-type

(defthm typep-of-tyname-to-type
  (b* ((type (tyname-to-type tyname)))
    (typep type))
  :rule-classes :rewrite)

Theorem: tyname-to-type-of-tyname-fix-tyname

(defthm tyname-to-type-of-tyname-fix-tyname
  (equal (tyname-to-type (tyname-fix tyname))
         (tyname-to-type tyname)))

Theorem: tyname-to-type-tyname-equiv-congruence-on-tyname

(defthm tyname-to-type-tyname-equiv-congruence-on-tyname
  (implies (tyname-equiv tyname tyname-equiv)
           (equal (tyname-to-type tyname)
                  (tyname-to-type tyname-equiv)))
  :rule-classes :congruence)