		Search-engine friendly clone of the ACL2 documentation.

Types

Type-completep

Check if a type is complete [C17:6.2.5].

Signature
(type-completep type) → yes/no
Arguments: type — Guard (typep type).
Returns: yes/no — Type (booleanp yes/no).

A type is complete when its size is determined, otherwise it is incomplete. While [C17:6.2.5] cautions that the same type may be complete or incomplete in different parts of a program, for now we capture the completeness of a type independently from where it occurs: this is adequate for our C subset and for our use of this predicate.

The void type is never complete [C17:6.2.5/19]. The basic types, which are the integer types in our subset of C, are always complete [C17:6.2.5/14]. A structure type is complete as soon as its declaration ends [C17:6.7.2.1/8]; it is incomplete inside the structure type, but we do not use this predicate for the member types. A pointer type is always complete [C17:6.2.5/20] (regardless of the pointed-to type). An array type needs its element type to be complete [C17:6.2.5/20], as formalized in check-tyname; the array type itself is complete if the size is specified, otherwise it is incomplete [C17:6.2.5/22].

Definitions and Theorems

Function: type-completep

(defun type-completep (type)
  (declare (xargs :guard (typep type)))
  (cond ((type-case type :void) nil)
        ((type-integerp type) t)
        ((type-case type :struct) t)
        ((type-case type :pointer) t)
        ((type-case type :array)
         (not (eq (type-array->size type) nil)))
        (t (impossible))))

Theorem: booleanp-of-type-completep

(defthm booleanp-of-type-completep
  (b* ((yes/no (type-completep type)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: type-completep-of-type-fix-type

(defthm type-completep-of-type-fix-type
  (equal (type-completep (type-fix type))
         (type-completep type)))

Theorem: type-completep-type-equiv-congruence-on-type

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