		Search-engine friendly clone of the ACL2 documentation.

Valid-decl-spec

Validate a declaration specifier.

Signature
(valid-decl-spec declspec type? tyspecs storspecs table ienv) → (mv erp new-declspec new-type? new-tyspecs new-storspecs return-types new-table)
Arguments: declspec — Guard (decl-specp declspec).; type? — Guard (type-optionp type?).; tyspecs — Guard (type-spec-listp tyspecs).; storspecs — Guard (stor-spec-listp storspecs).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; new-declspec — Type (decl-specp new-declspec).; new-type? — Type (type-optionp new-type?).; new-tyspecs — Type (type-spec-listp new-tyspecs).; new-storspecs — Type (stor-spec-listp new-storspecs).; return-types — Type (type-setp return-types).; new-table — Type (valid-tablep new-table).

For now we ignore type qualifiers, function specifiers, and attributes. We validate alignment specifiers but we do not make any use of them in our currently approximate type system. We handle type specifiers similarly to valid-spec/qual. In addition, we collect all the storage class specifiers encountered as we go through the declaration specifiers.

Definitions and Theorems

Theorem: type-spec-list-unambp-of-valid-decl-spec

(defthm type-spec-list-unambp-of-valid-decl-spec
  (implies
       (type-spec-list-unambp tyspecs)
       (b* (((mv acl2::?erp
                 ?new-declspec ?new-type? ?new-tyspecs
                 ?new-storspecs ?return-types ?new-table)
             (valid-decl-spec declspec
                              type? tyspecs storspecs table ienv)))
         (type-spec-list-unambp new-tyspecs))))

Theorem: not-type-and-type-specs-of-valid-decl-spec

(defthm not-type-and-type-specs-of-valid-decl-spec
  (implies
       (not (and type? tyspecs))
       (b* (((mv acl2::?erp
                 ?new-declspec ?new-type? ?new-tyspecs
                 ?new-storspecs ?return-types ?new-table)
             (valid-decl-spec declspec
                              type? tyspecs storspecs table ienv)))
         (not (and new-type? new-tyspecs)))))

Theorem: not-type-specs-of-valid-decl-spec-when-type

(defthm not-type-specs-of-valid-decl-spec-when-type
  (implies
       (not (and type? tyspecs))
       (b* (((mv acl2::?erp
                 ?new-declspec ?new-type? ?new-tyspecs
                 ?new-storspecs ?return-types ?new-table)
             (valid-decl-spec declspec
                              type? tyspecs storspecs table ienv)))
         (implies new-type? (not new-tyspecs)))))

Theorem: valid-decl-spec.new-storspecs-type-prescription

(defthm valid-decl-spec.new-storspecs-type-prescription
  (b* (((mv acl2::?erp
            ?new-declspec ?new-type? ?new-tyspecs
            ?new-storspecs ?return-types ?new-table)
        (valid-decl-spec declspec
                         type? tyspecs storspecs table ienv)))
    (true-listp new-storspecs))
  :rule-classes :type-prescription)