Exprs/decls/stmts
Fixtypes of expressions, declarations, statements,
and related entities
[C17:6.5] [C17:6.6] [C17:6.7] [C17:6.8]
[C17:A.2.1] [C17:A.2.2] [C17:A.2.3].
The grammar in [C17] defines expressions and declarations
via a large and complex collection of mutually recursive rules;
statements are not mutualy recursive with expressions and declarations.
However, GCC extensions include statement expressions,
i.e. the ability to use a parenthesized (compound) statement
as an expression:
this extends the mutual recursion to statements.
Here we want to capture GCC extensions,
so we define a collection of mutually recursive fixtypes
for expressions, declarations, statements, and related entities;
this takes 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.
Also, external declarations are defined outside the recursion,
after these mutualy 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 [C17:6.5] [C17:A.2.1].
- Type-spec
- Fixtype of type specifiers [C17:6.7.3] [C17:A.2.2].
- Stmt
- Fixtype of statements [C17:6.8] [C17:A.2.3].
- Amb-expr/tyname
- Fixtype of ambiguous expressions or type names.
- Dirdeclor
- Fixtype of direct declarators [C17:6.7.6] [C17:A.2.2].
- Asm-stmt
- Fixtype of assembler statements.
- Attrib
- Fixtype of GCC attributes.
- Amb-decl/stmt
- Fixtype of ambiguous declarations or statements.
- Dirabsdeclor
- Fixtype of direct abstract declarators [C17:6.7.7] [C17:A.2.2].
- Decl-spec
- Fixtype of declaration specifiers [C17:6.7] [C17:A.2.2].
- Structdecl
- Fixtype of structure declarations [C17:6.7.2.1] [C17:A.2.2].
- Amb-declor/absdeclor
- Fixtype of ambiguous declarators or abstract declarators.
- Param-declor
- Fixtype of parameter declarators [C17:6.7.6] [C17:A.2.2].
- Declor
- Fixtype of declarators [C17:6.7.6] [C17:A.2.2].
- Tyname
- Fixtype of type names [C17:6.7.7] [C17:A.2.2].
- Absdeclor
- Fixtype of abstract declarators [C17:6.7.7] [C17:A.2.2].
- Struni-spec
- Fixtype of structure or union specifiers [C17:6.7.2.1] [C17:A.2.2].
- Align-spec
- Fixtype of alignment specifiers [C17:6.7.5] [C17:A.2.2].
- Label
- Fixtype of labels [C17:6.8.1] [C17:A.2.3].
- Expr-option
- Fixtype of optional expressions.
- Spec/qual
- Fixtype of specifiers and qualifiers
[C17:6.7.2.1] [C17:A.2.2].
- Desiniter
- Fixtype of initializers with optional designations
[C17:6.7.9] [C17:A.2.2].
- Dirabsdeclor-option
- Fixtype of optional direct abstract declarators.
- Initdeclor
- Fixtype of initializer declarators [C17:6.7] [C17:A.2.2].
- Const-expr-option
- Fixtype of optional constant expressions.
- Attrib-spec
- Fixtype of GCC attribute specifiers.
- Structdeclor
- Fixtype of structure declarators [C17:6.7.2.1] [C17:A.2.2].
- Decl
- Fixtype of declarations [C17:6.7] [C17:A.2.2].
- Absdeclor-option
- Fixtype of optional abstract declarators [C17:6.7.7] [C17:A.2.2].
- Statassert
- Fixtype of static assertion declarations [C17:6.7.10] [C17:A.2.2].
- Param-declon
- Fixtype of parameter declarations [C17:6.7.6] [C17:A.2.2].
- Member-designor
- Fixtype of member designators.
- Initer-option
- Fixtype of optional initializers.
- Initer
- Fixtype of initializers [C17:6.7.9] [C17:A.2.2].
- Enumspec
- Fixtype of enumeration specifiers [C17:6.7.2.2] [C17:A.2.2].
- Declor-option
- Fixtype of optional declarators.
- Const-expr
- Fixtype of constant expressions [C17:6.6] [C17:A.2.1].
- Block-item
- Fixtype of block items [C17:6.8.2] [C17:A.2.3].
- Genassoc
- Fixtype of generic associations [C17:6.5.1.1] [C17:A.2.1].
- Asm-output
- Fixtype of assembler output operands.
- Asm-input
- Fixtype of assembler input operands.
- Enumer
- Fixtype of enumerators [C17:6.7.2.2] [C17:A.2.2].
- Designor
- Fixtype of designators [C17:6.7.9] [C17:A.2.2].
- Typequal/attribspec
- Fixtype of type qualifiers and attribute specifiers.
- Typequal/attribspec-list
- Fixtype of lists of type qualifiers and attribute specifiers.
- Decl-spec-list
- Fixtype of lists of declaration specifiers.
- Spec/qual-list
- Fixtype of lists of specifiers and qualifiers.
- Desiniter-list
- Fixtype of lists of initializers with optional designations.
- Param-declon-list
- Fixtype of lists of parameter declarations.
- Decl-list
- Fixtype of lists of declarations.
- Block-item-list
- Fixtype of lists of block items.
- Typequal/attribspec-list-list
- Fixtype of lists of lists of
type qualifiers and attribute specifiers.
- Structdeclor-list
- Fixtype of lists of structure declarators.
- Structdecl-list
- Fixtype of lists of structure declarations.
- Initdeclor-list
- Fixtype of lists of initializer declarators.
- Genassoc-list
- Fixtype of lists of generic associations.
- Enumer-list
- Fixtype of lists of enumerators.
- Attrib-spec-list
- Fixtype of lists of GCC attribute specifiers.
- Expr-list
- Fixtype of lists of expressions.
- Asm-output-list
- Fixtype of lists of assembler output operands.
- Asm-input-list
- Fixtype of lists of assembler input operands.
- Designor-list
- Fixtype of lists of designators.
- Attrib-list
- Fixtype of lists of GCC attributes.
