Abstract-syntax-irrelevants
Irrelevant values of the abstract syntax fixtypes.
These are nullary operations that return
``irrelevant'' values of the fixtypes that form the abstract syntax,
i.e. values that are never actually used.
For instance, an ACL2 function that returns multiple results,
the first one of which is an error indication,
while the other results include abstract syntax entities,
could return irrelevant values as the latter results
when the first result indicates an error.
The definitions are mostly boilerplate,
except that in some places we put something conveying irrelevance,
e.g. in the definition of irr-ident.
However, this is really unnecessary, and it should be possible to
define all of these according to boilerplate.
This could be an extension of the FTY library;
perhaps every fixtype definition could also generate
some kind of ``default'' value of the fixtype,
which could be used as an irrelevant value in the sense explained above.
For now, we collect these nullary functions in this file and XDOC topic,
to keep the file and XDOC topic of the abstract syntax tidier.
Note that some fixtypes do not have an irrelevant value defined here,
because there are already very short built-in values that can be used,
such as nil for list and option types.
Subtopics
- Irr-amb?-declor/absdeclor
- An irrelevant possibly ambiguous declarators or abstract declarators.
- Irr-typequal/attribspec
- An irrelevant type qualifier or attribute specifier.
- Irr-amb?-expr/tyname
- An irrelevant possibly ambiguous expression or type name.
- Irr-amb?-declon/stmt
- An irrelevant possibly ambiguous declaration or statement.
- Irr-transunit-ensemble
- An irrelevant ensemble of translation units.
- Irr-struni-spec
- An irrelevant structure or union specifier.
- Irr-struct-declor
- An irrelevant structure declarator.
- Irr-struct-declon
- An irrelevant structure declaration.
- Irr-statassert
- An irrelevant static assertion declaration.
- Irr-param-declon
- An irrelevant parameter declaration.
- Irr-member-designor
- An irrelevant member designator.
- Irr-init-declor
- An irrelevant initializer declarator.
- Irr-hex-quad
- An irrelevant quadruple of hexadecimal digits.
- Irr-fundef
- An irrelevant function definition.
- Irr-dirabsdeclor
- An irrelevant direct abstract declarator.
- Irr-desiniter
- An irrelevant initializer with optional designation.
- Irr-declor/absdeclor
- An irrelevant declarator or abstract declarator.
- Irr-declon/stmt
- An irrelevant declaration or statement.
- Irr-asm-stmt
- An irrelevant assembler statement.
- Irr-asm-output
- An irrelevant assembler output operand.
- Irr-asm-name-spec
- An irrelevant assembler name specifier.
- Irr-asm-input
- An irrelevant assembler input operand.
- Irr-type-spec
- An irrelevant type specifier.
- Irr-type-qual
- An irrelevant type qualifier.
- Irr-transunit
- An irrelevant translation unit.
- Irr-stringlit
- An irrelevant string literal.
- Irr-stor-spec
- An irrelevant storage class specifier.
- Irr-spec/qual
- An irrelevant type specifier or type qualifier.
- Irr-param-declor
- An irrelevant parameter declarator.
- Irr-ident
- An irrelevant identifier.
- Irr-iconst
- An irrelevant integer constant.
- Irr-header-name
- An irrelevant header name.
- Irr-genassoc
- An irrelevant generic association.
- Irr-fun-spec
- An irrelevant function specifier.
- Irr-ext-declon
- An irrelevant external declaration.
- Irr-expr/tyname
- An irrelevant expression or type name.
- Irr-enumer
- An irrelevant enumerator.
- Irr-enum-spec
- An irrelevant enumeration specifier.
- Irr-dirdeclor
- An irrelevant direct declarator.
- Irr-dexprefix
- An irrelevant decimal exponent prefix.
- Irr-dexpo
- An irrelevant decimal exponent.
- Irr-designor
- An irrelevant designator.
- Irr-declor
- An irrelevant declarator.
- Irr-declon
- An irrelevant declaration.
- Irr-decl-spec
- An irrelevant declaration specifier.
- Irr-const-expr
- An irrelevant constant expression.
- Irr-comp-stmt
- An irrelevant compound statement.
- Irr-block-item
- An irrelevant block item.
- Irr-bexprefix
- An irrelevant binary exponent prefix.
- Irr-bexpo
- An irrelevant binary exponent.
- Irr-attrib-spec
- An irrelevant attribute specifier.
- Irr-attrib-name
- An irrelevant attribute name.
- Irr-asm-qual
- An irrelevant assembler qualifier.
- Irr-asm-clobber
- An irrelevant assembler clobber.
- Irr-align-spec
- An irrelevant alignment specifier.
- Irr-absdeclor
- An irrelevant abstract declarator.
- Irr-unop
- An irrelevant unary operator.
- Irr-tyname
- An irrelevant type name.
- Irr-stmt
- An irrelevant statement.
- Irr-label
- An irrelevant label.
- Irr-initer
- An irrelevant initializer.
- Irr-expr
- An irrelevant expression.
- Irr-escape
- An irrelevant escape.
- Irr-const
- An irrelevant constant.
- Irr-binop
- An irrelevant binary operator.
- Irr-attrib
- An irrelevant attribute.
