Dimb-decl-spec
Disambiguate a declaration specifier.
- Signature
(dimb-decl-spec declspec kind table)
→
(mv erp new-declspec new-kind new-table)
- Arguments
- declspec — Guard (decl-specp declspec).
- kind — Guard (dimb-kindp kind).
- table — Guard (dimb-tablep table).
- Returns
- new-declspec — Type (decl-specp new-declspec).
- new-kind — Type (dimb-kindp new-kind).
- new-table — Type (dimb-tablep new-table).
Declaration specifiers (may) precede declarators,
which add identifiers to the current scope.
For our disambiguation purposes,
we need to determine which dimb-kind
those identifiers denote, which, for declarators,
is either :objfun or :typedef.
It is :typedef if the list of declaration specifiers
includes the typedef storage class specifier;
otherwise, it is :objfun.
Thus, when going through the declaration specifiers,
we initialize the kind to :objfun,
and change it to :typedef if we encounter a typedef.
This is why this ACL2 function takes and returns
a disambiguation kind, i.e. a value of type dimb-kind.
