		Search-engine friendly clone of the ACL2 documentation.

Valid-spec/qual

Validate a specifier or qualifier.

Signature
(valid-spec/qual specqual type? tyspecs table ienv) → (mv erp new-specqual new-type? new-tyspecs return-types new-table)
Arguments: specqual — Guard (spec/qual-p specqual).; type? — Guard (type-optionp type?).; tyspecs — Guard (type-spec-listp tyspecs).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; new-specqual — Type (spec/qual-p new-specqual).; new-type? — Type (type-optionp new-type?).; new-tyspecs — Type (type-spec-listp new-tyspecs).; return-types — Type (type-setp return-types).; new-table — Type (valid-tablep new-table).

For now we ignore type qualifiers [C17:6.7.3], as they do not have any impact on our approximate type system. We validate alignment specifiers (in a separate validation function), but make no use of them in our approximate type system. Thus, the validation of a specifier or qualifier returns the same results as the validation of a type specifier (see valid-type-spec). For now we also skip over attributes completely; see the ABNF grammar for specifier-qualifier-list.

Definitions and Theorems

Theorem: type-spec-list-unambp-of-valid-spec/qual

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

Theorem: not-type-and-type-specs-of-valid-spec/qual

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

Theorem: not-type-specs-of-valid-spec/qual-when-type

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