		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Tyspec+declor-to-ident+tyname

Turn a type specifier sequence and an object declarator into an identifier and a type name.

Signature
(tyspec+declor-to-ident+tyname tyspec declor) → (mv id tyname)
Arguments: tyspec — Guard (tyspecseqp tyspec).; declor — Guard (obj-declorp declor).
Returns: id — Type (identp id).; tyname — Type (tynamep tyname).

We decompose the declarator into an identifier and an abstract declarator, and we form a type name with the latter and the type specifier sequence.

The name of this ACL2 function does not mention obj explicitly, but the fact that it deals with object declarators is implicit in the fact that it returns an identifier and a type name.

In essence, we turn (the constituents of) an object declaration into its name and type, which are somewhat mixed in the C syntax.

Definitions and Theorems

Function: tyspec+declor-to-ident+tyname

(defun tyspec+declor-to-ident+tyname (tyspec declor)
  (declare (xargs :guard (and (tyspecseqp tyspec)
                              (obj-declorp declor))))
  (let ((__function__ 'tyspec+declor-to-ident+tyname))
    (declare (ignorable __function__))
    (b* (((mv id adeclor)
          (obj-declor-to-ident+adeclor declor)))
      (mv id
          (make-tyname :tyspec tyspec
                       :declor adeclor)))))

Theorem: identp-of-tyspec+declor-to-ident+tyname.id

(defthm identp-of-tyspec+declor-to-ident+tyname.id
  (b* (((mv acl2::?id ?tyname)
        (tyspec+declor-to-ident+tyname tyspec declor)))
    (identp id))
  :rule-classes :rewrite)

Theorem: tynamep-of-tyspec+declor-to-ident+tyname.tyname

(defthm tynamep-of-tyspec+declor-to-ident+tyname.tyname
  (b* (((mv acl2::?id ?tyname)
        (tyspec+declor-to-ident+tyname tyspec declor)))
    (tynamep tyname))
  :rule-classes :rewrite)

Theorem: tyspec+declor-to-ident+tyname-of-tyspecseq-fix-tyspec

(defthm tyspec+declor-to-ident+tyname-of-tyspecseq-fix-tyspec
  (equal (tyspec+declor-to-ident+tyname (tyspecseq-fix tyspec)
                                        declor)
         (tyspec+declor-to-ident+tyname tyspec declor)))

Theorem: tyspec+declor-to-ident+tyname-tyspecseq-equiv-congruence-on-tyspec

(defthm
 tyspec+declor-to-ident+tyname-tyspecseq-equiv-congruence-on-tyspec
 (implies
      (tyspecseq-equiv tyspec tyspec-equiv)
      (equal (tyspec+declor-to-ident+tyname tyspec declor)
             (tyspec+declor-to-ident+tyname tyspec-equiv declor)))
 :rule-classes :congruence)

Theorem: tyspec+declor-to-ident+tyname-of-obj-declor-fix-declor

(defthm tyspec+declor-to-ident+tyname-of-obj-declor-fix-declor
 (equal
      (tyspec+declor-to-ident+tyname tyspec (obj-declor-fix declor))
      (tyspec+declor-to-ident+tyname tyspec declor)))

Theorem: tyspec+declor-to-ident+tyname-obj-declor-equiv-congruence-on-declor

(defthm
 tyspec+declor-to-ident+tyname-obj-declor-equiv-congruence-on-declor
 (implies
      (obj-declor-equiv declor declor-equiv)
      (equal (tyspec+declor-to-ident+tyname tyspec declor)
             (tyspec+declor-to-ident+tyname tyspec declor-equiv)))
 :rule-classes :congruence)