		Search-engine friendly clone of the ACL2 documentation.

Disambiguator

Dimb-params-to-names

Disambiguate a list of parameter declarations to a list of names, if appropriate.

Signature
(dimb-params-to-names params fundefp table) → (mv yes/no names)
Arguments: params — Guard (param-declon-listp params).; fundefp — Guard (booleanp fundefp).; table — Guard (dimb-tablep table).
Returns: yes/no — Type (booleanp yes/no).; names — Type (ident-listp names).

There are two kinds of direct function declarators, both in the grammar and in the abstract syntax: one has a (non-empty) list of parameter declarations optionally followed by ellipsis; the other has a possibly empty list of names.

The second kind is allowed to be non-empty only if the function declarator is part of a function definition [C17:6.7.6.3/3]. This is indicated by the flag fundefp passed to this ACL2 function.

The parser always creates the first kind, because a name, which is an identifier, is syntactically ambiguous: it could be a parameter name, or it could be a typedef name. Also, if there are no parameters, the parser does not bother creating the second kind of declarator: it creates an empty list of parameter declarations, because this needs to be disambiguated anyhow.

This ACL2 function checks whether a possibly empty list of parameter declarations should in fact be a list of names. This is the case when either the list is empty, or the fundefp flag is t and every parameter declaration consists of a single type specifier consisting of a typedef name, but that identifier does not identify a typedef name in scope. This means that, for example, if we have two identifiers x and y, one of which is a typedef name but the other one is not, the re-classification to names fails. [C17:6.7.6.3/11] says that typedef names have priority, but strictly speaking it mentions only parameter declarations, not also identifier lists; nonetheless, some simple experiments with GCC show that this priority of typedef names also applies to the choice between parameter declarations and identifier lists, and not just within parameter declarations (this aspect is dealt with elsewhere, in the code to disambiguate parameter declarations). So, in the example above with x and y, the code is in fact invalid.

This ACL2 function returns a boolean saying whether the parameter declarations are re-classified into names, and in this case it also returns the list of names, which may be empty. If the check fails for any element of the list, the re-classification fails, and the caller will do its own processing and disambiguation of the (non-empty) list of parameter declarations, which will then remain parameter declarations (not names) after that processing and disambiguation.

Definitions and Theorems

Function: dimb-params-to-names-loop

(defun dimb-params-to-names-loop (params table)
  (declare (xargs :guard (and (param-declon-listp params)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-params-to-names-loop))
    (declare (ignorable __function__))
    (b* (((when (endp params)) (mv t nil))
         (param (car params))
         ((unless (param-declor-case (param-declon->declor param)
                                     :none))
          (mv nil nil))
         (declspecs (param-declon->specs param))
         ((unless (and (consp declspecs)
                       (endp (cdr declspecs))))
          (mv nil nil))
         (declspec (car declspecs))
         ((unless (decl-spec-case declspec :typespec))
          (mv nil nil))
         (tyspec (decl-spec-typespec->spec declspec))
         ((unless (type-spec-case tyspec :typedef))
          (mv nil nil))
         (ident (type-spec-typedef->name tyspec))
         (kind? (dimb-lookup-ident ident table))
         ((when (equal kind? (dimb-kind-typedef)))
          (mv nil nil))
         ((mv yes/no names)
          (dimb-params-to-names-loop (cdr params)
                                     table))
         ((unless yes/no) (mv nil nil)))
      (mv t (cons ident names)))))

Theorem: booleanp-of-dimb-params-to-names-loop.yes/no

