Disambiguate a list of parameter declarations to a list of names, if appropriate.
(dimb-params-to-names params fundefp table) → (mv yes/no 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
[C:6.7.6.3/3].
This is indicated by the flag
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
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
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, whieh may be empty. If the check for any element of the list, the re-classification fails, and the caller will do its own processing and disamguation of the (non-empty) list of parameter declarations, which will then remain parameter declarations (not names) after that processing and disambiguation.
Function:
(defun dimb-params-to-names-loop (params table) (declare (xargs :guard (and (paramdecl-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 (paramdeclor-case (paramdecl->decl param) :none)) (mv nil nil)) (declspecs (paramdecl->spec param)) ((unless (and (consp declspecs) (endp (cdr declspecs)))) (mv nil nil)) (declspec (car declspecs)) ((unless (declspec-case declspec :tyspec)) (mv nil nil)) (tyspec (declspec-tyspec->unwrap declspec)) ((unless (tyspec-case tyspec :tydef)) (mv nil nil)) (ident (tyspec-tydef->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:
(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:
(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:
(defthm dimb-params-to-names-loop-of-paramdecl-list-fix-params (equal (dimb-params-to-names-loop (paramdecl-list-fix params) table) (dimb-params-to-names-loop params table)))
Theorem:
(defthm dimb-params-to-names-loop-paramdecl-list-equiv-congruence-on-params (implies (paramdecl-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:
(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:
(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:
(defun dimb-params-to-names (params fundefp table) (declare (xargs :guard (and (paramdecl-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:
(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:
(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:
(defthm dimb-params-to-names-of-paramdecl-list-fix-params (equal (dimb-params-to-names (paramdecl-list-fix params) fundefp table) (dimb-params-to-names params fundefp table)))
Theorem:
(defthm dimb-params-to-names-paramdecl-list-equiv-congruence-on-params (implies (paramdecl-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:
(defthm dimb-params-to-names-of-bool-fix-fundefp (equal (dimb-params-to-names params (acl2::bool-fix fundefp) table) (dimb-params-to-names params fundefp table)))
Theorem:
(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:
(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:
(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)