		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Tyname-formalp

Check if a type name has formal dynamic semantics.

Signature
(tyname-formalp tyname) → yes/no
Arguments: tyname — Guard (tynamep tyname).
Returns: yes/no — Type (booleanp yes/no).

In the abstract syntax of the formal language definition, type names are only used in cast expressions, which are required by c::eval-cast to denote integer types (except the plain char type) in order to be supported. Thus we need to ensure that the list of type specifiers and qualifiers only contains supported type specifier sequences corresponding to those types, and that there is no abstract declarator. We must also ensure that there are no type qualifiers, which are not supported in the formal semantics.

Definitions and Theorems

Function: tyname-formalp

(defun tyname-formalp (tyname)
  (declare (xargs :guard (tynamep tyname)))
  (declare (xargs :guard (tyname-unambp tyname)))
  (let ((__function__ 'tyname-formalp))
    (declare (ignorable __function__))
    (b* (((tyname tyname) tyname)
         ((mv okp tyspecs)
          (check-spec/qual-list-all-typespec tyname.specqual)))
      (and okp
           (type-spec-list-integer-formalp tyspecs)
           (not tyname.decl?)))))

Theorem: booleanp-of-tyname-formalp

(defthm booleanp-of-tyname-formalp
  (b* ((yes/no (tyname-formalp tyname)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: tyname-formalp-of-tyname-fix-tyname

(defthm tyname-formalp-of-tyname-fix-tyname
  (equal (tyname-formalp (tyname-fix tyname))
         (tyname-formalp tyname)))

Theorem: tyname-formalp-tyname-equiv-congruence-on-tyname

(defthm tyname-formalp-tyname-equiv-congruence-on-tyname
  (implies (tyname-equiv tyname tyname-equiv)
           (equal (tyname-formalp tyname)
                  (tyname-formalp tyname-equiv)))
  :rule-classes :congruence)