(defthm booleanp-of-dimb-params-to-names-loop.yes/no
  (b* (((mv ?yes/no ?names)
        (dimb-params-to-names-loop params table)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: ident-listp-of-dimb-params-to-names-loop.names

(defthm ident-listp-of-dimb-params-to-names-loop.names
  (b* (((mv ?yes/no ?names)
        (dimb-params-to-names-loop params table)))
    (ident-listp names))
  :rule-classes :rewrite)

Theorem: dimb-params-to-names-loop-of-param-declon-list-fix-params

(defthm dimb-params-to-names-loop-of-param-declon-list-fix-params
  (equal (dimb-params-to-names-loop (param-declon-list-fix params)
                                    table)
         (dimb-params-to-names-loop params table)))

Theorem: dimb-params-to-names-loop-param-declon-list-equiv-congruence-on-params

(defthm
 dimb-params-to-names-loop-param-declon-list-equiv-congruence-on-params
 (implies (param-declon-list-equiv params params-equiv)
          (equal (dimb-params-to-names-loop params table)
                 (dimb-params-to-names-loop params-equiv table)))
 :rule-classes :congruence)

Theorem: dimb-params-to-names-loop-of-dimb-table-fix-table

(defthm dimb-params-to-names-loop-of-dimb-table-fix-table
  (equal (dimb-params-to-names-loop params (dimb-table-fix table))
         (dimb-params-to-names-loop params table)))

Theorem: dimb-params-to-names-loop-dimb-table-equiv-congruence-on-table

(defthm
     dimb-params-to-names-loop-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-params-to-names-loop params table)
                  (dimb-params-to-names-loop params table-equiv)))
  :rule-classes :congruence)

Function: dimb-params-to-names

(defun dimb-params-to-names (params fundefp table)
  (declare (xargs :guard (and (param-declon-listp params)
                              (booleanp fundefp)
                              (dimb-tablep table))))
  (let ((__function__ 'dimb-params-to-names))
    (declare (ignorable __function__))
    (b* (((when (endp params)) (mv t nil))
         ((unless fundefp) (mv nil nil)))
      (dimb-params-to-names-loop params table))))

Theorem: booleanp-of-dimb-params-to-names.yes/no

(defthm booleanp-of-dimb-params-to-names.yes/no
  (b* (((mv ?yes/no ?names)
        (dimb-params-to-names params fundefp table)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: ident-listp-of-dimb-params-to-names.names

(defthm ident-listp-of-dimb-params-to-names.names
  (b* (((mv ?yes/no ?names)
        (dimb-params-to-names params fundefp table)))
    (ident-listp names))
  :rule-classes :rewrite)

Theorem: dimb-params-to-names-of-param-declon-list-fix-params

(defthm dimb-params-to-names-of-param-declon-list-fix-params
  (equal (dimb-params-to-names (param-declon-list-fix params)
                               fundefp table)
         (dimb-params-to-names params fundefp table)))

Theorem: dimb-params-to-names-param-declon-list-equiv-congruence-on-params

(defthm
  dimb-params-to-names-param-declon-list-equiv-congruence-on-params
 (implies (param-declon-list-equiv params params-equiv)
          (equal (dimb-params-to-names params fundefp table)
                 (dimb-params-to-names params-equiv fundefp table)))
 :rule-classes :congruence)

Theorem: dimb-params-to-names-of-bool-fix-fundefp

(defthm dimb-params-to-names-of-bool-fix-fundefp
  (equal (dimb-params-to-names params (bool-fix fundefp)
                               table)
         (dimb-params-to-names params fundefp table)))

Theorem: dimb-params-to-names-iff-congruence-on-fundefp

(defthm dimb-params-to-names-iff-congruence-on-fundefp
 (implies (iff fundefp fundefp-equiv)
          (equal (dimb-params-to-names params fundefp table)
                 (dimb-params-to-names params fundefp-equiv table)))
 :rule-classes :congruence)

Theorem: dimb-params-to-names-of-dimb-table-fix-table

(defthm dimb-params-to-names-of-dimb-table-fix-table
 (equal (dimb-params-to-names params fundefp (dimb-table-fix table))
        (dimb-params-to-names params fundefp table)))

Theorem: dimb-params-to-names-dimb-table-equiv-congruence-on-table

(defthm dimb-params-to-names-dimb-table-equiv-congruence-on-table
 (implies (dimb-table-equiv table table-equiv)
          (equal (dimb-params-to-names params fundefp table)
                 (dimb-params-to-names params fundefp table-equiv)))
 :rule-classes :congruence)