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 tyqual 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].
- Tyspec
- 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].
- 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].
- Declor
- Fixtype of declarators [C:6.7.6] [C:A.2.2].
- Alignspec
- Fixtype of alignment specifiers [C:6.7.5] [C:A.2.2].
- Declspec
- Fixtype of declaration specifiers [C:6.7] [C:A.2.2].
- Strunispec
- Fixtype of structure or union specifiers [C:6.7.2.1] [C:A.2.2].
- Expr-option
- Fixtype of optional expressions.
- Dirabsdeclor-option
- Fixtype of optional direct abstract declarators.
- Desiniter
- Fixtype of initializers with optional designations
[C:6.7.9] [C:A.2.2].
- Absdeclor
- Fixtype of abstract declarators [C:6.7.7] [C:A.2.2].
- Structdeclor
- Fixtype of structure declarators [C:6.7.2.1] [C:A.2.2].
- Specqual
- Fixtype of type specifiers and type qualifiers
[C:6.7.2.1] [C:A.2.2].
- Const-expr-option
- Fixtype of optional constant expressions.
- 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].
- Tyname
- Fixtype of type names [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.
- Declor-option
- Fixtype of optional declarators.
- Initer
- Fixtype of initializers [C:6.7.9] [C:A.2.2].
- 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].
- Statassert
- Fixtype of static assertion declarations [C:6.7.10] [C:A.2.2].
- 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].
- Declspec-list
- Fixtype of lists of declaration specifiers.
- Specqual-list
- Fixtype of lists of type specifiers and type qualifiers.
- 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.
- Designor-list
- Fixtype of lists of designators.