Exprs/decls
Fixtypes of expressions, declarations, and related entities
[C:6.5] [C:6.6] [C:6.7] [C:A.2.1] [C:A.2.2].
The grammar in [C] defines expressions and declarations
via a large and complex collection of mutually recursive rules.
We use a corresponding collection of mutually recursive fixtypes,
which take a few seconds to process on fast machines.
A few fixtypes related to declarations
are actually outside this mutual recursion,
because they are not mutually recursive with others.
For instance, the fixtype type-qual for type qualifiers
is defined before these mutually recursive fixtypes,
and the fixtype decl for (top-level) declarations
is defined after these mutually recursive fixtypes.
As is sometimes the case with mutually recursive fixtypes,
we need to add :base-case-override to some sum fixtypes,
as well as :measure with two-nats-measure to all the fixtypes.
For instance, genassoc does not have a clear base case,
and thus we specify to use the :default case of this sum fixtype.
But then the accessor genassoc-default->expr must always return
an expression that is smaller than its input,
even when its input is not a genassoc value,
but any ACL2 value, including atoms.
In order to achieve that,
we add a second lexicographic component to the measure,
making a genassoc always larger than an expr
when the two have the same ACL2-count
(which is the case when they are certain atoms).
There are some additional patterns
in the use of this second lexicographic components:
a fty::defoption
has one more than the base fixtype;
a fty::defprod
has one more than the component fixtypes.
There is one instance in which it does not seem possible
to find appropriate second lexicographic components:
in a dirabsdeclor, all the cases except :paren
contain an dirabsdeclor-option,
which as discussed above must have a larger second lexicographic component;
thus the only possible base case is :paren,
which contains an absdeclor,
and so it must have a larger second lexicographic component,
but absdeclor is a fty::defprod
containing an dirabsdeclor,
which in turn must have a larger second lexicographic component.
Thus, we add a dummy base case :dummy-base to dirabsdeclor,
whch is unfortunate but perhaps unavoidable.
We will prohibit the occurrence of :dummy-base via separate checks.
Subtopics
- Expr
- Fixtype of expressions [C:6.5] [C:A.2.1].
- Type-spec
- Fixtype of type specifiers [C:6.7.3] [C:A.2.2].
- Amb-expr/tyname
- Fixtype of ambiguous expressions or type names.
- Dirdeclor
- Fixtype of direct declarators [C:6.7.6] [C:A.2.2].
- Attrib
- Fixtype of GCC attributes.
- Dirabsdeclor
- Fixtype of direct abstract declarators [C:6.7.7] [C:A.2.2].
- Amb-declor/absdeclor
- Fixtype of ambiguous declarators or abstract declarators.
- Paramdeclor
- Fixtype of parameter declarators [C:6.7.6] [C:A.2.2].
- Structdecl
- Fixtype of structure declarations [C:6.7.2.1] [C:A.2.2].
- Declspec
- Fixtype of declaration specifiers [C:6.7] [C:A.2.2].
- Declor
- Fixtype of declarators [C:6.7.6] [C:A.2.2].
- Absdeclor
- Fixtype of abstract declarators [C:6.7.7] [C:A.2.2].
- Align-spec
- Fixtype of alignment specifiers [C:6.7.5] [C:A.2.2].
- Spec/qual
- Fixtype of type specifiers and type qualifiers
[C:6.7.2.1] [C:A.2.2].
- Expr-option
- Fixtype of optional expressions.
- Strunispec
- Fixtype of structure or union specifiers [C:6.7.2.1] [C:A.2.2].
- Dirabsdeclor-option
- Fixtype of optional direct abstract declarators.
- Desiniter
- Fixtype of initializers with optional designations
[C:6.7.9] [C:A.2.2].
- Attrib-spec
- Fixtype of GCC attribute specifiers.
- Tyname
- Fixtype of type names [C:6.7.7] [C:A.2.2].
- Structdeclor
- Fixtype of structure declarators [C:6.7.2.1] [C:A.2.2].
- Const-expr-option
- Fixtype of optional constant expressions.
- Statassert
- Fixtype of static assertion declarations [C:6.7.10] [C:A.2.2].
- Enumspec
- Fixtype of enumeration specifiers [C:6.7.2.2] [C:A.2.2].
- Absdeclor-option
- Fixtype of optional abstract declarators [C:6.7.7] [C:A.2.2].
- Paramdecl
- Fixtype of parameter declarations [C:6.7.6] [C:A.2.2].
- Initer-option
- Fixtype of optional initializers.
- Initer
- Fixtype of initializers [C:6.7.9] [C:A.2.2].
- Declor-option
- Fixtype of optional declarators.
- Const-expr
- Fixtype of constant expressions [C:6.6] [C:A.2.1].
- Genassoc
- Fixtype of generic associations [C:6.5.1.1] [C:A.2.1].
- Designor
- Fixtype of designators [C:6.7.9] [C:A.2.2].
- Enumer
- Fixtype of enumerators [C:6.7.2.2] [C:A.2.2].
- Spec/qual-list
- Fixtype of lists of type specifiers and type qualifiers.
- Declspec-list
- Fixtype of lists of declaration specifiers.
- Structdeclor-list
- Fixtype of lists of structure declarators.
- Structdecl-list
- Fixtype of lists of structure declarations.
- Paramdecl-list
- Fixtype of lists of parameter declarations.
- Genassoc-list
- Fixtype of lists of generic associations.
- Desiniter-list
- Fixtype of lists of initializers with designations.
- Enumer-list
- Fixtype of lists of enumerators.
- Expr-list
- Fixtype of lists of expressions.
- Attrib-spec-list
- Fixtype of lists of GCC attribute specifiers.
- Designor-list
- Fixtype of lists of designators.
- Attrib-list
- Fixtype of lists of GCC attributes.