|
|
|---|
|
|
|
|---|
Fixtype of identifiers [C17:6.4.2] [C17:A.1.3].
This is a product type introduced by fty::defprod.
This corresponds to identifier in the grammar in [C17]. In this abstract syntax, we allow any ACL2 values as C identifiers. We wrap these arbitrary values into a one-component product fixtype so that we can more easily distinguish identifiers from other things.
Allowing arbitrary values as identifiers provides flexibility. For instance, a transformation on C code could introduce multiple versions of certain identifiers, indexed by numbers, in which case we could use pairs consisting of the original identifiers and the indices.
We plan to define, separately, predicates that restrict identifiers to certain forms, used for parsing, printing, transformations, etc. Restrictions are needed to print this abstract syntax into a form where identifiers respect the restrictions in [C17]; in addition, parsing code compliant to [C17] will result in specific forms of identifiers.