		Search-engine friendly clone of the ACL2 documentation.

Types

Make-pointers-to

Derive a pointer type for each type qualifier and attribute specifier list.

Signature
(make-pointers-to pointers type) → new-type
Arguments: pointers — Guard (typequal/attribspec-list-listp pointers).; type — Guard (typep type).
Returns: new-type — Type (typep new-type).

This takes the list of lists of type qualifiers and attribute specifiers from a declarator or abstract declarator, and creates the corresponding (possibly pointer) type.

Since our approximate type system does not incorporate type qualifiers, each cons of the pointers list is used only to derive a pointer from the type.

Definitions and Theorems

Function: make-pointers-to

(defun make-pointers-to (pointers type)
  (declare
       (xargs :guard (and (typequal/attribspec-list-listp pointers)
                          (typep type))))
  (if (endp pointers)
      (type-fix type)
    (make-type-pointer :to (make-pointers-to (rest pointers)
                                             type))))

Theorem: typep-of-make-pointers-to

(defthm typep-of-make-pointers-to
  (b* ((new-type (make-pointers-to pointers type)))
    (typep new-type))
  :rule-classes :rewrite)

Theorem: make-pointers-to-of-typequal/attribspec-list-list-fix-pointers

(defthm
     make-pointers-to-of-typequal/attribspec-list-list-fix-pointers
 (equal
      (make-pointers-to (typequal/attribspec-list-list-fix pointers)
                        type)
      (make-pointers-to pointers type)))

Theorem: make-pointers-to-typequal/attribspec-list-list-equiv-congruence-on-pointers

(defthm
 make-pointers-to-typequal/attribspec-list-list-equiv-congruence-on-pointers
 (implies
      (typequal/attribspec-list-list-equiv pointers pointers-equiv)
      (equal (make-pointers-to pointers type)
             (make-pointers-to pointers-equiv type)))
 :rule-classes :congruence)

Theorem: make-pointers-to-of-type-fix-type

(defthm make-pointers-to-of-type-fix-type
  (equal (make-pointers-to pointers (type-fix type))
         (make-pointers-to pointers type)))

Theorem: make-pointers-to-type-equiv-congruence-on-type

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