		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Tyspec+declor-to-ident+params+tyname

Turn a type specifier sequence and a function declarator into an identifier, a list of parameter declarations, and a type name.

Signature
(tyspec+declor-to-ident+params+tyname tyspec declor) → (mv id params tyname)
Arguments: tyspec — Guard (tyspecseqp tyspec).; declor — Guard (fun-declorp declor).
Returns: id — Type (identp id).; params — Type (param-declon-listp params).; 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 fun explicitly, but the fact that it deals with function declarators is implicit in the fact that it returns an identifier, a list of parameter declarations, and a type name.

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

The inverse of this is not well-defined for every type name, because the latter may include array declarators, which are not allowed in function declarators. We could define the inverse on type names that are restricted not to use array declarators; but we do not need the inverse for now.

Definitions and Theorems

Function: tyspec+declor-to-ident+params+tyname

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

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

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

Theorem: param-declon-listp-of-tyspec+declor-to-ident+params+tyname.params

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

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

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

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

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

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

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

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

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

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

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