		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Ident+tyname-to-tyspec+declor

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

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

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

Given an identifier and a type (name), this function provides the constituents for declaring it.

This is the inverse of tyspec+declor-to-ident+tyname.

Definitions and Theorems

Function: ident+tyname-to-tyspec+declor

(defun ident+tyname-to-tyspec+declor (id tyname)
  (declare (xargs :guard (and (identp id) (tynamep tyname))))
  (b* (((tyname tyname) tyname))
    (mv tyname.tyspec
        (ident+adeclor-to-obj-declor id tyname.declor))))

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

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

Theorem: obj-declorp-of-ident+tyname-to-tyspec+declor.declor

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

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

(defthm
     ident+tyname-to-tyspec+declor-of-tyspec+declor-to-ident+tyname
  (b* (((mv id tyname)
        (tyspec+declor-to-ident+tyname tyspec declor)))
    (equal (ident+tyname-to-tyspec+declor id tyname)
           (mv (tyspecseq-fix tyspec)
               (obj-declor-fix declor)))))

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

(defthm
     tyspec+declor-to-ident+tyname-of-ident+tyname-to-tyspec+declor
  (b* (((mv tyspec declor)
        (ident+tyname-to-tyspec+declor id tyname)))
    (equal (tyspec+declor-to-ident+tyname tyspec declor)
           (mv (ident-fix id)
               (tyname-fix tyname)))))

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

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

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

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

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

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

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

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