		Search-engine friendly clone of the ACL2 documentation.

Valid-designor

Validate a designator.

Signature
(valid-designor designor target-type table ienv) → (mv erp new-designor new-target-type return-types new-table)
Arguments: designor — Guard (designorp designor).; target-type — Guard (typep target-type).; table — Guard (valid-tablep table).; ienv — Guard (ienvp ienv).
Returns: new-designor — Type (designorp new-designor).; new-target-type — Type (typep new-target-type).; return-types — Type (type-setp return-types).; new-table — Type (valid-tablep new-table).

The target type passed as input is the one that the designator must apply to; the target type returned as result is the one that results from applying the designator to it. The target type is the type of the current object [C:6.7.9/17]. A subscript designator requires an array target type, and must have an integer expression [C:6.7.9/6]; the result is the unknown type, because currently we have just one array type without information about the element type. A dotted designator requires a struct or union type [C:6.7.9/7]; the result is the unknown type, because currently we do not have information about the members.

Definitions and Theorems

Theorem: valid-designor.new-target-type-not-function

(defthm valid-designor.new-target-type-not-function
  (b* (((mv acl2::?erp
            ?new-designor ?new-target-type
            ?return-types ?new-table)
        (valid-designor designor target-type table ienv)))
    (implies (not erp)
             (not (equal (type-kind new-target-type)
                         :function)))))

Theorem: valid-designor.new-target-type-not-void

(defthm valid-designor.new-target-type-not-void
  (b* (((mv acl2::?erp
            ?new-designor ?new-target-type
            ?return-types ?new-table)
        (valid-designor designor target-type table ienv)))
    (implies (not erp)
             (not (equal (type-kind new-target-type)
                         :void)))))